complete hash race

theories/coneris/examples/hash/con_hash_impl0.v

@@ -231,7 +231,7 @@ Section con_hash_impl.
 
   Lemma con_hash_alloc_tape N f l hm P {HP: ∀ m m', Timeless (P m m')} R {HR: ∀ m, Timeless (R m )} γ_tape γ_lock Q:
   {{{ con_hash_inv N f l hm P R γ_tape γ_lock ∗
-      (∀ m m' α, P m m' -∗ ⌜α∉dom m'⌝ -∗ |={⊤∖↑N}=> P m (<[α:=[]]>m') ∗ Q α)
+      (∀ m m' α, P m m' -∗ ⌜α∉dom m'⌝ -∗ |={⊤∖↑N.@"hash"}=> P m (<[α:=[]]>m') ∗ Q α)
   }}}
       allocate_tape #()
       {{{ (α: val), RET α; hash_tape α [] γ_tape ∗ Q α }}}.
@@ -248,9 +248,7 @@ Section con_hash_impl.
       iDestruct "Htokens" as "[? ?]".
       iApply (rand_token_exclusive with "[$][$]").
     }
-    iMod (fupd_mask_subseteq) as "Hclose'"; last iMod ("Hvs" with "[$HP][//]") as "[HP HQ]".
-    { apply difference_mono_l. apply nclose_subseteq. }
-    iMod "Hclose'" as "_".
+    iMod ("Hvs" with "[$HP][//]") as "[HP HQ]".
     iMod (abstract_tapes_new with "[$]") as "[Hauth Htape]"; last first.
     - iMod ("Hclose" with "[$Hown $HP Hauth Htoken Htokens]").
       + rewrite /hash_tape_auth. rewrite fmap_insert. iFrame.
@@ -261,14 +259,14 @@ Section con_hash_impl.
     - rewrite lookup_fmap. apply not_elem_of_dom_1 in H. by rewrite H.
   Qed.
 
-  Lemma con_hash_spec N f l hm P {HP: ∀ m m', Timeless (P m m')} R {HR: ∀ m, Timeless (R m )} γ_tape γ_lock Q1 Q2 α (v:nat):
+  Lemma con_hash_spec  N f l hm P {HP: ∀ m m', Timeless (P m m')} R {HR: ∀ m, Timeless (R m )} γ_tape γ_lock Q1 Q2 α (v:nat):
   {{{ con_hash_inv N f l hm P R γ_tape γ_lock ∗ 
-      ( ∀ m m', R m -∗ P m m' -∗ state_update (⊤∖↑N) (⊤∖↑N)
+      ( ∀ m m', R m -∗ P m m' -∗ hash_tape_auth m' γ_tape -∗ state_update (⊤∖↑N.@"hash") (⊤∖↑N.@"hash")
              match m!!v with
-             | Some res => R m ∗ P m m' ∗ Q1 res
-             | None => ∃ n ns, hash_tape α (n::ns) γ_tape ∗ P m m' ∗
+             | Some res => R m ∗ P m m' ∗ hash_tape_auth m' γ_tape ∗ Q1 res
+             | None => ∃ n ns, hash_tape α (n::ns) γ_tape ∗ P m (<[α:=n::ns]> m') ∗ hash_tape_auth (<[α:=n::ns]> m') γ_tape ∗
                               (∀ m'', P m m'' -∗  ⌜m''!!α=Some (n::ns)⌝
-                                      ={⊤∖↑N}=∗ R (<[v:=n]> m) ∗ P (<[v:=n]> m) (<[α:=ns]> m'') ∗ Q2 n ns)
+                                      ={⊤∖↑N.@"hash"}=∗ R (<[v:=n]> m) ∗ P (<[v:=n]> m) (<[α:=ns]> m'') ∗ Q2 n ns)
              end                                        
       )
   }}}
@@ -302,12 +300,10 @@ Section con_hash_impl.
       (* iDestruct (abstract_tapes_agree with "[$][$]") as "%H". *)
       (* rewrite lookup_fmap in H. apply fmap_Some_1 in H. *)
       (* destruct H as (?&?&?). simplify_eq. *)
-      iMod (fupd_mask_subseteq) as "Hclose'"; last iMod ("Hvs" with "[$][$]") as "Hvs"; try done.
-      { apply difference_mono_l. apply nclose_subseteq. }
-      iMod "Hclose'" as "_".
+      iMod ("Hvs" with "[$][$][$]") as "Hvs"; try done.
       rewrite Hres.
-      iDestruct "Hvs" as "(HR & HP & HQ)".
-      iMod ("Hclose" with "[$H1 $HP $Htauth $Htapes]") as "_"; first done.
+      iDestruct "Hvs" as "(HR & HP & [Htoken Htauth] & HQ)".
+      iMod ("Hclose" with "[$H1 $HP $Htauth $Htoken]") as "_"; first done.
       iModIntro.
       wp_apply (release_spec with "[$Hin2 $Hl $Hfrag $Hm $HR]") as "_"; first done.
       wp_pures.
