Commit 8612ca7a authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

More fixing.

parent 552cf701
......@@ -64,10 +64,11 @@ program_logic/model.v
program_logic/adequacy.v
program_logic/adequacy_inf.v
program_logic/hoare_lifting.v
program_logic/stepshifts.v
program_logic/pstepshifts.v
program_logic/lifting.v
program_logic/invariants.v
program_logic/viewshifts.v
program_logic/stepshifts.v
program_logic/wsat.v
program_logic/ownership.v
program_logic/weakestpre.v
......@@ -113,6 +114,7 @@ tests/proofmode.v
tests/barrier_client.v
proofmode/coq_tactics.v
proofmode/pviewshifts.v
proofmode/pstepshifts.v
proofmode/environments.v
proofmode/intro_patterns.v
proofmode/spec_patterns.v
......
......@@ -176,9 +176,22 @@ Definition cmra_update {A : cmraT} (x y : A) := ∀ n z,
Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
Definition cmra_supdateP {A: cmraT} (x: A) (y: A) (P Q: A Prop) := n z,
{n} (x y z) x' y', P x' Q y' {n} (x' y' z) x _(n) x'.
Instance: Params (@cmra_supdateP) 1.
Definition cmra_step_updateP {A : cmraT} (x : A) (xl: A) (P : A A Prop) := n z,
{n} (x xl z) y yl, P y yl {n} (y yl z) xl _(n) yl.
Instance: Params (@cmra_step_updateP) 1.
Notation "x # y ~~>>: P" := (cmra_step_updateP x y P) (at level 70).
Definition cmra_step_update {A : cmraT} (x xl y yl : A) := n z,
{n} (x xl z) {n} (y yl z) xl _(n) yl.
Notation "x # xl ~~>> y ## yl " := (cmra_step_update x xl y yl) (at level 70).
Lemma cmra_step_stepP {A: cmraT} (x xl y yl: A) :
x # xl ~~>> y ## yl (x # xl ~~>>: (λ x xl, y = x yl = xl)).
Proof.
split.
- by intros Hx n z ?; exists y, yl; destruct (Hx n z) as (?&?); auto.
- intros Hx n z ?. destruct (Hx n z) as (?&?&(<-&<-)&?); auto.
Qed.
Instance: Params (@cmra_step_update) 1.
(** * Properties **)
Section cmra.
......@@ -436,6 +449,17 @@ Qed.
Lemma cmra_update_id x : x ~~> x.
Proof. intro. auto. Qed.
(** ** Step updates *)
Lemma cmra_step_updateP_weaken (P Q : A A Prop) x xl:
x # xl ~~>>: P ( y yl, P y yl Q y yl) x # xl ~~>>: Q.
Proof.
intros Hs HPQ n z Hval.
edestruct (Hs n z Hval) as (y&yl&HP&Hval'&Hs').
exists y, yl. split_and!; eauto.
Qed.
Section unit_updates.
Context `{Empty A, !CMRAUnit A}.
Lemma cmra_update_unit x : x ~~> .
......@@ -502,6 +526,13 @@ Section cmra_transport.
Lemma cmra_transport_updateP' (P : A Prop) x :
x ~~>: P T x ~~>: λ y, y', y = cmra_transport H y' P y'.
Proof. eauto using cmra_transport_updateP. Qed.
Lemma cmra_transport_step_updateP (P : A A Prop) (Q : B B Prop) x xl :
x # xl ~~>>: P ( y yl, P y yl Q (T y) (T yl)) T x # T xl ~~>>: Q.
Proof. destruct H. eauto using cmra_step_updateP_weaken. Qed.
Lemma cmra_transport_step_updateP' (P : A A Prop) (Q : B B Prop) x xl :
x # xl ~~>>: P T x # T xl ~~>>: (λ y yl, y' yl', y = cmra_transport H y'
yl = cmra_transport H yl' P y' yl').
Proof. intros. eapply cmra_transport_step_updateP; eauto. Qed.
Lemma cmra_transport_sym_inv (x: A):
cmra_transport (eq_sym H) (cmra_transport H (x)) = x.
Proof.
......
......@@ -254,6 +254,15 @@ Section iprod_cmra.
Lemma iprod_singleton_updateP_empty' x (P : B x Prop) :
~~>: P ~~>: λ g, y2, g = iprod_singleton x y2 P y2.
Proof. eauto using iprod_singleton_updateP_empty. Qed.
(*
Lemma iprod_singleton_step_updateP x (P : B x B x Prop)
(Q : iprod B iprod B Prop) y1 yl1 :
y1 # yl1 ~~>>: P ( y2 yl2, P y2 yl2 Q (iprod_singleton x y2) (iprod_singleton x yl2))
iprod_singleton x y1 # iprod_singleton x yl1 ~~>>: Q.
Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP.
*)
End iprod_cmra.
Arguments iprodR {_ _ _} _.
......
......@@ -372,6 +372,16 @@ Infix "↔" := uPred_iff : uPred_scope.
Class TimelessP {M} (P : uPred M) := timelessP : P (P False).
Arguments timelessP {_} _ {_}.
(* Unfortunately, P and P are not timeless in this model. The
problem is that they involve an extra constraint on the linear part
which is not timeless. However, in the scope of a they become
timeless, since once we already know the affine part is empty,
these constraints become trivial. Therefore, we introduce the idea
of "Affine Timeless" to handle this *)
Class ATimelessP {M: cmraT} `{Empty M, !CMRAUnit M} (P : uPred M)
:= atimelessP : ⧆▷ P (P False).
Arguments atimelessP {_ _ _} _ {_}.
Class RelevantP {M} (P : uPred M) := relevantP : P P.
Arguments relevantP {_} _ {_}.
......@@ -652,6 +662,8 @@ Proof.
Qed.
Lemma equiv_iff P Q : P ⊣⊢ Q True (P Q).
Proof. intros ->; apply iff_refl. Qed.
Lemma equiv_iff' P Q : P ⊣⊢ Q Emp (P Q).
Proof. intros ->; apply iff_refl. Qed.
Lemma const_mono φ1 φ2 : (φ1 φ2) φ1 φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
......@@ -840,6 +852,14 @@ Proof.
exists x, x', y, y'; split_and?; auto.
eapply uPred_weaken with n x; eauto using cmra_validN_op_l.
Qed.
Lemma wand_intro_affine_r P Q R : (P Q) R P (Q - R).
Proof.
unseal=> HPQR. split=> n x y ?? Haffine; split; auto.
intros n' x' y' ????. apply HPQR; auto.
exists x, x', y, y'; split_and?; auto.
eapply uPred_weaken with n x; eauto using cmra_validN_op_l.
destruct Haffine; auto.
Qed.
Lemma wand_elim_l' P Q R : P (Q - R) (P Q) R.
Proof.
unseal =>HPQR. split; intros n x y ?? (?&?&?&?&?&?&?&?). cofe_subst.
......@@ -910,6 +930,8 @@ Proof.
Qed.
Lemma wand_intro_l P Q R : (Q P) R P (Q - R).
Proof. rewrite comm; apply wand_intro_r. Qed.
Lemma wand_intro_affine_l P Q R : (Q P) R P (Q - R).
Proof. rewrite comm; apply wand_intro_affine_r. Qed.
Lemma wand_elim_l P Q : ((P - Q) P) Q.
Proof. by apply wand_elim_l'. Qed.
Lemma wand_elim_r P Q : (P (P - Q)) Q.
......@@ -1320,6 +1342,26 @@ Lemma affine_affine_later P : (⧆ ▷ P) ⊣⊢ (⧆ ▷ ⧆P).
Proof. unseal. split=>-[|n] x y ??; auto.
simpl. split; intros; naive_solver eauto 2 using dist_le.
Qed.
Lemma affine_later_1 P : ( P) ( P).
Proof. rewrite affine_affine_later. rewrite affine_elim //=. Qed.
Lemma affine_later_distrib P Q: (⧆▷ (P Q) (⧆▷ P ⧆▷ Q)).
Proof.
unseal. split=>-[|n] x y ?? [HL ?]; auto; simpl.
- exists x, , , .
split_and!; rewrite ?right_id; auto.
- destruct HL as (x1&x2&y1&y2&?&?&(?&Hay1)&(?&Hay2)).
destruct (cmra_extend n x x1 x2)
as ([x1' x2']&Hx'&Hx1'&Hx2'); eauto using cmra_validN_S; simpl in *.
destruct (cmra_extend (S n) y )
as ([y1' y2']&Hy'&Hy1'&Hy2'); eauto using cmra_validN_S; simpl in *.
{ rewrite ?right_id; eauto using dist_le. }
exists x1', x2', y1', y2'; split_and!; auto.
* by rewrite Hx'.
* by rewrite Hy'.
* by rewrite Hx1' (dist_le _ _ _ _ Hy1') //= -?Hay1; last lia.
* by rewrite Hx2' (dist_le _ _ _ _ Hy2') //= -?Hay2; last lia.
Qed.
Lemma relevant_affine P : □⧆P ⊣⊢ ⧆□ P.
Proof.
apply (anti_symm ()).
......@@ -1331,6 +1373,16 @@ Proof.
split; auto. split; auto. rewrite -Heqy; auto.
Qed.
Lemma affine_relevant_later P: ⧆▷□P ⊣⊢ ⧆□▷ P.
Proof.
apply (anti_symm ()).
- unseal; auto; econstructor; intros n x y ??.
intros (HP&Haff). split; auto.
rewrite Haff in HP *. destruct n as [|n']; simpl; rewrite ?persistent; auto.
intros (HP&_). split; auto.
- apply affine_mono, relevant_later_1.
Qed.
(* Unlimited *)
Lemma unlimited_elim P : P P.
Proof.
......@@ -1798,6 +1850,115 @@ Proof.
cmra_timeless_included_l; eauto using cmra_validN_le.
Qed.
(* Affine Timeless *)
Lemma atimelessP_spec P : ATimelessP P n x, {n} x P 0 x P n x .
Proof.
split.
- intros HP n x ??; induction n as [|n]; auto.
move: HP; rewrite /ATimelessP; unseal=> /uPred_in_entails /(_ (S n) x ).
destruct 1 as [ HlP | HlF]; auto using cmra_validN_S, cmra_unit_validN.
* split; auto using cmra_validN_S, cmra_unit_validN.
* destruct HlP as (HP&?Haff). auto.
* simpl in *. exfalso; auto.
- move=> HP; rewrite /ATimelessP; unseal; split=> -[|n] x y /=; auto.
intros ?? (HP'&Haff). left.
split; auto. rewrite Haff.
apply HP, uPred_weaken with n x; eauto using cmra_validN_le, cmra_unit_validN.
rewrite -(dist_le _ _ _ _ Haff); auto.
Qed.
(* All timeless assertions are automatically affine timeless: *)
Lemma timeless_atimeless P: TimelessP P ATimelessP P.
Proof.
rewrite /TimelessP /ATimelessP. intros ->. rewrite ?affine_or.
apply or_mono; eauto using affine_elim.
Qed.
(* We could create an instance based on the above, but I will just directly
create ATimeless instances for all of the things we already know to be Timeless *)
Global Instance const_atimeless φ : ATimelessP ( φ : uPred M)%I.
Proof. apply timeless_atimeless; apply _. Qed.
Global Instance valid_atimeless {A : cmraT} `{CMRADiscrete A} (a : A) :
ATimelessP ( a : uPred M)%I.
Proof. apply timeless_atimeless; apply _. Qed.
Global Instance and_atimeless P Q: ATimelessP P ATimelessP Q ATimelessP (P Q).
Proof. rewrite /ATimelessP later_and ?affine_and or_and_r; apply and_mono. Qed.
Global Instance or_atimeless P Q : ATimelessP P ATimelessP Q ATimelessP (P Q).
Proof.
intros; rewrite /ATimelessP later_or ?affine_or (atimelessP _) (atimelessP Q); eauto 10.
Qed.
Global Instance impl_atimeless P Q : ATimelessP Q ATimelessP (P Q).
Proof.
rewrite !atimelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ?????; auto.
apply HP, HPQ, uPred_weaken with (S n') x'; eauto using cmra_validN_le.
Qed.
Global Instance sep_atimeless_1 P Q: TimelessP P TimelessP Q ATimelessP (P Q).
Proof.
intros; apply timeless_atimeless; apply _.
Qed.
Global Instance sep_atimeless_2 P Q:
AffineP P AffineP Q ATimelessP P ATimelessP Q ATimelessP (P Q).
Proof.
intros; rewrite /ATimelessP.
rewrite {1}(affineP P).
rewrite {1}(affineP Q).
rewrite affine_later_distrib.
rewrite (atimelessP P) (atimelessP Q).
rewrite sep_or_l. rewrite sep_or_r.
apply or_elim.
- apply or_elim.
* apply or_intro_l'. apply sep_affine_1.
* apply or_intro_r'. apply sep_elim_l.
- apply or_intro_r'. rewrite sep_or_r.
apply or_elim; first apply sep_elim_r.
unseal. split=> -[|n] x y ?? Hfalse /=; auto.
destruct Hfalse as (?&?&?&?&?&?&?&?). auto.
Qed.
Global Instance wand_atimeless P Q : AffineP P ATimelessP Q ATimelessP (P - Q).
Proof.
rewrite !atimelessP_spec.
unseal=> HA HP [|n] x ? HPQ [|n'] x' y' ??? HP'; auto.
apply affineP in HP'; eauto using cmra_validN_op_r.
revert HP'. unseal.
intros (HP'&Haff).
rewrite Haff ?right_id.
apply HP; auto.
specialize (HPQ 0 x' ). rewrite ?left_id in HPQ *=> HPQ.
eapply HPQ;
eauto 3 using cmra_validN_le, cmra_validN_op_r, cmra_validN_op_l, cmra_included_l.
apply uPred_weaken with (S n') x';
eauto 3 using cmra_validN_le, cmra_validN_op_r, cmra_validN_op_l, cmra_included_l.
rewrite -Haff. eauto.
Qed.
Global Instance forall_atimeless {A} (Ψ : A uPred M) :
( x, ATimelessP (Ψ x)) ATimelessP ( x, Ψ x).
Proof. by setoid_rewrite atimelessP_spec; unseal=> HΨ n x ?? a; apply HΨ. Qed.
Global Instance exist_atimeless {A} (Ψ : A uPred M) :
( x, ATimelessP (Ψ x)) ATimelessP ( x, Ψ x).
Proof.
by setoid_rewrite atimelessP_spec; unseal=> HΨ [|n] x ?;
[|intros [a ?]; exists a; apply HΨ].
Qed.
Global Instance relevant_atimeless P : ATimelessP P ATimelessP ( P).
Proof.
intros ?; rewrite /ATimelessP.
rewrite affine_relevant_later.
rewrite -relevant_affine atimelessP relevant_or relevant_affine.
apply or_mono; auto using relevant_elim.
Qed.
Global Instance affine_atimeless P : ATimelessP P ATimelessP ( P).
Proof.
rewrite /ATimelessP. intros HP.
by rewrite -affine_affine_later HP affine_affine0.
Qed.
Global Instance eq_atimeless {A : cofeT} (a b : A) :
Timeless a ATimelessP (a b : uPred M)%I.
Proof. intros. apply timeless_atimeless; apply _. Qed.
Global Instance ownM_atimeless (a : M) : Timeless a ATimelessP (uPred_ownM a).
Proof. intros. apply timeless_atimeless; apply _. Qed.
(* Relevance *)
Global Instance emp_relevant: RelevantP (Emp)%I.
Proof.
......@@ -1917,6 +2078,8 @@ Proof. rewrite -(affine_affine P). rewrite ?affine_equiv; auto. Qed.
Lemma sep_affine_distrib P Q `{!AffineP P, !AffineP Q}:
( P Q) ⊣⊢ (P Q).
Proof. rewrite ?affine_affine. auto. Qed.
Lemma affine_later_distrib' P Q `{!AffineP P, !AffineP Q}: (⧆▷ (P Q) (⧆▷ P ⧆▷ Q)).
Proof. by rewrite -{1}(affine_affine P) -{1}(affine_affine Q) affine_later_distrib. Qed.
Lemma affine_sep_elim_l' P Q R `{!AffineP Q}: P R (P Q) R.
Proof. rewrite -(affine_affine Q); auto. Qed.
Lemma affine_sep_elim_r' P Q R `{!AffineP P}: Q R (P Q) R.
......
From iris.algebra Require Export auth upred_tactics.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.proofmode Require Import invariants ghost_ownership pstepshifts.
Import uPred.
(* The CMRA we need. *)
Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
auth_inG :> inG Λ Σ (mapR gname (authR A));
auth_inG :> inG Λ Σ (gmapR gname (authR A));
auth_identity :> CMRAUnit A;
auth_timeless :> CMRADiscrete A;
}.
(* The Functor we need. *)
Definition authGF (A : cmraT) : gFunctor := GFunctor (mapRF gname (constRF (authR A))).
Definition authGF (A : cmraT) : gFunctor := GFunctor (gmapRF gname (constRF (authR A))).
(* Show and register that they match. *)
Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
`{CMRAUnit A, CMRADiscrete A} : authG Λ Σ A.
......@@ -21,7 +21,7 @@ Section definitions.
Definition auth_own (a : A) : iPropG Λ Σ :=
own γ ( a).
Definition auth_inv (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
( a, own γ ( a) φ a)%I.
( a, own γ ( a) φ a)%I.
Definition auth_ctx (N : namespace) (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
inv N (auth_inv φ).
......@@ -29,9 +29,9 @@ Section definitions.
Proof. solve_proper. Qed.
Global Instance auth_own_proper : Proper (() ==> (⊣⊢)) auth_own.
Proof. solve_proper. Qed.
Global Instance auth_own_timeless a : TimelessP (auth_own a).
Global Instance auth_own_atimeless a : ATimelessP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_ctx_persistent N φ : PersistentP (auth_ctx N φ).
Global Instance auth_ctx_relevant N φ : RelevantP (auth_ctx N φ).
Proof. apply _. Qed.
End definitions.
......@@ -51,39 +51,72 @@ Section auth.
Lemma auth_own_op γ a b :
auth_own γ (a b) ⊣⊢ (auth_own γ a auth_own γ b).
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Lemma auth_own_valid γ a : auth_own γ a a.
Lemma auth_own_valid γ a : auth_own γ a a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Existing Instance coq_tactics.envs_dom.
Lemma auth_alloc N E a :
a nclose N E
φ a (|={E}=> γ, auth_ctx γ N φ auth_own γ a).
φ a (|={E}=> γ, auth_ctx γ N φ auth_own γ a).
Proof.
iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']"); first done.
{ iNext. iExists a. by iFrame "Hφ". }
iPvsIntro; iExists γ; by iFrame "Hγ'".
iPoseProof (own_alloc (Auth (Excl a) a)) as "Hγ_pre"; first done.
rewrite affine_elim.
iPvs "Hγ_pre" as {γ} "Hγ"; iRevert "Hγ"; rewrite auth_both_op.
iIntros "(Hγ&Hγ')".
iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']") as "Hinv"; first done.
{ rewrite /auth_inv. rewrite later_exist affine_exist. iExists a.
unfold own.
apply affine_intro; first apply _.
rewrite later_sep.
iSplitL "Hγ".
* iNext; auto.
* rewrite affine_affine_later affine_elim. auto.
}
(*
{ unfold own.
rewrite -affine_affine_later.
apply affine_intro; first apply _. rewrite affine_elim. iNext.
iExists a. by iFrame "Hφ". }
*)
iPvsIntro. iExists γ. iSplit.
- unfold own. iClear "Hγ'". auto.
- iClear "Hinv". auto.
Qed.
Lemma auth_empty γ E : True |={E}=> auth_own γ .
Lemma auth_empty γ E : Emp |={E}=> auth_own γ .
Proof. by rewrite -own_empty. Qed.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
Lemma auth_fsa E N (Ψ : V iPropG Λ Σ) γ a :
fsaV nclose N E
(auth_ctx γ N φ auth_own γ a a',
(auth_ctx γ N φ auth_own γ a a',
(a a') φ (a a') -
fsa (E nclose N) (λ x, L Lv (Hup : LocalUpdate Lv L),
(Lv a (L a a')) φ (L a a')
(auth_own γ (L a) - Ψ x)))
fsa E Ψ.
Proof.
iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv N as {a'} "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
iDestruct (own_valid _ with "Hγ !") as "Hvalid".
iIntros {??} "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as "Hinv'".
rewrite {2}/auth_inv.
rewrite {1}later_exist.
rewrite {1}affine_exist.
iDestruct "Hinv'" as {a'} "Hinv'".
rewrite affine_later_distrib'.
iDestruct "Hinv'" as "(Hγ&Hφ)".
iTimeless "Hγ" (own γ ( a')).
iTimeless "Hγf" (own γ ( a)).
rewrite affine_elim.
rewrite affine_elim.
iCombine "Hγ" "Hγf" as "Hγ".
iPoseProof (own_valid_r _ with "Hγ") as "Hγval".
iDestruct "Hγval" as "(Hγ&#Hvalid)".
Check auth_validI.
Set Printing Implicits.
Unset Printing Notations.
iDestruct (proj1 (auth_validI _)) as "FOO".
iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
......
From iris.program_logic Require Import language.
From iris.prelude Require Import sets irelations.
Section chunk_lang.
Context (L: language).
Definition chunk_expr := list (option (expr L)).
Definition chunk_state := state L.
End chunk_lang.
......@@ -69,11 +69,24 @@ Section delayed_lang.
| _, _ => None
end.
Inductive delayed_atomic: delayed_expr Prop :=
(* The delayed language is not actually _used_ as an instantiated language in Iris,
it is purely a device for the refinement monoid, so I don't care too much to show
this is decidable *)
Inductive delayed_atomic': delayed_expr Prop :=
| delayed_succ_minimal_atomic:
v p, (exists p', plt p' p)
( p', plt p' p minimal p')
delayed_atomic (of_val v, p).
delayed_atomic' (of_val v, p).
Require ClassicalDescription.
Definition delayed_atomic: delayed_expr bool.
Proof.
intros e.
destruct (ClassicalDescription.excluded_middle_informative (delayed_atomic' e)).
- exact true.
- exact false.
Defined.
Inductive delayed_prim_step:
delayed_expr delayed_state delayed_expr delayed_state option (delayed_expr) Prop :=
......@@ -120,11 +133,22 @@ Section delayed_lang.
Lemma delayed_atomic_not_val:
e, delayed_atomic e delayed_to_val e = None.
Proof.
induction 1 as [v p Hpred].
intros e DA. unfold delayed_atomic in DA.
destruct (ClassicalDescription.excluded_middle_informative) as [d | nd]; last (exfalso; auto).
induction d as [v p Hpred].
unfold delayed_to_val.
simpl. rewrite to_of_val. destruct (minimal_dec p); auto.
exfalso; eauto.
Qed.
Lemma delayed_atomic_equiv:
e, delayed_atomic e = true delayed_atomic' e.
Proof.
intros e. unfold delayed_atomic.
destruct (ClassicalDescription.excluded_middle_informative) as [d | nd];
last (intros; congruence).
auto.
Qed.
Lemma delayed_atomic_step: e1 σ1 e2 σ2 ef,
delayed_atomic e1
......@@ -133,12 +157,18 @@ Section delayed_lang.
Proof.
intros e1 σ1 e2 σ2 ef Hda Hdps.
inversion Hdps; subst.
- inversion Hda as [v p'' Hnm Hpred].
- unfold delayed_atomic in Hda.
destruct (ClassicalDescription.excluded_middle_informative) as [Hda' | nd];
last (exfalso; auto).
inversion Hda' as [v p'' Hnm Hpred].
subst. exfalso.
assert (to_val (of_val v) = None) as HtoNone.
{ eapply val_stuck. eauto. }
rewrite to_of_val in HtoNone; congruence.
- inversion Hda as [v p'' Hnm Hpred]. subst.
- unfold delayed_atomic in Hda.
destruct (ClassicalDescription.excluded_middle_informative) as [Hda' | nd];
last (exfalso; auto).
inversion Hda' as [v p'' Hnm Hpred]. subst.
unfold delayed_to_val. rewrite to_of_val.
destruct minimal_dec; simpl; eauto.
simpl in *. exfalso. eapply Hpred; eauto.
......@@ -530,7 +560,6 @@ Section delayed_lang.
* exists i. econstructor. eauto.
Qed.
Require ClassicalDescription.
Lemma erase_trace:
(c: cfg delayed_lang) (e: trace (idx_step) c),
......
......@@ -11,7 +11,7 @@ Implicit Types v : val.
Implicit Types e : expr.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Notation wp_fork ef := (default True ef (flip (wp ) (λ _, True)))%I.
Notation wp_fork ef := (default Emp ef (flip (wp ) (λ _, uPred_stopped)))%I.
Lemma wp_ectx_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
......@@ -22,8 +22,8 @@ Lemma wp_lift_head_step E1 E2
E2 E1 to_val e1 = None
head_reducible e1 σ1
( e2 σ2 ef, head_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
(|={E1,E2}=> ownP σ1 e2 σ2 ef,
( φ e2 σ2 ef ownP σ2) - |={E2,E1}=> WP e2 @ E1 {{ Φ }} wp_fork ef)
(|={E1,E2}=> ownP σ1 e2 σ2 ef,
( φ e2 σ2 ef ownP σ2) - |={E2,E1}=>> WP e2 @ E1 {{ Φ }} wp_fork ef)
WP e1 @ E1 {{ Φ }}.
Proof. eauto using wp_lift_step. Qed.
......@@ -31,7 +31,7 @@ Lemma wp_lift_pure_head_step E (φ : expr → option expr → Prop) Φ e1 :
to_val e1 = None
( σ1, head_reducible e1 σ1)
( σ1 e2 σ2 ef, head_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
( e2 ef, φ e2 ef WP e2 @ E {{ Φ }} wp_fork ef) WP e1 @ E {{ Φ }}.
( e2 ef, φ e2 ef - |={E}=>> WP e2 @ E {{ Φ }} wp_fork ef) WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_pure_step. Qed.
Lemma wp_lift_atomic_head_step {E Φ} e1
......@@ -40,7 +40,7 @@ Lemma wp_lift_atomic_head_step {E Φ} e1
head_reducible e1 σ1
( e2 σ2 ef,
head_step e1 σ1 e2 σ2 ef φ e2 σ2 ef)
( ownP σ1 v2 σ2 ef, φ (of_val v2) σ2 ef ownP σ2 - Φ v2 wp_fork ef)
( ownP σ1 v2 σ2 ef, φ (of_val v2) σ2 ef ownP σ2 - |={E}=>> Φ v2 wp_fork ef)
WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_atomic_step. Qed.
......@@ -49,13 +49,13 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
head_reducible e1 σ1
( e2' σ2' ef', head_step e1 σ1 e2' σ2' ef'
σ2 = σ2' to_val e2' = Some v2 ef = ef')
( ownP σ1 (ownP σ2 - Φ v2 wp_fork ef)) WP e1 @ E {{ Φ }}.
( ownP σ1 (ownP σ2 - |={E}=>> Φ v2 wp_fork ef)) WP e1 @ E {{ Φ }}.
Proof. eauto using wp_lift_atomic_det_step. Qed.