Commit 800af69d authored by Janno's avatar Janno

merge master with ra-constructions

parents dc078e32 c84fed03
......@@ -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
......
......@@ -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)
......
......@@ -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.
......@@ -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.