Commit 1c256b12 authored by Dan Frumin's avatar Dan Frumin
Browse files

Add `a_invoke`

parent 03c3a419
......@@ -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,33 @@ Section proofs.
iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
Qed.
Lemma a_invoke_spec (ef ea : expr) (R R1 R2 : iProp Σ) Ψ Φ (f : val) :
IntoVal ef f
(R R1 R2)
awp ea R Ψ -
U ( a, Ψ a - R1 - (awp (ef a) R2 (λ v, R1 Φ v))) -
(* (∀ a, Ψ a -∗ U (awp (ef a) R Φ)) -∗ ?? *)
awp (a_invoke ef ea) R Φ.
Proof.
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Ψ". iModIntro.
awp_let.
iApply awp_atomic. iIntros "HR".
iDestruct (HR12 with "HR") as "[HR1 HR2]".
iExists R2. iFrame. awp_let.
iSpecialize ("Hfa" with "HΨ").
iApply (awp_wand with "[Hfa HR1]").
{ by iApply "Hfa". }
iIntros (v) "[HR1 $] HR2".
iApply HR12. iFrame.
Qed.
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 Φ.
Proof.
......@@ -300,4 +330,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.
......@@ -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.
Qed.
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 Φ.
Proof.
iIntros (<-%of_to_val) "Ha Hfa".
iApply (a_invoke_spec _ _ R True%I R with "Ha").
{ by rewrite bi.True_sep'. }
iModIntro. iIntros (a) "HΨ _".
iSpecialize ("Hfa" with "HΨ").
iApply (awp_wand with "Hfa"). eauto.
Qed.
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).
Proof.
iIntros "Hl".
iApply (a_invoke_spec_simpl _ _ _ (λ v, v = #l)%I).
{ iApply awp_ret. by wp_value_head. }
iModIntro.
iIntros (? ->).
awp_let. awp_load_ret l.
Qed.
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