From a2afd43dc70daf98c8ee399ca69e80f5d84817b7 Mon Sep 17 00:00:00 2001
From: William Mansky <mansky1@uic.edu>
Date: Mon, 22 Apr 2024 15:57:45 -0500
Subject: [PATCH] fixes for atomics and ghost state; resolves #769, resolves
 #770

---
 atomics/SC_atomics.v        |  10 +-
 atomics/general_atomics.v   |  13 +-
 atomics/verif_lock.v        |   6 -
 atomics/verif_lock_atomic.v |   2 +-
 lib/proof/spec_SC_atomics.v |   4 +-
 lib/proof/verif_locks.v     |  13 +-
 lib/test/verif_incr.v       |  18 ++-
 lib/test/verif_incr_main.v  |   6 +-
 progs/incr.c                |  12 +-
 progs/incr.v                | 302 +++++++++++++++++++-----------------
 progs/verif_incr.v          |  37 ++++-
 progs/verif_incr_atomic.v   |  43 ++++-
 progs64/incr.c              |   6 +-
 progs64/incr.v              | 193 ++++++++++++-----------
 progs64/verif_incr.v        |  37 ++++-
 progs64/verif_incr_atomic.v |  41 ++++-
 16 files changed, 450 insertions(+), 293 deletions(-)

diff --git a/atomics/SC_atomics.v b/atomics/SC_atomics.v
index d34bd2cefc..9a61467159 100644
--- a/atomics/SC_atomics.v
+++ b/atomics/SC_atomics.v
@@ -15,10 +15,16 @@ Context `{!VSTGS OK_ty Σ}.
 
 Class atomic_int_impl (atomic_int : type) := { atomic_int_at : share -> val -> val -> mpred;
   atomic_int_at__ : forall sh v p, atomic_int_at sh v p ⊢ atomic_int_at sh Vundef p;
-  atomic_int_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_int_at sh v p ∗ atomic_int_at sh v' p ⊢ False }.
+  atomic_int_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_int_at sh v p ∗ atomic_int_at sh v' p ⊢ False;
+  atomic_int_isptr : forall sh v p, atomic_int_at sh v p ⊢ ⌜isptr p⌝;
+  atomic_int_timeless sh v p :: Timeless (atomic_int_at sh v p)
+ }.
 
 Class atomic_ptr_impl := { atomic_ptr : type; atomic_ptr_at : share -> val -> val -> mpred;
-  atomic_ptr_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_ptr_at sh v p ∗ atomic_ptr_at sh v' p ⊢ False }.
+  atomic_ptr_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_ptr_at sh v p ∗ atomic_ptr_at sh v' p ⊢ False;
+  atomic_ptr_isptr : forall sh v p, atomic_ptr_at sh v p ⊢ ⌜isptr p⌝;
+  atomic_ptr_timeless sh v p :: Timeless (atomic_ptr_at sh v p)
+ }.
 
 Context {CS : compspecs} `{AI : atomic_int_impl} {AP : atomic_ptr_impl}.
 
diff --git a/atomics/general_atomics.v b/atomics/general_atomics.v
index ee1e845601..1ad45fdc14 100644
--- a/atomics/general_atomics.v
+++ b/atomics/general_atomics.v
@@ -855,7 +855,7 @@ Ltac start_function1 ::=
               |- _ => idtac
             | s:=?spec':_ |- _ => check_canonical_funspec spec'
             end; change (semax_body V G F s); subst s)
