redefine vcg_sp. Thanks to denv, now vcg_sp looks very nicely and is much more understandable.

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 env splitenv.
+From iris_c.vcgen Require Import dcexpr env splitenv denv.
 From iris_c.c_translation Require Import monad translation proofmode.
 From iris_c.lib Require Import locking_heap U.
 
@@ -86,59 +86,60 @@ Section vcg.
   end%I.
 
 
-  Fixpoint append_exhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr :=
-    match ps with
-    | (i, ((x,q), dv)) :: s' => Exhale (dLoc i) dv x q (append_exhale_list s' Φ)
+  Fixpoint append_exhale_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
+    match m with
     | [] => Φ
+    | dio :: m' =>
+      match dio with
+      | None => append_exhale_list_aux m' Φ (S i)
+      | Some (DenvItem x q dv)  =>
+         Exhale (dLoc i) dv x q (append_exhale_list_aux m' Φ (S i))
+      end
     end.
 
-  Fixpoint append_inhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr :=
-    match ps with
-    | (i, ((x,q), dv)) :: s' => InhaleKnown (dLoc i) dv x q (append_inhale_list s' Φ)
+  Definition append_exhale_list (m : denv) (Φ : wp_expr) := append_exhale_list_aux m Φ O.
+
+  Fixpoint append_inhale_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
+    match m with
     | [] => Φ
