diff --git a/Makefile b/Makefile
index 7e9b4c7264b0d37e5ca48299895607fe3a045817..9a069d7689496c599d9d0b0c3ca15487b84837c7 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_core.v iris_unsafe.v iris_vs.v iris_wp.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_meta.v iris_vs.v iris_wp.v lang.v masks.v world_prop.v -o Makefile
#
.DEFAULT_GOAL := all
@@ -82,10 +82,9 @@ endif
VFILES:=core_lang.v\
iris_core.v\
- iris_unsafe.v\
+ iris_meta.v\
iris_vs.v\
iris_wp.v\
- iris_meta.v\
lang.v\
masks.v\
world_prop.v
diff --git a/README.txt b/README.txt
index 083a4b2af5799dd6595202841003d9791c101798..d0dd05bacb744c269a5bc78dbb0a26b9001ddf35 100644
--- a/README.txt
+++ b/README.txt
@@ -63,7 +63,7 @@ CONTENTS
* iris_wp.v defines weakest preconditions and proves the rules for
Hoare triples
- * iris_unsafe.v proves rules for unsafe Hoare triples
+ * iris_meta.v proves adequacy, robust safety, 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)
diff --git a/iris_core.v b/iris_core.v
index 5c7260882f301732874bbe2ca729837e4dccdb63..2b4a74b21f34f9e8b75eebb9fd85f26bc72e545b 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -24,6 +24,8 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Module Export WP := WorldProp R.
Delimit Scope iris_scope with iris.
+ Local Open Scope ra_scope.
+ Local Open Scope bi_scope.
Local Open Scope iris_scope.
(** Instances for a bunch of types (some don't even have Setoids) *)
@@ -61,24 +63,26 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
(** And now we're ready to build the IRIS-specific connectives! *)
+ Implicit Types (P Q : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (u v : res) (σ : state).
+
Section Necessitation.
(** Note: this could be moved to BI, since it's possible to define
- for any UPred over a monoid. **)
+ for any UPred over a RA. **)
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 ra_pos_unit) _)])].
+ n[(fun P => m[(fun w => mkUPred (fun n r => P w n ra_pos_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.
+ eapply (met_morph_nonexp _ _ P); eassumption.
Qed.
Next Obligation.
intros w1 w2 Subw n r; simpl.
- apply p; assumption.
+ apply P; assumption.
Qed.
Next Obligation.
intros p1 p2 EQp w m r HLt; simpl.
@@ -87,6 +91,34 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
End Necessitation.
+ Notation "â–¡ P" := (box P) (at level 30, right associativity) : iris_scope.
+
+ (** Lemmas about box **)
+ Lemma box_intro P Q (Hpr : □P ⊑ Q) :
+ □P ⊑ □Q.
+ Proof.
+ intros w n r Hp; simpl; apply Hpr, Hp.
+ Qed.
+
+ Lemma box_elim P :
+ □P ⊑ P.
+ Proof.
+ intros w n r Hp; simpl in Hp.
+ eapply uni_pred, Hp; [reflexivity |].
+ now eapply unit_min.
+ 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.
+
(** "Internal" equality **)
Section IntEq.
Context {T} `{mT : metric T}.
@@ -124,10 +156,10 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Section Invariants.
(** Invariants **)
- Definition invP (i : nat) (p : Props) (w : Wld) : UPred pres :=
- intEqP (w i) (Some (ı' p)).
+ Definition invP i P w : UPred pres :=
+ intEqP (w i) (Some (ı' P)).
Program Definition inv i : Props -n> Props :=
- n[(fun p => m[(invP i p)])].
+ n[(fun P => m[(invP i P)])].
Next Obligation.
intros w1 w2 EQw; unfold invP; simpl morph.
destruct n; [apply dist_bound |].
@@ -148,34 +180,38 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
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" := (xist 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" := (xist 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.
+ Section Timeless.
+
+ Definition timelessP P 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 :=
+ 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 |].
+ omega.
+ 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.
+
+ End Timeless.
Section Ownership.
- Local Open Scope ra.
(** Ownership **)
(* We define this on *any* resource, not just the positive (valid) ones.
Note that this makes ownR trivially *False* for invalid u: There is no
- elment v such that u · v = r (where r is valid) *)
+ element v such that u · v = r (where r is valid) *)
Program Definition ownR: res -=> Props :=
s[(fun u => pcmconst (mkUPred(fun n r => u ⊑ ra_proj r) _) )].
Next Obligation.
@@ -186,13 +222,17 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
intros u1 u2 Hequ. intros w n r. split; intros [t Heqt]; exists t; [rewrite <-Hequ|rewrite Hequ]; assumption.
Qed.
- Lemma ownR_sc u t:
- ownR (u · t) == ownR u * ownR t.
+ Lemma ownR_timeless {u} :
+ valid(timeless(ownR u)).
+ Proof. intros w n _ w' k r _ _; now auto. Qed.
+
+ Lemma ownR_sc u v:
+ ownR (u · v) == ownR u * ownR v.
Proof.
intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
- destruct Hut as [s Heq]. rewrite-> assoc in Heq.
exists↓ (s · u) by auto_valid.
- exists↓ t by auto_valid.
+ exists↓ v by auto_valid.
split; [|split].
+ rewrite <-Heq. reflexivity.
+ exists s. reflexivity.
@@ -212,86 +252,40 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
(** Proper physical state: ownership of the machine state **)
Program Definition ownS : state -n> Props :=
- n[(fun s => ownR (ex_own _ s, 1%ra))].
+ n[(fun s => ownR (ex_own _ s, 1))].
Next Obligation.
intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
rewrite EQr. reflexivity.
Qed.
+ Lemma ownS_timeless {σ} : valid(timeless(ownS σ)).
+ Proof. exact ownR_timeless. Qed.
+
(** Proper ghost state: ownership of logical **)
Program Definition ownL : RL.res -n> Props :=
- n[(fun r => ownR (1%ra, r))].
+ n[(fun r : RL.res => ownR (1, r))].
Next Obligation.
intros r1 r2 EQr. destruct n as [| n]; [apply dist_bound |eapply dist_refl].
simpl in EQr. intros w m t. simpl. change ( (ex_unit state, r1) ⊑ (ra_proj t) <-> (ex_unit state, r2) ⊑ (ra_proj t)). rewrite EQr. reflexivity.
Qed.
+ Lemma ownL_timeless {r : RL.res} : valid(timeless(ownL r)).
+ Proof. exact ownR_timeless. Qed.
+
(** Ghost state ownership **)
- Lemma ownL_sc (u t : RL.res) :
- ownL (u · t) == ownL u * ownL t.
+ Lemma ownL_sc (r s : RL.res) :
+ ownL (r · s) == ownL r * ownL s.
Proof.
- assert (Heq: (ex_unit state, u · t) == ((ex_unit state, u) · (ex_unit state, t)) ) by reflexivity.
+ assert (Heq: (1, r · s) == ((1, r) · (1, s)) ) by reflexivity.
(* I cannot believe I have to write this... *)
- change (ownR (ex_unit state, u · t) == ownR (ex_unit state, u) * ownR (ex_unit state, t)).
+ change (ownR (1, r · s) == ownR (1, r) * ownR (1, s)).
rewrite Heq.
now eapply ownR_sc.
Qed.
End Ownership.
- (** 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 |].
- now eapply unit_min.
- 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.
-
- (** 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 |].
- omega.
- 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 WorldSatisfaction.
- Local Open Scope ra_scope.
- Local Open Scope bi_scope.
(* 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
@@ -359,7 +353,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Global Instance preo_unit : preoType () := disc_preo ().
- Program Definition wsat (σ : state) (m : mask) (r : res) (w : Wld) : UPred () :=
+ Program Definition wsat σ m (r : res) w : UPred () :=
â–¹ (mkUPred (fun n _ => exists rs : nat -f> pres,
state_sat (r · (comp_map rs)) σ
/\ forall i (Hm : m i),
@@ -383,7 +377,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
Qed.
- Global Instance wsat_dist n σ m r : Proper (dist n ==> dist n) (wsat σ m r).
+ Global Instance wsat_dist n σ m u : Proper (dist n ==> dist n) (wsat σ m u).
Proof.
intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
split; intros [rs [HE HM] ]; exists rs.
@@ -412,6 +406,39 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
End WorldSatisfaction.
- Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
+ Notation " P @ k " := ((P : UPred ()) k tt) (at level 60, no associativity).
+
+
+ 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.
+
+ (*
+ Simple monotonicity tactics for props and wsat.
+
+ The tactic propsM H proves P w' n' r' given H : P w n r when
+ w ⊑ w', n' <= n, r ⊑ r'
+ are immediate.
+
+ The tactic wsatM is similar.
+ *)
+
+ Lemma propsM {P w n r w' n' r'}
+ (HP : P w n r) (HSw : w ⊑ w') (HLe : n' <= n) (HSr : r ⊑ r') :
+ P w' n' r'.
+ Proof. by apply: (mu_mono _ _ P _ _ HSw); exact: (uni_pred _ _ _ _ _ HLe HSr). Qed.
+
+ Ltac propsM H := solve [ done | apply (propsM H); solve [ done | reflexivity | omega ] ].
+
+ Lemma wsatM {σ m} {r : res} {w n k}
+ (HW : wsat σ m r w @ n) (HLe : k <= n) :
+ wsat σ m r w @ k.
+ Proof. by exact: (uni_pred _ _ _ _ _ HLe). Qed.
+
+ Ltac wsatM H := solve [done | apply (wsatM H); solve [done | omega] ].
End IrisCore.
diff --git a/iris_meta.v b/iris_meta.v
index b60ae7bf6399ab37df832af736f7f31257cc0a2d..effbc85828a4502591f5217bc3c16fbc4324ccbc 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -7,14 +7,13 @@ Set Bullet Behavior "Strict Subproofs".
Module IrisMeta (RL : RA_T) (C : CORE_LANG).
Module Export WP := IrisWP RL C.
- Delimit Scope iris_scope with iris.
+ Local Open Scope lang_scope.
+ Local Open Scope ra_scope.
+ Local Open Scope bi_scope.
Local Open Scope iris_scope.
Section Adequacy.
- Local Open Scope mask_scope.
- Local Open Scope ra_scope.
- Local Open Scope bi_scope.
- Local Open Scope lang_scope.
+
Local Open Scope list_scope.
(* weakest-pre for a threadpool *)
@@ -199,12 +198,154 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
End Adequacy.
- Section Lifting.
+ Set Bullet Behavior "None". (* PDS: Ridiculous. *)
+ Section RobustSafety.
+
+ Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres) (w : Wld) (σ : state).
+
+ Program Definition restrictV (Q : expr -n> Props) : vPred :=
+ n[(fun v => Q (` v))].
+ Next Obligation.
+ move=> v v' Hv w k r; move: Hv.
+ case: n=>[_ Hk | n]; first by exfalso; omega.
+ by move=> /= ->.
+ Qed.
+
+ (*
+ * Primitive reductions are either pure (do not change the state)
+ * or atomic (step to a value).
+ *)
+
+ Hypothesis atomic_dec : forall e, atomic e + ~atomic e.
+
+ Hypothesis pure_step : forall e σ e' σ',
+ ~ atomic e ->
+ prim_step (e, σ) (e', σ') ->
+ σ = σ'.
+
+ Variable E : expr -n> Props.
+
+ (* Compatibility for those expressions wp cares about. *)
+ Hypothesis forkE : forall e, E (fork e) == E e.
+ Hypothesis fillE : forall K e, E (K [[e]]) == E e * E (K [[fork_ret]]).
+
+ (* One can prove forkE, fillE as valid internal equalities. *)
+ Remark valid_intEq {P P' : Props} (H : valid(P === P')) : P == P'.
+ Proof. move=> w n r; exact: H. Qed.
+
+ (* View shifts or atomic triples for every primitive reduction. *)
+ Variable wâ‚€ : Wld.
+ Definition valid₀ P := forall w n r (HSw₀ : w₀ ⊑ w), P w n r.
+
+ Hypothesis pureE : forall {e σ e'},
+ prim_step (e,σ) (e',σ) ->
+ validâ‚€ (vs mask_full mask_full (E e) (E e')).
- Local Open Scope mask_scope.
- Local Open Scope ra_scope.
- Local Open Scope bi_scope.
- Local Open Scope lang_scope.
+ Hypothesis atomicE : forall {e},
+ atomic e ->
+ validâ‚€ (ht false mask_full (E e) e (restrictV E)).
+
+ Lemma robust_safety {e} : validâ‚€(ht false mask_full (E e) e (restrictV E)).
+ Proof.
+ move=> wz nz rz HSwâ‚€ w HSw n r HLe _ He.
+ have {HSw₀ HSw} HSw₀ : w₀ ⊑ w by transitivity wz.
+
+ (* For e = K[fork e'] we'll have to prove wp(e', ⊤), so the IH takes a post. *)
+ pose post Q := forall (v : value) w n r, (E (`v)) w n r -> (Q v) w n r.
+ set Q := restrictV E; have HQ: post Q by done.
+ move: {HLe} HSwâ‚€ He HQ; move: n e w r Q; elim/wf_nat_ind;
+ move=> {wz nz rz} n IH e w r Q HSwâ‚€ He HQ.
+ apply unfold_wp; move=> w' k rf mf σ HSw HLt HD HW.
+ split; [| split; [| split; [| done] ] ]; first 2 last.
+
+ (* e forks: fillE, IH (twice), forkE *)
+ - move=> e' K HDec.
+ have {He} He: (E e) w' k r by propsM He.
+ move: He; rewrite HDec fillE; move=> [re' [rK [Hr [He' HK] ] ] ].
+ exists w' re' rK; split; first by reflexivity.
+ have {IH} IH: forall Q, post Q ->
+ forall e r, (E e) w' k r -> wp false mask_full e Q w' k r.
+ + by move=> Q0 HQ0 e0 r0 He0; apply: (IH _ HLt); first by transitivity w.
+ split; [exact: IH | split]; last first.
+ + by move: HW; rewrite -Hr => HW; wsatM HW.
+ have Htop: post (umconst ⊤) by done.
+ by apply: (IH _ Htop e' re'); move: He'; rewrite forkE.
+
+ (* e value: done *)
+ - move=> {IH} HV; exists w' r; split; [by reflexivity | split; [| done] ].
+ by apply: HQ; propsM He.
+
+ (* e steps: fillE, atomic_dec *)
+ move=> σ' ei ei' K HDec HStep.
+ have {HSw₀} HSw₀ : w₀ ⊑ w' by transitivity w.
+ move: He; rewrite HDec fillE; move=> [rei [rK [Hr [Hei HK] ] ] ].
+ move: HW; rewrite -Hr => HW.
+ (* bookkeeping common to both cases. *)
+ have {Hei} Hei: (E ei) w' (S k) rei by propsM Hei.
+ have HSw': w' ⊑ w' by reflexivity.
+ have HLe: S k <= S k by omega.
+ have H1ei: ra_pos_unit ⊑ rei by apply: unit_min.
+ have HLt': k < S k by omega.
+ move: HW; rewrite {1}mask_full_union -{1}(mask_full_union mask_emp) -assoc => HW.
+ case: (atomic_dec ei) => HA; last first.
+
+ (* ei pure: pureE, IH, fillE *)
+ - move: (pure_step _ _ _ _ HA HStep) => {HA} Hσ.
+ rewrite Hσ in HStep HW => {Hσ}.
+ move: (pureE _ _ _ HStep) => {HStep} He.
+ move: {He} (He w' (S k) r HSwâ‚€) => He.
+ move: {He HLe H1ei Hei} (He _ HSw' _ _ HLe H1ei Hei) => He.
+ move: {HD} (mask_emp_disjoint (mask_full ∪ mask_full)) => HD.
+ move: {He HSw' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [w'' [r' [HSw' [Hei' HW] ] ] ].
+ move: HW; rewrite assoc=>HW.
+ pose↓ α := (ra_proj r' · ra_proj rK).
+ + by apply wsat_valid in HW; auto_valid.
+ have {HSw₀} HSw₀: w₀ ⊑ w'' by transitivity w'.
+ exists w'' α; split; [done| split]; last first.
+ + by move: HW; rewrite 2! mask_full_union => HW; wsatM HW.
+ apply: (IH _ HLt _ _ _ _ HSwâ‚€); last done.
+ rewrite fillE; exists r' rK; split; [exact: equivR | split; [by propsM Hei' |] ].
+ have {HSw} HSw: w ⊑ w'' by transitivity w'.
+ by propsM HK.
+
+ (* ei atomic: atomicE, IH, fillE *)
+ move: (atomic_step _ _ _ _ HA HStep) => HV.
+ move: (atomicE _ HA) => He {HA}.
+ move: {He} (He w' (S k) rei HSwâ‚€) => He.
+ move: {He HLe H1ei Hei} (He _ HSw' _ _ HLe H1ei Hei) => He.
+ (* unroll wp(ei,E)—step case—to get wp(ei',E) *)
+ move: He; rewrite {1}unfold_wp => He.
+ move: {HD} (mask_emp_disjoint mask_full) => HD.
+ move: {He HSw' HLt' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [_ [HS _] ].
+ have Hεei: ei = ε[[ei]] by rewrite fill_empty.
+ move: {HS Hεei HStep} (HS _ _ _ _ Hεei HStep) => [w'' [r' [HSw' [He' HW] ] ] ].
+ (* unroll wp(ei',E)—value case—to get E ei' *)
+ move: He'; rewrite {1}unfold_wp => He'.
+ move: HW; case Hk': k => [| k'] HW.
+ - by exists w'' r'; split; [done | split; [exact: wpO | done] ].
+ have HSw'': w'' ⊑ w'' by reflexivity.
+ have HLt': k' < k by omega.
+ move: {He' HSw'' HLt' HD HW} (He' _ _ _ _ _ HSw'' HLt' HD HW) => [Hv _].
+ move: HV; rewrite -(fill_empty ei') => HV.
+ move: {Hv} (Hv HV) => [w''' [rei' [HSw'' [Hei' HW] ] ] ].
+ (* now IH *)
+ move: HW; rewrite assoc => HW.
+ pose↓ α := (ra_proj rei' · ra_proj rK).
+ + by apply wsat_valid in HW; auto_valid.
+ exists w''' α. split; first by transitivity w''.
+ split; last by rewrite mask_full_union -(mask_full_union mask_emp).
+ rewrite/= in Hei'; rewrite fill_empty -Hk' in Hei' * => {Hk'}.
+ have {HSw₀} HSw₀ : w₀ ⊑ w''' by transitivity w''; first by transitivity w'.
+ apply: (IH _ HLt _ _ _ _ HSwâ‚€); last done.
+ rewrite fillE; exists rei' rK; split; [exact: equivR | split; [done |] ].
+ have {HSw HSw' HSw''} HSw: w ⊑ w''' by transitivity w''; first by transitivity w'.
+ by propsM HK.
+ Qed.
+
+ End RobustSafety.
+ Set Bullet Behavior "Strict Subproofs".
+
+ Section Lifting.
Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q R : vPred) (r : pres).
@@ -221,7 +362,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
Qed.
Program Definition plugExpr safe m φ P Q: expr -n> Props :=
- n[(fun e => (lift_ePred φ e) ∨ (ht safe m P e Q))].
+ n[(fun e' => (lift_ePred φ e') → (ht safe m P e' Q))].
Next Obligation.
intros e1 e2 Heq w n' r HLt.
destruct n as [|n]; [now inversion HLt | simpl in *].
@@ -242,6 +383,6 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
Proof.
Admitted.
- End Lifting.
+ End Lifting.
End IrisMeta.
diff --git a/iris_unsafe.v b/iris_unsafe.v
deleted file mode 100644
index 44a55eda56232b87bb603e59a1f84e918d2eb8c8..0000000000000000000000000000000000000000
--- a/iris_unsafe.v
+++ /dev/null
@@ -1,256 +0,0 @@
-Set Automatic Coercions Import.
-Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import core_lang masks iris_wp.
-Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
-
-Module Unsafety (RL : RA_T) (C : CORE_LANG).
-
- Module Export Iris := IrisWP RL C.
- Local Open Scope mask_scope.
- Local Open Scope ra_scope.
- Local Open Scope bi_scope.
- Local Open Scope lang_scope.
- Local Open Scope iris_scope.
-
- (* PDS: Move to iris_core.v *)
- Lemma ownL_timeless {r : RL.res} :
- valid(timeless(ownL r)).
- Proof. intros w n _ w' k r' HSW HLE. auto. Qed.
-
- (* PDS: Hoist, somewhere. *)
- Program Definition restrictV (Q : expr -n> Props) : vPred :=
- n[(fun v => Q (` v))].
- Solve Obligations using resp_set.
- Next Obligation.
- move=> v v' Hv w k r; move: Hv.
- case: n=>[_ Hk | n]; first by exfalso; omega.
- by move=> /= ->.
- Qed.
-
- Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres) (w : Wld) (σ : state).
-
- (* PDS: Move to iris_wp.v *)
- Lemma htUnsafe {m P e Q} : ht true m P e Q ⊑ ht false m P e Q.
- Proof.
- move=> wz nz rz He w HSw n r HLe Hr HP.
- move: {He P wz nz rz HSw HLe Hr HP} (He _ HSw _ _ HLe Hr HP).
- move: n e Q w r; elim/wf_nat_ind; move=> n IH e Q w r He.
- rewrite unfold_wp; move=> w' k rf mf σ HSw HLt HD Hw.
- move: {IH} (IH _ HLt) => IH.
- move: He => /unfold_wp He; move: {He HSw HLt HD Hw} (He _ _ _ _ _ HSw HLt HD Hw) => [HV [HS [HF _] ] ].
- split; [done | clear HV; split; [clear HF | split; [clear HS | done] ] ].
- - move=> σ' ei ei' K HK Hs.
- move: {HS HK Hs} (HS _ _ _ _ HK Hs) => [w'' [r' [HSw' [He' Hw'] ] ] ].
- exists w'' r'; split; [done | split; [exact: IH | done] ].
- move=> e' K HK.
- move: {HF HK} (HF _ _ HK) => [w'' [rfk [rret [HSw' [Hk [He' Hw'] ] ] ] ] ].
- exists w'' rfk rret; split; [done | split; [exact: IH | split; [exact: IH | done] ] ].
- Qed.
-
- (*
- Adjustments.
-
- PDS: Should be moved or discarded.
- *)
- Notation "p * q" := (BI.sc p q) (at level 40, left associativity) : iris_scope. (* RJ: there's already notation for this in iris_core? *) (* PDS: The notation in Iris core uses sc : UPred (ra_pos res) -> UPred (ra_pos res) -> UPred (ra_pos res) rather than BI.sc. This variant is generic, so it survives more simplification. *)
-
- Lemma wpO {safe m e Q w r} : wp safe m e Q w O r.
- Proof.
- rewrite unfold_wp.
- move=> w' k rf mf σ HSw HLt HD HW.
- by exfalso; omega.
- Qed.
-
- (* Leibniz equality arise from SSR's case tactic.
- RJ: I could use this ;-) move to CSetoid? *) (* PDS: Feel free. I'd like to eventually get everything but the robust safety theorem out of this file. *)
- Lemma equivP {T : Type} `{eqT : Setoid T} {a b : T} : a = b -> a == b.
- Proof. by move=>->; reflexivity. Qed.
-
- (*
- Simple monotonicity tactics for props and wsat.
-
- The tactic propsM H proves P w' n' r' given H : P w n r when
- w ⊑ w', n' <= n, r ⊑ r'
- are immediate.
-
- The tactic wsatM is similar.
-
- PDS: Should be moved.
- *)
-
- Lemma propsM {P w n r w' n' r'}
- (HP : P w n r) (HSw : w ⊑ w') (HLe : n' <= n) (HSr : r ⊑ r') :
- P w' n' r'.
- Proof. by apply: (mu_mono _ _ P _ _ HSw); exact: (uni_pred _ _ _ _ _ HLe HSr). Qed.
-
- Ltac propsM H := solve [ done | apply (propsM H); solve [ done | reflexivity | omega ] ].
-
- Lemma wsatM {σ m} {r : res} {w n k}
- (HW : wsat σ m r w @ n) (HLe : k <= n) :
- wsat σ m r w @ k.
- Proof. by exact: (uni_pred _ _ _ _ _ HLe). Qed.
-
- Ltac wsatM H := solve [done | apply (wsatM H); solve [done | omega] ].
-
- (*
- * Robust safety:
- *
- * Assume E : Exp → Prop satisfies
- *
- * E(fork e) = E e
- * E(K[e]) = E e * E(K[()])
- *
- * and there exist Γ₀, Θ₀ s.t.
- *
- * (i) for every pure reduction ς; e → ς; e',
- * Γ₀ | □Θ₀ ⊢ E e ==>>_⊤ E e'
- *
- * (ii) for every atomic reduction ς; e → ς'; e',
- * Γ₀ | □Θ₀ ⊢ [E e] e [v. E v]_⊤
- *
- * Then, for every e, Γ₀ | □Θ₀ ⊢ [E e] e [v. E v]_⊤.
- *
- * The theorem has applications to security (hence the name).
- *)
- Section RobustSafety.
-
- (*
- * Assume primitive reductions are either pure (do not change the
- * state) or atomic (step to a value).
- *
- * PDS: I suspect we need these to prove the lifting lemmas. If
- * so, they should be in core_lang.v.
- *)
-
- Axiom atomic_dec : forall e, atomic e + ~atomic e.
-
- Axiom pure_step : forall e σ e' σ',
- ~ atomic e ->
- prim_step (e, σ) (e', σ') ->
- σ = σ'.
-
- Parameter E : expr -n> Props.
-
- (* Compatibility for those expressions wp cares about. *)
- Axiom forkE : forall e, E (fork e) == E e.
- Axiom fillE : forall K e, E (K [[e]]) == E e * E (K [[fork_ret]]).
-
- (* One can prove forkE, fillE as valid internal equalities. *)
- Remark valid_intEq {P P' : Props} (H : valid(P === P')) : P == P'.
- Proof. move=> w n r; exact: H. Qed.
-
- (* View shifts or atomic triples for every primitive reduction. *)
- Parameter wâ‚€ : Wld.
- Definition valid₀ P := forall {w n r} (HSw₀ : w₀ ⊑ w), P w n r.
-
- Axiom pureE : forall {e σ e'},
- prim_step (e,σ) (e',σ) ->
- validâ‚€ (vs mask_full mask_full (E e) (E e')).
-
- Axiom atomicE : forall {e},
- atomic e ->
- validâ‚€ (ht false mask_full (E e) e (restrictV E)).
-
- Lemma robust_safety {e} : validâ‚€(ht false mask_full (E e) e (restrictV E)).
- Proof.
- move=> wz nz rz HSwâ‚€ w HSw n r HLe _ He.
- have {HSw₀ HSw} HSw₀ : w₀ ⊑ w by transitivity wz.
-
- (* For e = K[fork e'] we'll have to prove wp(e', ⊤), so the IH takes a post. *)
- pose post Q := forall (v : value) w n r, (E (`v)) w n r -> (Q v) w n r.
- set Q := restrictV E; have HQ: post Q by done.
- move: {HLe} HSwâ‚€ He HQ; move: n e w r Q; elim/wf_nat_ind;
- move=> {wz nz rz} n IH e w r Q HSwâ‚€ He HQ.
- apply unfold_wp; move=> w' k rf mf σ HSw HLt HD HW.
- split; [| split; [| split; [| done] ] ]; first 2 last.
-
- (* e forks: fillE, IH (twice), forkE *)
- - move=> e' K HDec.
- have {He} He: (E e) w' k r by propsM He.
- move: He; rewrite HDec fillE; move=> [re' [rK [Hr [He' HK] ] ] ].
- exists w' re' rK; split; first by reflexivity.
- have {IH} IH: forall Q, post Q ->
- forall e r, (E e) w' k r -> wp false mask_full e Q w' k r.
- + by move=> Q0 HQ0 e0 r0 He0; apply: (IH _ HLt); first by transitivity w.
- split; [exact: IH | split]; last first.
- + by move: HW; rewrite -Hr => HW; wsatM HW.
- have Htop: post (umconst ⊤) by done.
- by apply: (IH _ Htop e' re'); move: He'; rewrite forkE.
-
- (* e value: done *)
- - move=> {IH} HV; exists w' r; split; [by reflexivity | split; [| done] ].
- by apply: HQ; propsM He.
-
- (* e steps: fillE, atomic_dec *)
- move=> σ' ei ei' K HDec HStep.
- have {HSw₀} HSw₀ : w₀ ⊑ w' by transitivity w.
- move: He; rewrite HDec fillE; move=> [rei [rK [Hr [Hei HK] ] ] ].
- move: HW; rewrite -Hr => HW.
- (* bookkeeping common to both cases. *)
- have {Hei} Hei: (E ei) w' (S k) rei by propsM Hei.
- have HSw': w' ⊑ w' by reflexivity.
- have HLe: S k <= S k by omega.
- have H1ei: ra_pos_unit ⊑ rei by apply: unit_min.
- have HLt': k < S k by omega.
- move: HW; rewrite
- {1}mask_full_union -{1}(mask_full_union mask_emp)
- -assoc
- => HW.
- case: (atomic_dec ei) => HA; last first.
-
- (* ei pure: pureE, IH, fillE *)
- - move: (pure_step _ _ _ _ HA HStep) => {HA} Hσ.
- rewrite Hσ in HStep HW => {Hσ}.
- move: (pureE HStep) => {HStep} He.
- move: {He} (He w' (S k) r HSwâ‚€) => He.
- move: {He HLe H1ei Hei} (He _ HSw' _ _ HLe H1ei Hei) => He.
- move: {HD} (mask_emp_disjoint (mask_full ∪ mask_full)) => HD.
- move: {He HSw' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [w'' [r' [HSw' [Hei' HW] ] ] ].
- move: HW; rewrite assoc=>HW.
- pose↓ α := (ra_proj r' · ra_proj rK).
- + by apply wsat_valid in HW; auto_valid.
- have {HSw₀} HSw₀: w₀ ⊑ w'' by transitivity w'.
- exists w'' α; split; [done| split]; last first.
- + by move: HW; rewrite 2! mask_full_union => HW; wsatM HW.
- apply: (IH _ HLt _ _ _ _ HSwâ‚€); last done.
- rewrite fillE; exists r' rK; split; [exact: equivP | split; [by propsM Hei' |] ].
- have {HSw} HSw: w ⊑ w'' by transitivity w'.
- by propsM HK.
-
- (* ei atomic: atomicE, IH, fillE *)
- move: (atomic_step _ _ _ _ HA HStep) => HV.
- move: (atomicE HA) => He {HA}.
- move: {He} (He w' (S k) rei HSwâ‚€) => He.
- move: {He HLe H1ei Hei} (He _ HSw' _ _ HLe H1ei Hei) => He.
- (* unroll wp(ei,E)—step case—to get wp(ei',E) *)
- move: He; rewrite {1}unfold_wp => He.
- move: {HD} (mask_emp_disjoint mask_full) => HD.
- move: {He HSw' HLt' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [_ [HS _] ].
- have Hεei: ei = ε[[ei]] by rewrite fill_empty.
- move: {HS Hεei HStep} (HS _ _ _ _ Hεei HStep) => [w'' [r' [HSw' [He' HW] ] ] ].
- (* unroll wp(ei',E)—value case—to get E ei' *)
- move: He'; rewrite {1}unfold_wp => He'.
- move: HW; case Hk': k => [| k'] HW.
- - by exists w'' r'; split; [done | split; [exact: wpO | done] ].
- have HSw'': w'' ⊑ w'' by reflexivity.
- have HLt': k' < k by omega.
- move: {He' HSw'' HLt' HD HW} (He' _ _ _ _ _ HSw'' HLt' HD HW) => [Hv _].
- move: HV; rewrite -(fill_empty ei') => HV.
- move: {Hv} (Hv HV) => [w''' [rei' [HSw'' [Hei' HW] ] ] ].
- (* now IH *)
- move: HW; rewrite assoc => HW.
- pose↓ α := (ra_proj rei' · ra_proj rK).
- + by apply wsat_valid in HW; auto_valid.
- exists w''' α. split; first by transitivity w''.
- split; last by rewrite mask_full_union -(mask_full_union mask_emp).
- rewrite/= in Hei'; rewrite fill_empty -Hk' in Hei' * => {Hk'}.
- have {HSw₀} HSw₀ : w₀ ⊑ w''' by transitivity w''; first by transitivity w'.
- apply: (IH _ HLt _ _ _ _ HSwâ‚€); last done.
- rewrite fillE; exists rei' rK; split; [exact: equivP | split; [done |] ].
- have {HSw HSw' HSw''} HSw: w ⊑ w''' by transitivity w''; first by transitivity w'.
- by propsM HK.
- Qed.
-
- End RobustSafety.
-
-End Unsafety.
diff --git a/iris_vs.v b/iris_vs.v
index 4f689abc0dd951d4c1a12e39ddef9c77c75e2c32..9a2ba7f9c619a849fa29607645683303ee951438 100644
--- a/iris_vs.v
+++ b/iris_vs.v
@@ -7,20 +7,21 @@ Set Bullet Behavior "Strict Subproofs".
Module IrisVS (RL : RA_T) (C : CORE_LANG).
Module Export CORE := IrisCore RL C.
- Delimit Scope iris_scope with iris.
+ Local Open Scope ra_scope.
+ Local Open Scope bi_scope.
Local Open Scope iris_scope.
+ Implicit Types (P Q R : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (σ : state).
+
Section ViewShifts.
- Local Open Scope mask_scope.
- Local Open Scope ra_scope.
Local Obligation Tactic := intros.
- Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred pres :=
+ Program Definition preVS m1 m2 P w : UPred pres :=
mkUPred (fun n r => forall w1 (rf: res) mf σ k (HSub : w ⊑ w1) (HLe : k < n)
(HD : mf # m1 ∪ m2)
(HE : wsat σ (m1 ∪ mf) (ra_proj r · rf) w1 @ S k),
exists w2 r',
- w1 ⊑ w2 /\ p w2 (S k) r'
+ w1 ⊑ w2 /\ P w2 (S k) r'
/\ wsat σ (m2 ∪ mf) (r' · rf) w2 @ S k) _.
Next Obligation.
intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
@@ -35,8 +36,8 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
Qed.
- Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
- n[(fun p => m[(preVS m1 m2 p)])].
+ Program Definition pvs m1 m2 : Props -n> Props :=
+ n[(fun P => m[(preVS m1 m2 P)])].
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).
@@ -46,7 +47,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
+ 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'; split; [assumption | split].
- * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | omega].
+ * eapply (met_morph_nonexp _ _ P), HP ; [symmetry; eassumption | omega].
* eapply wsat_dist, HE'; [symmetry; eassumption | omega].
- assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
@@ -54,7 +55,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
+ 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'; split; [assumption | split].
- * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | omega].
+ * eapply (met_morph_nonexp _ _ P), HP ; [symmetry; eassumption | omega].
* eapply wsat_dist, HE'; [symmetry; eassumption | omega].
Qed.
Next Obligation.
@@ -71,22 +72,17 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
apply EQp; [now eauto with arith | assumption].
Qed.
- Definition vs (m1 m2 : mask) (p q : Props) : Props :=
- □ (p → pvs m1 m2 q).
+ Definition vs m1 m2 P Q : Props :=
+ □(P → pvs m1 m2 Q).
End ViewShifts.
Section ViewShiftProps.
- Local Open Scope mask_scope.
- Local Open Scope ra_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.
+ 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.
@@ -96,18 +92,18 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
Qed.
- Lemma vsOpen i p :
- valid (vs (mask_sing i) mask_emp (inv i p) (â–¹ p)).
+ 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 14 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
- apply ı in HInv; rewrite ->(isoR p) in HInv.
+ apply ı in HInv; rewrite ->(isoR P) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
destruct HE as [rs [HE HM] ].
destruct (rs i) as [ri |] eqn: HLr.
- - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by (rewrite HLr; reflexivity).
+ - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by now eapply equivR.
rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE.
exists w'.
exists↓ (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
@@ -132,13 +128,13 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
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) ⊤).
+ 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 14 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
- apply ı in HInv; rewrite ->(isoR p) in HInv.
+ apply ı in HInv; rewrite ->(isoR P) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
destruct HE as [rs [HE HM] ].
@@ -149,15 +145,15 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
{ destruct (rs i) as [rsi |] eqn: EQrsi; subst;
[| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid].
clear - HE EQrsi. destruct HE as [HE _].
- rewrite ->comp_map_remove with (i:=i) in HE by (erewrite EQrsi; reflexivity).
+ rewrite ->comp_map_remove with (i:=i) in HE by (eapply equivR; eassumption).
rewrite ->(assoc (_ r)), (comm (_ r)), comm, assoc, <-(assoc (_ rsi) _), (comm _ (ra_proj r)), assoc in HE.
eapply ra_op_valid, ra_op_valid; now eauto with typeclass_instances.
}
exists (fdUpdate i rri rs); split; [| intros j Hm].
- simpl. erewrite ra_op_unit by apply _.
clear - HE EQri. destruct (rs i) as [rsi |] eqn: EQrsi.
- + subst rsi. erewrite <-comp_map_insert_old; [ eassumption | rewrite EQrsi; reflexivity | reflexivity ].
- + unfold rri. subst ri. simpl. erewrite <-comp_map_insert_new; [|rewrite EQrsi; reflexivity]. simpl.
+ + subst rsi. erewrite <-comp_map_insert_old; [ eassumption | eapply equivR; eassumption | reflexivity ].
+ + unfold rri. subst ri. simpl. erewrite <-comp_map_insert_new; [|now eapply equivR]. simpl.
erewrite ra_op_unit by apply _. assumption.
- specialize (HD j); unfold mask_sing, mask_set, mcup in *; simpl in Hm, HD.
destruct (Peano_dec.eq_nat_dec i j);
@@ -179,8 +175,8 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
rewrite <-HR, assoc. 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.
+ 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).
@@ -198,8 +194,8 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
setoid_rewrite HSw12; eauto 8.
Qed.
- Lemma vsEnt p q m :
- □ (p → q) ⊑ vs m m p q.
+ 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.
@@ -208,8 +204,8 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
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).
+ 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.
@@ -270,7 +266,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
Qed.
Program Definition inv' m : Props -n> {n : nat | m n} -n> Props :=
- n[(fun p => n[(fun n => inv n p)])].
+ n[(fun P => n[(fun n : {n | m n} => inv n P)])].
Next Obligation.
intros i i' EQi; destruct n as [| n]; [apply dist_bound |].
simpl in EQi; rewrite EQi; reflexivity.
@@ -297,19 +293,19 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
intros σ σc Hp; apply Hp.
Qed.
- Lemma vsNewInv p m (HInf : mask_infinite m) :
- valid (vs m m (â–¹ p) (xist (inv' m p))).
+ 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).
+ 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) (ra_pos_unit); split; [assumption | split].
+ exists (fdUpdate i (ı' P) w) (ra_pos_unit); split; [assumption | split].
- exists (exist _ i Hm). do 22 red.
unfold proj1_sig. rewrite fdUpdate_eq; reflexivity.
- unfold ra_pos_unit, proj1_sig. erewrite ra_op_unit by apply _.
@@ -321,7 +317,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
}
split.
{
- rewrite <-comp_map_insert_new by (rewrite HRi; reflexivity).
+ rewrite <-comp_map_insert_new by now eapply equivR.
rewrite ->assoc, (comm rf). assumption.
}
intros j Hm'.
diff --git a/iris_wp.v b/iris_wp.v
index 248e7167b514e8c7f43b352acaac6e0e1b0810ba..508ad887ddf6244180acfcceea61f43ed443b674 100644
--- a/iris_wp.v
+++ b/iris_wp.v
@@ -8,15 +8,13 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
Module Export L := Lang C.
Module Export VS := IrisVS RL C.
- Delimit Scope iris_scope with iris.
+ Local Open Scope lang_scope.
+ Local Open Scope ra_scope.
+ Local Open Scope bi_scope.
Local Open Scope iris_scope.
Section HoareTriples.
(* Quadruples, really *)
- Local Open Scope mask_scope.
- Local Open Scope ra_scope.
- Local Open Scope bi_scope.
- Local Open Scope lang_scope.
Instance LP_isval : LimitPreserving is_value.
Proof.
@@ -199,15 +197,11 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
Opaque wp.
- Definition ht safe m P e Q := □ (P → wp safe m e Q).
+ Definition ht safe m P e Q := □(P → wp safe m e Q).
End HoareTriples.
Section HoareTripleProperties.
- Local Open Scope mask_scope.
- Local Open Scope ra_scope.
- Local Open Scope bi_scope.
- Local Open Scope lang_scope.
Existing Instance LP_isval.
@@ -236,7 +230,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
- unfold safeExpr. auto.
Qed.
- Lemma wpO safe m e φ w r : wp safe m e φ w O r.
+ Lemma wpO {safe m e Q w r} : wp safe m e Q w O r.
Proof.
rewrite unfold_wp; intros w'; intros; now inversion HLt.
Qed.
@@ -474,7 +468,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
Lemma htAFrame safe m m' P R e Q
(HD : m # m')
(HAt : atomic e) :
- ht safe m P e Q ⊑ ht safe (m ∪ m') (P * ▹ R) e (lift_bin sc Q (umconst R)).
+ ht safe m P e Q ⊑ ht safe (m ∪ m') (P * ▹R) e (lift_bin sc Q (umconst R)).
Proof.
intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
@@ -521,7 +515,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
(** Fork **)
Lemma htFork safe m P R e :
- ht safe m P e (umconst ⊤) ⊑ ht safe m (▹ P * ▹ R) (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
+ ht safe m P e (umconst ⊤) ⊑ ht safe m (▹P * ▹R) (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
Proof.
intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
destruct n' as [| n']; [apply wpO |].
@@ -550,13 +544,30 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
- right; right; exists e empty_ctx; rewrite ->fill_empty; reflexivity.
Qed.
+ Set Bullet Behavior "None". (* PDS: Ridiculous. *)
+
+ Lemma htUnsafe {m P e Q} : ht true m P e Q ⊑ ht false m P e Q.
+ Proof.
+ move=> wz nz rz He w HSw n r HLe Hr HP.
+ move: {He P wz nz rz HSw HLe Hr HP} (He _ HSw _ _ HLe Hr HP).
+ move: n e Q w r; elim/wf_nat_ind; move=> n IH e Q w r He.
+ rewrite unfold_wp; move=> w' k rf mf σ HSw HLt HD Hw.
+ move: {IH} (IH _ HLt) => IH.
+ move: He => /unfold_wp He; move: {He HSw HLt HD Hw} (He _ _ _ _ _ HSw HLt HD Hw) => [HV [HS [HF _] ] ].
+ split; [done | clear HV; split; [clear HF | split; [clear HS | done] ] ].
+ - move=> σ' ei ei' K HK Hs.
+ move: {HS HK Hs} (HS _ _ _ _ HK Hs) => [w'' [r' [HSw' [He' Hw'] ] ] ].
+ exists w'' r'; split; [done | split; [exact: IH | done] ].
+ move=> e' K HK.
+ move: {HF HK} (HF _ _ HK) => [w'' [rfk [rret [HSw' [Hk [He' Hw'] ] ] ] ] ].
+ exists w'' rfk rret; split; [done | split; [exact: IH | split; [exact: IH | done] ] ].
+ Qed.
+
+ Set Bullet Behavior "Strict Subproofs".
+
End HoareTripleProperties.
Section DerivedRules.
- Local Open Scope mask_scope.
- Local Open Scope ra_scope.
- Local Open Scope bi_scope.
- Local Open Scope lang_scope.
Existing Instance LP_isval.
diff --git a/lib/ModuRes/BI.v b/lib/ModuRes/BI.v
index f05946fc57b81213c7ea8b7622b54ced3ad6c88c..2864bc6d360d5ad0b332c90740c46dde7f997d27 100644
--- a/lib/ModuRes/BI.v
+++ b/lib/ModuRes/BI.v
@@ -102,7 +102,19 @@ Class Later (T : Type) `{pcmT : pcmType T} {vT : Valid T} :=
loeb (t : T) (HL : later t ⊑ t) : valid t
}.
+Delimit Scope bi_scope with bi.
Notation " â–¹ p " := (later p) (at level 20) : bi_scope.
+Notation "⊤" := (top) : bi_scope.
+Notation "⊥" := (bot) : bi_scope.
+Notation "p ∧ q" := (and p q) (at level 40, left associativity) : bi_scope.
+Notation "p ∨ q" := (or p q) (at level 50, left associativity) : bi_scope.
+Notation "p * q" := (sc p q) (at level 40, left associativity) : bi_scope.
+Notation "p → q" := (impl p q) (at level 55, right associativity) : bi_scope.
+Notation "p '-*' q" := (si p q) (at level 55, right associativity) : bi_scope.
+Notation "∀ x , p" := (all n[(fun x => p)]) (at level 60, x ident, no associativity) : bi_scope.
+Notation "∃ x , p" := (xist n[(fun x => p)]) (at level 60, x ident, no associativity) : bi_scope.
+Notation "∀ x : T , p" := (all n[(fun x : T => p)]) (at level 60, x ident, no associativity) : bi_scope.
+Notation "∃ x : T , p" := (xist n[(fun x : T => p)]) (at level 60, x ident, no associativity) : bi_scope.
Require Import UPred.
@@ -144,7 +156,7 @@ Section UPredBI.
Local Open Scope ra_scope.
Local Obligation Tactic := intros; eauto with typeclass_instances.
- Definition pres := ra_pos res.
+ Let pres := âºres.
(* Standard interpretations of propositional connectives. *)
Global Program Instance top_up : topBI (UPred pres) := up_cr (const True).
diff --git a/lib/ModuRes/CSetoid.v b/lib/ModuRes/CSetoid.v
index 223a7089e4ebbe130a164b06fce19e1755a076cb..99b90253ea38646e00bb12d9454e0ea603c8833c 100644
--- a/lib/ModuRes/CSetoid.v
+++ b/lib/ModuRes/CSetoid.v
@@ -16,6 +16,13 @@ Generalizable Variables T U V W.
Definition equiv `{Setoid T} := SetoidClass.equiv.
Arguments equiv {_ _} _ _ /.
+(* Proof by reflexivity *)
+Lemma equivR {T : Type} `{eqT : Setoid T} {a b : T} :
+ a = b -> a == b.
+Proof.
+ intros Heq. subst a. reflexivity.
+Qed.
+
Notation "'mkType' R" := (@Build_Setoid _ R _) (at level 10).
(** A morphism between two types is an actual function together with a
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 1d690ad32193bc072cc9780321bc45da86feabf7..9055f583f353847f60fec607319c411b96e19032 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -30,15 +30,18 @@ Section Definitions.
End Definitions.
Arguments ra_valid {T} {_} t.
+Delimit Scope ra_scope with ra.
+Local Open Scope ra_scope.
+
Notation "1" := (ra_unit _) : ra_scope.
Notation "p · q" := (ra_op _ p q) (at level 40, left associativity) : ra_scope.
Notation "'↓' p" := (ra_valid p) (at level 35) : ra_scope.
-Delimit Scope ra_scope with ra.
(* General RA lemmas *)
Section RAs.
Context {T} `{RA T}.
- Local Open Scope ra_scope.
+
+ Implicit Types (t : T).
Lemma ra_op_unit2 t: t · 1 == t.
Proof.
@@ -66,7 +69,6 @@ End RAs.
(* RAs with cartesian products of carriers. *)
Section Products.
Context S T `{raS : RA S, raT : RA T}.
- Local Open Scope ra_scope.
Global Instance ra_unit_prod : RA_unit (S * T) := (ra_unit S, ra_unit T).
Global Instance ra_op_prod : RA_op (S * T) :=
@@ -96,7 +98,6 @@ End Products.
Section ProductLemmas.
Context {S T} `{raS : RA S, raT : RA T}.
- Local Open Scope ra_scope.
Lemma ra_op_prod_fst (st1 st2: S*T):
fst (st1 · st2) = fst st1 · fst st2.
@@ -121,10 +122,11 @@ End ProductLemmas.
Section PositiveCarrier.
Context {T} `{raT : RA T}.
- Local Open Scope ra_scope.
- Definition ra_pos: Type := { r | ↓ r }.
- Coercion ra_proj (t:ra_pos): T := proj1_sig t.
+ Definition ra_pos: Type := { t : T | ↓ t }.
+ Coercion ra_proj (r:ra_pos): T := proj1_sig r.
+
+ Implicit Types (t u : T) (r : ra_pos).
Global Instance ra_pos_type : Setoid ra_pos := _.
@@ -135,26 +137,26 @@ Section PositiveCarrier.
now eapply ra_valid_unit; apply _.
Qed.
- Lemma ra_proj_cancel r (VAL: ↓r):
- ra_proj (ra_mk_pos r (VAL:=VAL)) = r.
+ Lemma ra_proj_cancel t (VAL: ↓t):
+ ra_proj (ra_mk_pos t (VAL:=VAL)) = t.
Proof.
reflexivity.
Qed.
- Lemma ra_op_pos_valid t1 t2 t:
- t1 · t2 == ra_proj t -> ↓ t1.
+ Lemma ra_op_pos_valid t1 t2 r:
+ t1 · t2 == ra_proj r -> ↓ t1.
Proof.
- destruct t as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
+ destruct r as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
eapply ra_op_valid; eassumption.
Qed.
- Lemma ra_op_pos_valid2 t1 t2 t:
- t1 · t2 == ra_proj t -> ↓ t2.
+ Lemma ra_op_pos_valid2 t1 t2 r:
+ t1 · t2 == ra_proj r -> ↓ t2.
Proof.
rewrite comm. now eapply ra_op_pos_valid.
Qed.
- Lemma ra_pos_valid (r : ra_pos):
+ Lemma ra_pos_valid r:
↓(ra_proj r).
Proof.
destruct r as [r VAL].
@@ -163,6 +165,7 @@ Section PositiveCarrier.
End PositiveCarrier.
Global Arguments ra_pos T {_}.
+Notation "'âº' T" := (ra_pos T) (at level 75) : type_scope.
(** Validity automation tactics *)
Ltac auto_valid_inner :=
@@ -186,10 +189,11 @@ Tactic Notation "pose↓" ident(name) ":=" constr(t) "by" tactic(tac) := pose_va
Section Order.
Context T `{raT : RA T}.
- Local Open Scope ra_scope.
- Definition pra_ord (t1 t2 : ra_pos T) :=
- exists td, td · (ra_proj t1) == (ra_proj t2).
+ Implicit Types (t : T) (r s : ra_pos T).
+
+ Definition pra_ord r1 r2 :=
+ exists t, t · (ra_proj r1) == (ra_proj r2).
Global Instance pra_ord_preo: PreOrder pra_ord.
Proof.
@@ -215,7 +219,7 @@ Section Order.
now erewrite ra_op_unit2 by apply _.
Qed.
- Definition ra_ord (t1 t2 : T) :=
+ Definition ra_ord t1 t2 :=
exists t, t · t1 == t2.
Global Instance ra_ord_preo: PreOrder ra_ord.
@@ -253,16 +257,17 @@ End Order.
Section Exclusive.
Context (T: Type) `{Setoid T}.
- Local Open Scope ra_scope.
-
+
Inductive ra_res_ex: Type :=
| ex_own: T -> ra_res_ex
| ex_unit: ra_res_ex
| ex_bot: ra_res_ex.
- Definition ra_res_ex_eq e1 e2: Prop :=
- match e1, e2 with
- | ex_own s1, ex_own s2 => s1 == s2
+ Implicit Types (r s : ra_res_ex).
+
+ Definition ra_res_ex_eq r s: Prop :=
+ match r, s with
+ | ex_own t1, ex_own t2 => t1 == t2
| ex_unit, ex_unit => True
| ex_bot, ex_bot => True
| _, _ => False
@@ -282,15 +287,15 @@ Section Exclusive.
Global Instance ra_unit_ex : RA_unit ra_res_ex := ex_unit.
Global Instance ra_op_ex : RA_op ra_res_ex :=
- fun e1 e2 =>
- match e1, e2 with
- | ex_own s1, ex_unit => ex_own s1
- | ex_unit, ex_own s2 => ex_own s2
+ fun r s =>
+ match r, s with
+ | ex_own _, ex_unit => r
+ | ex_unit, ex_own _ => s
| ex_unit, ex_unit => ex_unit
| _, _ => ex_bot
end.
Global Instance ra_valid_ex : RA_valid ra_res_ex :=
- fun e => match e with
+ fun r => match r with
| ex_bot => False
| _ => True
end.
@@ -400,7 +405,7 @@ Section InfiniteProduct.
End InfiniteProduct.
-(* Package of a monoid as a module type (for use with other modules). *)
+(* Package a RA as a module type (for use with other modules). *)
Module Type RA_T.
Parameter res : Type.
diff --git a/masks.v b/masks.v
index 4fc39102f6bc9274a0639692e9c4f74e8b8c1927..baae9e2a8cc8a4751faf0348001169f29c2f2e94 100644
--- a/masks.v
+++ b/masks.v
@@ -39,6 +39,7 @@ Qed.
Global Instance mask_type : Setoid mask := mkType meq.
Delimit Scope mask_scope with mask.
+Bind Scope mask_scope with mask.
Notation "m1 ⊆ m2" := (mle m1 m2) (at level 70) : mask_scope.
Notation "m1 ∩ m2" := (mcap m1 m2) (at level 40) : mask_scope.
Notation "m1 \ m2" := (mminus m1 m2) (at level 30) : mask_scope.