Skip to content

GitLab

Commit eb79e96a authored by Ralf Jung's avatar Ralf Jung
Browse files

let wsat hide the shared resources

parent 14ff5436
Expand all Hide whitespace changes
Inline Side-by-side
iris_core.v
View file @ eb79e96a
......@@ -348,29 +348,32 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
Definition state_sat (r: option res) σ: Prop := match r with
| Some (ex_own s, _) => s = σ
| _ => False
end.
end.
Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
Proof.
intros r1 r2 EQr σ1 σ2 EQσ; apply ores_equiv_eq in EQr. rewrite EQσ, EQr. tauto.
Qed.
Global Instance preo_unit : preoType () := disc_preo ().
Program Definition wsat (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
▹ (mkUPred (fun n _ =>
state_sat (r · s) σ
/\ exists rs : nat -f> res,
comp_map rs == s /\
forall i (Hm : m i),
Program Definition wsat (σ : state) (m : mask) (r : option res) (w : Wld) : UPred () :=
▹ (mkUPred (fun n _ => exists rs : nat -f> res,
state_sat (r · (comp_map rs)) σ
/\ forall i (Hm : m i),
(i ∈ dom rs <-> i ∈ dom w) /\
forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
ı π w n ri) _).
Next Obligation.
intros n1 n2 _ _ HLe _ [HES HRS]; split; [assumption |].
intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
setoid_rewrite HLe; eassumption.
Qed.
Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv ==> equiv) (wsat σ).
Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv) (wsat σ).
Proof.
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]).
intros m1 m2 EQm r r' EQr w1 w2 EQw [| n] []; [reflexivity |];
apply ores_equiv_eq in EQr; subst r'.
split; intros [rs [HE HM] ]; 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.
rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
......@@ -379,10 +382,10 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
Qed.
Global Instance wsat_dist n σ m r s : Proper (dist n ==> dist n) (wsat σ m r s).
Global Instance wsat_dist n σ m r : Proper (dist n ==> dist n) (wsat σ m r).
Proof.
intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
split; intros [rs [HE HM] ]; exists rs.
- split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
assert (EQπ := EQw i); rewrite HLw in EQπ; clear HLw.
......@@ -399,10 +402,10 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
apply HR; [reflexivity | assumption].
Qed.
Lemma wsat_not_empty σ m r s w k (HN : r · s == 0) :
~ wsat σ m r s w (S k) tt.
Lemma wsat_not_empty σ m (r: option res) w k (HN : r == 0) :
~ wsat σ m r w (S k) tt.
Proof.
intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
intros [rs [HD _] ]; apply ores_equiv_eq in HN. setoid_rewrite HN in HD.
exact HD.
Qed.
......
iris_vs.v
View file @ eb79e96a
......@@ -13,22 +13,22 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
Local Obligation Tactic := intros.
Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
mkUPred (fun n r => forall w1 rf s mf σ k (HSub : w ⊑ w1) (HLe : k < n)
mkUPred (fun n r => forall w1 rf mf σ k (HSub : w ⊑ w1) (HLe : k < n)
(HD : mf # m1 ∪ m2)
(HE : wsat σ (m1 ∪ mf) (Some r · rf) s w1 @ S k),
exists w2 r' s',
(HE : wsat σ (m1 ∪ mf) (Some r · rf) w1 @ S k),
exists w2 r',
w1 ⊑ w2 /\ p w2 (S k) r'
/\ wsat σ (m2 ∪ mf) (Some r' · rf) s' w2 @ S k) _.
/\ wsat σ (m2 ∪ mf) (Some r' · rf) w2 @ S k) _.
Next Obligation.
intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
destruct (HP w1 (Some rd · rf) s mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ];
destruct (HP w1 (Some rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
try assumption; [now eauto with arith | |].
- eapply wsat_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 wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
exists w2 r2' s'; split; [assumption | split; [| assumption] ].
exists w2 r2'; split; [assumption | split; [| assumption] ].
eapply uni_pred, HP'; [| exists rd; rewrite HR']; reflexivity.
Qed.
......@@ -45,19 +45,19 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
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' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
+ eapply wsat_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 HE'];
exists (extend w1'' w2') r' s'; split; [assumption | split].
exists (extend w1'' w2') r'; split; [assumption | split].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply wsat_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' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
+ eapply wsat_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 HE'];
exists (extend w1'' w2') r' s'; split; [assumption | split].
exists (extend w1'' w2') r'; split; [assumption | split].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply wsat_dist, HE'; [symmetry; eassumption | now eauto with arith].
Qed.
......@@ -72,10 +72,10 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
Qed.
Next Obligation.
intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
- edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
- edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
clear HP; repeat (eexists; try eassumption); [].
apply EQp; [now eauto with arith | assumption].
- edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
- edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
clear HP; repeat (eexists; try eassumption); [].
apply EQp; [now eauto with arith | assumption].
Qed.
......@@ -99,7 +99,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
Proof.
intros w' n r1 HTL w HSub; rewrite HSub in HTL; clear w' HSub.
intros np rp HLe HS Hp w1; intros.
exists w1 rp s; split; [reflexivity | split; [| assumption] ]; clear HE HD.
exists w1 rp; split; [reflexivity | split; [| assumption] ]; clear HE HD.
destruct np as [| np]; [now inversion HLe0 |]; simpl in Hp.
unfold lt in HLe0; rewrite HLe0.
rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
......@@ -114,16 +114,14 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
apply ı in HInv; rewrite (isoR p) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
destruct HE as [HES [rs [HE HM] ] ].
destruct HE as [rs [HE HM] ].
destruct (rs i) as [ri |] eqn: HLr.
- rewrite comp_map_remove with (i := i) (r := ri) in HE by assumption.
assert (HR : Some r · rf · s == Some r · Some ri · rf · comp_map (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.
rewrite assoc, <- (assoc (Some r)), (comm rf), assoc in HE.
destruct (Some r · Some ri) as [rri |] eqn: HR;
[| erewrite !pcm_op_zero in HES by apply _; now contradiction].
exists w' rri (comp_map (fdRemove i rs)); split; [reflexivity |].
split; [| split; [assumption |] ].
[| erewrite !pcm_op_zero in HE by apply _; now contradiction].
exists w' rri; split; [reflexivity |].
split.
+ simpl; eapply HInv; [now auto with arith |].
eapply uni_pred, HM with i;
[| exists r; rewrite <- HR | | | rewrite HLr]; try reflexivity; [|].
......@@ -131,7 +129,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
destruct (Peano_dec.eq_nat_dec i i); tauto.
* specialize (HSub i); rewrite HLu in HSub.
symmetry; destruct (w' i); [assumption | contradiction].
+ exists (fdRemove i rs); split; [reflexivity | intros j Hm].
+ exists (fdRemove i rs); split; [assumption | 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].
......@@ -152,19 +150,17 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
apply ı in HInv; rewrite (isoR p) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
destruct HE as [HES [rs [HE HM] ] ].
exists w' (pcm_unit _) (Some r · s); split; [reflexivity | split; [exact I |] ].
assert (HR' : Some r · rf · s = rf · (Some r · s))
by (eapply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
setoid_rewrite HR' in HES; erewrite pcm_op_unit by apply _.
split; [assumption |].
destruct HE as [rs [HE HM] ].
exists w' (pcm_unit _); split; [reflexivity | split; [exact I |] ].
rewrite (comm (Some r)), <-assoc in HE.
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 comp_map_insert_old; [eassumption | rewrite <- EQR; reflexivity] |].
erewrite pcm_op_unit in EQR by apply _; rewrite EQR.
now apply comp_map_insert_new.
+ erewrite pcm_op_unit by apply _.
clear - HE EQR EQri. destruct (rs i) as [rsi |] eqn: EQrsi; subst.
* erewrite <-comp_map_insert_old; try eassumption. rewrite<- EQR; reflexivity.
* erewrite <-comp_map_insert_new; try eassumption. rewrite <-EQR.
erewrite pcm_op_unit by apply _. assumption.
+ 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 |
......@@ -184,9 +180,9 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
exists rd; assumption.
- destruct (rs i) as [rsi |] eqn: EQrsi; subst;
[| erewrite pcm_op_unit in EQR by apply _; discriminate].
clear - HE HES EQrsi EQR.
assert (HH : rf · (Some r · s) = 0); [clear HES | rewrite HH in HES; contradiction].
eapply ores_equiv_eq; rewrite <- HE, comp_map_remove by eassumption.
clear - HE EQrsi EQR.
assert (HH : rf · (Some r · comp_map rs) = 0); [clear HE | rewrite HH in HE; contradiction].
eapply ores_equiv_eq; rewrite comp_map_remove by eassumption.
rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
erewrite !pcm_op_zero by apply _; reflexivity.
Qed.
......@@ -196,13 +192,13 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
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 [sq [HSw12 [Hq HEq] ] ] ] ]; try eassumption; [|].
edestruct Hpq as [w2 [rq [HSw12 [Hq HEq] ] ] ]; try eassumption; [|].
{ clear - HD HMS; intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
destruct Hm12 as [Hm1 | Hm2]; [left; assumption | apply HMS, Hm2].
}
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 [sR [HSw23 [Hr HEr] ] ] ] ];
edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [HSw23 [Hr HEr] ] ] ];
try (reflexivity || eassumption); [now auto with arith | |].
{ clear - HD HMS; intros j [Hmf Hm23]; apply (HD j); split; [assumption |].
destruct Hm23 as [Hm2 | Hm3]; [apply HMS, Hm2 | right; assumption].
......@@ -216,7 +212,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
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 s; split; [reflexivity | split; [| assumption ] ].
exists w1 rp; 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.
......@@ -227,8 +223,8 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
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 : 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; [| |].
specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) (mf ∪ mf0) σ k); clear HS.
destruct HVS as [w'' [rq [HSub' [Hq HEq] ] ] ]; try assumption; [| |].
- (* disjointness of masks: possible lemma *)
clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
eapply HD; split; [eassumption | tauto].
......@@ -236,7 +232,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
clear; intros i; tauto.
- rewrite assoc in HEq; destruct (Some rq · Some rr) as [rqr |] eqn: HR';
[| apply wsat_not_empty in HEq; [contradiction | now erewrite !pcm_op_zero by apply _] ].
exists w'' rqr s'; split; [assumption | split].
exists w'' rqr; split; [assumption | split].
+ unfold lt in HLe0; rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr.
rewrite HR'; split; now auto.
+ eapply wsat_equiv, HEq; try reflexivity; [].
......@@ -275,14 +271,15 @@ Qed.
Proof.
unfold ownLP; intros _ _ _ w _ n [rp' rl'] _ _ HG w'; intros.
destruct rl as [rl |]; simpl in HG; [| contradiction].
destruct HE as [rs HE].
destruct HG as [ [rdp rdl] EQr]; rewrite pcm_op_split in EQr; destruct EQr as [EQrp EQrl].
erewrite comm, pcm_op_unit in EQrp by apply _; simpl in EQrp; subst rp'.
destruct (Some (rdp, rl') · rf · s) as [t |] eqn: EQt;
destruct (Some (rdp, rl') · rf · comp_map rs) as [t |] eqn: EQt;
[| destruct HE as [HES _]; setoid_rewrite EQt in HES; contradiction].
assert (EQt' : Some (rdp, rl') · rf · s == Some t) by (rewrite EQt; reflexivity).
assert (EQt' : Some (rdp, rl') · rf · comp_map rs == Some t) by (rewrite EQt; reflexivity).
clear EQt; rename EQt' into EQt.
destruct rf as [ [rfp rfl] |]; [| now erewrite (comm _ 0), !pcm_op_zero in EQt by apply _].
destruct s as [ [sp sl] |]; [| now erewrite (comm _ 0), pcm_op_zero in EQt by apply _].
destruct (comp_map rs) as [ [sp sl] |] eqn:EQrs; [| now erewrite (comm _ 0), pcm_op_zero in EQt by apply _].
destruct (Some (rdp, rl') · Some (rfp, rfl)) as [ [rdfp rdfl] |] eqn: EQdf;
setoid_rewrite EQdf in EQt; [| now erewrite pcm_op_zero in EQt by apply _].
destruct (HU (Some rdl · Some rfl · Some sl)) as [rsl [HPrsl HCrsl] ].
......@@ -292,14 +289,15 @@ Qed.
now rewrite <- EQdf, <- EQrl, (comm (Some rdl)), <- (assoc (Some rl)), <- assoc, HEq in EQt.
- destruct (rsl · Some rdl) as [rsl' |] eqn: EQrsl;
[| contradiction HCrsl; eapply ores_equiv_eq; now erewrite !assoc, EQrsl, !pcm_op_zero by apply _ ].
exists w' (rdp, rsl') (Some (sp, sl)); split; [reflexivity | split].
exists w' (rdp, rsl'); split; [reflexivity | split].
+ exists (exist _ rsl HPrsl); destruct rsl as [rsl |];
[simpl | now erewrite pcm_op_zero in EQrsl by apply _].
exists (rdp, rdl); rewrite pcm_op_split.
split; [now erewrite comm, pcm_op_unit by apply _ | now rewrite comm, EQrsl].
+ destruct HE as [HES HEL]; split; [| assumption]; clear HEL.
+ destruct HE as [HES HEL]. exists rs. split; [| assumption]; clear HEL.
assert (HT := ores_equiv_eq _ _ _ EQt); setoid_rewrite EQdf in HES;
setoid_rewrite HT in HES; clear HT; destruct t as [tp tl].
rewrite EQrs; clear rs EQrs.
destruct (rsl · (Some rdl · Some rfl · Some sl)) as [tl' |] eqn: EQtl;
[| now contradiction HCrsl]; clear HCrsl.
assert (HT : Some (rdp, rsl') · Some (rfp, rfl) · Some (sp, sl) = Some (tp, tl')); [| setoid_rewrite HT; apply HES].
......@@ -366,19 +364,22 @@ Qed.
{ 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 (fdUpdate i (ı' p) w) (pcm_unit _); 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 (eapply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
destruct HE as [HES [rs [HE HM] ] ].
split; [setoid_rewrite HR; assumption | clear HR].
destruct HE as [rs [HE HM] ].
exists (fdUpdate i r rs).
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 <- comp_map_insert_new, HE by assumption | intros j Hm'].
split.
{
rewrite <-comp_map_insert_new by assumption.
rewrite assoc, (comm rf). 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.
......
iris_wp.v
View file @ eb79e96a
This diff is collapsed.
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