Random stuff.

theories/vcgen/dcexpr.v

@@ -222,20 +222,30 @@ Global Instance base_lit_quote_default E l :
   BaseLitQuote E l (dLitUnknown l) | 1000.
 Proof. done. Qed.
 
+(** ExprIntoDVal *)
+Class ExprIntoDVal (E : known_locs) (e : expr) (dv : dval) :=
+  expr_into_dval : e = of_val (dval_interp E dv).
+
+Global Instance expr_into_dval_loc E l dl :
+  BaseLitQuote E l dl → ExprIntoDVal E (Lit l) (dLitV dl).
+Proof. by rewrite /BaseLitQuote /ExprIntoDVal=> ->. Qed.
+
+Global Instance expr_into_dval_default E e v :
+  IntoVal e v → ExprIntoDVal E e (dValUnknown v) | 1000.
+Proof. by intros <-. Qed.
+
 (** IntoDVal *)
-Class IntoDVal (E : known_locs) (e : expr) (dv : dval) :=
-  into_dval : e = of_val (dval_interp E dv).
+Class IntoDVal (E : known_locs) (v : val) (dv : dval) :=
+  into_dval : v = dval_interp E dv.
 
 Global Instance into_dval_loc E l dl :
-  BaseLitQuote E l dl → IntoDVal E (Lit l) (dLitV dl).
+  BaseLitQuote E l dl → IntoDVal E (LitV l) (dLitV dl).
 Proof. by rewrite /BaseLitQuote /IntoDVal=> ->. Qed.
 
-Global Instance into_dval_default E e v :
-  IntoVal e v → IntoDVal E e (dValUnknown v) | 1000.
-Proof. by intros <-. Qed.
+Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
+Proof. done. Qed.
 
 (** DCexpr *)
-
 Inductive dcexpr : Type :=
   | dCRet  : dval → dcexpr
   | dCAlloc : dcexpr → dcexpr
@@ -361,7 +371,7 @@ Class IntoDCexpr (E: known_locs) (e: expr) (de: dcexpr) :=
   into_dcexpr : e = dcexpr_interp E de.
 
 Global Instance into_dcexpr_ret E v dv:
-  IntoDVal E v dv →
+  ExprIntoDVal E v dv →
   IntoDCexpr E (a_ret v) (dCRet dv).
 Proof. by rewrite /IntoDCexpr=> ->. Qed.
 

theories/vcgen/tests/basics.v

@@ -11,7 +11,7 @@ Section test.
   Lemma test1 (l : loc) (v: val) :
     l ↦C v -∗ awp (∗ᶜ ♯l) True (λ w, ⌜w = v⌝ ∗ l ↦C v).
   Proof.
-    iIntros "Hl1". vcg_solver.
+    iIntros "Hl1". vcg_solver. auto.
    Qed.
 
   (* double dereferencing *)
