Skip to content
Snippets Groups Projects
Commit a01925c4 authored by Filip Sieczkowski's avatar Filip Sieczkowski
Browse files

Simplified some def's, proved more lemmas (box, composition of ghosts, 

more view-shifts), stated lemmas about hoare triples.
parent 0de5b6a9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 394 additions and 167 deletions
iris.v
+ 394
− 167
View file @ a01925c4
......@@ -156,6 +156,53 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
| None => ⊥
end.
Lemma ores_equiv_eq (r1 r2 : option res) (HEq : r1 == r2) : r1 = r2.
Proof.
destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction;
simpl in HEq; subst; reflexivity.
Qed.
(** Lemmas about box **)
Lemma box_intro p q (Hpq : □ p ⊑ q) :
□ p ⊑ □ q.
Proof.
intros w n r Hp; simpl; apply Hpq, Hp.
Qed.
Lemma box_elim p :
□ p ⊑ p.
Proof.
intros w n r Hp; simpl in Hp.
eapply uni_pred, Hp; [reflexivity |].
exists r; now erewrite comm, pcm_op_unit by apply _.
Qed.
(** Ghost state ownership **)
Lemma ownL_sc (u t : option RL.res) :
ownL (u · t)%pcm == ownL u * ownL t.
Proof.
intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
- destruct (u · t)%pcm as [ut |] eqn: EQut; [| contradiction].
do 13 red in Hut; rewrite <- Hut.
destruct u as [u |]; [| now erewrite pcm_op_zero in EQut by apply _].
assert (HT := comm (Some u) t); rewrite EQut in HT.
destruct t as [t |]; [| now erewrite pcm_op_zero in HT by apply _]; clear HT.
exists (pcm_unit RP.res, u) (pcm_unit RP.res, t).
split; [unfold pcm_op, res_op, pcm_op_prod | split; do 13 red; reflexivity].
now erewrite pcm_op_unit, EQut by apply _.
- destruct u as [u |]; [| contradiction]; destruct t as [t |]; [| contradiction].
destruct Hu as [ru EQu]; destruct Ht as [rt EQt].
rewrite <- EQt, assoc, (comm (Some r1)) in EQr.
rewrite <- EQu, assoc, <- (assoc (Some rt · Some ru)%pcm) in EQr.
unfold pcm_op at 3, res_op at 4, pcm_op_prod at 1 in EQr.
erewrite pcm_op_unit in EQr by apply _; clear EQu EQt.
destruct (Some u · Some t)%pcm as [ut |];
[| now erewrite comm, pcm_op_zero in EQr by apply _].
destruct (Some rt · Some ru)%pcm as [rut |];
[| now erewrite pcm_op_zero in EQr by apply _].
exists rut; assumption.
Qed.
Section Erasure.
Local Open Scope pcm_scope.
Local Open Scope bi_scope.
......@@ -208,11 +255,11 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Global Instance preo_unit : preoType () := disc_preo ().
Program Definition erasure (σ : state) (m : mask) (r s : res) (w : Wld) : UPred () :=
Program Definition erasure (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
▹ (mkUPred (fun n _ =>
erase_state (option_map fst (Some r · Some s)) σ
erase_state (option_map fst (r · s)) σ
/\ exists rs : nat -f> res,
erase rs == Some s /\
erase rs == s /\
forall i (Hm : m i),
(i ∈ dom rs <-> i ∈ dom w) /\
forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
......@@ -222,9 +269,10 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
setoid_rewrite HLe; eassumption.
Qed.
Global Instance erasure_equiv σ : Proper (meq ==> eq ==> eq ==> equiv ==> equiv) (erasure σ).
Global Instance erasure_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv ==> equiv) (erasure σ).
Proof.
intros m1 m2 EQm r r' EQr s s' EQs w1 w2 EQw [| n] []; [reflexivity |]; subst r' s'.
intros m1 m2 EQm r r' EQr s s' EQs w1 w2 EQw [| n] []; [reflexivity |];
apply ores_equiv_eq in EQr; apply ores_equiv_eq in EQs; subst r' s'.
split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
- split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
......@@ -263,25 +311,31 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Open Scope pcm_scope.
Local Obligation Tactic := intros.
Lemma erasure_not_empty σ m r s w k (HN : r · s == 0) :
~ erasure σ m r s w @ S k.
Proof.
intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
now apply erase_state_nonzero in HD.
Qed.
Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
mkUPred (fun n r => forall w1 rf rr s mf σ k (HSub : w ⊑ w1) (HLe : k < n)
(HD : mf # m1 ∪ m2) (HEq : Some r · Some rf == Some rr)
(HE : erasure σ (m1 ∪ mf) rr s w1 @ S k),
exists w2 r' rr' s',
w1 ⊑ w2 /\ p w2 (S k) r' /\ Some r' · Some rf == Some rr'
/\ erasure σ (m2 ∪ mf) rr' s' w2 @ S k) _.
mkUPred (fun n r => forall w1 rf s mf σ k (HSub : w ⊑ w1) (HLe : k < n)
(HD : mf # m1 ∪ m2)
(HE : erasure σ (m1 ∪ mf) (Some r · rf) s w1 @ S k),
exists w2 r' s',
w1 ⊑ w2 /\ p w2 (S k) r'
/\ erasure σ (m2 ∪ mf) (Some r' · rf) s' w2 @ S k) _.
Next Obligation.
intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
rewrite <- HR, (comm (Some rd)), <- assoc in HEq; clear r2 HR.
destruct (Some rd · Some rf) as [rf' |] eqn: HR;
[| erewrite comm, pcm_op_zero in HEq by apply _; contradiction].
destruct (HP w1 rf' rr s mf σ k) as [w2 [r1' [rr' [s' [HW [HP' [HR' HE'] ] ] ] ] ] ]; try assumption; [|].
- eauto with arith.
- rewrite <- HR, assoc in HR'; clear rf' HR HEq HP.
destruct (Some r1' · Some rd) as [r2' |] eqn: HR;
[| erewrite pcm_op_zero in HR' by apply _; contradiction].
exists w2 r2' rr' s'; split; [assumption | split; [| split; assumption] ].
eapply uni_pred, HP'; [| exists rd; rewrite comm, HR]; reflexivity.
destruct (HP w1 (Some rd · rf) s mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ];
try assumption; [now eauto with arith | |].
- eapply erasure_equiv, HE; try reflexivity.
rewrite assoc, (comm (Some r1)), HR; reflexivity.
- rewrite assoc, (comm (Some r1')) in HE'.
destruct (Some rd · Some r1') as [r2' |] eqn: HR';
[| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
exists w2 r2' s'; split; [assumption | split; [| assumption] ].
eapply uni_pred, HP'; [| exists rd; rewrite HR']; reflexivity.
Qed.
Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
......@@ -297,19 +351,19 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros.
- symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
edestruct HP as [w1'' [r' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
exists (extend w1'' w2') r' s'; split; [assumption | split].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
- assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
edestruct HP as [w1'' [r' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
exists (extend w1'' w2') r' s'; split; [assumption | split].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
Qed.
......@@ -324,10 +378,10 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Qed.
Next Obligation.
intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
- edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
- edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
clear HP; repeat (eexists; try eassumption); [].
apply EQp; [now eauto with arith | assumption].
- edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
- edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
clear HP; repeat (eexists; try eassumption); [].
apply EQp; [now eauto with arith | assumption].
Qed.
......@@ -358,30 +412,21 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
destruct HE as [HES [rs [HE HM] ] ].
destruct (rs i) as [ri |] eqn: HLr.
- rewrite erase_remove with (i := i) (r := ri) in HE by assumption.
destruct (Some rr · Some s) as [ss |] eqn: HR; setoid_rewrite HR in HES;
[| contradiction (erase_state_nonzero _ HES) ].
destruct (Some r · Some rf) as [rr' |] eqn: HR1;
[simpl in HEq; subst rr' | contradiction].
destruct (Some ri · erase (fdRemove i rs)) as [s' |] eqn: HR2;
[simpl in HE; subst s' | contradiction].
assert (HEq : Some r · Some ri · Some rf · erase (fdRemove i rs) == Some ss).
{ rewrite <- (assoc (Some r)), (comm (Some ri)), assoc, HR1, <- assoc, HR2, HR; reflexivity. }
clear HR HR1 HR2; destruct (Some r · Some ri) as [rri |] eqn: HR1;
[| now erewrite !pcm_op_zero in HEq by apply _].
destruct (Some rri · Some rf) as [rr' |] eqn: HR2;
[| now erewrite pcm_op_zero in HEq by apply _].
destruct (erase (fdRemove i rs)) as [s' |] eqn: HRS;
[| now erewrite comm, pcm_op_zero in HEq by apply _].
exists w' rri rr' s'; split; [reflexivity | split; [| split; [rewrite HR2; reflexivity | split] ] ].
assert (HR : Some r · rf · s == Some r · Some ri · rf · erase (fdRemove i rs))
by (rewrite <- HE, assoc, <- (assoc (Some r)), (comm rf), assoc; reflexivity).
apply ores_equiv_eq in HR; setoid_rewrite HR in HES; clear HR.
destruct (Some r · Some ri) as [rri |] eqn: HR;
[| erewrite !pcm_op_zero in HES by apply _; now apply erase_state_nonzero in HES].
exists w' rri (erase (fdRemove i rs)); split; [reflexivity |].
split; [| split; [assumption |] ].
+ simpl; eapply HInv; [now auto with arith |].
specialize (HSub i); rewrite HLu in HSub.
eapply uni_pred, HM with i; [| exists r; rewrite <- HR1 | | | rewrite HLr]; try reflexivity; [|].
eapply uni_pred, HM with i;
[| exists r; rewrite <- HR | | | rewrite HLr]; try reflexivity; [|].
* left; unfold mask_sing, mask_set.
destruct (Peano_dec.eq_nat_dec i i); tauto.
* symmetry; destruct (w' i); [assumption | contradiction].
+ destruct (Some rr' · Some s') as [ss' |] eqn: HR; [| contradiction].
setoid_rewrite HR; simpl in HEq; subst; assumption.
+ exists (fdRemove i rs); split; [rewrite HRS; reflexivity | intros j Hm].
* specialize (HSub i); rewrite HLu in HSub.
symmetry; destruct (w' i); [assumption | contradiction].
+ exists (fdRemove i rs); split; [reflexivity | intros j Hm].
destruct Hm as [| Hm]; [contradiction |]; specialize (HD j); simpl in HD.
unfold mask_sing, mask_set in HD; destruct (Peano_dec.eq_nat_dec i j);
[subst j; contradiction HD; tauto | clear HD].
......@@ -393,7 +438,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
destruct (Peano_dec.eq_nat_dec i i); tauto.
Qed.
(*Lemma vsClose i p :
Lemma vsClose i p :
valid (vs mask_emp (mask_sing i) (inv i p * ▹ p) ⊤).
Proof.
intros pw nn r w _; clear r pw.
......@@ -402,38 +447,51 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
apply ı in HInv; rewrite (isoR p) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
destruct k as [| k]; [now inversion HGt |].
destruct HE as [HES [rs [HE HM] ] ].
exists w' 1 (r · s); split; [reflexivity | split; [exact I |] ].
split; [erewrite pcm_op_unit, assoc, (comm rf) by apply _; assumption |].
remember (match rs i with Some ri => ri | None => 1 end) as ri eqn: EQri.
exists (fdUpdate i (ri · r) rs); split; intros.
- clear -HE EQri; destruct (rs i) as [rsi |] eqn: EQrsi; subst;
[erewrite erase_insert_old; [reflexivity | assumption] |].
erewrite pcm_op_unit, erase_insert_new; [reflexivity | assumption | apply _].
- specialize (HD i0); unfold mask_sing, mask_set in *; simpl in Hm, HD.
destruct (Peano_dec.eq_nat_dec i i0); [subst i0; clear Hm | destruct Hm as [Hm | Hm]; [contradiction |] ].
+ split; intros.
* specialize (HSub i); rewrite HLu in HSub.
rewrite !fdLookup_in_strong, fdUpdate_eq; destruct (w' i);
[intuition now eauto | contradiction].
* rewrite fdUpdate_eq in HLrs; simpl in HLrs; subst ri0.
destruct n as [| n]; [now inversion HLe |]; simpl in HP.
rewrite <- HSub; specialize (HSub i); rewrite HLu in HSub.
destruct (w' i) as [π' |]; [| contradiction]; simpl in HSub, HLw.
rewrite <- HLw, <- HSub; apply HInv; [now auto with arith |].
eapply uni_pred, HP; [now auto with arith |].
subst r; rewrite assoc; eexists; reflexivity.
+ rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption.
auto.
Qed.*)
exists w' (pcm_unit _) (Some r · s); split; [reflexivity | split; [exact I |] ].
assert (HR' : Some r · rf · s = rf · (Some r · s))
by (apply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
setoid_rewrite HR' in HES; erewrite pcm_op_unit by apply _.
split; [assumption |].
remember (match rs i with Some ri => ri | None => pcm_unit _ end) as ri eqn: EQri.
destruct (Some ri · Some r) as [rri |] eqn: EQR.
- exists (fdUpdate i rri rs); split; [| intros j Hm].
+ symmetry; rewrite <- HE; clear - EQR EQri; destruct (rs i) as [rsi |] eqn: EQrsi; subst;
[eapply erase_insert_old; [eassumption | rewrite <- EQR; reflexivity] |].
erewrite pcm_op_unit in EQR by apply _; rewrite EQR.
now apply erase_insert_new.
+ specialize (HD j); unfold mask_sing, mask_set in *; simpl in Hm, HD.
destruct (Peano_dec.eq_nat_dec i j);
[subst j; clear Hm |
destruct Hm as [Hm | Hm]; [contradiction | rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption; now auto] ].
rewrite !fdLookup_in_strong, fdUpdate_eq.
destruct n as [| n]; [now inversion HLe | simpl in HP].
rewrite HSub in HP; specialize (HSub i); rewrite HLu in HSub.
destruct (w' i) as [π' |]; [| contradiction].
split; [intuition now eauto | intros].
simpl in HLw, HLrs, HSub; subst ri0; rewrite <- HLw, <- HSub.
apply HInv; [now auto with arith |].
eapply uni_pred, HP; [now auto with arith |].
assert (HT : Some ri · Some r1 · Some r2 == Some rri)
by (rewrite <- EQR, <- HR, assoc; reflexivity); clear - HT.
destruct (Some ri · Some r1) as [rd |];
[| now erewrite pcm_op_zero in HT by apply _].
exists rd; assumption.
- destruct (rs i) as [rsi |] eqn: EQrsi; subst;
[| erewrite pcm_op_unit in EQR by apply _; discriminate].
contradiction (erase_state_nonzero σ); clear - HE HES EQrsi EQR.
assert (HH : rf · (Some r · s) = 0); [clear HES | rewrite HH in HES; assumption].
apply ores_equiv_eq; rewrite <- HE, erase_remove by eassumption.
rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
erewrite !pcm_op_zero by apply _; reflexivity.
Qed.
Lemma vsTrans p q r m1 m2 m3 (HMS : m2 ⊆ m1 ∪ m3) :
vs m1 m2 p q ∧ vs m2 m3 q r ⊑ vs m1 m3 p r.
Proof.
intros w' n r1 [Hpq Hqr] w HSub; specialize (Hpq _ HSub); rewrite HSub in Hqr; clear w' HSub.
intros np rp HLe HS Hp w1; intros; specialize (Hpq _ _ HLe HS Hp).
edestruct Hpq as [w2 [rq [rrq [sq [HSw12 [Hq [HEq' HErq] ] ] ] ] ] ]; try eassumption; [|].
edestruct Hpq as [w2 [rq [sq [HSw12 [Hq HEq] ] ] ] ]; try eassumption; [|].
{ (* XXX: possible lemma *)
clear - HD HMS.
intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
......@@ -441,7 +499,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
}
clear HS; assert (HS : pcm_unit _ ⊑ rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [rrR [sR [HSw23 [Hr [HR HEr] ] ] ] ] ] ];
edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [sR [HSw23 [Hr HEr] ] ] ] ];
try (reflexivity || eassumption); [now auto with arith | |].
{ (* XXX: possible lemma *)
clear - HD HMS.
......@@ -457,29 +515,32 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Proof.
intros w' n r1 Himp w HSub; rewrite HSub in Himp; clear w' HSub.
intros np rp HLe HS Hp w1; intros.
exists w1 rp rr s; split; [reflexivity | split; [| split; assumption ] ].
exists w1 rp s; split; [reflexivity | split; [| assumption ] ].
eapply Himp; [assumption | now eauto with arith | exists rp; now erewrite comm, pcm_op_unit by apply _ |].
unfold lt in HLe0; rewrite HLe0, <- HSub; assumption.
Qed.
(* Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
vs m1 m2 p q ⊑ vs (m1 ∪ mf) (m2 ∪ mf) (p * r) (q * r).
Proof.
intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
intros np rpr HLe _ [rp [rr [HR [Hp Hr] ] ] ] w'; intros.
assert (HS : 1 ⊑ rp) by (exists rp; erewrite comm, pcm_op_unit by apply _; reflexivity).
specialize (HVS _ _ HLe HS Hp w' s (rr · rf) (mf ∪ mf0) σ k); clear HS.
assert (HS : pcm_unit _ ⊑ rp) by (exists rp; now erewrite comm, pcm_op_unit by apply _).
specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) s (mf ∪ mf0) σ k); clear HS.
destruct HVS as [w'' [rq [s' [HSub' [Hq HEq] ] ] ] ]; try assumption; [| |].
- (* disjointness: possible lemma *)
- (* disjointness of masks: possible lemma *)
clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
eapply HD; split; [eassumption | tauto].
- rewrite assoc, HR; eapply erasure_equiv, HE; try reflexivity; [].
clear; intros i; tauto.
- exists w'' (rq · rr) s'; split; [assumption | split].
+ rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr; now auto.
+ rewrite <- assoc; eapply erasure_equiv, HEq; try reflexivity; [].
- rewrite assoc in HEq; destruct (Some rq · Some rr) as [rqr |] eqn: HR';
[| apply erasure_not_empty in HEq; [contradiction | now erewrite !pcm_op_zero by apply _] ].
exists w'' rqr s'; split; [assumption | split].
+ unfold lt in HLe0; rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr.
rewrite HR'; split; now auto.
+ eapply erasure_equiv, HEq; try reflexivity; [].
clear; intros i; tauto.
Qed.*)
Qed.
Lemma vsFalse m1 m2 :
valid (vs m1 m2 ⊥ ⊥).
......@@ -488,7 +549,84 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros n r _ _ HB; contradiction.
Qed.
(* XXX missing statements: NewInv, NewGhost, GhostUpd, VSTimeless *)
Global Instance nat_type : Setoid nat := discreteType.
Global Instance nat_metr : metric nat := discreteMetric.
Global Instance nat_cmetr : cmetric nat := discreteCMetric.
Program Definition inv' m : Props -n> {n : nat | m n} -n> Props :=
n[(fun p => n[(fun n => inv n p)])].
Next Obligation.
intros i i' EQi; simpl in EQi; rewrite EQi; reflexivity.
Qed.
Next Obligation.
intros i i' EQi; destruct n as [| n]; [apply dist_bound |].
simpl in EQi; rewrite EQi; reflexivity.
Qed.
Next Obligation.
intros p1 p2 EQp i; simpl morph.
apply (morph_resp (inv (` i))); assumption.
Qed.
Next Obligation.
intros p1 p2 EQp i; simpl morph.
apply (inv (` i)); assumption.
Qed.
Lemma fresh_region (w : Wld) m (HInf : mask_infinite m) :
exists i, m i /\ w i = None.
Proof.
destruct (HInf (S (List.last (dom w) 0%nat))) as [i [HGe Hm] ];
exists i; split; [assumption |]; clear - HGe.
rewrite <- fdLookup_notin_strong.
destruct w as [ [| [n v] w] wP]; unfold dom in *; simpl findom_t in *; [tauto |].
simpl List.map in *; rewrite last_cons in HGe.
unfold ge in HGe; intros HIn; eapply Gt.gt_not_le, HGe.
apply Le.le_n_S, SS_last_le; assumption.
Qed.
(* XXX: move up to definitions *)
Definition injProp (P : Prop) : Props :=
pcmconst (up_cr (const P)).
Instance LP_mask m : LimitPreserving m.
Proof.
intros σ σc Hp; apply Hp.
Qed.
Lemma vsNewInv p m (HInf : mask_infinite m) :
valid (vs m m (▹ p) (xist (inv' m p))).
Proof.
intros pw nn r w _; clear r pw.
intros n r _ _ HP w'; clear nn; intros.
destruct n as [| n]; [now inversion HLe | simpl in HP].
rewrite HSub in HP; clear w HSub; rename w' into w.
destruct (fresh_region w m HInf) as [i [Hm HLi] ].
assert (HSub : w ⊑ fdUpdate i (ı' p) w).
{ intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
now rewrite fdUpdate_neq by assumption.
}
exists (fdUpdate i (ı' p) w) (pcm_unit _) (Some r · s); split; [assumption | split].
- exists (exist _ i Hm); do 16 red.
unfold proj1_sig; rewrite fdUpdate_eq; reflexivity.
- erewrite pcm_op_unit by apply _.
assert (HR : rf · (Some r · s) = Some r · rf · s)
by (apply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
destruct HE as [HES [rs [HE HM] ] ].
split; [setoid_rewrite HR; assumption | clear HR].
assert (HRi : rs i = None).
{ destruct (HM i) as [HDom _]; [tauto |].
rewrite <- fdLookup_notin_strong, HDom, fdLookup_notin_strong; assumption.
}
exists (fdUpdate i r rs); split; [now rewrite <- erase_insert_new, HE by assumption | intros j Hm'].
rewrite !fdLookup_in_strong; destruct (Peano_dec.eq_nat_dec i j).
+ subst j; rewrite !fdUpdate_eq; split; [intuition now eauto | intros].
simpl in HLw, HLrs; subst ri; rewrite <- HLw, isoR, <- HSub.
eapply uni_pred, HP; [now auto with arith | reflexivity].
+ rewrite !fdUpdate_neq, <- !fdLookup_in_strong by assumption.
setoid_rewrite <- HSub.
apply HM; assumption.
Qed.
(* XXX missing statements: NewGhost, GhostUpd, VSTimeless *)
End ViewShiftProps.
......@@ -512,52 +650,49 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Obligation Tactic := intros; eauto with typeclass_instances.
Definition wpFP m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
forall w' k s rf rr σ
(HSw : w ⊑ w') (HLt : k < n) (HR : Some r · Some rf == Some rr)
(HE : erasure σ m rr s w' @ S k),
forall w' k s rf σ (HSw : w ⊑ w') (HLt : k < n)
(HE : erasure σ m (Some r · rf) s w' @ S k),
(forall (HV : is_value e),
exists w'' r' rr' s', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
/\ Some r' · Some rf == Some rr'
/\ erasure σ m rr' s' w'' @ S k) /\
exists w'' r' s', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
/\ erasure σ m (Some r' · rf) s' w'' @ S k) /\
(forall σ' ei ei' K (HDec : e = K [[ ei ]])
(HStep : prim_step (ei, σ) (ei', σ')),
exists w'' r' rr' s', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
/\ Some r' · Some rf == Some rr'
/\ erasure σ' m rr' s' w'' @ k) /\
exists w'' r' s', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
/\ erasure σ' m (Some r' · rf) s' w'' @ k) /\
(forall e' K (HDec : e = K [[ e' ]]),
exists w'' rfk rret rr' s', w' ⊑ w'' /\ Some rfk · Some rret · Some rf == Some rr'
/\ WP (K [[ fork_ret ]]) φ w'' k rret
/\ WP e' (umconst ⊤) w'' k rfk
/\ erasure σ m rr' s' w'' @ k).
exists w'' rfk rret s', w' ⊑ w''
/\ WP (K [[ fork_ret ]]) φ w'' k rret
/\ WP e' (umconst ⊤) w'' k rfk
/\ erasure σ m (Some rfk · Some rret · rf) s' w'' @ k).
Program Definition wpF m : (expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props :=
n[(fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP m WP e φ w) _)])])])].
Next Obligation.
intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf rr σ HSw HLt HR HE.
rewrite <- EQr, (comm (Some rd)), <- assoc in HR.
destruct (Some rd · Some rf) as [rf' |] eqn: HRF;
[| now erewrite comm, pcm_op_zero in HR by apply _].
specialize (Hp w' k s rf' rr σ); destruct Hp as [HV [HS HF] ];
intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf σ HSw HLt HE.
rewrite <- EQr, (comm (Some rd)), <- assoc in HE.
specialize (Hp w' k s (Some rd · rf) σ); destruct Hp as [HV [HS HF] ];
[| now eauto with arith | ..]; try assumption; [].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
- specialize (HV HV0); destruct HV as [w'' [r2' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
[| now erewrite pcm_op_zero in HR' by apply _].
exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
eapply uni_pred, Hφ; [| eexists; rewrite <- HR1]; reflexivity.
- specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r2' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
[| now erewrite pcm_op_zero in HR' by apply _].
exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
eapply uni_pred, HWP; [| eexists; rewrite <- HR1]; reflexivity.
- specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret2 [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
rewrite <- HRF, assoc, <- (assoc (Some rfk)), (comm (Some rret2)) in HR'.
destruct (Some rd · Some rret2) as [rret1 |] eqn: HR1;
[| now erewrite (comm _ 0), !pcm_op_zero in HR' by apply _].
exists w'' rfk rret1 rr'; exists s'; repeat (split; try assumption); [].
eapply uni_pred, HWR; [| eexists; rewrite <- HR1]; reflexivity.
- specialize (HV HV0); destruct HV as [w'' [r1' [s' [HSw' [Hφ HE'] ] ] ] ].
rewrite assoc, (comm (Some r1')) in HE'.
destruct (Some rd · Some r1') as [r2' |] eqn: HR;
[| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
exists w'' r2' s'; split; [assumption | split; [| assumption] ].
eapply uni_pred, Hφ; [| eexists; rewrite <- HR]; reflexivity.
- specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [s' [HSw' [HWP HE'] ] ] ] ].
rewrite assoc, (comm (Some r1')) in HE'.
destruct k as [| k]; [exists w'' r1' s'; simpl erasure; tauto |].
destruct (Some rd · Some r1') as [r2' |] eqn: HR;
[| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
exists w'' r2' s'; split; [assumption | split; [| assumption] ].
eapply uni_pred, HWP; [| eexists; rewrite <- HR]; reflexivity.
- specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
destruct k as [| k]; [exists w'' rfk rret1 s'; simpl erasure; tauto |].
rewrite assoc, <- (assoc (Some rfk)), (comm (Some rret1)) in HE'.
destruct (Some rd · Some rret1) as [rret2 |] eqn: HR;
[| apply erasure_not_empty in HE'; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
exists w'' rfk rret2 s'; repeat (split; try assumption); [].
eapply uni_pred, HWR; [| eexists; rewrite <- HR]; reflexivity.
Qed.
Next Obligation.
intros w1 w2 EQw n r; simpl.
......@@ -571,44 +706,44 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
edestruct (Hp (extend w2' w1)) as [HV [HS HF] ]; try eassumption;
[eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
+ specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
+ specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') r' rr' s'; split; [assumption |].
split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
exists (extend w1'' w2') r' s'; split; [assumption |].
split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
+ specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
+ specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') r' rr' s'; split; [assumption |].
split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
exists (extend w1'' w2') r' s'; split; [assumption |].
split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
+ specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+ specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
exists (extend w1'' w2') rfk rret s'; split; [assumption |].
split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
- assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
edestruct (Hp (extend w2' w2)) as [HV [HS HF] ]; try eassumption;
[eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
+ specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
+ specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') r' rr' s'; split; [assumption |].
split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
exists (extend w1'' w2') r' s'; split; [assumption |].
split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
+ specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
+ specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') r' rr' s'; split; [assumption |].
split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
exists (extend w1'' w2') r' s'; split; [assumption |].
split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
+ specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+ specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
exists (extend w1'' w2') rfk rret s'; split; [assumption |].
split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
Qed.
......@@ -624,24 +759,24 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
split; intros Hp w'; intros; edestruct Hp as [HV [HS HF] ]; try eassumption; [|].
- split; [| split]; intros.
+ clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
apply EQφ, Hφ; now eauto with arith.
+ clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
exists w'' rfk rret rr'; exists s'; repeat (split; try assumption); [].
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
exists w'' rfk rret s'; repeat (split; try assumption); [].
eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
- split; [| split]; intros.
+ clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
apply EQφ, Hφ; now eauto with arith.
+ clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | now eauto with arith].
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
exists w'' rfk rret rr'; exists s'; repeat (split; try assumption); [].
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
exists w'' rfk rret s'; repeat (split; try assumption); [].
eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | now eauto with arith].
Qed.
Next Obligation.
......@@ -660,18 +795,18 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros WP1 WP2 EQWP e φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
split; intros Hp w'; intros; edestruct Hp as [HF [HS HV] ]; try eassumption; [|].
- split; [assumption | split; intros].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply (EQWP _ _ _), HWP; now eauto with arith.
+ clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
exists w'' rfk rret s'; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
- split; [assumption | split; intros].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply (EQWP _ _ _), HWP; now eauto with arith.
+ clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
exists w'' rfk rret s'; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Qed.
......@@ -680,18 +815,18 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros n WP1 WP2 EQWP e φ w k r HLt.
split; intros Hp w'; intros; edestruct Hp as [HV [HS HF] ]; try eassumption; [|].
- split; [assumption | split; intros].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply EQWP, HWP; now eauto with arith.
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
exists w'' rfk rret s'; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
- split; [assumption | split; intros].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply EQWP, HWP; now eauto with arith.
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
exists w'' rfk rret s'; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Qed.
......@@ -702,4 +837,96 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
End HoareTriples.
Section HoareTripleProperties.
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
Local Open Scope bi_scope.
Local Open Scope lang_scope.
Existing Instance LP_isval.
Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (φ : value -n> Props) (r : res).
(** Ret **)
Program Definition eqV v : value -n> Props :=
n[(fun v' : value => v === v')].
Next Obligation.
intros v1 v2 EQv w n r; simpl in *; split; congruence.
Qed.
Next Obligation.
intros v1 v2 EQv w m r HLt; destruct n as [| n]; [now inversion HLt | simpl in *].
split; congruence.
Qed.
Lemma htRet e (HV : is_value e) m :
valid (ht m ⊤ e (eqV (exist _ e HV))).
Proof.
Admitted.
(** Bind **)
Program Definition plugV m φ φ' K :=
n[(fun v : value => ht m (φ v) (K [[` v]]) φ')].
Next Obligation.
intros v1 v2 EQv w n r; simpl.
setoid_rewrite EQv at 1.
simpl in EQv; rewrite EQv; reflexivity.
Qed.
Next Obligation.
intros v1 v2 EQv; unfold ht; eapply (met_morph_nonexp _ _ box).
eapply (impl_dist (ComplBI := Props_BI)).
- apply φ; assumption.
- destruct n as [| n]; [apply dist_bound | simpl in EQv].
rewrite EQv; reflexivity.
Qed.
Lemma htBind P φ φ' K e m :
ht m P e φ ∧ all (plugV m φ φ' K) ⊑ ht m P (K [[ e ]]) φ'.
Proof.
Admitted.
Lemma htBind_alt P Q φ φ' K e m
(He : Q ⊑ ht m P e φ)
(HK : forall v, Q ⊑ ht m (φ v) (K [[` v ]]) φ') :
Q ⊑ ht m P (K [[ e ]]) φ'.
Admitted.
Implicit Type (C : Props).
(** Consequence **)
Lemma htCons C P P' φ φ' m e
(HPre : C ⊑ vs m m P P')
(HT : C ⊑ ht m P' e φ')
(HPost : forall v, C ⊑ vs m m (φ' v) (φ v)) :
C ⊑ ht m P e φ.
Admitted.
Lemma htACons C P P' φ φ' m m' e
(HAt : atomic e)
(HSub : m' ⊆ m)
(HPre : C ⊑ vs m m' P P')
(HT : C ⊑ ht m' P' e φ')
(HPost : forall v, C ⊑ vs m' m (φ' v) (φ v)) :
C ⊑ ht m P e φ.
Admitted.
(** Framing **)
Lemma htFrame m P R e φ :
ht m P e φ ⊑ ht m (P * R) e (lift_bin sc φ (umconst R)).
Admitted.
Lemma htAFrame m P R e φ
(HAt : atomic e) :
ht m P e φ ⊑ ht m (P * ▹ R) e (lift_bin sc φ (umconst R)).
Admitted.
(** Fork **)
Lemma htFork m P R e φ :
ht m P e φ ⊑ ht m (P * ▹ R) (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
Admitted.
End HoareTripleProperties.
End Iris.
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