minor fixes in the lock spec and in the CG stack

theories/examples/stack/CG_stack.v

@@ -28,7 +28,9 @@ Definition CG_locked_pop : val := λ: "stt",
   release (Snd "stt");; "v".
 
 Definition CG_new_stack : val := λ: <>,
-  (ref NIL, newlock #())%E.
+  let: "st" := ref NIL in
+  let: "lk" := newlock #() in
+  ("st", "lk")%E.
 
 Definition CG_stack : val := Λ:
   (CG_new_stack, λ: "stt", CG_locked_pop "stt",
@@ -40,6 +42,11 @@ Fixpoint val_of_list (ls : list val) : val :=
   | v::vs => CONSV v (val_of_list vs)
   end.
 
+Instance val_to_list_inj : Inj (=@{list val}) (=@{val}) val_of_list.
+Proof.
+  intros ls1. induction ls1 as [|h1 ls1]=>ls2; destruct ls2; naive_solver.
+Qed.
+
 Definition is_stack `{!relocG Σ} (rs : val) (ls : list val) : iProp Σ :=
   ∃ (st : loc) l, ⌜rs = (#st, l)%V⌝ ∗ is_locked_r l false ∗ st ↦ₛ val_of_list ls.
 

theories/examples/stack/refinement.v

@@ -176,8 +176,8 @@ Section proof.
       iIntros (??) "_". repeat rel_pure_l. repeat rel_pure_r.
       rel_alloc_l istk as "Hisk".
       rel_alloc_l st as "Hst".
-      rel_apply_r refines_newlock_r. iIntros (l) "Hl".
-      rel_pure_r. rel_alloc_r st' as "Hst'". rel_pure_r.
+      rel_alloc_r st' as "Hst'". rel_pures_r.
+      rel_apply_r refines_newlock_r. iIntros (l) "Hl". rel_pures_r.
       rel_values.
       iMod (inv_alloc (stackN.@(st,(#st', l)%V)) _ (sinv A st (#st', l)%V) with "[-]")
         as "#Hinv".

theories/examples/various.v

@@ -293,7 +293,7 @@ Section proofs.
     iApply refines_arrow; auto.
     iIntros "!#" (f1 f2) "#Hf".
     rel_let_l. rel_let_r.
-    rel_apply_l (refines_acquire_l N _ l with "Hl").
+    rel_apply_l (refines_acquire_l N _ #l with "Hl").
     iNext. iIntros "Hlocked". iDestruct 1 as (n m) "[Hx Hy]".
     repeat rel_pure_l. rel_store_l. repeat rel_pure_l.
     iApply (refines_seq () with "[Hf]").
@@ -306,7 +306,7 @@ Section proofs.
       rel_values. }
     rel_load_l. repeat rel_pure_l.
     rel_load_r. repeat rel_pure_r.
-    rel_apply_l (refines_release_l N _ l γ with "Hl Hlocked [Hx Hy]"); eauto.
+    rel_apply_l (refines_release_l N _ #l γ with "Hl Hlocked [Hx Hy]"); eauto.
     { iExists _,_. iFrame. }
     iNext. repeat rel_pure_l.
     rel_values.

theories/experimental/helping/helping_stack.v

@@ -573,9 +573,8 @@ Section refinement.
     rel_values. iModIntro. iIntros (A). iModIntro.
     iIntros (? ?) "[-> ->]".
     rel_rec_r. rel_pures_r. rel_rec_r.
+    rel_alloc_r st' as "Hst'". rel_pures_r.
     rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
-    rel_pures_r.
-    rel_alloc_r st' as "Hst'".
     rel_pure_r. rel_pure_r.  rel_pure_r.  rel_pure_r.  rel_pure_r.
     rel_rec_l. rel_pures_l.
     rel_alloc_l mb as "Hmb". rel_pures_l.

theories/lib/lock.v

@@ -60,12 +60,12 @@ Section lockG_rules.
     iApply "Hlog". iExists l. eauto.
   Qed.
 
-  Lemma refines_release_l (R : iProp Σ) (lk : loc) γ K t A :
-    is_lock γ #lk R -∗
+  Lemma refines_release_l (R : iProp Σ) (lk : val) γ K t A :
+    is_lock γ lk R -∗
     locked γ -∗
     R -∗
     ▷(REL fill K (#() : expr) << t : A) -∗
-    REL fill K (release #lk) << t: A.
+    REL fill K (release lk) << t: A.
   Proof.
     iIntros "Hlock Hlocked HR Hlog".
     iDestruct "Hlock" as (l) "[% #?]"; simplify_eq.
@@ -78,10 +78,10 @@ Section lockG_rules.
     iApply "Hlog".
   Qed.
 
-  Lemma refines_acquire_l (R : iProp Σ) (lk : loc) γ K t A :
-    is_lock γ #lk R -∗
+  Lemma refines_acquire_l (R : iProp Σ) (lk : val) γ K t A :
+    is_lock γ lk R -∗
     ▷(locked γ -∗ R -∗ REL fill K (of_val #()) << t: A) -∗
-    REL fill K (acquire #lk) << t: A.
+    REL fill K (acquire lk) << t: A.
   Proof.
     iIntros "#Hlock Hlog".
     iLöb as "IH".