working on extending vcg_wp on function calls by evaluating the arguments

theories/c_translation/translation.v

@@ -90,6 +90,13 @@ Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
 Definition a_invoke: val := λ: "f" "arg",
   a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".
 
+Notation "f ❲ a ❳ " :=
+  ( a_invoke f a)%E
+  (at level 100, a at level 200,
+   format "f ❲ a ❳") : expr_scope.
+
+
+
 Section proofs.
   Context `{amonadG Σ}.
 

theories/vcgen/dcexpr.v

@@ -208,6 +208,7 @@ Inductive dcexpr : Type :=
   | dCUnOp : un_op → dcexpr → dcexpr
   | dCSeq : dcexpr → dcexpr → dcexpr
   | dCPar : dcexpr → dcexpr → dcexpr
+  | dCInvoke  (f: val) `{!Closed [] f}  (de: dcexpr)
   | dCUnknown (e : expr) `{!Closed [] e}.
 
 Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
@@ -217,10 +218,12 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
   | dCLoad de1 => a_load (dcexpr_interp E de1)
   | dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2)
   | dCBinOp op de1 de2 => a_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
-  | dCPreBinOp op de1 de2 => a_pre_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
+  | dCPreBinOp op de1 de2 =>
+    a_pre_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
   | dCUnOp op de => a_un_op op (dcexpr_interp E de)
   | dCSeq de1 de2 => dcexpr_interp E de1 ;ᶜ dcexpr_interp E de2
   | dCPar de1 de2 => dcexpr_interp E de1 |||ᶜ dcexpr_interp E de2
+  | dCInvoke fv de => fv ❲dcexpr_interp E de❳
   | dCUnknown e1 => e1
   end.
 
@@ -236,8 +239,9 @@ Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
 Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
   match de with
   | dCRet dv => dval_wf E dv
-  | dCAlloc de1 | dCLoad de1 | dCUnOp _ de1 => dcexpr_wf E de1
-  | dCStore de1 de2 | dCBinOp _ de1 de2 | dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
+  | dCAlloc de1 | dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1
+  | dCStore de1 de2 | dCBinOp _ de1 de2
+  | dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
       dcexpr_wf E de1 && dcexpr_wf E de2
   | dCUnknown _ => true
   end.
@@ -246,7 +250,7 @@ Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
 Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
   dval_wf E dv → E `prefix_of` E' → dval_wf E' dv.
 Proof.
-  induction dv as [d| |]; try naive_solver.
+  induction dv as [d| |  ]; try naive_solver.
   destruct d; eauto.
   destruct d as [i|]; last done; simplify_eq /=.
   intros Hb Hpre. case_bool_decide; last done.
@@ -285,7 +289,7 @@ Proof. destruct op, dv1,dv2; simpl; repeat case_match; naive_solver. Qed.
 Lemma dval_interp_mono (E E': known_locs) (dv: dval) :
   dval_wf E dv → E `prefix_of` E' → dval_interp E dv = dval_interp E' dv.
 Proof.
-  induction dv as [d| | ]; try naive_solver.
+  induction dv as [d| |]; try naive_solver.
   destruct d; eauto.
   destruct d as [i|]; last done; simplify_eq /=.
   intros Hb Hpre. case_bool_decide; last done.
@@ -438,6 +442,14 @@ Global Instance into_dcexpr_par E e1 e2 de1 de2:
   IntoDCexpr E (e1 |||ᶜ e2) (dCPar de1 de2).
 Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
 
+Global Instance into_dcexpr_invoke E `{Closed [] e1} ef f `{!IntoVal ef f} de1 :
+  IntoDCexpr E e1 de1 →
+  IntoDCexpr E (ef❲e1❳) (dCInvoke f de1).
+Proof.
+  intros. unfold IntoVal in *. simplify_eq /=.
+  split; simpl; auto; f_equal; by inversion H0.
+Qed.
+
 Global Instance into_dcexpr_unknown E e `{Closed [] e}:
   IntoDCexpr E e (dCUnknown e) | 100.
 Proof. done. Qed.

theories/vcgen/tests/basics.v

@@ -60,7 +60,15 @@ Section test.
     iIntros "**". vcg_solver. eauto with iFrame.
   Qed.
 