@@ -19,19 +19,19 @@ Section test.
     l1 ↦C #l2 -∗ l2 ↦C v -∗
     awp ( ∗ᶜ ∗ᶜ ♯l1) True (λ v, ⌜v = #1⌝ ∗ l1 ↦C #l2 -∗ l2 ↦C v).
   Proof.
-    iIntros "Hl1 Hl2". vcg_solver.
+    iIntros "Hl1 Hl2". vcg_solver. auto.
   Qed.
 
   Lemma test3 (l : loc) (v: val) :
     l ↦C v -∗ awp (∗ᶜ ♯l ;ᶜ ∗ᶜ ♯l) True (λ w, ⌜w = v⌝ ∗ l ↦C v).
   Proof.
-    iIntros "Hl1". vcg_solver. iModIntro. eauto.
+    iIntros "Hl1". vcg_solver. auto.
   Qed.
 
   Lemma test4 (l : loc) (v1 v2: val) :
     l ↦C v1 -∗ awp ( ♯l =ᶜ ret v2) True (λ v, ⌜v = v2⌝ ∗ l ↦C[LLvl] v2).
   Proof.
-    iIntros "Hl1". vcg_solver.
+    iIntros "Hl1". vcg_solver. auto.
   Qed.
 
   (* double dereferencing & modification *)
@@ -41,7 +41,6 @@ Section test.
     awp ( ♯l1 =ᶜ ♯r1 ;ᶜ ∗ᶜ ∗ᶜ ♯l1 ) True
       (λ w, ⌜w = v2⌝ ∗ l1 ↦C #r2 ∗ l2 ↦C v1 ∗ r1 ↦C #r2 -∗ r2 ↦C v2).
   Proof.
-    iIntros "Hl1 Hl2 Hr1 Hr2". vcg_solver. iModIntro. eauto.
+    iIntros "**". vcg_solver. auto.
   Qed.
-
-End test.
\ No newline at end of file
+End test.

theories/vcgen/tests/fact.v

@@ -30,7 +30,7 @@ Section factorial_spec.
     l ↦C #n -∗ (l ↦C[LLvl] #(n+1) -∗ Φ #(n+1)) -∗
     awp (incr #l) R Φ.
   Proof.
-    iIntros "Hl HΦ". awp_lam. vcg_solver.
+    iIntros "Hl HΦ". awp_lam. vcg_solver. auto.
    Qed.
 
   Lemma factorial_body_spec (n k : nat) (c r: loc) R :

theories/vcgen/tests/unknowns.v

@@ -8,7 +8,6 @@ From iris_c.lib Require Import locking_heap U.
 Section tests_vcg.
   Context `{amonadG Σ}.
 
-
   Lemma test1 (l k : loc) (e: expr) `{Closed [] e}:
     □ (∀ Φ v, k ↦C v -∗ (k ↦C #12 -∗ Φ v) -∗ awp e True Φ) -∗
     l ↦C #1 -∗
@@ -20,8 +19,7 @@ Section tests_vcg.
   Proof.
     iIntros "#He Hl Hk". vcg_solver.
     iIntros "Hk". iApply ("He" with "Hk"); iIntros "Hk".
-    vcg_continue.
-    iIntros "!> Hk Hl".
+    vcg_continue. iIntros "!> Hk Hl".
     iApply ("He" with "Hk"); iIntros "Hk".
     vcg_continue. eauto.
   Qed.
@@ -30,10 +28,8 @@ 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. vcg_solver. iIntros "Hk" (l) "Hl".
+    vcg_continue. eauto 42 with iFrame.
   Qed.
 
   (*

theories/vcgen/vcg_solver.v

@@ -28,39 +28,60 @@ Section vcg_continue.
     FromKnownLocs (PenvItem l x q v :: Γls) E_old (l :: E_new) | 100.
   Proof. done. Qed.
 
-  Lemma tac_exists_known_locs Γs_in Γs_out Γls Γp c ps v E_old E_new (Φ: known_locs → denv → dval → iProp Σ):
+  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
+    MapstoListFromEnv Γs_in Γs_out Γls →
+    E = penv_to_known_locs Γls →
+    ListOfMapsto Γls E m →
+    IntoDCexpr E e de →
+    denv_wf (penv_to_known_locs Γls) m →
+    dcexpr_wf E de →
+    envs_entails (Envs Γp Γs_out c)
+      (vcg_wp E m de R (λ E m dv,
+        mapsto_wand_list E m (Φ (dval_interp E dv)))) →
+    envs_entails (Envs Γp Γs_in c) (awp e R Φ).
+  Proof.
+    rewrite /IntoDCexpr /=. intros Hsplit ->.
+    rewrite /ListOfMapsto. intros Hpenv -> Hwf Hmwf Hgoal.
+    eapply tac_envs_split_mapsto; try eassumption.
+    revert Hgoal. rewrite environments.envs_entails_eq.
+    rewrite (vcg_wp_correct R); last done.
+    iIntros (->) "H1 H2".
+    iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
+    iIntros (v). iDestruct 1 as (E' dv m' Hpre) "(% & % & % & Hm & Hwp)".
+    rewrite Hpre.
+    rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
+  Qed.
+
+  Lemma tac_exists_known_locs Γs_in Γs_out Γls Γp c ps v dv E_old E_new (Φ: known_locs → denv → dval → iProp Σ):
     MapstoListFromEnv Γs_in Γs_out Γls →
     FromKnownLocs Γls E_old E_new →
     ListOfMapsto Γls (E_old ++ E_new) ps →
-    envs_entails (Envs Γp Γs_out c)
-                 (⌜denv_wf (E_old ++ E_new) ps⌝ ∧ Φ (E_old ++ E_new) ps (dValUnknown v)) →
-    envs_entails (Envs Γp Γs_in c) (vcg_wp_postcondition E_old Φ v).
+    IntoDVal (E_old ++ E_new) v dv →
+    dval_wf (E_old ++ E_new) dv →
+    denv_wf (E_old ++ E_new) ps →
+    envs_entails (Envs Γp Γs_out c) (Φ (E_old ++ E_new) ps dv) →
+    envs_entails (Envs Γp Γs_in c) (vcg_wp_continuation E_old Φ v).
   Proof.
-     unfold vcg_wp_postcondition.
     intros Hsplit. rewrite /ListOfMapsto environments.envs_entails_eq=> Hexhale.
-    unfold of_envs. simpl. intros HGls Hgoal.
+    unfold of_envs. simpl. intros HGls -> ?? Hgoal.
     rewrite mapsto_list_from_env.
     iIntros "(Hwf & #Hp & Hs & Hls)". iDestruct "Hwf" as %Hwf.
-    iPoseProof (Hgoal with "[Hs]") as "[% H]".
-    { repeat iSplit; eauto.
-      iPureIntro.   split; eauto.
-      + apply Hwf.
-      + apply Hsplit. apply Hwf.
-      + intros i. simpl. destruct (envs_disjoint _ Hwf i) as [Hp | Hp]; simpl in Hp.
-        * by left.
-        * right. by apply Hsplit.
-    }
-    iExists (E_old++E_new), (dValUnknown v), ps. repeat iSplit; eauto using prefix_app_r.
-    iFrame. by iApply HGls.
+    iExists (E_old ++ E_new), dv, ps.
+    repeat iSplit; eauto using prefix_app_r. iSplitL "Hls".
+    { by iApply HGls. }
+    iApply Hgoal. iIntros "{$Hp $Hs} !%". split; eauto.
+    + apply Hwf.
+    + apply Hsplit. apply Hwf.
+    + intros i. simpl. destruct (envs_disjoint _ Hwf i) as [Hp | Hp]; simpl in Hp.
+      * by left.
+      * right. by apply Hsplit.
   Qed.
-
 End vcg_continue.
 
-
-(* Arguments vcg_wp_unknown : simpl never. *)
+Arguments vcg_wp_continuation {_ _ _ _}.
 
 Declare Reduction vcg_cbv :=
-  cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load vcg_wp_unknown mapsto_wand_list].
+  cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load vcg_wp_awp_continuation mapsto_wand_list].
 
 Ltac vcg_compute :=
   match goal with
@@ -71,16 +92,18 @@ Ltac vcg_solver :=
   eapply tac_vcg_sound;
   [ apply _    (*  MapstoListFromEnv Γs_in Γs_out Γls *)
   | compute; reflexivity (*  E = penv_to_known_locs Γls *)
-  |       (* dcexpr_wf E de *)
-  |       (* denv_wf E m *)
   | apply _ (* ListOfMapsto Γls E m *)
   | apply _ (* IntoDCexpr E e dce *)
-  | vcg_compute; simpl ]; intuition.
+  | done  (* dcexpr_wf E de *)
+  | done  (* denv_wf E m *)
+  | vcg_compute; simpl ].
 
 Ltac vcg_continue :=
   eapply tac_exists_known_locs;
   [ apply _  (* MapstoListFromEnv Γs_in Γs_out Γls *)
   | apply _  (* FromKnownLocs Γls E_old E_new *)
   | apply _  (* ListOfMapsto Γls (E_old ++ E_new) ps *)
-  | repeat (iSplit; first done); simpl
-  ].
\ No newline at end of file
+  | apply _  (* IntoDVal (E_old ++ E_new) v dv *)
+  | done
+  | done
+  | vcg_compute; simpl ].