Change pupd into normal fupd in random counter 3 spec

logsem · Dec 3, 2024 · 530dac9 · 530dac9
1 parent 4aa91ef
commit 530dac9
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 13 deletions.
diff --git a/theories/coneris/examples/random_counter3/client.v b/theories/coneris/examples/random_counter3/client.v
@@ -98,9 +98,9 @@ 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].
-      iMod (state_update_inv_acc' with "[$]") as "[>(%n1 & %n2 & Hauth1 & Hauth2 & Herr) Hvs]"; first done.
+      iInv "Hinv" as ">(%n1 & %n2 & Hauth1 & Hauth2 & Herr)" "Hvs". 
       iDestruct (ghost_var_agree with "[$Hauth1][$]") as "->".
-      iApply state_update_mask_intro; first set_solver.
+      iApply fupd_mask_intro; first set_solver.
       iIntros "Hclose".
       case_match eqn:H.
       + iFrame. iExists  (λ _, 0%R).
@@ -143,9 +143,9 @@ Section client.
              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].
-      iMod (state_update_inv_acc' with "[$]") as "[>(%n1 & %n2 & Hauth1 & Hauth2 & Herr) Hvs]"; first done.
+      iInv "Hinv" as ">(%n1 & %n2 & Hauth1 & Hauth2 & Herr)" "Hvs". 
       iDestruct (ghost_var_agree with "[$Hauth2][$]") as "->".
-      iApply state_update_mask_intro; first set_solver.
+      iApply fupd_mask_intro; first set_solver.
       iIntros "Hclose".
       case_match eqn:H.
       + iFrame. iExists (λ _, 0%R). repeat iSplit; try iPureIntro.

diff --git a/theories/coneris/examples/random_counter3/impl1.v b/theories/coneris/examples/random_counter3/impl1.v
@@ -100,11 +100,11 @@ Section impl1.
   Lemma incr_counter_spec1 N E c γ1 (Q:nat->nat->iProp Σ)  :
     ↑N⊆E ->
     {{{ is_counter1 N c γ1 ∗
-        state_update E ∅
+        |={E, ∅}=>
           (∃ ε (ε2 : fin 4%nat -> R),
               ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
               ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
-              (∀ n, ↯ (ε2 n) -∗ state_update ∅ E
+              (∀ n, ↯ (ε2 n) ={∅, E}=∗
           (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
                       own γ1 (●F (z+n)%nat) ∗ Q z n)))
     }}}

diff --git a/theories/coneris/examples/random_counter3/impl2.v b/theories/coneris/examples/random_counter3/impl2.v
@@ -260,11 +260,11 @@ Section impl2.
 Lemma incr_counter_spec2 N E c γ1 (Q:nat->nat->iProp Σ)  :
     ↑N⊆E ->
     {{{ is_counter2 N c γ1 ∗
-        state_update E ∅
+        |={E, ∅}=>
           (∃ ε (ε2 : fin 4%nat -> R),
               ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
               ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
-              (∀ n, ↯ (ε2 n) -∗ state_update ∅ E
+              (∀ n, ↯ (ε2 n) ={∅, E}=∗
           (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
                     own γ1 (●F (z+n)%nat) ∗ Q z n)))
     }}}

diff --git a/theories/coneris/examples/random_counter3/impl3.v b/theories/coneris/examples/random_counter3/impl3.v
@@ -130,11 +130,11 @@ Section impl3.
   Lemma incr_counter_spec3 N E c γ1 (Q:nat->nat->iProp Σ)  :
     ↑N⊆E ->
     {{{ is_counter3 N c γ1 ∗
-        state_update E ∅
+        |={E,∅}=>
           (∃ ε (ε2 : fin 4%nat -> R),
               ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
               ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
-              (∀ n, ↯ (ε2 n) -∗ state_update ∅ E
+              (∀ n, ↯ (ε2 n) ={∅, E}=∗
           (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
                     own γ1 (●F (z+n)%nat) ∗ Q z n)))
 

diff --git a/theories/coneris/examples/random_counter3/random_counter.v b/theories/coneris/examples/random_counter3/random_counter.v
@@ -69,11 +69,11 @@ Class random_counter `{!conerisGS Σ} := RandCounter
   incr_counter_spec {L: counterG Σ} N E c γ1 (Q:nat->nat->iProp Σ)  :
     ↑N⊆E ->
     {{{ is_counter (L:=L) N c γ1 ∗
-        state_update E ∅
+        |={E,∅}=>
           (∃ ε (ε2 : fin 4%nat -> R),
               ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
               ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
-              (∀ n, ↯ (ε2 n) -∗ state_update ∅ E
+              (∀ 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)))
 
@@ -169,7 +169,7 @@ Section lemmas.
                with "[-HΦ]").
     - done.
     - iSplit; first done.
-      iApply state_update_mask_intro; first set_solver.
+      iApply fupd_mask_intro; first set_solver.
       iIntros "Hclose".
       iFrame.
       iExists (λ x, ε2 (fin_to_nat x)); repeat iSplit; try done.