NIT

logsem · Dec 3, 2024 · 181c0cd · 181c0cd
1 parent 530dac9
commit 181c0cd
Show file tree

Hide file tree

Showing 5 changed files with 21 additions and 22 deletions.
diff --git a/theories/coneris/examples/random_counter3/client.v b/theories/coneris/examples/random_counter3/client.v
@@ -97,7 +97,7 @@ Section client.
     }
     wp_apply (wp_par (λ _, ∃ (n:nat), own γ1 (◯E (Some n)) ∗ counter_content_frag γ (1/2) n)%I
                 (λ _, ∃ (n:nat), own γ2 (◯E (Some n)) ∗ counter_content_frag γ (1/2) n)%I with "[Hfrag1 Hc1][Hfrag2 Hc2]").
-    - wp_apply (incr_counter_spec _ _ _ _ (λ _ _, ∃ n : nat, own γ1 (◯E (Some n)) ∗ counter_content_frag γ (1 / 2) n )%I with "[$Hcounter Hfrag1 Hc1]"); [done| |by iIntros].
+    - wp_apply (incr_counter_spec _ _ _ _ (λ _ _ _ _, ∃ n : nat, own γ1 (◯E (Some n)) ∗ counter_content_frag γ (1 / 2) n )%I with "[$Hcounter Hfrag1 Hc1]"); [done| |by iIntros (??) "(%&%&?)"].
       iInv "Hinv" as ">(%n1 & %n2 & Hauth1 & Hauth2 & Herr)" "Hvs". 
       iDestruct (ghost_var_agree with "[$Hauth1][$]") as "->".
       iApply fupd_mask_intro; first set_solver.
@@ -142,7 +142,7 @@ Section client.
           -- iModIntro. iIntros (z) "Hauth".
              iMod (counter_content_update with "[$][$]") as "[$ ?]".
              by iFrame.
-    - wp_apply (incr_counter_spec _ _ _ _ (λ _ _, ∃ n : nat, own γ2 (◯E (Some n)) ∗ counter_content_frag γ (1 / 2) n )%I with "[$Hcounter Hfrag2 Hc2]"); [done| |by iIntros].
+    - wp_apply (incr_counter_spec _ _ _ _ (λ _ _ _ _, ∃ n : nat, own γ2 (◯E (Some n)) ∗ counter_content_frag γ (1 / 2) n )%I with "[$Hcounter Hfrag2 Hc2]"); [done| |by iIntros (??) "(%&%&?)"].
       iInv "Hinv" as ">(%n1 & %n2 & Hauth1 & Hauth2 & Herr)" "Hvs". 
       iDestruct (ghost_var_agree with "[$Hauth2][$]") as "->".
       iApply fupd_mask_intro; first set_solver.

diff --git a/theories/coneris/examples/random_counter3/impl1.v b/theories/coneris/examples/random_counter3/impl1.v
@@ -97,7 +97,7 @@ Section impl1.
   Qed.
 
 
-  Lemma incr_counter_spec1 N E c γ1 (Q:nat->nat->iProp Σ)  :
+  Lemma incr_counter_spec1 N E c γ1 (Q:_->_->nat->nat->iProp Σ)  :
     ↑N⊆E ->
     {{{ is_counter1 N c γ1 ∗
         |={E, ∅}=>
@@ -106,18 +106,18 @@ Section impl1.
               ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
               (∀ n, ↯ (ε2 n) ={∅, E}=∗
           (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
-                      own γ1 (●F (z+n)%nat) ∗ Q z n)))
+                      own γ1 (●F (z+n)%nat) ∗ Q ε ε2 z n)))
     }}}
       incr_counter1 c @ E
