separete vcg_solver from vcgen, to avoid waiting for vcgen to compile.

_CoqProject

@@ -14,6 +14,7 @@ theories/vcgen/dcexpr.v
 theories/vcgen/denv.v
 theories/vcgen/splitenv.v
 theories/vcgen/vcgen.v
+theories/vcgen/vcg_solver.v
 theories/vcgen/tests/basics.v
 theories/vcgen/tests/unknowns.v
 theories/vcgen/tests/test.v

theories/vcgen/tests/basics.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 vcgen.
+From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
 From iris_c.c_translation Require Import monad translation proofmode notation.
 From iris_c.lib Require Import locking_heap U.
 

theories/vcgen/tests/swap.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 vcgen.
+From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
 From iris_c.c_translation Require Import monad translation proofmode.
 From iris_c.lib Require Import locking_heap U.
 

theories/vcgen/tests/test.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 vcgen.
+From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
 From iris_c.c_translation Require Import monad translation proofmode.
 From iris_c.lib Require Import locking_heap U.
 

theories/vcgen/tests/unknowns.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 vcgen.
+From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
 From iris_c.c_translation Require Import monad translation proofmode notation.
 From iris_c.lib Require Import locking_heap U.
 
@@ -9,7 +9,21 @@ Section tests_vcg.
   Context `{amonadG Σ}.
 
 
-  Lemma test4 (l k : loc) (e: expr) `{Closed [] e}:
+  Lemma test0 (l : loc) (e: expr) `{Closed [] e}:
+    l ↦C #1 -∗  awp e True (λ _, True) -∗ awp  (e ;ᶜ ∗ᶜ ♯l) True (λ v, l ↦C #1).
+  Proof.
+    iIntros "Hl Hawp". vcg_solver. simpl. iIntros "Hk".
+    iApply (awp_wand with "Hawp"). iIntros (v ?).
+    (* this part should be automated *)
+    iExists [l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 1)))].
+    iExists (dValUnknown v).
+    iSplit; [done|]. iSplit; [done|].
+    iFrame "Hk"; iSplitR; first done.
+    simpl. iIntros "!> Hl". done.
+  Qed.
+
+
+  Lemma test1 (l k : loc) (e: expr) `{Closed [] e}:
     □ (∀ Φ v, k ↦C v -∗ (k ↦C #12 -∗ Φ v) -∗ awp e True Φ) -∗
     l ↦C #1 -∗
     k ↦C #10 -∗
@@ -20,8 +34,10 @@ Section tests_vcg.
   Proof.
     iIntros "#He Hl Hk". vcg_solver.
     iIntros "Hk". iApply ("He" with "Hk"); iIntros "Hk".
+    (* this part should be automated *)
     iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)))].
-    iExists (dLitV (dLitInt 10)). iSplit; [done|]. iSplit; [done|].
+    iExists (dLitV (dLitInt 10)).
+    iSplit; [done|]. iSplit; [done|].
     iFrame "Hk"; iSplitR; first done.
     simpl. iIntros "!> Hk Hl".
     iApply ("He" with "Hk"); iIntros "Hk".
@@ -32,13 +48,13 @@ Section tests_vcg.
     simpl. auto.
   Qed.
 
-  Lemma test5 (k : loc) :
+
+  Lemma test3 (k : loc) :
     k ↦C #10 -∗  awp (allocᶜ ♯11 =ᶜ ∗ᶜ♯k +ᶜ ♯2) True (λ v, True).
   Proof.
     iIntros "Hk". vcg_solver.
     iIntros "Hk".
-    iApply a_alloc_spec.
-    iApply awp_ret. iApply wp_value.
+    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)))],

theories/vcgen/vcg_solver.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 vcgen.
+From iris_c.c_translation Require Import monad translation proofmode notation.
+From iris_c.lib Require Import locking_heap U.
+
+Arguments vcg_wp_unknown : simpl never.
+(* TODO: How to avoid computing mapsto_wand and dloc under vcg_wp_unknown ? *)
+(* Arguments dloc_interp : simpl never. *)
+Declare Reduction vcg_cbv := cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load mapsto_wand_list].
+
+Ltac vcg_compute :=
+  match goal with
+    |- ?u => let v := eval vcg_cbv in u in change v
+  end.
+
+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.

theories/vcgen/vcgen.v

@@ -692,21 +692,3 @@ Section vcg_spec.
     rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
    Qed.
 End vcg_spec.
-
-Declare Reduction vcg_cbv :=
-  cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load mapsto_wand_list vcg_wp_unknown].
-
-Ltac vcg_compute :=
-  match goal with
-    |- ?u => let v := eval vcg_cbv in u in change v
-  end.
-
-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.