Oops etcdraft; checkpoint auditor.v

mit-pdos · Nov 15, 2024 · 575b4fe · 575b4fe
1 parent 0dc6632
commit 575b4fe
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 3 deletions.
diff --git a/new/proof/etcdraft.v b/new/proof/etcdraft.v
@@ -217,8 +217,7 @@ Proof.
   wp_pure.
   (* FIXME: need to make interfaceT comparable *)
   Show Ltac Profile.
-  destruct false_axiom.
-Qed.
+Admitted.
 
 Lemma wp_testLeaderElection2 :
   {{{ True }}}

diff --git a/src/program_proof/pav/auditor.v b/src/program_proof/pav/auditor.v
@@ -178,7 +178,29 @@ Proof.
   { done. }
   iIntros (?) "Hl".
   wp_pures.
-  wp_apply (wp_MapIter_fold _ _ _ _ with "[$]").
+  wp_apply (wp_MapIter_fold _ _ _ (λ _,
+                                     _
+              )%I with "[$] [-HΦ]").
+  { iNamedAccu. }
+  {
+    iIntros "* !# * [Hpre %Hlookup] HΦ".
+    iNamed "Hpre".
+    wp_pures.
+    wp_apply wp_StringToBytes.
+    iIntros "* ?".
+    iDestruct (own_slice_to_small with "[$]") as "?".
+    (* XXX: checkOneUpd only called here so inlining a proof. *)
+    wp_rec.
+    wp_pures.
+    wp_loadField.
+    wp_apply (wp_Tree_Get with "[$]").
+    iIntros "* HGetPost".
+    iNamed "HGetPost".
+    iNamed "Hreply".
+    wp_pures.
+    wp_loadField.
+    admit.
+  }
 Admitted.
 
 Lemma wp_Auditor__Get a (epoch : u64) :