From 19fab10294e1b953d74258eeeb1880328e49789f Mon Sep 17 00:00:00 2001
From: William Mansky <mansky1@uic.edu>
Date: Sun, 24 Mar 2024 06:02:05 -0500
Subject: [PATCH] more progress on 32-bit examples

---
 floyd/compat.v                |  30 ++-
 floyd/forward.v               |   5 +-
 floyd/funspec_old.v           |   2 +-
 progs/io_dry.v                | 221 ++++++---------------
 progs/io_mem_dry.v            |   4 +-
 progs/io_os_connection.v      |  11 +-
 progs/list_dt.v               |   2 +-
 progs/verif_append.v          |  13 +-
 progs/verif_append2.v         | 217 ++++++++++----------
 progs/verif_bin_search.v      |   5 +-
 progs/verif_bst.v             |   8 +-
 progs/verif_bst_oo.v          |  27 +--
 progs/verif_even.v            |   7 +-
 progs/verif_int_or_ptr.v      |  24 +--
 progs/verif_io_mem.v          | 221 +++++++++++----------
 progs/verif_load_demo.v       |   6 +-
 progs/verif_logical_compare.v |  27 ++-
 progs/verif_merge.v           |   3 +-
 progs/verif_message.v         |   1 +
 progs/verif_object.v          |  94 +++++----
 progs/verif_objectSelf.v      | 359 ++++++++--------------------------
 progs/verif_objectSelfFancy.v |  20 +-
 progs/verif_odd.v             |   2 +-
 progs/verif_queue.v           |  11 +-
 progs/verif_queue2.v          |  15 +-
 progs/verif_reverse.v         |  13 +-
 progs/verif_stackframe_demo.v |   2 +-
 progs/verif_store_demo.v      |   6 +-
 progs/verif_sumarray2.v       |   2 -
 progs/verif_switch.v          |   7 +-
 progs/verif_tree.v            |  34 +---
 progs/verif_union.v           |  14 +-
 sha/spec_sha.v                |   6 +-
 33 files changed, 553 insertions(+), 866 deletions(-)

diff --git a/floyd/compat.v b/floyd/compat.v
index b1903fee6b..a79d8110d0 100644
--- a/floyd/compat.v
+++ b/floyd/compat.v
@@ -77,6 +77,34 @@ Notation "|> P" := (▷ P)%I
 Notation "P <--> Q" := (P ↔ Q)%I
   (at level 95, no associativity, only parsing) : bi_scope.
 
+Notation TT := (True)%I.
+Notation FF := (False)%I.
+
 Open Scope bi_scope.
 
-Definition pred_ext := @bi.equiv_entails_2 (iPropI (VSTΣ unit)).
+Definition pred_ext := @bi.equiv_entails_2.
+Definition andp_right := @bi.and_intro.
+Definition prop_right := @bi.pure_intro.
+Definition sepcon_derives := @bi.sep_mono.
+Definition andp_derives := @bi.and_mono.
+Definition sepcon_emp := @bi.sep_emp.
+Definition emp_sepcon := @bi.emp_sep.
+Definition sepcon_comm := @bi.sep_comm.
+Definition sepcon_assoc := @bi.sep_assoc.
+Definition allp_right := @bi.forall_intro.
+
+Fixpoint iter_sepcon2 {B1 B2} (p : B1 -> B2 -> mpred) l :=
+    match l with
+    | nil => fun l2 =>
+       match l2 with
+       | nil => emp
+       | _ => FF
+       end
+    | x :: xl => fun l' =>
+       match l' with
+       | nil => FF
+       | y :: yl => p x y * iter_sepcon2 p xl yl
+       end
+    end.
+
+Global Tactic Notation "inv" ident(H):= Coqlib.inv H.
diff --git a/floyd/forward.v b/floyd/forward.v
index 37b9686bcc..e4c597447f 100644
--- a/floyd/forward.v
+++ b/floyd/forward.v
@@ -4487,7 +4487,8 @@ Ltac start_function1 :=
                POST [ tint ] _) |- _ => idtac
     | s := ?spec' |- _ => check_canonical_funspec spec'
    end;
-   change (semax_body V G F s); subst s
+   change (semax_body V G F s); subst s;
+   unfold mk_funspec'
  end;
 (* let DependedTypeList := fresh "DependedTypeList" in*)
  unfold NDmk_funspec;
@@ -4498,7 +4499,7 @@ Ltac start_function1 :=
    match Pre with
    | (monPred_at (convertPre _ _ (fun i => _))) =>  intros Espec (*DependedTypeList*) i
    | (λne x, monPred_at match _ with (a,b) => _ end) => intros Espec (*DependedTypeList*) [a b]
-   | (λne i, _) => intros Espec (*DependedTypeList*) i
+   | (λne i, _) => intros Espec (*DependedTypeList*) i (* this seems to be named "a" no matter what *)
    end;
    simpl fn_body; simpl fn_params; simpl fn_return
  end;
diff --git a/floyd/funspec_old.v b/floyd/funspec_old.v
index 36f252f66e..eb169472ec 100644
--- a/floyd/funspec_old.v
+++ b/floyd/funspec_old.v
@@ -780,7 +780,7 @@ Admitted. (* might be true *)
 
 End mpred.
 
-Ltac rewrite_old_main_pre ::= rewrite ?old_main_pre_eq; unfold convertPre.
+Ltac rewrite_old_main_pre ::= rewrite ?old_main_pre_eq; unfold convertPre, convertPre'.
 
 Ltac prove_all_defined := 
  red; simpl makePARAMS;
diff --git a/progs/io_dry.v b/progs/io_dry.v
index 2921a9ec0d..5b2c6b5a9c 100644
--- a/progs/io_dry.v
+++ b/progs/io_dry.v
@@ -3,18 +3,15 @@ Require Import VST.progs.io.
 Require Import VST.floyd.proofauto.
 Require Import VST.sepcomp.extspec.
 Require Import VST.veric.semax_ext.
-Require Import VST.veric.juicy_mem.
-Require Import VST.veric.compcert_rmaps.
-Require Import VST.veric.initial_world.
-Require Import VST.veric.ghost_PCM.
 Require Import VST.veric.SequentialClight.
-Require Import VST.concurrency.conclib.
 Require Import VST.progs.dry_mem_lemmas.
 
 Section IO_Dry.
 
 Context {E : Type -> Type} {IO_E : @IO_event nat -< E}.
 
+Notation IO_itree := (@IO_itree E).
+
 Definition getchar_pre (m : mem) (witness : byte -> IO_itree) (z : IO_itree) :=
   let k := witness in (sutt eq (r <- read stdin;; k r) z).
 
