prove a reasonable spec of the interface

logsem · Sep 10, 2024 · 200e794 · 200e794
1 parent c1bb2b1
commit 200e794
Showing 1 changed file with 11 additions and 3 deletions.
diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v
@@ -197,8 +197,16 @@ Section lemmas.
           naive_solver. }
         iPureIntro. split; first lia.
         apply leb_complete in H. lia.
-      + admit.
-    - admit.
-  Admitted.
+      + iModIntro.
+        iIntros (??) "[(%&Herr & Hcontent) Hcontent_auth]".
+        iFrame.
+        iDestruct (counter_content_less_than with "[$][$]") as "%".
+        by iMod (counter_content_update with "[$][$]") as "[$ $]".
+    - iIntros (??) "[(%&%&?&?)?]".
+      iApply "HΦ".
+      iFrame.
+      rewrite /ε2'. case_match eqn: H2; first by iFrame.
+      apply leb_iff_conv in H2. lia.
+  Qed.
 
 End lemmas.