Functions as first-class values.

theories/c_translation/monad.v

@@ -210,7 +210,7 @@ Section a_wp_rules.
   Qed.
 
   Lemma awp_atomic (ev : val) R Φ :
-    ▷ (R -∗ ∃ R', R' ∗ AWP ev #() @ R' {{ w, R' -∗ R ∗ Φ w }}) -∗
+    (R -∗ ▷ ∃ R', R' ∗ AWP ev #() @ R' {{ w, R' -∗ R ∗ Φ w }}) -∗
     AWP a_atomic ev @ R {{ Φ }}.
   Proof.
     iIntros "Hwp". rewrite awp_eq /awp_def. wp_lam. wp_pures.

theories/c_translation/translation.v

@@ -136,7 +136,9 @@ Notation "'whileVᶜ' ( cnd ) { e }" := (a_while (LamV <> cnd) (LamV <> e))
    format "'[v' 'whileVᶜ'  ( cnd )  {  '/  ' '[' e ']' '/'  } ']'") : expr_scope.
 
 Definition a_call: val := λ: "f" "arg",
-  "a" ←ᶜ "arg" ;ᶜ a_atomic (λ: <>, "f" "a").
+  (* sequence point before a function call *)
+  "fa" ←ᶜ ("f" |||ᶜ "arg");ᶜ
+  a_atomic (λ: <>, (Fst "fa") (Snd "fa")).
 Notation "'callᶜ' f a" :=
   (a_call f a)%E
   (at level 10, f, a at level 9,
@@ -506,17 +508,22 @@ Section proofs.
     iIntros "HI #Hinv". iApply a_while_spec. by iApply (a_whileV_inv_spec with "HI Hinv").
   Qed.
 
-  Lemma a_call_spec R Ψ Φ (f : val) ea :
-    AWP ea @ R {{ Ψ }} -∗
-    (∀ a, Ψ a -∗ U (R -∗ AWP f a {{ v, R ∗ Φ v }})) -∗
-    AWP callᶜ f ea @ R {{ Φ }}.
+  Lemma a_call_spec R Ψ1 Ψ2 Φ ef ea :
+    AWP ef @ R {{ Ψ1 }} -∗
+    AWP ea @ R {{ Ψ2 }} -∗
+    (∀ f a, Ψ1 f -∗ Ψ2 a -∗ U (R -∗ ▷ AWP f a {{ v, R ∗ Φ v }})) -∗
+    AWP callᶜ ef ea @ R {{ Φ }}.
   Proof.
-    iIntros "Ha Hfa".
-    awp_apply (a_wp_awp R with "Ha"); iIntros (va) "Ha". awp_lam. awp_pures.
-    iApply a_seq_bind_spec'. iApply (awp_wand with "Ha").
-    iIntros (a) "HΨ". iSpecialize ("Hfa" with "HΨ"). iModIntro. awp_pures.
-    iApply awp_atomic. iNext. iIntros "HR". iExists True%I. iSplit; first done.
-    awp_pures. iApply (awp_wand with "[-]"); first by iApply "Hfa". eauto.
+    iIntros "H1 H2 H".
+    awp_apply (a_wp_awp with "H2"); iIntros (vf) "H2".
+    awp_apply (a_wp_awp with "H1"); iIntros (va) "H1".
+    awp_lam. awp_pures.
+    iApply a_seq_bind_spec'. iApply (awp_par with "H1 H2").
+    iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2"); iModIntro.
+    awp_pures.
+    iApply awp_atomic. iIntros "HR". iSpecialize ("H" with "HR").
+    iExists True%I. iModIntro; iSplit; first done. awp_pures.
+    iApply (awp_wand with "H"); eauto.
   Qed.
 
   Lemma a_un_op_spec R Φ op e :
@@ -618,7 +625,7 @@ Section proofs.
     iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
     iIntros (v1 v2) "Hv1 Hv2 !>". awp_pures.
     iApply awp_atomic.
-    iIntros "!> $". iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
+    iIntros "$ !>". iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
     simplify_eq/=. iExists True%I. iSplit; first done. awp_pures.
     iApply awp_bind. iApply a_load_spec. iApply awp_ret. iApply wp_value.
     iExists cl, v; iFrame. iSplit; first done.

theories/tests/fact.v

@@ -8,7 +8,7 @@ Definition factorial : val := λ: "n",
   "r" ←mutᶜ ♯1;ᶜ
   "c" ←mutᶜ ♯0;ᶜ
   whileᶜ (∗ᶜ (a_ret "c") <ᶜ a_ret "n") {
-    callᶜ incr (a_ret "c");ᶜ
+    callᶜ (a_ret incr) (a_ret "c");ᶜ
     a_ret "r" =ᶜ ∗ᶜ (a_ret "r") *ᶜ ∗ᶜ (a_ret "c")
   };ᶜ
   ∗ᶜ(a_ret "r").
@@ -32,7 +32,7 @@ Section factorial_spec.
     iLöb as "IH" forall (n k Hk). iApply a_whileV_spec; iNext.
     vcg. iIntros "**". case_bool_decide.
     + iLeft. iSplit; eauto. iModIntro. vcg.
-      iIntros "Hc Hr !> $". iApply (incr_spec with "Hc"); iIntros "Hc".
+      iIntros "Hc Hr !> $ !>". iApply (incr_spec with "Hc"); iIntros "Hc".
       vcg_continue. iIntros "Hc Hr !>".
       assert (fact k * S k = fact (S k)) as -> by (simpl; lia).
       iApply ("IH" $! n (S k) with "[%] Hc Hr"). lia.

theories/tests/invoke.v

@@ -8,9 +8,9 @@ Section tests_vcg.
 
   Lemma test_invoke_1 (l: cloc)  R :
     l ↦C #42 -∗
-    AWP callᶜ c_id (∗ᶜ ♯ₗl) @ R {{ v, ⌜v = #42⌝ ∗ l ↦C #42 }}%I.
+    AWP callᶜ (a_ret c_id) (∗ᶜ ♯ₗl) @ R {{ v, ⌜v = #42⌝ ∗ l ↦C #42 }}%I.
   Proof.
-    iIntros "Hl". vcg. iIntros "Hl !> $".
+    iIntros "Hl". vcg. iIntros "Hl !> $ !>".
     awp_lam. vcg. iIntros "Hl". vcg_continue. eauto.
   Qed.
 
@@ -20,17 +20,17 @@ Section tests_vcg.
     (a_ret "v1") +ᶜ (a_ret "v2").
 
   Lemma test_invoke_2 R :
-    AWP callᶜ plus_pair (♯21 |||ᶜ ♯21) @ R {{ v, ⌜v = #42⌝ }}%I.
+    AWP callᶜ (a_ret plus_pair) (♯21 |||ᶜ ♯21) @ R {{ v, ⌜v = #42⌝ }}%I.
   Proof.
-    iIntros. vcg. iIntros "!> $". awp_lam. vcg. by vcg_continue.
+    iIntros. vcg. iIntros "!> $ !>". awp_lam. vcg. by vcg_continue.
   Qed.
 
   Lemma test_invoke_3 (l : cloc) R :
     l ↦C #21 -∗
-    AWP callᶜ plus_pair (∗ᶜ ♯ₗl |||ᶜ ∗ᶜ ♯ₗl) @ R
+    AWP callᶜ (a_ret plus_pair) (∗ᶜ ♯ₗl |||ᶜ ∗ᶜ ♯ₗl) @ R
       {{ v, ⌜v = #42⌝ ∗  l ↦C #21 }}%I.
   Proof.
-    iIntros. vcg. iIntros "Hl !> $". awp_lam. vcg.
+    iIntros. vcg. iIntros "Hl !> $ !>". awp_lam. vcg.
     iIntros "Hl". vcg_continue; eauto.
   Qed.
 End tests_vcg.

theories/tests/par_inc.v

@@ -5,7 +5,7 @@ Definition inc : val := λ: "l",
   a_ret "l" +=ᶜ ♯ 1 ;ᶜ ♯ 1.
 
 Definition par_inc : val := λ: "l",
-  callᶜ inc (a_ret "l") +ᶜ callᶜ inc (a_ret "l").
+  callᶜ (a_ret inc) (a_ret "l") +ᶜ callᶜ (a_ret inc) (a_ret "l").
 
 Section par_inc.
   Context `{amonadG Σ, !inG Σ (frac_authR natR)}.
@@ -25,9 +25,9 @@ Section par_inc.
     iApply (awp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
     { iExists 0%nat. iFrame. }
     iAssert (□ (own γ (◯!{1 / 2} 0%nat) -∗
-      AWP callᶜ inc (a_ret (cloc_to_val cl)) @ par_inc_inv ∗ R
+      AWP callᶜ (a_ret inc) (a_ret (cloc_to_val cl)) @ par_inc_inv ∗ R
       {{ v, ⌜v = #1⌝ ∧ own γ (◯!{1 / 2} 1%nat) }}))%I as "#H".
-    { iIntros "!> Hγ'". vcg; iIntros "!> [HR $]". iDestruct "HR" as (n') "[Hl Hγ]".
+    { iIntros "!> Hγ'". vcg; iIntros "!> [HR $] !>". iDestruct "HR" as (n') "[Hl Hγ]".
       iApply awp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl".
       iMod (own_update_2 with "Hγ Hγ'") as "[Hγ Hγ']".
       { apply frac_auth_update, (nat_local_update _ _ (S n') 1); lia. }

theories/vcgen/dcexpr.v

@@ -73,7 +73,7 @@ Inductive dcexpr : Type :=
   | dCPar : dcexpr → dcexpr → dcexpr
   | dCWhile : dcexpr → dcexpr → dcexpr
   | dCWhileV : dcexpr → dcexpr → dcexpr
-  | dCCall : val → dcexpr → dcexpr
+  | dCCall : dcexpr → dcexpr → dcexpr
   | dCUnknown : expr → dcexpr.
 
 Fixpoint dcexpr_size (de : dcexpr) : nat :=
@@ -81,8 +81,9 @@ Fixpoint dcexpr_size (de : dcexpr) : nat :=
   | dCRet _ | dCUnknown _ => 1
   | dCSeqBind _ de1 de2 | dCMutBind _ de1 de2 |dCAlloc de1 de2 | dCStore de1 de2
      | dCBinOp _ de1 de2 | dCPreBinOp _ de1 de2 | dCPar de1 de2
-     | dCWhile de1 de2 | dCWhileV de1 de2 => S (dcexpr_size de1 + dcexpr_size de2)
-  | dCLoad de | dCUnOp _ de | dCCall _ de => S (dcexpr_size de)
+     | dCWhile de1 de2 | dCWhileV de1 de2
+     | dCCall de1 de2 => S (dcexpr_size de1 + dcexpr_size de2)
+  | dCLoad de | dCUnOp _ de => S (dcexpr_size de)
   end.
 
 Definition dloc_of_dval (dv : dval) : option dloc :=
@@ -144,10 +145,10 @@ Fixpoint dcexpr_wf (E : known_locs) (de : dcexpr) : bool :=
   match de with
   | dCRet de => dexpr_wf E de
   | dCSeqBind _ de1 de2 | dCMutBind _ de1 de2 => dcexpr_wf E de1 && dcexpr_wf E de2
-  | dCLoad de1 | dCUnOp _ de1 | dCCall _ de1 => dcexpr_wf E de1
+  | dCLoad de1 | dCUnOp _ de1 => dcexpr_wf E de1
   | dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
-  | dCPreBinOp _ de1 de2 | dCWhile de1 de2 | dCWhileV de1 de2 | dCPar de1 de2 =>
-     dcexpr_wf E de1 && dcexpr_wf E de2
+  | dCPreBinOp _ de1 de2 | dCWhile de1 de2 | dCWhileV de1 de2
+     | dCPar de1 de2 | dCCall de1 de2 => dcexpr_wf E de1 && dcexpr_wf E de2
   | dCUnknown e => true
   end.
 
@@ -254,7 +255,7 @@ Fixpoint dcexpr_interp (E : known_locs) (de : dcexpr) : expr :=
   | dCPar de1 de2 => dcexpr_interp E de1 |||ᶜ dcexpr_interp E de2
   | dCWhile de1 de2 => whileᶜ (dcexpr_interp E de1) { dcexpr_interp E de2 }
   | dCWhileV de1 de2 => whileVᶜ (dcexpr_interp E de1) { dcexpr_interp E de2 }
-  | dCCall fv de => callᶜ fv (dcexpr_interp E de)
+  | dCCall de1 de2 => callᶜ (dcexpr_interp E de1) (dcexpr_interp E de2)
   | dCUnknown e1 => e1
   end.
 
@@ -782,7 +783,7 @@ Fixpoint dce_subst (E: known_locs) (x: string) (dv : dval) (dce : dcexpr) : dcex
   | dCPar de1 de2 => dCPar (dce_subst E x dv de1) (dce_subst E x dv de2)
   | dCWhile de1 de2 => dCWhile (dce_subst E x dv de1) (dce_subst E x dv de2)
   | dCWhileV de1 de2 => dCWhileV de1 de2
-  | dCCall v de1 => dCCall v (dce_subst E x dv de1)
+  | dCCall de1 de2 => dCCall (dce_subst E x dv de1) (dce_subst E x dv de2)
   | dCUnknown e => dCUnknown (subst x (dval_interp E dv) e)
   end.
 

theories/vcgen/reification.v

@@ -219,8 +219,9 @@ Instance into_dcexpr_whileV E E' E'' e1 e2 de1 de2 :
   IntoDCExpr E E' e1 de1 → IntoDCExpr E' E'' e2 de2 →
   IntoDCExpr E E'' (whileVᶜ(e1) { e2 }) (dCWhileV de1 de2).
 Proof. solve_into_dcexpr2. Qed.
-Instance into_dcexpr_call e1 E E' f de1 :
-  IntoDCExpr E E' e1 de1 → IntoDCExpr E E' (callᶜ (Val f) e1) (dCCall f de1).
-Proof. intros [-> ??]; by split. Qed.
+Instance into_dcexpr_call E E' E'' e1 e2 de1 de2 :
+  IntoDCExpr E E' e1 de1 → IntoDCExpr E' E'' e2 de2 →
+  IntoDCExpr E E'' (callᶜ e1 e2) (dCCall de1 de2).
+Proof. solve_into_dcexpr2. Qed.
 Instance into_dcexpr_unknown E e : IntoDCExpr E E e (dCUnknown e) | 100.
 Proof. done. Qed.

theories/vcgen/vcg.v

@@ -121,6 +121,12 @@ Section vcg.
          (cl ↦C[LLvl] w -∗ vcg_continuation E Φ v))
     end%I.
 
+  Definition vcg_call (E : known_locs) (dv1 dv2 : dval)
+      (m : denv) (R : iProp Σ) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ :=
+    (wand_denv_interp E m $ U (
+       R -∗
+       ▷ AWP (dval_interp E dv1) (dval_interp E dv2) {{ v, R ∗ vcg_continuation E Φ v }}))%I.
+
   Fixpoint vcg (E : known_locs) (n : nat) (m : denv) (de : dcexpr)
       (R : iProp Σ) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ :=
     match de, n with
@@ -216,10 +222,19 @@ Section vcg.
           end
        end
     | dCWhile de1 de2, S n => vcg_awp_continuation R E (dCWhileV de1 de2) m Φ
-    | dCCall ef de1, S n => vcg E n m de1 R $ λ E m dv,
-       wand_denv_interp E m $ U (
-         R -∗ AWP ef (dval_interp E dv)
-                {{ v, R ∗ vcg_continuation E Φ v }})
+    | dCCall de1 de2, S n =>
+       match forward E n m de1 with
+       | Some (m', mNew, dv1) =>
+          vcg E n m' de2 R $ λ E m'' dv2,
+            vcg_call E dv1 dv2 (denv_merge mNew m'') R Φ
+       | None =>
+          match forward E n m de2 with
+          | Some (m', mNew, dv2) =>
+             vcg E n m' de1 R $ λ E m'' dv1,
+               vcg_call E dv1 dv2 (denv_merge mNew m'') R Φ
+          | None => vcg_awp_continuation R E de m Φ
+          end
+       end
     | _, S p => vcg_awp_continuation R E de m Φ
     end%I.
 
@@ -611,13 +626,33 @@ Section vcg_spec.
     - (* whileV *)
       by iDestruct (vcg_awp_continuation_correct with "Hm H") as "?".
     - (* call *)
-      iApply (a_call_spec with "[H Hm]").
-      { iApply ("IH" with "[] [] Hm H"); eauto. }
-      iIntros (w) "H"; iDestruct "H" as (E' dv m' -> ???) "[Hm' H]".
-      iDestruct (wand_denv_interp_spec with "H Hm'") as "H".
-      iIntros "!> HR". iDestruct ("H" with "HR") as "H".
-      iApply (awp_wand with "H"); iIntros (v') "[$ H]".
-      by iApply vcg_continuation_mono.
+      destruct (forward _ _ m _) as [[[m' mNew] dv1]|] eqn:?; last first.
+      + destruct (forward _ _  m de2) as [[[m' mNew] dv2]|] eqn:?; last first.
+        { by iDestruct (vcg_awp_continuation_correct with "Hm H") as "?". }
+        iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto.
+        iApply (a_call_spec with "[H Hm'] H2").
+        { iApply ("IH" with "[] [] Hm' H"); eauto. }
+        iIntros (f a) "H [-> HmNew]";
+          iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
+        iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H".
+        { iApply denv_merge_interp; eauto using denv_wf_mono.
+          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
+        iIntros "!> HR". iSpecialize ("H" with "HR"); iModIntro.
+        rewrite (dval_interp_mono E E'); eauto.
+        iApply (awp_wand with "H"); iIntros (w) "[$ H]".
+        by iApply vcg_continuation_mono.
+      + iDestruct (forward_correct with "Hm") as "[Hm' H1]"; eauto.
+        iApply (a_call_spec with "H1 [H Hm']").
+        { iApply ("IH" with "[] [] Hm' H"); eauto. }
+        iIntros (f a) "[-> HmNew] H";
+          iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
+        iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H".
+        { iApply denv_merge_interp; eauto using denv_wf_mono.
+          iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
+        iIntros "!> HR". iSpecialize ("H" with "HR"); iModIntro.
+        rewrite (dval_interp_mono E E'); eauto.
+        iApply (awp_wand with "H"); iIntros (w) "[$ H]".
+        by iApply vcg_continuation_mono.
     - (* unknown *)
       by iDestruct (vcg_awp_continuation_correct with "Hm H") as "?".
   Qed.
@@ -677,3 +712,4 @@ Arguments vcg_store _ _ _ _ _ _ _ /.
 Arguments vcg_bin_op _ _ _ _ _ _ _ _ /.
 Arguments vcg_un_op _ _ _ _ _ _ _ /.
 Arguments vcg_pre_bin_op _ _ _ _ _ _ _ _ /.
+Arguments vcg_call _ _ _ _ _ _ _ _ /.