@@ -335,12 +331,11 @@ Section con_hash_impl.
       iInv "Hinv1" as ">(%&%&->&H1&[Htapes Htauth]&H2)" "Hclose".
       iDestruct (ghost_var_agree with "[$][$]") as "->".
       rewrite /hash_tape /hash_tape_auth.
-      iMod (fupd_mask_subseteq) as "Hclose'"; last iMod ("Hvs" with "[$][$]") as "Hvs"; try done.
-      { apply difference_mono_l. apply nclose_subseteq. }
+      iMod ("Hvs" with "[$][$][$]") as "Hvs"; try done.
       rewrite Hres.
-      iDestruct "Hvs" as "(%&%&[Htape Htape']&HP&Hvs)".
-      iMod ("Hclose'") as "_".
-      iMod ("Hclose" with "[$H1 $Htauth $Htapes $HP//]") as "_".
+      iDestruct "Hvs" as "(%&%&[Htape Htape']&HP&[Htapes Htauth]&Hvs)".
+      iDestruct (abstract_tapes_agree with "[$][$]") as "%Hsome'".
+      iMod ("Hclose" with "[$H1 $Htauth $Htapes $HP]") as "_"; first done.
       iModIntro.
       wp_apply (rand_tape_spec_some with "[$]") as "Htape"; first done.
       iApply fupd_pgl_wp.
@@ -351,9 +346,7 @@ Section con_hash_impl.
       iDestruct (ghost_var_agree with "[$][$]") as "->".
       iMod (abstract_tapes_pop with "[$][$]") as "[Hauth Htape']".
       simplify_eq.
-      iMod (fupd_mask_subseteq) as "Hclose'"; last iMod ("Hvs" with "[$][]") as "Hvs"; try done.
-      { apply difference_mono_l. apply nclose_subseteq. }
-      iMod "Hclose'" as "_".
+      iMod ("Hvs" with "[$][]") as "Hvs"; try done.
       iDestruct "Hvs" as "(HR&HP&HQ)". simplify_eq.
       iMod (ghost_var_update with "[$][$]") as "[Hown Hown']".
       iMod ("Hclose" with "[Hauth Htoken Hown HP]") as "_".
@@ -426,12 +419,12 @@ Section con_hash_impl.
   (*   iIntros (???) "[??][??]". *)
   (*   iApply (abstract_tapes_auth_exclusive with "[$][$]"). *)
   (* Qed. *)
-  (* Next Obligation. *)
-  (*   iIntros (????) "[??][??]". *)
-  (*   iDestruct (abstract_tapes_agree with "[$][$]") as "%H". *)
-  (*   rewrite lookup_fmap in H. apply fmap_Some_1 in H. *)
-  (*   destruct H as (?&?&?). by simplify_eq. *)
-  (* Qed. *)
+  Next Obligation.
+    iIntros (????) "[??][??]".
+    iDestruct (abstract_tapes_agree with "[$][$]") as "%H".
+    rewrite lookup_fmap in H. apply fmap_Some_1 in H.
+    destruct H as (?&?&?). by simplify_eq.
+  Qed.
   Next Obligation.
     iIntros (???????????????????) "#(%&[? Hinv]&?)[??][??]Herr".
     iDestruct (abstract_tapes_agree with "[$][$]") as "%H'".

theories/coneris/examples/hash/con_hash_impl1.v

@@ -282,7 +282,7 @@ Section con_hash_impl1.
 
   Lemma con_hash_alloc_tape N f l hm P {HP: ∀ m m', Timeless (P m m')} R {HR: ∀ m, Timeless (R m )} γ1 γ2 γ3 γ_lock Q:
   {{{ con_hash_inv N f l hm P R γ1 γ2 γ3 γ_lock ∗
-      (∀ m m' α, P m m' -∗ ⌜α∉dom m'⌝ -∗ |={⊤∖↑N}=> P m (<[α:=[]]>m') ∗ Q α)
+      (∀ m m' α, P m m' -∗ ⌜α∉dom m'⌝ -∗ |={⊤∖↑N.@"hash"}=> P m (<[α:=[]]>m') ∗ Q α)
   }}}
       allocate_tape #()
       {{{ (α: val), RET α; hash_tape α [] γ2 γ3 ∗ Q α }}}.
@@ -300,14 +300,14 @@ Section con_hash_impl1.
       iApply "HΦ". by iFrame.
   Qed.
 