@@ -30,172 +27,78 @@ Definition putchar_post (m0 m : mem) (r : int) (witness : byte * IO_itree) (z :
   (Int.signed r = -1 \/ Int.signed r = Byte.unsigned c) /\
   if eq_dec (Int.signed r) (-1) then sutt eq (write stdout c;; k) z else z = k.
 
-Context (ext_link : String.string -> ident).
-
-Instance Espec : OracleKind := IO_Espec ext_link.
+Existing Instance semax_lemmas.eq_dec_external_function.
 
-Definition io_ext_spec := OK_spec.
+Definition getchar_sig := {| sig_args := []; sig_res := Tret AST.Tint; sig_cc := cc_default |}.
+Definition putchar_sig := {| sig_args := [AST.Tint]; sig_res := Tret AST.Tint; sig_cc := cc_default |}.
 
-Program Definition io_dry_spec : external_specification mem external_function (@IO_itree E).
+Program Definition io_dry_spec : external_specification mem external_function IO_itree.
 Proof.
   unshelve econstructor.
   - intro e.
-    pose (ext_spec_type io_ext_spec e) as T; simpl in T.
-    destruct (oi_eq_dec _ _); [|destruct (oi_eq_dec _ _); [|exact False]];
-      match goal with T := (_ * ?A)%type |- _ => exact (mem * A)%type end.
+    destruct (eq_dec e (EF_external "putchar" putchar_sig)).
+    { exact (mem * (byte * IO_itree))%type. }
+    destruct (eq_dec e (EF_external "getchar" getchar_sig)).
+    { exact (mem * (byte -> IO_itree))%type. }
+    exact False%type.
   - simpl; intros.
-    destruct (oi_eq_dec _ _); [|destruct (oi_eq_dec _ _); [|contradiction]].
-    + destruct X as (m0 & _ & w).
-      exact (X1 = [Vubyte (fst w)] /\ m0 = X3 /\ putchar_pre X3 w X2).
-    + destruct X as (m0 & _ & w).
-      exact (X1 = [] /\ m0 = X3 /\ getchar_pre X3 w X2).
+    if_tac in X; [|if_tac in X; last contradiction]; destruct X as (m & w).
+    + exact (X1 = [Vubyte (fst w)] /\ m = X3 /\ putchar_pre X3 w X2).
+    + exact (X1 = [] /\ m = X3 /\ getchar_pre X3 w X2).
   - simpl; intros ??? ot ???.
-    destruct (oi_eq_dec _ _); [|destruct (oi_eq_dec _ _); [|contradiction]].
-    + destruct X as (m0 & _ & w).
-      destruct X1; [|exact False].
-      destruct v; [exact False | | exact False | exact False | exact False | exact False].
-      exact (ot <> AST.Tvoid /\ putchar_post m0 X3 i w X2).
-    + destruct X as (m0 & _ & w).
-      destruct X1; [|exact False].
-      destruct v; [exact False | | exact False | exact False | exact False | exact False].
-      exact (ot <> AST.Tvoid /\ getchar_post m0 X3 i w X2).
-  - intros; exact True.
+    if_tac in X; [|if_tac in X; last contradiction]; destruct X as (m0 & w).
+    + exact (exists r, X1 = Some (Vint r) /\ ot <> AST.Tvoid /\ putchar_post m0 X3 r w X2).
+    + exact (exists r, X1 = Some (Vint r) /\ ot <> AST.Tvoid /\ getchar_post m0 X3 r w X2).
+  - intros; exact True%type.
 Defined.
 
-Definition dessicate : forall ef (jm : juicy_mem), ext_spec_type io_ext_spec ef -> ext_spec_type io_dry_spec ef.
-Proof.
-  simpl; intros.
-  destruct (oi_eq_dec _ _); [|destruct (oi_eq_dec _ _); [|assumption]].
-  - destruct X as [_ X]; exact (m_dry jm, X).
-  - destruct X as [_ X]; exact (m_dry jm, X).
-Defined.
+Context (ext_link : string -> ident)
+  (ext_link_inj : forall s1 s2, In s1 ["getchar"; "putchar"] -> ext_link s1 = ext_link s2 -> s1 = s2).
 
-Theorem juicy_dry_specs : juicy_dry_ext_spec _ io_ext_spec io_dry_spec dessicate.
-Proof.
-  split; [|split]; try reflexivity; simpl.
-  - unfold funspec2pre, dessicate; simpl.
-    intros ?; if_tac.
-    + intros; subst.
-      destruct t as (? & ? & (c, k)); simpl in *.
-      destruct H1 as (? & phi0 & phi1 & J & Hpre & Hr & Hext).
-      destruct e; inv H; simpl in *.
-      destruct vl; try contradiction; simpl in *.
-      destruct H0, vl; try contradiction.
-      unfold SEPx in Hpre; simpl in Hpre.
-      rewrite seplog.sepcon_emp in Hpre.
-      destruct Hpre as [_ [Hargs [_ [it [H8 Htrace]]]]].
-      assert (Harg: v = Vubyte c) by (inv Hargs; auto). clear Hargs.
-      rewrite Harg.
-      eapply has_ext_compat in Hext as []; eauto; subst; auto.
-      eexists; eauto.
-    + unfold funspec2pre; simpl.
-      if_tac; [|contradiction].
-      intros; subst.
-      destruct t as (? & ? & k); simpl in *.
-      destruct H2 as (? & phi0 & phi1 & J & Hpre & Hr & Hext).
-      destruct e; inv H0; simpl in *.
-      destruct vl; try contradiction.
-      unfold putchar_pre; split; auto; split; auto.
-      unfold SEPx in Hpre; simpl in Hpre.
-      rewrite seplog.sepcon_emp in Hpre.
-      destruct Hpre as [_ [Hargs [_ [it [H8 Htrace]]]]].
-      eapply has_ext_compat in Hext as []; eauto; subst; auto.
-      eexists; eauto.
-  - unfold funspec2pre, funspec2post, dessicate; simpl.
-    intros ?; if_tac.
-    + intros; subst.
-      destruct H0 as (_ & vl & z0 & ? & _ & phi0 & phi1' & J & Hpre & ? & ?).
-      destruct t as (phi1 & t); subst; simpl in *.
-      destruct t as (? & (c, k)); simpl in *.
-      unfold SEPx in Hpre; simpl in Hpre.
-      rewrite seplog.sepcon_emp in Hpre.
-      destruct Hpre as [_ [Hargs [_ [it [H8 Htrace]]]]].
-      edestruct (has_ext_compat _ z0 _ (m_phi jm0) Htrace) as (? & ? & ?); eauto; [eexists; eauto|]; subst.
-      destruct v; try contradiction.
-      destruct v; try contradiction.
-      destruct H4 as (? & Hmem & ? & Hw); simpl in Hw; subst.
-      rewrite <- Hmem in *.
-      rewrite rebuild_same in H2.
-      unshelve eexists (age_to.age_to (level jm) (set_ghost phi0 (Some (ext_ghost x, NoneP) :: tl (ghost_of phi0)) _)), (age_to.age_to (level jm) phi1'); auto.
-      { rewrite <- ghost_of_approx at 2; simpl.
-        destruct (ghost_of phi0); auto. }
-      split; [|split].
-      * eapply age_rejoin; eauto.
-        intro; rewrite H2; auto.
-      * exists i.
-        split3; simpl.
-        -- split; auto.
-        -- unfold_lift. split; auto. split; [|intro Hx; inv Hx].
-             unfold eval_id; simpl. unfold semax.make_ext_rval; simpl.
-             destruct ot; try contradiction; reflexivity.
-        -- unfold SEPx; simpl.
-           rewrite seplog.sepcon_emp.
-           unfold ITREE; exists x; split; [if_tac; auto|].
-           { subst; apply eutt_sutt, Reflexive_eqit_eq. }
-           eapply age_to.age_to_pred, change_has_ext; eauto.
-      * eapply necR_trans; eauto; apply age_to.age_to_necR.
-    + unfold funspec2pre, funspec2post, dessicate; simpl.
-      if_tac; [|contradiction].
-      clear H0.
-      intros; subst.
-      destruct H0 as (_ & vl & z0 & ? & _ & phi0 & phi1' & J & Hpre & ? & ?).
-      destruct t as (phi1 & t); subst; simpl in *.
-      destruct t as (? & k); simpl in *.
-      unfold SEPx in Hpre; simpl in Hpre.
-      rewrite seplog.sepcon_emp in Hpre.
-      destruct Hpre as [_ [Hargs [_ [it [H8 Htrace]]]]].
-      edestruct (has_ext_compat _ z0 _ (m_phi jm0) Htrace) as (? & ? & ?); eauto; [eexists; eauto|]; subst.
-      destruct v; try contradiction.
-      destruct v; try contradiction.
-      destruct H4 as (? & Hmem & ? & Hw); simpl in Hw; subst.
-      rewrite <- Hmem in *.
-      rewrite rebuild_same in H2.
-      unshelve eexists (age_to.age_to (level jm) (set_ghost phi0 (Some (ext_ghost x, NoneP) :: tl (ghost_of phi0)) _)), (age_to.age_to (level jm) phi1'); auto.
-      { rewrite <- ghost_of_approx at 2; simpl.
-        destruct (ghost_of phi0); auto. }
-      split; [|split].
-      * eapply age_rejoin; eauto.
-        intro; rewrite H2; auto.
-      * exists i.
-        split3; simpl.
-        -- split; auto.
-        -- unfold_lift. split; auto. split; [|intro Hx; inv Hx].
-             unfold eval_id; simpl. unfold semax.make_ext_rval; simpl.
-             destruct ot; try contradiction; reflexivity.
-        -- unfold SEPx; simpl.
-             rewrite seplog.sepcon_emp.
-             unfold ITREE; exists x; split; [if_tac; auto|].
-             { subst; apply eutt_sutt, Reflexive_eqit_eq. }
-             eapply age_to.age_to_pred, change_has_ext; eauto.
-      * eapply necR_trans; eauto; apply age_to.age_to_necR.
-Qed.
-
-Instance mem_evolve_refl : Reflexive mem_evolve.
-Proof.
-  repeat intro.
-  destruct (access_at x loc Cur); auto.
-  destruct p; auto.
-Qed.
+Arguments eq_dec : simpl never.
 
-Lemma dry_spec_mem : ext_spec_mem_evolve _ io_dry_spec.
+Theorem io_spec_sound : forall `{!VSTGS IO_itree Σ}, ext_spec_entails (IO_ext_spec ext_link) io_dry_spec.
 Proof.
-  intros ??????????? Hpre Hpost.
-  simpl in Hpre, Hpost.
-  simpl in *.
-  if_tac in Hpre.
-  - destruct w as (m0 & _ & w).
-    destruct Hpre as (_ & ? & Hpre); subst.
-    destruct v; try contradiction.
-    destruct v; try contradiction.
-    destruct Hpost as (? & ? & ?); subst.
-    reflexivity.
-  - if_tac in Hpre; [|contradiction].
-    destruct w as (m0 & _ & w).
-    destruct Hpre as (_ & ? & Hpre); subst.
-    destruct v; try contradiction.
-    destruct v; try contradiction.
-    destruct Hpost as (? & ? & ?); subst.
-    reflexivity.
+  intros; apply juicy_dry_spec; last done; intros.
+  destruct H as [H | [H | ?]]; last done; injection H as <-%ext_link_inj <-; simpl; auto.
+  - if_tac; last done; intros.
+    exists (m, w).
+    destruct w as (c, k).
+    iIntros "(Hz & _ & %Hargs & H)".
+    rewrite /SEPx; monPred.unseal.
+    iDestruct "H" as "(_ & (% & % & Hext) & _)".
+    iDestruct (has_ext_state with "[$Hz $Hext]") as %<-.
+    iSplit; first done.
+    iIntros (???? (r & -> & ? & -> & Hr & Hz')).
+    iMod (change_ext_state with "[$]") as "($ & ?)".
+    iIntros "!>"; iExists r.
+    iSplit; first done.
+    rewrite /local /= /lift1; unfold_lift.
+    iSplit.
+    { iPureIntro; destruct ty; done. }
+    iSplit; last done.
+    iExists z'; iFrame; iPureIntro.
+    split; last done.
+    if_tac; subst; done.
+  - if_tac; last done; intros.
+    exists (m, w).
+    iIntros "(Hz & _ & %Hargs & H)".
+    rewrite /SEPx; monPred.unseal.
+    iDestruct "H" as "(_ & (% & % & Hext) & _)".
+    iDestruct (has_ext_state with "[$Hz $Hext]") as %<-.
+    iSplit; first done.
+    iIntros (???? (r & -> & ? & -> & Hr & Hz')).
+    simpl in Hz'.
+    iMod (change_ext_state with "[$]") as "($ & ?)".
+    iIntros "!>"; iExists r.
+    iSplit; first done.
+    rewrite /local /= /lift1; unfold_lift.
+    iSplit.
+    { iPureIntro; destruct ty; done. }
+    iSplit; last done.
+    iExists z'; iFrame; iPureIntro.
+    split; last done.
+    if_tac; subst; done.
 Qed.
 
 End IO_Dry.
diff --git a/progs/io_mem_dry.v b/progs/io_mem_dry.v
index f5da7210fc..9ab9306b5f 100644
--- a/progs/io_mem_dry.v
+++ b/progs/io_mem_dry.v
@@ -1,9 +1,9 @@
-Require Import VST.progs64.io_mem_specs.
+Require Import VST.progs.io_mem_specs.
 Require Import VST.floyd.proofauto.
 Require Import VST.sepcomp.extspec.
 Require Import VST.veric.semax_ext.
 Require Import VST.veric.SequentialClight.
-Require Import VST.progs64.dry_mem_lemmas.
+Require Import VST.progs.dry_mem_lemmas.
 Require Import VST.veric.mem_lessdef.
 
 Section IO_Dry.
diff --git a/progs/io_os_connection.v b/progs/io_os_connection.v
index d0f12be9a6..d1ca194996 100644
--- a/progs/io_os_connection.v
+++ b/progs/io_os_connection.v
@@ -16,6 +16,8 @@ Require Import VST.zlist.sublist.
 Require Import VST.progs.os_combine.
 Import ExtLib.Structures.Monad.
 
+Opaque eq_dec.eq_dec.
+
 Local Ltac inj :=
   repeat match goal with
   | H: _ = _ |- _ => assert_succeeds (injection H); Coqlib.inv H
@@ -729,9 +731,10 @@ Section Invariants.
       end) evs)).
   Proof.
     induction evs as [| ev evs]; cbn -[Zlength]; intros * Hall Hmax Hlen.
-    { cbn in *.
+    { rewrite app_nil_r.
+      cbn in *.
       replace (Zlength (compute_console' tr)) with CONS_BUFFER_MAX_CHARS by lia.
-      cbn; auto using app_nil_r.
+      cbn; auto.
     }
     rewrite Zlength_cons in Hlen.
     edestruct Hall as (? & ? & ? & ?); eauto; subst.
@@ -1913,7 +1916,7 @@ Import functional_base.
       split; auto; cbn in *.
       rewrite Int.signed_repr by (cbn; lia).
       destruct (Coqlib.zeq z1 (-1)); subst; auto.
-      if_tac; try easy.
+      destruct (eq_dec.eq_dec _ _); try easy.
       rewrite Zle_imp_le_bool by lia.
       destruct Hput as (? & [(? & ?) | (? & ?)]); subst; auto; try lia.
       rewrite Zmod_small; auto; functional_base.rep_lia.
@@ -1985,6 +1988,6 @@ Import functional_base.
       admit.
     - (* trace_itree_match *)
       admit.
-  Admitted.
+  Abort.
 
 End SpecsCorrect.
diff --git a/progs/list_dt.v b/progs/list_dt.v
index 08f0d714cc..8488f7a0fc 100644
--- a/progs/list_dt.v
+++ b/progs/list_dt.v
@@ -816,7 +816,7 @@ intros. unfold nullval.
 apply lseg_neq.
 destruct v; inv H; intuition; try congruence.
 intro. apply ptr_eq_e in H.
-destruct Archi.ptr64 eqn:Hp; inv H.
+destruct Archi.ptr64 eqn:Hp; inv H; try done.
 intro. simpl in H.
 destruct Archi.ptr64; congruence.
 Qed.
diff --git a/progs/verif_append.v b/progs/verif_append.v
index 8fd45c3391..515ff6ae6c 100644
--- a/progs/verif_append.v
+++ b/progs/verif_append.v
@@ -32,18 +32,12 @@ Definition append_spec :=
 
 Definition Gprog : funspecs :=   ltac:(with_library prog [ append_spec ]).
 
-Lemma ENTAIL_refl: forall Delta P, ENTAIL Delta, P |-- P.
-Proof. intros; apply andp_left2; auto. Qed.
-
 Lemma body_append: semax_body Vprog Gprog f_append append_spec.
 Proof.
 start_function.
 forward_if.
 *
  forward.
- Exists y.
- simpl app.
- entailer!!.
 *
  forward.
  apply semax_lseg_nonnull; [ | intros a s3 u ? ?].
@@ -64,10 +58,9 @@ forward_if.
  + entailer!!.
  + clear u H1; rename u0 into u. clear a s3 H0. rename a0 into a.
    gather_SEP (list_cell _ _ _ _) (field_at _ _ _ _ _) (lseg _ _ _ x _) (lseg _ _ _ u _).
-   replace_SEP 0 (lseg LS sh (s1a++[a]) x u * lseg LS sh s1b u nullval)%logic.
+   replace_SEP 0 (lseg LS sh (s1a++[a]) x u * lseg LS sh s1b u nullval).
    entailer.
-   rewrite <- (emp_sepcon (list_cell LS sh a t)).
-   apply (lseg_cons_right_list LS); auto.
+   rewrite <- lseg_cons_right_list; first cancel; auto.
    Intros. gather_SEP (lseg _ _ _ u _).
    apply semax_lseg_nonnull; [ | intros a1 s4 u2 ? ?].
    entailer!.
@@ -83,7 +76,7 @@ forward_if.
     forward.
     forward.
     Exists x. entailer!!.
-    apply derives_trans with (lseg LS sh (s1a++[a0]) x y * lseg LS sh s2 y nullval)%logic.
+    apply derives_trans with (lseg LS sh (s1a++[a0]) x y * lseg LS sh s2 y nullval).
     eapply derives_trans; [ | apply (lseg_cons_right_list LS) with (y:=t)]; auto.
     simpl valinject.
     cancel.
diff --git a/progs/verif_append2.v b/progs/verif_append2.v
index b2dc152dba..608fa9a0fc 100644
--- a/progs/verif_append2.v
+++ b/progs/verif_append2.v
@@ -1,27 +1,42 @@
 Require Import VST.floyd.proofauto.
-Require Import VST.floyd.compat.
 Require Import VST.progs.append.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 Definition t_struct_list := Tstruct _list noattr.
 
+Lemma not_bot_nonidentity : forall sh,  sh <> Share.bot -> sepalg.nonidentity sh.
+Proof.
+   intros.
+   unfold sepalg.nonidentity. unfold not.
+   intros. apply identity_share_bot in H0. contradiction.   
+Qed.
+Lemma nonidentity_not_bot : forall sh, sepalg.nonidentity sh -> sh <> Share.bot.
+Proof.
+   intros. unfold sepalg.nonidentity. unfold not. intros. apply H. rewrite H0. apply bot_identity.    
+Qed.
+#[export] Hint Resolve not_bot_nonidentity : core.
+#[export] Hint Resolve nonidentity_not_bot : core.
+
+Section Spec.
+
+Context  `{!default_VSTGS Σ}.
 
 Fixpoint listrep (sh: share)
             (contents: list val) (x: val) : mpred :=
  match contents with
  | h::hs =>
-              EX y:val,
-                data_at sh t_struct_list (h,y) x * listrep sh hs y
- | nil => !! (x = nullval) && emp
+              ∃ y:val,
+                data_at sh t_struct_list (h,y) x ∗ listrep sh hs y
+ | nil => ⌜x = nullval⌝ ∧ emp
  end.
 
 Arguments listrep sh contents x : simpl never.
 
 Lemma listrep_local_facts:
   forall sh contents p,
-     listrep sh contents p |--
-     !! (is_pointer_or_null p /\ (p=nullval <-> contents=nil)).
+     listrep sh contents p ⊢
+     ⌜is_pointer_or_null p ∧ (p=nullval <-> contents=nil)⌝.
 Proof.
 intros.
 revert p; induction contents; 
@@ -30,30 +45,28 @@ Intros y. entailer!.
 split; intro. subst p. destruct H; contradiction. inv H2.
 Qed.
 
-#[export] Hint Resolve listrep_local_facts : saturate_local.
+
 
 Lemma listrep_valid_pointer:
   forall sh contents p,
-   sepalg.nonidentity sh ->
-   listrep sh contents p |-- valid_pointer p.
+  sepalg.nonidentity sh ->
+   listrep sh contents p ⊢ valid_pointer p.
 Proof.
  destruct contents; unfold listrep; fold listrep; intros; Intros; subst.
  auto with valid_pointer.
  Intros y.
  apply sepcon_valid_pointer1.
  apply data_at_valid_ptr; auto.
- simpl;  computable.
+ simpl; computable.
 Qed.
 
-#[export] Hint Resolve listrep_valid_pointer : valid_pointer.
-
 Lemma listrep_null: forall sh contents,
-    listrep sh contents nullval = !! (contents=nil) && emp.
+    listrep sh contents nullval ⊣⊢ ⌜contents=nil⌝ ∧ emp.
 Proof.
 destruct contents; unfold listrep; fold listrep.
 autorewrite with norm. auto.
-apply pred_ext.
-Intros y. entailer. destruct H; contradiction.
+apply bi.equiv_entails_2.
+Intros y. entailer!. destruct H; contradiction.
 Intros. discriminate.
 Qed.
 
@@ -73,46 +86,48 @@ Definition append_spec :=
      PARAMS (x; y) GLOBALS()
      SEP (listrep sh s1 x; listrep sh s2 y)
   POST [ tptr t_struct_list ]
-    EX r: val,
+    ∃ r: val,
      PROP()
      RETURN (r)
      SEP (listrep sh (s1++s2) r).
 
 Definition Gprog : funspecs :=   ltac:(with_library prog [ append_spec ]).
 
-Module Proof1.
+Hint Resolve listrep_local_facts : saturate_local.
+Hint Extern 1 (listrep _ _ _ ⊢ valid_pointer _) =>
+    (simple apply listrep_valid_pointer; now auto) : valid_pointer.
 
-Definition lseg (sh: share) (contents: list val) (x z: val) : mpred :=
-  ALL cts2:list val, listrep sh cts2 z -* listrep sh (contents++cts2) x.
+Section Proof1.
 
 Lemma body_append: semax_body Vprog Gprog f_append append_spec.
 Proof.
 start_function.
 forward_if.
 *
- subst x. rewrite listrep_null.  Intros.  subst.
+ subst x.
  forward.
+ rewrite listrep_null. Intros; subst.
  Exists y.
  entailer!!.
  simpl; auto.
 *
  forward.
  destruct s1 as [ | v s1']; unfold listrep at 1; fold listrep.
- Intros.  contradiction.
+ { Intros. contradiction. }
  Intros u.
  remember (v::s1') as s1.
  forward.
  forward_while
-      ( EX a: val, EX s1b: list val, EX t: val, EX u: val,
+      (∃ a: val, ∃ s1b: list val, ∃ t: val, ∃ u: val,
             PROP ()
             LOCAL (temp _x x; temp _t t; temp _u u; temp _y y)
-            SEP (listrep sh (a::s1b++s2) t -* listrep sh (s1++s2) x;
+            SEP (listrep sh (a::s1b++s2) t -∗ listrep sh (s1++s2) x;
                    data_at sh t_struct_list (a,u) t;
                    listrep sh s1b u;
                    listrep sh s2 y))%assert.
 + (* current assertion implies loop invariant *)
    Exists v s1' x u.
-   subst s1. entailer!!. simpl. cancel_wand.
+   entailer!. simpl. cancel_wand.
 + (* loop test is safe to execute *)
    entailer!!.
 + (* loop body preserves invariant *)
@@ -124,14 +139,13 @@ forward_if.
    Exists (v,s1b,u0,z). unfold fst, snd.
    simpl app.
    entailer!!.
-   rewrite sepcon_comm.
-   apply RAMIF_PLAIN.trans''.
-   apply wand_sepcon_adjoint.
-   forget (v::s1b++s2) as s3.
-   unfold listrep; fold listrep; Exists u0; auto.
+   iIntros "[Ha Hb]". iIntros.
+   iApply "Ha".
+   unfold listrep; fold listrep. iExists u0; iFrame.
 + (* after the loop *)
    clear v s1' Heqs1.
    forward.
+   simpl. (* TODO this simpl wasn't needed. maybe store_tac_no_hint in forward1 is broken? *)
    forward.
    rewrite (proj1 H2 (eq_refl _)).
    Exists x.
@@ -139,19 +153,19 @@ forward_if.
    clear.
    entailer!!.
    unfold listrep at 3; fold listrep. Intros.
-   pull_right (listrep sh (a :: s2) t -* listrep sh (s1 ++ s2) x).
-   apply modus_ponens_wand'.
-   unfold listrep at 2; fold listrep. Exists y; cancel.
+   iIntros "(Ha & Hb & Hc & Hd)".
+   iApply "Ha".
+   unfold listrep at -1; fold listrep. iExists y; iFrame.
 Qed.
 
 End Proof1.
 
-Module Proof2.
+Section Proof2.
 
 Definition lseg (sh: share) (contents: list val) (x z: val) : mpred :=
-  ALL cts2:list val, listrep sh cts2 z -* listrep sh (contents++cts2) x.
+  ∀ cts2:list val, listrep sh cts2 z -∗ listrep sh (contents++cts2) x.
 
-Lemma body_append: semax_body Vprog Gprog f_append append_spec.
+Lemma body_append2: semax_body Vprog Gprog f_append append_spec.
 Proof.
 start_function.
 forward_if.
@@ -168,7 +182,7 @@ forward_if.
  remember (v::s1') as s1.
  forward.
  forward_while
-      (EX s1a: list val,  EX a: val, EX s1b: list val, EX t: val, EX u: val,
+      (∃ s1a: list val, ∃ a: val, ∃ s1b: list val, ∃ t: val, ∃ u: val,
             PROP (s1 = s1a ++ a :: s1b)
             LOCAL (temp _x x; temp _t t; temp _u u; temp _y y)
             SEP (lseg sh s1a x t;
@@ -177,7 +191,7 @@ forward_if.
                    listrep sh s2 y))%assert.
 + (* current assertion implies loop invariant *)
    Exists (@nil val) v s1' x u.  entailer!!.
-   unfold lseg. apply allp_right; intro. simpl. cancel_wand.
+   unfold lseg. iIntros. simpl. auto.
 + (* loop test is safe to execute *)
    entailer!!.
 + (* loop body preserves invariant *)
@@ -190,101 +204,93 @@ forward_if.
    rewrite <- !app_assoc. simpl app.
    entailer!!.
    unfold lseg.
-   rewrite sepcon_comm.
+   rewrite bi.sep_comm.
    clear.
-   apply RAMIF_Q.trans'' with (cons a).
-   extensionality cts; simpl; rewrite <- app_assoc; reflexivity.
-   apply allp_right; intro. apply wand_sepcon_adjoint.
-   unfold listrep at 2; fold listrep; Exists u0.  apply derives_refl.
+   iIntros "[H1 H2]".
+   iIntros (cts2) "H3".
+   iSpecialize ("H2" $! (a :: cts2)).
+   rewrite -app_assoc.
+   iApply ("H2").
+   unfold listrep at -1; fold listrep. iExists u0. iFrame.
  + (* after the loop *)
-   forward. forward.
+   forward. simpl. forward.
    Exists x. entailer!!.
    destruct H3 as [? _]. specialize (H3 (eq_refl _)). subst s1b.
    unfold listrep at 1.  Intros. autorewrite with norm.  rewrite H0. rewrite <- app_assoc. simpl app.
    unfold lseg.
-   rewrite sepcon_assoc.
-   eapply derives_trans; [apply allp_sepcon1 | ]. apply allp_left with (a::s2).
-   rewrite sepcon_comm.
-   eapply derives_trans; [ | apply modus_ponens_wand].
-   apply sepcon_derives; [ | apply derives_refl].
-   unfold listrep at 2; fold listrep. Exists y; auto.
+   iIntros "(H1 & H2 & H3)".
+   iApply ("H1" $! (a :: s2)).
+   unfold listrep at 2; fold listrep. iExists y; iFrame.
 Qed.
 
 End Proof2.
 
-Module Proof3.  (*************** inductive lseg *******************)
+Section Proof3.  (*************** inductive lseg *******************)
 
-Fixpoint lseg (sh: share)
+Fixpoint lseg2 (sh: share)
             (contents: list val) (x z: val) : mpred :=
  match contents with
- | h::hs => !! (x<>z) && 
-              EX y:val,
-                data_at sh t_struct_list (h,y) x * lseg sh hs y z
- | nil => !! (x = z /\ is_pointer_or_null x) && emp
+ | h::hs => ⌜x<>z⌝ ∧ 
+              ∃ y:val,
+                data_at sh t_struct_list (h,y) x ∗ lseg2 sh hs y z
+ | nil => ⌜x = z /\ is_pointer_or_null x⌝ ∧ emp
  end.
 
-Arguments lseg sh contents x z : simpl never.
+Arguments lseg2 sh contents x z : simpl never.
+Notation lseg := lseg2.
 
 Lemma lseg_local_facts:
   forall sh contents p q,
-     lseg sh contents p q |--
-     !! (is_pointer_or_null p /\ is_pointer_or_null q /\ (p=q <-> contents=nil)).
+     lseg sh contents p q ⊢
+     ⌜is_pointer_or_null p /\ is_pointer_or_null q /\ (p=q <-> contents=nil)⌝.
 Proof.
 intros.
-apply derives_trans with (lseg sh contents p q && !! (is_pointer_or_null p /\
-        is_pointer_or_null q /\ (p = q <-> contents = []))).
-2: entailer!.
 revert p; induction contents; intros; simpl; unfold lseg; fold lseg.
-entailer!.
-intuition.
-Intros y. Exists y.
-eapply derives_trans.
-apply sepcon_derives.
-apply derives_refl.
-apply IHcontents.
+{ normalize. }
+Intros y.
 entailer!.
 intuition congruence.
 Qed.
 
-#[export] Hint Resolve lseg_local_facts : saturate_local.
+Hint Resolve lseg_local_facts : saturate_local.
 
 Lemma lseg_valid_pointer:
   forall sh contents p ,
    sepalg.nonidentity sh ->
-   lseg sh contents p nullval |-- valid_pointer p.
+   lseg sh contents p nullval ⊢ valid_pointer p.
 Proof.
  destruct contents; unfold lseg; fold lseg; intros. entailer!.
  Intros *.
  auto with valid_pointer.
 Qed.
 
-#[export] Hint Resolve lseg_valid_pointer : valid_pointer.
+Hint Extern 1 (lseg _ _ _ nullval ⊢ valid_pointer _) =>
+    (simple apply lseg_valid_pointer; now auto) : valid_pointer.
 
 Lemma lseg_eq: forall sh contents x,
-    lseg sh contents x x = !! (contents=nil /\ is_pointer_or_null x) && emp.
+    lseg sh contents x x ⊣⊢ ⌜contents=nil /\ is_pointer_or_null x⌝ ∧ emp.
 Proof.
 intros.
 destruct contents; unfold lseg; fold lseg.
-f_equal. f_equal. f_equal. apply prop_ext; intuition.
-apply pred_ext.
-Intros y. contradiction.
-Intros. discriminate.
+- apply and_mono_iff; auto. apply bi.pure_iff. intuition.
+- iSplit. 
+  + iIntros "[%H1 H2]". contradiction.
+  + iIntros "[%H1 H2]". destruct H1. discriminate.
 Qed.
 
 Lemma lseg_null: forall sh contents,
-    lseg sh contents nullval nullval = !! (contents=nil) && emp.
+    lseg sh contents nullval nullval ⊣⊢ ⌜contents=nil⌝ ∧ emp.
 Proof.
 intros.
  rewrite lseg_eq.
- apply pred_ext.
- entailer!.
- entailer!.
+ apply and_mono_iff; auto.
+ apply bi.pure_iff; intuition.
 Qed.
 
-Lemma lseg_cons: forall sh (v u x: val) s,
+Lemma lseg_cons: forall sh (v u x: val) (s: list val),
    readable_share sh ->
- data_at sh t_struct_list (v, u) x * lseg sh s u nullval
- |-- lseg sh [v] x u * lseg sh s u nullval.
+ data_at sh t_struct_list (v, u) x ∗ lseg sh s u nullval
+ ⊢ lseg sh [v] x u ∗ lseg sh s u nullval.
 Proof.
 intros.
      unfold lseg at 2. Exists u. 
@@ -292,20 +298,20 @@ intros.
      destruct s; unfold lseg at 1; fold lseg; entailer.
 Qed.
 
-Lemma lseg_cons': forall sh (v u x a b: val) ,
+Lemma lseg_cons': forall sh (v u x a b: val),
    readable_share sh ->
- data_at sh t_struct_list (v, u) x * data_at sh t_struct_list (a,b) u
- |-- lseg sh [v] x u * data_at sh t_struct_list (a,b) u.
+ data_at sh t_struct_list (v, u) x ∗ data_at sh t_struct_list (a,b) u
+ ⊢ lseg sh [v] x u ∗ data_at sh t_struct_list (a,b) u.
 Proof.
 intros.
-     unfold lseg. Exists u. 
+     unfold lseg. Exists u.
      entailer!.
 Qed.
 
 Lemma lseg_app': forall sh s1 s2 (a w x y z: val),
    readable_share sh ->
-   lseg sh s1 w x * lseg sh s2 x y * data_at sh t_struct_list (a,z) y |--
-   lseg sh (s1++s2) w y * data_at sh t_struct_list (a,z) y.
+   (lseg sh s1 w x ∗ lseg sh s2 x y) ∗ data_at sh t_struct_list (a,z) y ⊢
+   lseg sh (s1++s2) w y ∗ data_at sh t_struct_list (a,z) y.
 Proof.
  intros.
  revert w; induction s1; intro; simpl.
@@ -313,12 +319,12 @@ Proof.
  unfold lseg at 1 3; fold lseg. Intros j; Exists j.
  entailer.
  sep_apply (IHs1 j).
- cancel. 
+ cancel.
 Qed.
-
+ 
 Lemma lseg_app_null: forall sh s1 s2 (w x: val),
    readable_share sh ->
-   lseg sh s1 w x * lseg sh s2 x nullval |--
+   lseg sh s1 w x ∗ lseg sh s2 x nullval ⊢
    lseg sh (s1++s2) w nullval.
 Proof.
  intros.
@@ -332,31 +338,31 @@ Qed.
 
 Lemma lseg_app: forall sh s1 s2 a s3 (w x y z: val),
    readable_share sh ->
-   lseg sh s1 w x * lseg sh s2 x y * lseg sh (a::s3) y z |--
-   lseg sh (s1++s2) w y * lseg sh (a::s3) y z.
+   lseg sh s1 w x ∗ lseg sh s2 x y ∗ lseg sh (a::s3) y z ⊢
+   lseg sh (s1++s2) w y ∗ lseg sh (a::s3) y z.
 Proof.
  intros.
  unfold lseg at 3 5; fold lseg.
- Intros u; Exists u. rewrite prop_true_andp by auto.
+ Intros u; Exists u. rewrite prop_true_andp //.
  sep_apply (lseg_app' sh s1 s2 a w x y u); auto.
  cancel.
 Qed.
 
 Lemma listrep_lseg_null :
- listrep = fun sh s p => lseg sh s p nullval.
+ ∀ sh s p, listrep sh s p ⊣⊢ lseg sh s p nullval.
 Proof.
-extensionality sh s p.
+intros.
 revert p.
 induction s; intros.
-unfold lseg, listrep; apply pred_ext; entailer!.
+unfold lseg, listrep; apply bi.equiv_entails_2; entailer!.
 unfold lseg, listrep; fold lseg; fold listrep.
-apply pred_ext; Intros y; Exists y; rewrite IHs; entailer!.
+apply bi.equiv_entails_2; Intros y; Exists y; rewrite IHs; entailer!.
 Qed.
 
-Lemma body_append: semax_body Vprog Gprog f_append append_spec.
+Lemma body_append3: semax_body Vprog Gprog f_append append_spec.
 Proof.
 start_function.
-revert POSTCONDITION; rewrite listrep_lseg_null; intro.
+rewrite -> listrep_lseg_null in * |- *.
 forward_if.
 *
  subst x. rewrite lseg_null. Intros. subst.
@@ -373,7 +379,7 @@ forward_if.
  remember (v::s1') as s1.
  forward.
  forward_while
-      (EX s1a: list val, EX a: val, EX s1b: list val, EX t: val, EX u: val,
+      (∃ s1a: list val, ∃ a: val, ∃ s1b: list val, ∃ t: val, ∃ u: val,
             PROP (s1 = s1a ++ a :: s1b)
             LOCAL (temp _x x; temp _t t; temp _u u; temp _y y)
             SEP (lseg sh s1a x t; 
@@ -382,7 +388,7 @@ forward_if.
                    lseg sh s2 y nullval))%assert.
  + (* current assertion implies loop invariant *)
      Exists (@nil val) v s1' x u.
-     subst s1. rewrite lseg_eq.
+     subst s1. rewrite lseg_eq listrep_lseg_null.
      entailer.
 (*     sep_apply (lseg_cons sh v u x s1'); auto. *)
  + (* loop test is safe to execute *)
@@ -404,13 +410,14 @@ forward_if.
     subst. rewrite lseg_eq. Intros. subst. 
     forward.
     forward.
-    Exists x. 
+    Exists x.
     entailer!!.
     sep_apply (lseg_cons sh a y t s2); auto.
     sep_apply (lseg_app_null sh [a] s2 t y); auto.
     rewrite <- app_assoc.
     sep_apply (lseg_app_null sh s1a ([a]++s2) x t); auto.
+    rewrite listrep_lseg_null //.
 Qed.
 
 End Proof3.
-
+End Spec.
diff --git a/progs/verif_bin_search.v b/progs/verif_bin_search.v
index f8a2981fa3..26897fa870 100644
--- a/progs/verif_bin_search.v
+++ b/progs/verif_bin_search.v
@@ -80,7 +80,7 @@ Qed.
 
 Fixpoint sorted2 l :=
   match l with
-  | [] => True
+  | [] => True%type
   | x :: rest => Forall (fun y => x <= y) rest /\ sorted2 rest
   end.
 
@@ -264,6 +264,7 @@ Definition four_contents := [1; 2; 3; 4].
 Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
 Proof.
   start_function.
+  rename a into gv.
   forward_call (gv _four,Ews,four_contents,3,0,4).
   { change (Zlength four_contents) with 4.
     repeat constructor; computable.
@@ -271,8 +272,6 @@ Proof.
   Intro r; forward.
 Qed.
 
-#[export] Existing Instance NullExtension.Espec.
-
 Lemma prog_correct:
   semax_prog prog tt Vprog Gprog.
 Proof.
diff --git a/progs/verif_bst.v b/progs/verif_bst.v
index 122dfaef46..0e1f2b5dee 100644
--- a/progs/verif_bst.v
+++ b/progs/verif_bst.v
@@ -311,7 +311,7 @@ Proof.
   rewrite (field_at_data_at _ t_struct_tree [StructField _left]).
   unfold treebox_rep at 1. Exists p1. cancel.
 
-  iIntros "(? & ? & ? & ? & ? & ?) Hleft".
+  iIntros "(? & ? & ? & ?) Hleft".
   clear p1.
   unfold treebox_rep.
   iExists p.
@@ -323,7 +323,7 @@ Proof.
   iFrame.
   unfold_data_at (data_at _ _ _ p).
   rewrite (field_at_data_at _ t_struct_tree [StructField _left]).
-  iFrame.
+  by iFrame.
 Qed.
 
 Lemma bst_right_entail: forall (t1 t2 t2': tree val) k (v p1 p2 p b: val),
@@ -342,7 +342,7 @@ Proof.
   rewrite (field_at_data_at _ t_struct_tree [StructField _right]).
   unfold treebox_rep at 1. Exists p2. cancel.
 
-  iIntros "(? & ? & ? & ? & ? & ?) Hright".
+  iIntros "(? & ? & ? & ?) Hright".
   clear p2.
   unfold treebox_rep.
   iExists p.
@@ -354,7 +354,7 @@ Proof.
   iFrame.
   unfold_data_at (data_at _ _ _ p).
   rewrite (field_at_data_at _ t_struct_tree [StructField _right]).
-  iFrame.
+  by iFrame.
 Qed.
 
 Lemma if_trueb: forall {A: Type} b (a1 a2: A), b = true -> (if b then a1 else a2) = a1.
diff --git a/progs/verif_bst_oo.v b/progs/verif_bst_oo.v
index b04cea37e5..f7519d89d4 100644
--- a/progs/verif_bst_oo.v
+++ b/progs/verif_bst_oo.v
@@ -63,11 +63,11 @@ Fixpoint treebox_rep (t: tree val) (b: val) : mpred :=
   match t with
   | E => data_at Tsh (tptr t_struct_tree) nullval b
   | T l x p r =>
-      !! (Int.min_signed <= x <= Int.max_signed) &&
+      (!! (Int.min_signed <= x <= Int.max_signed) &&
       data_at Tsh (tptr t_struct_tree) p b *
       field_at Tsh t_struct_tree [StructField _key] (Vint (Int.repr x)) p *
       treebox_rep l (field_address t_struct_tree [StructField _left] p) *
-      treebox_rep r (field_address t_struct_tree [StructField _right] p)
+      treebox_rep r (field_address t_struct_tree [StructField _right] p))%I
   end.
 
 Fixpoint key_store (s: tree val) (x: key) (q: val): Prop :=
@@ -88,8 +88,8 @@ Definition value_at (t: tree val) (v: val) (x: Z): mpred :=
 
 (* TODO: maybe not useful *)
 Lemma treebox_rep_spec: forall (t: tree val) (b: val),
-  treebox_rep t b =
-  data_at Tsh (tptr t_struct_tree)
+  treebox_rep t b ⊣⊢
+  (data_at Tsh (tptr t_struct_tree)
     match t return val with
     | E => nullval
     | T _ _ p _ => p
@@ -101,7 +101,7 @@ Lemma treebox_rep_spec: forall (t: tree val) (b: val),
       field_at Tsh t_struct_tree [StructField _key] (Vint (Int.repr x)) p *
       treebox_rep l (field_address t_struct_tree [StructField _left] p) *
       treebox_rep r (field_address t_struct_tree [StructField _right] p)
-  end.
+  end)%I.
 Proof.
   intros.
   destruct t; simpl; apply pred_ext; entailer!.
@@ -290,24 +290,15 @@ Qed.
 #[export] Hint Resolve tree_rep_valid_pointer: valid_pointer.
 
 *)
-Lemma modus_ponens_wand' {A}{ND: NatDed A}{SL: SepLog A}:
-  forall P Q R: A, (P |-- Q) -> P * (Q -* R) |-- R.
-Proof.
-  intros.
-  eapply derives_trans; [| apply modus_ponens_wand].
-  apply sepcon_derives; [| apply derives_refl].
-  auto.
-Qed.
-
-Lemma RAMIF_Q2_trans' {X Y A : Type} {ND : NatDed A} {SL : SepLog A}:
+Lemma RAMIF_Q2_trans' {X Y} {A : bi}:
   forall (m l: A) (g' m' l' : X -> Y -> A),
-    (m |-- l * (ALL p: X, ALL q: Y, l' p q -* m' p q)) ->
-    m * (ALL p: X, ALL q: Y, m' p q -* g' p q) |-- l * (ALL p: X, ALL q: Y, l' p q -* g' p q).
+    (m |-- l * (ALL p: X, ALL q: Y, (l' p q -* m' p q))) ->
+    m * (ALL p: X, ALL q: Y, (m' p q -* g' p q)) |-- l * (ALL p: X, ALL q: Y, (l' p q -* g' p q)).
 Proof.
   intros.
   eapply derives_trans; [apply sepcon_derives; [exact H | apply derives_refl] |].
   clear H.
-  rewrite sepcon_assoc.
+  rewrite <- sepcon_assoc.
   apply sepcon_derives; auto.
   apply allp_right; intros p.
   apply allp_right; intros q.
diff --git a/progs/verif_even.v b/progs/verif_even.v
index bd2f0adcf0..2e98ecea5a 100644
--- a/progs/verif_even.v
+++ b/progs/verif_even.v
@@ -11,6 +11,7 @@ Definition Gprog : funspecs :=
 Lemma body_even : semax_body Vprog Gprog f_even even_spec.
 Proof.
 start_function.
+rename a into z.
 forward_if.
 *
  forward.
@@ -30,7 +31,7 @@ forward.
 Qed.
 
 
-Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog even.prog) Gprog.
+Definition Espec := add_funspecs_rec unit (ext_link_prog even.prog) (void_spec _) Gprog.
 #[export] Existing Instance Espec.
 (* The Espec for odd is different from the Espec for even;
   the former has only "even" as an external function, and vice versa. *)
@@ -39,6 +40,10 @@ Lemma prog_correct:
 Proof.
 prove_semax_prog.
 semax_func_cons_ext.
+{ destruct x; simpl.
+  unfold PROPx, LOCALx, SEPx, local, lift1; simpl; unfold liftx; simpl; unfold lift.
+  monPred.unseal; Intros.
+  destruct ret; unfold eval_id in H0; simpl in H0; subst; simpl; [auto | contradiction]. }
 semax_func_cons body_even.
 semax_func_cons body_main.
 Qed.
diff --git a/progs/verif_int_or_ptr.v b/progs/verif_int_or_ptr.v
index d296252313..17ca11ceac 100644
--- a/progs/verif_int_or_ptr.v
+++ b/progs/verif_int_or_ptr.v
@@ -23,7 +23,7 @@ Definition valid_int_or_ptr (x: val) :=
  | Vint i => Int.testbit i 0 = true
               \/ Int.unsigned i < POINTER_BOUNDARY
  | Vptr b z => Ptrofs.testbit z 0 = false
- | _ => False
+ | _ => False%type
  end.
 
 Lemma valid_int_or_ptr_ii1:
@@ -100,7 +100,7 @@ Qed.
 
 #[export] Hint Resolve treerep_local_facts : saturate_local.
 
-Definition test_int_or_ptr_spec :=
+Definition test_int_or_ptr_spec : ident * funspec :=
  DECLARE _test_int_or_ptr
  WITH x : val
  PRE [ int_or_ptr_type ]
@@ -113,7 +113,7 @@ Definition test_int_or_ptr_spec :=
                     end)))
    SEP().
 
-Definition int_or_ptr_to_int_spec :=
+Definition int_or_ptr_to_int_spec : ident * funspec :=
  DECLARE _int_or_ptr_to_int
  WITH x : val
  PRE [ int_or_ptr_type ]
@@ -121,7 +121,7 @@ Definition int_or_ptr_to_int_spec :=
  POST [ tint ]
    PROP() RETURN (x) SEP().
 
-Definition int_or_ptr_to_ptr_spec :=
+Definition int_or_ptr_to_ptr_spec : ident * funspec :=
  DECLARE _int_or_ptr_to_ptr
  WITH x : val
  PRE [ int_or_ptr_type ]
@@ -129,7 +129,7 @@ Definition int_or_ptr_to_ptr_spec :=
  POST [ tptr tvoid ]
    PROP() RETURN (x) SEP().
 
-Definition int_to_int_or_ptr_spec :=
+Definition int_to_int_or_ptr_spec : ident * funspec :=
  DECLARE _int_to_int_or_ptr
  WITH x : val
  PRE [ tint ]
@@ -137,7 +137,7 @@ Definition int_to_int_or_ptr_spec :=
  POST [ int_or_ptr_type ]
    PROP() RETURN(x) SEP().
 
-Definition ptr_to_int_or_ptr_spec :=
+Definition ptr_to_int_or_ptr_spec : ident * funspec :=
  DECLARE _ptr_to_int_or_ptr
  WITH x : val
  PRE [ tptr tvoid ]
@@ -145,7 +145,7 @@ Definition ptr_to_int_or_ptr_spec :=
  POST [ int_or_ptr_type ]
    PROP() RETURN(x) SEP().
 
-Definition makenode_spec :=
+Definition makenode_spec : ident * funspec :=
  DECLARE _makenode 
   WITH p: val, q: val
   PRE [ int_or_ptr_type, int_or_ptr_type ]
@@ -155,7 +155,7 @@ Definition makenode_spec :=
     PROP() RETURN (r) 
     SEP (data_at Tsh (Tstruct _tree noattr) (p,q) r).
 
-Definition copytree_spec :=
+Definition copytree_spec : ident * funspec :=
  DECLARE _copytree
   WITH t: tree, p : val
   PRE  [ int_or_ptr_type ]
@@ -186,9 +186,7 @@ Proof.
  forward_call (Vint (Int.repr (i+i+1))).
  forward_if.
  - (* then clause *)
-   forward. simpl.
-   Exists (Vint (Int.repr(i+i+1))).
-   entailer!!.
+   forward.
  - (* else clause *)
   inv H0.
 * (* NODE *) 
@@ -230,8 +228,6 @@ Proof.
   }
   forward_call r.
   forward. simpl.
-  Exists r p q p1 p2.
+  Exists r p1 p2 p q.
   entailer!!.
 Qed.
-
-
diff --git a/progs/verif_io_mem.v b/progs/verif_io_mem.v
index 768f0047f3..e28349dc7f 100644
--- a/progs/verif_io_mem.v
+++ b/progs/verif_io_mem.v
@@ -2,12 +2,17 @@ Require Import VST.progs.io_mem.
 Require Import VST.progs.io_mem_specs.
 Require Import VST.floyd.proofauto.
 Require Import VST.floyd.library.
+Require Import ITree.Core.ITreeDefinition.
 
 Local Open Scope itree_scope.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
+Section IO.
+
+Context `{!VSTGS (@IO_itree (IO_event(file_id := nat))) Σ}.
+
 Definition putchars_spec := DECLARE _putchars putchars_spec.
 Definition getchars_spec := DECLARE _getchars getchars_spec.
 
@@ -20,16 +25,18 @@ Proof.
   rewrite <- Nat2Z.inj_div by discriminate.
   rewrite !Nat2Z.id.
   apply Nat2Z.inj_lt.
-  rewrite Nat2Z.inj_div, Z2Nat.id by lia; simpl.
+  rewrite -> Nat2Z.inj_div, Z2Nat.id by lia; simpl.
   apply Z.div_lt; auto; lia.
 Qed.
 
+Local Obligation Tactic := unfold RelationClasses.complement, Equivalence.equiv;
+  Tactics.program_simpl.
+
 Program Fixpoint chars_of_Z (n : Z) { measure (Z.to_nat n) } : list byte :=
   let n' := n / 10 in
   match n' <=? 0 with true => [Byte.repr (n + char0)] | false => chars_of_Z n' ++ [Byte.repr (n mod 10 + char0)] end.
 Next Obligation.
 Proof.
-  rewrite ?Zaux.Zdiv_eucl_unique in *.  (* Coq 8.15 and after *)
   apply div_10_dec.
   symmetry in Heq_anonymous; apply Z.leb_nle in Heq_anonymous.
   eapply Z.lt_le_trans, Z_mult_div_ge with (b := 10); lia.
@@ -112,10 +119,6 @@ Proof.
   rewrite !Int.unsigned_repr; auto.
 Qed.
 
-(*Opaque bind.
-
-Opaque Nat.div Nat.modulo.*)
-
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -148,14 +151,14 @@ Proof.
   rewrite (intr_eq n).
   destruct (n <=? 0) eqn: Hn.
   { apply Zle_bool_imp_le in Hn; lia. }
-  rewrite Zlength_app, Zlength_cons, Zlength_nil; lia.
+  rewrite -> Zlength_app, Zlength_cons, Zlength_nil; lia.
 Qed.
 
 Lemma replace_list_nil : forall {X} i (l : list X), 0 <= i <= Zlength l -> replace_list i l [] = l.
 Proof.
   intros; unfold replace_list.
-  rewrite Zlength_nil, Z.add_0_r; simpl.
-  rewrite sublist_rejoin, sublist_same by lia; auto.
+  rewrite -> Zlength_nil, Z.add_0_r; simpl.
+  rewrite -> sublist_rejoin, sublist_same by lia; auto.
 Qed.
 
 Lemma replace_list_upd_snoc : forall {X} i (l l' : list X) x, 0 <= i -> i + Zlength l' < Zlength l ->
@@ -164,13 +167,13 @@ Proof.
   intros; unfold replace_list.
   rewrite upd_Znth_app2; rewrite ?Zlength_sublist; try rep_lia.
   f_equal.
-  rewrite Z.sub_0_r, Z.add_simpl_l, upd_Znth_app2; rewrite ?Zlength_sublist; try rep_lia.
-  rewrite Zminus_diag, Zlength_app, Zlength_cons, Zlength_nil, upd_Znth0_old, <- app_assoc; simpl; f_equal; f_equal.
-  rewrite Zlength_sublist by rep_lia.
-  rewrite sublist_sublist by rep_lia.
+  rewrite -> Z.sub_0_r, Z.add_simpl_l, upd_Znth_app2; rewrite ?Zlength_sublist; try rep_lia.
+  rewrite -> Zminus_diag, Zlength_app, Zlength_cons, Zlength_nil, upd_Znth0_old, <- app_assoc; simpl; f_equal; f_equal.
+  rewrite -> Zlength_sublist by rep_lia.
+  rewrite -> sublist_sublist by rep_lia.
   f_equal; lia.
   { rewrite Zlength_sublist; rep_lia. }
-  { rewrite Zlength_app, Zlength_sublist; rep_lia. }
+  { rewrite -> Zlength_app, Zlength_sublist; rep_lia. }
 Qed.
 
 Lemma body_print_intr: semax_body Vprog Gprog f_print_intr print_intr_spec.
@@ -181,43 +184,43 @@ Proof.
     LOCAL (temp _k (Vint (Int.repr (Zlength (intr i) - 1))))
     SEP (data_at sh (tarray tuchar (Zlength contents)) (replace_list 0 contents (map Vubyte (intr i))) buf)).
   - forward.
-    rewrite divu_repr by rep_lia.
+    rewrite -> divu_repr by rep_lia.
     forward.
     forward_call (sh, i / 10, buf, contents).
-    { rewrite intr_lt by lia; split; auto; try lia.
+    { rewrite -> intr_lt by lia; split; auto; try lia.
       assert (i / 10 < i).
       { apply Z.div_lt; lia. }
        split.
       apply Z.div_pos; lia. 
       rep_lia.
     }
-    rewrite modu_repr by (lia || computable).
+    rewrite -> modu_repr by (lia || computable).
     assert (repable_signed (Zlength (intr (i / 10)))).
     { split; try rep_lia.
       rewrite intr_lt; try lia. }
     forward.
-    { entailer!!.
+    { entailer!.
       split; try rep_lia.
       rewrite intr_lt; try lia. }
-    entailer!!.
-    { rewrite intr_lt by lia; auto. }
+    entailer!.
+    { rewrite -> intr_lt by lia; auto. }
     rewrite (intr_eq i).
     destruct (i <=? 0) eqn: Hi; [apply Zle_bool_imp_le in Hi; lia|].
     pose proof (Z_mod_lt i 10).
     rewrite <- (Zlength_map _ _ Vubyte), <- (Z.add_0_l (Zlength (map _ _))), replace_list_upd_snoc.
-    rewrite (zero_ext_inrange 8 (Int.repr (i mod 10))), add_repr.
-    rewrite zero_ext_inrange, map_app.
+    rewrite -> (zero_ext_inrange 8 (Int.repr (i mod 10))), add_repr.
+    rewrite -> zero_ext_inrange, map_app.
     unfold Vubyte at 3; simpl.
-    rewrite Byte.unsigned_repr by (unfold char0; rep_lia); apply derives_refl.
+    rewrite -> Byte.unsigned_repr by (unfold char0; rep_lia); apply derives_refl.
     { rewrite Int.unsigned_repr; simpl; rep_lia. }
     { rewrite Int.unsigned_repr; simpl; rep_lia. }
     { lia. }
-    { rewrite Zlength_map, intr_lt; rep_lia. }
+    { rewrite Zlength_map intr_lt; rep_lia. }
   - forward.
-    entailer!!.
-    rewrite replace_list_nil by rep_lia; auto.
+    entailer!.
+    rewrite -> replace_list_nil by rep_lia; auto.
   - forward.
-    rewrite Z.sub_simpl_r; entailer!!.
+    rewrite Z.sub_simpl_r; entailer!.
 Qed.
 
 Lemma chars_of_Z_eq : forall n, chars_of_Z n =
@@ -236,15 +239,13 @@ Proof.
   intros.
   destruct (Z.leb_spec n 0).
   { rewrite chars_of_Z_eq; simpl.
-  rewrite ?Zaux.Zdiv_eucl_unique in *.  (* Coq 8.15 and after *)
     apply Zdiv_le_compat_r with (p := 10) in H; try lia.
     rewrite Zdiv_0_l in H.
     destruct (Z.leb_spec (n / 10) 0); auto; lia. }
   induction n as [? IH] using (well_founded_induction (Zwf.Zwf_well_founded 0)).
-  rewrite chars_of_Z_eq, intr_eq.
+  rewrite chars_of_Z_eq intr_eq.
   destruct (n <=? 0) eqn: Hn; [apply Zle_bool_imp_le in Hn; lia|].
   simpl.
-  rewrite ?Zaux.Zdiv_eucl_unique in *.  (* Coq 8.15 and after *)
   destruct (n / 10 <=? 0) eqn: Hdiv.
   - apply Zle_bool_imp_le in Hdiv.
     assert (0 <= n / 10).
@@ -265,14 +266,14 @@ Proof.
   rewrite intr_eq.
   destruct (Z.leb_spec n 0); [rewrite Zlength_nil; lia|].
   rewrite Zlength_app.
-  assert (Zlength (intr (n / 10)) <= a - 1); [|rewrite Zlength_cons, Zlength_nil; lia].
+  assert (Zlength (intr (n / 10)) <= a - 1); [|rewrite Zlength_cons Zlength_nil; lia].
   assert (0 <= a - 1).
   { destruct (Z.eq_dec a 0); subst; simpl in *; lia. }
   apply H; auto.
   - split; try lia.
     apply Z.div_lt; auto; lia.
   - apply Zmult_lt_reg_r with 10; try lia.
-    rewrite (Z.mul_comm (10 ^ _)), <- Z.pow_succ_r by auto.
+    rewrite -> (Z.mul_comm (10 ^ _)), <- Z.pow_succ_r by auto.
     unfold Z.succ; rewrite Z.sub_simpl_r.
     eapply Z.le_lt_trans; eauto.
     rewrite Z.mul_comm; apply Z.mul_div_le; lia.
@@ -283,7 +284,7 @@ Proof.
   intros.
   rewrite chars_of_Z_intr.
   destruct (Z.leb_spec n 0); [|apply intr_length; lia].
-  rewrite Zlength_cons, Zlength_nil; lia.
+  rewrite Zlength_cons Zlength_nil; lia.
 Qed.
 
 Lemma body_print_int: semax_body Vprog Gprog f_print_int print_int_spec.
@@ -293,11 +294,11 @@ Proof.
   { split; auto; simpl; computable. }
   Intro buf.
   forward_if (buf <> nullval).
-  { if_tac; entailer!!. }
+  { if_tac; entailer!. }
   { forward_call 1; contradiction. }
   { forward.
-    entailer!!. }
-  Intros; rewrite if_false by auto.
+    entailer!. }
+  Intros; rewrite -> if_false by auto.
   forward_if (PROP ()
     LOCAL (temp _buf buf; gvars gv; temp _i (Vint (Int.repr i));
                  temp _k (Vint (Int.repr (Zlength (chars_of_Z i ++ [Byte.repr newline])))))
@@ -309,29 +310,28 @@ Proof.
     forward.
     forward.
     forward.
-    entailer!!.
+    entailer!.
   - Intros.
     sep_apply data_at__data_at.
     unfold default_val; simpl.
     assert (Zlength (intr i) <= 4).
     { apply intr_length; try lia. }
     forward_call (Ews, i, buf, [Vundef; Vundef; Vundef; Vundef; Vundef]).
-    { rewrite !Zlength_cons, Zlength_nil.
+    { rewrite -> !Zlength_cons, Zlength_nil.
       simpl; repeat (split; auto); rep_lia. }
     forward.
-    { entailer!!.
-      rewrite !Zlength_cons, Zlength_nil; rep_lia. }
+    { entailer!.
+      rewrite -> !Zlength_cons, Zlength_nil; rep_lia. }
     forward.
-    entailer!!.
-    { rewrite Zlength_app, Zlength_cons, Zlength_nil, chars_of_Z_intr.
+    entailer!.
+    { rewrite -> Zlength_app, Zlength_cons, Zlength_nil, chars_of_Z_intr.
       destruct (Z.leb_spec i 0); auto; lia. }
     unfold replace_list; simpl.
     rewrite (sublist_repeat _ _ 5 Vundef).
-    rewrite !Zlength_cons, Zlength_nil, Zlength_map; simpl.
+    rewrite -> !Zlength_cons, Zlength_nil, Zlength_map; simpl.
     rewrite upd_Znth_app2.
-    rewrite Zlength_map, Zminus_diag, upd_Znth0_old, sublist_repeat; try lia.
-    apply derives_refl'.
-    f_equal.
+    rewrite -> Zlength_map, Zminus_diag, upd_Znth0_old, sublist_repeat; try lia.
+    f_equiv.
     rewrite chars_of_Z_intr.
     destruct (Z.leb_spec i 0); try lia.
     rewrite zero_ext_inrange.
@@ -340,14 +340,14 @@ Proof.
     { simpl; rewrite Int.unsigned_repr; rep_lia. }
     { rewrite Zlength_repeat; lia. }
     { rewrite Zlength_repeat; lia. }
-    { rewrite Zlength_map, Zlength_repeat; lia. }
+    { rewrite Zlength_map Zlength_repeat; lia. }
     { rewrite Zlength_map; rep_lia. }
-    { rewrite !Zlength_cons, Zlength_nil, Zlength_map; lia. }
+    { rewrite -> !Zlength_cons, Zlength_nil, Zlength_map; lia. }
   - forward_call (Ews, buf, chars_of_Z i ++ [Byte.repr newline],
       5, repeat Vundef (Z.to_nat (4 - Zlength (chars_of_Z i))), tr).
-    { rewrite map_app, <- app_assoc; simpl; cancel. }
+    { rewrite -> map_app, <- app_assoc; simpl; cancel. }
     forward_call (tarray tuchar 5, buf, gv).
-    { rewrite if_false by auto; cancel. }
+    { rewrite -> if_false by auto; cancel. }
     forward.
 Qed.
 
@@ -365,13 +365,13 @@ Proof.
   rewrite bind_bind.
   apply eqit_bind; [reflexivity|].
   intros [].
-  - rewrite bind_ret_l, tau_eutt.
+  - rewrite bind_ret_l tau_eutt.
     rewrite unfold_iter.
-    rewrite bind_ret_l; reflexivity.
+    rewrite bind_ret_l //.
   - rewrite bind_bind.
     apply eqit_bind; [reflexivity|].
     intro.
-    rewrite bind_ret_l, tau_eutt; reflexivity.
+    rewrite bind_ret_l tau_eutt //.
 Qed.
 
 Lemma for_loop_eq : forall {file_id} i z body,
@@ -384,9 +384,9 @@ Proof.
   rewrite bind_bind.
   apply eqit_bind; [reflexivity|].
   intros [].
-  - rewrite bind_ret_l, tau_eutt, unfold_iter.
-    rewrite bind_ret_l; reflexivity.
-  - rewrite bind_ret_l, tau_eutt; reflexivity.
+  - rewrite bind_ret_l tau_eutt unfold_iter.
+    rewrite bind_ret_l //.
+  - rewrite bind_ret_l tau_eutt //.
 Qed.
 
 Lemma sum_Z_app : forall l1 l2, sum_Z (l1 ++ l2) = sum_Z l1 + sum_Z l2.
@@ -398,131 +398,132 @@ Qed.
 Lemma body_main: semax_body Vprog Gprog f_main main_spec.
 Proof.
   start_function.
+  rename a into gv.
   sep_apply (has_ext_ITREE(E := @IO_event nat)).
-  rewrite <- (emp_sepcon (ITREE _)); Intros.
+  rewrite <- (bi.emp_sep (ITREE _)); Intros.
   replace_SEP 0 (mem_mgr gv) by (go_lower; apply create_mem_mgr).
   forward.
   forward_call (tarray tuchar 4, gv).
   { simpl; repeat (split; auto); rep_lia. }
   Intro buf.
   forward_if (buf <> nullval).
-  { if_tac; entailer!!. }
+  { if_tac; entailer!. }
   { forward_call 1; contradiction. }
   { forward.
     entailer!. }
-  Intros; rewrite if_false by auto.
+  Intros; rewrite -> if_false by auto.
   unfold main_itree.
   forward_call (Ews, buf, 4, fun lc => read_sum 0 lc).
   { simpl; cancel. }
   Intros lc.
-  set (Inv := EX n : Z, EX lc : list byte,
+  set (Inv := ∃ n : Z, ∃ lc : list byte,
     PROP (0 <= n < 1040)
     LOCAL (temp _i (Vint (Int.repr 4)); temp _buf buf; temp _n (Vint (Int.repr n)); gvars gv)
     SEP (ITREE (read_sum n lc); data_at Ews (tarray tuchar 4) (map Vubyte lc) buf;
       mem_mgr gv; malloc_token Ews (tarray tuchar 4) buf)).
   forward_while Inv.
-  { Exists 0 lc; entailer!!. }
-  { entailer!!. }
+  { Exists 0 lc; entailer!. }
+  { entailer!. }
   - clear dependent lc; rename lc0 into lc.
     rewrite read_sum_eq.
-    rewrite if_true by auto; simpl ITREE.
+    rewrite -> if_true by auto; simpl ITREE.
     set (nums := map (fun i => Byte.unsigned i - char0) lc).
     assert_PROP (Zlength lc = 4).
     { entailer!.
-      rewrite Zlength_map in *; auto. }
+      rewrite -> Zlength_map in *; auto. }
     assert (Zlength nums = 4) by (subst nums; rewrite Zlength_map; auto).
-    forward_for_simple_bound 4 (EX j : Z, PROP (0 <= n + sum_Z (sublist 0 j nums) < 1000 + 10 * j)
+    forward_for_simple_bound 4 (∃ j : Z, PROP (0 <= n + sum_Z (sublist 0 j nums) < 1000 + 10 * j)
      LOCAL (temp _i (Vint (Int.repr 4)); temp _buf buf; temp _n (Vint (Int.repr (n + sum_Z (sublist 0 j nums)))); gvars gv)
      SEP (ITREE (b <- for_loop j 4
          (read_sum_inner n nums) ;; if (b : bool) then Ret tt else lc' <- read_list stdin 4 ;; read_sum (n + sum_Z nums) lc');
              data_at Ews (tarray tuchar 4) (map Vubyte lc) buf; mem_mgr gv; malloc_token Ews (tarray tuchar 4) buf)).
-    + entailer!!. lia.
+    + entailer!.
+      { lia. }
     + simpl.
       forward.
       { entailer!.
         unfold Vubyte; simpl.
         rewrite Int.unsigned_repr; rep_lia. }
       forward.
-      rewrite Znth_map by lia; simpl.
+      rewrite -> Znth_map by lia; simpl.
       rewrite zero_ext_inrange.
       forward.
       unfold Int.sub.
-      rewrite !Int.unsigned_repr by rep_lia.
+      rewrite -> !Int.unsigned_repr by rep_lia.
       forward_if (0 <= Byte.unsigned (Znth i lc) - char0 < 10).
       { forward_call (tarray tuchar 4, buf, gv).
-        { rewrite if_false by auto; cancel. }
+        { rewrite -> if_false by auto; cancel. }
         forward.
-        entailer!!.
+        entailer!.
         rewrite for_loop_eq.
         destruct (Z.ltb_spec i 4); try lia.
         unfold read_sum_inner at 1.
         replace (_ || _)%bool with true.
         rewrite !bind_ret_l; auto.
         { symmetry; rewrite orb_true_iff.
-          subst nums; rewrite Znth_map by lia.
+          subst nums; rewrite -> Znth_map by lia.
           destruct (Z.ltb_spec (Byte.unsigned (Znth i lc) - char0) 0); auto.
-          rewrite Int.unsigned_repr in * by (unfold char0 in *; rep_lia).
+          rewrite -> Int.unsigned_repr in * by (unfold char0 in *; rep_lia).
           left; apply Z.leb_le; unfold char0 in *; lia. } }
       { forward.
-        entailer!!.
-        rewrite Int.unsigned_repr_eq in *.
+        entailer!.
+        rewrite -> Int.unsigned_repr_eq in *.
         destruct (zlt (Byte.unsigned (Znth i lc)) char0).
         { unfold char0 in *; rewrite <- Z_mod_plus_full with (b := 1), Zmod_small in *; rep_lia. }
-        unfold char0 in *; rewrite Zmod_small in *; rep_lia. }
+        unfold char0 in *; rewrite -> Zmod_small in *; rep_lia. }
       forward.
       rewrite add_repr.
       rewrite for_loop_eq.
       destruct (Z.ltb_spec i 4); try lia.
       unfold read_sum_inner at 1.
-      unfold nums; rewrite Znth_map by lia.
+      unfold nums; rewrite -> Znth_map by lia.
       assert (((10 <=? Byte.unsigned (Znth i lc) - char0) || (Byte.unsigned (Znth i lc) - char0 <? 0))%bool = false) as Hin.
       { rewrite orb_false_iff.
         split; [apply Z.leb_nle | apply Z.ltb_nlt]; lia. }
       rewrite Hin.
       assert (sublist 0 (i + 1) nums = sublist 0 i nums ++ [Byte.unsigned (Znth i lc) - char0]) as Hi.
-      { rewrite (sublist_split _ i (i + 1)), (sublist_one i (i + 1)) by lia.
+      { rewrite -> (sublist_split _ i (i + 1)), (sublist_one i (i + 1)) by lia.
         f_equal; subst nums.
-        rewrite Znth_map by lia; auto. }
+        rewrite -> Znth_map by lia; auto. }
       forward_call (gv, n + sum_Z (sublist 0 (i + 1) nums),
         b <- for_loop (i + 1) 4 (read_sum_inner n nums) ;; if (b : bool) then Ret tt else lc' <- read_list stdin 4 ;; read_sum (n + sum_Z nums) lc').
-      { entailer!!.
-        rewrite Hi, sum_Z_app; simpl.
-        rewrite Z.add_assoc, Z.add_0_r; auto. }
-      { rewrite sepcon_assoc; apply sepcon_derives; cancel.
+      { entailer!.
+        rewrite Hi sum_Z_app; simpl.
+        rewrite Z.add_assoc Z.add_0_r; auto. }
+      { apply bi.sep_mono; last cancel.
         rewrite !bind_bind.
         apply ITREE_impl.
         apply eqit_bind; [reflexivity|].
         intros [].
         rewrite bind_ret_l; reflexivity. }
-      { rewrite Hi, sum_Z_app; simpl; lia. }
-      entailer!!.
-      { rewrite Hi, sum_Z_app; simpl.
-        rewrite Z.add_0_r, Z.add_assoc; split; auto; lia. }
-      { rewrite Int.unsigned_repr by rep_lia.
+      { rewrite Hi sum_Z_app; simpl; lia. }
+      entailer!.
+      { rewrite Hi sum_Z_app; simpl.
+        rewrite Z.add_0_r Z.add_assoc; split; auto; lia. }
+      { rewrite -> Int.unsigned_repr by rep_lia.
         pose proof (Byte.unsigned_range (Znth i lc)) as [_ Hmax].
         unfold Byte.modulus, two_power_nat in Hmax; simpl in *; lia. }
     + rewrite for_loop_eq.
       destruct (Z.ltb_spec 4 4); try lia.
       forward_call (Ews, buf, 4, fun lc' => read_sum (n + sum_Z nums) lc').
-      { rewrite sepcon_assoc; apply sepcon_derives; cancel.
-        simpl; rewrite bind_ret_l; auto. }
+      { simpl; rewrite bind_ret_l; cancel. }
       Intros lc'.
       forward.
-      rewrite sublist_same in * by auto.
+      rewrite -> sublist_same in * by auto.
       Exists (n + sum_Z nums, lc'); entailer!.
       apply derives_refl.
   - subst Inv.
     forward_call (tarray tuchar 4, buf, gv).
-    { rewrite if_false by auto; cancel. }
+    { rewrite -> if_false by auto; cancel. }
     forward.
     cancel.
     rewrite read_sum_eq.
-    rewrite if_false; [auto | lia].
+    if_tac; auto; lia.
 Qed.
 
 Definition ext_link := ext_link_prog prog.
 
-#[export] Instance Espec : OracleKind := IO_Espec ext_link.
+#[local] Instance IO_ext_spec : ext_spec IO_itree := IO_ext_spec ext_link.
 
 Lemma prog_correct:
   semax_prog prog main_itree Vprog Gprog.
@@ -530,18 +531,23 @@ Proof.
 prove_semax_prog.
 semax_func_cons body_exit.
 semax_func_cons body_free.
-semax_func_cons body_malloc. apply semax_func_cons_malloc_aux.
+semax_func_cons body_malloc.
+{ destruct x; apply semax_func_cons_malloc_aux. }
 semax_func_cons_ext.
-{ simpl; Intro msg.
+{ simpl; destruct x as (((?, ?), ?), ?); monPred.unseal; Intro msg.
   apply typecheck_return_value with (t := Tint16signed); auto. }
 semax_func_cons_ext.
+{ simpl; destruct x as (((((?, ?), ?), ?), ?), ?).
+  apply typecheck_return_value with (t := Tint16signed); auto. }
 semax_func_cons body_print_intr.
 semax_func_cons body_print_int.
 semax_func_cons body_main.
 Qed.
 
+End IO.
+
 Require Import VST.veric.SequentialClight.
-Require Import VST.progs.io_mem_dry.
+Require Import VST.progs64.io_mem_dry.
 
 Definition init_mem_exists : { m | Genv.init_mem prog = Some m }.
 Proof.
@@ -574,26 +580,19 @@ Qed.
 
 Definition main_block := proj1_sig main_block_exists.
 
-Axiom (Jsub: forall ef se lv m t v m' (EFI : ef_inline ef = true) m1
-       (EFC : Events.external_call ef se lv m t v m'), juicy_mem.mem_sub m m1 ->
-       exists m1' (EFC1 : Events.external_call ef se lv m1 t v m1'),
-         juicy_mem.mem_sub m' m1' /\ proj1_sig (Clight_core.inline_external_call_mem_events _ _ _ _ _ _ _ EFI EFC1) =
-         proj1_sig (Clight_core.inline_external_call_mem_events _ _ _ _ _ _ _ EFI EFC)).
-
 Theorem prog_toplevel : exists q,
   semantics.initial_core (Clight_core.cl_core_sem (globalenv prog)) 0 init_mem q init_mem (Vptr main_block Ptrofs.zero) [] /\
   forall n, @step_lemmas.dry_safeN _ _ _ _ semax.genv_symb_injective (Clight_core.cl_core_sem (globalenv prog))
-             (io_dry_spec ext_link) {| genv_genv := Genv.globalenv prog; genv_cenv := prog_comp_env prog |} n
+             io_dry_spec {| genv_genv := Genv.globalenv prog; genv_cenv := prog_comp_env prog |} n
             main_itree q init_mem.
 Proof.
-  edestruct whole_program_sequential_safety_ext with (V := Vprog) as (b & q & Hb & Hq & Hsafe).
-  - repeat intro; simpl. apply I.
-  - apply Jsub.
-  - apply add_funspecs_frame.
-  - apply juicy_dry_specs.
-  - apply dry_spec_mem.
-  - intros; apply I.
-  - apply CSHL_Sound.semax_prog_sound, prog_correct.
+  edestruct whole_program_sequential_safety_ext with (Espec := @IO_ext_spec (VSTΣ (@IO_itree (@IO_event nat))))(V := Vprog) as (b & q & Hb & Hq & Hsafe).
+  - apply SequentialClight.subG_VSTGpreS, subG_refl.
+  - repeat intro; apply I.
+  - apply io_spec_sound.
+    intros ?? [<- | [<- | ?]]; last done;
+      rewrite /ext_link /ext_link_prog /prog /=; repeat (if_tac; first done); done.
+  - intros; apply CSHL_Sound.semax_prog_sound, prog_correct.
   - apply (proj2_sig init_mem_exists).
   - exists q.
     rewrite (proj2_sig main_block_exists) in Hb; inv Hb.
diff --git a/progs/verif_load_demo.v b/progs/verif_load_demo.v
index f87b79b667..17e45ade3d 100644
--- a/progs/verif_load_demo.v
+++ b/progs/verif_load_demo.v
@@ -178,7 +178,7 @@ Lemma body_get22_root_expr: semax_body Vprog Gprog f_get22 get22_spec.
  forward.
  simpl (temp _p _).
  (* Assert_PROP what forward asks us for (only for the root expression "p"):  *)
- assert_PROP (offset_val 8 (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
+ assert_PROP (offset_val (64/8) (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
    = field_address (tarray pair_pair_t array_size) [StructField _right; ArraySubsc i] pps) as E. {
    entailer!. rewrite field_compatible_field_address by auto with field_compatible.
   simpl. normalize.
@@ -199,7 +199,7 @@ simpl (temp _p _).
 
 (* Assert_PROP what forward asks us for (for the full expression "p->snd"): *)
 assert_PROP (
-  offset_val 4 (offset_val 8 (force_val
+  offset_val (32/8) (offset_val (64/8) (force_val
     (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))
   = (field_address (tarray pair_pair_t array_size)
                    [StructField _snd; StructField _right; ArraySubsc i] pps)). {
@@ -220,7 +220,7 @@ forward.
 simpl (temp _p _).
 
 (* Alternative: Make p nice enough so that no hint is required: *)
-assert_PROP (offset_val 8 (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
+assert_PROP (offset_val (64/8) (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
   = field_address (tarray pair_pair_t array_size) [StructField _right; ArraySubsc i] pps) as E. {
   entailer!. rewrite field_compatible_field_address by auto with field_compatible.
   simpl.
diff --git a/progs/verif_logical_compare.v b/progs/verif_logical_compare.v
index 5aadb55f61..bbca4ceeef 100644
--- a/progs/verif_logical_compare.v
+++ b/progs/verif_logical_compare.v
@@ -1,7 +1,6 @@
 Require Import VST.floyd.proofauto.
 Require Import VST.floyd.compat.
 Require Import VST.progs.logical_compare.
-Import compcert.lib.Maps.
 
 #[export] Instance CompSpecs : compspecs. Proof. make_compspecs prog. Defined.
 
@@ -16,16 +15,16 @@ Definition logical_or_result v1 v2 : int :=
 Fixpoint quick_shortcut_logical (s: statement) : option ident :=
 match s with
 | Sifthenelse _
-     (Sset id (Econst_int _ (Tint I32 Signed {| attr_volatile := false; attr_alignas := None |})))
+     (Sset id (Econst_int _ (Tint I32 Signed {| attr_volatile := false; attr_alignas := None |} )))
      s2 => match quick_shortcut_logical s2 with None => None | Some id2 =>
                  if ident_eq id id2 then Some id else None
                 end
 | Sifthenelse _ s2
-     (Sset id (Econst_int _ (Tint I32 Signed {| attr_volatile := false; attr_alignas := None |})))
+     (Sset id (Econst_int _ (Tint I32 Signed {| attr_volatile := false; attr_alignas := None |} )))
       => match quick_shortcut_logical s2 with None => None | Some id2 =>
                  if ident_eq id id2 then Some id else None
             end
-| Sset id (Ecast _ (Tint IBool Unsigned {| attr_volatile := false; attr_alignas := None |})) =>
+| Sset id (Ecast _ (Tint IBool Unsigned {| attr_volatile := false; attr_alignas := None |} )) =>
         Some id
 | _ => None
 end.
@@ -34,7 +33,7 @@ Fixpoint shortcut_logical (eval: expr -> option val) (tid: ident) (s: statement)
             : option (int * list expr) :=
 match s with
 | Sifthenelse e1
-     (Sset id (Econst_int one (Tint I32 Signed {| attr_volatile := false; attr_alignas := None |})))
+     (Sset id (Econst_int one (Tint I32 Signed {| attr_volatile := false; attr_alignas := None |} )))
      s2 => if andb (eqb_ident id tid) (Int.eq one Int.one)
                 then match eval e1 with
                         | Some (Vint v1) =>
@@ -46,7 +45,7 @@ match s with
                         end
                 else None
 | Sifthenelse e1 s2
-     (Sset id (Econst_int zero (Tint I32 Signed {| attr_volatile := false; attr_alignas := None |})))
+     (Sset id (Econst_int zero (Tint I32 Signed {| attr_volatile := false; attr_alignas := None |} )))
       => if andb (eqb_ident id tid) (Int.eq zero Int.zero)
             then match eval e1 with
                      | Some (Vint v1) =>
@@ -57,7 +56,7 @@ match s with
                    | _ => None
                 end
             else None
-| Sset id (Ecast e (Tint IBool Unsigned {| attr_volatile := false; attr_alignas := None |})) =>
+| Sset id (Ecast e (Tint IBool Unsigned {| attr_volatile := false; attr_alignas := None |} )) =>
         if eqb_ident id tid
         then match eval (Ecast e tbool) with
                  | Some (Vint v) => Some (v, (Ecast e tbool :: nil))
@@ -68,20 +67,20 @@ match s with
 end.
 
 Lemma semax_shortcut_logical:
-  forall Espec {cs: compspecs} Delta P Q R tid s v Qtemp Qvar GV el,
+  forall Espec {cs: compspecs} E Delta P Q R tid s v Qtemp Qvar GV el,
    quick_shortcut_logical s = Some tid ->
    typeof_temp Delta tid = Some tint ->
    local2ptree Q = (Qtemp, Qvar, nil, GV) ->
-   Qtemp ! tid = None ->
+   Qtemp !! tid = None ->
    shortcut_logical (msubst_eval_expr Delta Qtemp Qvar GV) tid s = Some (v, el) ->
    ENTAIL Delta, PROPx P (LOCALx Q (SEPx R)) |-- fold_right (fun e q => tc_expr Delta e && q) TT el ->
-   @semax cs Espec Delta (PROPx P (LOCALx Q (SEPx R)))
+   semax(OK_spec := Espec)(C := cs) E Delta (PROPx P (LOCALx Q (SEPx R)))
           s (normal_ret_assert (PROPx P (LOCALx (temp tid (Vint v) :: Q) (SEPx R)))).
 Admitted.
 
 (***** END *)
 
-Definition do_or_spec :=
+Definition do_or_spec : ident * funspec :=
  DECLARE _do_or
   WITH a: int, b : int
   PRE [ tbool, tbool ]
@@ -91,7 +90,7 @@ Definition do_or_spec :=
         SEP().
 
 
-Definition do_and_spec :=
+Definition do_and_spec : ident * funspec :=
  DECLARE _do_and
   WITH a: int, b : int
   PRE [ tbool, tbool ]
@@ -121,7 +120,6 @@ Ltac do_semax_shortcut_logical :=
 Lemma body_do_or: semax_body Vprog Gprog f_do_or do_or_spec.
 Proof.
 start_function.
-
 eapply semax_seq'; [do_semax_shortcut_logical | abbreviate_semax].
 forward.
 destruct H,H0; subst; simpl; entailer!.
@@ -141,8 +139,6 @@ start_function.
 forward.
 Qed.
 
-#[export] Existing Instance NullExtension.Espec.
-
 Lemma prog_correct:
   semax_prog prog tt Vprog Gprog.
 Proof.
@@ -151,4 +147,3 @@ semax_func_cons body_do_or.
 semax_func_cons body_do_and.
 semax_func_cons body_main.
 Qed.
-
diff --git a/progs/verif_merge.v b/progs/verif_merge.v
index 21525aed33..1715ea3fd7 100644
--- a/progs/verif_merge.v
+++ b/progs/verif_merge.v
@@ -1,9 +1,8 @@
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs.merge.
 Require Import VST.progs.list_dt. Import LsegSpecial.
 
-Open Scope logic.
-
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
diff --git a/progs/verif_message.v b/progs/verif_message.v
index 9d37188b86..7f22f60aa3 100644
--- a/progs/verif_message.v
+++ b/progs/verif_message.v
@@ -171,6 +171,7 @@ Lemma body_main: semax_body Vprog Gprog f_main main_spec.
 Proof.
 function_pointers.
 start_function.
+rename a into gv.
 set (ipm := gv _intpair_message).
 fold cc_default noattr.
 make_func_ptr _intpair_deserialize.
diff --git a/progs/verif_object.v b/progs/verif_object.v
index 5e9054604c..f56c5fbc3a 100644
--- a/progs/verif_object.v
+++ b/progs/verif_object.v
@@ -1,11 +1,14 @@
 Require Import VST.floyd.proofauto.
-Require Import VST.floyd.compat.
 Require Import VST.floyd.library.
 Require Import VST.progs.object.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
+Section Spec.
+
+Context  `{!default_VSTGS Σ}.
+
 Local Open Scope Z.
 
 Definition object_invariant := list Z -> val -> mpred.
@@ -29,39 +32,39 @@ Definition twiddle_spec (instance: object_invariant) :=
           PARAMS (self; Vint (Int.repr i))
           SEP (instance history self)
   POST [ tint ]
-      EX v: Z, 
+      ∃ v: Z, 
           PROP(2* fold_right Z.add 0 history < v <= 2* fold_right Z.add 0 (i::history))
           RETURN (Vint (Int.repr v))
           SEP(instance (i::history) self).
 
 Definition object_methods (instance: object_invariant) (mtable: val) : mpred :=
-  EX sh: share, EX reset: val, EX twiddle: val,
-  !! readable_share sh && 
-  func_ptr (reset_spec instance) reset *
-  func_ptr (twiddle_spec instance) twiddle *
+  ∃ (sh: share) (reset: val) (twiddle: val),
+  ⌜readable_share sh⌝ ∧
+  func_ptr (reset_spec instance) reset ∗
+  func_ptr (twiddle_spec instance) twiddle ∗
   data_at sh (Tstruct _methods noattr) (reset,twiddle) mtable.
 
 Lemma object_methods_local_facts: forall instance p,
-  object_methods instance p |-- !! isptr p.
+  object_methods instance p ⊢ ⌜isptr p⌝.
 Proof.
 intros.
 unfold object_methods.
 Intros sh reset twiddle.
 entailer!.
 Qed.
-#[export] Hint Resolve object_methods_local_facts : saturate_local.
+Hint Resolve object_methods_local_facts : saturate_local.
 
 Definition object_mpred (history: list Z) (self: val) : mpred :=
-  EX instance: object_invariant, EX mtable: val, 
-       (object_methods instance mtable *
-     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable self*
+  ∃ (instance: object_invariant) (mtable: val), 
+       (object_methods instance mtable ∗
+     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable self∗
      instance history self).
 
 Definition foo_invariant : object_invariant :=
   (fun (history: list Z) p =>
     withspacer Ews (sizeof size_t + sizeof tint) (2 * sizeof size_t) (field_at Ews (Tstruct _foo_object noattr) 
             [StructField _data] (Vint (Int.repr (2*fold_right Z.add 0 history)))) p
-      *  malloc_token Ews (Tstruct _foo_object noattr) p).
+      ∗  malloc_token Ews (Tstruct _foo_object noattr) p).
 
 Definition foo_reset_spec :=
  DECLARE _foo_reset (reset_spec foo_invariant).
@@ -76,7 +79,7 @@ Definition make_foo_spec :=
     PROP () PARAMS() GLOBALS (gv) 
     SEP (mem_mgr gv; object_methods foo_invariant (gv _foo_methods))
  POST [ tobject ]
-    EX p: val, PROP () RETURN (p)
+    ∃ p: val, PROP () RETURN (p)
      SEP (mem_mgr gv; object_mpred nil p; object_methods foo_invariant (gv _foo_methods)).
 
 Definition main_spec :=
@@ -84,21 +87,28 @@ Definition main_spec :=
   WITH gv: globals
   PRE  [] main_pre prog tt gv
   POST [ tint ]
-     EX i:Z, PROP(0<=i<=6) RETURN (Vint (Int.repr i)) SEP(TT).
+     ∃ i:Z, PROP(0<=i<=6) RETURN (Vint (Int.repr i)) SEP(True).
 
 Definition Gprog : funspecs :=   ltac:(with_library prog [
     foo_reset_spec; foo_twiddle_spec; make_foo_spec; main_spec]).
 
 Lemma object_mpred_i:
   forall (history: list Z) (self: val) (instance: object_invariant) (mtable: val),
-    object_methods instance mtable *
-     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable self *
+    object_methods instance mtable ∗
+     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable self ∗
      instance history self 
-    |-- object_mpred history self.
+    ⊢ object_mpred history self.
 Proof.
 intros. unfold object_mpred. Exists instance mtable; auto.
 Qed.
 
+
+Lemma bind_ret0_unfold:
+  forall Q, bind_ret None tvoid Q ⊣⊢ (@assert_of Σ (fun rho => Q (globals_only rho))).
+Proof.
+  rewrite /bind_ret; split => rho; monPred.unseal; done.
+Qed.
+
 Lemma body_foo_reset: semax_body Vprog Gprog f_foo_reset foo_reset_spec.
 Proof.
 unfold foo_reset_spec, foo_invariant, reset_spec.
@@ -128,36 +138,30 @@ simpl.
 Exists (2 * fold_right Z.add 0 history + i).
 simpl;
 entailer!!.
-rewrite Z.mul_add_distr_l, Z.add_comm.
+rewrite ->Z.mul_add_distr_l, Z.add_comm.
 unfold withspacer; simpl.
 entailer!!.
 Qed.
 
 Lemma split_object_methods:
   forall instance m, 
-    object_methods instance m |-- object_methods instance m * object_methods instance m.
+    object_methods instance m ⊢ object_methods instance m ∗ object_methods instance m.
 Proof.
 intros.
 unfold object_methods.
 Intros sh reset twiddle.
-
-Exists (fst (slice.cleave sh)) reset twiddle.
-Exists (snd (slice.cleave sh)) reset twiddle.
-rewrite (split_func_ptr (reset_spec instance) reset) at 1.
-rewrite (split_func_ptr (twiddle_spec instance) twiddle) at 1.
-entailer!!.
-split.
-apply slice.cleave_readable1; auto.
-apply slice.cleave_readable2; auto.
-rewrite (data_at_share_join (fst (slice.cleave sh)) (snd (slice.cleave sh)) sh).
-auto.
-apply slice.cleave_join.
+destruct (slice.split_readable_share sh) as (sh1 & sh2 & ? & ? & ?); [assumption|].
+Exists sh1 reset twiddle.
+Exists sh2 reset twiddle.
+rewrite <- (data_at_share_join sh1 sh2 sh) by assumption.
+iIntros "(#$ & #$ & $ & $)"; auto.
 Qed.
 
 Lemma body_make_foo: semax_body Vprog Gprog f_make_foo make_foo_spec.
 Proof.
 unfold make_foo_spec.
 start_function.
+rename a into gv.
 forward_call (Tstruct _foo_object noattr, gv).
 Intros p.
 forward_if
@@ -174,7 +178,7 @@ if_tac; entailer!!.
 forward_call 1.
 contradiction.
 *
-rewrite if_false by auto.
+rewrite ->if_false by auto.
 Intros.
 forward.  (*  /*skip*/;  *)
 entailer!!.
@@ -194,9 +198,7 @@ unfold_data_at (field_at _ _ nil _ p).
 cancel.
 unfold withspacer; simpl.
 rewrite !field_at_data_at.
-simpl.
-apply derives_refl'.
-rewrite <- ?sepcon_assoc. (* needed if Archi.ptr64=true *)
+cancel.
 rewrite !field_compatible_field_address; auto with field_compatible.
 clear - H.
 (* TODO: simplify the following proof. *)
@@ -220,14 +222,13 @@ reflexivity.
 left; auto.
 Qed.
 
-
 Lemma make_object_methods:
-  forall sh instance reset twiddle mtable,
+  forall sh instance reset twiddle (mtable: val),
   readable_share sh ->
-  func_ptr (reset_spec instance) reset *
-  func_ptr (twiddle_spec instance) twiddle *
+  func_ptr (reset_spec instance) reset ∗
+  func_ptr (twiddle_spec instance) twiddle ∗
   data_at sh (Tstruct _methods noattr) (reset, twiddle) mtable
-  |-- object_methods instance mtable.
+  ⊢ object_methods instance mtable.
 Proof.
   intros.
   unfold object_methods.
@@ -238,7 +239,7 @@ Qed.
 Ltac method_call witness hist' result :=
 repeat apply seq_assoc1;
 match goal with 
-   |- semax _ (PROPx _ (LOCALx ?Q (SEPx ?R))) 
+   |- semax _ _ (PROPx _ (LOCALx ?Q (SEPx ?R))) 
             (Ssequence (Sset ?mt (Efield (Ederef (Etempvar ?x _)  _) _ _))
                  _) _  =>
     match Q with context [temp ?x ?x'] =>
@@ -262,6 +263,7 @@ end.
 Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
 Proof.
 start_function.
+rename a into gv.
 sep_apply (create_mem_mgr gv).
 (* assert_gvar _foo_methods. (* TODO: this is needed for a field_compatible later on *) *)
 fold noattr cc_default.
@@ -273,8 +275,8 @@ replace_SEP 0 (data_at Ews (Tstruct _methods noattr)
   unfold_data_at (data_at _ (Tstruct _methods _) _ (gv _foo_methods)).
   rewrite <- mapsto_field_at with (gfs := [StructField _twiddle]) (v:= (gv _foo_twiddle))
   by  auto with field_compatible.
-  rewrite field_at_data_at.  rewrite !field_compatible_field_address by auto with field_compatible.
-  rewrite !isptr_offset_val_zero by auto.
+  rewrite field_at_data_at.  rewrite ->!field_compatible_field_address by auto with field_compatible.
+  rewrite ->!isptr_offset_val_zero by auto.
   cancel.
 }
 
@@ -293,7 +295,6 @@ assert_PROP (p<>Vundef) by entailer!.
    Method 1:  comment out lines AA and BB and the entire range CC-DD.
    Method 2:  comment out lines AA-BB, inclusive.
 *)
-
 (* AA *) try (tryif 
   (method_call (p, @nil Z) (@nil Z) whatever;
    method_call (p, 3, @nil Z) [3%Z] i;
@@ -341,7 +342,4 @@ forward.  (* return i; *)
 Exists i; entailer!!.
 Qed.
 
-
-
-
-
+End Spec.
diff --git a/progs/verif_objectSelf.v b/progs/verif_objectSelf.v
index 40d876b145..c62937bf0a 100644
--- a/progs/verif_objectSelf.v
+++ b/progs/verif_objectSelf.v
@@ -1,14 +1,14 @@
+Require Import iris.bi.lib.fixpoint.
 Require Import VST.floyd.proofauto.
-Require Import VST.floyd.compat.
 Require Import VST.floyd.library.
 Require Import VST.progs.objectSelf.
 
-Require Import VST.floyd.Funspec_old_Notation.
-
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
-Local Open Scope Z.
+Section mpred.
+
+Context `{!default_VSTGS Σ}.
 
 (*Andrew's definition
 Definition object_invariant := list Z -> val -> mpred.*)
@@ -21,61 +21,48 @@ Definition tobject := tptr (Tstruct _object noattr).
 
 Definition reset_spec (instance: object_invariant) :=
   WITH hs:ObjInv (*modified*)
-  PRE [ _self OF tobject]
+  PRE [ tobject]
           PROP (isptr (snd hs) (*NEW*))
-          LOCAL (temp _self (snd hs))
+          PARAMS (snd hs)
           SEP (instance hs)
   POST [ tvoid ]
           PROP() LOCAL () SEP(instance (nil, snd hs)).
 
 Definition twiddle_spec (instance: object_invariant) :=
   WITH hs: ObjInv, i: Z (*modified*)
-  PRE [ _self OF tobject, _i OF tint]
+  PRE [ tobject, tint]
           PROP (0 < i <= Int.max_signed / 4;
                 0 <= fold_right Z.add 0 (fst hs) <= Int.max_signed / 4; 
                isptr (snd hs) (*NEW*))
-          LOCAL (temp _self (snd hs); temp _i (Vint (Int.repr i)))
+          PARAMS (snd hs; Vint (Int.repr i))
           SEP (instance hs)
   POST [ tint ]
-      EX v: Z, 
+      ∃ v: Z,
           PROP(2* fold_right Z.add 0 (fst hs) < v <= 2* fold_right Z.add 0 (i::(fst hs)))
           LOCAL (temp ret_temp (Vint (Int.repr v))) 
           SEP(instance (i::(fst hs), snd hs)).
-(*
-Require Import VST.concurrency.conclib.
-Require Import VST.concurrency.semax_conc.
-Require Import VST.msl.seplog.
-Require Import VST.msl.predicates_hered.
-Lemma Contractive: forall Q R v, 
-  predicates_hered.allp (fun x : ObjInv => |> R x <=> |> Q x)
-  |-- func_ptr (reset_spec R) v <=> func_ptr (reset_spec Q) v.
-Proof. intros. rewrite fash_andp. apply andp_right. 
-+ red. intros n N. unfold func_ptr, func_ptr_si. apply subp_exp.
-Search seplog.imp fash. exp.
- red. intros r. simpl. apply subp_i1. Search fash seplog.imp. unfold func_ptr, func_ptr_si.
-apply eqp_exp. p_right. red.
-   *)
+
 Definition object_methods (instance: object_invariant) (mtable: val) : mpred :=
-  EX sh: share, EX reset: val, EX twiddle: val, EX twiddleR:val,
-  !! readable_share sh && 
-  func_ptr' (reset_spec instance) reset *
-  func_ptr' (twiddle_spec instance) twiddle *
-  func_ptr' (twiddle_spec instance) twiddleR *
+  ∃ sh: share, ∃ reset: val, ∃ twiddle: val, ∃ twiddleR:val,
+  ⌜readable_share sh⌝ ∧
+  func_ptr (reset_spec instance) reset ∗
+  func_ptr (twiddle_spec instance) twiddle ∗
+  func_ptr (twiddle_spec instance) twiddleR ∗
   data_at sh (Tstruct _methods noattr) (reset,(twiddle, twiddleR)) mtable.
 
 Lemma object_methods_local_facts: forall instance p,
-  object_methods instance p |-- !! isptr p.
+  object_methods instance p ⊢ ⌜isptr p⌝.
 Proof.
 intros.
 unfold object_methods.
 Intros sh reset twiddle twiddleR.
 entailer!.
 Qed.
-#[export] Hint Resolve object_methods_local_facts : saturate_local.
+Hint Resolve object_methods_local_facts : saturate_local.
 
 (*Andrew's definition
 Definition object_mpred (history: list Z) (self: val) : mpred :=
-  EX instance: object_invariant, EX mtable: val, 
+  ∃ instance: object_invariant, ∃ mtable: val, 
        (object_methods instance mtable *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable self*
      instance history self).*)
@@ -84,250 +71,67 @@ Section ObjMpred.
 Variable instance: object_invariant.
 
 Definition F (X: ObjInv -> mpred) (hs: ObjInv): mpred :=
-   ((EX mtable: val, !!(isptr mtable) (*This has to hold NOW, not ust LATER*)&&
-     (|> object_methods X mtable) *
-     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
-
-Definition HOcontractive1 {A: Type}{NA: NatDed A}{IA: Indir A}{RI: RecIndir A}{X: Type}
-     (f: (X -> A) -> (X -> A)) := 
- forall P Q : X -> A,
- ALL x : X, |> fash (P x <--> Q x)
- |-- ALL x : X, fash (f P x --> f Q x).
-
-Lemma HOcontractive_i1:
- forall  (A: Type)(NA: NatDed A){IA: Indir A}{RI: RecIndir A}{X: Type}
-     (f: (X -> A) -> (X -> A)),
-  HOcontractive1 f -> HOcontractive f.
-Proof.
-intros.
-red in H|-*.
-intros.
-eapply derives_trans.
-apply andp_right.
-apply H.
-specialize (H Q P).
-eapply derives_trans.
-2: apply H.
-apply allp_derives; intros.
-apply later_derives.
-apply fash_derives.
-rewrite andp_comm.
-auto.
-apply allp_right; intro.
-rewrite fash_andp.
-apply andp_right.
-apply andp_left1.
-apply allp_left with v; auto.
-apply andp_left2.
-apply allp_left with v; auto.
-Qed.
+   ((∃ mtable: val, ⌜isptr mtable⌝ (*This has to hold NOW, not just LATER*)∧
+     (▷ object_methods X mtable) ∗
+     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) ∗
+   instance hs)%I.
 
-Lemma HOcontrF
-     (*Need sth like this (HI: HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x))*):
-      HOcontractive F.
+Program Instance F_mono : BiMonoPred F.
+
+(*Local Instance F_contractive : Contractive F.
 Proof.
-unfold F.
-apply HOcontractive_i1.
-red; intros.
-apply allp_right; intro oi.
-apply subp_sepcon_mpred; [ | apply subp_refl].
-apply subp_exp; intro v.
-apply subp_sepcon_mpred; [ | apply subp_refl].
-clear oi.
-apply subp_andp; [ apply subp_refl | ].
-eapply derives_trans, subp_later1.
-rewrite <- later_allp.
-apply later_derives.
-unfold object_methods.
-apply subp_exp; intro sh.
-apply subp_exp; intro reset.
-apply subp_exp; intro twiddle.
-apply subp_exp; intro twiddleR.
-apply subp_sepcon_mpred; [ | apply subp_refl].
-repeat simple apply subp_sepcon_mpred;
-try (simple apply subp_andp; [simple apply subp_refl | ]).
-+
-unfold func_ptr'.
-apply subp_andp; [ | apply subp_refl].
-clear - instance.
-eapply derives_trans; [ | apply fash_func_ptr_ND].
-apply allp_right; intro oi.
-apply andp_right.
-*
-apply allp_right; intro rho.
-apply subp_i1.
-rewrite unfash_allp.
-set (zz := allp _).
-unfold convertPre.
-unfold PROPx, LOCALx, SEPx, local, lift1; simpl.
-unfold_lift.
-normalize.
-rewrite prop_true_andp by tauto.
-subst zz.
-eapply derives_trans.
-apply andp_derives; [ | apply derives_refl].
-apply allp_left with oi.
-apply unfash_fash.
-eapply derives_trans.
-apply andp_derives.
-apply andp_left2. apply derives_refl. apply derives_refl.
-rewrite andp_comm. apply modus_ponens.
-*
-apply allp_right; intro rho.
-apply subp_i1.
-rewrite unfash_allp.
-set (zz := allp _).
-unfold convertPre.
-unfold PROPx, LOCALx, SEPx, local, lift1; simpl.
-unfold_lift.
-normalize.
-subst zz.
-eapply derives_trans.
-apply andp_derives; [ | apply derives_refl].
-apply allp_left with ([], snd oi).
-apply unfash_fash.
-eapply derives_trans.
-apply andp_derives.
-apply andp_left1. apply derives_refl. apply derives_refl.
-rewrite andp_comm. apply modus_ponens.
-+
-unfold func_ptr'.
-apply subp_andp; [ | apply subp_refl].
-clear - instance.
-eapply derives_trans; [ | apply fash_func_ptr_ND].
-apply allp_right; intros [hs i].
-apply andp_right.
-*
-apply allp_right; intro rho.
-apply subp_i1.
-rewrite unfash_allp.
-set (zz := allp _).
-unfold convertPre.
-unfold PROPx, LOCALx, SEPx, local, lift1; simpl.
-unfold_lift.
-normalize.
-rewrite prop_true_andp by tauto.
-subst zz.
-eapply derives_trans.
-apply andp_derives; [ | apply derives_refl].
-apply allp_left with hs.
-apply unfash_fash.
-eapply derives_trans.
-apply andp_derives.
-apply andp_left2. apply derives_refl. apply derives_refl.
-rewrite andp_comm. apply modus_ponens.
-*
-apply allp_right; intro rho.
-apply subp_i1.
-rewrite unfash_allp.
-set (zz := allp _).
-unfold PROPx, LOCALx, SEPx, local, lift1; simpl.
-unfold_lift.
-normalize.
-subst zz.
-apply exp_right with x.
-normalize.
-rewrite prop_true_andp by tauto.
-eapply derives_trans.
-apply andp_derives; [ | apply derives_refl].
-apply allp_left with (i::fst hs, snd hs).
-apply unfash_fash.
-eapply derives_trans.
-apply andp_derives.
-apply andp_left1. apply derives_refl. apply derives_refl.
-rewrite andp_comm. apply modus_ponens.
-+
-unfold func_ptr'.
-apply subp_andp; [ | apply subp_refl].
-clear - instance.
-eapply derives_trans; [ | apply fash_func_ptr_ND].
-apply allp_right; intros [hs i].
-apply andp_right.
-*
-apply allp_right; intro rho.
-apply subp_i1.
-rewrite unfash_allp.
-set (zz := allp _).
-unfold convertPre.
-unfold PROPx, LOCALx, SEPx, local, lift1; simpl.
-unfold_lift.
-normalize.
-rewrite prop_true_andp by tauto.
-subst zz.
-eapply derives_trans.
-apply andp_derives; [ | apply derives_refl].
-apply allp_left with hs.
-apply unfash_fash.
-eapply derives_trans.
-apply andp_derives.
-apply andp_left2. apply derives_refl. apply derives_refl.
-rewrite andp_comm. apply modus_ponens.
-*
-apply allp_right; intro rho.
-apply subp_i1.
-rewrite unfash_allp.
-set (zz := allp _).
-unfold PROPx, LOCALx, SEPx, local, lift1; simpl.
-unfold_lift.
-normalize.
-subst zz.
-apply exp_right with x.
-normalize.
-rewrite prop_true_andp by tauto.
-eapply derives_trans.
-apply andp_derives; [ | apply derives_refl].
-apply allp_left with (i::fst hs, snd hs).
-apply unfash_fash.
-eapply derives_trans.
-apply andp_derives.
-apply andp_left1. apply derives_refl. apply derives_refl.
-rewrite andp_comm. apply modus_ponens.
-Qed.
+  rewrite /semax_ => n semax semax' Hsemax [??????].
+  do 8 f_equiv.
+  rewrite /believepred.
+  do 15 f_equiv.
+  rewrite /believe_internal_.
+  do 14 f_equiv.
+  by f_contractive.
+Qed.*)
 
-Definition obj_mpred:ObjInv -> mpred := (HORec F). (*ie same type as Andrew's object_mpred.*)
+Definition obj_mpred:ObjInv -> mpred := bi_least_fixpoint(A := leibnizO ObjInv) F.
 
 Lemma ObjMpred_fold_unfold: 
-HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x) ->
-obj_mpred = 
-fun hs => 
-  ((EX mtable: val,!!(isptr mtable) &&
-     (|> object_methods obj_mpred mtable) *
-     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
+(*HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x) ->*)
+forall hs, obj_mpred hs ⊣⊢
+  ((∃ mtable: val,⌜isptr mtable⌝ ∧
+     (▷ object_methods obj_mpred mtable) ∗
+     field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) ∗
+   instance hs).
 Proof.
   intros; unfold obj_mpred at 1.
+  rewrite least_fixpoint_unfold.
   rewrite HORec_fold_unfold; [ reflexivity | apply HOcontrF]; trivial.
 Qed.
 Lemma ObjMpred_fold_unfold' hs: 
 HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x) ->
 obj_mpred hs = 
-  ((EX mtable: val, !!(isptr mtable) &&
-     (|> object_methods obj_mpred mtable) *
+  ((∃ mtable: val, ⌜isptr mtable) ∧
+     (▷ object_methods obj_mpred mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
+   instance hs).
 Proof.
   intros. rewrite ObjMpred_fold_unfold, <- ObjMpred_fold_unfold; trivial. 
 Qed.
 
 Lemma ObjMpred_isptr
    (H: HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x))
-    hs: obj_mpred hs |-- !!(isptr (snd hs)).
+    hs: obj_mpred hs ⊢ ⌜isptr (snd hs)).
 Proof. rewrite ObjMpred_fold_unfold' by trivial; Intros m. entailer!. Qed.
 
 End ObjMpred.
 
 Definition object_mpred: object_invariant := fun hs =>
-  EX instance, !!(HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x)) &&
+  ∃ instance, ⌜HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x)) ∧
                obj_mpred instance hs.
 (*This now plays the role of Andrew's obj_mpred*)
 
-Lemma object_mpred_isptr hs: object_mpred hs |-- !!(isptr (snd hs)).
+Lemma object_mpred_isptr hs: object_mpred hs ⊢ ⌜isptr (snd hs)).
 Proof. unfold object_mpred; Intros inst. apply ObjMpred_isptr; trivial. Qed.
 
 Lemma obj_mpred_entails_object_mpred inst hs
   (H: HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => inst x)):
-  obj_mpred inst hs |-- object_mpred hs.
+  obj_mpred inst hs ⊢ object_mpred hs.
 Proof. unfold object_mpred. Exists inst. entailer!. Qed.
 
 (*Andrew's specs 
@@ -352,7 +156,7 @@ Definition make_foo_spec :=
     PROP () LOCAL (gvars gv) 
     SEP (mem_mgr gv; object_methods foo_invariant (gv _foo_methods))
  POST [ tobject ]
-    EX p: val, PROP () LOCAL (temp ret_temp p)
+    ∃ p: val, PROP () LOCAL (temp ret_temp p)
      SEP (mem_mgr gv; object_mpred (*nil p*)(nil, p); object_methods foo_invariant (gv _foo_methods)).
 
 *)
@@ -378,10 +182,10 @@ Definition foo_obj_invariant :object_invariant := obj_mpred foo_data.
 (*New lemma!*)
 Lemma foo_obj_invariant_fold_unfold: foo_obj_invariant =
  fun hs =>
-  ((EX mtable: val, !!(isptr mtable) &&
-     (|>object_methods foo_obj_invariant  mtable) *
+  ((∃ mtable: val, ⌜isptr mtable) ∧
+     (▷object_methods foo_obj_invariant  mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   foo_data hs)%logic.
+   foo_data hs).
 Proof.
   unfold foo_obj_invariant.
   rewrite <- ObjMpred_fold_unfold. trivial. apply foo_data_HOcontr.
@@ -389,13 +193,13 @@ Qed.
 
 (*Sometimes this variant is preferable, sometimes the one above*)
 Lemma foo_obj_invariant_fold_unfold' hs: foo_obj_invariant hs =
-  ((EX mtable: val, !!(isptr mtable) &&
-     (|>object_methods foo_obj_invariant  mtable) *
+  ((∃ mtable: val, ⌜isptr mtable) ∧
+     (▷object_methods foo_obj_invariant  mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   foo_data hs)%logic.
+   foo_data hs).
 Proof. rewrite foo_obj_invariant_fold_unfold. rewrite <- foo_obj_invariant_fold_unfold; trivial. Qed.
 
-Lemma foo_data_isptr hs: foo_data hs = !!(isptr (snd hs)) && foo_data hs.
+Lemma foo_data_isptr hs: foo_data hs = ⌜isptr (snd hs)) ∧ foo_data hs.
 apply pred_ext; entailer.
 unfold foo_data. entailer!. destruct (snd hs); simpl in *; trivial;  contradiction.
 Qed.
@@ -416,7 +220,7 @@ Definition make_foo_spec :=
     PROP () LOCAL (gvars gv) 
     SEP (mem_mgr gv; object_methods foo_obj_invariant (gv _foo_methods))
  POST [ tobject ]
-    EX p: val, PROP () LOCAL (temp ret_temp p)
+    ∃ p: val, PROP () LOCAL (temp ret_temp p)
      SEP (mem_mgr gv; object_mpred (nil,p); object_methods foo_obj_invariant (gv _foo_methods)).
 End NewSpecs.
 
@@ -425,7 +229,7 @@ Definition main_spec :=
   WITH gv: globals
   PRE  [] main_pre prog tt gv
   POST [ tint ]
-     EX i:Z, PROP(0<=i<=6) LOCAL (temp ret_temp (Vint (Int.repr i))) SEP(TT).
+     ∃ i:Z, PROP(0<=i<=6) LOCAL (temp ret_temp (Vint (Int.repr i))) SEP(TT).
 
 Definition Gprog : funspecs :=   ltac:(with_library prog [
     foo_reset_spec; foo_twiddle_spec; foo_twiddleR_spec; make_foo_spec; main_spec]).
@@ -434,11 +238,11 @@ Definition Gprog : funspecs :=   ltac:(with_library prog [
 Lemma object_mpred_i:
   forall (*(history: list Z) (self: val)*)(x:ObjInv) (instance: object_invariant) (mtable: val)
   ((*NEW*)CONTR: HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x)),
-  match x with (history, self) => !!(isptr mtable) &&
-     (|>object_methods instance mtable) *
+  match x with (history, self) => ⌜isptr mtable) ∧
+     (▷object_methods instance mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable self *
      instance (*history self*)x 
-    |-- object_mpred (*history self*)x
+    ⊢ object_mpred (*history self*)x
   end.
 Proof.
 (*intros. unfold object_mpred. Exists instance mtable; auto.*)
@@ -451,17 +255,17 @@ apply exp_derives; intros r.
 apply exp_derives; intros t.
 apply exp_derives; intros tR. entailer!.
 apply sepcon_derives. admit.
-apply func_ptr'_mono. clear - CONTR. do_funspec_sub.
+apply func_ptr_mono. clear - CONTR. do_funspec_sub.
  rewrite ObjMpred_fold_unfold by trivial.
 Exists w; destruct w; entailer!. unfold convertPre. Intros.
-Exists (EX mtable : val,
- !! isptr mtable && |> object_methods (obj_mpred instance) mtable *
+Exists (∃ mtable : val,
+ ⌜isptr mtable ∧ ▷ object_methods (obj_mpred instance) mtable *
  field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd o)).
 entailer!.
 intros. Exists mtable x0. entailer!. destruct w.
- Exists w (EX mtable : val,
-      !! isptr mtable &&
-      |> object_methods (obj_mpred instance) mtable *
+ Exists w (∃ mtable : val,
+      ⌜isptr mtable ∧
+      ▷ object_methods (obj_mpred instance) mtable *
       field_at Ews (Tstruct _object noattr) [
         StructField _mtable] mtable (snd hs)). entailer!.
   intros. destruct w as [hist i]. 
@@ -532,11 +336,11 @@ Qed.
 Lemma make_object_methods:
   forall sh instance reset twiddle twiddleR mtable,
   readable_share sh ->
-  func_ptr' (reset_spec instance) reset *
-  func_ptr' (twiddle_spec instance) twiddle *
-  func_ptr' (twiddle_spec instance) twiddleR * 
+  func_ptr (reset_spec instance) reset *
+  func_ptr (twiddle_spec instance) twiddle *
+  func_ptr (twiddle_spec instance) twiddleR * 
   data_at sh (Tstruct _methods noattr) (reset, (twiddle, twiddleR)) mtable
-  |-- object_methods instance mtable.
+  ⊢ object_methods instance mtable.
 Proof.
   intros.
   unfold object_methods.
@@ -547,11 +351,11 @@ Qed.
 Lemma make_object_methods_later:
   forall sh instance reset twiddle twiddleR mtable,
   readable_share sh ->
-  func_ptr' (reset_spec instance) reset *
-  func_ptr' (twiddle_spec instance) twiddle *
-  func_ptr' (twiddle_spec instance) twiddleR * 
+  func_ptr (reset_spec instance) reset *
+  func_ptr (twiddle_spec instance) twiddle *
+  func_ptr (twiddle_spec instance) twiddleR * 
   data_at sh (Tstruct _methods noattr) (reset, (twiddle, twiddleR)) mtable
-  |-- |> object_methods instance mtable.
+  ⊢ ▷ object_methods instance mtable.
 Proof.
 intros. eapply derives_trans. apply make_object_methods; trivial. apply now_later.
 Qed.
@@ -598,7 +402,7 @@ Qed.
 
 Lemma split_object_methods:
   forall instance m, 
-    object_methods instance m |-- object_methods instance m * object_methods instance m.
+    object_methods instance m ⊢ object_methods instance m * object_methods instance m.
 Proof.
 intros.
 unfold object_methods.
@@ -606,9 +410,9 @@ Intros sh reset twiddle twiddleR.
 
 Exists (fst (slice.cleave sh)) reset twiddle twiddleR.
 Exists (snd (slice.cleave sh)) reset twiddle twiddleR.
-rewrite (split_func_ptr' (reset_spec instance) reset) at 1.
-rewrite (split_func_ptr' (twiddle_spec instance) twiddle) at 1.
-rewrite (split_func_ptr' (twiddle_spec instance) twiddleR) at 1.
+rewrite (split_func_ptr (reset_spec instance) reset) at 1.
+rewrite (split_func_ptr (twiddle_spec instance) twiddle) at 1.
+rewrite (split_func_ptr (twiddle_spec instance) twiddleR) at 1.
 entailer!!.
 split.
 apply slice.cleave_readable1; auto.
@@ -827,7 +631,4 @@ forward.  (* return i; *)
 Exists i; entailer!!.
 Qed.
 
-
-
-
-
+end mpred.
\ No newline at end of file
diff --git a/progs/verif_objectSelfFancy.v b/progs/verif_objectSelfFancy.v
index 37547d2141..926da16faf 100644
--- a/progs/verif_objectSelfFancy.v
+++ b/progs/verif_objectSelfFancy.v
@@ -108,7 +108,7 @@ Definition F (X: ObjInv -> mpred) (hs: ObjInv): mpred :=
    ((EX mtable: val, !!(isptr mtable) (*This has to hold NOW, not ust LATER*)&&
      (|> object_methods X mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
+   instance hs).
 
 Definition HOcontractive1 {A: Type}{NA: NatDed A}{IA: Indir A}{RI: RecIndir A}{X: Type}
      (f: (X -> A) -> (X -> A)) := 
@@ -315,7 +315,7 @@ fun hs =>
   ((EX mtable: val,!!(isptr mtable) &&
      (|> object_methods obj_mpred mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
+   instance hs).
 Proof.
   intros; unfold obj_mpred at 1.
   rewrite HORec_fold_unfold; [ reflexivity | apply HOcontrF]; trivial.
@@ -326,7 +326,7 @@ obj_mpred hs =
   ((EX mtable: val, !!(isptr mtable) &&
      (|> object_methods obj_mpred mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
+   instance hs).
 Proof.
   intros. rewrite ObjMpred_fold_unfold, <- ObjMpred_fold_unfold; trivial. 
 Qed.
@@ -402,7 +402,7 @@ Lemma foo_obj_invariant_fold_unfold: foo_obj_invariant =
   ((EX mtable: val, !!(isptr mtable) &&
      (|>object_methods foo_obj_invariant  mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   foo_data hs)%logic.
+   foo_data hs).
 Proof.
   unfold foo_obj_invariant.
   rewrite <- ObjMpred_fold_unfold. trivial. apply foo_data_HOcontr.
@@ -413,7 +413,7 @@ Lemma foo_obj_invariant_fold_unfold' hs: foo_obj_invariant hs =
   ((EX mtable: val, !!(isptr mtable) &&
      (|>object_methods foo_obj_invariant  mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   foo_data hs)%logic.
+   foo_data hs).
 Proof. rewrite foo_obj_invariant_fold_unfold. rewrite <- foo_obj_invariant_fold_unfold; trivial. Qed.
 
 Lemma foo_data_isptr hs: foo_data hs = !!(isptr (snd hs)) && foo_data hs.
@@ -757,7 +757,7 @@ Definition G (X: fObjInv -> mpred) (hs: fObjInv): mpred :=
    ((EX mtable: val, !!(isptr mtable) (*This has to hold NOW, not ust LATER*)&&
      (|> fobject_methods X mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
+   instance hs).
 
 Lemma HOcontrG
      (*Need sth like this (HI: HOcontractive (fun (_ : ObjInv -> mpred) (x : ObjInv) => instance x))*):
@@ -1024,7 +1024,7 @@ fun hs =>
   ((EX mtable: val,!!(isptr mtable) &&
      (|> fobject_methods fobj_mpred mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
+   instance hs).
 Proof.
   intros; unfold fobj_mpred at 1.
   rewrite HORec_fold_unfold; [ reflexivity | apply HOcontrG]; trivial.
@@ -1035,7 +1035,7 @@ fobj_mpred hs =
   ((EX mtable: val, !!(isptr mtable) &&
      (|> fobject_methods fobj_mpred mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   instance hs)%logic.
+   instance hs).
 Proof.
   intros. rewrite fObjMpred_fold_unfold, <- fObjMpred_fold_unfold; trivial. 
 Qed.
@@ -1089,7 +1089,7 @@ Lemma fancyfoo_obj_invariant_fold_unfold: fancyfoo_obj_invariant =
   ((EX mtable: val, !!(isptr mtable) &&
      (|>fobject_methods fancyfoo_obj_invariant  mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   fancyfoo_data hs)%logic.
+   fancyfoo_data hs).
 Proof.
   unfold fancyfoo_obj_invariant.
   rewrite <- fObjMpred_fold_unfold. trivial. apply fancyfoo_data_HOcontr.
@@ -1100,7 +1100,7 @@ Lemma fancyfoo_obj_invariant_fold_unfold' hs: fancyfoo_obj_invariant hs =
   ((EX mtable: val, !!(isptr mtable) &&
      (|>fobject_methods fancyfoo_obj_invariant  mtable) *
      field_at Ews (Tstruct _object noattr) [StructField _mtable] mtable (snd hs)) *
-   fancyfoo_data hs)%logic.
+   fancyfoo_data hs).
 Proof. rewrite fancyfoo_obj_invariant_fold_unfold. rewrite <- fancyfoo_obj_invariant_fold_unfold; trivial. Qed.
 
 Lemma fancyfoo_data_isptr hs: fancyfoo_data hs = !!(isptr (snd hs)) && fancyfoo_data hs.
diff --git a/progs/verif_odd.v b/progs/verif_odd.v
index b4fa4c7c71..e592547a69 100644
--- a/progs/verif_odd.v
+++ b/progs/verif_odd.v
@@ -25,7 +25,7 @@ Qed.
 
 (* The Espec for odd is different from the Espec for even;
   the former has only "even" as an external function, and vice versa. *)
-Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog odd.prog) Gprog.
+Definition Espec := add_funspecs_rec unit (ext_link_prog odd.prog) (void_spec _) Gprog.
 #[export] Existing Instance Espec.
 
 (* Can't prove   prog_correct: semax_prog prog Vprog Gprog
diff --git a/progs/verif_queue.v b/progs/verif_queue.v
index cee60aa59b..16e2a89f66 100644
--- a/progs/verif_queue.v
+++ b/progs/verif_queue.v
@@ -15,7 +15,7 @@ Definition t_struct_fifo := Tstruct _fifo noattr.
 Proof. eapply mk_listspec; reflexivity. Defined.
 
 Lemma isnil: forall {T: Type} (s: list T), {s=nil}+{s<>nil}.
-Proof. intros. destruct s; [left|right]; auto. intro Hx; inv Hx. Qed.
+Proof. intros. destruct s; [left|right]; auto. Qed.
 
 Definition Qsh : share := fst (Share.split extern_retainer).
 Definition Qsh' := Share.lub (snd (Share.split extern_retainer)) Share.Rsh.
@@ -47,7 +47,6 @@ unfold Share.Lsh in *.
 destruct (Share.split Share.top) eqn:?H.
 simpl in *; subst.
 apply Share.split_nontrivial in H; auto.
-apply Share.nontrivial; auto.
 *
 apply leq_join_sub.
 apply Share.lub_upper2.
@@ -181,8 +180,8 @@ intros.
 f_equal.
 unfold field_at, list_cell.
 autorewrite with gather_prop.
-f_equal.
-apply ND_prop_ext.
+f_equiv.
+f_equiv.
 rewrite field_compatible_cons; simpl.
 rewrite field_compatible_cons; simpl.
 intuition.
@@ -562,8 +561,6 @@ forward_call (*  free(p, sizeof( *p)); *)
 forward. (* return i+j; *)
 Qed.
 
-#[export] Existing Instance NullExtension.Espec.
-
 Lemma prog_correct:
   semax_prog prog tt Vprog Gprog.
 Proof.
@@ -579,5 +576,3 @@ semax_func_cons body_fifo_get.
 semax_func_cons body_make_elem.
 semax_func_cons body_main.
 Qed.
-
-
diff --git a/progs/verif_queue2.v b/progs/verif_queue2.v
index 3b921be23c..164c243dea 100644
--- a/progs/verif_queue2.v
+++ b/progs/verif_queue2.v
@@ -14,21 +14,21 @@ Definition t_struct_fifo := Tstruct _fifo noattr.
 Proof. eapply mk_listspec; reflexivity. Defined.
 
 Lemma isnil: forall {T: Type} (s: list T), {s=nil}+{s<>nil}.
-Proof. intros. destruct s; [left|right]; auto. intro Hx; inv Hx. Qed.
+Proof. intros. destruct s; [left|right]; auto. Qed.
 
 Lemma field_at_list_cell:
   forall sh i v p,
   data_at sh t_struct_elem (i,v) p
-  = list_cell QS sh i p *
+  ⊣⊢ list_cell QS sh i p *
   field_at sh t_struct_elem [StructField _next] v p.
 Proof.
 intros.
 unfold_data_at (data_at _ _ _ _).
-f_equal.
+f_equiv.
 unfold field_at, list_cell.
 autorewrite with gather_prop.
-f_equal.
-apply ND_prop_ext.
+f_equiv; last done.
+f_equiv.
 rewrite field_compatible_cons; simpl.
 intuition.
 left; auto.
@@ -55,7 +55,7 @@ Definition fifo_body (contents: list val) (hd tl : val) :=
               !!(contents = prefix++last::nil)
             &&  (lseg QS Ews prefix hd tl
                    * malloc_token Ews t_struct_elem tl
-                   * data_at Ews t_struct_elem (last, nullval) tl)))%logic.
+                   * data_at Ews t_struct_elem (last, nullval) tl))).
 
 Definition fifo (contents: list val) (p: val) : mpred :=
   EX ht: (val*val), let (hd,tl) := ht in
@@ -346,8 +346,6 @@ assert_PROP (isptr p3); [entailer! | rewrite if_false by (intro; subst; contradi
 forward. (* return i; *)
 Qed.
 
-#[export] Existing Instance NullExtension.Espec.
-
 Lemma prog_correct:
   semax_prog prog tt Vprog Gprog.
 Proof.
@@ -363,4 +361,3 @@ Proof.
   semax_func_cons body_make_elem.
   semax_func_cons body_main.
 Qed.
-
diff --git a/progs/verif_reverse.v b/progs/verif_reverse.v
index 6d4a39c86a..b633b012bd 100644
--- a/progs/verif_reverse.v
+++ b/progs/verif_reverse.v
@@ -85,7 +85,7 @@ Definition main_spec :=
   WITH gv : globals
   PRE  [] main_pre prog tt gv
   POST [ tint ]
-     PROP() RETURN (Vint (Int.repr (3+2+1))) SEP(TT).
+     PROP() RETURN (Vint (Int.repr (3+2+1))) SEP(True).
 
 (** List all the function-specs, to form the global hypothesis *)
 Definition Gprog : funspecs :=   ltac:(with_library prog [
@@ -95,7 +95,7 @@ Definition Gprog : funspecs :=   ltac:(with_library prog [
 Lemma list_cell_eq: forall sh i p ,
    sepalg.nonidentity sh ->
    field_compatible t_struct_list [] p ->
-   list_cell LS sh (Vint i) p =
+   list_cell LS sh (Vint i) p ⊣⊢
    field_at sh t_struct_list (DOT _head) (Vint i) p.
 Proof.
   intros.
@@ -199,7 +199,7 @@ Exists (h::cts1,r,v,y).
 entailer!.  (* smt_test verif_reverse_example2 *)
  - rewrite <- app_assoc. auto.
  - rewrite (lseg_unroll _ sh (h::cts1)).
-    apply orp_right2.
+    rewrite <- bi.or_intro_r.
    unfold lseg_cons.
    apply andp_right.
    + apply prop_right.
@@ -220,8 +220,6 @@ Qed.
  ** to have a nicer proof theory for reasoning about this kind of thing.
  **)
 
-Import compcert.lib.Maps.
-
 Lemma setup_globals:
  forall Delta gv,
   PTree.get _three (glob_types Delta) = Some (tarray t_struct_list 3) ->
@@ -287,6 +285,7 @@ Qed.
 Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
 Proof.
 start_function.
+rename a into gv.
 change (Tstruct _ _) with t_struct_list.
 fold noattr. fold (tptr t_struct_list).
 eapply semax_pre; [
@@ -302,8 +301,6 @@ forward_call  (* s = sumlist(r); *)
 forward.  (* return s; *)
 Qed.
 
-#[export] Existing Instance NullExtension.Espec.
-
 Lemma prog_correct:
   semax_prog prog tt Vprog Gprog.
 Proof.
@@ -312,5 +309,3 @@ semax_func_cons body_sumlist.
 semax_func_cons body_reverse.
 semax_func_cons body_main.
 Qed.
-
-
diff --git a/progs/verif_stackframe_demo.v b/progs/verif_stackframe_demo.v
index 958476e0d3..188e299641 100644
--- a/progs/verif_stackframe_demo.v
+++ b/progs/verif_stackframe_demo.v
@@ -28,6 +28,7 @@ Qed.
 Lemma body_iden': semax_body Vprog Gprog f_iden iden_spec.
 Proof.
   start_function.
+  rename a into x.
   forward.
   forward.
   forward.
@@ -41,4 +42,3 @@ Proof.
   (* Should it fail? Yes. Because the lvar clause are used in stackframe cancel.
      The error message? We'd Better improve it.  --- Qinxiang 2019.11.8 *)
 Abort.
-
diff --git a/progs/verif_store_demo.v b/progs/verif_store_demo.v
index 9c34ab8d22..c2b9225501 100644
--- a/progs/verif_store_demo.v
+++ b/progs/verif_store_demo.v
@@ -77,7 +77,7 @@ forward.
 forward.
 simpl (temp _p _).
 (* Assert_PROP what forward asks us for (only for the root expression "p"):  *)
-assert_PROP (offset_val 8 (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
+assert_PROP (offset_val (64/8) (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
   = field_address (tarray pair_pair_t array_size) [StructField _right; ArraySubsc i] pps) as E. {
   entailer!. rewrite field_compatible_field_address by auto with field_compatible.
   simpl. reflexivity.
@@ -98,7 +98,7 @@ simpl (temp _p _).
 
 (* Assert_PROP what forward asks us for (for the full expression "p->snd"): *)
 assert_PROP (
-  offset_val 4 (offset_val 8 (force_val
+  offset_val (32/8) (offset_val (64/8) (force_val
     (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i)))))
   = (field_address (tarray pair_pair_t array_size)
                    [StructField _snd; StructField _right; ArraySubsc i] pps)). {
@@ -120,7 +120,7 @@ forward.
 simpl (temp _p _).
 
 (* Alternative: Make p nice enough so that no hint is required: *)
-assert_PROP (offset_val 8 (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
+assert_PROP (offset_val (64/8) (force_val (sem_add_ptr_int (Tstruct _pair_pair noattr) Signed pps (Vint (Int.repr i))))
   = field_address (tarray pair_pair_t array_size) [StructField _right; ArraySubsc i] pps) as E. {
   entailer!. rewrite field_compatible_field_address by auto with field_compatible.
   simpl. reflexivity.
diff --git a/progs/verif_sumarray2.v b/progs/verif_sumarray2.v
index dc179531b1..8c3df06f08 100644
--- a/progs/verif_sumarray2.v
+++ b/progs/verif_sumarray2.v
@@ -125,8 +125,6 @@ forward_call (*  s = sumarray(four+2,2); *)
   forward. (* return *)
 Qed.
 
-#[export] Existing Instance NullExtension.Espec.
-
 Lemma prog_correct:
   semax_prog prog tt Vprog Gprog.
 Proof.
diff --git a/progs/verif_switch.v b/progs/verif_switch.v
index f2752f21c4..5c753c888f 100644
--- a/progs/verif_switch.v
+++ b/progs/verif_switch.v
@@ -37,7 +37,8 @@ Definition Gprog : funspecs :=   ltac:(with_library prog [twice_spec]).
 Lemma body_twice: semax_body Vprog Gprog f_twice twice_spec.
 Proof.
 start_function.
-forward_if (PROP() LOCAL(temp _n (Vint (Int.repr (n+n)))) SEP()).
+rename a into n.
+forward_if (PROP() LOCAL(temp _n (Vint (Int.repr (n+n)))) SEP() : assert).
 repeat forward; entailer!!.
 repeat forward; entailer!!.
 repeat forward; entailer!!.
@@ -49,12 +50,10 @@ Qed.
 Lemma body_f: semax_body Vprog Gprog f_f f_spec.
 Proof.
 start_function.
-forward_if (False).
+forward_if (False : assert).
 forward.
 forward.
 forward.
 forward.
 forward.
 Qed.
-
-
diff --git a/progs/verif_tree.v b/progs/verif_tree.v
index 0bf54a8ca1..b14dee4749 100644
--- a/progs/verif_tree.v
+++ b/progs/verif_tree.v
@@ -100,12 +100,8 @@ Definition map_tree {V1 V2: Type} (f: V1 -> V2): tree V1 -> tree V2 :=
 
 Section IterTreeSepCon.
 
-  Context {A : Type}.
+  Context {A : bi}.
   Context {B : Type}.
-  Context {ND : NatDed A}.
-  Context {SL : SepLog A}.
-  Context {ClS: ClassicalSep A}.
-  Context {CoSL: CorableSepLog A}.
   Context (p : B -> A).
 
 Fixpoint iter_tree_sepcon (t1 : tree B) : A :=
@@ -118,12 +114,8 @@ End IterTreeSepCon.
 
 Section IterTreeSepCon2.
 
-  Context {A : Type}.
+  Context {A : bi}.
   Context {B1 B2 : Type}.
-  Context {ND : NatDed A}.
-  Context {SL : SepLog A}.
-  Context {ClS: ClassicalSep A}.
-  Context {CoSL: CorableSepLog A}.
   Context (p : B1 -> B2 -> A).
 
 Fixpoint iter_tree_sepcon2 (t1 : tree B1) : tree B2 -> A :=
@@ -131,17 +123,17 @@ Fixpoint iter_tree_sepcon2 (t1 : tree B1) : tree B2 -> A :=
     | E => fun t2 =>
        match t2 with
        | E => emp
-       | _ => FF
+       | _ => False
        end
     | T xa x xb => fun t2 =>
        match t2 with
-       | E => FF
+       | E => False
        | T ya y yb => p x y * iter_tree_sepcon2 xa ya * iter_tree_sepcon2 xb yb
        end
   end.
 
 Lemma iter_tree_sepcon2_spec: forall tl1 tl2,
-  iter_tree_sepcon2 tl1 tl2 =
+  iter_tree_sepcon2 tl1 tl2 ⊣⊢
   EX tl: tree (B1 * B2),
   !! (tl1 = map_tree fst tl /\ tl2 = map_tree snd tl) &&
   iter_tree_sepcon (uncurry p) tl.
@@ -151,29 +143,25 @@ Proof.
   + revert tl2; induction tl1; intros; destruct tl2.
     - apply (exp_right E); simpl.
       apply andp_right; auto.
-      apply prop_right; auto.
     - simpl.
-      apply FF_left.
+      apply False_left.
     - simpl.
-      apply FF_left.
+      apply False_left.
     - simpl.
       specialize (IHtl1_1 tl2_1).
       specialize (IHtl1_2 tl2_2).
       eapply derives_trans; [apply sepcon_derives; [apply sepcon_derives |]; [apply derives_refl | apply IHtl1_1 | apply IHtl1_2] | clear IHtl1_1 IHtl1_2].
       Intros tl_2 tl_1; subst.
-      rewrite sepcon_andp_prop. apply derives_extract_prop; intros [? ?].
-      rewrite sepcon_andp_prop, sepcon_andp_prop'.
-      apply derives_extract_prop; intros [? ?].
       Exists (T tl_1 (v, b) tl_2).
       simpl.
       apply andp_right; [apply prop_right; subst; auto |].
       apply derives_refl.
-  + apply exp_left; intros tl. Intros; subst.
+  + Intros tl. subst.
     induction tl.
     - simpl. auto.
     - simpl.
       eapply derives_trans; [apply sepcon_derives; [apply sepcon_derives |]; [apply derives_refl | apply IHtl1 | apply IHtl2] | clear IHtl1 IHtl2].
-      apply derives_refl.
+      destruct v; simpl; cancel.
 Qed.
 
 End IterTreeSepCon2.
@@ -888,8 +876,6 @@ Proof.
   forward.
 Qed.
 
-#[export] Existing Instance NullExtension.Espec.
-
 Lemma prog_correct:
   semax_prog prog tt Vprog Gprog.
 Proof.
@@ -901,5 +887,3 @@ semax_func_cons body_YTree_add.
 semax_func_cons body_Xfoo.
 semax_func_cons body_main.
 Qed.
-
-
diff --git a/progs/verif_union.v b/progs/verif_union.v
index 1ef2c5685a..a9f73b7347 100644
--- a/progs/verif_union.v
+++ b/progs/verif_union.v
@@ -106,7 +106,7 @@ revert k H; induction p; simpl; intros.
 rewrite Pos2Z.inj_succ in H.
 specialize (IHp (k-1)).
 spec IHp; [lia | ].
-replace (2^(k-1)) with (2^1 * 2^(k-1-1)).
+replace (2^(k-1)) with (2^1 * 2^(k-1-1))%Z.
 2:{ rewrite <- Z.pow_add_r by lia. f_equal. lia. }
 rewrite Pos2Z.inj_xI.
 lia.
@@ -114,12 +114,12 @@ lia.
 rewrite Pos2Z.inj_succ in H.
 specialize (IHp (k-1)).
 spec IHp; [lia | ].
-replace (2^(k-1)) with (2^1 * 2^(k-1-1)).
+replace (2^(k-1)) with (2^1 * 2^(k-1-1))%Z.
 2:{ rewrite <- Z.pow_add_r by lia. f_equal. lia. }
 rewrite Pos2Z.inj_xO.
 lia.
 -
-replace (2^(k-1)) with (2^1 * 2^(k-1-1)).
+replace (2^(k-1)) with (2^1 * 2^(k-1-1))%Z.
 2:{ rewrite <- Z.pow_add_r by lia. f_equal. lia. }
 change (2^1) with 2.
 assert (0 < 2 ^ (k-1-1)).
@@ -128,7 +128,7 @@ lia.
 Qed.
 
 
-Definition abs_nan (any_nan: {x : Bits.binary32 | Binary.is_nan 24 128 x = true}) (f: Binary.binary_float 24 128)   :=
+Definition abs_nan (any_nan: {x : Bits.binary32 | Binary.is_nan 24 128 x = true} ) (f: Binary.binary_float 24 128)   :=
 match f with
 | @Binary.B754_nan _ _ _ p H =>
     exist (fun x : Binary.binary_float 24 128 => Binary.is_nan 24 128 x = true)
@@ -162,7 +162,7 @@ Qed.
 
 Lemma binary32_abs_lemma:
  forall (x : Bits.binary32)
-      (any_nan : {x : Bits.binary32 | Binary.is_nan 24 128 x = true}),
+      (any_nan : {x : Bits.binary32 | Binary.is_nan 24 128 x = true} ),
   Bits.b32_of_bits (Bits.bits_of_b32 x mod 2 ^ 31) =
   Binary.Babs 24 128 (abs_nan any_nan) x.
 Proof.
@@ -292,7 +292,7 @@ End FABS_STUFF.
 
 Module Single.
 
-Definition fabs_single_spec :=
+Definition fabs_single_spec : ident * funspec :=
  DECLARE _fabs_single
  WITH x: float32
  PRE [ Tfloat F32 noattr]
@@ -321,7 +321,7 @@ Module Float.
    In fact, Vfloat x is wrong, leading to an unsatisfying precondition,
    it must be Vsingle. *)
 
-Definition fabs_single_spec :=
+Definition fabs_single_spec : ident * funspec :=
  DECLARE _fabs_single
  WITH x: float
  PRE [ Tfloat F32 noattr]
diff --git a/sha/spec_sha.v b/sha/spec_sha.v
index cec12ceb95..107b72e67f 100644
--- a/sha/spec_sha.v
+++ b/sha/spec_sha.v
@@ -150,11 +150,11 @@ Definition SHA256_Init_spec :=
 Definition SHA256_Update_spec :=
   DECLARE _SHA256_Update
    WITH a: s256abs, data: list byte, c : val, wsh: share, d: val, sh: share, len : Z, gv: globals
-   PRE [ _c OF tptr t_struct_SHA256state_st, _data_ OF tptr tvoid, _len OF tuint ]
+   PRE [ _c OF tptr t_struct_SHA256state_st, _data OF tptr tvoid, _len OF tuint ]
          PROP (writable_share wsh; readable_share sh; 
                    len <= Zlength data; 0 <= len <= Int.max_unsigned;
                    (s256a_len a + len * 8 < two_p 64)%Z)
-         LOCAL (temp _c c; temp _data_ d; temp _len (Vint (Int.repr len));
+         LOCAL (temp _c c; temp _data d; temp _len (Vint (Int.repr len));
                      gvars gv)
          SEP(K_vector gv;
                sha256state_ wsh a c; data_block sh data d)
@@ -209,7 +209,7 @@ Definition Gprog : funspecs :=
 Fixpoint do_builtins (n: nat) (defs : list (ident * globdef Clight.fundef type)) : funspecs :=
  match n, defs with
   | S n', (id, Gfun (External (EF_builtin _ sig) argtys resty cc_default))::defs' =>
-     (id, NDmk_funspec ((*iota_formals 1%positive*) typelist2list argtys, resty) cc_default unit FF FF)
+     (id, NDmk_funspec ((*iota_formals 1%positive*) typelist2list argtys, resty) cc_default unit (fun _ => FF) (fun _ => FF))
       :: do_builtins n' defs'
   | _, _ => nil
  end.