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_meta.v b/iris_meta.v
index 01451fe8ef43ded356f02205fe4c12893e187ae3..e43cfe7a41f8921c849ff0327f65fb3d9b2cd664 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -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).