Commit c84b97ab authored by Robbert Krebbers's avatar Robbert Krebbers

Seal C-WP, better proof mode support for C-WP, get rid of some Rs.

parent 7eafceed
......@@ -74,23 +74,18 @@ Section a_wp.
In some sense it is a form of CPSing on a logical level.
But I still cannot precisely state why is it needed.
*)
Definition awp (e : expr)
Definition awp_def (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
tc_opaque (WP e {{ ev,
WP e {{ ev,
(γ : flock_name) (env : val) (l : val) (I : gmap prop_id lock_res),
is_flock amonadN γ l -
flock_resources γ I -
([ map] X I, res_prop X) (env_inv env R) -
WP ev env l {{ v, Φ v flock_resources γ I }}
}})%I.
Global Instance elim_bupd_awp p e Φ :
ElimModal True p false (|==> P) P (awp e R Φ) (awp e R Φ).
Proof.
iIntros (P R _) "[HP HA]".
rewrite /awp /tc_opaque /= bi.intuitionistically_if_elim.
iMod "HP". by iApply "HA".
Qed.
}}%I.
Definition awp_aux : seal (@awp_def). by eexists. Qed.
Definition awp := unseal awp_aux.
Definition awp_eq : @awp = @awp_def := seal_eq awp_aux.
End a_wp.
Notation "'AWP' e @ R {{ Φ } }" := (awp e%E R%I Φ)
......@@ -113,26 +108,26 @@ Section a_wp_rules.
( v : val, AWP v @ R {{ Φ }} - Ψ v) -
WP e {{ Ψ }}.
Proof.
iIntros "Hwp H". rewrite /awp /=. iApply (wp_wand with "Hwp").
iIntros "Hwp H". rewrite awp_eq /=. iApply (wp_wand with "Hwp").
iIntros (v) "Hwp". iApply "H". by iApply wp_value'.
Qed.
Lemma wp_awp_bind R Φ K e :
WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }} -
AWP (fill K e) @ R {{ Φ }}.
Proof. by apply: wp_bind. Qed.
AWP fill K e @ R {{ Φ }}.
Proof. rewrite awp_eq. by apply: wp_bind. Qed.
Lemma wp_awp_bind_inv R Φ K e :
AWP (fill K e) @ R {{ Φ }} -
WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }}.
Proof. by apply: wp_bind_inv. Qed.
AWP fill K e @ R {{ Φ }} -
WP e {{ v, AWP fill K (of_val v) @ R {{ Φ }} }}.
Proof. rewrite awp_eq. by apply: wp_bind_inv. Qed.
Lemma awp_insert_res e Φ R1 R2 :
R1 -
AWP e @ (R1 R2) {{ v, R1 ={}= Φ v }} -
AWP e @ R2 {{ Φ }}.
Proof.
iIntros "HR1 Hawp". rewrite /awp /=.
iIntros "HR1 Hawp". rewrite awp_eq.
iApply (wp_wand with "Hawp").
iIntros (v) "HΦ".
iIntros (γ env l I) "#Hflock Hres #Heq".
......@@ -154,17 +149,33 @@ Section a_wp_rules.
by iApply "HΦ".
Qed.
Lemma awp_wand e (Φ Ψ : val iProp Σ) R :
Lemma awp_fupd_wand e Φ Ψ R :
AWP e @ R {{ Φ }} -
( v, Φ v - Ψ v) -
( v, Φ v ={}= Ψ v) -
AWP e @ R {{ Ψ }}.
Proof.
iIntros "HAWP Hv". rewrite /awp /=.
iApply (wp_wand with "HAWP").
iIntros (v) "HΦ".
iIntros (γ env l I) "#Hflock Hres #Heq".
iIntros "Hwp H". rewrite awp_eq.
iApply (wp_wand with "Hwp"); iIntros (v) "HΦ".
iIntros (γ env l I) "#Hflock Hres #Heq". iApply wp_fupd.
iApply (wp_wand with "[HΦ Hres]"). iApply ("HΦ" with "Hflock Hres Heq").
iIntros (w) "[HΦ $]". by iApply "Hv".
iIntros (w) "[HΦ $]". by iApply "H".
Qed.
Lemma awp_fupd e Φ R :
AWP e @ R {{ v, |={}=> Φ v }} - AWP e @ R {{ Φ }}.
Proof. iIntros "Hwp". iApply (awp_fupd_wand with "Hwp"); auto. Qed.
Lemma fupd_awp e Φ R :
(|={}=> AWP e @ R {{ v, Φ v }}) - AWP e @ R {{ Φ }}.
Proof. rewrite awp_eq. by iIntros ">Hwp". Qed.
Lemma awp_wand e Φ Ψ R :
AWP e @ R {{ Φ }} -
( v, Φ v - Ψ v) -
AWP e @ R {{ Ψ }}.
Proof.
iIntros "Hwp H". iApply (awp_fupd_wand with "Hwp"); iIntros (v) "HΦ !>".
by iApply "H".
Qed.
Lemma awp_pure K φ n e1 e2 R Φ :
......@@ -178,18 +189,18 @@ Section a_wp_rules.
Qed.
Lemma awp_ret e R Φ :
WP e {{ Φ }} - AWP (a_ret e) @ R {{ Φ }}.
WP e {{ Φ }} - AWP a_ret e @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite /awp /=. wp_apply (wp_wand with "Hwp").
iIntros "Hwp". rewrite awp_eq /awp_def. wp_apply (wp_wand with "Hwp").
iIntros (v) "HΦ". wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures. iFrame.
Qed.
Lemma awp_bind (f : val) (e : expr) R Φ :
AWP e @ R {{ ev, AWP (f ev) @ R {{ Φ }} }} -
AWP e @ R {{ ev, AWP f ev @ R {{ Φ }} }} -
AWP a_bind e f @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite /awp /=.
iIntros "Hwp". rewrite awp_eq /awp_def.
wp_apply (wp_wand with "Hwp"). iIntros (ev) "Hwp".
wp_lam. wp_pures.
iIntros (γ env l I) "#Hflock Hres #Heq". wp_pures. wp_bind (ev env l).
......@@ -202,7 +213,7 @@ Section a_wp_rules.
(R - R', R' AWP ev #() @ R' {{ w, R' - R Φ w }}) -
AWP a_atomic ev @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite /awp /=. wp_lam. wp_pures.
iIntros "Hwp". rewrite awp_eq /awp_def. wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
......@@ -236,7 +247,7 @@ Section a_wp_rules.
WP ev env {{ w, (env_inv env R Φ w) }}) -
AWP a_atomic_env ev @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite /awp /=. wp_lam. wp_pures.
iIntros "Hwp". rewrite awp_eq /awp_def. wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
......@@ -253,13 +264,13 @@ Section a_wp_rules.
iIntros "$". wp_pures. iFrame.
Qed.
Lemma awp_par (Ψ1 Ψ2 : val iProp Σ) e1 e2 R (Φ : val iProp Σ) :
Lemma awp_par Ψ1 Ψ2 e1 e2 R Φ :
AWP e1 @ R {{ Ψ1 }} -
AWP e2 @ R {{ Ψ2 }} -
( w1 w2, Ψ1 w1 - Ψ2 w2 - Φ (w1,w2)%V) -
AWP e1 ||| e2 @ R {{ Φ }}.
Proof.
iIntros "Hwp1 Hwp2 HΦ". rewrite /awp /=.
iIntros "Hwp1 Hwp2 HΦ". rewrite awp_eq /awp_def.
wp_apply (wp_wand with "Hwp2").
iIntros (ev2) "Hwp2".
wp_apply (wp_wand with "Hwp1").
......@@ -287,36 +298,64 @@ Section a_wp_rules.
by rewrite -flock_res_op Qp_div_2. }
iApply ("HΦ" with "[$] [$]").
Qed.
Global Instance frame_awp p R' e R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v))
Frame p R (AWP e @ R' {{ Φ }}) (AWP e @ R' {{ Ψ }}).
Proof.
rewrite /Frame. iIntros (HR) "[HR H]". iApply (awp_wand with "H").
iIntros (v) "H". iApply HR; iFrame.
Qed.
Global Instance is_except_0_awp R e Φ : IsExcept0 (AWP e @ R {{ Φ }}).
Proof. rewrite /IsExcept0. iIntros "H". iApply fupd_awp. by iMod "H". Qed.
Global Instance elim_modal_bupd_awp p R e P Φ :
ElimModal True p false (|==> P) P (AWP e @ R {{ Φ }}) (AWP e @ R {{ Φ }}).
Proof.
rewrite /ElimModal bi.intuitionistically_if_elim; iIntros (_) "[HP HR]".
iApply fupd_awp. iMod "HP". by iApply "HR".
Qed.
Global Instance elim_modal_fupd_wp p R e P Φ :
ElimModal True p false (|={}=> P) P (AWP e @ R {{ Φ }}) (AWP e @ R {{ Φ }}).
Proof.
rewrite /ElimModal bi.intuitionistically_if_elim; iIntros (_) "[HP HR]".
iApply fupd_awp. iMod "HP". by iApply "HR".
Qed.
Global Instance add_modal_fupd_wp R e P Φ :
AddModal (|={}=> P) P (AWP e @ R {{ Φ }}).
Proof. rewrite /AddModal. iIntros "[>HP H]". by iApply "H". Qed.
End a_wp_rules.
Section a_wp_run.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}.
Lemma awp_run (ev : val) R Φ :
R - ( `{amonadG Σ}, AWP ev @ R {{ w, R ={}= Φ w }}) -
Lemma awp_run (ev : val) Φ :
( `{amonadG Σ}, AWP ev {{ w, Φ w }}) -
WP a_run ev {{ Φ }}.
Proof.
iIntros "HR Hwp". rewrite /awp /=. wp_lam.
iIntros "Hwp". wp_lam.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "Henv". wp_let.
iMod locking_heap_init as (?) "Hσ".
pose (amg := AMonadG Σ _ _ _ _).
iSpecialize ("Hwp" $! amg).
iSpecialize ("Hwp" $! amg). rewrite awp_eq /awp_def.
wp_apply (newflock_spec amonadN); first done.
iIntros (k γ') "#Hlock". iApply wp_fupd.
iMod (flock_res_alloc_strong _ _ _ (env_inv env R)%I
with "Hlock [Henv Hσ $HR]") as (s ρ) "[_ Hres]"; first done.
iMod (flock_res_alloc_strong _ _ _ (env_inv env)%I
with "Hlock [Henv Hσ]") as (s ρ) "[_ Hres]"; first done.
{ iNext. iExists , . iFrame. iPureIntro; set_solver. }
wp_let.
iMod (wp_value_inv with "Hwp") as "Hwp".
iApply (wp_wand with "[Hwp Hres]").
- iApply ("Hwp" $! _ _ _ {[s := LockRes _ 1 ρ]} with "Hlock [Hres] []").
+ rewrite /flock_resources big_sepM_singleton //.
+ rewrite big_sepM_singleton //.
+ by rewrite big_sepM_singleton right_id.
- iIntros (w) "[HΦ Hres]".
rewrite /flock_resources big_sepM_singleton /=.
iMod (flock_res_dealloc with "Hlock Hres") as "[Henv HR]"; try done.
iApply "HΦ". iFrame.
by iMod (flock_res_dealloc with "Hlock Hres") as "Henv".
Qed.
End a_wp_run.
......
......@@ -508,16 +508,15 @@ Section proofs.
Lemma a_call_spec R Ψ Φ (f : val) ea :
AWP ea @ R {{ Ψ }} -
( a, Ψ a - U (R - R', R' (AWP f a @ R' {{ v, R' - R Φ v }}))) -
( a, Ψ a - U (R - AWP f a {{ v, R Φ v }})) -
AWP call (f, 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".
iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
iExists R'. iFrame. by 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.
Qed.
Lemma a_un_op_spec R Φ op e :
......@@ -619,7 +618,7 @@ Section proofs.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_pures.
iApply awp_atomic.
iIntros "!> HR". 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.
......@@ -633,7 +632,7 @@ Section proofs.
- iIntros (? ? -> ->).
iExists _, _; iFrame. iSplit; first done.
iIntros "?". awp_seq. iApply awp_ret; iApply wp_value.
iIntros "_". iFrame "HR". by iApply "HΦ".
iIntros "_". by iApply "HΦ".
Qed.
End proofs.
......
......@@ -95,11 +95,11 @@ Section test.
Proof. iIntros. vcg. eauto with iFrame. Qed.
Definition stupid (l : cloc) : expr :=
a_store (♯ₗ l) ( 1); a_ret #0.
♯ₗ l = 1; a_ret #0.
Lemma test_seq_fail l :
l C[ULvl] #0 -
AWP ((stupid l) + (stupid l)) + (a_ret #0) {{ v, l C #1 }}.
AWP (stupid l + stupid l) + (a_ret #0) {{ v, l C #1 }}.
Proof. iIntros. vcg. Fail by eauto with iFrame. Abort.
Lemma test_seq5 l k :
......
From iris_c.vcgen Require Import proofmode.
Definition incr : val := λ: "l",
(a_ret "l") = ∗ᶜ (a_ret "l") + 1 ;
(a_ret "l") += 1 ;
().
Definition factorial : val := λ: "n",
......@@ -32,8 +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 !> HR". iExists R. iFrame "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.
......
......@@ -10,8 +10,8 @@ Section tests_vcg.
l C #42 -
AWP call (c_id, ∗ᶜ ♯ₗl) @ R {{ v, v = #42 l C #42 }}%I.
Proof.
iIntros "Hl". vcg. iIntros "Hl !> HR". iExists R. iFrame.
awp_lam. vcg. iIntros "Hl $". vcg_continue. eauto.
iIntros "Hl". vcg. iIntros "Hl !> $".
awp_lam. vcg. iIntros "Hl". vcg_continue. eauto.
Qed.
Definition plus_pair : val := λ: "vv",
......@@ -22,8 +22,7 @@ Section tests_vcg.
Lemma test_invoke_2 R :
AWP call (plus_pair, 21 ||| 21) @ R {{ v, v = #42 }}%I.
Proof.
iIntros. vcg. iIntros "!> HR". iExists R. iFrame. awp_lam. vcg.
iIntros "$". by vcg_continue.
iIntros. vcg. iIntros "!> $". awp_lam. vcg. by vcg_continue.
Qed.
Lemma test_invoke_3 (l : cloc) R :
......@@ -31,7 +30,7 @@ Section tests_vcg.
AWP call (plus_pair, (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl)) @ R
{{ v, v = #42 l C #21 }}%I.
Proof.
iIntros. vcg. iIntros "Hl !> HR". iExists R. iFrame. awp_lam. vcg.
iIntros "Hl $". vcg_continue; eauto.
iIntros. vcg. iIntros "Hl !> $". awp_lam. vcg.
iIntros "Hl". vcg_continue; eauto.
Qed.
End tests_vcg.
......@@ -292,9 +292,8 @@ Section vcg.
| dCWhile de1 de2, S n => vcg_wp_awp_continuation R E (dCWhileV de1 de2) m Φ
| dCCall ef de1, S n => vcg_wp E n m de1 R $ λ E m dv,
wand_denv_interp E m $ U (
R - R',
R' AWP ef (dval_interp E dv) @ R'
{{ v, R' - R vcg_wp_continuation E Φ v }})
R - AWP ef (dval_interp E dv)
{{ v, R vcg_wp_continuation E Φ v }})
| _, S p => vcg_wp_awp_continuation R E de m Φ
end%I.
......@@ -898,9 +897,9 @@ Section vcg_spec.
{ 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 (R') "[HR' H]".
iExists R'. iFrame "HR'". iApply (awp_wand with "H"); iIntros (v') "H HR".
iDestruct ("H" with "HR") as "[$ H]". by iApply vcg_wp_continuation_mono.
iIntros "!> HR". iDestruct ("H" with "HR") as "H".
iApply (awp_wand with "H"); iIntros (v') "[$ H]".
by iApply vcg_wp_continuation_mono.
- (* unknown *)
by iDestruct (vcg_wp_awp_continuation_correct with "Hm H") as "?".
Qed.
......
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