From 721698ac1aa0a5f98b01b5d74d4e269a5c3098c4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 24 Feb 2015 10:27:11 +0100
Subject: [PATCH] reorganize files for a more sane structure
---
Makefile | 30 +-
iris_core.v | 178 +----------
iris_derived_rules.v | 37 +++
iris_wp_rules.v => iris_ht_rules.v | 32 +-
iris_meta.v | 11 +-
iris_plog.v | 458 +++++++++++++++++++++++++++++
iris_vs.v => iris_vs_rules.v | 78 +----
iris_wp.v | 213 --------------
8 files changed, 520 insertions(+), 517 deletions(-)
create mode 100644 iris_derived_rules.v
rename iris_wp_rules.v => iris_ht_rules.v (95%)
create mode 100644 iris_plog.v
rename iris_vs.v => iris_vs_rules.v (77%)
delete mode 100644 iris_wp.v
diff --git a/Makefile b/Makefile
index 1d0c327fc..a7e4ef57a 100644
--- a/Makefile
+++ b/Makefile
@@ -1,21 +1,5 @@
-#############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# 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
-#
+# This Makefile started being auto-generated, but now it's hand-crafted and automatically finds all the files.
+# YOU SHOULD NOT HAVE TO EDIT THIS FILE.
.DEFAULT_GOAL := all
@@ -80,15 +64,7 @@ endif
# #
######################
-VFILES:=core_lang.v\
- iris_core.v\
- iris_meta.v\
- iris_vs.v\
- iris_wp.v\
- iris_wp_rules.v\
- lang.v\
- masks.v\
- world_prop.v
+VFILES:=$(wildcard *.v)
-include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES))
diff --git a/iris_core.v b/iris_core.v
index eacbbe386..5609f3f44 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -25,6 +25,9 @@ Module IrisRes (RL : RA_T) (C : CORE_LANG) <: IRIS_RES RL C.
Include IRIS_RES RL C. (* I cannot believe Coq lets me do this... *)
End IrisRes.
+(* This instantiates the framework(s) provided by ModuRes to obtain a higher-order
+ separation logic with ownership, later, necessitation and equality.
+ The logic has "worlds" in its model, but nothing here uses them yet. *)
Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R).
Export C.
Export R.
@@ -160,33 +163,6 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Notation "t1 '===' t2" := (intEq t1 t2) (at level 70) : iris_scope.
- Section Invariants.
-
- (** Invariants **)
- 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)])].
- Next Obligation.
- intros w1 w2 EQw; unfold invP; simpl morph.
- destruct n; [apply dist_bound |].
- apply intEq_dist; [apply EQw | reflexivity].
- Qed.
- Next Obligation.
- intros w1 w2 Sw; unfold invP; simpl morph.
- intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
- destruct (w1 i) as [μ1 |]; [| contradiction].
- destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
- rewrite <- Sw; assumption.
- Qed.
- Next Obligation.
- intros p1 p2 EQp w; unfold invP; simpl morph.
- apply intEq_dist; [reflexivity |].
- apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
- Qed.
-
- End Invariants.
-
Section Timeless.
Definition timelessP P w n :=
@@ -292,130 +268,6 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
End Ownership.
- Section WorldSatisfaction.
-
- (* 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
- constructs. Hopefully we can provide a fold that'd work for
- that at some point
- *)
- Fixpoint comp_list (xs : list pres) : res :=
- match xs with
- | nil => 1
- | (x :: xs)%list => ra_proj x · comp_list xs
- end.
-
- Lemma comp_list_app rs1 rs2 :
- comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
- Proof.
- induction rs1; simpl comp_list; [now rewrite ->ra_op_unit by apply _ |].
- now rewrite ->IHrs1, assoc.
- Qed.
-
- Definition cod (m : nat -f> pres) : list pres := List.map snd (findom_t m).
- Definition comp_map (m : nat -f> pres) : res := comp_list (cod m).
-
- Lemma comp_map_remove (rs : nat -f> pres) i r (HLu : rs i == Some r) :
- comp_map rs == ra_proj r · comp_map (fdRemove i rs).
- Proof.
- destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
- induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
- destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; reflexivity | contradiction |].
- simpl comp_list; rewrite ->IHrs by eauto using SS_tail.
- rewrite-> !assoc, (comm (_ s)); reflexivity.
- Qed.
-
- Lemma comp_map_insert_new (rs : nat -f> pres) i r (HNLu : rs i == None) :
- ra_proj r · comp_map rs == comp_map (fdUpdate i r rs).
- Proof.
- destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
- induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
- destruct (comp i j); [contradiction | reflexivity |].
- simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
- rewrite-> !assoc, (comm (_ r)); reflexivity.
- Qed.
-
- Lemma comp_map_insert_old (rs : nat -f> pres) i r1 r2 r
- (HLu : rs i == Some r1) (HEq : ra_proj r1 · ra_proj r2 == ra_proj r) :
- ra_proj r2 · comp_map rs == comp_map (fdUpdate i r rs).
- Proof.
- destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
- induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
- destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; clear HLu | contradiction |].
- - simpl comp_list; rewrite ->assoc, (comm (_ r2)), <- HEq; reflexivity.
- - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
- rewrite-> !assoc, (comm (_ r2)); reflexivity.
- Qed.
-
- Definition state_sat (r: res) σ: Prop := ↓r /\
- match fst r with
- | ex_own s => s = σ
- | _ => True
- end.
-
- Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
- Proof.
- intros [ [s1| |] r1] [ [s2| |] r2] [EQs EQr] σ1 σ2 EQσ; unfold state_sat; simpl in *; try tauto; try rewrite !EQs; try rewrite !EQr; try rewrite !EQσ; reflexivity.
- Qed.
-
- Global Instance preo_unit : preoType () := disc_preo ().
-
- 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),
- (i ∈ dom rs <-> i ∈ dom w) /\
- forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
- ı π w n ri) _).
- Next Obligation.
- intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
- setoid_rewrite HLe; eassumption.
- Qed.
-
- Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv) (wsat σ).
- Proof.
- intros m1 m2 EQm r r' EQr w1 w2 EQw [| n] []; [reflexivity |].
- split; intros [rs [HE HM] ]; exists rs.
- - split; [rewrite <-EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
- destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
- rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
- - split; [rewrite EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite EQw; apply HM, Hm] ].
- destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
- rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
- Qed.
-
- Global Instance 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.
- - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
- intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
- assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
- destruct (w1 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
- apply ı in EQπ; apply EQπ; [now auto with arith |].
- apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
- apply HR; [reflexivity | assumption].
- - split; [assumption | split; [rewrite (domeq _ _ _ EQw); apply HM, Hm |] ].
- intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
- assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
- destruct (w2 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
- apply ı in EQπ; apply EQπ; [now auto with arith |].
- apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
- apply HR; [reflexivity | assumption].
- Qed.
-
- Lemma wsat_valid σ m (r: res) w k :
- wsat σ m r w (S k) tt -> ↓r.
- Proof.
- intros [rs [HD _] ]. destruct HD as [VAL _].
- eapply ra_op_valid; [now apply _|]. eassumption.
- Qed.
-
- End WorldSatisfaction.
-
- Notation " P @ k " := ((P : UPred ()) k tt) (at level 60, no associativity).
-
-
Lemma valid_iff P :
valid P <-> (⊤ ⊑ P).
Proof.
@@ -424,30 +276,6 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
- 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 IRIS_CORE.
Module IrisCore (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) : IRIS_CORE RL C R WP.
diff --git a/iris_derived_rules.v b/iris_derived_rules.v
new file mode 100644
index 000000000..3d4b04cb8
--- /dev/null
+++ b/iris_derived_rules.v
@@ -0,0 +1,37 @@
+Require Import ssreflect.
+Require Import world_prop core_lang lang masks iris_core iris_plog iris_vs_rules iris_ht_rules.
+Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
+
+Set Bullet Behavior "Strict Subproofs".
+
+Module Type IRIS_DERIVED_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) (VS_RULES: IRIS_VS_RULES RL C R WP CORE PLOG) (HT_RULES: IRIS_HT_RULES RL C R WP CORE PLOG).
+ Export VS_RULES.
+ Export HT_RULES.
+
+ Local Open Scope lang_scope.
+ Local Open Scope ra_scope.
+ Local Open Scope bi_scope.
+ Local Open Scope iris_scope.
+
+ Section DerivedRules.
+
+ Existing Instance LP_isval.
+
+ Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (r : res).
+
+ Lemma vsFalse m1 m2 :
+ valid (vs m1 m2 ⊥ ⊥).
+ Proof.
+ rewrite ->valid_iff, box_top.
+ unfold vs; apply box_intro.
+ rewrite <- and_impl, and_projR.
+ apply bot_false.
+ Qed.
+
+ End DerivedRules.
+
+End IRIS_DERIVED_RULES.
+
+Module IrisDerivedRules (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) (VS_RULES: IRIS_VS_RULES RL C R WP CORE PLOG) (HT_RULES: IRIS_HT_RULES RL C R WP CORE PLOG) : IRIS_DERIVED_RULES RL C R WP CORE PLOG VS_RULES HT_RULES.
+ Include IRIS_DERIVED_RULES RL C R WP CORE PLOG VS_RULES HT_RULES.
+End IrisDerivedRules.
diff --git a/iris_wp_rules.v b/iris_ht_rules.v
similarity index 95%
rename from iris_wp_rules.v
rename to iris_ht_rules.v
index fcb65a786..7d5f1e5f4 100644
--- a/iris_wp_rules.v
+++ b/iris_ht_rules.v
@@ -1,12 +1,11 @@
Require Import ssreflect.
-Require Import world_prop core_lang lang masks iris_core iris_vs iris_wp.
+Require Import world_prop core_lang lang masks iris_core iris_plog.
Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Set Bullet Behavior "Strict Subproofs".
-Module Type IRIS_WP_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (VS: IRIS_VS RL C R WP CORE) (HT: IRIS_HT RL C R WP CORE).
- Export VS.
- Export HT.
+Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE).
+ Export PLOG.
Local Open Scope lang_scope.
Local Open Scope ra_scope.
@@ -374,25 +373,8 @@ Module Type IRIS_WP_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
End HoareTripleProperties.
- Section DerivedRules.
+End IRIS_HT_RULES.
- Existing Instance LP_isval.
-
- Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (r : res).
-
- Lemma vsFalse m1 m2 :
- valid (vs m1 m2 ⊥ ⊥).
- Proof.
- rewrite ->valid_iff, box_top.
- unfold vs; apply box_intro.
- rewrite <- and_impl, and_projR.
- apply bot_false.
- Qed.
-
- End DerivedRules.
-
-End IRIS_WP_RULES.
-
-Module IrisWPRules (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (VS: IRIS_VS RL C R WP CORE) (HT: IRIS_HT RL C R WP CORE) : IRIS_WP_RULES RL C R WP CORE VS HT.
- Include IRIS_WP_RULES RL C R WP CORE VS HT.
-End IrisWPRules.
+Module IrisHTRules (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) : IRIS_HT_RULES RL C R WP CORE PLOG.
+ Include IRIS_HT_RULES RL C R WP CORE PLOG.
+End IrisHTRules.
diff --git a/iris_meta.v b/iris_meta.v
index 6c2f6b323..47d850365 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -1,12 +1,11 @@
Require Import ssreflect.
-Require Import core_lang masks world_prop iris_core iris_vs iris_wp.
+Require Import core_lang masks world_prop iris_core iris_plog.
Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Set Bullet Behavior "Strict Subproofs".
-Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (VS: IRIS_VS RL C R WP CORE) (HT: IRIS_HT RL C R WP CORE).
- Export VS.
- Export HT.
+Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE).
+ Export PLOG.
Local Open Scope lang_scope.
Local Open Scope ra_scope.
@@ -390,6 +389,6 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
End IRIS_META.
-Module IrisMeta (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (VS: IRIS_VS RL C R WP CORE) (HT: IRIS_HT RL C R WP CORE) : IRIS_META RL C R WP CORE VS HT.
- Include IRIS_META RL C R WP CORE VS HT.
+Module IrisMeta (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) : IRIS_META RL C R WP CORE PLOG.
+ Include IRIS_META RL C R WP CORE PLOG.
End IrisMeta.
diff --git a/iris_plog.v b/iris_plog.v
new file mode 100644
index 000000000..b6f23949b
--- /dev/null
+++ b/iris_plog.v
@@ -0,0 +1,458 @@
+Require Import ssreflect.
+Require Import world_prop core_lang lang masks iris_core.
+Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
+
+Set Bullet Behavior "Strict Subproofs".
+
+(* This enriches the Iris core logic with program logic features:
+ Invariants, View Shifts, and Hoare Triples. The last two make use
+ of a notion of "world satisfaction" (which you can also think of
+ as the erasure from logical states to physical ones). *)
+Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP).
+ Export CORE.
+ Module Export L := Lang C.
+
+ Local Open Scope lang_scope.
+ Local Open Scope ra_scope.
+ Local Open Scope bi_scope.
+ Local Open Scope iris_scope.
+
+ Implicit Types (P : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (u v : res) (σ : state) (φ : vPred).
+
+
+
+ Section Invariants.
+
+ (** Invariants **)
+ 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)])].
+ Next Obligation.
+ intros w1 w2 EQw; unfold invP; simpl morph.
+ destruct n; [apply dist_bound |].
+ apply intEq_dist; [apply EQw | reflexivity].
+ Qed.
+ Next Obligation.
+ intros w1 w2 Sw; unfold invP; simpl morph.
+ intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
+ destruct (w1 i) as [μ1 |]; [| contradiction].
+ destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
+ rewrite <- Sw; assumption.
+ Qed.
+ Next Obligation.
+ intros p1 p2 EQp w; unfold invP; simpl morph.
+ apply intEq_dist; [reflexivity |].
+ apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
+ Qed.
+
+ End Invariants.
+
+ Section WorldSatisfaction.
+
+ (* 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
+ constructs. Hopefully we can provide a fold that'd work for
+ that at some point
+ *)
+ Fixpoint comp_list (xs : list pres) : res :=
+ match xs with
+ | nil => 1
+ | (x :: xs)%list => ra_proj x · comp_list xs
+ end.
+
+ Lemma comp_list_app rs1 rs2 :
+ comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
+ Proof.
+ induction rs1; simpl comp_list; [now rewrite ->ra_op_unit by apply _ |].
+ now rewrite ->IHrs1, assoc.
+ Qed.
+
+ Definition cod (m : nat -f> pres) : list pres := List.map snd (findom_t m).
+ Definition comp_map (m : nat -f> pres) : res := comp_list (cod m).
+
+ Lemma comp_map_remove (rs : nat -f> pres) i r (HLu : rs i == Some r) :
+ comp_map rs == ra_proj r · comp_map (fdRemove i rs).
+ Proof.
+ destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
+ induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
+ destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; reflexivity | contradiction |].
+ simpl comp_list; rewrite ->IHrs by eauto using SS_tail.
+ rewrite-> !assoc, (comm (_ s)); reflexivity.
+ Qed.
+
+ Lemma comp_map_insert_new (rs : nat -f> pres) i r (HNLu : rs i == None) :
+ ra_proj r · comp_map rs == comp_map (fdUpdate i r rs).
+ Proof.
+ destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
+ induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
+ destruct (comp i j); [contradiction | reflexivity |].
+ simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
+ rewrite-> !assoc, (comm (_ r)); reflexivity.
+ Qed.
+
+ Lemma comp_map_insert_old (rs : nat -f> pres) i r1 r2 r
+ (HLu : rs i == Some r1) (HEq : ra_proj r1 · ra_proj r2 == ra_proj r) :
+ ra_proj r2 · comp_map rs == comp_map (fdUpdate i r rs).
+ Proof.
+ destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
+ induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
+ destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; clear HLu | contradiction |].
+ - simpl comp_list; rewrite ->assoc, (comm (_ r2)), <- HEq; reflexivity.
+ - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
+ rewrite-> !assoc, (comm (_ r2)); reflexivity.
+ Qed.
+
+ Definition state_sat (r: res) σ: Prop := ↓r /\
+ match fst r with
+ | ex_own s => s = σ
+ | _ => True
+ end.
+
+ Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
+ Proof.
+ intros [ [s1| |] r1] [ [s2| |] r2] [EQs EQr] σ1 σ2 EQσ; unfold state_sat; simpl in *; try tauto; try rewrite !EQs; try rewrite !EQr; try rewrite !EQσ; reflexivity.
+ Qed.
+
+ Global Instance preo_unit : preoType () := disc_preo ().
+
+ 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),
+ (i ∈ dom rs <-> i ∈ dom w) /\
+ forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
+ ı π w n ri) _).
+ Next Obligation.
+ intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
+ setoid_rewrite HLe; eassumption.
+ Qed.
+
+ Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv) (wsat σ).
+ Proof.
+ intros m1 m2 EQm r r' EQr w1 w2 EQw [| n] []; [reflexivity |].
+ split; intros [rs [HE HM] ]; exists rs.
+ - split; [rewrite <-EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
+ destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
+ rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
+ - split; [rewrite EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite EQw; apply HM, Hm] ].
+ destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
+ rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
+ Qed.
+
+ Global Instance 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.
+ - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
+ intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
+ assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
+ destruct (w1 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
+ apply ı in EQπ; apply EQπ; [now auto with arith |].
+ apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
+ apply HR; [reflexivity | assumption].
+ - split; [assumption | split; [rewrite (domeq _ _ _ EQw); apply HM, Hm |] ].
+ intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
+ assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
+ destruct (w2 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
+ apply ı in EQπ; apply EQπ; [now auto with arith |].
+ apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
+ apply HR; [reflexivity | assumption].
+ Qed.
+
+ Lemma wsat_valid σ m (r: res) w k :
+ wsat σ m r w (S k) tt -> ↓r.
+ Proof.
+ intros [rs [HD _] ]. destruct HD as [VAL _].
+ eapply ra_op_valid; [now apply _|]. eassumption.
+ Qed.
+
+ End WorldSatisfaction.
+
+ 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.
+ *)
+
+ 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] ].
+
+ Section ViewShifts.
+ Local Obligation Tactic := intros.
+
+ 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'
+ /\ wsat σ (m2 ∪ mf) (r' · rf) w2 @ S k) _.
+ Next Obligation.
+ intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
+ destruct (HP w1 (rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
+ try assumption; [now eauto with arith | |].
+ - eapply wsat_equiv, HE; try reflexivity.
+ rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
+ - rewrite ->assoc, (comm (_ r1')) in HE'.
+ exists w2. exists↓ (rd · ra_proj r1').
+ { apply wsat_valid in HE'. auto_valid. }
+ split; [assumption | split; [| assumption] ].
+ eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
+ Qed.
+
+ 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).
+ assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
+ edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
+ + eapply wsat_dist, HE; [symmetry; eassumption | omega].
+ + 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 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; [ | ].
+ + eapply wsat_dist, HE; [symmetry; eassumption | omega].
+ + 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 wsat_dist, HE'; [symmetry; eassumption | omega].
+ Qed.
+ Next Obligation.
+ intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
+ etransitivity; eassumption.
+ Qed.
+ Next Obligation.
+ intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
+ - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
+ clear HP; repeat (eexists; try eassumption); [].
+ apply EQp; [now eauto with arith | assumption].
+ - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
+ clear HP; repeat (eexists; try eassumption); [].
+ apply EQp; [now eauto with arith | assumption].
+ Qed.
+
+ Definition vs m1 m2 P Q : Props :=
+ □(P → pvs m1 m2 Q).
+
+ End ViewShifts.
+
+
+ Section HoareTriples.
+ (* Quadruples, really *)
+
+ Instance LP_isval : LimitPreserving is_value.
+ Proof.
+ intros σ σc HC; apply HC.
+ Qed.
+
+ Local Obligation Tactic := intros; eauto with typeclass_instances.
+
+ Definition safeExpr e σ :=
+ is_value e \/
+ (exists σ' ei ei' K, e = K [[ ei ]] /\ prim_step (ei, σ) (ei', σ')) \/
+ (exists e' K, e = K [[ fork e' ]]).
+
+ Definition wpFP safe m (WP : expr -n> vPred -n> Props) e φ w n r :=
+ forall w' k rf mf σ (HSw : w ⊑ w') (HLt : k < n) (HD : mf # m)
+ (HE : wsat σ (m ∪ mf) (ra_proj r · rf) w' @ S k),
+ (forall (HV : is_value e),
+ exists w'' r', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
+ /\ wsat σ (m ∪ mf) (ra_proj r' · rf) w'' @ S k) /\
+ (forall σ' ei ei' K (HDec : e = K [[ ei ]])
+ (HStep : prim_step (ei, σ) (ei', σ')),
+ exists w'' r', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
+ /\ wsat σ' (m ∪ mf) (ra_proj r' · rf) w'' @ k) /\
+ (forall e' K (HDec : e = K [[ fork e' ]]),
+ exists w'' rfk rret, w' ⊑ w''
+ /\ WP (K [[ fork_ret ]]) φ w'' k rret
+ /\ WP e' (umconst ⊤) w'' k rfk
+ /\ wsat σ (m ∪ mf) (ra_proj rfk · ra_proj rret · rf) w'' @ k) /\
+ (forall HSafe : safe = true, safeExpr e σ).
+
+ (* Define the function wp will be a fixed-point of *)
+ Program Definition wpF safe m : (expr -n> vPred -n> Props) -> (expr -n> vPred -n> Props) :=
+ fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP safe m WP e φ w) _)])])].
+ Next Obligation.
+ intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k rf mf σ HSw HLt HD HE.
+ rewrite <- EQr, (comm rd), <- assoc in HE.
+ specialize (Hp w' k (rd · rf) mf σ); destruct Hp as [HV [HS [HF HS' ] ] ];
+ [| omega | ..]; try assumption; [].
+ split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
+ - specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
+ rewrite ->assoc, (comm (_ r1')) in HE'.
+ exists w''. exists↓ (rd · ra_proj r1').
+ { clear -HE'. apply wsat_valid in HE'. auto_valid. }
+ split; [assumption | split; [| assumption] ].
+ eapply uni_pred, Hφ; [| exists rd]; reflexivity.
+ - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
+ rewrite ->assoc, (comm (_ r1')) in HE'. exists w''.
+ destruct k as [| k]; [exists r1'; simpl wsat; tauto |].
+ exists↓ (rd · ra_proj r1').
+ { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+ split; [assumption | split; [| assumption] ].
+ eapply uni_pred, HWP; [| exists rd]; reflexivity.
+ - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
+ destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
+ rewrite ->assoc, <- (assoc (_ rfk)) in HE'.
+ exists w''. exists rfk. exists↓ (rd · ra_proj rret1).
+ { clear- HE'. apply wsat_valid in HE'. rewrite comm. eapply ra_op_valid, ra_op_valid; try now apply _.
+ rewrite ->(comm (_ rfk)) in HE'. eassumption. }
+ repeat (split; try assumption).
+ + eapply uni_pred, HWR; [| exists rd]; reflexivity.
+ + clear -HE'. unfold ra_proj. rewrite ->(comm _ rd) in HE'. exact HE'.
+ - auto.
+ Qed.
+ Next Obligation.
+ intros w1 w2 EQw n' r HLt; simpl; destruct n as [| n]; [now inversion HLt |]; split; intros Hp w2'; intros.
+ - symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
+ edestruct (Hp (extend w2' w1)) as [HV [HS [HF HS'] ] ]; try eassumption;
+ [eapply wsat_dist, HE; [eassumption | omega] |].
+ split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
+ + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
+ assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+ assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+ exists (extend w1'' w2') r'; split; [assumption |].
+ split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
+ eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | omega].
+ + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
+ assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+ assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+ exists (extend w1'' w2') r'; split; [assumption |].
+ split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
+ eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | omega].
+ + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
+ assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+ assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+ exists (extend w1'' w2') rfk rret; split; [assumption |].
+ split; [| split; [| eapply wsat_dist, HE'; [eassumption | omega] ] ];
+ eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; omega.
+ + auto.
+ - assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
+ edestruct (Hp (extend w2' w2)) as [HV [HS [HF HS'] ] ]; try eassumption;
+ [eapply wsat_dist, HE; [eassumption | omega] |].
+ split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF] ] ]; intros.
+ + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
+ assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+ assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+ exists (extend w1'' w2') r'; split; [assumption |].
+ split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
+ eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | omega].
+ + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
+ assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+ assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+ exists (extend w1'' w2') r'; split; [assumption |].
+ split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
+ eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | omega].
+ + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
+ assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+ assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+ exists (extend w1'' w2') rfk rret; split; [assumption |].
+ split; [| split; [| eapply wsat_dist, HE'; [eassumption | omega] ] ];
+ eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; omega.
+ + auto.
+ Qed.
+ Next Obligation.
+ intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
+ etransitivity; eassumption.
+ Qed.
+ Next Obligation.
+ intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
+ split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
+ - split; [| split; [| split] ]; intros.
+ + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+ exists w'' r'; split; [assumption | split; [| assumption] ].
+ apply EQφ, Hφ; omega.
+ + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+ exists w'' r'; split; [assumption | split; [| assumption] ].
+ eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | omega].
+ + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+ exists w'' rfk rret ; repeat (split; try assumption); [].
+ eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | omega].
+ + auto.
+ - split; [| split; [| split] ]; intros.
+ + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+ exists w'' r'; split; [assumption | split; [| assumption] ].
+ apply EQφ, Hφ; omega.
+ + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+ exists w'' r'; split; [assumption | split; [| assumption] ].
+ eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | omega].
+ + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+ exists w'' rfk rret; repeat (split; try assumption); [].
+ eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | omega].
+ + auto.
+ Qed.
+ Next Obligation.
+ intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
+ simpl in EQe; subst e2; reflexivity.
+ Qed.
+
+ Instance contr_wpF safe m : contractive (wpF safe m).
+ Proof.
+ intros n WP1 WP2 EQWP e φ w k r HLt.
+ split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
+ - split; [assumption | split; [| split]; intros].
+ + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
+ exists w'' r'; split; [assumption | split; [| assumption] ].
+ eapply EQWP, HWP; omega.
+ + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+ exists w'' rfk rret; split; [assumption |].
+ split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
+ + auto.
+ - split; [assumption | split; [| split]; intros].
+ + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
+ exists w'' r'; split; [assumption | split; [| assumption] ].
+ eapply EQWP, HWP; omega.
+ + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+ exists w'' rfk rret; split; [assumption |].
+ split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
+ + auto.
+ Qed.
+
+ Definition wp safe m : expr -n> vPred -n> Props :=
+ fixp (wpF safe m) (umconst (umconst ⊤)).
+
+ Lemma unfold_wp safe m :
+ wp safe m == (wpF safe m) (wp safe m).
+ Proof.
+ unfold wp; apply fixp_eq.
+ Qed.
+
+ Opaque wp.
+
+ Lemma wpO {safe m e φ w r} : wp safe m e φ w O r.
+ Proof.
+ rewrite unfold_wp; intros w'; intros; now inversion HLt.
+ Qed.
+
+ Definition ht safe m P e Q := □(P → wp safe m e Q).
+
+ End HoareTriples.
+
+End IRIS_PLOG.
+
+Module IrisPlog (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_PLOG RL C R WP CORE.
+ Include IRIS_PLOG RL C R WP CORE.
+End IrisPlog.
diff --git a/iris_vs.v b/iris_vs_rules.v
similarity index 77%
rename from iris_vs.v
rename to iris_vs_rules.v
index c9edec2f0..5b905802b 100644
--- a/iris_vs.v
+++ b/iris_vs_rules.v
@@ -1,11 +1,11 @@
Require Import ssreflect.
-Require Import world_prop core_lang masks iris_core.
+Require Import world_prop core_lang masks iris_core iris_plog.
Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Set Bullet Behavior "Strict Subproofs".
-Module Type IRIS_VS (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP).
- Export CORE.
+Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE).
+ Export PLOG.
Local Open Scope ra_scope.
Local Open Scope bi_scope.
@@ -13,70 +13,6 @@ Module Type IRIS_VS (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PR
Implicit Types (P Q R : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (σ : state).
- Section ViewShifts.
- Local Obligation Tactic := intros.
-
- 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'
- /\ wsat σ (m2 ∪ mf) (r' · rf) w2 @ S k) _.
- Next Obligation.
- intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
- destruct (HP w1 (rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
- try assumption; [now eauto with arith | |].
- - eapply wsat_equiv, HE; try reflexivity.
- rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
- - rewrite ->assoc, (comm (_ r1')) in HE'.
- exists w2. exists↓ (rd · ra_proj r1').
- { apply wsat_valid in HE'. auto_valid. }
- split; [assumption | split; [| assumption] ].
- eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
- Qed.
-
- 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).
- assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
- edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
- + eapply wsat_dist, HE; [symmetry; eassumption | omega].
- + 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 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; [ | ].
- + eapply wsat_dist, HE; [symmetry; eassumption | omega].
- + 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 wsat_dist, HE'; [symmetry; eassumption | omega].
- Qed.
- Next Obligation.
- intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
- etransitivity; eassumption.
- Qed.
- Next Obligation.
- intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
- - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
- clear HP; repeat (eexists; try eassumption); [].
- apply EQp; [now eauto with arith | assumption].
- - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
- clear HP; repeat (eexists; try eassumption); [].
- apply EQp; [now eauto with arith | assumption].
- Qed.
-
- Definition vs m1 m2 P Q : Props :=
- □(P → pvs m1 m2 Q).
-
- End ViewShifts.
-
Section ViewShiftProps.
Lemma vsTimeless m P :
@@ -330,8 +266,8 @@ Module Type IRIS_VS (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PR
End ViewShiftProps.
-End IRIS_VS.
+End IRIS_VS_RULES.
-Module IrisVS (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_VS RL C R WP CORE.
- Include IRIS_VS RL C R WP CORE.
-End IrisVS.
+Module IrisVSRules (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE): IRIS_VS_RULES RL C R WP CORE PLOG.
+ Include IRIS_VS_RULES RL C R WP CORE PLOG.
+End IrisVSRules.
diff --git a/iris_wp.v b/iris_wp.v
deleted file mode 100644
index 7dd2fd703..000000000
--- a/iris_wp.v
+++ /dev/null
@@ -1,213 +0,0 @@
-Require Import ssreflect.
-Require Import world_prop core_lang lang masks iris_core.
-Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
-
-Set Bullet Behavior "Strict Subproofs".
-
-Module Type IRIS_HT (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP).
- Export CORE.
- Module Export L := Lang C.
-
- Local Open Scope lang_scope.
- Local Open Scope ra_scope.
- Local Open Scope bi_scope.
- Local Open Scope iris_scope.
-
- Section HoareTriples.
- (* Quadruples, really *)
-
- Instance LP_isval : LimitPreserving is_value.
- Proof.
- intros σ σc HC; apply HC.
- Qed.
-
- Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : vPred) (r : pres).
-
- Local Obligation Tactic := intros; eauto with typeclass_instances.
-
- Definition safeExpr e σ :=
- is_value e \/
- (exists σ' ei ei' K, e = K [[ ei ]] /\ prim_step (ei, σ) (ei', σ')) \/
- (exists e' K, e = K [[ fork e' ]]).
-
- Definition wpFP safe m (WP : expr -n> vPred -n> Props) e φ w n r :=
- forall w' k rf mf σ (HSw : w ⊑ w') (HLt : k < n) (HD : mf # m)
- (HE : wsat σ (m ∪ mf) (ra_proj r · rf) w' @ S k),
- (forall (HV : is_value e),
- exists w'' r', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
- /\ wsat σ (m ∪ mf) (ra_proj r' · rf) w'' @ S k) /\
- (forall σ' ei ei' K (HDec : e = K [[ ei ]])
- (HStep : prim_step (ei, σ) (ei', σ')),
- exists w'' r', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
- /\ wsat σ' (m ∪ mf) (ra_proj r' · rf) w'' @ k) /\
- (forall e' K (HDec : e = K [[ fork e' ]]),
- exists w'' rfk rret, w' ⊑ w''
- /\ WP (K [[ fork_ret ]]) φ w'' k rret
- /\ WP e' (umconst ⊤) w'' k rfk
- /\ wsat σ (m ∪ mf) (ra_proj rfk · ra_proj rret · rf) w'' @ k) /\
- (forall HSafe : safe = true, safeExpr e σ).
-
- (* Define the function wp will be a fixed-point of *)
- Program Definition wpF safe m : (expr -n> vPred -n> Props) -> (expr -n> vPred -n> Props) :=
- fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP safe m WP e φ w) _)])])].
- Next Obligation.
- intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k rf mf σ HSw HLt HD HE.
- rewrite <- EQr, (comm rd), <- assoc in HE.
- specialize (Hp w' k (rd · rf) mf σ); destruct Hp as [HV [HS [HF HS' ] ] ];
- [| omega | ..]; try assumption; [].
- split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
- - specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
- rewrite ->assoc, (comm (_ r1')) in HE'.
- exists w''. exists↓ (rd · ra_proj r1').
- { clear -HE'. apply wsat_valid in HE'. auto_valid. }
- split; [assumption | split; [| assumption] ].
- eapply uni_pred, Hφ; [| exists rd]; reflexivity.
- - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
- rewrite ->assoc, (comm (_ r1')) in HE'. exists w''.
- destruct k as [| k]; [exists r1'; simpl wsat; tauto |].
- exists↓ (rd · ra_proj r1').
- { clear- HE'. apply wsat_valid in HE'. auto_valid. }
- split; [assumption | split; [| assumption] ].
- eapply uni_pred, HWP; [| exists rd]; reflexivity.
- - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
- destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
- rewrite ->assoc, <- (assoc (_ rfk)) in HE'.
- exists w''. exists rfk. exists↓ (rd · ra_proj rret1).
- { clear- HE'. apply wsat_valid in HE'. rewrite comm. eapply ra_op_valid, ra_op_valid; try now apply _.
- rewrite ->(comm (_ rfk)) in HE'. eassumption. }
- repeat (split; try assumption).
- + eapply uni_pred, HWR; [| exists rd]; reflexivity.
- + clear -HE'. unfold ra_proj. rewrite ->(comm _ rd) in HE'. exact HE'.
- - auto.
- Qed.
- Next Obligation.
- intros w1 w2 EQw n' r HLt; simpl; destruct n as [| n]; [now inversion HLt |]; split; intros Hp w2'; intros.
- - symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
- edestruct (Hp (extend w2' w1)) as [HV [HS [HF HS'] ] ]; try eassumption;
- [eapply wsat_dist, HE; [eassumption | omega] |].
- split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
- + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
- assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
- assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') r'; split; [assumption |].
- split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
- eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | omega].
- + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
- assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
- assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') r'; split; [assumption |].
- split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
- eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | omega].
- + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
- assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
- assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') rfk rret; split; [assumption |].
- split; [| split; [| eapply wsat_dist, HE'; [eassumption | omega] ] ];
- eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; omega.
- + auto.
- - assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
- edestruct (Hp (extend w2' w2)) as [HV [HS [HF HS'] ] ]; try eassumption;
- [eapply wsat_dist, HE; [eassumption | omega] |].
- split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF] ] ]; intros.
- + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
- assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
- assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') r'; split; [assumption |].
- split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
- eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | omega].
- + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
- assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
- assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') r'; split; [assumption |].
- split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
- eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | omega].
- + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
- assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
- assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') rfk rret; split; [assumption |].
- split; [| split; [| eapply wsat_dist, HE'; [eassumption | omega] ] ];
- eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; omega.
- + auto.
- Qed.
- Next Obligation.
- intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
- etransitivity; eassumption.
- Qed.
- Next Obligation.
- intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
- split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
- - split; [| split; [| split] ]; intros.
- + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
- exists w'' r'; split; [assumption | split; [| assumption] ].
- apply EQφ, Hφ; omega.
- + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
- exists w'' r'; split; [assumption | split; [| assumption] ].
- eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | omega].
- + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
- exists w'' rfk rret ; repeat (split; try assumption); [].
- eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | omega].
- + auto.
- - split; [| split; [| split] ]; intros.
- + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
- exists w'' r'; split; [assumption | split; [| assumption] ].
- apply EQφ, Hφ; omega.
- + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
- exists w'' r'; split; [assumption | split; [| assumption] ].
- eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | omega].
- + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
- exists w'' rfk rret; repeat (split; try assumption); [].
- eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | omega].
- + auto.
- Qed.
- Next Obligation.
- intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
- simpl in EQe; subst e2; reflexivity.
- Qed.
-
- Instance contr_wpF safe m : contractive (wpF safe m).
- Proof.
- intros n WP1 WP2 EQWP e φ w k r HLt.
- split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
- - split; [assumption | split; [| split]; intros].
- + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
- exists w'' r'; split; [assumption | split; [| assumption] ].
- eapply EQWP, HWP; omega.
- + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
- exists w'' rfk rret; split; [assumption |].
- split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
- + auto.
- - split; [assumption | split; [| split]; intros].
- + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
- exists w'' r'; split; [assumption | split; [| assumption] ].
- eapply EQWP, HWP; omega.
- + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
- exists w'' rfk rret; split; [assumption |].
- split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
- + auto.
- Qed.
-
- Definition wp safe m : expr -n> vPred -n> Props :=
- fixp (wpF safe m) (umconst (umconst ⊤)).
-
- Lemma unfold_wp safe m :
- wp safe m == (wpF safe m) (wp safe m).
- Proof.
- unfold wp; apply fixp_eq.
- Qed.
-
- Opaque wp.
-
- 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.
-
- Definition ht safe m P e Q := □(P → wp safe m e Q).
-
- End HoareTriples.
-
-End IRIS_HT.
-
-Module IrisHT (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_HT RL C R WP CORE.
- Include IRIS_HT RL C R WP CORE.
-End IrisHT.
--
GitLab