Commit cb9d659c authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Remove more unneeded files; small clean-ups.

parent 0701bd20
-Q theories fri
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-projection-no-head-constant,-arguments-assert
theories/prelude/list.v
theories/prelude/compact.v
theories/prelude/set_finite_setoid.v
......@@ -62,8 +62,6 @@ theories/program_logic/refine_raw_adequacy.v
theories/program_logic/refine.v
theories/program_logic/refine_ectx.v
theories/program_logic/refine_ectx_delay.v
theories/program_logic/boxes.v
theories/proofmode/sts.v
theories/heap_lang/lang.v
theories/heap_lang/tactics.v
theories/heap_lang/wp_tactics.v
......
This diff is collapsed.
From stdpp Require Import gmap.
From fri.algebra Require Export upred.
From fri.algebra Require Export upred_big_op.
Import uPred.
Module uPred_reflection. Section uPred_reflection.
Context {M : ucmraT}.
Inductive expr :=
| ETrue : expr
| EVar : nat expr
| ESep : expr expr expr.
Fixpoint eval (Σ : list (uPred M)) (e : expr) : uPred M :=
match e with
| ETrue => Emp
| EVar n => from_option id Emp%IP (Σ !! n)
| ESep e1 e2 => eval Σ e1 eval Σ e2
end.
Fixpoint flatten (e : expr) : list nat :=
match e with
| ETrue => []
| EVar n => [n]
| ESep e1 e2 => flatten e1 ++ flatten e2
end.
Notation eval_list Σ l := ([] ((λ n, from_option id Emp%IP (Σ !! n)) <$> l))%IP.
Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
Proof.
induction e as [| |e1 IH1 e2 IH2];
rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //.
Qed.
(*
Lemma flatten_entails Σ e1 e2 :
flatten e2 `contains` flatten e1 eval Σ e1 eval Σ e2.
Proof.
intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
Qed.
*)
Lemma flatten_equiv Σ e1 e2 :
flatten e2 ≡ₚ flatten e1 eval Σ e1 ⊣⊢ eval Σ e2.
Proof. intros He. by rewrite !eval_flatten He. Qed.
Lemma flatten_equiv_entails Σ e1 e2 :
flatten e2 ≡ₚ flatten e1 eval Σ e1 eval Σ e2.
Proof. intros He. by rewrite !eval_flatten He. Qed.
Fixpoint prune (e : expr) : expr :=
match e with
| ETrue => ETrue
| EVar n => EVar n
| ESep e1 e2 =>
match prune e1, prune e2 with
| ETrue, e2' => e2'
| e1', ETrue => e1'
| e1', e2' => ESep e1' e2'
end
end.
Lemma flatten_prune e : flatten (prune e) = flatten e.
Proof.
induction e as [| |e1 IH1 e2 IH2]; simplify_eq/=; auto.
rewrite -IH1 -IH2. by repeat case_match; rewrite ?right_id_L.
Qed.
Lemma prune_correct Σ e : eval Σ (prune e) ⊣⊢ eval Σ e.
Proof. by rewrite !eval_flatten flatten_prune. Qed.
Fixpoint cancel_go (n : nat) (e : expr) : option expr :=
match e with
| ETrue => None
| EVar n' => if decide (n = n') then Some ETrue else None
| ESep e1 e2 =>
match cancel_go n e1 with
| Some e1' => Some (ESep e1' e2)
| None => ESep e1 <$> cancel_go n e2
end
end.
Definition cancel (ns : list nat) (e: expr) : option expr :=
prune <$> fold_right (mbind cancel_go) (Some e) ns.
Lemma flatten_cancel_go e e' n :
cancel_go n e = Some e' flatten e ≡ₚ n :: flatten e'.
Proof.
revert e'; induction e as [| |e1 IH1 e2 IH2]; intros;
repeat (simplify_option_eq || case_match); auto.
- by rewrite IH1 //.
- by rewrite IH2 // Permutation_middle.
Qed.
Lemma flatten_cancel e e' ns :
cancel ns e = Some e' flatten e ≡ₚ ns ++ flatten e'.
Proof.
rewrite /cancel fmap_Some=> -[{e'}e' [He ->]]; rewrite flatten_prune.
revert e' He; induction ns as [|n ns IH]=> e' He; simplify_option_eq; auto.
rewrite Permutation_middle -flatten_cancel_go //; eauto.
Qed.
Lemma cancel_entails Σ e1 e2 e1' e2' ns :
cancel ns e1 = Some e1' cancel ns e2 = Some e2'
(eval Σ e1' eval Σ e2') eval Σ e1 eval Σ e2.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
rewrite !fmap_app !big_sep_app. apply sep_mono_r.
Qed.
Fixpoint to_expr (l : list nat) : expr :=
match l with
| [] => ETrue
| [n] => EVar n
| n :: l => ESep (EVar n) (to_expr l)
end.
Arguments to_expr !_ / : simpl nomatch.
Lemma eval_to_expr Σ l : eval Σ (to_expr l) ⊣⊢ eval_list Σ l.
Proof.
induction l as [|n1 [|n2 l] IH]; csimpl; rewrite ?right_id //.
by rewrite IH.
Qed.
Lemma split_l Σ e ns e' :
cancel ns e = Some e' eval Σ e ⊣⊢ (eval Σ (to_expr ns) eval Σ e').
Proof.
intros He%flatten_cancel.
by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
Qed.
Lemma split_r Σ e ns e' :
cancel ns e = Some e' eval Σ e ⊣⊢ (eval Σ e' eval Σ (to_expr ns)).
Proof. intros. rewrite /= comm. by apply split_l. Qed.
Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
Global Instance quote_True Σ : Quote Σ Σ True ETrue.
Global Instance quote_var Σ1 Σ2 P i:
rlist.QuoteLookup Σ1 Σ2 P i Quote Σ1 Σ2 P (EVar i) | 1000.
Global Instance quote_sep Σ1 Σ2 Σ3 P1 P2 e1 e2 :
Quote Σ1 Σ2 P1 e1 Quote Σ2 Σ3 P2 e2 Quote Σ1 Σ3 (P1 P2) (ESep e1 e2).
Class QuoteArgs (Σ: list (uPred M)) (Ps: list (uPred M)) (ns: list nat) := {}.
Global Instance quote_args_nil Σ : QuoteArgs Σ nil nil.
Global Instance quote_args_cons Σ Ps P ns n :
rlist.QuoteLookup Σ Σ P n
QuoteArgs Σ Ps ns QuoteArgs Σ (P :: Ps) (n :: ns).
End uPred_reflection.
Ltac quote :=
match goal with
| |- ?P1 ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
change (eval Σ3 e1 eval Σ3 e2) end end
end.
Ltac quote_l :=
match goal with
| |- ?P1 ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
change (eval Σ2 e1 P2) end
end.
End uPred_reflection.
Tactic Notation "solve_sep_entails" :=
uPred_reflection.quote; apply uPred_reflection.flatten_equiv_entails;
apply (bool_decide_unpack _); vm_compute; exact Logic.I.
Ltac close_uPreds Ps tac :=
let M := match goal with |- @uPred_entails ?M _ _ => M end in
let rec go Ps Qs :=
lazymatch Ps with
| [] => let Qs' := eval cbv [reverse rev_append] in (reverse Qs) in tac Qs'
| ?P :: ?Ps => find_pat P ltac:(fun Q => go Ps (Q :: Qs))
end in
(* avoid evars in case Ps = @nil ?A *)
try match Ps with [] => unify Ps (@nil (uPred M)) end;
go Ps (@nil (uPred M)).
Tactic Notation "cancel" constr(Ps) :=
uPred_reflection.quote;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
eapply uPred_reflection.cancel_entails with (ns:=ns');
[cbv; reflexivity|cbv; reflexivity|simpl].
Tactic Notation "ecancel" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Qs => cancel Qs).
(** [to_front [P1, P2, ..]] rewrites in the premise of such that
the assumptions P1, P2, ... appear at the front, in that order. *)
Tactic Notation "to_front" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
uPred_reflection.quote_l;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
eapply entails_equiv_l;
first (apply uPred_reflection.split_l with (ns:=ns'); cbv; reflexivity);
simpl).
Tactic Notation "to_back" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
uPred_reflection.quote_l;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
eapply entails_equiv_l;
first (apply uPred_reflection.split_r with (ns:=ns'); cbv; reflexivity);
simpl).
(** [sep_split] is used to introduce a ().
Use [sep_split left: [P1, P2, ...]] to define which assertions will be
taken to the left; the rest will be available on the right.
[sep_split right: [P1, P2, ...]] works the other way around. *)
Tactic Notation "sep_split" "right:" open_constr(Ps) :=
to_back Ps; apply sep_mono.
Tactic Notation "sep_split" "left:" open_constr(Ps) :=
to_front Ps; apply sep_mono.
......@@ -6,7 +6,6 @@ From fri.chan_lang Require Export lang derived refine refine_heap refine_heap_pr
From fri.chan2heap Require Export chan2heap.
From fri.chan_lang Require Import tactics.
From fri.heap_lang Require Import lang heap proofmode notation.
From fri.proofmode Require Import sts.
Import heap_lang.
Import uPred.
......
From fri.heap_lang Require Export notation.
Definition newbarrier : val := λ: <>, ref #0.
Definition signal : val := λ: "x", "x" <- #1.
Definition wait : val :=
rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
Global Opaque newbarrier signal wait.
From stdpp Require Import functions.
From fri.algebra Require Import upred_big_op.
From fri.program_logic Require Import saved_prop.
From fri.heap_lang Require Import proofmode.
From iris.proofmode Require Import sts.
From fri.heap_lang.lib.barrier Require Export barrier.
From fri.heap_lang.lib.barrier Require Import protocol.
Import uPred.
(** The CMRAs we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class barrierG Σ := BarrierG {
barrier_stsG :> stsG heap_lang Σ sts;
barrier_savedPropG :> savedPropG heap_lang Σ idCF;
}.
(** The Functors we need. *)
Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF idCF].
(* Show and register that they match. *)
Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ.
Proof. destruct H as (?&?&?). split; apply _. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!heapG Σ, !barrierG Σ} (N : namespace).
Implicit Types I : gset gname.
Local Notation iProp := (iPropG heap_lang Σ).
Definition ress_one (P : iProp) (i : gname) : iProp :=
( Ψ : gname iProp,
(P - (Ψ i)) (saved_prop_own i (Ψ i)))%I.
(* I think there's somethingfishy going on with notation, but I don't want to diagnose it *)
Definition ress (P : iProp) (I : gset gname) : iProp :=
( Ψ : gname iProp,
(P - [ set] i I, Ψ i) [ set] i I, saved_prop_own i (Ψ i))%I.
Coercion state_to_val (s : state) : val :=
match s with State Low _ => #0 | State High _ => #1 end.
Arguments state_to_val !_ / : simpl nomatch.
Definition state_to_prop (s : state) (P : iProp) : iProp :=
match s with State Low _ => P | State High _ => True%I end.
Arguments state_to_prop !_ _ / : simpl nomatch.
Definition barrier_inv (l : loc) (P : iProp) (s : state) : iProp :=
(l s ress (state_to_prop s P) (state_I s))%I.
Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
( (heapN N) heap_ctx sts_ctx γ N (barrier_inv l P))%I.
Definition send (l : loc) (P : iProp) : iProp :=
( γ, barrier_ctx γ l P sts_ownS γ low_states {[ Send ]})%I.
Definition recv (l : loc) (R : iProp) : iProp :=
( γ P Q i,
barrier_ctx γ l P sts_ownS γ (i_states i) {[ Change i ]}
saved_prop_own i Q (Q - R))%I.
(*
Global Instance barrier_ctx_relevant (γ : gname) (l : loc) (P : iProp) :
RelevantP (barrier_ctx γ l P).
Proof. apply _. Qed.
*)
Typeclasses Opaque barrier_ctx send recv.
(** Setoids *)
Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
Proof. solve_proper. Qed.
Global Instance state_to_prop_ne n s :
Proper (dist n ==> dist n) (state_to_prop s).
Proof. solve_proper. Qed.
Global Instance barrier_inv_ne n l :
Proper (dist n ==> eq ==> dist n) (barrier_inv l).
Proof. solve_proper. Qed.
Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
Proof. solve_proper. Qed.
Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
Proof. solve_proper. Qed.
Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
Proof. solve_proper. Qed.
(** Helper lemmas *)
(*
Lemma ress_split i i1 i2 Q R1 R2 P I :
i I i1 I i2 I i1 i2
saved_prop_own i Q saved_prop_own i1 R1 saved_prop_own i2 R2
(Q - R1 R2) ress P I
ress P ({[i1;i2]} I {[i]}).
Proof.
iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
rewrite -assoc_L !big_sepS_fn_insert'; [|abstract set_solver ..].
by iFrame.
- rewrite -assoc_L !big_sepS_fn_insert; [|abstract set_solver ..]. eauto.
Qed.
(** Actual proofs *)
Lemma newbarrier_spec (P : iProp) (Φ : val iProp) :
heapN N
heap_ctx ( l, recv l P send l P - Φ #l) WP newbarrier #() {{ Φ }}.
Proof.
iIntros (HN) "[#? HΦ]".
rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
iApply "HΦ".
iPvs (saved_prop_alloc (F:=idCF) _ P) as (γ) "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame.
iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
sts_ownS γ' low_states {[Send]})%I with "|==>[-]" as "[Hr Hs]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver.
+ iApply (sts_own_weaken with "Hγ'");
auto using sts.closed_op, i_states_closed, low_states_closed;
abstract set_solver. }
iPvsIntro. rewrite /recv /send. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame. auto.
- auto.
Qed.
Lemma signal_spec l P (Φ : val iProp) :
send l P P Φ #() WP signal #l {{ Φ }}.
Proof.
rewrite /signal /send /barrier_ctx.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_store. iPvsIntro. destruct p; [|done].
iExists (State High I), ( : set token).
iSplit; [iPureIntro; by eauto using signal_step|].
iSplitR "HΦ"; [iNext|by auto].
rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
iIntros "> _"; by iApply "Hr".
Qed.
Lemma wait_spec l P (Φ : val iProp) :
recv l P (P - Φ #()) WP wait #l {{ Φ }}.
Proof.
rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_load. iPvsIntro. destruct p.
- (* a Low state. The comparison fails, and we recurse. *)
iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
{ iNext. rewrite {2}/barrier_inv /=. by iFrame. }
iIntros "Hγ".
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "|==>[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). auto.
- (* a High state: the comparison succeeds, and we perform a transition and
return to the client *)
iExists (State High (I {[ i ]})), ( : set token).
iSplit; [iPureIntro; by eauto using wait_step|].
iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert ( Ψ i [ set] j I {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
iSplitL "HΨ' Hl Hsp"; [iNext|].
+ rewrite {2}/barrier_inv /=; iFrame "Hl".
iExists Ψ; iFrame. auto.
+ iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.
Lemma recv_split E l P1 P2 :
nclose N E recv l (P1 P2) ={E}=> recv l P1 recv l P2.
Proof.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iApply pvs_trans'.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
iPvs (saved_prop_alloc_strong _ (R1: %CF iProp) I) as (i1) "[% #Hi1]".
iPvs (saved_prop_alloc_strong _ (R2: %CF iProp) (I {[i1]}))
as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2; iPvsIntro.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iExists (State p ({[i1; i2]} I {[i]})).
iExists ({[Change i1; Change i2 ]}).
iSplit; [by eauto using split_step|iSplitL].
- iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto.
- iIntros "Hγ".
iAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I with "|==>[-]" as "[Hγ1 Hγ2]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver.
+ iApply (sts_own_weaken with "Hγ");
eauto using sts.closed_op, i_states_closed.
abstract set_solver. }
iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
+ iExists γ, P, R1, i1. iFrame; auto.
+ iExists γ, P, R2, i2. iFrame; auto.
Qed.
Lemma recv_weaken l P1 P2 : (P1 - P2) recv l P1 - recv l P2.
Proof.
rewrite /recv.
iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
iIntros "> HQ". by iApply "HP"; iApply "HP1".
Qed.
Lemma recv_mono l P1 P2 : (P1 P2) recv l P1 recv l P2.
Proof.
intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
Qed.
*)
End proof.
Typeclasses Opaque barrier_ctx send recv.
From fri.algebra Require Export sts.
From fri.program_logic Require Import ghost_ownership.
(** The STS describing the main barrier protocol. Every state has an index-set
associated with it. These indices are actually [gname], because we use them
with saved propositions. *)
Inductive phase := Low | High.
Record state := State { state_phase : phase; state_I : gset gname }.
Add Printing Constructor state.
Inductive token := Change (i : gname) | Send.
Global Instance stateT_inhabited: Inhabited state := populate (State Low ).
Global Instance Change_inj : Inj (=) (=) Change.
Proof. by injection 1. Qed.
Inductive prim_step : relation state :=
| ChangeI p I2 I1 : prim_step (State p I1) (State p I2)
| ChangePhase I : prim_step (State Low I) (State High I).
Definition tok (s : state) : set token :=
{[ t | i, t = Change i i state_I s ]}
(if state_phase s is High then {[ Send ]} else ).
Global Arguments tok !_ /.
Canonical Structure sts := sts.STS prim_step tok.
(* The set of states containing some particular i *)
Definition i_states (i : gname) : set state := {[ s | i state_I s ]}.
(* The set of low states *)
Definition low_states : set state := {[ s | state_phase s = Low ]}.
Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
Proof.
split; first (intros [[] I]; set_solver).
(* If we do the destruct of the states early, and then inversion
on the proof of a transition, it doesn't work - we do not obtain
the equalities we need. So we destruct the states late, because this
means we can use "destruct" instead of "inversion". *)
intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans as [[] ??|]; done || set_solver.
Qed.
Lemma low_states_closed : sts.closed low_states {[ Send ]}.
Proof.
split; first (intros [??]; set_solver).
intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans as [[] ??|]; done || set_solver.
Qed.
(* Proof that we can take the steps we need. *)
Lemma signal_step I : sts.steps (State Low I, {[Send]}) (State High I, ).
Proof. apply rtc_once. constructor; first constructor; set_solver. Qed.
Lemma wait_step i I :
i I
sts.steps (State High I, {[ Change i ]}) (State High (I {[ i ]}), ).
Proof.
intros. apply rtc_once.
constructor; first constructor; [set_solver..|].
apply elem_of_equiv=>-[j|]; last set_solver.
destruct (decide (i = j)); set_solver.
Qed.
Lemma split_step p i i1 i2 I :
i I i1 I i2 I i1 i2
sts.steps
(State p I, {[ Change i ]})
(State p ({[i1; i2]} I {[i]}), {[ Change i1; Change i2 ]}).
Proof.
intros. apply rtc_once. constructor; first constructor.
- destruct p; set_solver.
- destruct p; set_solver.
- apply elem_of_equiv=> /= -[j|]; last set_solver.
set_unfold; rewrite !(inj_iff Change).
assert (Change j match p with Low => | High => {[Send]} end False)
as -> by (destruct p; set_solver).
destruct (decide (i1 = j)) as [->|]; first naive_solver.
destruct (decide (i2 = j)) as [->|]; first naive_solver.
destruct (decide (i = j)) as [->|]; naive_solver.
Qed.
From fri.program_logic Require Export hoare.
From fri.heap_lang.lib.barrier Require Export barrier.
From fri.heap_lang.lib.barrier Require Import proof.
From fri.heap_lang Require Import proofmode.
Import uPred.