Commit 14ff5436 authored by Ralf Jung's avatar Ralf Jung

rename for consistency: erasure -> world satisfaction; soundness -> adequacy

parent 6de81061
......@@ -58,10 +58,10 @@ CONTENTS
* iris_core.v defines erasure and the simpler assertions
* iris_vs.v defines view shifts and proves their rules
* iris_wp.v defines weakest preconditions and proves the rules for
Hoare triples
* iris_vs.v defines view shifts and proves their rules
The development uses ModuRes, a Coq library by Sieczkowski et al. to
solve the recursive domain equation (see the paper for a reference)
......@@ -73,8 +73,8 @@ REQUIREMENTS
Coq
We have tested the development using Coq v. 8.4pl4 on Linux and Mac
machines with 8GB RAM. The entire compilation took around an hour.
We have tested the development using Coq 8.4pl4 on Linux and Mac
machines. The entire compilation took less than an hour.
HOW TO COMPILE
......@@ -111,5 +111,5 @@ OVERVIEW OF LEMMAS
Fork iris_wp.v:/htFork
The main adequacy result is expressed by Theorem
iris_wp.v:/soundness_obs.
iris_wp.v:/adequacy_obs.
......@@ -295,11 +295,11 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
eapply HT, Hp; [etransitivity |]; eassumption.
Qed.
Section Erasure.
Section WorldSatisfaction.
Local Open Scope pcm_scope.
Local Open Scope bi_scope.
(* First, we need to erase a finite map. This won't be pretty, for
(* First, we need to compose the resources of a finite map. This won't be pretty, for
now, since the library does not provide enough
constructs. Hopefully we can provide a fold that'd work for
that at some point
......@@ -311,33 +311,33 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
end.
Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
Definition erase (m : nat -f> res) : option res := comp_list (cod m).
Definition comp_map (m : nat -f> res) : option res := comp_list (cod m).
Lemma erase_remove (rs : nat -f> res) i r (HLu : rs i = Some r) :
erase rs == Some r · erase (fdRemove i rs).
Lemma comp_map_remove (rs : nat -f> res) i r (HLu : rs i = Some r) :
comp_map rs == Some r · comp_map (fdRemove i rs).
Proof.
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
destruct (comp i j); [inversion HLu; reflexivity | discriminate |].
simpl comp_list; rewrite IHrs by eauto using SS_tail.
rewrite !assoc, (comm (Some s)); reflexivity.
Qed.
Lemma erase_insert_new (rs : nat -f> res) i r (HNLu : rs i = None) :
Some r · erase rs == erase (fdUpdate i r rs).
Lemma comp_map_insert_new (rs : nat -f> res) i r (HNLu : rs i = None) :
Some r · comp_map rs == comp_map (fdUpdate i r rs).
Proof.
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
destruct (comp i j); [discriminate | reflexivity |].
simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
rewrite !assoc, (comm (Some r)); reflexivity.
Qed.
Lemma erase_insert_old (rs : nat -f> res) i r1 r2 r
Lemma comp_map_insert_old (rs : nat -f> res) i r1 r2 r
(HLu : rs i = Some r1) (HEq : Some r1 · Some r2 == Some r) :
Some r2 · erase rs == erase (fdUpdate i r rs).
Some r2 · comp_map rs == comp_map (fdUpdate i r rs).
Proof.
destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
destruct (comp i j); [inversion HLu; subst; clear HLu | discriminate |].
- simpl comp_list; rewrite assoc, (comm (Some r2)), <- HEq; reflexivity.
......@@ -345,18 +345,18 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
rewrite !assoc, (comm (Some r2)); reflexivity.
Qed.
Definition erase_state (r: option res) σ: Prop := match r with
Definition state_sat (r: option res) σ: Prop := match r with
| Some (ex_own s, _) => s = σ
| _ => False
end.
Global Instance preo_unit : preoType () := disc_preo ().
Program Definition erasure (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
Program Definition wsat (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
(mkUPred (fun n _ =>
erase_state (r · s) σ
state_sat (r · s) σ
/\ exists rs : nat -f> res,
erase rs == s /\
comp_map rs == s /\
forall i (Hm : m i),
(i dom rs <-> i dom w) /\
forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
......@@ -366,7 +366,7 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
setoid_rewrite HLe; eassumption.
Qed.
Global Instance erasure_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv ==> equiv) (erasure σ).
Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> 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'.
......@@ -379,7 +379,7 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
Qed.
Global Instance erasure_dist n σ m r s : Proper (dist n ==> dist n) (erasure σ m r s).
Global Instance wsat_dist n σ m r s : Proper (dist n ==> dist n) (wsat σ m r s).
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]).
......@@ -399,14 +399,14 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
apply HR; [reflexivity | assumption].
Qed.
Lemma erasure_not_empty σ m r s w k (HN : r · s == 0) :
~ erasure σ m r s w (S k) tt.
Lemma wsat_not_empty σ m r s w k (HN : r · s == 0) :
~ wsat σ m r s w (S k) tt.
Proof.
intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
exact HD.
Qed.
End Erasure.
End WorldSatisfaction.
Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
......
......@@ -15,19 +15,19 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
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)
(HD : mf # m1 m2)
(HE : erasure σ (m1 mf) (Some r · rf) s w1 @ S k),
(HE : wsat σ (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) _.
/\ wsat σ (m2 mf) (Some r' · rf) s' 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'] ] ] ] ];
try assumption; [now eauto with arith | |].
- eapply erasure_equiv, HE; try reflexivity.
- 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 erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
[| apply wsat_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.
......@@ -46,20 +46,20 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
- 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; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ 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].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [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; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ 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].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
* eapply wsat_dist, HE'; [symmetry; eassumption | now eauto with arith].
Qed.
Next Obligation.
intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
......@@ -116,13 +116,13 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
do 8 red in HInv.
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.
assert (HR : Some r · rf · s == Some r · Some ri · rf · erase (fdRemove i rs))
- 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.
destruct (Some r · Some ri) as [rri |] eqn: HR;
[| erewrite !pcm_op_zero in HES by apply _; now contradiction].
exists w' rri (erase (fdRemove i rs)); split; [reflexivity |].
exists w' rri (comp_map (fdRemove i rs)); split; [reflexivity |].
split; [| split; [assumption |] ].
+ simpl; eapply HInv; [now auto with arith |].
eapply uni_pred, HM with i;
......@@ -162,9 +162,9 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
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] |].
[eapply comp_map_insert_old; [eassumption | rewrite <- EQR; reflexivity] |].
erewrite pcm_op_unit in EQR by apply _; rewrite EQR.
now apply erase_insert_new.
now apply comp_map_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 |
......@@ -186,7 +186,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
[| 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, erase_remove by eassumption.
eapply ores_equiv_eq; rewrite <- HE, comp_map_remove by eassumption.
rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
erewrite !pcm_op_zero by apply _; reflexivity.
Qed.
......@@ -232,14 +232,14 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
- (* 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; [].
- rewrite assoc, HR; eapply wsat_equiv, HE; try reflexivity; [].
clear; intros i; tauto.
- 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 _] ].
[| apply wsat_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; [].
+ eapply wsat_equiv, HEq; try reflexivity; [].
clear; intros i; tauto.
Qed.
......@@ -378,7 +378,7 @@ Qed.
{ 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'].
exists (fdUpdate i r rs); split; [now rewrite <- comp_map_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.
......
This diff is collapsed.
Markdown is supported
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