Prove wp_map_make; get further along symbolically executing test case

mit-pdos · Nov 9, 2024 · cf81236 · cf81236
1 parent 84bdb1c
commit cf81236
Show file tree

Hide file tree

Showing 3 changed files with 40 additions and 6 deletions.
diff --git a/new/golang/theory/map.v b/new/golang/theory/map.v
@@ -20,8 +20,7 @@ Local Definition is_map_val (mv : val) (m : gmap K V) : Prop :=
                   else go mv
      | _ => False
      end
-  ) mv
-.
+  ) mv.
 
 Definition own_map_def mptr dq (m : gmap K V) : iProp Σ :=
   ∃ (v : val) ,
@@ -99,6 +98,27 @@ Proof.
       iApply ("IH" with "[//] HΦ").
 Qed.
 
+Lemma wp_map_make :
+  is_comparable_go_type kt = true →
+  {{{ True }}}
+    map.make kt vt #()
+  {{{ mref, RET #mref; mref ↦$ (∅ : gmap K V) }}}.
+Proof.
+  rewrite own_map_unseal.
+  iIntros (??) "_ HΦ".
+  wp_call.
+  iApply wp_alloc_untyped; try done.
+  iNext.
+  iIntros (?) "Hl".
+  replace (LitV l) with #l; last by rewrite to_val_unseal.
+  iApply "HΦ".
+  iFrame. iPureIntro.
+  split; first done.
+  unfold is_map_val.
+  intros ?.
+  by rewrite default_val_eq_zero_val.
+Qed.
+
 End defns_and_lemmas.
 
 Notation "mref ↦$ dq m" := (own_map mref dq m)

diff --git a/new/golang/theory/slice.v b/new/golang/theory/slice.v
@@ -370,15 +370,15 @@ Proof.
 Qed.
 
 Lemma wp_slice_for_range {stk E} sl dq (vs : list V) (body : val) Φ :
-  sl ↦*{dq} vs ∗
+  sl ↦*{dq} vs -∗
   (fold_right (λ v P (i : w64),
                  WP body #i #v @ stk ; E {{ v', ⌜ v' = execute_val #()%V ⌝ ∗ P (word.add i 1) }})
     (λ (_ : w64), sl ↦*{dq} vs -∗ Φ (execute_val #()))
     vs) (W64 0) -∗
   WP slice.for_range t #sl body @ stk ; E {{ Φ }}
 .
 Proof.
-  iIntros "[Hsl HΦ]".
+  iIntros "Hsl HΦ".
   wp_call.
   wp_apply wp_ref_ty.
   iIntros (j_ptr) "Hi".

diff --git a/new/proof/etcdraft.v b/new/proof/etcdraft.v
@@ -190,17 +190,31 @@ Proof.
                                            reduction.pm_reflexivity |
                                  ]); try tc_solve |
 
+                               (* for loading from a slice.elem_ref_f *)
+                               wp_bind (load_ty _ _);
+                               unshelve (eapply tac_wp_load_ty;
+                                         [ eapply points_to_access_slice_elem_ref; shelve |
+                                           iAssumptionCore |
+                                 ]); try tc_solve |
+
                                (* for making progress inside body of for loop control-flow handler *)
                                rewrite [in (Fst (execute_val _))]execute_val_unseal |
+                               unshelve (wp_apply wp_map_make; [done| iIntros (?) "?"]); try tc_solve |
                                wp_call
                       ]).
   Time repeat wp_progress.
   rewrite -H in H0 |- *.
   rewrite length_replicate w64_to_nat_id in H0.
   vm_compute bool_decide.
   Time repeat wp_progress.
-
-  (* FIXME: WP for map.make *)
+  iDestruct select (sl ↦* _) as "Hsl".
+  (* FIXME: want to match syntax of expr first, then solve goal. *)
+  wp_apply (wp_slice_for_range with "[$Hsl]").
+  simpl.
+  Time repeat wp_progress.
+  wp_pure.
+  (* FIXME: need to make interfaceT comparable *)
+  Show Ltac Profile.
 Admitted.
 
 Lemma wp_testLeaderElection2 :