Clean up the bit example

theories/examples/bit.v

 From iris.proofmode Require Import tactics.
-From iris_logrel Require Import logrel.
+From iris_logrel Require Import logrel examples.lock.
 
 Definition bitτ : type :=
-  (TExists (TProd (TProd (TArrow (TVar 0) (TBool))
+  (TExists (TProd (TProd (TVar 0)
                          (TArrow (TVar 0) (TVar 0)))
-                         (TVar 0))).
+                         (TArrow (TVar 0) (TBool)))).
 Hint Unfold bitτ : typeable.
 
 Definition bit_bool : val :=
-  PackV ((λ: "b", "b"), (λ: "b", "b" ⊕ #true), #true).
+  PackV (#true, (λ: "b", "b" ⊕ #true), (λ: "b", "b")).
 
 Definition flip_nat : val := λ: "n",
   if: "n" = #0
   then #1
   else #0.
 Definition bit_nat : val :=
-  PackV ((λ: "b", "b" = #0), flip_nat, #0).
+  PackV (#1, flip_nat, (λ: "b", "b" = #1)).
 
 (** * Typeability *)
 (** ** Boolean bit *)
@@ -47,8 +47,8 @@ Section bit_refinement.
 
   Definition bitf (b : bool) : nat :=
     match b with
-    | true => 0
-    | false => 1
+    | true => 1
+    | false => 0
     end.
   
   (* This is the graph of the `bitf` function *)
@@ -65,14 +65,7 @@ Section bit_refinement.
     simpl.
     iApply (bin_log_related_pack _ bitτi).
     repeat iApply bin_log_related_pair.
-    - iApply bin_log_related_arrow_val; try by unlock.
-      iAlways. iIntros (v1 v2) "/= Hi".
-      iDestruct "Hi" as (b) "[% %]"; simplify_eq.
-      unlock.
-      rel_rec_l.
-      rel_rec_r.
-      rel_op_r.
-      rel_vals; destruct b; simpl; eauto.
+    - rel_vals; simpl; eauto.
     - unfold flip_nat.
       iApply bin_log_related_arrow_val; try by unlock.
       iAlways. iIntros (v1 v2) "/= #Hi".
@@ -82,10 +75,15 @@ Section bit_refinement.
       rel_rec_r.
       rel_op_l; simpl.
       rel_op_r; simpl.
-      destruct b; simpl.
-      + rel_if_true_r. rel_vals; simpl; eauto.
-      + rel_if_false_r. rel_vals; simpl; eauto.
-    - rel_vals; simpl; eauto.
+      destruct b; simpl; rel_if_r; rel_vals; simpl; eauto.
+    - iApply bin_log_related_arrow_val; try by unlock.
+      iAlways. iIntros (v1 v2) "/= Hi".
+      iDestruct "Hi" as (b) "[% %]"; simplify_eq.
+      unlock.
+      rel_rec_l.
+      rel_rec_r.
+      rel_op_r.
+      rel_vals; destruct b; simpl; eauto.
   Qed.
 
 End bit_refinement.
@@ -97,15 +95,15 @@ Proof.
   apply bit_prerefinement.
 Qed.
 
-
 Definition heapify : val := λ: "b", Unpack "b" $ λ: "b'",
-  let: "init" := Snd "b'" in
+  let: "init" := Fst (Fst "b'") in
   let: "flip" := Snd (Fst "b'") in
-  let: "view" := Fst (Fst "b'") in
+  let: "view" := Snd "b'" in
   let: "x" := ref "init" in
-  let: "flip_ref" := λ: <>, "x" <- "flip" (!"x") in
+  let: "l" := newlock #() in
+  let: "flip_ref" := λ: <>, acquire "l";; "x" <- "flip" (!"x");; release "l" in
   let: "view_ref" := λ: <>, "view" (!"x") in
-  Pack ("view_ref", "flip_ref", #()).
+  Pack (#(), "flip_ref", "view_ref").
 
 Lemma heapify_type Γ :
   typed Γ heapify (TArrow bitτ bitτ).
@@ -120,89 +118,6 @@ Section heapify_refinement.
   Context `{logrelG Σ}.
   Variable (Δ : list (prodC valC valC -n> iProp Σ)).
 
-  Lemma heapify_prerefinement Γ E1 (b1 b2 : val) :
-    nclose logrelN ⊆ E1 →
-    □ (interp E1 E1 bitτ Δ (PackV b1, PackV b2)) -∗
-    {E1,E1;Δ;Γ} ⊨ heapify (Pack b1) ≤log≤ heapify (Pack b2) : bitτ.
-  Proof.
-    simpl.
-    iIntros (?) "#Hlog".
-    iDestruct "Hlog" as ([? ?]) "[% #Hlog]"; simplify_eq.
-    iDestruct "Hlog" as (τi) "[% Hlog]".
-    iDestruct "Hlog" as ([? ?] [init1 init2]) "[% [#Hlog #Hτi]]"; simplify_eq.
-    iDestruct "Hlog" as ([view1 view2] [flip1 flip2]) "[% [#Hview #Hflip]]"; simplify_eq/=.
-    unfold heapify. unlock.
-    rel_rec_l.
-    rel_rec_r.
-    rel_pure_l (Unpack (Pack _) _).
-    rel_pure_r (Unpack (Pack _) _).
-    rel_rec_l.
-    rel_rec_r.
-    rel_proj_l.
-    rel_rec_l.
-    rel_proj_l. rel_proj_l.
-    rel_rec_l.
-    rel_proj_l. rel_proj_l.
-    rel_rec_l.
-    repeat rel_pure_r _.
-    rel_alloc_l as x1 "Hx1".
-    rel_alloc_r as x2 "Hx2".
-    repeat rel_pure_l _.
-    repeat rel_pure_r _.
-    iApply (bin_log_related_pack _ (interp_unit [])).
-    iMod (inv_alloc (logN .@ (x1,x2)) _ (interp_ref_inv (x1,x2) τi) with "[-]") as "#Hinv".
-    { iNext. unfold interp_ref_inv. simpl.
-      iExists (init1,init2). simpl. by iFrame. }
-    repeat iApply bin_log_related_pair.
-    - iApply bin_log_related_arrow_val; try by unlock.
-      iAlways. iIntros (v1 v2) "/= #Hi".
-      iDestruct "Hi" as "[% %]"; simplify_eq.
-      rel_rec_l.
-      rel_rec_r.
-      rel_load_l_atomic.
-      iInv (logN .@ (x1,x2)) as ([v1 v2]) "(Hx1 & Hx2 & #Hvv) /=" "Hcl".
-        iExists v1; iFrame. iModIntro. iNext.
-        iIntros "Hx1".
-      rel_load_r.
-      iMod ("Hcl" with "[-]").
-      { iNext. iExists (_,_). by iFrame. }
-      iSpecialize ("Hview" with "Hvv"). simpl.
-      rewrite bin_log_related_eq /bin_log_related_def.
-      iIntros (vvs ρ) "Hspec HΓ /=". unfold env_subst.
-      rewrite !Closed_subst_p_id.
-      iApply "Hview".
-    - iApply bin_log_related_arrow_val; try by unlock.
-      iAlways. iIntros (v1 v2) "/= #Hi".
-      iDestruct "Hi" as "[% %]"; simplify_eq.
-      rel_rec_l.
-      rel_rec_r.
-      rel_load_l_atomic.
-      iInv (logN .@ (x1,x2)) as ([v1 v2]) "(Hx1 & Hx2 & #Hvv) /=" "Hcl".
-        iExists v1; iFrame. iModIntro. iNext.
-        iIntros "Hx1".
-      rel_load_r.
-      iMod ("Hcl" with "[-]").
-      { iNext. iExists (_,_). by iFrame. }
-      iSpecialize ("Hflip" with "Hvv"). simpl. iClear "Hvv".
-      rewrite bin_log_related_eq /bin_log_related_def.
-      iIntros (vvs ρ) "Hspec #HΓ /=". unfold env_subst.
-      rewrite !Closed_subst_p_id.
-      iIntros (j K) "Hj /=".
-      tp_bind j (flip2 v2).
-      iMod ("Hflip" with "Hj") as "Hfl". iModIntro.
-      wp_bind (flip1 v1).
-      iApply (wp_wand with "Hfl"). iIntros (v1').
-      iDestruct 1 as (v2') "[Hj #Hvv']".
-      iInv (logN .@ (x1,x2)) as ([? ?]) "(Hx1 & Hx2 & #Hxs) /=" "Hcl".
-      iApply (wp_store with "Hx1"); eauto using to_of_val. iNext.
-      iIntros "Hx1".
-      tp_store j.
-      iMod ("Hcl" with "[-Hj]").
-      { iNext. iExists (_,_). by iFrame. }
-      iModIntro. iExists (#()); iFrame "Hj". eauto.
-    - rel_vals; simpl; eauto.
-  Qed.
-
   Lemma heapify_refinement_ez Γ E1 b1 b2 :
     ↑logrelN ⊆ E1 →
     {E1,E1;Δ;Γ} ⊨ b1 ≤log≤ b2 : bitτ -∗
@@ -212,6 +127,89 @@ Section heapify_refinement.
     iApply bin_log_related_app; eauto.
     iApply binary_fundamental_masked; eauto with typeable.
   Qed.
+
+  (* Lemma heapify_prerefinement Γ E1 (b1 b2 : val) : *)
+  (*   nclose logrelN ⊆ E1 → *)
+  (*   □ (interp E1 E1 bitτ Δ (PackV b1, PackV b2)) -∗ *)
+  (*   {E1,E1;Δ;Γ} ⊨ heapify (Pack b1) ≤log≤ heapify (Pack b2) : bitτ. *)
+  (* Proof. *)
+  (*   simpl. *)
+  (*   iIntros (?) "#Hlog". *)
+  (*   iDestruct "Hlog" as ([? ?]) "[% #Hlog]"; simplify_eq. *)
+  (*   iDestruct "Hlog" as (τi) "[% Hlog]". *)
+  (*   iDestruct "Hlog" as ([? ?] [init1 init2]) "[% [#Hlog #Hτi]]"; simplify_eq. *)
+  (*   iDestruct "Hlog" as ([view1 view2] [flip1 flip2]) "[% [#Hview #Hflip]]"; simplify_eq/=. *)
+  (*   unfold heapify. unlock. *)
+  (*   rel_rec_l. *)
+  (*   rel_rec_r. *)
+  (*   rel_pure_l (Unpack (Pack _) _). *)
+  (*   rel_pure_r (Unpack (Pack _) _). *)
+  (*   rel_rec_l. *)
+  (*   rel_rec_r. *)
+  (*   rel_proj_l. *)
+  (*   rel_rec_l. *)
+  (*   rel_proj_l. rel_proj_l. *)
+  (*   rel_rec_l. *)
+  (*   rel_proj_l. rel_proj_l. *)
+  (*   rel_rec_l. *)
+  (*   repeat rel_pure_r _. *)
+  (*   rel_alloc_l as x1 "Hx1". *)
+  (*   rel_alloc_r as x2 "Hx2". *)
+  (*   repeat rel_pure_l _. *)
+  (*   repeat rel_pure_r _. *)
+  (*   iApply (bin_log_related_pack _ (interp_unit [])). *)
+  (*   iMod (inv_alloc (logN .@ (x1,x2)) _ (interp_ref_inv (x1,x2) τi) with "[-]") as "#Hinv". *)
+  (*   { iNext. unfold interp_ref_inv. simpl. *)
+  (*     iExists (init1,init2). simpl. by iFrame. } *)
+  (*   repeat iApply bin_log_related_pair. *)
+  (*   - iApply bin_log_related_arrow_val; try by unlock. *)
+  (*     iAlways. iIntros (v1 v2) "/= #Hi". *)
+  (*     iDestruct "Hi" as "[% %]"; simplify_eq. *)
+  (*     rel_rec_l. *)
+  (*     rel_rec_r. *)
+  (*     rel_load_l_atomic. *)
+  (*     iInv (logN .@ (x1,x2)) as ([v1 v2]) "(Hx1 & Hx2 & #Hvv) /=" "Hcl". *)
+  (*       iExists v1; iFrame. iModIntro. iNext. *)
+  (*       iIntros "Hx1". *)
+  (*     rel_load_r. *)
+  (*     iMod ("Hcl" with "[-]"). *)
+  (*     { iNext. iExists (_,_). by iFrame. } *)
+  (*     iSpecialize ("Hview" with "Hvv"). simpl. *)
+  (*     rewrite bin_log_related_eq /bin_log_related_def. *)
+  (*     iIntros (vvs ρ) "Hspec HΓ /=". unfold env_subst. *)
+  (*     rewrite !Closed_subst_p_id. *)
+  (*     iApply "Hview". *)
+  (*   - iApply bin_log_related_arrow_val; try by unlock. *)
+  (*     iAlways. iIntros (v1 v2) "/= #Hi". *)
+  (*     iDestruct "Hi" as "[% %]"; simplify_eq. *)
+  (*     rel_rec_l. *)
+  (*     rel_rec_r. *)
+  (*     rel_load_l_atomic. *)
+  (*     iInv (logN .@ (x1,x2)) as ([v1 v2]) "(Hx1 & Hx2 & #Hvv) /=" "Hcl". *)
+  (*       iExists v1; iFrame. iModIntro. iNext. *)
+  (*       iIntros "Hx1". *)
+  (*     rel_load_r. *)
+  (*     iMod ("Hcl" with "[-]"). *)
+  (*     { iNext. iExists (_,_). by iFrame. } *)
+  (*     iSpecialize ("Hflip" with "Hvv"). simpl. iClear "Hvv". *)
+  (*     rewrite bin_log_related_eq /bin_log_related_def. *)
+  (*     iIntros (vvs ρ) "Hspec #HΓ /=". unfold env_subst. *)
+  (*     rewrite !Closed_subst_p_id. *)
+  (*     iIntros (j K) "Hj /=". *)
+  (*     tp_bind j (flip2 v2). *)
+  (*     iMod ("Hflip" with "Hj") as "Hfl". iModIntro. *)
+  (*     wp_bind (flip1 v1). *)
+  (*     iApply (wp_wand with "Hfl"). iIntros (v1'). *)
+  (*     iDestruct 1 as (v2') "[Hj #Hvv']". *)
+  (*     iInv (logN .@ (x1,x2)) as ([? ?]) "(Hx1 & Hx2 & #Hxs) /=" "Hcl". *)
+  (*     iApply (wp_store with "Hx1"); eauto using to_of_val. iNext. *)
+  (*     iIntros "Hx1". *)
+  (*     tp_store j. *)
+  (*     iMod ("Hcl" with "[-Hj]"). *)
+  (*     { iNext. iExists (_,_). by iFrame. } *)
+  (*     iModIntro. iExists (#()); iFrame "Hj". eauto. *)
+  (*   - rel_vals; simpl; eauto. *)
+  (* Qed. *)
   
 End heapify_refinement.