diff --git a/README.txt b/README.txt
index 6144b8653df134517b5ad34316d18b40e0949b98..6f0c8257fb7921430b53506759812d0655087cd4 100644
--- a/README.txt
+++ b/README.txt
@@ -51,19 +51,23 @@ CONTENTS
* lang.v defines the threadpool reduction and derives some lemmas
from core_lang.v
- * masks.v introduces some lemmas about masks
+ * world_prop_recdom.v uses the ModuRes Coq library to construct the domain
+ for Iris propositions, satisfying the interface to the Iris domain
+ defined in world_prop.v
- * world_prop.v uses the ModuRes Coq library to construct the domain
- for Iris propositions
+ * iris_core.v constructs the BI structure on the Iris domain, and defines
+ some additional connectives (box, later, ownership).
- * iris_core.v defines world satisfaction and the simpler assertions
+ * iris_plog.v adds the programming logic: World satisfaction, primitive view shifts,
+ weakest precondition.
- * iris_vs.v defines view shifts and proves their rules
+ * iris_vs_rules.v and iris_wp_rules.v contain proofs of the primitive proof
+ rules for primitive view shifts and weakest precondition, respectively.
- * iris_wp.v defines weakest preconditions and proves the rules for
- Hoare triples
+ * iris_derived_rules.v derives rules for Hoare triples and view shifts
+ (as presented in the appendix).
- * iris_meta.v proves adequacy, robust safety, and the lifting lemmas
+ * iris_meta.v proves adequacy and the lifting lemmas
The development uses ModuRes, a Coq library by Sieczkowski et al. to
solve the recursive domain equation (see the paper for a reference)
@@ -76,7 +80,7 @@ REQUIREMENTS
Coq
We have tested the development using Coq 8.4pl4 on Linux and Mac
- machines. The entire compilation took less than an hour.
+ machines. The entire compilation took less than 15 minutes.
HOW TO COMPILE
@@ -95,23 +99,23 @@ OVERVIEW OF LEMMAS
RULE Coq lemma
-----------------------
- VSTimeless iris_vs.v:/vsTimeless
- NewInv iris_vs.v:/vsNewInv
- InvOpen iris_vs.v:/vsOpen
- InvClose iris_vs.v:/vsClose
- VSTrans iris_vs.v:/vsTrans
- VSImp iris_vs.v:/vsEnt
- VSFrame iris_vs.v:/vsFrame
- FpUpd iris_vs.v:/vsGhostUpd
-
- Ret iris_wp.v:/htRet
- Bind iris_wp.v:/htBind
- Frame iris_wp.v:/htFrame
- AFrame iris_wp.v:/htAFrame
- Csq iris_wp.v:/htCons
- ACSQ iris_wp.v:/htACons
- Fork iris_wp.v:/htFork
+ VSTimeless iris_derived_rules.v:vsTimeless
+ NewInv iris_derived_rules.v:vsNewInv
+ InvOpen iris_derived_rules.v:vsOpen
+ InvClose iris_derived_rules.v:vsClose
+ VSTrans iris_derived_rules.v:vsTrans
+ VSImp iris_derived_rules.v:vsEnt
+ VSFrame iris_derived_rules.v:vsFrame
+ FpUpd iris_derived_rules.v:vsGhostUpd
+
+ Ret iris_derived_rules.v:htRet
+ Bind iris_derived_rules.v:htBind
+ Frame iris_derived_rules.v:htFrame
+ AFrame iris_derived_rules.v:htAFrame
+ Csq iris_derived_rules.v:htCons
+ ACSQ iris_derived_rules.v:htACons
+ Fork iris_derived_rules.v:htFork
The main adequacy result is expressed by Theorem
- iris_wp.v:/adequacy_obs.
+ iris_meta.v:adequacy_obs.
diff --git a/iris_core.v b/iris_core.v
index f3eb0d5c37785d490011062d4fe92a127099e051..be03783f5c27ca6808057cd55003943ba05d5889 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -295,6 +295,15 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
- move=>wf /= m Hle HP. apply (H wf (S m)); assumption || omega.
Qed.
+ Lemma later_wand P Q:
+ â–¹(P -* Q) == â–¹P -* â–¹Q.
+ Proof.
+ intros w n. split; (destruct n; first (intro; exact:bpred)); intro H.
+ - simpl in H. move=>wf /= m Hle HP.
+ destruct m; first exact I. apply H; assumption || omega.
+ - move=>wf /= m Hle HP. apply (H wf (S m)); assumption || omega.
+ Qed.
+
Lemma later_top P:
▹⊤ == ⊤.
Proof.
@@ -481,12 +490,32 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Qed.
Lemma box_impl P Q:
- □(P → Q) ⊑ □P → □Q. (* The backwards direction does NOT hold. *)
+ □(P → Q) ⊑ □P → □Q.
+ (* The backwards direction does NOT hold: We can have □⊤ → own m
+ without having □(⊤ → own m). *)
Proof.
apply and_impl. rewrite -box_conj. apply box_intro.
rewrite ->box_elim. apply and_impl. reflexivity.
Qed.
+ Lemma box_wand P Q:
+ □(P -* Q) ⊑ □P -* □Q.
+ (* The backwards direction does NOT hold: We can have □⊤ -* own m
+ without having □(⊤ -* own m). *)
+ Proof.
+ apply sc_si. rewrite -box_star. apply box_intro.
+ rewrite ->box_elim. apply sc_si. reflexivity.
+ Qed.
+
+ Lemma box_impl_si P Q:
+ □(P → Q) == □(P -* Q).
+ Proof.
+ apply pord_antisym.
+ { apply box_intro. rewrite ->box_elim. apply impl_si. }
+ apply box_intro. apply and_impl. rewrite <-box_conj_star.
+ rewrite ->box_elim. apply sc_si. reflexivity.
+ Qed.
+
Lemma box_dup P :
â–¡P == â–¡P * â–¡P.
Proof.
@@ -663,7 +692,15 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
eapply HTQ, HPQ; [omega|omega|].
eapply dpred, HP. omega.
Qed.
-
+
+ Lemma timeless_si P Q:
+ timeless Q ⊑ timeless (P -* Q).
+ Proof.
+ move=>w n HTQ /= w' k Ltk HPQ w'' [|[|m]] Lem HP; first exact: bpred.
+ { apply HPQ, HP. omega. }
+ eapply HTQ, HPQ; [omega|omega|].
+ eapply dpred, HP. omega.
+ Qed.
Section TimelessQuant.
Context {T} `{cT : cmetric T}.
diff --git a/iris_derived_rules.v b/iris_derived_rules.v
index 404b686abae1ec25550c85165790ecc519856d65..89addfbc0399a42df8453e8601db095208a3b193 100644
--- a/iris_derived_rules.v
+++ b/iris_derived_rules.v
@@ -308,7 +308,7 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
Lemma htAFrame safe m m' P R e Q
(HD : m # m')
- (HAt : atomic e) :
+ (HNv : ~is_value e) :
ht safe m P e Q ⊑ ht safe (m ∪ m') (P * ▹R) e (lift_bin sc Q (umconst R)).
Proof.
rewrite {1}/ht. apply htIntro.
diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 61c2a1a2a5a2c326fb2d6fddf2e6bf47804ee22e..4a02e440d550ed0a994245103664423f98f1b31e 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -84,6 +84,37 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
exists e' (K ∘ K0). rewrite -> HE, fill_comp. auto. }
Qed.
+ (** Fork **)
+ Lemma wpFork safe m R e :
+ ▹wp safe m e (umconst ⊤) * ▹R ⊑ wp safe m (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)). (* PDS: Why sc not and? RJ: 'cause sc is stronger. *)
+ Proof.
+ intros w n. destruct n; first (intro; exact:bpred).
+ intros [[w1 w2] [EQw [Hwp HLR]]].
+ rewrite ->unfold_wp; intros w'; intros.
+ split; [| split; intros; [exfalso | split; intros ] ].
+ - intros. contradiction (fork_not_value HV).
+ - assert (HT := fill_fork HDec); subst K; rewrite ->fill_empty in HDec; subst.
+ eapply fork_stuck with (K := ε); [| repeat eexists; eassumption ]; reflexivity.
+ - assert (HT := fill_fork HDec); subst K; rewrite ->fill_empty in HDec.
+ apply fork_inj in HDec; subst e'. simpl in EQw.
+ unfold lt in HLt. simpl in Hwp.
+ simpl in HLR; rewrite <- Le.le_n_Sn in HE.
+ do 2 eexists. split; last first.
+ { split.
+ - eapply propsMN, Hwp. omega.
+ - eapply wsat_dist, HE; try reflexivity; [].
+ apply cmra_op_dist; last reflexivity.
+ eapply mono_dist, EQw; omega. }
+ rewrite ->fill_empty; rewrite <- (le_S_n _ _ HLt) in HLR.
+ eapply wpValue. exists (1 w2, w2). simpl. split_conjs.
+ + now rewrite ra_op_unit.
+ + reflexivity.
+ + eexact HLR.
+ - right; right; exists e empty_ctx; rewrite ->fill_empty; reflexivity.
+ Grab Existential Variables.
+ { exact:fork_ret_is_value. }
+ Qed.
+
(** Consequence **)
Lemma wpMon safe m e φ φ':
φ ⊑ φ' -> wp safe m e φ ⊑ wp safe m e φ'.
@@ -225,72 +256,37 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
Qed.
Lemma wpAFrameRes safe m R e φ
- (HAt : atomic e) :
+ (HNv : ~is_value e) :
(wp safe m e φ) * ▹R ⊑ wp safe m e (lift_bin sc φ (umconst R)).
Proof.
intros w n. destruct n; first (intro; exact:bpred).
move=>[[w1 w2] [/= EQr [Hwp HLR]]].
rewrite->unfold_wp; intros wf; intros.
rewrite ->unfold_wp in Hwp.
- edestruct (Hwp (w2 · wf) k mf) as [_ [HeS [_ Hsafe]]]; [omega|assumption| |].
+ edestruct (Hwp (w2 · wf) k mf) as [_ [HeS [HeF Hsafe]]]; [omega|assumption| |].
{ eapply wsat_dist, HE; first reflexivity; last reflexivity.
rewrite assoc. apply cmra_op_dist; last reflexivity.
eapply mono_dist, EQr. omega. }
- split; [intros; exfalso | split; intros; [| split; intros; [exfalso| ] ] ].
- - contradiction (atomic_not_value e).
+ split; [intros; exfalso | split; intros; [| split; intros ] ].
+ - contradiction.
- edestruct HeS as [w'' [He' HE']]; try eassumption; [].
- clear HE Hwp HeS; rewrite ->assoc in HE'.
- exists (w'' · w2). split; [| eassumption].
- assert (HNV : ~ is_value ei)
- by (intros HV; eapply (values_stuck HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
- subst e; assert (HT := atomic_fill HAt HNV); subst K; clear HNV.
- rewrite ->fill_empty in *. unfold lt in HLt.
- assert (HV := atomic_step HAt HStep).
- clear - He' HV HLR HLt; rename w'' into w.
- eapply wpValuePvs. move=>wf; intros.
- rewrite ->unfold_wp in He'. rewrite <-assoc in HE.
- edestruct He' as [HVal _]; try eassumption; first de_auto_eq; [].
- specialize (HVal HV); destruct HVal as [w'' [Hφ HE']].
- exists (w'' · w2). split; [| now rewrite -assoc].
- exists (w'', w2); split; simpl morph.
- { rewrite [ra_op]lock /= -lock. reflexivity. }
- split; first eassumption.
- rewrite /const /=. eapply propsMN, HLR. omega.
- - subst; eapply fork_not_atomic; eassumption.
+ clear HE Hwp HeS HeF; rewrite ->assoc in HE'.
+ exists (w'' · w2). split; [| eassumption]. subst e.
+ eapply wpFrameRes. exists (w'', w2).
+ split; first (apply sp_eq_iff; reflexivity).
+ split; first assumption.
+ eapply dpred, HLR. omega.
+ - edestruct HeF as [wfk [wret [He' [Ht' HE']]]]; try eassumption; [].
+ clear HE Hwp HeS HeF; rewrite ->assoc in HE'. subst e.
+ exists wfk (wret · w2). split; [| split; rewrite ->?assoc; eassumption].
+ eapply wpFrameRes. exists (wret, w2).
+ split; first (apply sp_eq_iff; reflexivity).
+ split; first assumption.
+ eapply dpred, HLR. omega.
- now auto.
Qed.
- (** Fork **)
- Lemma wpFork safe m R e :
- ▹wp safe m e (umconst ⊤) * ▹R ⊑ wp safe m (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)). (* PDS: Why sc not and? RJ: 'cause sc is stronger. *)
- Proof.
- intros w n. destruct n; first (intro; exact:bpred).
- intros [[w1 w2] [EQw [Hwp HLR]]].
- rewrite ->unfold_wp; intros w'; intros.
- split; [| split; intros; [exfalso | split; intros ] ].
- - intros. contradiction (fork_not_value HV).
- - assert (HT := fill_fork HDec); subst K; rewrite ->fill_empty in HDec; subst.
- eapply fork_stuck with (K := ε); [| repeat eexists; eassumption ]; reflexivity.
- - assert (HT := fill_fork HDec); subst K; rewrite ->fill_empty in HDec.
- apply fork_inj in HDec; subst e'. simpl in EQw.
- unfold lt in HLt. simpl in Hwp.
- simpl in HLR; rewrite <- Le.le_n_Sn in HE.
- do 2 eexists. split; last first.
- { split.
- - eapply propsMN, Hwp. omega.
- - eapply wsat_dist, HE; try reflexivity; [].
- apply cmra_op_dist; last reflexivity.
- eapply mono_dist, EQw; omega. }
- rewrite ->fill_empty; rewrite <- (le_S_n _ _ HLt) in HLR.
- eapply wpValue. exists (1 w2, w2). simpl. split_conjs.
- + now rewrite ra_op_unit.
- + reflexivity.
- + eexact HLR.
- - right; right; exists e empty_ctx; rewrite ->fill_empty; reflexivity.
- Grab Existential Variables.
- { exact:fork_ret_is_value. }
- Qed.
-
+ (* Unsafe and safe weakest-pre *)
Lemma wpUnsafe {m e φ} : wp true m e φ ⊑ wp false m e φ.
Proof.
move=> w n. move: n w e φ; elim/wf_nat_ind. move=> n IH w e φ He.
diff --git a/iris_meta.v b/iris_meta.v
index 01451fe8ef43ded356f02205fe4c12893e187ae3..c8d91366e8e585cf311f68cdd7f9a26500cd3156 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -184,7 +184,7 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
n[(fun v => pcmconst (sp_const (Q v)))].
Next Obligation.
move=>v1 v2 EQv. destruct n; first exact:dist_bound.
- intros w m Hlt. rewrite /= /sp_constF. destruct m; first reflexivity.
+ intros w m Hlt. rewrite /=. destruct m; first reflexivity.
rewrite EQv. reflexivity.
Qed.
@@ -227,129 +227,6 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
End Adequacy.
- (* Section RobustSafety.
-
- Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (v : value) (Q : vPred) (r : res) (w : Wld) (σ : state).
-
- Implicit Types (E : expr -n> Props) (Θ : Props).
-
- Program Definition restrictV E : vPred :=
- n[(fun v => E (` v))].
- Next Obligation.
- move=> v v' Hv w k r; move: Hv.
- case: n=>[_ Hk | n]; first by exfalso; omega.
- by move=> /= ->.
- Qed.
-
- Definition pure e := ~ atomic e /\ forall σ e' σ',
- prim_step (e,σ) (e',σ') ->
- σ = σ'.
-
- Definition restrict_lang := forall e,
- reducible e ->
- atomic e \/ pure e.
-
- Definition fork_compat E Θ := forall e,
- Θ ⊑ (E (fork e) → E e).
-
- Definition fill_compat E Θ := forall K e,
- Θ ⊑ (E (fill K e) ↔ E e * E (fill K fork_ret)).
-
- Definition atomic_compat E Θ m := forall e,
- atomic e ->
- Θ ⊑ ht false m (E e) e (restrictV E).
-
- Definition pure_compat E Θ m := forall e σ e',
- prim_step (e,σ) (e',σ) ->
- Θ ⊑ vs m m (E e) (E e').
-
- Lemma robust_safety {E Θ e m}
- (LANG : restrict_lang)
- (FORK : fork_compat E Θ)
- (FILL : fill_compat E Θ)
- (HT : atomic_compat E Θ m)
- (VS : pure_compat E Θ m) :
- □Θ ⊑ ht false m (E e) e (restrictV E).
- Proof.
- move=> wz nz rz HΘ w HSw n r HLe _ He.
- have {HΘ wz nz rz HSw HLe} HΘ: Θ w n 1 by rewrite/= in HΘ; exact: propsMWN HΘ.
- (* generalize IH's post-condition for the fork case *)
- pose post Q := forall v w n r, (E (`v)) w n r -> (Q v) w n r.
- set Q := restrictV E; have HQ: post Q by done.
- move: HΘ He HQ; move: n e w r Q; elim/wf_nat_ind => n IH e w r Q HΘ He HQ.
- rewrite unfold_wp; move=> w' k rf mf σ HSw HLt HD HW.
- (* specialize a bit *)
- move/(_ _ _ _ _ HΘ): FORK => FORK.
- move/(_ _ _ _ _ _ HΘ): FILL => FILL.
- move/(_ _ _)/biimpL: (FILL) => SPLIT; move/(_ _ _)/biimpR: FILL => FILL.
- move/(_ _ _ _ _ _ HΘ): HT => HT.
- move/(_ _ _ _ _ _ _ _ HΘ): VS => VS.
- have {IH HΘ Θ} IH: forall e w' r Q,
- w ⊑ w' -> (E e) w' k r -> post Q -> ((wp false m e) Q) w' k r.
- { move=> ? ? ? ? HSw'; move/(propsMWN HSw' (lelt HLt)): HΘ => HΘ. exact: IH. }
- have HLe: S k <= n by omega.
- split.
- (* e value *)
- { move=> HV {FORK FILL LANG HT VS IH}.
- exists w' r. split; [by reflexivity | split; [| done]].
- apply: HQ. exact: propsMWN He. }
- split; [| split; [| done]]; first last.
- (* e forks *)
- { move=> e' K HDec {LANG FILL HT VS}; rewrite HDec {HDec} in He.
- move/(SPLIT _ _ _ (prefl w) _ _ (lerefl n) unit_min)
- /(propsMWN HSw (lelt HLt)): He => [re' [rK [Hr [He' HK]]]] {SPLIT}.
- move/(FORK _ _ HSw _ _ (lelt HLt) unit_min): He' => He' {FORK}.
- exists w' re' rK. split; [by reflexivity | split; [exact: IH | split; [exact: IH |]]].
- move: HW; rewrite -Hr. exact: wsatM. }
- (* e steps *)
- (* both forthcoming cases work at step-indices S k and (for the IH) k. *)
- have HLt': k < S k by done.
- move=> σ' ei ei' K HDec HStep; rewrite HDec {HDec} in He.
- move/(SPLIT _ _ _ (prefl w) _ _ (lerefl n) unit_min)
- /(propsMWN HSw HLe): He => [rei [rK [Hr [Hei HK]]]] {SPLIT}.
- move: HW; rewrite -Hr -assoc => HW {Hr r}.
- have HRed: reducible ei by exists σ (ei',σ').
- case: (LANG ei HRed)=>[HA {VS} | [_ HP] {HT}] {LANG HRed}; last first.
- (* pure step *)
- { move/(_ _ _ _ HStep): HP => HP; move: HStep HW. rewrite HP => HStep HW {HP σ}.
- move/(_ _ _ _ HStep _ HSw _ _ HLe unit_min Hei): VS => VS {HStep HLe Hei}.
- move: HD; rewrite -{1}(mask_union_idem m) => HD.
- move/(_ _ _ _ _ _ (prefl w') HLt' HD HW): VS => [w'' [r' [HSw' [Hei' HW']]]] {HLt' HD HW}.
- have HLe': k <= S k by omega.
- exists w'' (r' · rK). split; [done | split; [| by move/(wsatM HLe'): HW'; rewrite assoc]].
- set HwSw'' := ptrans HSw HSw'.
- apply: IH; [done | | done].
- apply: (FILL _ _ _ HwSw'' _ _ (lelt HLt) unit_min).
- exists r' rK. split; first by reflexivity.
- split; [ exact: propsMN Hei' | exact: propsMWN HK ]. }
- (* atomic step *)
- move/(_ _ HA _ HSw (S k) _ HLe unit_min Hei): HT => {Hei HLe} Hei.
- (* unroll wp(ei,E)—step case—to get wp(ei',E) *)
- move: Hei; rewrite {1}unfold_wp => Hei.
- move/(_ _ _ _ _ _ (prefl w') HLt' HD HW): Hei => [_ [HS _]] {HLt' HW}.
- have Hεei: ei = fill ε ei by rewrite fill_empty.
- move/(_ _ _ _ _ Hεei HStep): HS => [w'' [r' [HSw' [Hei' HW']]]] {Hεei}.
- (* unroll wp(ei',E)—value case—to get E ei' *)
- move: Hei'; rewrite (fill_empty ei') {1}unfold_wp => Hei'.
- move: IH HLt HK HW' Hei'; case: k => [| k'] IH HLt HK HW' Hei'.
- { exists w'' r'. by split; [done | split; [exact: wpO | done]]. }
- have HLt': k' < S k' by done.
- move/(_ _ _ _ _ _ (prefl w'') HLt' HD HW'): Hei' => [Hv _] {HLt' HD HW'}.
- move: (atomic_step HA HStep) => HV {HA HStep}.
- move/(_ HV): Hv => [w''' [rei' [HSw'' [Hei' HW]]]].
- move: HW; rewrite assoc => HW.
- set Hw'Sw''' := ptrans HSw' HSw''.
- set HwSw''' := ptrans HSw Hw'Sw'''.
- exists w''' (rei' · rK). split; [done | split; [| done]].
- apply: IH; [done | | done].
- apply: (FILL _ _ _ HwSw''' _ _ (lelt HLt) unit_min).
- exists rei' rK. split; [by reflexivity | split; [done |]].
- have HLe: S k' <= S (S k') by omega.
- exact: propsMWN HK.
- Qed.
-
- End RobustSafety. *)
-
Section StatefulLifting.
Implicit Types (P : Props) (n k : nat) (safe : bool) (m : DecEnsemble nat) (e : expr) (r : res) (σ : state) (w : Wld).
@@ -502,7 +379,7 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
apply top_valid. apply htValid. rewrite sc_top_unit.
(* Now fall back to proving this in the model. *)
move=>w n. destruct n; first (intro;exact:bpred).
- rewrite /= /sp_constF. move=>[[Hφ Hval] HownS].
+ rewrite /=. move=>[[Hφ Hval] HownS].
eapply wpValue; [].
simpl. exists σ'. split; assumption.
Grab Existential Variables.
diff --git a/iris_plog.v b/iris_plog.v
index 7dc8d6a247e524099b8b70b8305e1633483a3aa5..a11329fa96b5496d4189b26ef1d07d5ce317aba2 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -118,11 +118,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
rewrite comm -comp_finmap_move comm ra_op_unit. reflexivity.
Qed.
- (* Go through some struggle to even write down world satisfaction... *)
- (*
- Local Open Scope finmap_scope.
- *)
-
+ (** Now we define world satisfaction **)
Lemma world_inv_val {wt n}:
forall (pv: cmra_valid wt n) {i agP} (Heq: (Invs wt) i = n = Some agP), cmra_valid agP n.
Proof.
@@ -191,16 +187,13 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
Qed.
(* It may be possible to use "later_sp" here, but let's avoid indirections where possible. *)
- Definition wsatF σ m w n :=
- match n with
- | S (S n') => exists s : nat -f> Wld,
- let wt := comp_finmap w s in
- wsatTotal (S n') σ s m wt
- | _ => True
- end.
-
Program Definition wsat σ m w : SPred :=
- p[(wsatF σ m w)].
+ p[(fun n => match n return _ with
+ | S (S n') => exists s : nat -f> Wld,
+ let wt := comp_finmap w s in
+ wsatTotal (S n') σ s m wt
+ | _ => True
+ end)].
Next Obligation.
intros n1 n2 HLe. do 2 (destruct n2; first (intro; exact I)).
do 2 (destruct n1; first (exfalso; omega)).
@@ -501,20 +494,27 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
rewrite unfold_wp; intros w'; intros; now inversion HLt.
Qed.
+ (* The two definitions are actually closely related. *)
Lemma wpValuePvs e (HV : is_value e) safe m φ :
- pvs m m (φ (exist _ e HV)) ⊑ wp safe m e φ.
+ pvs m m (φ (exist _ e HV)) == wp safe m e φ.
Proof.
- intros w n Hvs.
- rewrite unfold_wp; intros wf; intros; split; [| split; [| split] ]; intros.
- - edestruct (Hvs wf k mf) as [w' [Hφ HE']]; try eassumption; first de_auto_eq; [].
- exists w'. split; last assumption.
- eapply spredNE, dpred, Hφ; last omega.
- apply (met_morph_nonexp φ). apply dist_refl.
- reflexivity.
- - contradiction (values_stuck HV HDec).
- repeat eexists; eassumption.
- - subst e; contradiction (fork_not_value (fill_value HV)).
- - unfold safeExpr. auto.
+ intros w n. split.
+ - intros Hvs.
+ rewrite unfold_wp; intros wf; intros; split; [| split; [| split] ]; intros.
+ + edestruct (Hvs wf k mf) as [w' [Hφ HE']]; try eassumption; first de_auto_eq; [].
+ exists w'. split; last assumption.
+ eapply spredNE, dpred, Hφ; last omega.
+ apply (met_morph_nonexp φ). apply dist_refl.
+ reflexivity.
+ + contradiction (values_stuck HV HDec).
+ repeat eexists; eassumption.
+ + subst e; contradiction (fork_not_value (fill_value HV)).
+ + unfold safeExpr. auto.
+ - move=>Hwp. intros wf; intros.
+ rewrite ->unfold_wp in Hwp.
+ edestruct (Hwp wf k mf) as [HVal _]; try eassumption; first de_auto_eq; [].
+ destruct (HVal HV) as [w' [Hφ Hws]].
+ exists w'. split; assumption.
Qed.
Lemma wpValue e (HV : is_value e) safe m φ :
diff --git a/lib/ModuRes/Agreement.v b/lib/ModuRes/Agreement.v
index f7d0375dce2ee82420bb3e2bd622d0d311c7410e..8dae4ac6f04d7099eb608c2947e0bdcf34dae355 100644
--- a/lib/ModuRes/Agreement.v
+++ b/lib/ModuRes/Agreement.v
@@ -301,19 +301,14 @@ Section Agreement.
move=><-. assumption.
Qed.
- Definition ra_ag_tsdiag_n (σ : chain ra_agree) n: T :=
- match σ n with
- | ag_inj v' ts' tsx' => ts' n
- end.
-
Program Definition ra_ag_compl (σ : chain ra_agree) {σc : cchain σ} :=
ag_inj (compl (ra_ag_vchain σ))
- (fun n => ra_ag_tsdiag_n σ n) _.
+ (fun n => match σ n return _ with
+ | ag_inj v' ts' tsx' => ts' n end) _.
Next Obligation.
move=>n i HLe pv. simpl. rewrite -/dist.
assert (pvc: compl (ra_ag_vchain σ) i) by assumption.
destruct n as [|n]; first by apply: dist_bound.
- unfold ra_ag_tsdiag_n.
ddes (σ i) at 1 3 as [vi tsi tsxi] deqn:EQi.
ddes (σ (S n)) at 1 3 as [vSn tsSn tsxSn] deqn:EQSn.
cchain_eleq σ at i (S n) lvl:(S n); move=>[EQv EQts].
@@ -336,7 +331,6 @@ Section Agreement.
inversion EQi; subst. reflexivity.
- move=>j HLej pv1.
destruct j as [|j]; first by apply: dist_bound.
- unfold ra_ag_tsdiag_n.
rewrite /ra_ag_vchain /= in pv1. move:pv1.
ddes (σ (S j)) at 1 3 6 as [vSSj tsSSj tsxSSj] deqn:EQSSj.
intros pv1. cchain_eleq σ at (S j) i lvl:(S j); move=>[EQv EQts].
@@ -347,15 +341,6 @@ Section Agreement.
Global Instance ra_ag_pcm: pcmType ra_agree.
Proof.
split. repeat intro. eapply ra_ag_pord. unfold compl, ra_ag_cmt, ra_ag_compl.
- assert (HT: forall n, ra_ag_vchain Ï n n -> ra_ag_tsdiag_n σ n = n = ra_ag_tsdiag_n Ï n).
- { move=>n pv. destruct n as [|n]; first by apply: dist_bound.
- unfold ra_ag_tsdiag_n.
- ddes (σ (S n)) at 1 3 as [vσn tsσn tsxσn] deqn:EQσn.
- ddes (Ï (S n)) at 1 3 as [vÏn tsÏn tsxÏn] deqn:EQÏn.
- specialize (H (S n)). rewrite ->ra_ag_pord in H.
- rewrite <-EQσn, <-EQÏn, comm in H. destruct H as [EQv EQts].
- apply EQts. rewrite EQv. rewrite /ra_ag_vchain -EQÏn in pv. assumption.
- }
split.
- move=>n. split; first by (intros (pv1 & pv2 & _); tauto).
simpl. move=>pv. move:(pv). rewrite {1}/ra_ag_vchain. simpl.
@@ -366,7 +351,12 @@ Section Agreement.
ddes (σ n) at 1 3 as [vσn tsσn tsxσn] deqn:EQσn.
specialize (H n). rewrite ->ra_ag_pord, <-EQÏn, <-EQσn, comm in H.
destruct H as [EQv _]. rewrite <-EQv in pvÏ. destruct pvÏ as [pv1 _]. assumption. }
- do 2 (split; first assumption). symmetry. apply HT. assumption.
+ do 2 (split; first assumption). symmetry.
+ destruct n as [|n]; first by apply: dist_bound.
+ rewrite -EQÏn. destruct (σ (S n)) as [vσn tsσn rsxσn] eqn:EQσn.
+ specialize (H (S n)). rewrite ->ra_ag_pord in H.
+ rewrite ->EQσn, <-EQÏn, comm in H. destruct H as [EQv EQts].
+ apply EQts. rewrite EQv. rewrite /ra_ag_vchain -EQÏn in pv. assumption.
- intros n (pv1 & pv2 & EQ). reflexivity.
Qed.
diff --git a/lib/ModuRes/BI.v b/lib/ModuRes/BI.v
index 9efd81dfc4bf8a82c9d454626e31f97f36666055..a96d3b411849e13ce3d1f6ecac765b0dfa5df334 100644
--- a/lib/ModuRes/BI.v
+++ b/lib/ModuRes/BI.v
@@ -252,6 +252,13 @@ Section ComplBIProps.
- apply or_injR.
Qed.
+ Lemma impl_si P Q:
+ P → Q ⊑ P -* Q.
+ Proof.
+ apply sc_si. rewrite ->sc_and.
+ apply and_impl. reflexivity.
+ Qed.
+
Lemma all_L {U} `{cmU : cmetric U} u (P: U -n> B) Q:
P u ⊑ Q -> all P ⊑ Q.
Proof.
diff --git a/lib/ModuRes/DecEnsemble.v b/lib/ModuRes/DecEnsemble.v
index 439483357c5a273e3740dc892ce916801e6c0a04..0cb4d3e9a396e1532600699fef34dcbde87ce07c 100644
--- a/lib/ModuRes/DecEnsemble.v
+++ b/lib/ModuRes/DecEnsemble.v
@@ -95,7 +95,7 @@ Notation "de1 # de2" := (de1 ∩ de2 == de_emp) (at level 70) : de_scope.
in the context that also occurs in one of the <de>s. In this case, it can help to
do the specialization manually, and call de_tauto directly.
*)
-Ltac de_unfold := unfold de_cap, de_cup, de_minus, de_compl, const; unlock; simpl.
+Ltac de_unfold := unfold de_cap, de_cup, de_minus, de_compl; unlock; simpl.
Ltac de_in_destr := simpl;
repeat (match goal with
| [ |- context[dec_eq ?i ?j] ] => destruct (dec_eq i j); first try subst j; try contradiction_eq; simpl
diff --git a/lib/ModuRes/Finmap.v b/lib/ModuRes/Finmap.v
index c5da2f2cc80c79f7a1bd055c41051606484f29b6..7215550b57d84810642947250dd1252b6f1d7f8d 100644
--- a/lib/ModuRes/Finmap.v
+++ b/lib/ModuRes/Finmap.v
@@ -552,39 +552,46 @@ Section FinDom2.
(Temp: T fdEmpty).
Context (Tstep: forall (k:K) (v:V) (f: K -f> V), ~(k ∈ dom f) -> T f -> T (f + [fd k <- v ] )).
- Definition fdRectInner: forall l f, dom f = l -> T f.
- Proof.
- refine (fix F (l: list K) :=
- match l as l return (forall f, dom f = l -> T f) with
- | [] => fun f Hdom => Text fdEmpty f _ Temp
- | k::l' => fun f Hdom => let f' := f \ k in
- let Hindom: k ∈ dom f := _ in
- let v' := fdLookup_indom f k Hindom in
- Text (f' + [fd k <- v' ]) f _
- (Tstep k v' f' _ (F l' f' _))
- end); clear F.
- - split.
- + move=>k /=. symmetry. apply fdLookup_notin_strong. rewrite Hdom. tauto.
- + rewrite Hdom. reflexivity.
- - rewrite Hdom. left. reflexivity.
- - subst f'. split.
- + move=>k'. destruct (dec_eq k k') as [EQ|NEQ].
- * subst k'. rewrite fdStrongUpdate_eq. subst v'. symmetry. eapply fdLookup_indom_corr.
- reflexivity.
- * erewrite !fdStrongUpdate_neq by assumption. reflexivity.
- + rewrite Hdom /dom /=. f_equal. rewrite /dom /= Hdom.
- rewrite DecEq_refl.
- assert (Hnod := dom_nodup f). rewrite Hdom in Hnod.
- assert (Hfilt1: (filter_dupes ([])%list l') = l').
- { apply filter_dupes_id. simpl. inversion Hnod; subst. assumption. }
- rewrite Hfilt1. apply filter_dupes_id. assumption.
- - subst f'. apply fdLookup_notin. rewrite fdStrongUpdate_eq. reflexivity.
- - subst f'. rewrite /dom /fdStrongUpdate /=.
- rewrite Hdom. destruct (dec_eq k k) as [_|NEQ]; last (exfalso; now apply NEQ).
- apply filter_dupes_id with (dupes:=[]); simpl.
- assert (Hno:= dom_nodup f). rewrite Hdom in Hno.
- inversion Hno; subst. assumption.
- Defined.
+ Program Fixpoint fdRectInner l: forall f, dom f = l -> T f :=
+ match l as l return (forall f, dom f = l -> T f) with
+ | [] => fun f Hdom => Text fdEmpty f _ Temp
+ | k::l' => fun f Hdom => let f' := f \ k in
+ let Hindom: k ∈ dom f := _ in
+ let v' := fdLookup_indom f k Hindom in
+ Text (f' + [fd k <- v' ]) f _
+ (Tstep k v' f' _ (fdRectInner l' f' _))
+ end.
+ Next Obligation.
+ split.
+ - move=>k /=. symmetry. apply fdLookup_notin_strong. rewrite Hdom. tauto.
+ - rewrite Hdom. reflexivity.
+ Qed.
+ Next Obligation.
+ rewrite Hdom. left. reflexivity.
+ Qed.
+ Next Obligation.
+ split.
+ - move=>k'. destruct (dec_eq k k') as [EQ|NEQ].
+ + subst k'. rewrite fdStrongUpdate_eq. symmetry. eapply fdLookup_indom_corr.
+ reflexivity.
+ + erewrite !fdStrongUpdate_neq by assumption. reflexivity.
+ - rewrite Hdom /dom /=. f_equal. rewrite /dom /= Hdom.
+ rewrite DecEq_refl.
+ assert (Hnod := dom_nodup f). rewrite Hdom in Hnod.
+ assert (Hfilt1: (filter_dupes ([])%list l') = l').
+ { apply filter_dupes_id. simpl. inversion Hnod; subst. assumption. }
+ rewrite Hfilt1. apply filter_dupes_id. assumption.
+ Qed.
+ Next Obligation.
+ apply fdLookup_notin. rewrite fdStrongUpdate_eq. reflexivity.
+ Qed.
+ Next Obligation.
+ rewrite /dom /fdStrongUpdate /=.
+ rewrite Hdom. destruct (dec_eq k k) as [_|NEQ]; last (exfalso; now apply NEQ).
+ apply filter_dupes_id with (dupes:=[]); simpl.
+ assert (Hno:= dom_nodup f). rewrite Hdom in Hno.
+ inversion Hno; subst. assumption.
+ Qed.
Definition fdRect: forall f, T f :=
fun f => fdRectInner (dom f) f eq_refl.
diff --git a/lib/ModuRes/SPred.v b/lib/ModuRes/SPred.v
index f89346aa21c94412e568e900f4492bc60c14abbb..b0a3fd28d9d1dcb53b9d8c2ff5df239de6a2d3ef 100644
--- a/lib/ModuRes/SPred.v
+++ b/lib/ModuRes/SPred.v
@@ -16,12 +16,10 @@ Arguments mkSPred _ _ _.
Notation "'p[(' f ')]'" := (mkSPred f _ _).
Section Props.
- Definition sp_constF (P: Prop) :=
- fun n => match n with
- | O => True
- | S _ => P end.
Program Definition sp_const P :=
- p[(sp_constF P)].
+ p[(fun n => match n return _ with
+ | O => True
+ | S _ => P end)].
Next Obligation.
move=>n m Hle. destruct m, n; simpl; tauto || inversion Hle.
Qed.