Commit 4ea80cea authored by Ike Mulder's avatar Ike Mulder
Browse files

Fixed atomic examples with new hint notation.

parent b7c603f7
From diaframe.heap_lang Require Import stepping_tacs.
From diaframe.lib Require Import own_hints.
From iris.heap_lang Require Import proofmode.
From iris.algebra Require Import excl proofmode_classes frac.
Set Default Proof Using "Type".
Definition mk_offer : val :=
λ: "_", ref #0.
Definition take_offer : val :=
λ: "l", CAS "l" #0 #1.
Definition revoke_offer : val :=
λ: "l", CAS "l" #0 #2.
Definition mk_mailbox : val := λ: "_", AllocN #3 #0.
Definition empty_box : val :=
rec: "empty_box" "m" :=
if: CAS "m" #1 #0
then #()
else "empty_box" "m".
Definition post_to_box : val :=
λ: "m" "v",
if: CAS "m" #0 #2
then
let: "off" := mk_offer #() in
("m" + #2) <- "v";;
("m" + #1) <- "off";;
"m" <- #1;;
empty_box "m";;
revoke_offer "off"
else #true.
Definition check_box : val :=
λ: "m",
if: CAS "m" #1 #2
then
if: take_offer (! ("m" + #1))
then
let: "v" := ! ("m" + #2) in
"m" <- #1;;
SOME "v"
else NONE
else NONE.
Definition new_stack : val := λ: "_", (mk_mailbox #(), ref NONEV).
Definition push : val :=
rec: "push" "p" "v" :=
let: "mailbox" := Fst "p" in
let: "s" := Snd "p" in
if: post_to_box "mailbox" "v" (* do I still have it? *)
then
let: "tail" := ! "s" in
let: "new" := SOME (ref ("v", "tail")) in
if: CAS "s" "tail" "new" then #() else "push" "p" "v"
else #() (* someone took it *).
Definition pop : val :=
rec: "pop" "p" :=
let: "mailbox" := Fst "p" in
let: "s" := Snd "p" in
match: check_box "mailbox" with
NONE =>
match: !"s" with
NONE => NONEV
| SOME "l" =>
let: "pair" := !"l" in
if: CAS "s" (SOME "l") (Snd "pair")
then SOME (Fst "pair")
else "pop" "p"
end
| SOME "x" => SOME "x"
end.
Definition channelR := exclR unitR.
Class channelG Σ := { channel_inG :> inG Σ channelR }.
Definition channelΣ : gFunctors := #[GFunctor channelR].
Instance subG_channelΣ {Σ} : subG channelΣ Σ channelG Σ.
Proof. solve_inG. Qed.
Obligation Tactic := iProgramStepsS.
Section side_channel.
Context `{!heapGS Σ, !channelG Σ} (N : namespace).
Implicit Types l : loc.
Definition revoke_tok γ := own γ (Excl ()).
Definition stages γ (P : iProp Σ) l : iProp Σ :=
(z : Z), l #z ((z = 0 P)
z = 1
(z = 2 revoke_tok γ))%I.
Lemma mk_offer_spec P (v : val) :
{{{ P }}} mk_offer v {{{ o γ, RET #o; revoke_tok γ inv N (stages γ P o) }}}.
Proof. iStepsS. Qed.
(* A partial specification for revoke that will be useful later *)
Global Program Instance revoke_spec γ P (o : loc) :
SPEC {{ inv N (stages γ P o) revoke_tok γ }}
revoke_offer #o
{{ (b : bool), RET #b; b = true P b = false }}.
(* A partial specification for take that will be useful later *)
Global Program Instance take_spec γ P (o : loc) :
SPEC {{ inv N (stages γ P o) }}
take_offer #o
{{ (b : bool), RET #b; b = true P b = false }}.
End side_channel.
Definition mailboxUR := prodUR (optionUR $ exclR unitR) (optionUR $ exclR unitR).
Class mailboxG Σ := { mailbox_inG :> inG Σ mailboxUR }.
Definition mailboxΣ : gFunctors := #[GFunctor mailboxUR].
Instance subG_mailboxΣ {Σ} : subG mailboxΣ Σ mailboxG Σ.
Proof. solve_inG. Qed.
Section mailbox.
Context `{!heapGS Σ, channelG Σ, mailboxG Σ} (N : namespace).
Implicit Types l : loc.
Definition Noffer := N .@ "offer".
Definition mailbox_inv γ (P : val iProp Σ) (m : loc) : iProp Σ :=
( (z : Z), m #z
((z = 0 v1 v2, (m + 1) v1 (m + 2) v2 own γ (Excl' (), Excl' ()))
(z = 1 (l : loc) (v : val) γ_off, (m + 1) #l (m + 2) v
inv Noffer (stages γ_off (P v) l) own γ (Excl' (), None))
z = 2)).
Theorem mk_mailbox_spec (P : val iProp Σ) :
{{{ True }}} mk_mailbox #() {{{ (m : loc) (γ : gname), RET #m; inv N (mailbox_inv γ P m) }}}.
Proof. iStepsS. Qed.
Global Program Instance check_box_works γ (P : val iProp Σ) (m : loc) :
SPEC {{ inv N (mailbox_inv γ P m) }}
check_box #m
{{ (ov : val), RET ov; ov = NONEV v, ov = SOMEV v P v}}.
Global Instance empty_box_spec γ (P : val iProp Σ) (m : loc) :
SPEC {{ inv N (mailbox_inv γ P m) own γ (None, Excl' ()) }}
empty_box #m
{{ RET #(); True }}.
Proof.
iStepsS. iLöb as "IH".
wp_lam. iStepsS.
Qed.
Opaque mk_offer.
Global Instance post_to_box_works γ (P : val iProp Σ) (m : loc) (v : val) :
SPEC {{ inv N (mailbox_inv γ P m) P v }}
post_to_box #m v
{{ (b : bool), RET #b; b = true P v b = false }}.
Proof.
iStepsS.
wp_apply (mk_offer_spec with "H3").
iStepsS.
Qed.
End mailbox.
Section stack_works.
Context `{!heapGS Σ, channelG Σ, mailboxG Σ} (N : namespace).
Implicit Types l : loc.
Definition Nmailbox := N .@ "mailbox".
Definition is_list_pre (P : val iProp Σ) (F : val -d> iPropO Σ) :
val -d> iPropO Σ := (λ v,
v = NONEV (
(l : loc), v = SOMEV #l (h : val) (t : val), l ↦□ (h, t)%V P h F t))%I.
Local Instance is_list_contr (P : val iProp Σ) : Contractive (is_list_pre P).
Proof.
rewrite /is_list_pre => n f f' Hf v.
repeat (f_contractive || f_equiv).
apply Hf.
Qed.
Definition is_list_def (P : val -> iProp Σ) := fixpoint (is_list_pre P).
Definition is_list_aux P : seal (@is_list_def P). by eexists. Qed.
Definition is_list P := unseal (is_list_aux P).
Definition is_list_eq P : @is_list P = @is_list_def P := seal_eq (is_list_aux P).
Lemma is_list_unfold (P : val iProp Σ) v :
is_list P v is_list_pre P (is_list P) v.
Proof.
rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
Qed.
Lemma is_list_dup (P : val iProp Σ) v :
is_list P v - is_list P v (v = NONEV l, v = SOMEV (LitV (LitLoc l)) h t, l ↦□ (h, t)).
Proof. rewrite is_list_unfold. iHammer. Qed.
Global Instance biabd_islist_none P :
BiAbd (TTl := [tele]) (TTr := [tele]) false empty_hyp_first (is_list P NONEV) id emp%I emp%I.
Proof. rewrite /BiAbd /= is_list_unfold /=. iHammer. Qed.
Global Instance biabd_islist_some P (l : loc) :
BiAbd (TTl := [tele (_ : val) (_ : val)]) (TTr := [tele]) false empty_hyp_last (is_list P $ SOMEV #l)
id (λ h t, l ↦□ (h, t)%V P h is_list P t)%I (λ _ _, emp)%I.
Proof.
rewrite /BiAbd /= empty_hyp_last_eq => h t.
rewrite (is_list_unfold _ (InjRV _)) left_id right_id /=. iStepS.
iRight. iStepsS.
Qed.
(* we don't want to make is_list into_or, because that will recursively unfold all possible lengths of list *)
Instance is_list_remember_part P v :
MergablePersist (is_list P v) (λ p Pin Pout,
TCAnd (TCEq Pin empty_hyp_first)
(TCEq Pout (v = NONEV l, v = SOMEV (LitV (LitLoc l)) val_is_unboxed v h t, l ↦□ (h, t))))%I | 30.
Proof.
rewrite /MergablePersist => p Pin Pout [-> ->] /=.
rewrite bi.intuitionistically_if_elim is_list_dup.
iStepsS; iIntros "!>"; iStepsS.
Qed.
Global Instance biabd_islist_pop P l h v E p :
BiAbd (TTl := [tele]) (TTr := [tele]) p (l ↦□ (h, v)%V)%I ( is_list P v)%I
(fupd E E) (is_list P (SOMEV #l))%I (val_is_unboxed v P h)%I | 30.
Proof.
rewrite /BiAbd /= bi.intuitionistically_if_elim.
rewrite (is_list_unfold _ (InjRV _)) /=. iStepS.
rewrite is_list_unfold; iRevert "H3". iHammer.
Qed.
Definition stack_inv P l :=
( vl, l vl is_list P vl val_is_unboxed vl)%I.
Definition is_stack P v :=
( (m l : loc) γ, v = (#m, #l)%V inv Nmailbox (mailbox_inv Nmailbox γ P m) inv N (stack_inv P l))%I.
Opaque mk_mailbox.
Theorem new_stack_spec P :
{{{ True }}} new_stack #() {{{ v, RET v; is_stack P v }}}.
Proof.
iStepsS. iIntros "!>".
wp_apply mk_mailbox_spec; [done|].
iStepsS.
Qed.
Theorem push_spec P (s v : val) :
SPEC {{ is_stack P s P v }} push s v {{ RET #(); True }}.
Proof.
iStepsS. iLöb as "IH" forall (v).
wp_lam. iStepsS.
Qed.
Theorem pop_spec P (s : val) :
SPEC {{ is_stack P s }} pop s {{ (ov : val), RET ov; ov = NONEV v, ov = SOMEV v P v }}.
Proof.
iStepsS. iLöb as "IH". wp_lam. iStepsS.
Qed.
End stack_works.
\ No newline at end of file
......@@ -105,18 +105,16 @@ Section problems.
Qed.
Instance frac_abd q :
BiAbd (TTl := [tele]) (TTr := [tele]) false (P q) (P 1) id
((q < 1%Qp q', (q + q')%Qp = 1%Qp P q') q = 1%Qp)%I True%I.
HINT P q [- ; (q < 1%Qp q', (q + q')%Qp = 1%Qp P q') q = 1%Qp] [id]; P 1 [True].
Proof.
rewrite /BiAbd /=.
iStepsS.
iCombine "H1 H2" as "H".
rewrite H1. iStepsS.
Qed.
Instance co_frac_abd q : BiAbd (TTl := [tele]) (TTr := [tele]) false (co_frac_P q) (P 1) id (P q) emp%I.
Instance co_frac_abd q : HINT co_frac_P q [- ; P q] [id]; P 1 [emp].
Proof.
rewrite /BiAbd /= /co_frac_P. iStepS.
iStepS.
iCombine "H1 H2" as "HP". rewrite Qp_add_comm H0.
iStepsS.
Qed.
......
......@@ -60,13 +60,13 @@ Section spec.
(l : loc), v = #l inv N (stack_inv l)%I.
Global Instance biabd_islist_none xs :
BiAbd (TTl := [tele]) (TTr := [tele]) false empty_hyp_first (is_list xs NONEV) id xs = []%I xs = []%I.
Proof. rewrite /BiAbd /=. iStepsS. Qed.
HINT empty_hyp_first [xs = []] [id]; is_list xs NONEV [xs = []].
Proof. iStepsS. Qed.
Global Instance biabd_islist_some (l : loc) xs :
BiAbd (TTl := [tele_pair val; list val; val]) (TTr := [tele]) false empty_hyp_last (is_list xs $ SOMEV #l)%I
id (λ x xs' t, l ↦□ (x, t) is_list xs' t xs = x :: xs')%I (λ x xs' _, xs = x:: xs')%I.
Proof. rewrite /BiAbd /=. iStepsS. Qed.
HINT empty_hyp_last [x xs' t; l ↦□ (x, t) is_list xs' t xs = x :: xs'] [id];
is_list xs (SOMEV #l) [xs = x :: xs'].
Proof. iStepsS. Qed.
Lemma is_list_agree xs ys v : is_list xs v is_list ys v xs = ys.
Proof.
......
......@@ -61,10 +61,10 @@ Section proof.
Proof.
iStepsS; [iRight| iRight|iLeft]; iStepsS.
- rewrite Zmod_small //. split; lia.
- rewrite -H2. replace (x1 + 1 + x2 - x1)%Z with (x2 + 1)%Z; last lia. done.
- assert (x1 = Z.pos max_state)%Z as -> by lia.
- rewrite -H2. replace (x4 + 1 + x2 - x4)%Z with (x2 + 1)%Z; last lia. done.
- assert (x4 = Z.pos max_state)%Z as -> by lia.
rewrite Z_mod_same_full //.
- rewrite -H2. replace (0%nat + x2 - x1)%Z with (x2 + 1 - (Zpos max_state + 1))%Z by lia.
- rewrite -H2. replace (0%nat + x2 - x4)%Z with (x2 + 1 - (Zpos max_state + 1))%Z by lia.
by rewrite /eqm -(Z_mod_plus_full (x2 + 1)%Z (-1)%Z).
Qed.
......
......@@ -92,9 +92,8 @@ Section spec.
Definition is_queue_head γe (p : loc) : iProp Σ := own γe ( (Excl' p)).
Global Instance update_lock_holder_biabd γe l1 l2 E :
BiAbd (TTl := [tele_pair loc]) (TTr := [tele]) false (own γe ( (Excl' l1))) (own γe ( (Excl' l2))) (fupd E E)
(λ p, own γe ( (Excl' p)))%I (λ p, own γe ( (Excl' l2)) p = l1)%I | 99.
Proof. rewrite /BiAbd /=. iStepS. iStepS. rewrite comm. iStepsS. Qed.
HINT own γe ( Excl' l1) [p; own γe ( Excl' p)] [fupd E E]; own γe ( Excl' l2) [own γe ( Excl' l2) p = l1] | 99.
Proof. iStepS. iStepS. rewrite comm. iStepsS. Qed.
Definition acquired_node γe n (p : loc) : iProp Σ :=
(n + 1) #p own γe ( (Excl' p)) p #false (l' : loc), n #l' is_queued_loc γe l' l' {#1/2} #true.
......
......@@ -58,13 +58,13 @@ Section spec.
vl, l vl is_list xs vl val_is_unboxed vl%I.
Global Instance biabd_islist_none xs :
BiAbd (TTl := [tele]) (TTr := [tele]) false empty_hyp_first (is_list xs NONEV) id xs = []%I xs = []%I.
Proof. rewrite /BiAbd /=. iStepsS. Qed.
HINT empty_hyp_first [xs = []] [id]; is_list xs NONEV [xs = []].
Proof. iStepsS. Qed.
Global Instance biabd_islist_some (l : loc) xs :
BiAbd (TTl := [tele_pair val; list val; val]) (TTr := [tele]) false empty_hyp_last (is_list xs $ SOMEV #l)%I
id (λ x xs' t, l ↦□ (x, t) is_list xs' t xs = x :: xs')%I (λ x xs' _, xs = x:: xs')%I.
Proof. rewrite /BiAbd /=. iStepsS. Qed.
HINT empty_hyp_last [x xs' t; l ↦□ (x, t) is_list xs' t xs = x :: xs'] [id];
is_list xs (SOMEV #l) [xs = x :: xs'].
Proof. iStepsS. Qed.
Lemma is_list_agree xs ys v : is_list xs v is_list ys v xs = ys.
Proof.
......
......@@ -77,7 +77,7 @@ Section proof.
iStepsS. iLöb as "IH".
lang_open_tac.
iStepsS; last iSmash.
destruct (decide (x2 = v)); iSmash.
destruct (decide (x3 = v)); iSmash.
Qed.
Transparent vals_compare_safe.
......
......@@ -139,30 +139,25 @@ Section biabd_instances.
Global Instance mapsto_val_may_need_more (l : loc) (v1 v2 : val) (q1 q2 : Qp) mq q :
FracSub q2 q1 mq
TCEq mq (Some q)
BiAbd (TTl := [tele_pair val]) (TTr := [tele]) false (l {#q1} v1)%I (l {#q2} v2)%I id
(λ v', v1 = v2 l {#q} v')%I (λ v', v1 = v2 v' = v1)%I | 55.
Proof.
rewrite /BiAbd /= /FracSub => <- -> v'.
iStepsS.
Qed.
HINT l {#q1} v1 [v'; v1 = v2 l {#q} v'] [id];
l {#q2} v2 [v1 = v2 v' = v1] | 55.
Proof. move => <- ->. iStepsS. Qed.
Global Instance mapsto_val_have_enough (l : loc) (v1 v2 : val) (q1 q2 : Qp) mq :
FracSub q1 q2 mq
BiAbd (TTl := [tele]) (TTr := [tele]) false (l {#q1} v1)%I (l {#q2} v2)%I id v1 = v2%I
(v1 = v2 match mq with | Some q => l {#q} v1 | _ => True end)%I | 54.
HINT l {#q1} v1 [v1 = v2] [id]; l {#q2} v2 [v1 = v2 match mq with Some q => l {#q} v1 | _ => True end].
Proof.
rewrite /BiAbd /= /FracSub => <-.
move => <-.
destruct mq; iStepsS.
iDestruct "H1" as "[H1 H1']".
iStepsS.
Qed.
Global Instance as_persistent_mapsto p l q v :
BiAbd (TTl := [tele]) (TTr := [tele]) p (l {q} v)%I (l ↦□ v)%I (bupd) emp%I (l ↦□ v)%I | 100.
HINT □⟨p l {q} v [emp] [bupd]; l ↦□v [l ↦□ v] | 100.
Proof.
rewrite /BiAbd /= right_id bi.intuitionistically_if_elim.
iIntros "Hl".
iMod (mapsto_persist with "Hl") as "#Hl".
iStepS. rewrite bi.intuitionistically_if_elim.
iMod (mapsto_persist with "H1") as "#Hl".
iStepsS.
Qed.
End biabds.
......
......@@ -67,7 +67,7 @@ Section aupd_autom.
(* when we need to prove an atomic update, we first run the greatest laterable fixpoint *)
Global Instance abduct_aupd_as_gfp {TA TB : tele} Eo Ei (α : TA PROP) (β Φ : TA TB PROP) :
Abduct (TT := [tele]) false empty_hyp_last (atomic_update Eo Ei α β Φ) id (greatest_laterable_fixpoint_wrt (λ Ψ, make_laterable $ atomic_acc' Eo Ei α Ψ β Φ) emp%I).
HINT1 empty_hyp_last [greatest_laterable_fixpoint_wrt (λ Ψ, make_laterable $ atomic_acc' Eo Ei α Ψ β Φ) emp] [id]; atomic_update Eo Ei α β Φ.
Proof.
rewrite /Abduct /= empty_hyp_last_eq left_id. rewrite <-atomic_update_to_gfp.
rewrite greatest_laterable_fixpoint_wrt_eq.
......@@ -82,15 +82,16 @@ Section aupd_autom.
(* after running the fixpoint and introducing make_laterable, we proceed as follows: *)
Global Instance atomic_acc_abd {TA TB : tele} Eo Ei' Ei (α : TA PROP) P (β Φ : TA TB PROP) beq :
SimplTeleEq TB beq
Abduct (TT := [tele]) false empty_hyp_first (atomic_acc' Eo Ei α P β Φ) id
(|={Eo, Ei'}=> .. x, α x (* A neat trick is that we need Ei ⊆ Ei', but we can actually defer that to below! *)
( (b : bool), b = true b = false - .. (my : if b then TB else [tele]),
α x b = false (.. y : TB, β x y b = true match b, my with | true, y' => tele_app (tele_app beq y') y | false, _ => False end) ={Ei',Eo}= Ei Ei'
(* extra mask here forces closing invariant first *)
|={Eo}=> match b, my with
| true, my => Φ x my
| false, _ => P
end)).
HINT1 empty_hyp_first [
|={Eo, Ei'}=> .. x, α x (* A neat trick is that we need Ei ⊆ Ei', but we can actually defer that to below! *)
( (b : bool), b = true b = false - .. (my : if b then TB else [tele]),
α x b = false (.. y : TB, β x y b = true match b, my with | true, y' => tele_app (tele_app beq y') y | false, _ => False end) ={Ei',Eo}= Ei Ei'
(* extra mask here forces closing invariant first *)
|={Eo}=> match b, my with
| true, my => Φ x my
| false, _ => P
end)
] [id]; atomic_acc' Eo Ei α P β Φ.
Proof.
rewrite /Abduct /atomic_acc' /= empty_hyp_first_eq left_id => Hbeq.
iIntros ">[%x (Hα & Hy)]".
......
Supports Markdown
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