Random changes.

theories/vcgen/denv.v

@@ -159,6 +159,14 @@ Section denv_spec.
      denv_interp E m' ∗ dloc_interp E (dLoc i) ↦C{1} dval_interp E dv ⊣⊢ denv_interp E m.
    Proof. Admitted.
 
+   Lemma denv_delete_frac_2_interp E i mIn mOut mIn1 mOut1 q dv :
+     denv_delete_frac_2 i mIn mOut = Some (mIn1, mOut1, q, dv) →
+     denv_interp E mIn -∗
+     (denv_interp E mIn1 ∗ (denv_interp E mOut -∗ denv_interp E mOut1 ∗
+       dloc_interp E (dLoc i) ↦C{q} dval_interp E dv)).
+   Proof.
+   Admitted.
+
    Lemma denv_delete_full_2_interp E i mIn mOut mIn1 mOut1 dv :
      denv_delete_full_2 i mIn mOut = Some (mIn1, mOut1, dv) →
      denv_interp E mIn -∗

theories/vcgen/test.v

@@ -8,11 +8,6 @@ From iris_c.lib Require Import locking_heap U.
 Section tests_vcg.
   Context `{amonadG Σ}.
 
-  Definition swap : val := λ: "l1" "l2" "r",
-    (a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
-    (a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
-    (a_store (a_ret "l2") (a_load (a_ret "r"))).
-
   Lemma store_load (s l : loc) R :
     s ↦C #0 -∗ l ↦C #1 -∗
     awp (a_store (a_ret #s) (a_load (a_ret #l))) R (λ _, s ↦C[LLvl] #1 ∗ l ↦C #1).
@@ -37,24 +32,48 @@ Section tests_vcg.
                          (a_store (a_ret #l) (a_ret #2)))%E True (λ v, True).
   Proof. iIntros "Hl". vcg_solver. Abort.
 
-  Lemma test4 (l : loc) (e: expr) `{Closed [] e}:
-    (∀ Φ, Φ #10 -∗ awp e True Φ) -∗
+  Lemma test4 (l k : loc) (e: expr) `{Closed [] e}:
+    □ (∀ Φ v, k ↦C v -∗ (k ↦C #12 -∗ Φ v) -∗ awp e True Φ) -∗
     l ↦C #1 -∗
-    awp (a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2))
-                         e) True (λ v, True).
+    k ↦C #10 -∗
+    awp
+      (a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2)) e;;;;
+      (a_store (a_ret #l) e))
+    True (λ v, True).
   Proof.
-    iIntros "He Hl". vcg_solver.
-    iApply "He".
-    (* Now we need some way to mechanically continue, i.e run the
-    optimizer now. *)
-    (* What I do here is a way to do so, but it's not really right:
-    - We need to reify everything again. New constants or locations could have
-      been introduced like the `#10` in this example.
-    - `simpl` will probably unfold too much, and as such, it does not work in
-      a nested fashion. *)
-    iApply (optimize_sound [] with "[-]");
-      [iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
-    iExists (dValUnknown (#12)). eauto.
+    iIntros "#He Hl Hk". vcg_solver.
+    iIntros "Hk". iApply ("He" with "Hk"); iIntros "Hk".
+    iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)))].
+    iExists (dLitV (dLitInt 10)). iSplit; [done|]. iSplit; [done|].
+    iFrame "Hk"; iSplitR; first done.
+    simpl. iIntros "!> Hk Hl".
+    iApply ("He" with "Hk"); iIntros "Hk".
+    iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)));
+      Some (DenvItem ULvl 1 (dLitV (dLitInt 2)))].
+    iExists (dLitV (dLitInt 12)). iSplit; [done|]. iSplit; [done|].
+    iFrame "Hl Hk". iSplitR; first done.
+    simpl. auto.
+  Qed.
+
+  Lemma test5 (k : loc) :
+    k ↦C #10 -∗
+    awp
+      (a_bin_op PlusOp (a_store (a_alloc (a_ret #11)) (a_load (a_ret #k)))
+                       (a_ret #2))
+    True (λ v, True).
+  Proof.
+    iIntros "Hk". vcg_solver.
+    iIntros "Hk".
+    iApply a_alloc_spec.
+    iApply awp_ret. iApply wp_value.
+    iIntros (l) "Hl".
+    iExists [k;l], [Some (DenvItem ULvl (1/2) (dLitV (dLitInt 10)));
+        Some (DenvItem ULvl 1 (dLitV (dLitInt 11)))],
+      (dLitV (dLitLoc (dLoc 1))).
+    iSplit; first done.
+    iSplit. iPureIntro. apply prefix_cons, prefix_nil.
+    iFrame "Hl Hk". iSplitR; first done.
+    simpl. auto.
   Qed.
 
   Lemma test5 (l k : loc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:

theories/vcgen/tests/swap.v

@@ -14,9 +14,9 @@ Section tests_vcg.
     (a_store (a_ret "l2") (a_load (a_ret "r"))) ;;;;
     (a_ret #0).
 
-  Lemma swap_spec_by_vcg_opt (l1 l2 r : loc) (v1 v2: nat) R :
-    r ↦C #0 -∗ l1 ↦C #1 ∗ l2 ↦C #2 -∗
-    awp (swap #l1 #l2 #r) R (λ _, l2 ↦C #1 ∗ l1 ↦C #2).
+  Lemma swap_spec_by_vcg_opt (l1 l2 r : loc) (v1 v2: val) R :
+    r ↦C #0 -∗ l1 ↦C v1 ∗ l2 ↦C v2 -∗
+    awp (swap #l1 #l2 #r) R (λ _, l2 ↦C v1 ∗ l1 ↦C v2).
   Proof.
     iIntros "Hr [Hl1 Hl2]". do 3 awp_lam.
     vcg_solver. iIntros "!> !> !>". eauto with iFrame.

theories/vcgen/vcgen.v

@@ -5,6 +5,27 @@ From iris_c.vcgen Require Import dcexpr splitenv denv.
 From iris_c.c_translation Require Import monad translation proofmode.
 From iris_c.lib Require Import locking_heap U.
 
+(*
+TODO
+
+- Fix all the unknown cases, introduce a function for that (which should be
+  simpl never)
+- Write more tests with unknown stuff in it
+- Support alloc in `vcg_wp`
+- Automatically come up with the new `E`, `m` and `dv` and stuff in the
+  unknown case
+- Finish the proofs
+- Maybe drop `wp_expr`? We are not taking it as an input of anything anymore
+
+Less urgent TODO
+
+- Symbolic fractions
+- Support bind
+- Support conditional
+- Write examples with R
+- Deal with functions
+*)
+
 (*
 TODO:
 Inductive dfrac :=
@@ -51,7 +72,7 @@ Section vcg.
     | MapstoStar dl Φ =>
        ∃ q v, dloc_interp E dl ↦C{q} v ∗ wp_interp_sane E (Φ q (dValUnknown v))
     | MapstoStarFull dl Φ =>
-       ∃ v, dloc_interp E dl ↦C{1} v ∗ wp_interp E (Φ (dValUnknown v))
+       ∃ v, dloc_interp E dl ↦C{1} v ∗ wp_interp_sane E (Φ (dValUnknown v))
     | MapstoWand dl dv x q Φ =>
        dloc_interp E dl ↦C[x]{q} dval_interp E dv -∗ wp_interp_sane E Φ
     | IsSome dmx Φ  =>
@@ -75,6 +96,9 @@ Section vcg.
   Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
     mapsto_wand_list_aux m Φ O.
 
+  (*
+  TODO: add to tests fine: `!(l := 10;;;; l)`
+  *)
   Fixpoint vcg_sp (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
     match de with
     | dCRet dv    => Some (m, nil, dv)
@@ -109,38 +133,8 @@ Section vcg.
     | dCAlloc _ |  dCUnknown _ => None
     end.
 
-  Fixpoint optimize (m : denv) (Φ : wp_expr) : wp_expr :=
-    match Φ with
-    | Base Φ1 => mapsto_wand_list m (Base Φ1)
-    | MapstoStar (dLoc i) Φ1 =>
-       match denv_delete_frac i m with
-       | Some (m1, q1, dv) => optimize m1 (Φ1 q1 dv)
-       | None => MapstoStar (dLoc i) (λ q dv, optimize m (Φ1 q dv))
-       end
-    | MapstoStarFull (dLoc i) Φ1 =>
-       match denv_delete_full i m with
-       | Some (m1, dv) => optimize m1 (Φ1 dv)
-       | None => MapstoStarFull (dLoc i) (λ dv, optimize m (Φ1 dv))
-       end
-    | MapstoWand (dLoc i) dv x q Φ1 => optimize (denv_insert i x q dv m) Φ1
-    | MapstoStar dl Φ1 =>  MapstoStar dl (λ q dv, optimize m (Φ1 q dv))
-    | MapstoStarFull dl Φ1 => MapstoStarFull dl (λ dv, optimize m (Φ1 dv))
-    | MapstoWand dl w x q Φ1 => MapstoWand dl w x q (optimize m Φ1)
-    | IsSome dmx Φ1 =>
-        match dmx with
-        | dNone => Base False
-        | dSome x => optimize m (Φ1 x)
-        | _ => IsSome dmx (λ v, optimize m (Φ1 v))
-        end
-    | IsLoc dv Φ1 =>
-        match dv with
-        | dLitV (dLitLoc l) => optimize m (Φ1 l)
-        | dLitV (dLitUnknown _) | dValUnknown _ => IsLoc dv (λ v, optimize m (Φ1 v))
-        | _ => Base False
-        end
-    | UMod Φ => optimize (denv_unlock m) Φ
-    end.
-
+  (* TODO: change the fail though cases, in the same way as the unknown case 
+  of vcg_wp. Also factor that out in a function vcg_unknown *)
   Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
       (Φ : denv → dval → wp_expr) : wp_expr :=
     match is_dloc E dv with
@@ -151,7 +145,10 @@ Section vcg.
           mapsto_wand_list m $ MapstoStar (dLoc i) $ λ q dw,
             MapstoWand (dLoc i) dw ULvl q (Φ [] dw)
        end
-    | _ => Base False
+    | _ =>
+       mapsto_wand_list m $ IsLoc dv (λ dl,
+         MapstoStar dl $ λ q dw,
+           MapstoWand dl dw ULvl q (Φ [] dw))
     end.
 
   Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
@@ -164,7 +161,10 @@ Section vcg.
           mapsto_wand_list m $ MapstoStarFull (dLoc i) $ λ _,
             MapstoWand (dLoc i) dv2 LLvl 1 (Φ [] dv2)
        end
-    | _ => Base False
+    | _ =>
+       mapsto_wand_list m $ IsLoc dv1 (λ dl,
+         MapstoStarFull dl $ λ _,
+            MapstoWand dl dv2 LLvl 1 (Φ [] dv2))
     end.
 
   Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval)
@@ -175,53 +175,58 @@ Section vcg.
     end.
 
   Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
-      (R : iProp Σ) (Φ : denv → dval → wp_expr) : wp_expr :=
+      (R : iProp Σ) (Φ : known_locs → denv → dval → wp_expr) : wp_expr :=
     match de with
-    | dCRet dv => Φ m dv
+    | dCRet dv => Φ E m dv
     | dCLoad de1 =>
-       vcg_wp E m de1 R (λ m' dv, vcg_wp_load E dv m Φ)
+       vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m (Φ E))
     | dCStore de1 de2 =>
        match vcg_sp E m de1 with
        | Some (mIn, mOut, dv1) =>
-          vcg_wp E mIn de2 R (λ mIn dv2,
-            vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) Φ)
+          vcg_wp E mIn de2 R (λ E mIn dv2,
+            vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
        | None =>
           match vcg_sp E m de2 with
           | Some (mIn, mOut, dv2) =>
-             vcg_wp E mIn de1 R (λ mIn dv1,
-               vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) Φ)
+             vcg_wp E mIn de1 R (λ E mIn dv1,
+               vcg_wp_store E dv1 dv2 (denv_merge mOut mIn) (Φ E))
           | None =>
              mapsto_wand_list m $ Base $
-               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ [] (dValUnknown v)))
+               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ E [] (dValUnknown v)))
           end
         end
     | dCBinOp op de1 de2 =>
        match vcg_sp E m de1 with
        | Some (mIn, mOut, dv1) =>
-          vcg_wp E mIn de2 R (λ mIn dv2,
-            vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) Φ)
+          vcg_wp E mIn de2 R (λ E mIn dv2,
+            vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
        | None =>
           match vcg_sp E m de2 with
           | Some (mIn, mOut, dv2) =>
-             vcg_wp E mIn de1 R (λ mIn dv1,
-               vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) Φ)
+             vcg_wp E mIn de1 R (λ E mIn dv1,
+               vcg_wp_bin_op E op dv1 dv2 (denv_merge mOut mIn) (Φ E))
           | None =>
              mapsto_wand_list m $ Base $
-               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ [] (dValUnknown v)))
+               awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ E [] (dValUnknown v)))
           end
