Clean up dcexpr and make well-formedness part of the reification

theories/vcgen/dcexpr.v

@@ -189,62 +189,6 @@ Proof.
       destruct b; by inversion 1.
 Qed.
 
-(** ** LocLookup *)
-Class LocLookup (E : known_locs) (l : loc) (i : nat) :=
-  loc_lookup : E !! i = Some l.
-
-Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
-Proof. done. Qed.
-
-Global Instance loc_lookup_there l l' E i :
-  LocLookup E l i → LocLookup (l' :: E) l (S i).
-Proof. done. Qed.
-
-(** ** BaseLitQuote *)
-Class BaseLitQuote (E : known_locs) (l : base_lit) (dl : dbase_lit) :=
-  base_lit_quote : l = dbase_lit_interp E dl.
-
-(** BaseLitQuote for locs *)
-Global Instance base_lit_quote_loc E l i :
-  LocLookup E l i → BaseLitQuote E (LitLoc l) (dLitLoc (dLoc i)) | 1.
-Proof. by rewrite /LocLookup /BaseLitQuote /= => ->. Qed.
-
-Global Instance base_lit_quote_loc_unknown E l :
-  BaseLitQuote E (LitLoc l) (dLitLoc (dLocUnknown l)) | 10.
-Proof. done. Qed.
-
-(** BaseLitQuote for constants *)
-Global Instance base_lit_quote_int E i :
-  BaseLitQuote E (LitInt i) (dLitInt i).
-Proof. by rewrite /BaseLitQuote /=. Qed.
-
-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) (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 (LitV l) (dLitV dl).
-Proof. by rewrite /BaseLitQuote /IntoDVal=> ->. Qed.
-
-Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
-Proof. done. Qed.
-
 (** DCexpr *)
 Inductive dcexpr : Type :=
   | dCRet  : dval → dcexpr
@@ -328,10 +272,11 @@ Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw:
   dbin_op_eval E op dv1 dv2 = dSome dw → dval_wf E dw.
 Proof. destruct op, dv1,dv2; simpl; repeat case_match; intros; simplify_eq/=; done. Qed.
 
-Lemma dbin_op_eval_dUnknown_wf E dv1 dv2 op w:
-  dval_wf E dv1 →  dval_wf E dv2 →
-  dbin_op_eval E op dv1 dv2 = dUnknown (Some w) → dval_wf E w.
-Proof. Admitted.
+(* DF: we don't use it anywhere *)
+(* Lemma dbin_op_eval_dUnknown_wf E dv1 dv2 op w: *)
+(*   dval_wf E dv1 →  dval_wf E dv2 → *)
+(*   dbin_op_eval E op dv1 dv2 = dUnknown (Some w) → dval_wf E w. *)
+(* Proof. Admitted. *)
 
 (** / Well-foundness of dcexpr w.r.t. known_locs *)
 
@@ -367,47 +312,118 @@ Qed.
 Global Instance dcexpr_closed E de : Closed [] (dcexpr_interp E de).
 Proof. induction de; simpl; solve_closed. Qed.
 
+(** * Reification of C syntax *)
+(** ** LocLookup *)
+Class LocLookup (E : known_locs) (l : loc) (i : nat) :=
+  loc_lookup : E !! i = Some l.
+
+Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
+Proof. done. Qed.
+
+Global Instance loc_lookup_there l l' E i :
+  LocLookup E l i → LocLookup (l' :: E) l (S i).
+Proof. done. Qed.
+
+(** ** BaseLitQuote *)
+Class BaseLitQuote (E : known_locs) (l : base_lit) (dl : dbase_lit) :=
+  { base_lit_quote : l = dbase_lit_interp E dl;
+    base_lit_quote_wf : dval_wf E (dLitV dl) }.
+
+(** BaseLitQuote for locs *)
+Global Instance base_lit_quote_loc E l i :
+  LocLookup E l i → BaseLitQuote E (LitLoc l) (dLitLoc (dLoc i)) | 1.
+Proof.
+  rewrite /LocLookup=>Hi.
+  split; rewrite /= ?Hi //.
+Qed.
+
+Global Instance base_lit_quote_loc_unknown E l :
+  BaseLitQuote E (LitLoc l) (dLitLoc (dLocUnknown l)) | 10.
+Proof. done. Qed.
+
+(** BaseLitQuote for constants *)
+Global Instance base_lit_quote_int E i :
+  BaseLitQuote E (LitInt i) (dLitInt i).
+Proof. split; eauto. Qed.
+
+Global Instance base_lit_quote_default E l :
+  BaseLitQuote E l (dLitUnknown l) | 1000.
+Proof. split; eauto. Qed.
+
+(** ** ExprIntoDVal *)
+Class ExprIntoDVal (E : known_locs) (e : expr) (dv : dval) :=
+  { expr_into_dval : e = of_val (dval_interp E dv);
+    expr_into_dval_wf : dval_wf E dv }.
+
+Global Instance expr_into_dval_loc E l dl :
+  BaseLitQuote E l dl → ExprIntoDVal E (Lit l) (dLitV dl).
+Proof.
+  intros ?; split; simpl; eauto using base_lit_quote_wf.
+  rewrite -base_lit_quote //.
+Qed.
+
+Global Instance expr_into_dval_default E e v :
+  IntoVal e v → ExprIntoDVal E e (dValUnknown v) | 1000.
+Proof. done. Qed.
+
+(** ** IntoDVal *)
+Class IntoDVal (E : known_locs) (v : val) (dv : dval) :=
+  { into_dval : v = dval_interp E dv;
+    into_dval_wf : dval_wf E dv }.
+
+Global Instance into_dval_loc E l dl :
+  BaseLitQuote E l dl → IntoDVal E (LitV l) (dLitV dl).
+Proof.
+  intros ?; split; simpl; eauto using base_lit_quote_wf.
+  rewrite -base_lit_quote //.
+Qed.
+
+Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
+Proof. done. Qed.
+
+(** ** IntoDCexpr *)
 Class IntoDCexpr (E: known_locs) (e: expr) (de: dcexpr) :=
-  into_dcexpr : e = dcexpr_interp E de.
+  { into_dcexpr : e = dcexpr_interp E de;
+    into_dcexpr_wf : dcexpr_wf E de }.
 
 Global Instance into_dcexpr_ret E v dv:
   ExprIntoDVal E v dv →
   IntoDCexpr E (a_ret v) (dCRet dv).
-Proof. by rewrite /IntoDCexpr=> ->. Qed.
+Proof. intros [-> ?]; split; auto. Qed.
 
 Global Instance into_dcexpr_alloc E e de:
   IntoDCexpr E e de →
   IntoDCexpr E (a_alloc e) (dCAlloc de).
-Proof. by rewrite /IntoDCexpr=> ->. Qed.
+Proof. intros [-> ?]; split; auto. Qed.
 
 Global Instance into_dcexpr_load E e de:
   IntoDCexpr E e de →
   IntoDCexpr E (a_load e) (dCLoad de).
-Proof. by rewrite /IntoDCexpr=> ->. Qed.
+Proof. intros [-> ?]; split; auto. Qed.
 
 Global Instance into_dcexpr_store E e1 e2 de1 de2:
   IntoDCexpr E e1 de1 →
   IntoDCexpr E e2 de2 →
   IntoDCexpr E (a_store e1 e2) (dCStore de1 de2).
-Proof. by rewrite /IntoDCexpr=> -> ->. Qed.
+Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
 
 Global Instance into_dcexpr_binop E e1 e2 op de1 de2:
   IntoDCexpr E e1 de1 →
   IntoDCexpr E e2 de2 →
   IntoDCexpr E (a_bin_op op e1 e2) (dCBinOp op de1 de2).
-Proof. by rewrite /IntoDCexpr=> -> ->. Qed.
+Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
 
 Global Instance into_dcexpr_unop E e op de:
   IntoDCexpr E e de →
   IntoDCexpr E (a_un_op op e) (dCUnOp op de).
-Proof. by rewrite /IntoDCexpr=> ->. Qed.
+Proof. intros [-> ?]; split; auto. Qed.
 
 Global Instance into_dcexpr_sequence E e1 e2 de1 de2:
   IntoDCexpr E e1 de1 →
   IntoDCexpr E e2 de2 →
   IntoDCexpr E (e1 ;ᶜ e2) (dCSeq de1 de2).
-Proof. by rewrite /IntoDCexpr=> -> ->. Qed.
+Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
 
 Global Instance into_dcexpr_unknown E e `{Closed [] e}:
   IntoDCexpr E e (dCUnknown e) | 100.
-Proof. by rewrite /IntoDCexpr. Qed.
+Proof. done. Qed.

theories/vcgen/splitenv.v

@@ -58,7 +58,7 @@ Section splitenv.
     ListOfMapsto (PenvItem l x q (LitV lit) :: Γls) E
                  (denv_insert i x q (dLitV dlit) ps).
   Proof.
-    rewrite /BaseLitQuote /LocLookup => Hlit Hi.
+    rewrite /LocLookup => [[Hlit ?] Hi].
     rewrite /ListOfMapsto => HΓls /=.
     iDestruct 1 as "[Hl H]". cbn.
     rewrite Hlit. unfold penv_interp in *. rewrite HΓls.
@@ -71,7 +71,7 @@ Section splitenv.
     ListOfMapsto (PenvItem l x q v :: Γls) E
                  (denv_insert i x q (dValUnknown v) ps) | 100.
   Proof.
-    rewrite /BaseLitQuote /LocLookup => Hi.
+    rewrite /LocLookup => Hi.
     rewrite /ListOfMapsto => HΓls /=.
     iDestruct 1 as "[Hl H]". cbn.
     unfold penv_interp in *. rewrite HΓls.
@@ -99,3 +99,4 @@ Section splitenv.
     - by iApply Hexhale.
   Qed.
 End splitenv.
+

theories/vcgen/tests/unknowns.v

@@ -25,38 +25,28 @@ Section tests_vcg.
   Qed.
 
   Lemma test2 (k : loc) :
-    k ↦C #10 -∗  awp (allocᶜ ♯11 =ᶜ ∗ᶜ♯k +ᶜ ♯2) True (λ v, True).
+    k ↦C #10 -∗  awp (allocᶜ ♯11 =ᶜ ∗ᶜ♯k +ᶜ ♯2) True (λ v, ⌜v = #12⌝).
   Proof.
     iIntros "Hk". vcg_solver.
     iIntros "Hk". iApply a_alloc_spec. vcg_solver. iIntros "Hk" (l) "Hl".
     vcg_continue. eauto 42 with iFrame.
   Qed.
 
-  (*
+  
   Lemma test6 (l k : loc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
     (∀ Φ, Φ #11 -∗ awp e1 True Φ) -∗
     (∀ Φ, Φ #12 -∗ awp e2 True Φ) -∗
     l ↦C #1 -∗
     k ↦C #1 -∗
-    awp (a_bin_op PlusOp
-          (a_store (a_ret #l) (a_ret #2))
-          (a_store (a_ret #k) e1 ;ᶜ e2)) True (λ v, l ↦C[LLvl] #2 ∗ k ↦C #11).
+    AWP (♯l =ᶜ ♯2) +ᶜ (♯k =ᶜ e1;ᶜ e2)
+        {{ v, l ↦C[LLvl] #2 ∗ k ↦C #11 ∧ ⌜v = #14⌝ }}.
   Proof.
     iIntros "He1 He2 Hl Hk". vcg_solver.
     iIntros "Hk".
     iApply "He1".
-    (* Now we need some way to mechanically continue *)
-    iApply (optimize_sound [] with "[-]");
-      [iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
-    (* This stuff should happen automagically *)
-    iExists _. iFrame "Hk".
-    iApply (optimize_sound [] with "[-]");
-      [iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
-    iIntros "?".
+    vcg_continue. iModIntro. iIntros "Hk".
     iApply "He2".
-    iApply (optimize_sound [] with "[-]");
-      [iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
-    iExists (dValUnknown (#14)). eauto with iFrame.
+    vcg_continue. iIntros "Hk Hl". eauto with iFrame.
   Qed.
-*)
+
 End tests_vcg.

theories/vcgen/vcg_solver.v

@@ -34,14 +34,13 @@ Section vcg_continue.
     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.
+    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.
@@ -57,13 +56,12 @@ Section vcg_continue.
     FromKnownLocs Γls E_old E_new →
     ListOfMapsto Γls (E_old ++ E_new) ps →
     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.
     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.
     iExists (E_old ++ E_new), dv, ps.
@@ -90,12 +88,11 @@ Ltac vcg_compute :=
 
 Ltac vcg_solver :=
   eapply tac_vcg_sound;
-  [ apply _    (*  MapstoListFromEnv Γs_in Γs_out Γls *)
-  | compute; reflexivity (*  E = penv_to_known_locs Γls *)
-  | apply _ (* ListOfMapsto Γls E m *)
-  | apply _ (* IntoDCexpr E e dce *)
-  | done  (* dcexpr_wf E de *)
-  | done  (* denv_wf E m *)
+  [ apply _              (* Separate the - ↦ - propositions out of the context*)
+  | compute; reflexivity (* Compute the known locations *)
+  | apply _              (* Compute the symbolic environment based on known locations *)
+  | apply _              (* Reify the expression *)
+  | done                 (* Prove that the environment is well-formed  *)
   | vcg_compute; simpl ].
 
 Ltac vcg_continue :=
@@ -104,6 +101,5 @@ Ltac vcg_continue :=
   | apply _  (* FromKnownLocs Γls E_old E_new *)
   | apply _  (* ListOfMapsto Γls (E_old ++ E_new) ps *)
   | apply _  (* IntoDVal (E_old ++ E_new) v dv *)
-  | done
-  | done
+  | done     (* ps is well-formed *)
   | vcg_compute; simpl ].

theories/vcgen/vcgen.v

 From iris.heap_lang Require Export proofmode notation.
 From iris.algebra Require Import frac.
 From iris.bi Require Import big_op.
-From iris_c.vcgen Require Import dcexpr splitenv denv.
+From iris_c.vcgen Require Import dcexpr denv.
 From iris_c.c_translation Require Import monad translation proofmode.
 From iris_c.lib Require Import locking_heap U.