fix spec of incr_counter_tape_spec_some

logsem · Sep 27, 2024 · 22b341b · 22b341b
1 parent a75cb86
commit 22b341b
Show file tree

Hide file tree

Showing 2 changed files with 55 additions and 52 deletions.
diff --git a/theories/coneris/examples/random_counter/impl1.v b/theories/coneris/examples/random_counter/impl1.v
@@ -8,8 +8,8 @@ Section impl1.
   Context `{H:conerisGS Σ, r1:@rand_spec Σ H, L:randG Σ, !inG Σ (frac_authR natR)}.
 
   Definition new_counter1 : val:= λ: "_", ref #0.
-  Definition allocate_tape1 : val := λ: "_", rand_allocate_tape #3.
-  Definition incr_counter_tape1 :val := λ: "l" "α", let: "n" := rand_tape "α" #3 in (FAA "l" "n", "n").
+  Definition allocate_tape1 : val := λ: "_", rand_allocate_tape #3%nat.
+  Definition incr_counter_tape1 :val := λ: "l" "α", let: "n" := rand_tape "α" #3%nat in (FAA "l" "n", "n").
   Definition read_counter1 : val := λ: "l", !"l".
   Class counterG1 Σ := CounterG1 { counterG1_randG : randG Σ;
                                    counterG1_frac_authR:: inG Σ (frac_authR natR) }.
@@ -91,38 +91,31 @@ Section impl1.
           ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, [])
       }}}.
   Proof.
-  Admitted.
-  (*   iIntros (Hsubset Φ) "#Hinv HΦ". *)
-  (*   rewrite /allocate_tape1. *)
-  (*   wp_pures. *)
-  (*   wp_alloctape α as "Hα". *)
-  (*   iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *)
-  (*   iDestruct (hocap_tapes_notin with "[$][$]") as "%". *)
-  (*   iMod (hocap_tapes_new with "[$]") as "[H4 H7]"; first done. *)
-  (*   iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Hα]") as "_". *)
-  (*   { iNext. iSplitL; last done. *)
-  (*     rewrite big_sepM_insert; [simpl; iFrame|done]. *)
-  (*   } *)
-  (*   iApply "HΦ". *)
-  (*   by iFrame. *)
-  (* Qed. *)
+    iIntros (Hsubset Φ) "[#Hinv #Hinv'] HΦ".    
+    rewrite /allocate_tape1.
+    wp_pures.
+    wp_apply rand_allocate_tape_spec; [by eapply nclose_subseteq'|done..].
+  Qed.
 
   Lemma incr_counter_tape_spec_some1 N E c γ1 γ2 (Q:nat->nat -> list nat -> iProp Σ) (α:loc) :
     ↑N⊆E ->
     {{{ is_counter1 N c γ1 γ2 ∗
-        (∀ (z:nat), own γ2 (●F z) ={E∖ ↑N, ∅}=∗
-                   ∃ n ns, rand_tapes_frag (L:=L) γ1 α (3%nat, n::ns) ∗
-                    (rand_tapes_frag (L:=L) γ1 α (3%nat, ns) ={∅, E∖↑N}=∗
-                     own γ2 (●F (z+n)%nat) ∗ Q z n ns)
+        ( |={E∖ ↑N, ∅}=>
+                   ∃ n ns, rand_tapes_frag (L:=L) γ1 α (3, n::ns) ∗
+                    (rand_tapes_frag (L:=L) γ1 α (3, ns) ={∅, E∖↑N}=∗
+                     ∀ (z:nat), own γ2 (●F z)
+                              ={E∖↑N}=∗
+                              own γ2 (●F (z+n)) ∗ Q z n ns)
           )
     }}}
       incr_counter_tape1 c #lbl:α @ E
       {{{ (z n:nat), RET (#z, #n); ∃ ns, Q z n ns}}}.
   Proof.
-  Admitted.
-  (*   iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP & Hα) HΦ". *)
-  (*   rewrite /incr_counter_tape1. *)
-  (*   wp_pures. *)
+    iIntros (Hsubset Φ) "([#Hinv #Hinv'] & Hvs) HΦ".
+    rewrite /incr_counter_tape1.
+    wp_pures.
+    wp_apply (rand_tape_spec_some with "[Hvs]"); [by eapply nclose_subseteq'|iSplit; first done|..].
+  (*   - iSplit *)
   (*   wp_bind (rand(_) _)%E. *)
   (*   iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *)
   (*   iDestruct (hocap_tapes_agree with "[$][$]") as "%". *)
@@ -153,7 +146,8 @@ Section impl1.
   (*   iModIntro. wp_pures. *)
   (*   iApply "HΦ". *)
   (*   by iFrame. *)
-  (* Qed. *)
+    (* Qed. *)
+  Admitted.
 
   Lemma counter_presample_spec1  NS E T γ1 γ2 c:
     ↑NS ⊆ E ->

diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v
@@ -77,10 +77,12 @@ Class random_counter `{!conerisGS Σ} := RandCounter
   incr_counter_tape_spec_some {L: counterG Σ} N E c γ1 γ2 (Q:nat->nat->list nat->iProp Σ) (α:loc) :
     ↑N⊆E ->
     {{{ is_counter (L:=L) N c γ1 γ2 ∗
-        (∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖ ↑N, ∅}=∗
+        ( |={E∖ ↑N, ∅}=>
                    ∃ n ns, counter_tapes_frag (L:=L) γ1 α (n::ns) ∗
                     (counter_tapes_frag (L:=L) γ1 α ns ={∅, E∖↑N}=∗
-                     counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ns)
+                     ∀ (z:nat), counter_content_auth (L:=L) γ2 z
+                              ={E∖↑N}=∗
+                              counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ns)
           ) 
     }}}
       incr_counter_tape c #lbl:α @ E