-        end
+       end
     | dCUnOp op de =>
-       vcg_wp E m de R (λ m dv,
+       vcg_wp E m de R (λ E m dv,
          match dun_op_eval E op dv with
-         | dSome dw => Φ m dw
-         | mdw => IsSome mdw (Φ m)
+         | dSome dw => Φ E m dw
+         | mdw => IsSome mdw (Φ E m)
          end)
     | dCSeq de1 de2 =>
-       vcg_wp E m de1 R (λ m _,
+       vcg_wp E m de1 R (λ E m _,
          UMod (vcg_wp E (denv_unlock m) de2 R Φ))
     | _ =>
        mapsto_wand_list m $ Base $
-         awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ [] (dValUnknown v)))
+         awp (dcexpr_interp E de) R (λ v,
+           ∃ E' m' dv,
+           ⌜ v = dval_interp E' dv ⌝ ∧
+           ⌜ E `prefix_of` E' ⌝ ∧
+           denv_interp E' m' ∗
+           wp_interp_sane E' (Φ E' m' dv))%I
     end.
 End vcg.
 
@@ -358,7 +363,7 @@ Section vcg_spec.
     wp_interp E (vcg_wp E m de R Φ) -∗
     awp (dcexpr_interp E de) R
       (λ v, ∃ dv m', ⌜dval_interp E dv = v⌝ ∧ wp_interp E (Φ m' dv)).