-  (*TODO: test function call with multiple arguments *)
+
+  Definition c_id : val := λ: "v", a_ret ("v").
+  Lemma test_invoke_1 (l: loc) (v : val) R :
+    l ↦C v -∗
+      AWP  c_id❲∗ᶜ ♯l❳ @ R {{ v, ⌜v = #73⌝ }}%I.
+  Proof.
+    iIntros "Hl". vcg_solver.
+  Admitted.
+
 
   Lemma test6 (l : loc) (z0 : Z) R:
     l ↦C #z0 -∗
@@ -72,7 +80,8 @@ Section test.
   Lemma test7 (l k : loc) (z0 z1 : Z) R:
     l ↦C #z0 -∗
     k ↦C #z1 -∗
-    AWP (♯l +=ᶜ ♯1) +ᶜ (∗ᶜ♯k) @ R {{ v, ⌜v = #(z0+z1)⌝ ∧ l ↦C[LLvl] #(z0+1) ∗ k ↦C #z1 }}.
+    AWP (♯l +=ᶜ ♯1) +ᶜ (∗ᶜ♯k) @
+    R {{ v, ⌜v = #(z0+z1)⌝ ∧ l ↦C[LLvl] #(z0+1) ∗ k ↦C #z1 }}.
   Proof.
     iIntros "Hl Hk". vcg_solver. eauto with iFrame.
   Qed.

theories/vcgen/vcgen.v

@@ -75,7 +75,7 @@ Section vcg.
        ''(ms1, mNew1, dv1) ← vcg_sp E ms de1;
        ''(ms2, mNew2, dv2) ← vcg_sp E ms1 de2;
          Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
- | dCAlloc _ |  dCUnknown _  => None
+ | dCAlloc _ |  dCUnknown _ | dCInvoke _ _ => None
     end.
 
   Definition vcg_sp'
@@ -153,7 +153,8 @@ Section vcg.
          match dbin_op_eval E op dw dv2 with
          | dSome dw' => Φ E (denv_insert i LLvl 1 dw' m') dw
          | mdw => ∃ dw', ⌜doption_interp mdw = Some dw'⌝ ∧
-             mapsto_wand_list E (denv_insert i LLvl 1 dw' m') (vcg_wp_continuation E Φ (dval_interp E dw))
+             mapsto_wand_list E (denv_insert i LLvl 1 dw' m')
+               (vcg_wp_continuation E Φ (dval_interp E dw))
          end
        | None => mapsto_wand_list E m (∃ (v w : val),
                    dloc_interp E (dLoc i) ↦C v ∗
@@ -237,6 +238,9 @@ Section vcg.
         | None => vcg_wp_awp_continuation R E de m Φ
         end
       end
+    | dCInvoke ef de1 => vcg_wp E m de1 R (λ E m dv,
+        (vcg_wp_awp_continuation R E
+           (dCUnknown (ef (dval_interp E dv))) m Φ))
     | _ => vcg_wp_awp_continuation R E de m Φ
     end%I.
 End vcg.
@@ -279,24 +283,35 @@ Section vcg_spec.
     - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout; simplify_eq /=.
       destruct dv1 as [ dv1|  | dv1 ]; try destruct dv1; simplify_eq/=.
       destruct d as [i|?]; simplify_eq/=.
-      destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
-      transitivity (length ms1); eauto using denv_delete_frac_2_length.
-    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
+      destruct (denv_delete_frac_2 i ms1 mNew1)
+      as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
+      transitivity (length ms1).
+      + by eapply IHde.
+      + by eapply denv_delete_frac_2_length.
+    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1;
+      simplify_eq /=.
       destruct dv1 as [dv1| | dv1]; try destruct dv1; simplify_eq/=.
       destruct d as [i|?]; simplify_eq/=.
-      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq /=.
-      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
-      transitivity (length ms1); eauto.
-      transitivity (length ms2); eauto using denv_delete_full_2_length.
+      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
+      simplify_eq /=.
+      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
+      as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
+      transitivity (length ms1).
+      + by eapply IHde1.
+      + transitivity (length ms2). by eapply IHde2.
+        by eapply denv_delete_full_2_length.
     - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
-      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
+      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
+      simplify_eq/=.
       destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
       transitivity (length ms1); eauto.
     - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
       destruct dv1 as [dv1| | dv1]; try destruct dv1; simplify_eq/=.
       destruct d as [i|?]; simplify_eq/=.
-      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
-      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
+      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
+      simplify_eq/=.
+      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
+        as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
       destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
       transitivity (length ms1); eauto.
       transitivity (length ms2); eauto using denv_delete_full_2_length.
@@ -306,17 +321,21 @@ Section vcg_spec.
     - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
       destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
       as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
-      destruct ms2; simplify_eq/=. transitivity (length ms1); eauto.
-      apply IHde2 in Hde2; by simplify_eq/=.
-    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
-      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
+      destruct ms2; simplify_eq/=. transitivity (length ms1).
+      + by eapply IHde1.
+      + apply IHde2 in Hde2; by simplify_eq/=.
+    - destruct (vcg_sp E ms de1)
+        as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
+      destruct (vcg_sp E ms1 de2)
+        as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
       transitivity (length ms1); eauto.
   Qed.
 
   Lemma vcg_sp_correct' E de ms ms' mNew dv R :
     vcg_sp E ms de = Some (ms', mNew, dv) →
     (denv_stack_interp ms ms' E
-       (awp (dcexpr_interp E de) R (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew)))%I.
+       (awp (dcexpr_interp E de) R
+          (λ v, ⌜v = dval_interp E dv⌝ ∧ denv_interp E mNew)))%I.
   Proof.
     revert ms ms' mNew dv. induction de;
     iIntros (ms ms' mNew dv Hsp); simplify_eq/=.
@@ -340,9 +359,8 @@ Section vcg_spec.
       iExists _, _. iSplit; eauto.
       iDestruct ("Hm" with "HmNew1") as "[HmNew2 $]".
       iIntros "Hl". iSplit; eauto.
-      rewrite -denv_insert_interp.
-      by iFrame.
-    - specialize (IHde1 ms).
+      rewrite -denv_insert_interp. by iFrame.
+      - specialize (IHde1 ms).
       destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=.
       destruct dv1 as [dv1| | dv1]; try destruct dv1; simplify_eq/=.
       destruct d as [i|?]; simplify_eq/=.
@@ -442,7 +460,8 @@ Section vcg_spec.
       iClear "Hawp1 Hawp2".
       iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
       iApply (awp_par with "Hawp1 Hawp2").
-      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>"; simplify_eq/=; iSplit; eauto.
+      iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
+      simplify_eq/=; iSplit; eauto.
       rewrite -denv_merge_interp. iFrame.
   Qed.
 
@@ -510,7 +529,8 @@ Section vcg_spec.
       destruct Hout1 as (?&?&?).
       repeat split; eauto using denv_wf_insert.
       eauto using denv_wf_merge.
-    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
+    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
+      simplify_eq/=.
       destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
       simplify_eq/=.
       destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
@@ -519,11 +539,14 @@ Section vcg_spec.
       destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
       repeat split; eauto. apply denv_wf_merge; eauto.
       eapply (dbin_op_eval_dSome_wf _ dv1 dv2); eauto.
-    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
+    - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
+      simplify_eq/=.
       destruct dv1 as [dv1| | dv1]; try destruct dv1; simplify_eq/=.
       destruct d as [i|?]; simplify_eq/=.
-      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
-      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
+      destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2;
+      simplify_eq/=.
+      destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
+        as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
       apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
       destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
       destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
@@ -534,6 +557,7 @@ Section vcg_spec.
       eapply denv_wf_insert; eauto.
       eapply (dbin_op_eval_dSome_wf _ dv dv2); eauto.
       by eapply denv_wf_merge.
+
     - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
       destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
       destruct (dun_op_eval E u dv1) as [|?|?] eqn:Hop; simplify_eq/=.
@@ -642,8 +666,9 @@ Section vcg_spec.
     dval_wf E dv2 →
     denv_interp E m -∗
     vcg_wp_pre_bin_op E op dv1 dv2 m Φ -∗
-    ∃ l v w, l ↦C v ∗ ⌜dval_interp E dv1 = #l⌝ ∗ ⌜bin_op_eval op v (dval_interp E dv2) = Some w⌝
-          ∗  (l ↦C[LLvl] w -∗ vcg_wp_continuation E Φ v).
+    ∃ l v w, l ↦C v ∗ ⌜dval_interp E dv1 = #l⌝ ∗
+      ⌜bin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗
+      (l ↦C[LLvl] w -∗ vcg_wp_continuation E Φ v).
   Proof.
     iIntros (? ?) "Hm Hwp". rewrite /vcg_wp_pre_bin_op.
     destruct (is_dloc E dv1) as [i|] eqn:Hloc; last first.
@@ -655,14 +680,17 @@ Section vcg_spec.
     - rewrite mapsto_wand_list_spec.
       iDestruct ("Hwp" with "Hm") as (v w) "(Hl&%&Hwp)".
       iExists (dloc_interp E (dLoc i)),v,w. iFrame. eauto.
-    - iDestruct (denv_delete_full_interp E with "Hm") as "[Hm' Hl]"; first eassumption.
+    - iDestruct (denv_delete_full_interp E with "Hm") as "[Hm' Hl]";
+      first eassumption.
       destruct (dbin_op_eval E op dw dv2) as [|dw'|] eqn:Hop.
       { iDestruct "Hwp" as (dw') "[% Hwp]".
-        iExists (dloc_interp E (dLoc i)),(dval_interp E dw),(dval_interp E dw'). iFrame.
+        iExists (dloc_interp E (dLoc i)),
+        (dval_interp E dw), (dval_interp E dw'). iFrame.
         repeat iSplit; eauto.
         iIntros "Hl". iCombine "Hm' Hl" as "Hm'". rewrite denv_insert_interp.
         rewrite mapsto_wand_list_spec. by iApply "Hwp". }
-      { iExists (dloc_interp E (dLoc i)),(dval_interp E dw),(dval_interp E dw'). iFrame.
+      { iExists (dloc_interp E (dLoc i)),
+        (dval_interp E dw), (dval_interp E dw'). iFrame.
         repeat iSplit; eauto; try iPureIntro.
         - apply dbin_op_eval_correct. by rewrite Hop.
         - iIntros "Hl". iCombine "Hm' Hl" as "Hm'". rewrite denv_insert_interp.
@@ -671,14 +699,15 @@ Section vcg_spec.
           apply dbin_op_eval_dSome_wf in Hop; eauto.
           repeat iSplit; eauto using denv_wf_insert. }
       { iDestruct "Hwp" as (dw') "[% Hwp]".
-        iExists (dloc_interp E (dLoc i)),(dval_interp E dw),(dval_interp E dw'). iFrame.
+        iExists (dloc_interp E (dLoc i)), (dval_interp E dw),
+        (dval_interp E dw'). iFrame.
         repeat iSplit; eauto.
         - iPureIntro. apply dbin_op_eval_correct. by rewrite Hop.
         - iIntros "Hl". iCombine "Hm' Hl" as "Hm'". rewrite denv_insert_interp.
           rewrite mapsto_wand_list_spec. by iApply "Hwp". }
   Qed.
 
-  Lemma vcg_wp_store_correct E m dv1 dv2 Φ :
+ Lemma vcg_wp_store_correct E m dv1 dv2 Φ :
     denv_wf E m →
     dval_wf E dv2 →
     denv_interp E m -∗
@@ -696,7 +725,9 @@ Section vcg_spec.
         iSplit; first done.
         iPoseProof (denv_delete_full_interp E) as "Hdel". eassumption.
         iSpecialize ("Hdel" with "Hm"). iDestruct "Hdel" as "[HmDel Hl]"; iFrame.
-        iIntros "Hl". iExists E, dv2, (denv_insert i LLvl 1 dv2 m'); repeat (iSplit; first done).
+        iIntros "Hl".
+        iExists E, dv2, (denv_insert i LLvl 1 dv2 m');
+          repeat (iSplit; first done).
         iSplit. iPureIntro. apply denv_wf_insert; last done.
         by destruct (denv_wf_delete_full E dv_old i m m' Hwf Hdel) as [Hdelwf ?].
         rewrite -denv_insert_interp. eauto with iFrame.
@@ -708,6 +739,7 @@ Section vcg_spec.
       iSpecialize ("Hwp" with "[Hm]"); iFrame.
   Qed.
 
+
   Lemma vcg_wp_continuation_mono E E' Φ w:
     E `prefix_of` E' → vcg_wp_continuation E' Φ w -∗ vcg_wp_continuation E Φ w.
   Proof.
@@ -818,10 +850,12 @@ Section vcg_spec.
         rewrite IHde1; [| done | done]. iSpecialize ("Hm'" with "Hwp").
         iApply (a_pre_bin_op_spec with "Hm' Hde2"); fold dcexpr_interp.
         iNext. iIntros (v1 v2) "Hex (-> & HmNew) $".
-        iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
+        iDestruct "Hex" as (E' dv1 m'' Heq Hpre Hm'wf) "(% & Hm' & Hwp)";
+        simplify_eq /=.
         iDestruct (denv_interp_mono with "HmNew") as "HmNew"; eauto.
         iCombine ("HmNew Hm'") as "Hm". rewrite denv_merge_interp.
-        iDestruct (vcg_wp_pre_bin_op_correct with "Hm Hwp") as (l v w) "(Hl & % & % & Hwp)".
+        iDestruct (vcg_wp_pre_bin_op_correct with "Hm Hwp")
+          as (l v w) "(Hl & % & % & Hwp)".
         { apply denv_wf_merge; eauto using denv_wf_mono. }
         { eapply dval_wf_mono; eauto. }
         iExists l, v, w. iFrame. repeat iSplit; eauto.
@@ -834,16 +868,18 @@ Section vcg_spec.
         iRename "Hm'" into "Hde2".
         iApply (a_pre_bin_op_spec with "Hde1 Hde2");  fold dcexpr_interp.
         iNext. iIntros (v1 v2) "(-> & HmNew) Hex $".
-        iDestruct "Hex" as (E' dv2 m2 Hpre ? Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
+        iDestruct "Hex" as (E' dv2 m2 Hpre ? Hm'wf) "(% & Hm' & Hwp)";
+        simplify_eq /=.
         iDestruct (denv_interp_mono with "HmNew") as "HmNew"; eauto.
         iCombine ("HmNew Hm'") as "Hm". rewrite denv_merge_interp.
-        iDestruct (vcg_wp_pre_bin_op_correct with "Hm Hwp") as (l v w) "(Hl & % & % & Hwp)".
+        iDestruct (vcg_wp_pre_bin_op_correct with "Hm Hwp")
+          as (l v w) "(Hl & % & % & Hwp)".
         { apply denv_wf_merge; eauto using denv_wf_mono. }
         { eapply dval_wf_mono; eauto. }
         iExists l, v, w. iFrame. repeat iSplit; eauto.
         * iPureIntro. rewrite (dval_interp_mono E E'); auto.
         * rewrite (vcg_wp_continuation_mono E E'); auto.
-    - rewrite IHde //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
+     - rewrite IHde //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
       iApply (awp_wand with "Hm"). iIntros (v) "Hex".
       iDestruct "Hex" as (E' dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)".
       destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
@@ -910,6 +946,15 @@ Section vcg_spec.
                   eauto using dval_wf_mono, denv_wf_mono, denv_wf_merge).
         iFrame. rewrite (denv_interp_mono E) //.
         iApply denv_merge_interp. iFrame.
+    - simpl. rewrite IHde //.  iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
+      iApply (a_invoke_spec with "Hm"). iIntros (arg) "Hf !> HR".
+        iDestruct "Hf" as (E' dv1 m' Heq Hpre Hm'wf) "(% & Hm' & Hwp)".
+        unfold vcg_wp_awp_continuation.
+        rewrite mapsto_wand_list_spec. iSpecialize ("Hwp" with "Hm'").
+        simplify_eq /=. iExists R. iFrame.
+        iApply (awp_wand with "Hwp"). iIntros (v) "Hc Hr".
+        rewrite (vcg_wp_continuation_mono E) //.
+        iFrame.
     - by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
   Qed.
 End vcg_spec.