Commit dd523881 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of

parents a5ff7225 14a8f568
......@@ -50,6 +50,9 @@ Definition a_while: val :=
rec: "while" "cnd" "bdy" :=
a_if ("cnd" #()) (λ:<>, "bdy" #() ;;;; "while" "cnd" "bdy") a_seq%E.
Definition a_invoke: val := λ: "f" "arg",
a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".
Section proofs.
Context `{amonadG Σ}.
......@@ -260,6 +263,32 @@ Section proofs.
iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
Lemma a_invoke_spec (ef ea : expr) (R R1 R2 : iProp Σ) Ψ Φ (f : val) :
IntoVal ef f
(R R1 R2)
awp ea R Ψ -
( a, Ψ a - U (R1 - (awp (ef a) R2 (λ v, R1 Φ v)))) -
awp (a_invoke ef ea) R Φ.
iIntros (<-%of_to_val HR12) "Ha Hfa".
rewrite /a_invoke. awp_lam.
awp_apply (a_wp_awp R with "Ha").
iIntros (a) "Ha". awp_let.
iApply a_sequence_spec.
iApply (awp_wand with "Ha"). clear a.
iIntros (a) "HΨ".
iSpecialize ("Hfa" with "HΨ").
iApply awp_atomic. iIntros "HR".
iDestruct (HR12 with "HR") as "[HR1 HR2]".
iExists R2. iFrame. awp_let.
iApply (awp_wand with "[Hfa HR1]").
{ by iApply "Hfa". }
iIntros (v) "[HR1 $] HR2".
iApply HR12. iFrame.
Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
awp e1 R Φ - awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ.
......@@ -300,4 +329,4 @@ Section proofs.
End proofs.
(* Make sure that we only use the provided rules and don't break the abstraction *)
Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while.
Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke.
......@@ -25,6 +25,7 @@ Section contents.
rewrite !bi.big_sepL_nil. eauto.
(** [U] behaves like an applicative functor aka "lax functor with a strength" *)
Lemma U_sep_2 P Q : U P U Q U (P Q).
iIntros "[HP HQ]".
......@@ -36,6 +37,19 @@ Section contents.
- by iApply "HQ2".
Lemma U_stength P Q : P U Q U (P Q).
Proof. by rewrite {1}(U_intro P) U_sep_2. Qed.
Lemma U_applicative P Q : U (P - Q) U P - U Q.
iDestruct 1 as (ls1) "[HPQ1 HPQ2]".
iDestruct 1 as (ls2) "[HP1 HP2]".
iExists (ls1++ls2). rewrite !bi.big_sepL_app. iFrame.
iIntros "[HPQ1 HP1]".
iApply ("HPQ2" with "HPQ1").
iApply ("HP2" with "HP1").
Lemma U_unlock l v : l L v U (l U v).
iIntros "Hl". iExists [(l,v)]. iIntros "/= {$Hl} [$ _]".
......@@ -61,4 +61,32 @@ Section test.
awp_load_ret r. iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
Lemma a_invoke_spec_simpl (ef ea : expr) R Ψ Φ (f : val) :
IntoVal ef f
awp ea R Ψ -
U ( a, Ψ a - (awp (ef a) R Φ)) -
(* (∀ a, Ψ a -∗ U (awp (ef a) R Φ)) -∗ *)
awp (a_invoke ef ea) R Φ.
iIntros (<-%of_to_val) "Ha Hfa".
iApply (a_invoke_spec _ _ R True%I R with "Ha").
{ by rewrite bi.True_sep'. }
iIntros (a) "HΨ". iModIntro. iIntros (_).
iSpecialize ("Hfa" with "HΨ").
iApply (awp_wand with "Hfa"). eauto.
Lemma test_invoke (l : loc) R :
l L #1 -
awp (a_invoke (λ: "x", a_load (a_ret "x")) (a_ret #l))%E R (fun v => v = #1 l U #1).
iIntros "Hl".
iApply (a_invoke_spec_simpl _ _ _ (λ v, v = #l)%I).
{ iApply awp_ret. by wp_value_head. }
iIntros (? ->).
awp_let. awp_load_ret l.
End test.
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