-   end; unfold NDmk_funspec;
+   end;
    (let gv := fresh "gv" in
     match goal with
     | |- semax_body _ _ _ (_, mk_funspec _ _ _ _ ?Pre _) =>
@@ -871,8 +871,15 @@ Ltac start_function1 ::=
                                | (a, b) => _
                                end => intros Espec [a b]
            | λne i, _ => intros Espec i
-           end; simpl fn_body; simpl fn_params; simpl fn_return
-    end;
+           end
+    | |- semax_body _ _ _ (pair _ (NDmk_funspec _ _ _ ?Pre _)) =>
+          split3; [check_parameter_types' | check_return_type | ];
+           match Pre with
+           | (convertPre _ _ (fun i => _)) =>  intros Espec (*DependedTypeList*) i
+           | (fun x => match _ with (a,b) => _ end) => intros Espec (*DependedTypeList*) [a b]
+           | (fun i => _) => intros Espec (*DependedTypeList*) i (* this seems to be named "a" no matter what *)
+           end
+    end; simpl fn_body; simpl fn_params; simpl fn_return;
      cbv[dtfr dependent_type_functor_rec constOF idOF prodOF discrete_funOF ofe_morOF
         sigTOF listOF oFunctor_car ofe_car] in *; cbv[ofe_mor_car];
      rewrite_old_main_pre; rewrite ?argsassert_of_at ?assert_of_at;
diff --git a/atomics/verif_lock.v b/atomics/verif_lock.v
index 11fad8525d..740ac83e44 100644
--- a/atomics/verif_lock.v
+++ b/atomics/verif_lock.v
@@ -9,12 +9,6 @@ Section mpred.
 
 Context `{!VSTGS OK_ty Σ, !cinvG Σ, atom_impl : !atomic_int_impl (Tstruct _atom_int noattr)}.
 
-(* add these to atomic_int_impl? *)
-Axiom atomic_int_isptr : forall sh v p, atomic_int_at sh v p ⊢ ⌜isptr p⌝.
-#[local] Hint Resolve atomic_int_isptr : saturate_local.
-Axiom atomic_int_timeless : forall sh v p, Timeless (atomic_int_at sh v p).
-#[export] Existing Instance atomic_int_timeless.
-
 #[global] Opaque atomic_int_at.
 
 Section PROOFS.
diff --git a/atomics/verif_lock_atomic.v b/atomics/verif_lock_atomic.v
index c9005f63ae..8cfefa92ab 100644
--- a/atomics/verif_lock_atomic.v
+++ b/atomics/verif_lock_atomic.v
@@ -91,7 +91,7 @@ Section PROOFS.
   Proof.
     start_function.
     Intros v.
-    assert_PROP (is_pointer_or_null a) by entailer.
+    assert_PROP (is_pointer_or_null p) by entailer.
     forward_call.
     - Exists v. cancel.
     - entailer!.
diff --git a/lib/proof/spec_SC_atomics.v b/lib/proof/spec_SC_atomics.v
index f369239398..554b58ed5d 100644
--- a/lib/proof/spec_SC_atomics.v
+++ b/lib/proof/spec_SC_atomics.v
@@ -17,8 +17,8 @@ Notation vint z := (Vint (Int.repr z)).
    atomic_int_at__ : forall sh v p, atomic_int_at sh v p ⊢ atomic_int_at sh Vundef p;
    atomic_int_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_int_at sh v p ∗ atomic_int_at sh v' p ⊢ False%I;
    atomic_int_isptr : forall sh v p, atomic_int_at sh v p ⊢ ⌜isptr p⌝;
-   atomic_int_timeless : forall sh v p, Timeless (atomic_int_at sh v p);
-   atomic_ptr : type := Tstruct _atom_ptr noattr; 
+   atomic_int_timeless sh v p :: Timeless (atomic_int_at sh v p);
+   atomic_ptr : type := Tstruct _atom_ptr noattr;
    atomic_ptr_at : share -> val -> val -> mpred;
   atomic_ptr_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_ptr_at sh v p ∗ atomic_ptr_at sh v' p ⊢ False%I
 }.
diff --git a/lib/proof/verif_locks.v b/lib/proof/verif_locks.v
index 3e9d6e6e3c..a7d15bccfa 100755
--- a/lib/proof/verif_locks.v
+++ b/lib/proof/verif_locks.v
@@ -17,7 +17,7 @@ Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
 Section mpred.
 
-Context `{!VSTGS OK_ty Σ, !cinvG Σ, atom_impl : !atomic_int_impl (Tstruct _atom_int noattr)}.
+Context `{!VSTGS OK_ty Σ, !cinvG Σ(*, atom_impl : !atomic_int_impl (Tstruct _atom_int noattr)*)}.
 
 
 #[export] Program Instance M : lockAPD := {
@@ -98,8 +98,6 @@ Definition Gprog := lockImports ++ LockASI.
       { eapply semax_pre, semax_ff; go_lower; done. }
   Qed.
 
-Opaque inv_for_lock.
-
   Lemma body_release: semax_body Vprog Gprog f_release release_spec.
   Proof.
   (* the following line should not be necessary;
@@ -112,7 +110,6 @@ Opaque inv_for_lock.
     - destruct h as ((p, i), g); simpl; Intros.
       subst Frame; instantiate (1 := []); simpl; cancel.
       iIntros "(HR & #I & ? & P & HQ)".
- (* the next line fails for some reason 
       iInv i as "((% & >p & ?) & Hown)" "Hclose".
       destruct b.
       + iExists Ews; rewrite (bi.pure_True (writable_share _)) //.
@@ -127,7 +124,6 @@ Opaque inv_for_lock.
         rewrite bi.affinely_elim; iNext; iApply ("HR" with "[$]").
     - entailer!.
   Qed.
-*) Admitted.
 
   Lemma body_acquire: semax_body Vprog Gprog f_acquire acquire_spec.
   Proof.
@@ -151,7 +147,7 @@ Opaque inv_for_lock.
     - unfold lock_inv; destruct h as ((p, i), g); Intros.
       subst Frame; instantiate (1 := []); simpl fold_right_sepcon; cancel.
       iIntros "(#I & ?)".
- (* the next line fails for some reason 
+      rewrite {1}/inv_for_lock /=.
       iInv "I" as "((% & >? & ?) & ?)" "Hclose".
       iExists Ews, (Val.of_bool b); rewrite (bi.pure_True (writable_share _)) //.
       iFrame.
@@ -165,8 +161,9 @@ Opaque inv_for_lock.
     - Intros r. if_tac; forward_if; try discriminate; try contradiction.
       + forward. simpl lock_inv; entailer!.
       + forward. simpl lock_inv; entailer!.
-  Qed. *)
-  Admitted.
+  Qed.
+
+Opaque inv_for_lock.
 
 #[global] Opaque M.
 
diff --git a/lib/test/verif_incr.v b/lib/test/verif_incr.v
index 7d881e6288..c5bd48c4b3 100644
--- a/lib/test/verif_incr.v
+++ b/lib/test/verif_incr.v
@@ -3,7 +3,9 @@ Require Import VST.floyd.VSU.
 Require Import VST.concurrency.conclib.
 From VSTlib Require Import spec_locks spec_threads spec_malloc.
 Require VSTlib.verif_locks.
+Require Import iris_ora.algebra.ext_order.
 Require Import iris_ora.logic.cancelable_invariants.
+Require Import iris.algebra.lib.excl_auth.
 Require Import VSTlibtest.incr.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
@@ -12,11 +14,12 @@ Definition Vprog : varspecs. mk_varspecs prog. Defined.
 #[export] Existing Instance verif_locks.M.
 #[export] Existing Instance verif_malloc.M.
 
+Canonical Structure excl_authR A := inclR (excl_authR A).
 
 Section mpred.
-Context `{VSTGS1: !VSTGS unit Σ, 
-          cinvG1: !cinvG Σ, 
-          inG1: !inG Σ (excl_authR natO), 
+Context `{VSTGS1: !VSTGS unit Σ,
+          cinvG1: !cinvG Σ,
+          inG1: !inG Σ (excl_authR natO),
           aii1: !atomic_int_impl (Tstruct _atom_int noattr)}.
 
 Definition spawn_spec := DECLARE _spawn spawn_spec.
@@ -216,7 +219,6 @@ Proof.
   ghost_alloc (fun g => own g (●E O ⋅ ◯E O : excl_authR natO)).
   { apply excl_auth_valid. }
   Intro g2.
-  sep_apply (library.create_mem_mgr gv).
   forward_call (gv, fun _ : lock_handle => cptr_lock_inv g1 g2 ctr).
   Intros lock.
   forward.
@@ -253,11 +255,13 @@ Proof.
   { lock_props.
     rewrite -{2}Qp.half_half -frac_op -lock_inv_share_join.
     subst ctr; cancel. }
-  forward. 
+  forward.
   unfold_data_at (data_at_ _ _ _). simpl.
   cancel.
-  admit.
- Admitted.
+  unfold cptr_lock_inv; Intros z x y; cancel.
+  rewrite -(field_at_share_join _ _ Ews); [|eauto]; cancel.
+  by iIntros "(_ & _ & _ & _)".
+ Qed.
 
 (*
 
diff --git a/lib/test/verif_incr_main.v b/lib/test/verif_incr_main.v
index 62845331a6..466b35e79e 100644
--- a/lib/test/verif_incr_main.v
+++ b/lib/test/verif_incr_main.v
@@ -23,7 +23,7 @@ Definition AB_VSU :=
 Require VSTlib.verif_locks.
 Definition ABC_VSU:=
   ltac:(linkVSUs AB_VSU 
-         (verif_locks.LockVSU (atom_impl := aii1))).
+         (verif_locks.LockVSU)).
 
 Ltac SC_tac ::=
  match goal with |- SC_test ?ids _ _ =>
@@ -42,13 +42,13 @@ Ltac SC_tac ::=
           end.
 
 Definition core_VSU :=
-  ltac:(linkVSUs (IncrVSU (aii1:=aii1)) ABC_VSU).
+  ltac:(linkVSUs IncrVSU ABC_VSU).
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition main_QPprog := ltac:(QPprog prog).
 Definition whole_prog := ltac:(QPlink_progs main_QPprog (VSU_prog core_VSU)).
 Definition Vprog: varspecs := QPvarspecs whole_prog.
-Definition Main_imports := filter (matchImportExport main_QPprog) (VSU_Exports core_VSU). 
+Definition Main_imports := filter (matchImportExport main_QPprog) (VSU_Exports core_VSU).
 
 Definition main_spec :=
  DECLARE _main
diff --git a/progs/incr.c b/progs/incr.c
index 2b2dea2608..a68f4759ad 100644
--- a/progs/incr.c
+++ b/progs/incr.c
@@ -1,7 +1,7 @@
 #include "../concurrency/threads.h"
 //#include <stdio.h>
 
-typedef struct counter { unsigned ctr; lock_t *lock; } counter;
+typedef struct counter { unsigned ctr; lock_t lock; } counter;
 counter c;
 
 void incr() {
@@ -21,16 +21,16 @@ int thread_func(void *thread_lock) {
   //Increment the counter
   incr();
   //Yield: 'ready to join'.
-  release((lock_t *)thread_lock);
+  release((lock_t)thread_lock);
   return 0;
 }
 
-int main(void)
+int compute2(void)
 {
   c.ctr = 0;
   c.lock = makelock();
   release(c.lock);
-  lock_t *thread_lock = makelock();
+  lock_t thread_lock = makelock();
   /* Spawn */
   spawn((void *)&thread_func, (void *)thread_lock);
 
@@ -49,3 +49,7 @@ int main(void)
 
   return t;
 }
+
+int main(void) {
+ return compute2();
+}
diff --git a/progs/incr.v b/progs/incr.v
index 8f4d9f51c5..3a90e8e18a 100644
--- a/progs/incr.v
+++ b/progs/incr.v
@@ -6,19 +6,20 @@ Local Open Scope string_scope.
 Local Open Scope clight_scope.
 
 Module Info.
-  Definition version := "3.12".
+  Definition version := "3.13".
   Definition build_number := "".
   Definition build_tag := "".
   Definition build_branch := "".
   Definition arch := "x86".
-  Definition model := "32sse2".
+  Definition model := "64".
   Definition abi := "standard".
-  Definition bitsize := 32.
+  Definition bitsize := 64.
   Definition big_endian := false.
   Definition source_file := "progs/incr.c".
   Definition normalized := true.
 End Info.
 
+Definition ___builtin_ais_annot : ident := $"__builtin_ais_annot".
 Definition ___builtin_annot : ident := $"__builtin_annot".
 Definition ___builtin_annot_intval : ident := $"__builtin_annot_intval".
 Definition ___builtin_bswap : ident := $"__builtin_bswap".
@@ -77,6 +78,7 @@ Definition ___compcert_va_int64 : ident := $"__compcert_va_int64".
 Definition _acquire : ident := $"acquire".
 Definition _atom_int : ident := $"atom_int".
 Definition _c : ident := $"c".
+Definition _compute2 : ident := $"compute2".
 Definition _counter : ident := $"counter".
 Definition _ctr : ident := $"ctr".
 Definition _freelock : ident := $"freelock".
@@ -99,7 +101,7 @@ Definition _t'6 : ident := 133%positive.
 
 Definition v_c := {|
   gvar_info := (Tstruct _counter noattr);
-  gvar_init := (Init_space 8 :: nil);
+  gvar_init := (Init_space 16 :: nil);
   gvar_readonly := false;
   gvar_volatile := false
 |}.
@@ -109,20 +111,19 @@ Definition f_incr := {|
   fn_callconv := cc_default;
   fn_params := nil;
   fn_vars := nil;
-  fn_temps := ((_t'3, (tptr (tptr (Tstruct _atom_int noattr)))) ::
-               (_t'2, tuint) ::
-               (_t'1, (tptr (tptr (Tstruct _atom_int noattr)))) :: nil);
+  fn_temps := ((_t'3, (tptr (Tstruct _atom_int noattr))) :: (_t'2, tuint) ::
+               (_t'1, (tptr (Tstruct _atom_int noattr))) :: nil);
   fn_body :=
 (Ssequence
   (Ssequence
     (Sset _t'3
       (Efield (Evar _c (Tstruct _counter noattr)) _lock
-        (tptr (tptr (Tstruct _atom_int noattr)))))
+        (tptr (Tstruct _atom_int noattr))))
     (Scall None
       (Evar _acquire (Tfunction
                        (Tcons (tptr (Tstruct _atom_int noattr)) Tnil) tvoid
                        cc_default))
-      ((Etempvar _t'3 (tptr (tptr (Tstruct _atom_int noattr)))) :: nil)))
+      ((Etempvar _t'3 (tptr (Tstruct _atom_int noattr))) :: nil)))
   (Ssequence
     (Ssequence
       (Sset _t'2 (Efield (Evar _c (Tstruct _counter noattr)) _ctr tuint))
@@ -132,12 +133,12 @@ Definition f_incr := {|
     (Ssequence
       (Sset _t'1
         (Efield (Evar _c (Tstruct _counter noattr)) _lock
-          (tptr (tptr (Tstruct _atom_int noattr)))))
+          (tptr (Tstruct _atom_int noattr))))
       (Scall None
         (Evar _release (Tfunction
                          (Tcons (tptr (Tstruct _atom_int noattr)) Tnil) tvoid
                          cc_default))
-        ((Etempvar _t'1 (tptr (tptr (Tstruct _atom_int noattr)))) :: nil)))))
+        ((Etempvar _t'1 (tptr (Tstruct _atom_int noattr))) :: nil)))))
 |}.
 
 Definition f_read := {|
@@ -145,32 +146,31 @@ Definition f_read := {|
   fn_callconv := cc_default;
   fn_params := nil;
   fn_vars := nil;
-  fn_temps := ((_t, tuint) ::
-               (_t'2, (tptr (tptr (Tstruct _atom_int noattr)))) ::
-               (_t'1, (tptr (tptr (Tstruct _atom_int noattr)))) :: nil);
+  fn_temps := ((_t, tuint) :: (_t'2, (tptr (Tstruct _atom_int noattr))) ::
+               (_t'1, (tptr (Tstruct _atom_int noattr))) :: nil);
   fn_body :=
 (Ssequence
   (Ssequence
     (Sset _t'2
       (Efield (Evar _c (Tstruct _counter noattr)) _lock
-        (tptr (tptr (Tstruct _atom_int noattr)))))
+        (tptr (Tstruct _atom_int noattr))))
     (Scall None
       (Evar _acquire (Tfunction
                        (Tcons (tptr (Tstruct _atom_int noattr)) Tnil) tvoid
                        cc_default))
-      ((Etempvar _t'2 (tptr (tptr (Tstruct _atom_int noattr)))) :: nil)))
+      ((Etempvar _t'2 (tptr (Tstruct _atom_int noattr))) :: nil)))
   (Ssequence
     (Sset _t (Efield (Evar _c (Tstruct _counter noattr)) _ctr tuint))
     (Ssequence
       (Ssequence
         (Sset _t'1
           (Efield (Evar _c (Tstruct _counter noattr)) _lock
-            (tptr (tptr (Tstruct _atom_int noattr)))))
+            (tptr (Tstruct _atom_int noattr))))
         (Scall None
           (Evar _release (Tfunction
                            (Tcons (tptr (Tstruct _atom_int noattr)) Tnil)
                            tvoid cc_default))
-          ((Etempvar _t'1 (tptr (tptr (Tstruct _atom_int noattr)))) :: nil)))
+          ((Etempvar _t'1 (tptr (Tstruct _atom_int noattr))) :: nil)))
       (Sreturn (Some (Etempvar _t tuint))))))
 |}.
 
@@ -189,143 +189,153 @@ Definition f_thread_func := {|
                        (Tcons (tptr (Tstruct _atom_int noattr)) Tnil) tvoid
                        cc_default))
       ((Ecast (Etempvar _thread_lock (tptr tvoid))
-         (tptr (tptr (Tstruct _atom_int noattr)))) :: nil))
+         (tptr (Tstruct _atom_int noattr))) :: nil))
     (Sreturn (Some (Econst_int (Int.repr 0) tint)))))
 |}.
 
-Definition f_main := {|
+Definition f_compute2 := {|
   fn_return := tint;
   fn_callconv := cc_default;
   fn_params := nil;
   fn_vars := nil;
-  fn_temps := ((_thread_lock, (tptr (tptr (Tstruct _atom_int noattr)))) ::
+  fn_temps := ((_thread_lock, (tptr (Tstruct _atom_int noattr))) ::
                (_t, tuint) :: (_t'3, tuint) ::
                (_t'2, (tptr (Tstruct _atom_int noattr))) ::
                (_t'1, (tptr (Tstruct _atom_int noattr))) ::
-               (_t'6, (tptr (tptr (Tstruct _atom_int noattr)))) ::
-               (_t'5, (tptr (tptr (Tstruct _atom_int noattr)))) ::
-               (_t'4, (tptr (tptr (Tstruct _atom_int noattr)))) :: nil);
+               (_t'6, (tptr (Tstruct _atom_int noattr))) ::
+               (_t'5, (tptr (Tstruct _atom_int noattr))) ::
+               (_t'4, (tptr (Tstruct _atom_int noattr))) :: nil);
   fn_body :=
 (Ssequence
+  (Sassign (Efield (Evar _c (Tstruct _counter noattr)) _ctr tuint)
+    (Econst_int (Int.repr 0) tint))
   (Ssequence
-    (Sassign (Efield (Evar _c (Tstruct _counter noattr)) _ctr tuint)
-      (Econst_int (Int.repr 0) tint))
+    (Ssequence
+      (Scall (Some _t'1)
+        (Evar _makelock (Tfunction Tnil (tptr (Tstruct _atom_int noattr))
+                          cc_default)) nil)
+      (Sassign
+        (Efield (Evar _c (Tstruct _counter noattr)) _lock
+          (tptr (Tstruct _atom_int noattr)))
+        (Etempvar _t'1 (tptr (Tstruct _atom_int noattr)))))
     (Ssequence
       (Ssequence
-        (Scall (Some _t'1)
-          (Evar _makelock (Tfunction Tnil (tptr (Tstruct _atom_int noattr))
-                            cc_default)) nil)
-        (Sassign
+        (Sset _t'6
           (Efield (Evar _c (Tstruct _counter noattr)) _lock
-            (tptr (tptr (Tstruct _atom_int noattr))))
-          (Etempvar _t'1 (tptr (Tstruct _atom_int noattr)))))
+            (tptr (Tstruct _atom_int noattr))))
+        (Scall None
+          (Evar _release (Tfunction
+                           (Tcons (tptr (Tstruct _atom_int noattr)) Tnil)
+                           tvoid cc_default))
+          ((Etempvar _t'6 (tptr (Tstruct _atom_int noattr))) :: nil)))
       (Ssequence
         (Ssequence
-          (Sset _t'6
-            (Efield (Evar _c (Tstruct _counter noattr)) _lock
-              (tptr (tptr (Tstruct _atom_int noattr)))))
-          (Scall None
-            (Evar _release (Tfunction
-                             (Tcons (tptr (Tstruct _atom_int noattr)) Tnil)
-                             tvoid cc_default))
-            ((Etempvar _t'6 (tptr (tptr (Tstruct _atom_int noattr)))) :: nil)))
+          (Scall (Some _t'2)
+            (Evar _makelock (Tfunction Tnil (tptr (Tstruct _atom_int noattr))
+                              cc_default)) nil)
+          (Sset _thread_lock
+            (Etempvar _t'2 (tptr (Tstruct _atom_int noattr)))))
         (Ssequence
+          (Scall None
+            (Evar _spawn (Tfunction
+                           (Tcons
+                             (tptr (Tfunction (Tcons (tptr tvoid) Tnil) tint
+                                     cc_default)) (Tcons (tptr tvoid) Tnil))
+                           tvoid cc_default))
+            ((Ecast
+               (Eaddrof
+                 (Evar _thread_func (Tfunction (Tcons (tptr tvoid) Tnil) tint
+                                      cc_default))
+                 (tptr (Tfunction (Tcons (tptr tvoid) Tnil) tint cc_default)))
+               (tptr tvoid)) ::
+             (Ecast (Etempvar _thread_lock (tptr (Tstruct _atom_int noattr)))
+               (tptr tvoid)) :: nil))
           (Ssequence
-            (Scall (Some _t'2)
-              (Evar _makelock (Tfunction Tnil
-                                (tptr (Tstruct _atom_int noattr)) cc_default))
-              nil)
-            (Sset _thread_lock
-              (Etempvar _t'2 (tptr (Tstruct _atom_int noattr)))))
-          (Ssequence
-            (Scall None
-              (Evar _spawn (Tfunction
-                             (Tcons
-                               (tptr (Tfunction (Tcons (tptr tvoid) Tnil)
-                                       tint cc_default))
-                               (Tcons (tptr tvoid) Tnil)) tvoid cc_default))
-              ((Ecast
-                 (Eaddrof
-                   (Evar _thread_func (Tfunction (Tcons (tptr tvoid) Tnil)
-                                        tint cc_default))
-                   (tptr (Tfunction (Tcons (tptr tvoid) Tnil) tint
-                           cc_default))) (tptr tvoid)) ::
-               (Ecast
-                 (Etempvar _thread_lock (tptr (tptr (Tstruct _atom_int noattr))))
-                 (tptr tvoid)) :: nil))
+            (Scall None (Evar _incr (Tfunction Tnil tvoid cc_default)) nil)
             (Ssequence
-              (Scall None (Evar _incr (Tfunction Tnil tvoid cc_default)) nil)
+              (Scall None
+                (Evar _acquire (Tfunction
+                                 (Tcons (tptr (Tstruct _atom_int noattr))
+                                   Tnil) tvoid cc_default))
+                ((Etempvar _thread_lock (tptr (Tstruct _atom_int noattr))) ::
+                 nil))
               (Ssequence
-                (Scall None
-                  (Evar _acquire (Tfunction
-                                   (Tcons (tptr (Tstruct _atom_int noattr))
-                                     Tnil) tvoid cc_default))
-                  ((Etempvar _thread_lock (tptr (tptr (Tstruct _atom_int noattr)))) ::
-                   nil))
+                (Ssequence
+                  (Scall (Some _t'3)
+                    (Evar _read (Tfunction Tnil tuint cc_default)) nil)
+                  (Sset _t (Etempvar _t'3 tuint)))
                 (Ssequence
                   (Ssequence
-                    (Scall (Some _t'3)
-                      (Evar _read (Tfunction Tnil tuint cc_default)) nil)
-                    (Sset _t (Etempvar _t'3 tuint)))
+                    (Sset _t'5
+                      (Efield (Evar _c (Tstruct _counter noattr)) _lock
+                        (tptr (Tstruct _atom_int noattr))))
+                    (Scall None
+                      (Evar _acquire (Tfunction
+                                       (Tcons
+                                         (tptr (Tstruct _atom_int noattr))
+                                         Tnil) tvoid cc_default))
+                      ((Etempvar _t'5 (tptr (Tstruct _atom_int noattr))) ::
+                       nil)))
                   (Ssequence
+                    (Scall None
+                      (Evar _freelock (Tfunction
+                                        (Tcons
+                                          (tptr (Tstruct _atom_int noattr))
+                                          Tnil) tvoid cc_default))
+                      ((Etempvar _thread_lock (tptr (Tstruct _atom_int noattr))) ::
+                       nil))
                     (Ssequence
-                      (Sset _t'5
-                        (Efield (Evar _c (Tstruct _counter noattr)) _lock
-                          (tptr (tptr (Tstruct _atom_int noattr)))))
-                      (Scall None
-                        (Evar _acquire (Tfunction
-                                         (Tcons
-                                           (tptr (Tstruct _atom_int noattr))
-                                           Tnil) tvoid cc_default))
-                        ((Etempvar _t'5 (tptr (tptr (Tstruct _atom_int noattr)))) ::
-                         nil)))
-                    (Ssequence
-                      (Scall None
-                        (Evar _freelock (Tfunction
-                                          (Tcons
-                                            (tptr (Tstruct _atom_int noattr))
-                                            Tnil) tvoid cc_default))
-                        ((Etempvar _thread_lock (tptr (tptr (Tstruct _atom_int noattr)))) ::
-                         nil))
                       (Ssequence
-                        (Ssequence
-                          (Sset _t'4
-                            (Efield (Evar _c (Tstruct _counter noattr)) _lock
-                              (tptr (tptr (Tstruct _atom_int noattr)))))
-                          (Scall None
-                            (Evar _freelock (Tfunction
-                                              (Tcons
-                                                (tptr (Tstruct _atom_int noattr))
-                                                Tnil) tvoid cc_default))
-                            ((Etempvar _t'4 (tptr (tptr (Tstruct _atom_int noattr)))) ::
-                             nil)))
-                        (Sreturn (Some (Etempvar _t tuint))))))))))))))
+                        (Sset _t'4
+                          (Efield (Evar _c (Tstruct _counter noattr)) _lock
+                            (tptr (Tstruct _atom_int noattr))))
+                        (Scall None
+                          (Evar _freelock (Tfunction
+                                            (Tcons
+                                              (tptr (Tstruct _atom_int noattr))
+                                              Tnil) tvoid cc_default))
+                          ((Etempvar _t'4 (tptr (Tstruct _atom_int noattr))) ::
+                           nil)))
+                      (Sreturn (Some (Etempvar _t tuint))))))))))))))
+|}.
+
+Definition f_main := {|
+  fn_return := tint;
+  fn_callconv := cc_default;
+  fn_params := nil;
+  fn_vars := nil;
+  fn_temps := ((_t'1, tint) :: nil);
+  fn_body :=
+(Ssequence
+  (Ssequence
+    (Scall (Some _t'1) (Evar _compute2 (Tfunction Tnil tint cc_default)) nil)
+    (Sreturn (Some (Etempvar _t'1 tint))))
   (Sreturn (Some (Econst_int (Int.repr 0) tint))))
 |}.
 
 Definition composites : list composite_definition :=
 (Composite _counter Struct
    (Member_plain _ctr tuint ::
-    Member_plain _lock (tptr (tptr (Tstruct _atom_int noattr))) :: nil)
+    Member_plain _lock (tptr (Tstruct _atom_int noattr)) :: nil)
    noattr :: nil).
 
 Definition global_definitions : list (ident * globdef fundef type) :=
 ((___compcert_va_int32,
    Gfun(External (EF_runtime "__compcert_va_int32"
-                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
      (Tcons (tptr tvoid) Tnil) tuint cc_default)) ::
  (___compcert_va_int64,
    Gfun(External (EF_runtime "__compcert_va_int64"
-                   (mksignature (AST.Tint :: nil) AST.Tlong cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tlong cc_default))
      (Tcons (tptr tvoid) Tnil) tulong cc_default)) ::
  (___compcert_va_float64,
    Gfun(External (EF_runtime "__compcert_va_float64"
-                   (mksignature (AST.Tint :: nil) AST.Tfloat cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default))
      (Tcons (tptr tvoid) Tnil) tdouble cc_default)) ::
  (___compcert_va_composite,
    Gfun(External (EF_runtime "__compcert_va_composite"
-                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint
-                     cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons (tptr tvoid) (Tcons tulong Tnil))
      (tptr tvoid) cc_default)) ::
  (___compcert_i64_dtos,
    Gfun(External (EF_runtime "__compcert_i64_dtos"
@@ -396,6 +406,12 @@ Definition global_definitions : list (ident * globdef fundef type) :=
                    (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
                      cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
      cc_default)) ::
+ (___builtin_ais_annot,
+   Gfun(External (EF_builtin "__builtin_ais_annot"
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid
+                     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
+     (Tcons (tptr tschar) Tnil) tvoid
+     {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
  (___builtin_bswap64,
    Gfun(External (EF_builtin "__builtin_bswap64"
                    (mksignature (AST.Tlong :: nil) AST.Tlong cc_default))
@@ -418,8 +434,8 @@ Definition global_definitions : list (ident * globdef fundef type) :=
      (Tcons tuint Tnil) tint cc_default)) ::
  (___builtin_clzl,
    Gfun(External (EF_builtin "__builtin_clzl"
-                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
-     (Tcons tuint Tnil) tint cc_default)) ::
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons tulong Tnil) tint cc_default)) ::
  (___builtin_clzll,
    Gfun(External (EF_builtin "__builtin_clzll"
                    (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
@@ -430,8 +446,8 @@ Definition global_definitions : list (ident * globdef fundef type) :=
      (Tcons tuint Tnil) tint cc_default)) ::
  (___builtin_ctzl,
    Gfun(External (EF_builtin "__builtin_ctzl"
-                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
-     (Tcons tuint Tnil) tint cc_default)) ::
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
+     (Tcons tulong Tnil) tint cc_default)) ::
  (___builtin_ctzll,
    Gfun(External (EF_builtin "__builtin_ctzll"
                    (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
@@ -455,10 +471,10 @@ Definition global_definitions : list (ident * globdef fundef type) :=
  (___builtin_memcpy_aligned,
    Gfun(External (EF_builtin "__builtin_memcpy_aligned"
                    (mksignature
-                     (AST.Tint :: AST.Tint :: AST.Tint :: AST.Tint :: nil)
-                     AST.Tvoid cc_default))
+                     (AST.Tlong :: AST.Tlong :: AST.Tlong :: AST.Tlong ::
+                      nil) AST.Tvoid cc_default))
      (Tcons (tptr tvoid)
-       (Tcons (tptr tvoid) (Tcons tuint (Tcons tuint Tnil)))) tvoid
+       (Tcons (tptr tvoid) (Tcons tulong (Tcons tulong Tnil)))) tvoid
      cc_default)) ::
  (___builtin_sel,
    Gfun(External (EF_builtin "__builtin_sel"
@@ -468,13 +484,13 @@ Definition global_definitions : list (ident * globdef fundef type) :=
      {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
  (___builtin_annot,
    Gfun(External (EF_builtin "__builtin_annot"
-                   (mksignature (AST.Tint :: nil) AST.Tvoid
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid
                      {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|}))
      (Tcons (tptr tschar) Tnil) tvoid
      {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
  (___builtin_annot_intval,
    Gfun(External (EF_builtin "__builtin_annot_intval"
-                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tint
                      cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil))
      tint cc_default)) ::
  (___builtin_membar,
@@ -483,21 +499,21 @@ Definition global_definitions : list (ident * globdef fundef type) :=
      cc_default)) ::
  (___builtin_va_start,
    Gfun(External (EF_builtin "__builtin_va_start"
-                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
      (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
  (___builtin_va_arg,
    Gfun(External (EF_builtin "__builtin_va_arg"
-                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid
                      cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
      tvoid cc_default)) ::
  (___builtin_va_copy,
    Gfun(External (EF_builtin "__builtin_va_copy"
-                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tvoid
                      cc_default))
      (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) ::
  (___builtin_va_end,
    Gfun(External (EF_builtin "__builtin_va_end"
-                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
      (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
  (___builtin_unreachable,
    Gfun(External (EF_builtin "__builtin_unreachable"
@@ -505,8 +521,8 @@ Definition global_definitions : list (ident * globdef fundef type) :=
      cc_default)) ::
  (___builtin_expect,
    Gfun(External (EF_builtin "__builtin_expect"
-                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint
-                     cc_default)) (Tcons tint (Tcons tint Tnil)) tint
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
+                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
      cc_default)) ::
  (___builtin_fmax,
    Gfun(External (EF_builtin "__builtin_fmax"
@@ -548,21 +564,21 @@ Definition global_definitions : list (ident * globdef fundef type) :=
      cc_default)) ::
  (___builtin_read16_reversed,
    Gfun(External (EF_builtin "__builtin_read16_reversed"
-                   (mksignature (AST.Tint :: nil) AST.Tint16unsigned
+                   (mksignature (AST.Tlong :: nil) AST.Tint16unsigned
                      cc_default)) (Tcons (tptr tushort) Tnil) tushort
      cc_default)) ::
  (___builtin_read32_reversed,
    Gfun(External (EF_builtin "__builtin_read32_reversed"
-                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
      (Tcons (tptr tuint) Tnil) tuint cc_default)) ::
  (___builtin_write16_reversed,
    Gfun(External (EF_builtin "__builtin_write16_reversed"
-                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid
                      cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil))
      tvoid cc_default)) ::
  (___builtin_write32_reversed,
    Gfun(External (EF_builtin "__builtin_write32_reversed"
-                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid
                      cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil))
      tvoid cc_default)) ::
  (___builtin_debug,
@@ -573,33 +589,34 @@ Definition global_definitions : list (ident * globdef fundef type) :=
      {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) ::
  (_makelock,
    Gfun(External (EF_external "makelock"
-                   (mksignature nil AST.Tint cc_default)) Tnil
+                   (mksignature nil AST.Tlong cc_default)) Tnil
      (tptr (Tstruct _atom_int noattr)) cc_default)) ::
  (_freelock,
    Gfun(External (EF_external "freelock"
-                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
      (Tcons (tptr (Tstruct _atom_int noattr)) Tnil) tvoid cc_default)) ::
  (_acquire,
    Gfun(External (EF_external "acquire"
-                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
      (Tcons (tptr (Tstruct _atom_int noattr)) Tnil) tvoid cc_default)) ::
  (_release,
    Gfun(External (EF_external "release"
-                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
+                   (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default))
      (Tcons (tptr (Tstruct _atom_int noattr)) Tnil) tvoid cc_default)) ::
  (_spawn,
    Gfun(External (EF_external "spawn"
-                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
+                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tvoid
                      cc_default))
      (Tcons (tptr (Tfunction (Tcons (tptr tvoid) Tnil) tint cc_default))
        (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) :: (_c, Gvar v_c) ::
  (_incr, Gfun(Internal f_incr)) :: (_read, Gfun(Internal f_read)) ::
  (_thread_func, Gfun(Internal f_thread_func)) ::
- (_main, Gfun(Internal f_main)) :: nil).
+ (_compute2, Gfun(Internal f_compute2)) :: (_main, Gfun(Internal f_main)) ::
+ nil).
 
 Definition public_idents : list ident :=
-(_main :: _thread_func :: _read :: _incr :: _c :: _spawn :: _release ::
- _acquire :: _freelock :: _makelock :: ___builtin_debug ::
+(_main :: _compute2 :: _thread_func :: _read :: _incr :: _c :: _spawn ::
+ _release :: _acquire :: _freelock :: _makelock :: ___builtin_debug ::
  ___builtin_write32_reversed :: ___builtin_write16_reversed ::
  ___builtin_read32_reversed :: ___builtin_read16_reversed ::
  ___builtin_fnmsub :: ___builtin_fnmadd :: ___builtin_fmsub ::
@@ -612,13 +629,14 @@ Definition public_idents : list ident :=
  ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: ___builtin_clzll ::
  ___builtin_clzl :: ___builtin_clz :: ___builtin_bswap16 ::
  ___builtin_bswap32 :: ___builtin_bswap :: ___builtin_bswap64 ::
- ___compcert_i64_umulh :: ___compcert_i64_smulh :: ___compcert_i64_sar ::
- ___compcert_i64_shr :: ___compcert_i64_shl :: ___compcert_i64_umod ::
- ___compcert_i64_smod :: ___compcert_i64_udiv :: ___compcert_i64_sdiv ::
- ___compcert_i64_utof :: ___compcert_i64_stof :: ___compcert_i64_utod ::
- ___compcert_i64_stod :: ___compcert_i64_dtou :: ___compcert_i64_dtos ::
- ___compcert_va_composite :: ___compcert_va_float64 ::
- ___compcert_va_int64 :: ___compcert_va_int32 :: nil).
+ ___builtin_ais_annot :: ___compcert_i64_umulh :: ___compcert_i64_smulh ::
+ ___compcert_i64_sar :: ___compcert_i64_shr :: ___compcert_i64_shl ::
+ ___compcert_i64_umod :: ___compcert_i64_smod :: ___compcert_i64_udiv ::
+ ___compcert_i64_sdiv :: ___compcert_i64_utof :: ___compcert_i64_stof ::
+ ___compcert_i64_utod :: ___compcert_i64_stod :: ___compcert_i64_dtou ::
+ ___compcert_i64_dtos :: ___compcert_va_composite ::
+ ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 ::
+ nil).
 
 Definition prog : Clight.program := 
   mkprogram composites global_definitions public_idents _main Logic.I.
diff --git a/progs/verif_incr.v b/progs/verif_incr.v
index ceed6a693b..86f28bdcc5 100644
--- a/progs/verif_incr.v
+++ b/progs/verif_incr.v
@@ -2,11 +2,15 @@ Require Import VST.concurrency.conclib.
 Require Import VST.concurrency.lock_specs.
 Require Import VST.atomics.SC_atomics.
 Require Import VST.atomics.verif_lock.
+Require Import iris_ora.algebra.ext_order.
+Require Import iris.algebra.lib.excl_auth.
 Require Import VST.progs.incr.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
+Canonical Structure excl_authR A := inclR (excl_authR A).
+
 Section mpred.
 
 (* box up concurrentGS? *)
@@ -69,6 +73,16 @@ Definition thread_func_spec :=
          RETURN (Vint Int.zero)
          SEP ().
 
+Definition compute2_spec :=
+ DECLARE _compute2
+ WITH gv: globals
+ PRE [] PROP() PARAMS() GLOBALS(gv)
+          SEP(library.mem_mgr gv;
+                data_at Ews t_counter (Vint (Int.repr 0), Vundef) (gv _c);
+                has_ext tt)
+ POST [ tint ] PROP() RETURN (Vint (Int.repr 2)) 
+                    SEP(library.mem_mgr gv; data_at_ Ews t_counter (gv _c); has_ext tt).
+
 Definition main_spec :=
  DECLARE _main
   WITH gv : globals
@@ -76,7 +90,7 @@ Definition main_spec :=
   POST [ tint ] main_post prog gv.
 
 Definition Gprog : funspecs := ltac:(with_library prog [acquire_spec; release_spec; makelock_spec; freelock_spec;
-  spawn_spec; incr_spec; read_spec; thread_func_spec; main_spec]).
+  spawn_spec; incr_spec; read_spec; thread_func_spec; compute2_spec; main_spec]).
 
 Lemma ctr_inv_exclusive : forall g1 g2 p,
   exclusive_mpred (cptr_lock_inv g1 g2 p).
@@ -183,7 +197,7 @@ Proof.
   forward.
 Qed.
 
-Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
+Lemma body_compute2:  semax_body Vprog Gprog f_compute2 compute2_spec.
 Proof.
   start_function.
   set (ctr := gv _c).
@@ -194,7 +208,6 @@ Proof.
   ghost_alloc (fun g => own g (●E O ⋅ ◯E O : excl_authR natO)).
   { apply excl_auth_valid. }
   Intro g2.
-  sep_apply (library.create_mem_mgr gv).
   forward_call (gv, fun _ : lock_handle => cptr_lock_inv g1 g2 ctr).
   Intros lock.
   forward.
@@ -232,6 +245,23 @@ Proof.
     rewrite -{2}Qp.half_half -frac_op -lock_inv_share_join.
     subst ctr; cancel. }
   forward.
+  unfold_data_at (data_at_ _ _ _). simpl.
+  cancel.
+  unfold cptr_lock_inv; Intros z x y; cancel.
+  rewrite -(field_at_share_join _ _ Ews); [|eauto]; cancel.
+  by iIntros "(_ & _ & _ & _)".
+Qed.
+
+Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
+Proof.
+  start_function.
+  sep_apply (library.create_mem_mgr gv).
+  forward_call.
+  { rewrite zero_val_eq.
+    repeat change (fold_reptype ?a) with a.
+    repeat unfold_data_at (data_at _ _ _ _); simpl.
+    rewrite zero_val_eq; cancel. }
+  forward.
 Qed.
 
 Lemma prog_correct:
@@ -254,6 +284,7 @@ semax_func_cons_ext.
 semax_func_cons body_incr.
 semax_func_cons body_read.
 semax_func_cons body_thread_func.
+semax_func_cons body_compute2.
 semax_func_cons body_main.
 Qed.
 
diff --git a/progs/verif_incr_atomic.v b/progs/verif_incr_atomic.v
index 77ef7567f4..7f85f46400 100644
--- a/progs/verif_incr_atomic.v
+++ b/progs/verif_incr_atomic.v
@@ -1,10 +1,14 @@
 Require Import VST.concurrency.conclib.
 Require Import VST.atomics.verif_lock_atomic.
+Require Import iris_ora.algebra.ext_order.
+Require Import iris.algebra.lib.excl_auth.
 Require Import VST.progs.incr.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
+Canonical Structure excl_authR A := inclR (excl_authR A).
+
 Section mpred.
 
 (* box up concurrentGS? *)
@@ -69,6 +73,16 @@ Definition thread_func_spec :=
          RETURN (Vint Int.zero)
          SEP ().
 
+Definition compute2_spec :=
+ DECLARE _compute2
+ WITH gv: globals
+ PRE [] PROP() PARAMS() GLOBALS(gv)
+          SEP(library.mem_mgr gv;
+                data_at Ews t_counter (Vint (Int.repr 0), Vundef) (gv _c);
+                has_ext tt)
+ POST [ tint ] PROP() RETURN (Vint (Int.repr 2)) 
+                    SEP(library.mem_mgr gv; data_at_ Ews t_counter (gv _c); has_ext tt).
+
 Definition main_spec :=
  DECLARE _main
   WITH gv : globals
@@ -76,7 +90,7 @@ Definition main_spec :=
   POST [ tint ] main_post prog gv.
 
 Definition Gprog : funspecs :=   ltac:(with_library prog [acquire_spec; release_spec; makelock_spec;
-  freelock_spec; spawn_spec; incr_spec; read_spec; thread_func_spec; main_spec]).
+  freelock_spec; spawn_spec; incr_spec; read_spec; thread_func_spec; compute2_spec; main_spec]).
 
 Lemma ctr_inv_exclusive : forall gv g, exclusive_mpred (ctr_inv gv g).
 Proof.
@@ -199,12 +213,15 @@ Proof.
     iSplit; auto; iSplit; auto.
     unfold ctr_state; iFrame. }
   simpl. forward.
+  Exists n; entailer!!.
 Qed.
 
 #[local] Instance ctr_inv_timeless : forall gv g, Timeless (ctr_inv gv g).
 Proof.
   intros; unfold ctr_inv.
-  apply bi.exist_timeless; intros []; apply _.
+  apply bi.exist_timeless; intros.
+  apply bi.sep_timeless; try apply _.
+  apply bi.and_timeless; apply _.
 Qed.
 
 (* In this client, the ctr_state is assembled from the combination of the counter's lock assertion
@@ -267,7 +284,7 @@ Qed.
 
 Opaque Qp.div.
 
-Lemma body_main : semax_body Vprog Gprog f_main main_spec.
+Lemma body_compute2 : semax_body Vprog Gprog f_compute2 compute2_spec.
 Proof.
   start_function.
   forward.
@@ -280,8 +297,6 @@ Proof.
   ghost_alloc (fun g => own g (●E O ⋅ ◯E O : excl_authR natO)).
   { apply excl_auth_valid. }
   Intro g.
-  rename a into gv.
-  sep_apply (library.create_mem_mgr gv).
   (* We allocate the lock here, but give it an invariant later. *)
   forward_call (gv).
   Intros lockp.
@@ -363,6 +378,23 @@ Proof.
   { lock_props.
     rewrite -{3}Qp.half_half -frac_op -lock_inv_share_join; cancel. }
   forward.
+  unfold_data_at (data_at_ _ _ _). simpl.
+  cancel.
+  unfold ctr_inv; Intros n; cancel.
+  rewrite -(field_at_share_join _ _ Ews); [|eauto]; cancel.
+  by iIntros "(_ & _ & _)".
+Qed.
+
+Lemma body_main : semax_body Vprog Gprog f_main main_spec.
+Proof.
+  start_function.
+  sep_apply (library.create_mem_mgr gv).
+  forward_call.
+  { rewrite zero_val_eq.
+    repeat change (fold_reptype ?a) with a.
+    repeat unfold_data_at (data_at _ _ _ _); simpl.
+    rewrite zero_val_eq; cancel. }
+  forward.
 Qed.
 
 Lemma prog_correct:
@@ -382,6 +414,7 @@ semax_func_cons_ext.
 semax_func_cons body_incr.
 semax_func_cons body_read.
 semax_func_cons body_thread_func.
+semax_func_cons body_compute2.
 semax_func_cons body_main.
 Qed.
 
diff --git a/progs64/incr.c b/progs64/incr.c
index 752031d40e..a68f4759ad 100644
--- a/progs64/incr.c
+++ b/progs64/incr.c
@@ -25,7 +25,7 @@ int thread_func(void *thread_lock) {
   return 0;
 }
 
-int main(void)
+int compute2(void)
 {
   c.ctr = 0;
   c.lock = makelock();
@@ -49,3 +49,7 @@ int main(void)
 
   return t;
 }
+
+int main(void) {
+ return compute2();
+}
diff --git a/progs64/incr.v b/progs64/incr.v
index fcaf3852c2..c1f7727eaa 100644
--- a/progs64/incr.v
+++ b/progs64/incr.v
@@ -6,7 +6,7 @@ Local Open Scope string_scope.
 Local Open Scope clight_scope.
 
 Module Info.
-  Definition version := "3.14".
+  Definition version := "3.13".
   Definition build_number := "".
   Definition build_tag := "".
   Definition build_branch := "".
@@ -75,35 +75,21 @@ Definition ___compcert_va_composite : ident := $"__compcert_va_composite".
 Definition ___compcert_va_float64 : ident := $"__compcert_va_float64".
 Definition ___compcert_va_int32 : ident := $"__compcert_va_int32".
 Definition ___compcert_va_int64 : ident := $"__compcert_va_int64".
-Definition ___dummy : ident := $"__dummy".
-Definition ___pthread_t : ident := $"__pthread_t".
 Definition _acquire : ident := $"acquire".
-Definition _args : ident := $"args".
-Definition _atom_CAS : ident := $"atom_CAS".
 Definition _atom_int : ident := $"atom_int".
-Definition _atom_store : ident := $"atom_store".
-Definition _b : ident := $"b".
 Definition _c : ident := $"c".
+Definition _compute2 : ident := $"compute2".
 Definition _counter : ident := $"counter".
 Definition _ctr : ident := $"ctr".
-Definition _exit : ident := $"exit".
-Definition _exit_thread : ident := $"exit_thread".
-Definition _expected : ident := $"expected".
-Definition _f : ident := $"f".
-Definition _free_atomic : ident := $"free_atomic".
 Definition _freelock : ident := $"freelock".
 Definition _incr : ident := $"incr".
 Definition _lock : ident := $"lock".
 Definition _main : ident := $"main".
-Definition _make_atomic : ident := $"make_atomic".
 Definition _makelock : ident := $"makelock".
-Definition _r : ident := $"r".
 Definition _read : ident := $"read".
 Definition _release : ident := $"release".
 Definition _spawn : ident := $"spawn".
 Definition _t : ident := $"t".
-Definition _thrd_create : ident := $"thrd_create".
-Definition _thrd_exit : ident := $"thrd_exit".
 Definition _thread_func : ident := $"thread_func".
 Definition _thread_lock : ident := $"thread_lock".
 Definition _t'1 : ident := 128%positive.
@@ -207,7 +193,7 @@ Definition f_thread_func := {|
     (Sreturn (Some (Econst_int (Int.repr 0) tint)))))
 |}.
 
-Definition f_main := {|
+Definition f_compute2 := {|
   fn_return := tint;
   fn_callconv := cc_default;
   fn_params := nil;
@@ -221,99 +207,109 @@ Definition f_main := {|
                (_t'4, (tptr (Tstruct _atom_int noattr))) :: nil);
   fn_body :=
 (Ssequence
+  (Sassign (Efield (Evar _c (Tstruct _counter noattr)) _ctr tuint)
+    (Econst_int (Int.repr 0) tint))
   (Ssequence
-    (Sassign (Efield (Evar _c (Tstruct _counter noattr)) _ctr tuint)
-      (Econst_int (Int.repr 0) tint))
+    (Ssequence
+      (Scall (Some _t'1)
+        (Evar _makelock (Tfunction Tnil (tptr (Tstruct _atom_int noattr))
+                          cc_default)) nil)
+      (Sassign
+        (Efield (Evar _c (Tstruct _counter noattr)) _lock
+          (tptr (Tstruct _atom_int noattr)))
+        (Etempvar _t'1 (tptr (Tstruct _atom_int noattr)))))
     (Ssequence
       (Ssequence
-        (Scall (Some _t'1)
-          (Evar _makelock (Tfunction Tnil (tptr (Tstruct _atom_int noattr))
-                            cc_default)) nil)
-        (Sassign
+        (Sset _t'6
           (Efield (Evar _c (Tstruct _counter noattr)) _lock
-            (tptr (Tstruct _atom_int noattr)))
-          (Etempvar _t'1 (tptr (Tstruct _atom_int noattr)))))
+            (tptr (Tstruct _atom_int noattr))))
+        (Scall None
+          (Evar _release (Tfunction
+                           (Tcons (tptr (Tstruct _atom_int noattr)) Tnil)
+                           tvoid cc_default))
+          ((Etempvar _t'6 (tptr (Tstruct _atom_int noattr))) :: nil)))
       (Ssequence
         (Ssequence
-          (Sset _t'6
-            (Efield (Evar _c (Tstruct _counter noattr)) _lock
-              (tptr (Tstruct _atom_int noattr))))
-          (Scall None
-            (Evar _release (Tfunction
-                             (Tcons (tptr (Tstruct _atom_int noattr)) Tnil)
-                             tvoid cc_default))
-            ((Etempvar _t'6 (tptr (Tstruct _atom_int noattr))) :: nil)))
+          (Scall (Some _t'2)
+            (Evar _makelock (Tfunction Tnil (tptr (Tstruct _atom_int noattr))
+                              cc_default)) nil)
+          (Sset _thread_lock
+            (Etempvar _t'2 (tptr (Tstruct _atom_int noattr)))))
         (Ssequence
+          (Scall None
+            (Evar _spawn (Tfunction
+                           (Tcons
+                             (tptr (Tfunction (Tcons (tptr tvoid) Tnil) tint
+                                     cc_default)) (Tcons (tptr tvoid) Tnil))
+                           tvoid cc_default))
+            ((Ecast
+               (Eaddrof
+                 (Evar _thread_func (Tfunction (Tcons (tptr tvoid) Tnil) tint
+                                      cc_default))
+                 (tptr (Tfunction (Tcons (tptr tvoid) Tnil) tint cc_default)))
+               (tptr tvoid)) ::
+             (Ecast (Etempvar _thread_lock (tptr (Tstruct _atom_int noattr)))
+               (tptr tvoid)) :: nil))
           (Ssequence
-            (Scall (Some _t'2)
-              (Evar _makelock (Tfunction Tnil
-                                (tptr (Tstruct _atom_int noattr)) cc_default))
-              nil)
-            (Sset _thread_lock
-              (Etempvar _t'2 (tptr (Tstruct _atom_int noattr)))))
-          (Ssequence
-            (Scall None
-              (Evar _spawn (Tfunction
-                             (Tcons
-                               (tptr (Tfunction (Tcons (tptr tvoid) Tnil)
-                                       tint cc_default))
-                               (Tcons (tptr tvoid) Tnil)) tvoid cc_default))
-              ((Ecast
-                 (Eaddrof
-                   (Evar _thread_func (Tfunction (Tcons (tptr tvoid) Tnil)
-                                        tint cc_default))
-                   (tptr (Tfunction (Tcons (tptr tvoid) Tnil) tint
-                           cc_default))) (tptr tvoid)) ::
-               (Ecast
-                 (Etempvar _thread_lock (tptr (Tstruct _atom_int noattr)))
-                 (tptr tvoid)) :: nil))
+            (Scall None (Evar _incr (Tfunction Tnil tvoid cc_default)) nil)
             (Ssequence
-              (Scall None (Evar _incr (Tfunction Tnil tvoid cc_default)) nil)
+              (Scall None
+                (Evar _acquire (Tfunction
+                                 (Tcons (tptr (Tstruct _atom_int noattr))
+                                   Tnil) tvoid cc_default))
+                ((Etempvar _thread_lock (tptr (Tstruct _atom_int noattr))) ::
+                 nil))
               (Ssequence
-                (Scall None
-                  (Evar _acquire (Tfunction
-                                   (Tcons (tptr (Tstruct _atom_int noattr))
-                                     Tnil) tvoid cc_default))
-                  ((Etempvar _thread_lock (tptr (Tstruct _atom_int noattr))) ::
-                   nil))
+                (Ssequence
+                  (Scall (Some _t'3)
+                    (Evar _read (Tfunction Tnil tuint cc_default)) nil)
+                  (Sset _t (Etempvar _t'3 tuint)))
                 (Ssequence
                   (Ssequence
-                    (Scall (Some _t'3)
-                      (Evar _read (Tfunction Tnil tuint cc_default)) nil)
-                    (Sset _t (Etempvar _t'3 tuint)))
+                    (Sset _t'5
+                      (Efield (Evar _c (Tstruct _counter noattr)) _lock
+                        (tptr (Tstruct _atom_int noattr))))
+                    (Scall None
+                      (Evar _acquire (Tfunction
+                                       (Tcons
+                                         (tptr (Tstruct _atom_int noattr))
+                                         Tnil) tvoid cc_default))
+                      ((Etempvar _t'5 (tptr (Tstruct _atom_int noattr))) ::
+                       nil)))
                   (Ssequence
+                    (Scall None
+                      (Evar _freelock (Tfunction
+                                        (Tcons
+                                          (tptr (Tstruct _atom_int noattr))
+                                          Tnil) tvoid cc_default))
+                      ((Etempvar _thread_lock (tptr (Tstruct _atom_int noattr))) ::
+                       nil))
                     (Ssequence
-                      (Sset _t'5
-                        (Efield (Evar _c (Tstruct _counter noattr)) _lock
-                          (tptr (Tstruct _atom_int noattr))))
-                      (Scall None
-                        (Evar _acquire (Tfunction
-                                         (Tcons
-                                           (tptr (Tstruct _atom_int noattr))
-                                           Tnil) tvoid cc_default))
-                        ((Etempvar _t'5 (tptr (Tstruct _atom_int noattr))) ::
-                         nil)))
-                    (Ssequence
-                      (Scall None
-                        (Evar _freelock (Tfunction
-                                          (Tcons
-                                            (tptr (Tstruct _atom_int noattr))
-                                            Tnil) tvoid cc_default))
-                        ((Etempvar _thread_lock (tptr (Tstruct _atom_int noattr))) ::
-                         nil))
                       (Ssequence
-                        (Ssequence
-                          (Sset _t'4
-                            (Efield (Evar _c (Tstruct _counter noattr)) _lock
-                              (tptr (Tstruct _atom_int noattr))))
-                          (Scall None
-                            (Evar _freelock (Tfunction
-                                              (Tcons
-                                                (tptr (Tstruct _atom_int noattr))
-                                                Tnil) tvoid cc_default))
-                            ((Etempvar _t'4 (tptr (Tstruct _atom_int noattr))) ::
-                             nil)))
-                        (Sreturn (Some (Etempvar _t tuint))))))))))))))
+                        (Sset _t'4
+                          (Efield (Evar _c (Tstruct _counter noattr)) _lock
+                            (tptr (Tstruct _atom_int noattr))))
+                        (Scall None
+                          (Evar _freelock (Tfunction
+                                            (Tcons
+                                              (tptr (Tstruct _atom_int noattr))
+                                              Tnil) tvoid cc_default))
+                          ((Etempvar _t'4 (tptr (Tstruct _atom_int noattr))) ::
+                           nil)))
+                      (Sreturn (Some (Etempvar _t tuint))))))))))))))
+|}.
+
+Definition f_main := {|
+  fn_return := tint;
+  fn_callconv := cc_default;
+  fn_params := nil;
+  fn_vars := nil;
+  fn_temps := ((_t'1, tint) :: nil);
+  fn_body :=
+(Ssequence
+  (Ssequence
+    (Scall (Some _t'1) (Evar _compute2 (Tfunction Tnil tint cc_default)) nil)
+    (Sreturn (Some (Etempvar _t'1 tint))))
   (Sreturn (Some (Econst_int (Int.repr 0) tint))))
 |}.
 
@@ -615,11 +611,12 @@ Definition global_definitions : list (ident * globdef fundef type) :=
        (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) :: (_c, Gvar v_c) ::
  (_incr, Gfun(Internal f_incr)) :: (_read, Gfun(Internal f_read)) ::
  (_thread_func, Gfun(Internal f_thread_func)) ::
- (_main, Gfun(Internal f_main)) :: nil).
+ (_compute2, Gfun(Internal f_compute2)) :: (_main, Gfun(Internal f_main)) ::
+ nil).
 
 Definition public_idents : list ident :=
-(_main :: _thread_func :: _read :: _incr :: _c :: _spawn :: _release ::
- _acquire :: _freelock :: _makelock :: ___builtin_debug ::
+(_main :: _compute2 :: _thread_func :: _read :: _incr :: _c :: _spawn ::
+ _release :: _acquire :: _freelock :: _makelock :: ___builtin_debug ::
  ___builtin_write32_reversed :: ___builtin_write16_reversed ::
  ___builtin_read32_reversed :: ___builtin_read16_reversed ::
  ___builtin_fnmsub :: ___builtin_fnmadd :: ___builtin_fmsub ::
diff --git a/progs64/verif_incr.v b/progs64/verif_incr.v
index 5bc35205d7..6b1a5d1e6a 100644
--- a/progs64/verif_incr.v
+++ b/progs64/verif_incr.v
@@ -3,11 +3,15 @@ Require Import VST.concurrency.conclib.
 Require Import VST.concurrency.lock_specs.
 Require Import VST.atomics.SC_atomics.
 Require Import VST.atomics.verif_lock.
+Require Import iris_ora.algebra.ext_order.
+Require Import iris.algebra.lib.excl_auth.
 Require Import VST.progs64.incr.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
+Canonical Structure excl_authR A := inclR (excl_authR A).
+
 Section mpred.
 
 (* box up concurrentGS? *)
@@ -70,6 +74,16 @@ Definition thread_func_spec :=
          RETURN (Vint Int.zero)
          SEP ().
 
+Definition compute2_spec :=
+ DECLARE _compute2
+ WITH gv: globals
+ PRE [] PROP() PARAMS() GLOBALS(gv)
+          SEP(library.mem_mgr gv;
+                data_at Ews t_counter (Vint (Int.repr 0), Vundef) (gv _c);
+                has_ext tt)
+ POST [ tint ] PROP() RETURN (Vint (Int.repr 2)) 
+                    SEP(library.mem_mgr gv; data_at_ Ews t_counter (gv _c); has_ext tt).
+
 Definition main_spec :=
  DECLARE _main
   WITH gv : globals
@@ -77,7 +91,7 @@ Definition main_spec :=
   POST [ tint ] main_post prog gv.
 
 Definition Gprog : funspecs := ltac:(with_library prog [acquire_spec; release_spec; makelock_spec; freelock_spec;
-  spawn_spec; incr_spec; read_spec; thread_func_spec; main_spec]).
+  spawn_spec; incr_spec; read_spec; thread_func_spec; compute2_spec; main_spec]).
 
 Lemma ctr_inv_exclusive : forall g1 g2 p,
   exclusive_mpred (cptr_lock_inv g1 g2 p).
@@ -184,7 +198,7 @@ Proof.
   forward.
 Qed.
 
-Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
+Lemma body_compute2:  semax_body Vprog Gprog f_compute2 compute2_spec.
 Proof.
   start_function.
   set (ctr := gv _c).
@@ -195,7 +209,6 @@ Proof.
   ghost_alloc (fun g => own g (●E O ⋅ ◯E O : excl_authR natO)).
   { apply excl_auth_valid. }
   Intro g2.
-  sep_apply (library.create_mem_mgr gv).
   forward_call (gv, fun _ : lock_handle => cptr_lock_inv g1 g2 ctr).
   Intros lock.
   forward.
@@ -233,6 +246,23 @@ Proof.
     rewrite -{2}Qp.half_half -frac_op -lock_inv_share_join.
     subst ctr; cancel. }
   forward.
+  unfold_data_at (data_at_ _ _ _). simpl.
+  cancel.
+  unfold cptr_lock_inv; Intros z x y; cancel.
+  rewrite -(field_at_share_join _ _ Ews); [|eauto]; cancel.
+  by iIntros "(_ & _ & _ & _)".
+Qed.
+
+Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
+Proof.
+  start_function.
+  sep_apply (library.create_mem_mgr gv).
+  forward_call.
+  { rewrite zero_val_eq.
+    repeat change (fold_reptype ?a) with a.
+    repeat unfold_data_at (data_at _ _ _ _); simpl.
+    rewrite zero_val_eq; cancel. }
+  forward.
 Qed.
 
 Lemma prog_correct:
@@ -255,6 +285,7 @@ semax_func_cons_ext.
 semax_func_cons body_incr.
 semax_func_cons body_read.
 semax_func_cons body_thread_func.
+semax_func_cons body_compute2.
 semax_func_cons body_main.
 Qed.
 
diff --git a/progs64/verif_incr_atomic.v b/progs64/verif_incr_atomic.v
index fd8d4ec4ca..4e6a48db2a 100644
--- a/progs64/verif_incr_atomic.v
+++ b/progs64/verif_incr_atomic.v
@@ -1,10 +1,14 @@
 Require Import VST.concurrency.conclib.
 Require Import VST.atomics.verif_lock_atomic.
+Require Import iris_ora.algebra.ext_order.
+Require Import iris.algebra.lib.excl_auth.
 Require Import VST.progs64.incr.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
+Canonical Structure excl_authR A := inclR (excl_authR A).
+
 Section mpred.
 
 (* box up concurrentGS? *)
@@ -69,6 +73,16 @@ Definition thread_func_spec :=
          RETURN (Vint Int.zero)
          SEP ().
 
+Definition compute2_spec :=
+ DECLARE _compute2
+ WITH gv: globals
+ PRE [] PROP() PARAMS() GLOBALS(gv)
+          SEP(library.mem_mgr gv;
+                data_at Ews t_counter (Vint (Int.repr 0), Vundef) (gv _c);
+                has_ext tt)
+ POST [ tint ] PROP() RETURN (Vint (Int.repr 2)) 
+                    SEP(library.mem_mgr gv; data_at_ Ews t_counter (gv _c); has_ext tt).
+
 Definition main_spec :=
  DECLARE _main
   WITH gv : globals
@@ -76,7 +90,7 @@ Definition main_spec :=
   POST [ tint ] main_post prog gv.
 
 Definition Gprog : funspecs :=   ltac:(with_library prog [acquire_spec; release_spec; makelock_spec;
-  freelock_spec; spawn_spec; incr_spec; read_spec; thread_func_spec; main_spec]).
+  freelock_spec; spawn_spec; incr_spec; read_spec; thread_func_spec; compute2_spec; main_spec]).
 
 Lemma ctr_inv_exclusive : forall gv g, exclusive_mpred (ctr_inv gv g).
 Proof.
@@ -207,7 +221,8 @@ Proof.
   intros; unfold ctr_inv.
   apply bi.exist_timeless; intros.
   apply bi.sep_timeless; try apply _.
-Admitted.
+  apply bi.and_timeless; apply _.
+Qed.
 
 (* In this client, the ctr_state is assembled from the combination of the counter's lock assertion
    and a global invariant for the ghost state. In theory we could put it all in a global invariant,
@@ -269,7 +284,7 @@ Qed.
 
 Opaque Qp.div.
 
-Lemma body_main : semax_body Vprog Gprog f_main main_spec.
+Lemma body_compute2 : semax_body Vprog Gprog f_compute2 compute2_spec.
 Proof.
   start_function.
   forward.
@@ -282,8 +297,6 @@ Proof.
   ghost_alloc (fun g => own g (●E O ⋅ ◯E O : excl_authR natO)).
   { apply excl_auth_valid. }
   Intro g.
-  rename a into gv.
-  sep_apply (library.create_mem_mgr gv).
   (* We allocate the lock here, but give it an invariant later. *)
   forward_call (gv).
   Intros lockp.
@@ -365,6 +378,23 @@ Proof.
   { lock_props.
     rewrite -{3}Qp.half_half -frac_op -lock_inv_share_join; cancel. }
   forward.
+  unfold_data_at (data_at_ _ _ _). simpl.
+  cancel.
+  unfold ctr_inv; Intros n; cancel.
+  rewrite -(field_at_share_join _ _ Ews); [|eauto]; cancel.
+  by iIntros "(_ & _ & _)".
+Qed.
+
+Lemma body_main : semax_body Vprog Gprog f_main main_spec.
+Proof.
+  start_function.
+  sep_apply (library.create_mem_mgr gv).
+  forward_call.
+  { rewrite zero_val_eq.
+    repeat change (fold_reptype ?a) with a.
+    repeat unfold_data_at (data_at _ _ _ _); simpl.
+    rewrite zero_val_eq; cancel. }
+  forward.
 Qed.
 
 Lemma prog_correct:
@@ -384,6 +414,7 @@ semax_func_cons_ext.
 semax_func_cons body_incr.
 semax_func_cons body_read.
 semax_func_cons body_thread_func.
+semax_func_cons body_compute2.
 semax_func_cons body_main.
 Qed.