-                                 {{{ (z n:nat), RET (#z, #n); Q z n }}}.
+                                 {{{ (z n:nat), RET (#z, #n); ∃ ε ε2, Q ε ε2 z n }}}.
   Proof.
     iIntros (Hineq Φ) "[#Hinv Hvs] HΦ".
     rewrite /incr_counter1.
     wp_pures.
     wp_apply (rand_allocate_tape_spec with "[//]") as (α) "Htape".
     iAssert (state_update E E (∃ n, rand_tapes (L:=L) α (3%nat, [fin_to_nat n]) ∗
-                                    (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q z n)
-            ))%I with "[Hvs Htape]" as ">(%n & Htape &Hvs)".
+                                   ∃ε ε2, (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q ε ε2 z n)
+            ))%I with "[Hvs Htape]" as ">(%n & Htape &%&%&Hvs)".
     { iMod "Hvs" as "(%&%&?&%&%&Hvs)".
       iMod (counter_tapes_presample1 with "[$][$][$]") as "(%&?&?)"; [done..|].
       iMod ("Hvs" with "[$]").

diff --git a/theories/coneris/examples/random_counter3/impl2.v b/theories/coneris/examples/random_counter3/impl2.v
@@ -257,7 +257,7 @@ Section impl2.
         iPureIntro. constructor; [lia|constructor]. 
   Qed.
 
-Lemma incr_counter_spec2 N E c γ1 (Q:nat->nat->iProp Σ)  :
+Lemma incr_counter_spec2 N E c γ1 (Q:_-> _->nat->nat->iProp Σ)  :
     ↑N⊆E ->
     {{{ is_counter2 N c γ1 ∗
         |={E, ∅}=>
@@ -266,19 +266,19 @@ Lemma incr_counter_spec2 N E c γ1 (Q:nat->nat->iProp Σ)  :
               ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
               (∀ n, ↯ (ε2 n) ={∅, E}=∗
           (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
-                    own γ1 (●F (z+n)%nat) ∗ Q z n)))
+                    own γ1 (●F (z+n)%nat) ∗ Q ε ε2 z n)))
     }}}
       incr_counter2 c @ E
-      {{{ (z n:nat), RET (#z, #n); Q z n }}}.
+      {{{ (z n:nat), RET (#z, #n); ∃ ε ε2, Q ε ε2 z n }}}.
   Proof.
     iIntros (Hsubset Φ) "(#Hinv & Hvs) HΦ".
     rewrite /incr_counter2.
     wp_pures.
     wp_apply flip_allocate_tape_spec as (α) "Htape"; first done.
     wp_pures.
     iAssert (state_update E E (∃ n, (flip_tapes (L:=L) α (expander ([fin_to_nat n])) ∗ ⌜Forall (λ x, x<4) ([fin_to_nat n])⌝) ∗
-                                    (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q z n)
-            ))%I with "[Hvs Htape]" as ">(%n & (Htape&%) &Hvs)".
+                              ∃ ε ε2, (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q ε ε2 z n)
+            ))%I with "[Hvs Htape]" as ">(%n & (Htape&%) &%&%&Hvs)".
     { iMod "Hvs" as "(%&%&?&%&%&Hvs)".
       iMod (counter_tapes_presample2 with "[$][Htape][$]") as "(%&?&(?&%))"; [try done..|].
       - simpl. iFrame. iPureIntro. by rewrite Forall_nil.

diff --git a/theories/coneris/examples/random_counter3/impl3.v b/theories/coneris/examples/random_counter3/impl3.v
@@ -127,7 +127,7 @@ Section impl3.
       rewrite /filter_f. lia.
   Qed.
 
-  Lemma incr_counter_spec3 N E c γ1 (Q:nat->nat->iProp Σ)  :
+  Lemma incr_counter_spec3 N E c γ1 (Q:_->_->nat->nat->iProp Σ)  :
     ↑N⊆E ->
     {{{ is_counter3 N c γ1 ∗
         |={E,∅}=>
@@ -136,11 +136,11 @@ Section impl3.
               ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
               (∀ n, ↯ (ε2 n) ={∅, E}=∗
           (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
-                    own γ1 (●F (z+n)%nat) ∗ Q z n)))
+                    own γ1 (●F (z+n)%nat) ∗ Q ε ε2 z n)))
 
     }}}
       incr_counter3 c @ E
-      {{{ (z n:nat), RET (#z, #n); Q z n }}}.
+      {{{ (z n:nat), RET (#z, #n); ∃ ε ε2, Q ε ε2 z n }}}.
   Proof.
     iIntros (Hsubset Φ) "(#Hinv & Hvs) HΦ".
     rewrite /incr_counter3.
@@ -149,8 +149,8 @@ Section impl3.
     do 3 wp_pure.
     iAssert (state_update E E (∃ n,
                    (∃ ls, ⌜filter filter_f ls = ([fin_to_nat n])⌝ ∗ rand_tapes (L:=L) α (4, ls)) ∗
-                                    (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q z n)
-            ))%I with "[Hvs Htape]" as ">(%n & Htape &Hvs)".
+                                 ∃ ε ε2,  (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q ε ε2 z n)
+            ))%I with "[Hvs Htape]" as ">(%n & Htape &%&%&Hvs)".
     { iMod "Hvs" as "(%&%&?&%&%&Hvs)".
       iMod (counter_tapes_presample3 with "[$][$Htape][$]") as "(%&?&?)"; [try done..|].
       iMod ("Hvs" with "[$]").

diff --git a/theories/coneris/examples/random_counter3/random_counter.v b/theories/coneris/examples/random_counter3/random_counter.v
@@ -66,7 +66,7 @@ Class random_counter `{!conerisGS Σ} := RandCounter
     {{{ c, RET c; ∃ γ1, is_counter (L:=L) N c γ1 ∗
                            counter_content_frag (L:=L) γ1 1%Qp 0%nat
     }}};
-  incr_counter_spec {L: counterG Σ} N E c γ1 (Q:nat->nat->iProp Σ)  :
+  incr_counter_spec {L: counterG Σ} N E c γ1 (Q:_->_->nat->nat->iProp Σ)  :
     ↑N⊆E ->
     {{{ is_counter (L:=L) N c γ1 ∗
         |={E,∅}=>
@@ -75,11 +75,11 @@ Class random_counter `{!conerisGS Σ} := RandCounter
               ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
               (∀ n, ↯ (ε2 n) ={∅, E}=∗
           (∀ (z:nat), counter_content_auth (L:=L) γ1 z ={E∖↑N}=∗
-                      counter_content_auth (L:=L) γ1 (z+n) ∗ Q z n)))
+                      counter_content_auth (L:=L) γ1 (z+n) ∗ Q ε ε2 z n)))
 
     }}}
       incr_counter c @ E
-                                 {{{ (z n:nat), RET (#z, #n); Q z n }}}; 
+                                 {{{ (z n:nat), RET (#z, #n); ∃ ε ε2, Q ε ε2 z n }}}; 
   read_counter_spec {L: counterG Σ} N E c γ1 Q:
     ↑N ⊆ E ->
     {{{  is_counter (L:=L) N c γ1 ∗
@@ -162,7 +162,7 @@ Section lemmas.
     iIntros (Hsubset Hpos Hineq Φ) "(#Hinv & Herr & Hcontent) HΦ".
     pose (ε2' := (λ x, if (x<=?3)%nat then ε2 x else 1%R)).
     wp_apply (incr_counter_spec _ _ _ _
-                (λ z' n , ⌜0<=n<4⌝ ∗ ⌜z<=z'⌝ ∗
+                (λ _ _ z' n , ⌜0<=n<4⌝ ∗ ⌜z<=z'⌝ ∗
                           ↯ (ε2 n) ∗
                                  counter_content_frag (L:=L) γ1 q (z+n)%nat
                 )%I
@@ -186,7 +186,6 @@ Section lemmas.
     - iIntros (z' n) "(% & % & Herr & Hfrag' )".
       iApply "HΦ".
       iFrame.
-      by iSplit.
   Qed.
 
 End lemmas.