nit

logsem · Aug 28, 2024 · 2c66cf7 · 2c66cf7
1 parent 1f2440b
commit 2c66cf7
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 6 deletions.
diff --git a/theories/coneris/examples/random_counter.v b/theories/coneris/examples/random_counter.v
@@ -220,10 +220,8 @@ Section impl1.
     iDestruct "H3" as "[Htape H3]".
     iDestruct (wp_update_presample_exp' E _ _ _ _ (ε2 ε) with "[$]") as "Hupdate"; [intros; naive_solver|naive_solver|].
     (** Here we need to do an update on H4 and Hfrag, but we dont know what to update to???*)
-
-
-    iMod ("Hvs" with "[$HP $H2 $H4 //]") as "Hcont".
-    iModIntro.
+    (** maybe wp_update is the wrong abstraction. 
+        We also need to destruct Hupdate to reestablish the invariant*)
 
 
   Abort.

diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v
@@ -92,7 +92,7 @@ Section wp_update.
   Lemma wp_update_one_inv N E P R R':
     ↑N ⊆ E -> 
     inv N P -∗
-    (▷ P ∗ R ={E∖↑N}=∗ ▷P ∗ wp_update E R') -∗
+    (▷ P ∗ R ={E∖↑N}=∗ ▷P ∗wp_update E R') -∗
     R -∗ wp_update E R'.
   Proof.
     iIntros (?) "#Hinv Hvs HR".
@@ -102,7 +102,7 @@ Section wp_update.
     iMod ("Hvs" with "[$]") as "[HP HR]".
     by iMod ("Hclose" with "[$]").
   Qed.
-
+    
   Global Instance from_modal_wp_update_wp_update P E :
     FromModal True modality_id (wp_update E P) (wp_update E P) P.
   Proof. iIntros (_) "HP /=". by iApply wp_update_ret. Qed.