-  Proof.
+  Proof. (*
     revert Φ m. induction de; intros Φ m.
     - iIntros "Hd". iApply awp_ret. wp_value_head. eauto.
     - iIntros "Hawp". iApply (awp_wand with "Hawp"). iIntros (v) "H".
@@ -489,10 +494,12 @@ Section vcg_spec.
       rewrite wp_interp_sane_sound. iExists _,_; iFrame; eauto.
   Qed.
 *)
+  Admitted.
 
   Lemma optimize_sound (m: denv) E (Φ: wp_expr) :
+    denv_interp E m -∗
     wp_interp E (optimize m Φ) -∗
-    denv_interp E m -∗ (wp_interp E Φ).
+    wp_interp E Φ.
   Proof. (*
     generalize dependent m.
     induction Φ; simpl; intros m.
@@ -570,6 +577,7 @@ Section vcg_spec.
       iModIntro. by iApply "HΦ".
   *)
   Admitted.
+*)
 
   Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
     MapstoListFromEnv Γs_in Γs_out Γls →
@@ -577,7 +585,7 @@ Section vcg_spec.
     ListOfMapsto Γls E m →
     IntoDCexpr E e dce →
     environments.envs_entails (environments.Envs Γp Γs_out c)
-      (wp_interp_sane E (vcg_wp E m dce R (λ m dv,
+      (wp_interp_sane E (vcg_wp E m dce R (λ E m dv,
         mapsto_wand_list m $ Base (Φ (dval_interp E dv))))) →
     environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
   Proof.