@@ -121,14 +123,15 @@ Section lemmas.
               ↯ ε ∗ counter_tapes_frag (L:=L) γ1 α [] ∗
               ⌜(∀ n, 0<=ε2 n)%R⌝ ∗
               ⌜(((ε2 0%nat) + (ε2 1%nat)+ (ε2 2%nat)+ (ε2 3%nat))/4 <= ε)%R⌝ ∗
-              (∀ n, ↯ (ε2 n) ∗ counter_tapes_frag (L:=L) γ1 α [n] ={∅,E∖↑N}=∗
-                    ∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖↑N, ∅}=∗
-                             counter_tapes_frag (L:=L) γ1 α [n]∗
-                           (counter_tapes_frag (L:=L) γ1 α []={∅, E∖↑N}=∗
-                    counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ε ε2
+              (∀ n, ↯ (ε2 n) ∗ counter_tapes_frag (L:=L) γ1 α [n] ={∅, E∖↑N}=∗
+                    |={E∖↑N, ∅}=>
+                    counter_tapes_frag (L:=L) γ1 α [n] ∗
+                    (counter_tapes_frag (L:=L) γ1 α [] ={∅,E∖↑N}=∗
+                     ∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖↑N}=∗
+                              counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ε ε2
+                    )
               )
-              )
-        ) 
+              ) 
     }}}
       incr_counter_tape c #lbl:α @ E
                                  {{{ (z n:nat), RET (#z, #n); ∃ ε ε2, Q z n ε ε2 }}}.
@@ -138,13 +141,15 @@ Section lemmas.
             (λ ε α' ε2 num ns ns',
                ∃ n ε2', 
                  ⌜num=1%nat⌝ ∗ ⌜α'=α⌝ ∗ ⌜ns=[]⌝ ∗ ⌜ns'=[n]⌝ ∗
-                 ⌜(ε2' = λ x, ε2 [x])%R⌝ ∗
-                 (∀ z : nat,
-                    counter_content_auth γ2 z ={E ∖ ↑N,∅}=∗
-                    counter_tapes_frag γ1 α [n] ∗
-                    (counter_tapes_frag γ1 α [] ={∅,E ∖ ↑N}=∗
-                    counter_content_auth γ2 (z + n) ∗ Q z n ε ε2'))
-            )%I with "[//][-HΦ]") as "(%ε & % & %ε2 & %num & %ns & %ns' & %n & %ε2' & -> & -> & -> & -> & -> & Hrest)"; try done.
+                 ⌜(ε2' = λ x, ε2 [x])%R⌝ ∗ 
+                  ( |={E∖ ↑N, ∅}=>
+                    counter_tapes_frag (L:=L) γ1 α [n] ∗
+                    (counter_tapes_frag (L:=L) γ1 α [] ={∅, E∖↑N}=∗
+                     ∀ (z:nat), counter_content_auth (L:=L) γ2 z
+                              ={E∖↑N}=∗
+                              counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ε ε2')
+                  )
+            )%I with "[//][-HΦ]") as "(%ε & % & %ε2 & %num & %ns & %ns' & %n & %ε2' & -> & -> & -> & -> & -> & Hrest)"; first done.
     - iMod "Hvs" as "(%ε & %ε2 & Herr & Hfrag & %Hpos & %Hineq & Hrest)".
       iFrame. iModIntro.
       iExists (λ l, match l with |[x] => ε2 x | _ => 1 end)%R, 1%nat.
@@ -157,17 +162,19 @@ Section lemmas.
         * apply NoDup_fmap_2; last apply NoDup_enum_uniform_fin_list.
           apply list_fmap_eq_inj, fin_to_nat_inj.
       + iIntros (ns') "[Herr Hfrag]". destruct (ns') as [|n[|??]]; [by iDestruct (ec_contradict with "[$]") as "%"| |by iDestruct (ec_contradict with "[$]") as "%"].
-        iMod ("Hrest" $! n with "[$]").
-        iFrame.
-        by iPureIntro.
+        iMod ("Hrest" $! n with "[$]") as "?".
+        iModIntro.
+        by iFrame.
     - wp_apply (incr_counter_tape_spec_some _ _ _ _ _ (λ z n ns, ∃ ε ε2, Q z n ε ε2)%I with "[Hrest]"); first exact.
       + iSplit; first done.
-        iIntros (z) "Hauth".
-        iMod ("Hrest" with "[$]") as "[Hfrag Hrest]".
+        iMod "Hrest" as "[? Hrest]".
         iFrame.
         iModIntro.
-        iIntros "Hfrag".
-        iMod ("Hrest" with "[$]") as "[Hauth HQ]".
+        iIntros.
+        iMod ("Hrest" with "[$]") as "Hrest".
+        iModIntro.
+        iIntros (z) "Hauth".
+        iMod ("Hrest" with "[$]") as "[??]".
         by iFrame.
       + iIntros (??) "(%&%&%&HQ)".
         iApply "HΦ".
@@ -211,18 +218,20 @@ Section lemmas.
       + iIntros (n) "[Herr Hfrag]".
         iMod "Hclose" as "_".
         iModIntro.
-        iIntros (z') "Hauth".
         iApply fupd_mask_intro; first set_solver.
         iIntros "Hclose".
         rewrite /ε2'.
         case_match eqn:H; last by (iDestruct (ec_contradict with "[$]") as "%").
         iFrame.
         iIntros "Hfrag'".
-        iDestruct (counter_content_less_than with "[$][$]") as "%".
-        iMod (counter_content_update with "[$][$]") as "[??]".
         iMod "Hclose" as "_".
         iFrame.
         apply leb_complete in H.
+        iModIntro.
+        iIntros (z') "Hauth".
+        iDestruct (counter_content_less_than with "[$][$]") as "%".
+        iMod (counter_content_update with "[$][$]") as "[??]".
+        iFrame.
         iPureIntro; repeat split; try done; lia. 
     - iIntros (z' n) "(%ε' & %ε2'' & % & % &-> & -> & Herr & Hfrag & Hfrag')".
       iApply "HΦ".