Commit 5e98b3d6 authored by Dan Frumin's avatar Dan Frumin

Stronger spec for c_call

parent 84f6294f
...@@ -539,7 +539,7 @@ Section proofs. ...@@ -539,7 +539,7 @@ Section proofs.
Lemma cwp_call R Ψ1 Ψ2 Φ ef ea : Lemma cwp_call R Ψ1 Ψ2 Φ ef ea :
CWP ef @ R {{ Ψ1 }} - CWP ef @ R {{ Ψ1 }} -
CWP ea @ R {{ Ψ2 }} - CWP ea @ R {{ Ψ2 }} -
( f a, Ψ1 f - Ψ2 a - U (R - CWP f a {{ v, R Φ v }})) - ( f a, Ψ1 f - Ψ2 a - R - U (CWP f a {{ v, R Φ v }})) -
CWP call ef ea @ R {{ Φ }}. CWP call ef ea @ R {{ Φ }}.
Proof. Proof.
iIntros "H1 H2 H". iIntros "H1 H2 H".
...@@ -550,8 +550,9 @@ Section proofs. ...@@ -550,8 +550,9 @@ Section proofs.
iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2"). iIntros "!>" (f a) "H1 H2 !>". iSpecialize ("H" with "H1 H2").
cwp_pures. iApply cwp_atomic. iIntros "HR". iNext. cwp_pures. iApply cwp_atomic. iIntros "HR". iNext.
iExists True%I. iSplitR; first done. cwp_pures. iExists True%I. iSplitR; first done. cwp_pures.
iSpecialize ("H" with "HR").
iApply cwp_bind. iApply cwp_mset_clear. iNext. iModIntro. iApply cwp_bind. iApply cwp_mset_clear. iNext. iModIntro.
iSpecialize ("H" with "HR"). cwp_pures. cwp_pures.
iApply (cwp_wand with "H"); eauto. iApply (cwp_wand with "H"); eauto.
Qed. Qed.
......
...@@ -33,7 +33,7 @@ Section factorial_spec. ...@@ -33,7 +33,7 @@ Section factorial_spec.
iLöb as "IH" forall (n k Hk). iApply cwp_whileV; iNext. iLöb as "IH" forall (n k Hk). iApply cwp_whileV; iNext.
vcg. iIntros "**". case_bool_decide. vcg. iIntros "**". case_bool_decide.
+ iLeft. iSplit; eauto. iModIntro. vcg. + iLeft. iSplit; eauto. iModIntro. vcg.
iIntros "Hc Hr !> $ !>". iApply (inc_spec with "Hc"); iIntros "Hc". iIntros "Hc Hr $ !> !>". iApply (inc_spec with "Hc"); iIntros "Hc".
vcg_continue. iIntros "Hc Hr !>". vcg_continue. iIntros "Hc Hr !>".
assert (fact k * S k = fact (S k)) as -> by (simpl; lia). assert (fact k * S k = fact (S k)) as -> by (simpl; lia).
iApply ("IH" $! n (S k) with "[%] Hc Hr"). lia. iApply ("IH" $! n (S k) with "[%] Hc Hr"). lia.
......
...@@ -10,7 +10,7 @@ Section tests_vcg. ...@@ -10,7 +10,7 @@ Section tests_vcg.
l C #42 - l C #42 -
CWP call (c_ret c_id) (∗ᶜ ♯ₗl) @ R {{ v, v = #42 l C #42 }}%I. CWP call (c_ret c_id) (∗ᶜ ♯ₗl) @ R {{ v, v = #42 l C #42 }}%I.
Proof. Proof.
iIntros "Hl". vcg. iIntros "Hl !> $ !>". iIntros "Hl". vcg. iIntros "Hl $ !> !>".
cwp_lam. vcg. iIntros "Hl". vcg_continue. eauto. cwp_lam. vcg. iIntros "Hl". vcg_continue. eauto.
Qed. Qed.
...@@ -22,7 +22,7 @@ Section tests_vcg. ...@@ -22,7 +22,7 @@ Section tests_vcg.
Lemma test_invoke_2 R : Lemma test_invoke_2 R :
CWP call (c_ret plus_pair) (21 ||| 21) @ R {{ v, v = #42 }}%I. CWP call (c_ret plus_pair) (21 ||| 21) @ R {{ v, v = #42 }}%I.
Proof. Proof.
iIntros. vcg. iIntros "!> $ !>". cwp_lam. vcg. by vcg_continue. iIntros. vcg. iIntros "$ !> !>". cwp_lam. vcg. by vcg_continue.
Qed. Qed.
Lemma test_invoke_3 (l : cloc) R : Lemma test_invoke_3 (l : cloc) R :
...@@ -30,7 +30,7 @@ Section tests_vcg. ...@@ -30,7 +30,7 @@ Section tests_vcg.
CWP call (c_ret plus_pair) (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl) @ R CWP call (c_ret plus_pair) (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl) @ R
{{ v, v = #42 l C #21 }}%I. {{ v, v = #42 l C #21 }}%I.
Proof. Proof.
iIntros. vcg. iIntros "Hl !> $ !>". cwp_lam. vcg. iIntros. vcg. iIntros "Hl $ !> !>". cwp_lam. vcg.
iIntros "Hl". vcg_continue; eauto. iIntros "Hl". vcg_continue; eauto.
Qed. Qed.
End tests_vcg. End tests_vcg.
...@@ -29,7 +29,7 @@ Section par_inc. ...@@ -29,7 +29,7 @@ Section par_inc.
iAssert ( (own γ (!{1 / 2} 0%nat) - iAssert ( (own γ (!{1 / 2} 0%nat) -
CWP call (c_ret inc) (c_ret (cloc_to_val cl)) @ par_inc_inv R CWP call (c_ret inc) (c_ret (cloc_to_val cl)) @ par_inc_inv R
{{ v, v = #1 own γ (!{1 / 2} 1%nat) }}))%I as "#H". {{ 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 cwp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl". iApply cwp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl".
iMod (own_update_2 with "Hγ Hγ'") as "[Hγ Hγ']". iMod (own_update_2 with "Hγ Hγ'") as "[Hγ Hγ']".
{ apply frac_auth_update, (nat_local_update _ _ (S n') 1); lia. } { apply frac_auth_update, (nat_local_update _ _ (S n') 1); lia. }
...@@ -43,4 +43,4 @@ Section par_inc. ...@@ -43,4 +43,4 @@ Section par_inc.
iDestruct 1 as (n') ">[Hl Hγ]". iCombine "Hγ1 Hγ2" as "Hγ'". iDestruct 1 as (n') ">[Hl Hγ]". iCombine "Hγ1 Hγ2" as "Hγ'".
iDestruct (own_valid_2 with "Hγ Hγ'") as %->%frac_auth_agreeL. iFrame; auto. iDestruct (own_valid_2 with "Hγ Hγ'") as %->%frac_auth_agreeL. iFrame; auto.
Qed. Qed.
End par_inc. End par_inc.
\ No newline at end of file
...@@ -123,9 +123,9 @@ Section vcg. ...@@ -123,9 +123,9 @@ Section vcg.
Definition vcg_call (E : known_locs) (dv1 dv2 : dval) Definition vcg_call (E : known_locs) (dv1 dv2 : dval)
(m : denv) (R : iProp Σ) (Φ : known_locs denv dval iProp Σ) : iProp Σ := (m : denv) (R : iProp Σ) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
(wand_denv_interp E m $ U ( (wand_denv_interp E m
R - (R -
CWP (dval_interp E dv1) (dval_interp E dv2) {{ v, R vcg_continuation E Φ v }}))%I. U (CWP (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) Fixpoint vcg (E : known_locs) (n : nat) (m : denv) (de : dcexpr)
(R : iProp Σ) (Φ : known_locs denv dval iProp Σ) : iProp Σ := (R : iProp Σ) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
...@@ -634,12 +634,12 @@ Section vcg_spec. ...@@ -634,12 +634,12 @@ Section vcg_spec.
iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto. iDestruct (forward_correct with "Hm") as "[Hm' H2]"; eauto.
iApply (cwp_call with "[H Hm'] H2"). iApply (cwp_call with "[H Hm'] H2").
{ iApply ("IH" with "[] [] Hm' H"); eauto. } { iApply ("IH" with "[] [] Hm' H"); eauto. }
iIntros (f a) "H [-> HmNew]"; iIntros (f a) "H [-> HmNew]".
iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]". iDestruct "H" as (E' dv m'' -> ???) "[Hm'' H]".
iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H". iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H".
{ iApply denv_merge_interp; eauto using denv_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono.
iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
iIntros "!> HR". iSpecialize ("H" with "HR"); iModIntro. iIntros "HR". iSpecialize ("H" with "HR"). iNext. iModIntro.
rewrite (dval_interp_mono E E'); eauto. rewrite (dval_interp_mono E E'); eauto.
iApply (cwp_wand with "H"); iIntros (w) "[$ H]". iApply (cwp_wand with "H"); iIntros (w) "[$ H]".
by iApply vcg_continuation_mono. by iApply vcg_continuation_mono.
...@@ -651,7 +651,7 @@ Section vcg_spec. ...@@ -651,7 +651,7 @@ Section vcg_spec.
iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H". iDestruct (wand_denv_interp_spec with "H [Hm'' HmNew]") as "H".
{ iApply denv_merge_interp; eauto using denv_wf_mono. { iApply denv_merge_interp; eauto using denv_wf_mono.
iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. } iFrame "Hm''". iApply (denv_interp_mono with "HmNew"); eauto. }
iIntros "!> HR". iSpecialize ("H" with "HR"); iModIntro. iIntros "HR". iSpecialize ("H" with "HR"); iNext; iModIntro.
rewrite (dval_interp_mono E E'); eauto. rewrite (dval_interp_mono E E'); eauto.
iApply (cwp_wand with "H"); iIntros (w) "[$ H]". iApply (cwp_wand with "H"); iIntros (w) "[$ H]".
by iApply vcg_continuation_mono. by iApply vcg_continuation_mono.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment