diff --git a/Makefile b/Makefile
index 8ce5888616a6133cf17c954854a94cf14404c767..a8778388f11e575a45e484e4b14ffc369e629a0b 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
-# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris.v iris_core.v lang.v masks.v world_prop.v -o Makefile
+# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris_core.v iris_vs.v iris_wp.v lang.v masks.v world_prop.v -o Makefile
#
.DEFAULT_GOAL := all
@@ -81,8 +81,9 @@ endif
######################
VFILES:=core_lang.v\
- iris.v\
iris_core.v\
+ iris_vs.v\
+ iris_wp.v\
lang.v\
masks.v\
world_prop.v
diff --git a/iris_core.v b/iris_core.v
index 855d57ce9234f960fed60bf9196b99710643eff3..2557b9fbfd6a6e593d8be5d59204aa24515477e6 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -9,10 +9,10 @@ Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
Instance res_pcm : PCM res := _.
End IrisRes.
-Module Iris (RL : PCM_T) (C : CORE_LANG).
- Module Import L := Lang C.
- Module Import R := IrisRes RL C.
- Module Import WP := WorldProp R.
+Module IrisCore (RL : PCM_T) (C : CORE_LANG).
+ Module Export L := Lang C.
+ Module Export R := IrisRes RL C.
+ Module Export WP := WorldProp R.
Delimit Scope iris_scope with iris.
Local Open Scope iris_scope.
@@ -410,4 +410,4 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
-End Iris.
+End IrisCore.
diff --git a/iris_vs.v b/iris_vs.v
new file mode 100644
index 0000000000000000000000000000000000000000..16671a66af3c89fb63bd92e336399b81820a9b55
--- /dev/null
+++ b/iris_vs.v
@@ -0,0 +1,393 @@
+Require Import world_prop core_lang masks iris_core.
+Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
+
+Module IrisVS (RL : PCM_T) (C : CORE_LANG).
+ Module Export CORE := IrisCore RL C.
+
+ Delimit Scope iris_scope with iris.
+ Local Open Scope iris_scope.
+
+ Section ViewShifts.
+ Local Open Scope mask_scope.
+ Local Open Scope pcm_scope.
+ 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)
+ (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.
+ 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 :=
+ n[(fun p => m[(preVS m1 m2 p)])].
+ Next Obligation.
+ intros w1 w2 EQw n r; split; intros HP w2'; intros.
+ - eapply HP; try eassumption; [].
+ rewrite EQw; assumption.
+ - eapply HP; try eassumption; [].
+ rewrite <- EQw; assumption.
+ Qed.
+ Next Obligation.
+ 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; [ | ].
+ + 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 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' [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 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.
+ Next Obligation.
+ intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
+ etransitivity; eassumption.
+ Qed.
+ Next Obligation.
+ intros p1 p2 EQp w n r; split; intros HP w1; intros.
+ - setoid_rewrite <- EQp; eapply HP; eassumption.
+ - setoid_rewrite EQp; eapply HP; eassumption.
+ 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; [].
+ clear HP; repeat (eexists; try eassumption); [].
+ apply EQp; [now eauto with arith | assumption].
+ - 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.
+
+ Definition vs (m1 m2 : mask) (p q : Props) : Props :=
+ □ (p → pvs m1 m2 q).
+
+ End ViewShifts.
+
+ Section ViewShiftProps.
+ Local Open Scope mask_scope.
+ Local Open Scope pcm_scope.
+ Local Open Scope bi_scope.
+
+ Implicit Types (p q r : Props) (i : nat) (m : mask).
+
+ Definition mask_sing i := mask_set mask_emp i True.
+
+ Lemma vsTimeless m p :
+ timeless p ⊑ vs m m (▹ p) p.
+ 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.
+ destruct np as [| np]; [now inversion HLe0 |]; simpl in Hp.
+ unfold lt in HLe0; rewrite HLe0.
+ rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
+ Qed.
+
+ Lemma vsOpen i p :
+ valid (vs (mask_sing i) mask_emp (inv i p) (â–¹ p)).
+ Proof.
+ intros pw nn r w _; clear r pw.
+ intros n r _ _ HInv w'; clear nn; intros.
+ do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
+ 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 (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))
+ 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 |].
+ split; [| split; [assumption |] ].
+ + simpl; eapply HInv; [now auto with arith |].
+ 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.
+ * 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].
+ rewrite fdLookup_in; setoid_rewrite (fdRemove_neq _ _ _ n0); rewrite <- fdLookup_in; now auto.
+ - rewrite <- fdLookup_notin_strong in HLr; contradiction HLr; clear HLr.
+ specialize (HSub i); rewrite HLu in HSub; clear - HM HSub.
+ destruct (HM i) as [HD _]; [left | rewrite HD, fdLookup_in_strong; destruct (w' i); [eexists; reflexivity | contradiction] ].
+ clear; unfold mask_sing, mask_set.
+ destruct (Peano_dec.eq_nat_dec i i); tauto.
+ Qed.
+
+ Lemma vsClose i p :
+ valid (vs mask_emp (mask_sing i) (inv i p * ▹ p) ⊤).
+ Proof.
+ intros pw nn r w _; clear r pw.
+ intros n r _ _ [r1 [r2 [HR [HInv HP] ] ] ] w'; clear nn; intros.
+ do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
+ 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 |].
+ 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].
+ 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.
+ 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 [sq [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] ] ] ] ];
+ 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].
+ }
+ clear HEq Hq HS.
+ setoid_rewrite HSw12; eauto 8.
+ Qed.
+
+ Lemma vsEnt p q m :
+ □ (p → q) ⊑ vs m m p q.
+ 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 ] ].
+ 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) :
+ 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 : 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 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.
+ - 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.
+
+ Instance LP_optres (P : option RL.res -> Prop) : LimitPreserving P.
+ Proof.
+ intros σ σc HPc; simpl; unfold option_compl.
+ generalize (@eq_refl _ (σ 1%nat)).
+ pattern (σ 1%nat) at 1 3; destruct (σ 1%nat); [| intros HE; rewrite HE; apply HPc].
+ intros HE; simpl; unfold discreteCompl, unSome.
+ generalize (@eq_refl _ (σ 2)); pattern (σ 2) at 1 3; destruct (σ 2).
+ + intros HE'; rewrite HE'; apply HPc.
+ + intros HE'; exfalso; specialize (σc 1 1 2)%nat.
+ rewrite <- HE, <- HE' in σc; contradiction σc; auto with arith.
+ Qed.
+
+ Definition ownLP (P : option RL.res -> Prop) : {s : option RL.res | P s} -n> Props :=
+ ownL <M< inclM.
+
+Lemma pcm_op_split rp1 rp2 rp sp1 sp2 sp :
+ Some (rp1, sp1) · Some (rp2, sp2) == Some (rp, sp) <->
+ Some rp1 · Some rp2 == Some rp /\ Some sp1 · Some sp2 == Some sp.
+Proof.
+ unfold pcm_op at 1, res_op at 2, pcm_op_prod at 1.
+ destruct (Some rp1 · Some rp2) as [rp' |]; [| simpl; tauto].
+ destruct (Some sp1 · Some sp2) as [sp' |]; [| simpl; tauto].
+ simpl; split; [| intros [EQ1 EQ2]; subst; reflexivity].
+ intros EQ; inversion EQ; tauto.
+Qed.
+
+ Lemma vsGhostUpd m rl (P : option RL.res -> Prop)
+ (HU : forall rf (HD : rl · rf <> None), exists sl, P sl /\ sl · rf <> None) :
+ valid (vs m m (ownL rl) (xist (ownLP P))).
+ Proof.
+ unfold ownLP; intros _ _ _ w _ n [rp' rl'] _ _ HG w'; intros.
+ destruct rl as [rl |]; simpl in HG; [| contradiction].
+ 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 HE as [HES _]; setoid_rewrite EQt in HES; contradiction].
+ assert (EQt' : Some (rdp, rl') · rf · s == 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 (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] ].
+ - intros HEq; destruct t as [tp tl]; apply pcm_op_split in EQt; destruct EQt as [_ EQt].
+ assert (HT : Some (rdp, rl') · Some (rfp, rfl) == Some (rdfp, rdfl)) by (rewrite EQdf; reflexivity); clear EQdf.
+ apply pcm_op_split in HT; destruct HT as [_ EQdf].
+ 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 (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.
+ assert (HT := ores_equiv_eq _ _ _ EQt); setoid_rewrite EQdf in HES;
+ setoid_rewrite HT in HES; clear HT; destruct t as [tp tl].
+ 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].
+ rewrite <- EQdf, <- assoc in EQt; clear EQdf; eapply ores_equiv_eq; rewrite <- assoc.
+ destruct (Some (rfp, rfl) · Some (sp, sl)) as [ [up ul] |] eqn: EQu;
+ setoid_rewrite EQu in EQt; [| now erewrite comm, pcm_op_zero in EQt by apply _].
+ apply pcm_op_split in EQt; destruct EQt as [EQt _]; apply pcm_op_split; split; [assumption |].
+ assert (HT : Some rfl · Some sl == Some ul);
+ [| now rewrite <- EQrsl, <- EQtl, <- HT, !assoc].
+ apply (proj2 (A := Some rfp · Some sp == Some up)), pcm_op_split.
+ now erewrite EQu.
+ Qed.
+ (* The above proof is rather ugly in the way it handles the monoid elements,
+ but it works *)
+
+ 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.
+
+ 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 (eapply 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.
+
+ End ViewShiftProps.
+
+End IrisVS.
diff --git a/iris.v b/iris_wp.v
similarity index 54%
rename from iris.v
rename to iris_wp.v
index 4596631efcd4b02ef0d9a18f90d04542cc3fe5cc..afe37f76c71a3e70b154e2dd7f5cf05903c81c8e 100644
--- a/iris.v
+++ b/iris_wp.v
@@ -1,782 +1,12 @@
-Require Import world_prop core_lang lang masks.
+Require Import world_prop core_lang masks iris_vs.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
-Module Iris (RL : PCM_T) (C : CORE_LANG).
-
- Module Import L := Lang C.
- Module Import R <: PCM_T.
- Definition res := (pcm_res_ex state * RL.res)%type.
- Instance res_op : PCM_op res := _.
- Instance res_unit : PCM_unit res := _.
- Instance res_pcm : PCM res := _.
- End R.
- Module Import WP := WorldProp R.
+Module IrisWP (RL : PCM_T) (C : CORE_LANG).
+ Module Export VS := IrisVS RL C.
Delimit Scope iris_scope with iris.
Local Open Scope iris_scope.
- (** The final thing we'd like to check is that the space of
- propositions does indeed form a complete BI algebra.
-
- The following instance declaration checks that an instance of
- the complete BI class can be found for Props (and binds it with
- a low priority to potentially speed up the proof search).
- *)
-
- Instance Props_BI : ComplBI Props | 0 := _.
- Instance Props_Later : Later Props | 0 := _.
-
- (** And now we're ready to build the IRIS-specific connectives! *)
-
- Section Necessitation.
- (** Note: this could be moved to BI, since it's possible to define
- for any UPred over a monoid. **)
-
- Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
-
- Program Definition box : Props -n> Props :=
- n[(fun p => m[(fun w => mkUPred (fun n r => p w n (pcm_unit _)) _)])].
- Next Obligation.
- intros n m r s HLe _ Hp; rewrite HLe; assumption.
- Qed.
- Next Obligation.
- intros w1 w2 EQw m r HLt; simpl.
- eapply (met_morph_nonexp _ _ p); eassumption.
- Qed.
- Next Obligation.
- intros w1 w2 Subw n r; simpl.
- apply p; assumption.
- Qed.
- Next Obligation.
- intros p1 p2 EQp w m r HLt; simpl.
- apply EQp; assumption.
- Qed.
-
- End Necessitation.
-
- (** "Internal" equality **)
- Section IntEq.
- Context {T} `{mT : metric T}.
-
- Program Definition intEqP (t1 t2 : T) : UPred res :=
- mkUPred (fun n r => t1 = S n = t2) _.
- Next Obligation.
- intros n1 n2 _ _ HLe _; apply mono_dist; now auto with arith.
- Qed.
-
- Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
-
- Instance intEq_equiv : Proper (equiv ==> equiv ==> equiv) intEqP.
- Proof.
- intros l1 l2 EQl r1 r2 EQr n r.
- split; intros HEq; do 2 red.
- - rewrite <- EQl, <- EQr; assumption.
- - rewrite EQl, EQr; assumption.
- Qed.
-
- Instance intEq_dist n : Proper (dist n ==> dist n ==> dist n) intEqP.
- Proof.
- intros l1 l2 EQl r1 r2 EQr m r HLt.
- split; intros HEq; do 2 red.
- - etransitivity; [| etransitivity; [apply HEq |] ];
- apply mono_dist with n; eassumption || now auto with arith.
- - etransitivity; [| etransitivity; [apply HEq |] ];
- apply mono_dist with n; eassumption || now auto with arith.
- Qed.
-
- End IntEq.
-
- Notation "t1 '===' t2" := (intEq t1 t2) (at level 70) : iris_scope.
-
- Section Invariants.
-
- (** Invariants **)
- Definition invP (i : nat) (p : Props) (w : Wld) : UPred res :=
- intEqP (w i) (Some (ı' p)).
- Program Definition inv i : Props -n> Props :=
- n[(fun p => m[(invP i p)])].
- Next Obligation.
- intros w1 w2 EQw; unfold equiv, invP in *.
- apply intEq_equiv; [apply EQw | reflexivity].
- Qed.
- Next Obligation.
- intros w1 w2 EQw; unfold invP; simpl morph.
- destruct n; [apply dist_bound |].
- apply intEq_dist; [apply EQw | reflexivity].
- Qed.
- Next Obligation.
- intros w1 w2 Sw; unfold invP; simpl morph.
- intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
- destruct (w1 i) as [μ1 |]; [| contradiction].
- destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
- rewrite <- Sw; assumption.
- Qed.
- Next Obligation.
- intros p1 p2 EQp w; unfold equiv, invP in *; simpl morph.
- apply intEq_equiv; [reflexivity |].
- rewrite EQp; reflexivity.
- Qed.
- Next Obligation.
- intros p1 p2 EQp w; unfold invP; simpl morph.
- apply intEq_dist; [reflexivity |].
- apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
- Qed.
-
- End Invariants.
-
- Notation "â–¡ p" := (box p) (at level 30, right associativity) : iris_scope.
- Notation "⊤" := (top : Props) : iris_scope.
- Notation "⊥" := (bot : Props) : iris_scope.
- Notation "p ∧ q" := (and p q : Props) (at level 40, left associativity) : iris_scope.
- Notation "p ∨ q" := (or p q : Props) (at level 50, left associativity) : iris_scope.
- Notation "p * q" := (sc p q : Props) (at level 40, left associativity) : iris_scope.
- Notation "p → q" := (BI.impl p q : Props) (at level 55, right associativity) : iris_scope.
- Notation "p '-*' q" := (si p q : Props) (at level 55, right associativity) : iris_scope.
- Notation "∀ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
- Notation "∃ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
- Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
- Notation "∃ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
-
- Lemma valid_iff p :
- valid p <-> (⊤ ⊑ p).
- Proof.
- split; intros Hp.
- - intros w n r _; apply Hp.
- - intros w n r; apply Hp; exact I.
- Qed.
-
- (** Ownership **)
- Definition ownR (r : res) : Props :=
- pcmconst (up_cr (pord r)).
-
- (** Physical part **)
- Definition ownRP (r : pcm_res_ex state) : Props :=
- ownR (r, pcm_unit _).
-
- (** Logical part **)
- Definition ownRL (r : RL.res) : Props :=
- ownR (pcm_unit _, r).
-
- (** Proper physical state: ownership of the machine state **)
- Instance state_type : Setoid state := discreteType.
- Instance state_metr : metric state := discreteMetric.
- Instance state_cmetr : cmetric state := discreteCMetric.
-
- Program Definition ownS : state -n> Props :=
- n[(fun s => ownRP (ex_own _ s))].
- Next Obligation.
- intros r1 r2 EQr. hnf in EQr. now rewrite EQr.
- Qed.
- Next Obligation.
- intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
- simpl in EQr. subst; reflexivity.
- Qed.
-
- (** Proper ghost state: ownership of logical w/ possibility of undefined **)
- Lemma ores_equiv_eq T `{pcmT : PCM T} (r1 r2 : option T) (HEq : r1 == r2) : r1 = r2.
- Proof.
- destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction;
- simpl in HEq; subst; reflexivity.
- Qed.
-
- Instance logR_metr : metric RL.res := discreteMetric.
- Instance logR_cmetr : cmetric RL.res := discreteCMetric.
-
- Program Definition ownL : (option RL.res) -n> Props :=
- n[(fun r => match r with
- | Some r => ownRL r
- | None => ⊥
- end)].
- Next Obligation.
- intros r1 r2 EQr; apply ores_equiv_eq in EQr; now rewrite EQr.
- Qed.
- Next Obligation.
- intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
- destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction; simpl in EQr; 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.
-
- Lemma box_top : ⊤ == □ ⊤.
- Proof.
- intros w n r; simpl; unfold const; reflexivity.
- Qed.
-
- Lemma box_disj p q :
- □ (p ∨ q) == □ p ∨ □ q.
- Proof.
- intros w n r; reflexivity.
- 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 15 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 (pcm_res_ex state), u) (pcm_unit (pcm_res_ex state), t).
- split; [unfold pcm_op, res_op, pcm_op_prod | split; do 15 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.
-
- (** Timeless *)
-
- Definition timelessP (p : Props) w n :=
- forall w' k r (HSw : w ⊑ w') (HLt : k < n) (Hp : p w' k r), p w' (S k) r.
-
- Program Definition timeless (p : Props) : Props :=
- m[(fun w => mkUPred (fun n r => timelessP p w n) _)].
- Next Obligation.
- intros n1 n2 _ _ HLe _ HT w' k r HSw HLt Hp; eapply HT, Hp; [eassumption |].
- now eauto with arith.
- Qed.
- Next Obligation.
- intros w1 w2 EQw n rr; simpl; split; intros HT k r HLt;
- [rewrite <- EQw | rewrite EQw]; apply HT; assumption.
- Qed.
- Next Obligation.
- intros w1 w2 EQw k; simpl; intros _ HLt; destruct n as [| n]; [now inversion HLt |].
- split; intros HT w' m r HSw HLt' Hp.
- - symmetry in EQw; assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw).
- apply (met_morph_nonexp _ _ p) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith).
- - assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw).
- apply (met_morph_nonexp _ _ p) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith).
- Qed.
- Next Obligation.
- intros w1 w2 HSw n; simpl; intros _ HT w' m r HSw' HLt Hp.
- eapply HT, Hp; [etransitivity |]; eassumption.
- Qed.
-
- Section Erasure.
- Local Open Scope pcm_scope.
- Local Open Scope bi_scope.
-
- (* First, we need to erase 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
- *)
- Fixpoint comp_list (xs : list res) : option res :=
- match xs with
- | nil => 1
- | (x :: xs)%list => Some x · comp_list xs
- 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).
-
- Lemma erase_remove (rs : nat -f> res) i r (HLu : rs i = Some r) :
- erase rs == Some r · erase (fdRemove i rs).
- Proof.
- destruct rs as [rs rsP]; unfold erase, 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).
- Proof.
- destruct rs as [rs rsP]; unfold erase, 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
- (HLu : rs i = Some r1) (HEq : Some r1 · Some r2 == Some r) :
- Some r2 · erase rs == erase (fdUpdate i r rs).
- Proof.
- destruct rs as [rs rsP]; unfold erase, 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.
- - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
- rewrite !assoc, (comm (Some r2)); reflexivity.
- Qed.
-
- Definition erase_state (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 () :=
- â–¹ (mkUPred (fun n _ =>
- erase_state (r · s) σ
- /\ exists rs : nat -f> res,
- 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),
- ı π w n ri) _).
- Next Obligation.
- intros n1 n2 _ _ HLe _ [HES HRS]; split; [assumption |].
- setoid_rewrite HLe; eassumption.
- Qed.
-
- 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 |];
- 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.
- rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
- - 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.
- Qed.
-
- Global Instance erasure_dist n σ m r s : Proper (dist n ==> dist n) (erasure σ 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]).
- - 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.
- destruct (w1 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
- apply ı in EQπ; apply EQπ; [now auto with arith |].
- apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [now auto with arith |].
- apply HR; [reflexivity | assumption].
- - 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.
- destruct (w2 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
- apply ı in EQπ; apply EQπ; [now auto with arith |].
- apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [now auto with arith |].
- 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.
- Proof.
- intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
- exact HD.
- Qed.
-
- End Erasure.
-
- Check erasure.
-
- Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
-
- Section ViewShifts.
- Local Open Scope mask_scope.
- Local Open Scope pcm_scope.
- 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)
- (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.
- 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 :=
- n[(fun p => m[(preVS m1 m2 p)])].
- Next Obligation.
- intros w1 w2 EQw n r; split; intros HP w2'; intros.
- - eapply HP; try eassumption; [].
- rewrite EQw; assumption.
- - eapply HP; try eassumption; [].
- rewrite <- EQw; assumption.
- Qed.
- Next Obligation.
- 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; [ | ].
- + 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 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' [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 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.
- Next Obligation.
- intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
- etransitivity; eassumption.
- Qed.
- Next Obligation.
- intros p1 p2 EQp w n r; split; intros HP w1; intros.
- - setoid_rewrite <- EQp; eapply HP; eassumption.
- - setoid_rewrite EQp; eapply HP; eassumption.
- 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; [].
- clear HP; repeat (eexists; try eassumption); [].
- apply EQp; [now eauto with arith | assumption].
- - 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.
-
- Definition vs (m1 m2 : mask) (p q : Props) : Props :=
- □ (p → pvs m1 m2 q).
-
- End ViewShifts.
-
- Check vs.
-
- Section ViewShiftProps.
- Local Open Scope mask_scope.
- Local Open Scope pcm_scope.
- Local Open Scope bi_scope.
-
- Implicit Types (p q r : Props) (i : nat) (m : mask).
-
- Definition mask_sing i := mask_set mask_emp i True.
-
- Lemma vsTimeless m p :
- timeless p ⊑ vs m m (▹ p) p.
- 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.
- destruct np as [| np]; [now inversion HLe0 |]; simpl in Hp.
- unfold lt in HLe0; rewrite HLe0.
- rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
- Qed.
-
- Lemma vsOpen i p :
- valid (vs (mask_sing i) mask_emp (inv i p) (â–¹ p)).
- Proof.
- intros pw nn r w _; clear r pw.
- intros n r _ _ HInv w'; clear nn; intros.
- do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
- 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 (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))
- 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 |].
- split; [| split; [assumption |] ].
- + simpl; eapply HInv; [now auto with arith |].
- 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.
- * 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].
- rewrite fdLookup_in; setoid_rewrite (fdRemove_neq _ _ _ n0); rewrite <- fdLookup_in; now auto.
- - rewrite <- fdLookup_notin_strong in HLr; contradiction HLr; clear HLr.
- specialize (HSub i); rewrite HLu in HSub; clear - HM HSub.
- destruct (HM i) as [HD _]; [left | rewrite HD, fdLookup_in_strong; destruct (w' i); [eexists; reflexivity | contradiction] ].
- clear; unfold mask_sing, mask_set.
- destruct (Peano_dec.eq_nat_dec i i); tauto.
- Qed.
-
- Lemma vsClose i p :
- valid (vs mask_emp (mask_sing i) (inv i p * ▹ p) ⊤).
- Proof.
- intros pw nn r w _; clear r pw.
- intros n r _ _ [r1 [r2 [HR [HInv HP] ] ] ] w'; clear nn; intros.
- do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
- 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 |].
- 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].
- 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.
- 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 [sq [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] ] ] ] ];
- 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].
- }
- clear HEq Hq HS.
- setoid_rewrite HSw12; eauto 8.
- Qed.
-
- Lemma vsEnt p q m :
- □ (p → q) ⊑ vs m m p q.
- 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 ] ].
- 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) :
- 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 : 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 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.
- - 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.
-
- Instance LP_optres (P : option RL.res -> Prop) : LimitPreserving P.
- Proof.
- intros σ σc HPc; simpl; unfold option_compl.
- generalize (@eq_refl _ (σ 1%nat)).
- pattern (σ 1%nat) at 1 3; destruct (σ 1%nat); [| intros HE; rewrite HE; apply HPc].
- intros HE; simpl; unfold discreteCompl, unSome.
- generalize (@eq_refl _ (σ 2)); pattern (σ 2) at 1 3; destruct (σ 2).
- + intros HE'; rewrite HE'; apply HPc.
- + intros HE'; exfalso; specialize (σc 1 1 2)%nat.
- rewrite <- HE, <- HE' in σc; contradiction σc; auto with arith.
- Qed.
-
- Definition ownLP (P : option RL.res -> Prop) : {s : option RL.res | P s} -n> Props :=
- ownL <M< inclM.
-
-Lemma pcm_op_split rp1 rp2 rp sp1 sp2 sp :
- Some (rp1, sp1) · Some (rp2, sp2) == Some (rp, sp) <->
- Some rp1 · Some rp2 == Some rp /\ Some sp1 · Some sp2 == Some sp.
-Proof.
- unfold pcm_op at 1, res_op at 2, pcm_op_prod at 1.
- destruct (Some rp1 · Some rp2) as [rp' |]; [| simpl; tauto].
- destruct (Some sp1 · Some sp2) as [sp' |]; [| simpl; tauto].
- simpl; split; [| intros [EQ1 EQ2]; subst; reflexivity].
- intros EQ; inversion EQ; tauto.
-Qed.
-
- Lemma vsGhostUpd m rl (P : option RL.res -> Prop)
- (HU : forall rf (HD : rl · rf <> None), exists sl, P sl /\ sl · rf <> None) :
- valid (vs m m (ownL rl) (xist (ownLP P))).
- Proof.
- unfold ownLP; intros _ _ _ w _ n [rp' rl'] _ _ HG w'; intros.
- destruct rl as [rl |]; simpl in HG; [| contradiction].
- 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 HE as [HES _]; setoid_rewrite EQt in HES; contradiction].
- assert (EQt' : Some (rdp, rl') · rf · s == 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 (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] ].
- - intros HEq; destruct t as [tp tl]; apply pcm_op_split in EQt; destruct EQt as [_ EQt].
- assert (HT : Some (rdp, rl') · Some (rfp, rfl) == Some (rdfp, rdfl)) by (rewrite EQdf; reflexivity); clear EQdf.
- apply pcm_op_split in HT; destruct HT as [_ EQdf].
- 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 (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.
- assert (HT := ores_equiv_eq _ _ _ EQt); setoid_rewrite EQdf in HES;
- setoid_rewrite HT in HES; clear HT; destruct t as [tp tl].
- 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].
- rewrite <- EQdf, <- assoc in EQt; clear EQdf; eapply ores_equiv_eq; rewrite <- assoc.
- destruct (Some (rfp, rfl) · Some (sp, sl)) as [ [up ul] |] eqn: EQu;
- setoid_rewrite EQu in EQt; [| now erewrite comm, pcm_op_zero in EQt by apply _].
- apply pcm_op_split in EQt; destruct EQt as [EQt _]; apply pcm_op_split; split; [assumption |].
- assert (HT : Some rfl · Some sl == Some ul);
- [| now rewrite <- EQrsl, <- EQtl, <- HT, !assoc].
- apply (proj2 (A := Some rfp · Some sp == Some up)), pcm_op_split.
- now erewrite EQu.
- Qed.
- (* The above proof is rather ugly in the way it handles the monoid elements,
- but it works *)
-
- 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.
-
- 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 (eapply 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.
-
- End ViewShiftProps.
-
Section HoareTriples.
(* Quadruples, really *)
Local Open Scope mask_scope.
@@ -984,8 +214,6 @@ Qed.
End HoareTriples.
- Check wp.
-
Section Soundness.
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
@@ -1201,8 +429,6 @@ Qed.
End Soundness.
- Check soundness.
-
Section HoareTripleProperties.
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
@@ -1558,4 +784,4 @@ Qed.
End DerivedRules.
-End Iris.
+End IrisWP.