-  Lemma con_hash_spec N f l hm P {HP: ∀ m m', Timeless (P m m')} R {HR: ∀ m, Timeless (R m )} γ1 γ2 γ3 γ_lock Q1 Q2 α (v:nat):
+  Lemma con_hash_spec  N f l hm P {HP: ∀ m m', Timeless (P m m')} R {HR: ∀ m, Timeless (R m )} γ1 γ2 γ3 γ_lock Q1 Q2 α (v:nat):
   {{{ con_hash_inv N f l hm P R γ1 γ2 γ3 γ_lock ∗ 
-      ( ∀ m m', R m -∗ P m m' -∗ hash_auth m γ1 γ2 -∗ state_update (⊤∖↑N) (⊤∖↑N)
+      ( ∀ m m', R m -∗ P m m' -∗ hash_tape_auth m' γ2 γ3 -∗ hash_auth m γ1 γ2 -∗ state_update (⊤∖↑N.@"hash") (⊤∖↑N.@"hash")
              match m!!v with
-             | Some res => R m ∗ P m m' ∗ hash_auth m γ1 γ2 ∗ Q1 res
-             | None => ∃ n ns, hash_tape α (n::ns) γ2 γ3 ∗ P m m' ∗
+             | Some res => R m ∗ P m m' ∗ hash_auth m γ1 γ2 ∗ hash_tape_auth m' γ2 γ3 ∗ Q1 res
+             | None => ∃ n ns, hash_tape α (n::ns) γ2 γ3 ∗ P m (<[α:=n::ns]> m') ∗ hash_tape_auth (<[α:=n::ns]> m') γ2 γ3 ∗
                               (∀ m'', P m m'' -∗  ⌜m''!!α=Some (n::ns)⌝
-                                      ={⊤∖↑N}=∗ R (<[v:=n]> m) ∗ P (<[v:=n]> m) (<[α:=ns]> m'') ∗
+                                      ={⊤∖↑N.@"hash"}=∗ R (<[v:=n]> m) ∗ P (<[v:=n]> m) (<[α:=ns]> m'') ∗
                                       hash_auth (<[v:=n]> m) γ1 γ2  ∗ Q2 n ns)
              end                                        
       )
@@ -320,13 +320,14 @@ Section con_hash_impl1.
   Proof.
     iIntros (Φ) "(#Hinv  & Hvs) HΦ".
     iApply (con_hash_spec0 _ _ _ _ _ _ _ _ Q1 (λ n ns, Q2 n ns ∗ [∗ list] n∈ns, hash_set_frag n _)%I with "[$Hinv Hvs]").
-    - iIntros (??) "[Hauth HR](#?&HP)".
-      iMod ("Hvs" with "[$][$][$]") as "Hcont".
+    - iIntros (??) "[Hauth HR](#?&HP)Htauth".
+      iMod ("Hvs" with "[$][$][$][$]") as "Hcont".
       case_match.
-      + by iDestruct "Hcont" as "($&$&$&$)".
-      + iDestruct "Hcont" as "(%&%&[? #Hfrag]&?&Hcont)".
+      + iDestruct "Hcont" as "(?&?&?&[??]&?)". by iFrame.
+      + iDestruct "Hcont" as "(%&%&[? #Hfrag]&?&[Htauth #?]&Hcont)".
         iFrame. iModIntro.
-        iSplit; first done.
+        iSplit.
+        { iApply big_sepM_insert_2; done. }
         iIntros (?) "[#? HP] %".
         iMod ("Hcont" with "[$][//]") as "(?&?&?&?)".
         iFrame. iModIntro. iSplit. 
@@ -408,10 +409,10 @@ Section con_hash_impl1.
   (*   iIntros (????) "[H1 ?][ H2 ?]". *)
   (*   iApply (con_hash_interface0.hash_tape_auth_exclusive with "[$][$]"). *)
   (* Qed. *)
-  (* Next Obligation. *)
-  (*   iIntros (?????) "[??][??]". *)
-  (*   iApply (con_hash_interface0.hash_tape_auth_frag_agree with "[$][$]"). *)
-  (* Qed. *)
+  Next Obligation.
+    iIntros (?????) "[??][??]".
+    iApply (con_hash_interface0.hash_tape_auth_frag_agree with "[$][$]").
+  Qed.
   Next Obligation.
     iIntros (??)"(?&%H&?)". iPureIntro. intros n H'.
     apply H in H'. lia.

theories/coneris/examples/hash/con_hash_impl2.v

@@ -116,7 +116,7 @@ Section con_hash_impl2.
 
   Lemma con_hash_alloc_tape N f l hm P {HP: ∀ m m', Timeless (P m m')} R {HR:∀ m, Timeless (R m)} γ1 γ2 γ3 γ4 γ5 γ_lock Q:
   {{{ con_hash_inv N f l hm P R γ1 γ2 γ3 γ4 γ5 γ_lock ∗
-      (∀ m m' α, P m m' -∗ ⌜α∉dom m'⌝ -∗ |={⊤∖↑N}=> P m (<[α:=[]]>m') ∗ Q α)
+      (∀ m m' α, P m m' -∗ ⌜α∉dom m'⌝ -∗ |={⊤∖↑N.@"hash"}=> P m (<[α:=[]]>m') ∗ Q α)
   }}}
       allocate_tape #()
       {{{ (α: val), RET α; hash_tape α [] γ2 γ3 ∗ Q α }}}.
@@ -135,12 +135,12 @@ Section con_hash_impl2.
 
   Lemma con_hash_spec N f l hm P {HP: ∀ m m', Timeless (P m m')} R {HR: ∀ m, Timeless (R m )} γ1 γ2 γ3 γ4 γ5 γ_lock Q1 Q2 α (v:nat):
   {{{ con_hash_inv N f l hm P R γ1 γ2 γ3 γ4 γ5 γ_lock ∗ 
-      ( ∀ m m', R m -∗ P m m' -∗ hash_auth m γ1 γ2 γ4 γ5-∗ state_update (⊤∖↑N) (⊤∖↑N)
+      ( ∀ m m', R m -∗ P m m' -∗ hash_tape_auth m' γ2 γ3 -∗ hash_auth m γ1 γ2 γ4 γ5-∗ state_update (⊤∖↑N.@"hash") (⊤∖↑N.@"hash")
              match m!!v with
-             | Some res => R m ∗ P m m' ∗ hash_auth m γ1 γ2 γ4 γ5∗ Q1 res
-             | None => ∃ n ns, hash_tape α (n::ns) γ2 γ3 ∗ P m m' ∗
+             | Some res => R m ∗ P m m' ∗ hash_tape_auth m' γ2 γ3 ∗ hash_auth m γ1 γ2 γ4 γ5∗ Q1 res
+             | None => ∃ n ns, hash_tape α (n::ns) γ2 γ3 ∗ P m (<[α:=n::ns]> m') ∗ hash_tape_auth (<[α:=n::ns]> m') γ2 γ3 ∗
                               (∀ m'', P m m'' -∗  ⌜m''!!α=Some (n::ns)⌝
-                                      ={⊤∖↑N}=∗ R (<[v:=n]> m) ∗ P (<[v:=n]> m) (<[α:=ns]> m'') ∗
+                                      ={⊤∖↑N.@"hash"}=∗ R (<[v:=n]> m) ∗ P (<[v:=n]> m) (<[α:=ns]> m'') ∗
                                       hash_auth (<[v:=n]> m) γ1 γ2 γ4 γ5∗ Q2 n ns)
              end                                        
       )
@@ -154,21 +154,21 @@ Section con_hash_impl2.
     iIntros (Φ) "(#Hinv  & Hvs) HΦ".
     rewrite /hash_tape/hash_set_frag.
     iApply (con_hash_spec1 _ _ _ _ _ _ _ _ _ _ Q1 Q2 with "[$Hinv Hvs]").
-    - iIntros (??) "(Hhv & Hfrag & HR) HP Hauth1".
+    - iIntros (??) "(Hhv & Hfrag & HR) HP Htauth Hauth1".
       rewrite /hash_auth.
       rewrite /hash_set_frag.
-      iMod ("Hvs" with "[$][$][Hauth1 $Hhv Hfrag]") as "Hcont".
+      iMod ("Hvs" with "[$][$][$][Hauth1 $Hhv Hfrag]") as "Hcont".
       { rewrite big_sepM_sep. iFrame "Hfrag". iSplit; first done.
         rewrite big_sepM_forall. iIntros.
         iDestruct (con_hash_interface1.hash_auth_duplicate with "[$]") as "#?"; first done.
         by iApply hash_frag_in_hash_set.
       }
       case_match.
-      + iDestruct "Hcont" as "($&$&($&?&H)&$)".
+      + iDestruct "Hcont" as "($&$&$&($&?&H)&$)".
         iFrame.
         rewrite big_sepM_sep.
         by iDestruct "H" as "[??]".
-      + iDestruct "Hcont" as "(%&%&?&?&Hcont)".
+      + iDestruct "Hcont" as "(%&%&?&?&?&Hcont)".
         iModIntro.
         iFrame. iIntros.
         iMod ("Hcont" with "[$][//]") as "(?&?&(?&?&H)&?)".
@@ -252,7 +252,10 @@ Section con_hash_impl2.
     iModIntro. rewrite big_sepM_sep.
     by iFrame.
   Qed.
-
+  Next Obligation.
+    iIntros.
+    iApply (con_hash_interface1.hash_tape_auth_frag_agree with "[$][$]").
+  Qed.
   Next Obligation.
     iIntros (????) "?".
     by iApply con_hash_interface1.hash_tape_valid.