diff --git a/iris_meta.v b/iris_meta.v
index 790aad26a9da2dc8ecf36e69276d09dcfbf87772..c3af7e374ec7b45572bf63924eeb5f266fee12c8 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -199,144 +199,125 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Section RobustSafety.
- Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : res) (w : Wld) (σ : state).
+ Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (v : value) (Q : vPred) (r : res) (w : Wld) (σ : state).
- Program Definition restrictV (Q : expr -n> Props) : vPred :=
- n[(fun v => Q (` v))].
+ 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.
- (*
- * 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. *)
+ Definition fork_compat E := forall e,
+ E (fork e) == E e.
+
+ Definition fill_compat E := forall K e,
+ E (K [[e]]) == E e * E (K [[fork_ret]]).
+
+ (* One can prove fork_compat, fill_compat as valid internal equalities. *)
(* RJ: We don't have rules for internal equality of propositions, don't we? Maybe we should have an axiom,
saying they are equal iff they are equivalent. *)
(* PDS: Would you like to flush out §5.1 of the appendix? *)
- Remark valid_intEq {P P' : Props} (H : valid(P === P')) : P == P'.
+ Remark valid_intEq {P P'} (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')).
+ Definition pure e := forall σ e' σ',
+ prim_step (e,σ) (e',σ') ->
+ σ == σ'.
+
+ Definition restrict_lang := forall e,
+ reducible e ->
+ atomic e \/ pure e.
- Hypothesis atomicE : forall {e},
+ Definition atomic_compat E Θ m := forall e,
atomic e ->
- validâ‚€ (ht false mask_full (E e) e (restrictV E)).
+ Θ ⊑ ht false m (E e) e (restrictV E).
- Lemma robust_safety {e} : validâ‚€(ht false mask_full (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}
+ (FORK : fork_compat E)
+ (FILL : fill_compat E)
+ (LANG : restrict_lang)
+ (HT : atomic_compat E Θ m)
+ (VS : pure_compat E Θ m) :
+ □Θ ⊑ ht false m (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.
+ 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: (propsM HSw HLe (prefl 1) 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: {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; exact: (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.
- set HSw' := prefl w'.
- set HLe := lerefl (S k).
- have H1ei: 1 ⊑ rei by apply: unit_min.
+ 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.
+ split.
+ (* e value *)
+ { move=> HV {FORK FILL LANG HT VS IH}.
+ exists w' r. split; [by reflexivity | split; [| done] ].
+ apply: HQ; have HLe: S k <= n by omega.
+ exact: (propsM HSw HLe (prefl r)). }
+ split; [| split; [| done] ]; first last.
+ (* e forks *)
+ { move=> e' K HDec {LANG HT VS}.
+ have HLe: k <= n by omega.
+ move/(propsM HSw HLe (prefl r)): He => He.
+ move/(propsM HSw HLe (prefl 1)): HΘ => HΘ {HLe}.
+ move: He; rewrite HDec FILL FORK; move=> [re' [rK [Hr [He' HK] ] ] ].
+ exists w' re' rK. split; [by reflexivity | split; [exact: IH | split; [exact: IH |] ] ].
+ by move: HW; rewrite -Hr; exact: wsatM. }
+ (* e steps *)
+ move=> σ' ei ei' K HDec HStep {FORK}.
+ move: He; rewrite HDec FILL; move=> [rei [rK [Hr [Hei HK] ] ] ].
+ move: HW; rewrite -Hr -assoc => HW {Hr r}.
+ (* both forthcoming cases work at step-indices S k and (for the IH) k. *)
+ have HLe: S k <= n by omega.
have HLt': k < S k by done.
- 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.
- have {HSw₀} HSw₀: w₀ ⊑ w'' by transitivity w'.
- exists w'' (r' · rK); split; [done| split]; last first.
- { by move: HW; rewrite 2! mask_full_union => HW; exact: (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.
+ move/(propsM HSw HLe (prefl rei)): Hei => Hei.
+ move/(propsM HSw HLe (prefl rK)): HK => HK.
+ 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 _ _ _ HΘ _ HSw _ _ HLe (unit_min _ rei) 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]; last by move/(wsatM HLe'): HW'; rewrite assoc.
+ apply: (IH _ HLt); last done.
+ { have HLe: k <= n by omega.
+ by exact: (propsM (ptrans w' HSw HSw') HLe (prefl 1) HΘ). }
+ rewrite FILL; exists r' rK. split; first by reflexivity.
+ split; [ exact: (propsMN HLe') | exact: (propsM HSw' HLe' (prefl rK) HK) ]. }
+ (* atomic step *)
+ move/(_ _ HA _ _ _ HΘ _ HSw (S k) _ HLe (unit_min _ rei) Hei): HT => {Hei HLe} Hei.
(* 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 _] ].
+ move: Hei; rewrite {1}unfold_wp => Hei.
+ move/(_ _ _ _ _ _ (prefl w') HLt' HD HW): Hei => [_ [HS _] ] {HLt' HW}.
have Hεei: ei = ε[[ei]] by rewrite fill_empty.
- move: {HS Hεei HStep} (HS _ _ _ _ Hεei HStep) => [w'' [r' [HSw' [He' HW] ] ] ].
+ move/(_ _ _ _ _ Hεei HStep): HS => [w'' [r' [HSw' [Hei' HW'] ] ] ] {Hεei}.
(* 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: Hei'; rewrite (fill_empty ei') {1}unfold_wp => Hei'.
+ move: HLt HK HW' Hei'; case: k => [| k'] 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.
- exists w''' (rei' · rK). 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.
+ move: (ptrans w'' HSw' HSw'') => HSw''' {HSw''}.
+ exists w''' (rei' · rK). split; [done | split; [| done] ].
+ apply: (IH _ HLt); last done.
+ { have HLe: S k' <= n by omega.
+ by exact: (propsM (ptrans w' HSw HSw''') HLe (prefl 1) HΘ). }
+ rewrite FILL; exists rei' rK. split; [by reflexivity | split; [done |] ].
+ have HLe: S k' <= S (S k') by omega.
+ exact: (propsM HSw''' HLe (prefl rK)).
Qed.
End RobustSafety.
@@ -391,7 +372,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
{ clear - HPS HW HSw2.
move: HPS => [r1 [r2 [Hr [_ /(propsMW HSw2) HS ] ] ] ] {HSw2}.
apply: (ownS_wsat HS HW); move=> {HS HW}.
- exists (r1 · rf); move: Hr=><-.
+ exists (r1 · rf). move: Hr=><-.
by rewrite -{1}assoc [rf · _]comm {1}assoc; reflexivity. }
split; [| split; [| split ] ]; first 2 last.
{ move=> e' K HDec; exfalso; exact: (reducible_not_fork RED HDec). }
@@ -418,17 +399,17 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
{ have {HLt} HLt: k <= n' by omega.
move/(propsMW HSw2): HP; move/(propsMN HLt) => HP.
have HS': (ownS σ') w2 k rS' by exists 1; rewrite ra_op_unit; split; reflexivity.
- exists rP rS'; split; [by reflexivity | split; [done | done] ]. }
+ exists rP rS'. split; [by reflexivity | split; [done | done] ]. }
move/(_ (e',σ') _ HSw1 _ rz (lerefl nz) (prefl rz) He'): {He'} Hfrom => He'.
have {HLe HLt} HLe: k <= nz by omega.
move/(_ _ HSw2 _ r' HLe (unit_min _ _) HPS): He' => He' {HLe HPS}.
(* wsat σ' r' follows from wsat σ r (by the construction of r'). *)
- exists w2 r'; split; [by reflexivity | split; [done |] ].
+ exists w2 r'. split; [by reflexivity | split; [done |] ].
have HLe: k <= S k by omega.
move/(wsatM HLe): HW; move=>{He' HLe}.
case: k=>[| k]; first done; move=>[rs [Hstate HWld] ].
- exists rs; split; last done.
+ exists rs. split; last done.
clear - Hr HrS Hstate; move: Hstate=>[Hv _]; move: Hv.
rewrite -Hr -HrS /r'/= => {Hr HrS r' rS}.
rewrite (* ((P(gσ))f)s *) [rP · _]comm -3!assoc =>/ra_opV2 Hv {rSg}. (* ((σP)f)s *)
diff --git a/iris_plog.v b/iris_plog.v
index 553ba9c5f35c81ffd1b3fed0e97e52910af5dab8..fb84350cb710d4a412bdc1851dea5332900776d0 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -178,21 +178,16 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Notation " P @ k " := ((P : UPred ()) k tt) (at level 60, no associativity).
- (*
- 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.
- *)
+ (* Simple view lemmas. *)
Lemma prefl {T} `{oT : preoType T} (t : T) : t ⊑ t. Proof. by reflexivity. Qed.
- Definition lerefl (n : nat) : n <= n. Proof. by reflexivity. Qed.
+ Lemma ptrans {T} `{oT : preoType T} {t t''} (t' : T) (HL : t ⊑ t') (HU : t' ⊑ t'') : t ⊑ t''.
+ Proof. by transitivity t'. Qed.
+
+ Lemma lerefl (n : nat) : n <= n. Proof. by reflexivity. Qed.
- Definition lt0 (n : nat) : ~ n < 0. Proof. by omega. Qed.
+ Lemma lt0 (n : nat) : ~ n < 0. Proof. by omega. Qed.
Lemma propsMW {P w n r w'} (HSw : w ⊑ w') : P w n r -> P w' n r.
Proof. exact: (mu_mono _ _ P _ _ HSw). Qed.
@@ -206,12 +201,9 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Lemma propsMR {P w n r r'} (HSr : r ⊑ r') : P w n r -> P w n r'.
Proof. exact: (propsMNR (lerefl n) HSr). Qed.
- 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: (propsMW HSw); exact: (propsMNR HLe HSr). Qed.
-
- Ltac propsM H := solve [ done | apply (propsM H); solve [ done | reflexivity | omega ] ].
+ Lemma propsM {P w n r w' n' r'} (HSw : w ⊑ w') (HLe : n' <= n) (HSr : r ⊑ r') :
+ P w n r -> P w' n' r'.
+ Proof. move=> HP; by apply: (propsMW HSw); exact: (propsMNR HLe HSr). Qed.
Lemma wsatM {σ m} {r : res} {w n k} (HLe : k <= n) :
wsat σ m r w @ n -> wsat σ m r w @ k.