+    | dio :: m' =>
+      match dio with
+      | None => append_inhale_list_aux m' Φ (S i)
+      | Some (DenvItem x q dv)  =>
+         InhaleKnown (dLoc i) dv x q (append_inhale_list_aux m' Φ (S i))
+      end
     end.
 
-   (* vcg_sp E s de = Some (s1, s2, dv)
-     - s1 = s / resources for de
-     - s2 = new resources that you get from de
-   *)
-  Fixpoint vcg_sp (E: env_locs) (s: env_ps_dv) (de : dcexpr) :
-    option (env_ps_dv * env_ps_dv * dval) :=
+  Definition append_inhale_list (m : denv) (Φ : wp_expr) := append_inhale_list_aux m Φ O.
+
+  Fixpoint vcg_sp (E: env_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
     match de with
-    | dCVal dv => Some (s, nil, dv)
+    | dCVal dv => Some (m, nil, dv)
     | dCLoad de1 =>
-                ''(s1, s2, dv1) ← vcg_sp E s de1;
-                              i ← is_dloc E dv1;
-         ''(s1', ((x, q), dv2)) ← find_and_remove s1 (dLoc i);
-     if (bool_decide (x = ULvl))
-     then
-         (* NB: 'x' can be a Coq variable, so here we can't check that 'x' is Ulvl *)
-         Some ((i, ((x, (q/2)%Qp), dv2)) :: s1', (i, ((x, (q/2)%Qp), dv2)) :: s2, dv2)
-     else None
+      ''(inh, exh, dl) ← vcg_sp E m de1;
+                     i ← is_dloc E dl;
+       ''(inh1, q, dv) ← denv_inhale_frac i inh;
+       Some (inh1, denv_exhale i ULvl q dv exh, dv)
     | dCStore de1 de2 =>
-               ''(s1, s2, dv1) ← vcg_sp E s de1;
-                             i ← is_dloc E dv1;
-             ''(s1', s2', dv2) ← vcg_sp E s1 de2;
-             (* we can't use s1 below any more *)
-             ''(s1'', s2'', ((x, q), _)) ← find_and_remove_2 s1' (s2 ++ s2') (dLoc i);
-             (* NB: this should be fixed, adding 'q' & 'x' to env *)
-     if (bool_decide (q = Qp_one) && bool_decide (x = ULvl))
-     then Some (s1'', (i, ((LLvl, 1%Qp), dv2)) :: s2'', dv2)
-     else None
+      ''(inh1, exh1, dl) ← vcg_sp E m de1;
+                       i ← is_dloc E dl;
+      ''(inh2, exh2, dv) ← vcg_sp E inh1 de2;
+       ''(inh3, exh3, _) ← denv_inhale_full_2 i inh2 (denv_merge exh1 exh2);
+       Some (inh3, denv_exhale i LLvl 1%Qp dv exh3, dv)
     | dCBinOp op de1 de2 =>
-        ''(s1, s2, dv1) ← vcg_sp E s de1;
-      ''(s1', s2', dv2) ← vcg_sp E s1 de2;
+      ''(inh1, exh1, dv1) ← vcg_sp E m de1;
+      ''(inh2, exh2, dv2) ← vcg_sp E inh1 de2;
       match dbin_op_eval E op dv1 dv2 with
-      | dSome dv => Some (s1', s2 ++ s2', dv)
-      (* | dUnknown (Some dv) => Some (s1', s2 ++ s2', dv) (*TODO: not sure here *)
-         RK: probably just fail with None *)
+      | dSome dv => Some (inh2, denv_merge exh1 exh2, dv)
       | dNone | dUnknown _ => None
+      (* | dUnknown (Some dv) =>  RK: probably just fail with None *)
       end
     end.
 
-  Fixpoint vcg_wp (E: env_locs) (s: env_ps_dv) (de : dcexpr) (R : iProp Σ) (Φ : dval → wp_expr) : wp_expr :=
+
+  Fixpoint vcg_wp (E: env_locs) (m: denv) (de : dcexpr) (R : iProp Σ) (Φ : dval → wp_expr) : wp_expr :=
     match de with
-    | dCVal dv => Φ dv
+  (*  | dCVal dv => Φ dv
     | dCLoad de1 => vcg_wp E s de1 R (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w ULvl 1%Qp (Φ w))))
     | dCBinOp op de1 de2 =>
       match vcg_sp E s de1 with
@@ -146,7 +147,7 @@ Section vcg.
           append_inhale_list s (vcg_wp E s1 de2 R (λ dv2,
             append_exhale_list (s1 ++ s2) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
       | None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
-      end
+      end *)
     | _ => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
     end.
 
@@ -178,32 +179,36 @@ Section vcg_spec.
       iApply ("HΦ" with "Hv1 Hv2").
   Qed.
 
-  Lemma vcg_inhale_list_sound E s t :
-    wp_interp E (append_inhale_list s t) -∗ env_ps_dv_interp E s ∗ wp_interp E t.
+
+  Lemma vcg_inhale_list_sound E m t :
+    wp_interp E (append_inhale_list m t) -∗ denv_interp E m ∗ wp_interp E t.
   Proof.
-    unfold env_ps_dv_interp.
+  Admitted.
+(*    unfold env_ps_dv_interp.
     induction s as [| [i [[x q] w]] s']; simpl.
     - by iIntros "$ _".
     - iIntros "[H1 H2]". iFrame "H1". by iApply (IHs' with "H2").
-  Qed.
+  Qed. *)
 
-  Lemma vcg_exhale_list_sound E s t :
-    wp_interp E (append_exhale_list s t) -∗ env_ps_dv_interp E s -∗ wp_interp E t.
+  Lemma vcg_exhale_list_sound E m t :
+    wp_interp E (append_exhale_list m t) -∗ denv_interp E m -∗ wp_interp E t.
   Proof.
-    unfold env_ps_dv_interp.
+  Admitted.
+  (*  unfold env_ps_dv_interp.
     induction s as [| [i [[x q] w]] s']; simpl.
     - by iIntros "$ _".
     - iIntros "H [H1 H2]".
       iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
-  Qed.
+  Qed. *)
 
-  Lemma vcg_sp_correct E s de ps1 ps2 dv R :
-    vcg_sp E s de = Some (ps1, ps2, dv) →
-    env_ps_dv_interp E s -∗
-      env_ps_dv_interp E ps1 ∗
-      awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ env_ps_dv_interp E ps2).
+  Lemma vcg_sp_correct E m de inh exh dv R :
+    vcg_sp E m de = Some (inh, exh, dv) →
+    denv_interp E m -∗
+      denv_interp E inh ∗
+      awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E exh).
   Proof.
-    revert s ps1 ps2 dv. induction de;
+  Admitted.
+(*    revert s ps1 ps2 dv. induction de;
     iIntros (s ps1 ps2 dv Hsp) "Hs"; simplify_eq/=.
     - iFrame. iApply awp_ret. wp_value_head. iSplit; eauto. unfold env_ps_dv_interp. done.
     - specialize (IHde s).
@@ -257,12 +262,14 @@ Section vcg_spec.
       + iPureIntro. apply dbin_op_eval_correct. rewrite -HeqHboe. reflexivity.
       +  iCombine "Hs2' Hs2''" as "Hs2". iFrame.
   Qed.
+ *)
 
-  Lemma vcg_wp_correct R E s de Φ :
-    wp_interp E (vcg_wp E s de R Φ) ⊢
+  Lemma vcg_wp_correct R E m de Φ :
+    wp_interp E (vcg_wp E m de R Φ) ⊢
     awp (dcexpr_interp E de) R (λ v, ∃ dv, ⌜dval_interp E dv = v ⌝ ∧ wp_interp E (Φ dv)).
   Proof.
-    revert Φ s. induction de; simpl; intros Φ s.
+  Admitted.
+(*    revert Φ s. induction de; simpl; intros Φ s.
     - iIntros "Hd". iApply awp_ret. wp_value_head.
       iExists d. eauto.
     - iIntros "Hd".
@@ -302,15 +309,16 @@ Section vcg_spec.
       iSplit.
       iPureIntro. by apply dbin_op_eval_correct.
       eauto with iFrame.
-  Qed.
+  Qed. *)
 
-  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E dce :
+  (*Todo: adapt this to denv *)
+ (* Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
     MapstoListFromEnv Γs_in Γs_out Γls →
     E = env_to_known_locs Γls →
     ListOfMapsto Γls E ps →
     IntoDCexpr E e dce →
      coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_out c)
-       (env_ps_dv_interp E ps -∗ wp_interp_sane E (vcg_wp E ps dce R (λ dv, Base (Φ (dval_interp E dv))))) →
+       (denv_interp E m -∗ wp_interp_sane E (vcg_wp E m dce R (λ dv, Base (Φ (dval_interp E dv))))) →
     coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ).
   Proof.
     rewrite /IntoDCexpr /=. intros Hsplit ->.
@@ -321,6 +329,6 @@ Section vcg_spec.
     intros ->. iIntros "H1 H2".
     iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1").
     iIntros (v) "H". by iDestruct "H" as (dv) "[-> $]".
-  Qed.
+  Qed. *)
 
 End vcg_spec.