get rid of vcg_wp for alloc

theories/vcgen/dcexpr.v

@@ -50,12 +50,6 @@ Definition dloc_interp (E : known_locs) (dl : dloc) : loc :=
   | dLocUnknown l => l
   end.
 
-Lemma dloc_interp_lookup_endl E l :
-  l = (dloc_interp (E ++ [l]) (dLoc (length E))).
-Proof.
-  induction E; simplify_eq /=; done.
-Qed.
-
 Definition dbase_lit_interp (E : known_locs) (l : dbase_lit) : base_lit :=
   match l with
   | dLitInt x => LitInt x

theories/vcgen/tests/swap.v

@@ -35,16 +35,8 @@ Definition swap_with_alloc : val := λ: "l1" "l2",
        awp (swap_with_alloc #l1 #l2) R (λ _, l1 ↦C v2 ∗ l2 ↦C v1).
   Proof.
     iIntros "Hl1 Hl2".
-    (* proof WITH calling vcgen on alloc, does not work well :  *)
-    do 2 awp_lam. iApply awp_bind. vcg_solver.
-    (* >>>>>> annoying part *)
-    iIntros (l) "Hl2 Hl1 Hl". awp_lam. vcg_solver.
-    (* <<<<<< annoying part *)
-    iIntros "!> !> !>". eauto with iFrame.
-
-    (* proof WITHOUT calling vcgen on alloc, works well :
-    do 2 awp_lam. iApply awp_bind. vcg_solver. awp_alloc_ret r "Hr".
-    vcg_solver. iIntros "!> !> !>". eauto with iFrame. *)
+    do 2 awp_lam. iApply awp_bind.  awp_alloc_ret r "Hr".
+    vcg_solver. iIntros "!> !> !>". eauto with iFrame.
 
     (* Compared with step-by-step proof *) (*
 

theories/vcgen/tests/unknowns.v

@@ -9,13 +9,6 @@ Section tests_vcg.
   Context `{amonadG Σ}.
 
 
-(*  Lemma test0 (l1 l2 : loc) (e: expr) `{Closed [] e}:
-    l1 ↦C #1 -∗ l2 ↦C #1 -∗  awp e True (λ _, True) -∗
-       awp  (allocᶜ ♯1;ᶜ e ;ᶜ ∗ᶜ ♯l1) True (λ v, l1 ↦C #1 ∗ l2 ↦C #1).
-  Proof.
-    iIntros "Hl1 Hl2 Hawp". vcg_solver.
-    iIntros "Hl2 Hl1". Abort. *)
-
   Lemma test1 (l k : loc) (e: expr) `{Closed [] e}:
     □ (∀ Φ v, k ↦C v -∗ (k ↦C #12 -∗ Φ v) -∗ awp e True Φ) -∗
     l ↦C #1 -∗
@@ -37,9 +30,10 @@ Section tests_vcg.
     k ↦C #10 -∗  awp (allocᶜ ♯11 =ᶜ ∗ᶜ♯k +ᶜ ♯2) True (λ v, True).
   Proof.
     iIntros "Hk". vcg_solver.
-(*    iIntros "Hk". iApply a_alloc_spec. awp_ret_value.
-    iIntros  (l) "Hl". vcg_continue.
-    eauto 42 with iFrame. *)
+    iIntros "Hk". iApply a_alloc_spec. awp_ret_value.
+    iIntros (l) "Hl".
+    vcg_continue.
+    eauto 42 with iFrame.
   Qed.
 
   (*

theories/vcgen/vcg_solver.v

@@ -60,7 +60,7 @@ End vcg_continue.
 (* Arguments vcg_wp_unknown : simpl never. *)
 
 Declare Reduction vcg_cbv :=
-  cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load  mapsto_wand_list].
+  cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load vcg_wp_unknown mapsto_wand_list].
 
 Ltac vcg_compute :=
   match goal with

theories/vcgen/vcgen.v

@@ -196,9 +196,6 @@ Section vcg.
     | dCSeq de1 de2 =>
        vcg_wp E m de1 R (λ E m _,
          U (vcg_wp E (denv_unlock m) de2 R Φ))
-    | dCAlloc de =>
-      vcg_wp E m de R (λ E m' dv,
-         ∀ l : loc, Φ (E++[l]) (denv_insert (length E) ULvl 1 dv m')  (dLitV $ dLitLoc (dLoc (length E))))
     | _ => vcg_wp_unknown R E de m Φ
     end%I.
 End vcg.
@@ -577,25 +574,7 @@ Section vcg_spec.
     revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
     - iApply awp_ret. wp_value_head.
       iExists E, d, m. iSplit; first done; by iFrame.
-    -  rewrite IHde //. iRename "Hm" into "Hawp".
-       iSpecialize ("Hawp" with "Hwp"); simpl.
-       iApply a_alloc_spec. iApply (awp_wand with "Hawp").
-       iIntros (v) "Hpost". iDestruct "Hpost" as (E' dv m' -> Hwf0 Hm'wf Hwf2) "(Hm & Hwp)".
-       iIntros (l) "Hl". iSpecialize ("Hwp" $! l).
-       unfold vcg_wp_postcondition.
-       iExists (E' ++ [l]), (dLitV (dLitLoc (dLoc (length E')))), (denv_insert (length E') ULvl 1 dv m').
-       iSplit. iPureIntro. compute[dval_interp dbase_lit_interp]. do 2 f_equal.
-       apply (dloc_interp_lookup_endl E' l).
-       iSplit. iPureIntro. trans E'; first done. by apply prefix_app_r.
-       iSplit. iPureIntro. by apply denv_wf_extend.
-       iSplit. iPureIntro. compute[dval_wf].
-       case_bool_decide; first done. apply H0. apply lookup_lt_is_Some_2.
-       rewrite app_length. simpl. lia.
-       iFrame. rewrite -denv_insert_interp.
-       iSplitL "Hm". iApply (denv_interp_mono with "Hm"); first done.
-       trans E'; first done. by apply prefix_app_r.
-       rewrite -(dloc_interp_lookup_endl E' l).
-       rewrite (dval_interp_mono E' (E'++[l])) //. by apply prefix_app_r .
+    - by iApply (vcg_wp_unknown_correct with "Hm Hwp").
     - rewrite IHde //. iRename "Hm" into "Hawp".
       iSpecialize ("Hawp" with "Hwp"); simpl.
       iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp").