Finish improvements to tutorial/kvservice/proof.v

mit-pdos · Nov 22, 2024 · fbb36a6 · fbb36a6
1 parent 5979dff
commit fbb36a6
Show file tree

Hide file tree

Showing 5 changed files with 242 additions and 473 deletions.
diff --git a/src/ShouldBuild.v b/src/ShouldBuild.v
@@ -99,7 +99,7 @@ From Perennial.program_proof.tutorial Require
      basics.proof
      queue.proof
      kvservice.proof
-     (* kvservice.full_proof *).
+     kvservice.full_proof.
 
 From Perennial.program_proof.cachekv Require proof.
 

diff --git a/src/program_proof/tutorial/kvservice/bank_proof.v b/src/program_proof/tutorial/kvservice/bank_proof.v
@@ -70,15 +70,13 @@ Proof.
   iIntros (Φ) "(Hlck & #Hln1_islock & #Hln2_islock) Hpost".
   wp_rec.
   wp_pures.
-  destruct bool_decide; wp_pures.
-  {
-    wp_apply (wp_LockClerk__Lock with "[$Hlck $Hln1_islock]").
-    iIntros "[Hlck HP1]".
-    wp_pures.
-    wp_apply (wp_LockClerk__Lock with "[$Hlck $Hln2_islock]").
-    iIntros "[Hlck HP2]".
-    wp_pures.
-    iApply "Hpost". by iFrame.
+  wp_apply (wp_LockClerk__Lock with "[$Hlck]").
+  iIntros "[Hlck HP1]".
+  wp_pures.
+  wp_apply (wp_LockClerk__Lock with "[$Hlck $Hln2_islock]").
+  iIntros "[Hlck HP2]".
+  wp_pures.
+  iApply "Hpost". by iFrame.
   }
   {
     wp_apply (wp_LockClerk__Lock with "[$Hlck $Hln2_islock]").