Commit a936f361 authored by Ralf Jung's avatar Ralf Jung

port iris_wp, iris_meta

parent a1527a82
Require Import ModuRes.PCM.
Module Type CORE_LANG.
Delimit Scope lang_scope with lang.
Local Open Scope lang_scope.
......
......@@ -403,7 +403,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
apply HR; [reflexivity | assumption].
Qed.
Lemma wsat_not_empty σ m (r: res) w k :
Lemma wsat_valid σ m (r: res) w k :
wsat σ m r w (S k) tt -> r.
Proof.
intros [rs [HD _] ]. destruct HD as [VAL _].
......
Require Import ssreflect.
Require Import core_lang masks iris_wp.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
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.
......@@ -10,13 +12,13 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
Section Adequacy.
Local Open Scope mask_scope.
Local Open Scope pcm_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 *)
Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list res -> list vPred -> Prop :=
Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list pres -> list vPred -> Prop :=
| wp_emp : wptp safe m w n nil nil nil
| wp_cons e φ r tp rs φs
(WPE : wp safe m e φ w n r)
......@@ -76,7 +78,7 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
[reflexivity | now apply le_n | now apply mask_emp_disjoint | |].
+ eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |].
rewrite !comp_list_app; simpl comp_list; unfold equiv.
rewrite ->assoc, (comm (Some r)), <- assoc. reflexivity.
rewrite ->assoc, (comm (_ r)), <- assoc. reflexivity.
+ edestruct HS as [w' [r' [HSW [WPE' HE'] ] ] ];
[reflexivity | eassumption | clear WPE HS].
setoid_rewrite HSW. eapply IHn; clear IHn.
......@@ -85,7 +87,7 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
constructor; [eassumption | eapply wptp_closure, WPTP; [assumption | now auto with arith] ].
* eapply wsat_equiv, HE'; [now erewrite mask_emp_union| |reflexivity].
rewrite !comp_list_app; simpl comp_list; unfold equiv.
rewrite ->2!assoc, (comm (Some r')). reflexivity.
rewrite ->2!assoc, (comm (_ r')). reflexivity.
}
(* fork *)
inversion H; subst; clear H.
......@@ -95,7 +97,7 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
[reflexivity | now apply le_n | now apply mask_emp_disjoint | |].
+ eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |].
rewrite !comp_list_app; simpl comp_list; unfold equiv.
rewrite ->assoc, (comm (Some r)), <- assoc. reflexivity.
rewrite ->assoc, (comm (_ r)), <- assoc. reflexivity.
+ specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [HSW [WPE' [WPS HE'] ] ] ] ] ]; clear WPE.
setoid_rewrite HSW. edestruct IHn as [w'' [rs'' [φs'' [HSW'' [HSWTP'' HSE''] ] ] ] ]; first eassumption; first 2 last.
* exists w'' rs'' ([umconst ] ++ φs''). split; [eassumption|].
......@@ -106,20 +108,20 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
constructor; [|now constructor]. eassumption.
* eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
rewrite comp_list_app. simpl comp_list. rewrite !comp_list_app. simpl comp_list.
rewrite (comm (Some rfk) 1). erewrite pcm_op_unit by apply _. unfold equiv.
rewrite (comm _ (Some rfk)). rewrite ->!assoc. apply pcm_op_equiv;[|reflexivity]. unfold equiv.
rewrite <-assoc, (comm (Some rret)), comm. reflexivity.
rewrite (comm (_ rfk)). erewrite ra_op_unit by apply _.
rewrite (comm _ (_ rfk)). rewrite ->!assoc. eapply ra_op_proper;[now apply _ | |reflexivity]. unfold equiv.
rewrite <-assoc, (comm (_ rret)). rewrite (comm (_ rret)). reflexivity.
Qed.
Lemma adequacy_ht {safe m e P Q n k tp' σ σ' w r}
(HT : valid (ht safe m P e Q))
(HSN : stepn n ([e], σ) (tp', σ'))
(HP : P w (n + S k) r)
(HE : wsat σ m (Some r) w @ n + S k) :
(HE : wsat σ m (ra_proj r) w @ n + S k) :
exists w' rs' φs',
w w' /\ wptp safe m w' (S k) tp' rs' (Q :: φs') /\ wsat σ' m (comp_list rs') w' @ S k.
Proof.
edestruct preserve_wptp with (rs:=[r]) as [w' [rs' [φs' [HSW' [HSWTP' HSWS'] ] ] ] ]; [eassumption | | simpl comp_list; erewrite comm, pcm_op_unit by apply _; eassumption | clear HT HSN HP HE].
edestruct preserve_wptp with (rs:=[r]) as [w' [rs' [φs' [HSW' [HSWTP' HSWS'] ] ] ] ]; [eassumption | | simpl comp_list; erewrite comm, ra_op_unit by apply _; eassumption | clear HT HSN HP HE].
- specialize (HT w (n + S k) r). apply HT in HP; try reflexivity; [|now apply unit_min].
econstructor; [|now econstructor]. eassumption.
- exists w' rs' φs'. now auto.
......@@ -133,12 +135,13 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
wptp safe m w' (S k') tp' rs' (Q :: φs') /\ wsat σ' m (comp_list rs') w' @ S k'.
Proof.
destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN.
edestruct (adequacy_ht (w:=fdEmpty) (k:=k') (r:=(ex_own _ σ, pcm_unit _)) HT HSN') as [w' [rs' [φs' [HW [HSWTP HWS] ] ] ] ]; clear HT HSN'.
- exists (pcm_unit _); now rewrite ->pcm_op_unit by apply _.
- hnf. rewrite Plus.plus_comm. exists (fdEmpty (V:=res)). split.
+ assert (HS : Some (ex_own _ σ, pcm_unit _) · 1 = Some (ex_own _ σ, pcm_unit _));
[| now setoid_rewrite HS].
eapply ores_equiv_eq; now erewrite comm, pcm_op_unit by apply _.
pose r := (ex_own _ σ, 1:RL.res).
{ unfold ra_valid. simpl. eapply ra_valid_unit. now apply _. }
edestruct (adequacy_ht (w:=fdEmpty) (k:=k') (r:=r) HT HSN') as [w' [rs' [φs' [HW [HSWTP HWS] ] ] ] ]; clear HT HSN'.
- exists (ra_unit _); now rewrite ->ra_op_unit by apply _.
- hnf. rewrite Plus.plus_comm. exists (fdEmpty (V:=pres)). split.
+ unfold r, comp_map. simpl. rewrite ra_op_unit2. split; first assumption.
reflexivity.
+ intros i _; split; [reflexivity |].
intros _ _ [].
- do 3 eexists. split; [eassumption|]. assumption.
......@@ -170,9 +173,7 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
[reflexivity | unfold lt; reflexivity | now apply mask_emp_disjoint | rewrite mask_emp_union; eassumption |].
fold comp_list in HVal.
specialize (HVal HV); destruct HVal as [w'' [r'' [HSW'' [Hφ'' HE''] ] ] ].
destruct (Some r'' · comp_list rs) as [r''' |] eqn: EQr.
+ assumption.
+ exfalso. eapply wsat_not_empty, HE''. reflexivity.
exact Hφ''.
Qed.
(* Adequacy for safe triples *)
......@@ -192,7 +193,7 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
- rewrite mask_emp_union.
eapply wsat_equiv, HWS; try reflexivity.
rewrite comp_list_app. simpl comp_list.
rewrite ->(assoc (comp_list rs1)), ->(comm (comp_list rs1) (Some r)), <-assoc. reflexivity.
rewrite ->(assoc (comp_list rs1)), ->(comm (comp_list rs1) (ra_proj r)), <-assoc. reflexivity.
- apply HSafe. reflexivity.
Qed.
......@@ -201,11 +202,11 @@ Module IrisMeta (RL : PCM_T) (C : CORE_LANG).
Section Lifting.
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
Local Open Scope ra_scope.
Local Open Scope bi_scope.
Local Open Scope lang_scope.
Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q R : vPred) (r : res).
Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q R : vPred) (r : pres).
Program Definition lift_ePred (φ : expr -=> Prop) : expr -n> Props :=
......
......@@ -30,7 +30,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
- rewrite ->assoc, (comm (_ r1')) in HE'.
exists w2. exists (rd · ra_proj r1').
{ apply wsat_not_empty in HE'. auto_valid. }
{ apply wsat_valid in HE'. auto_valid. }
split; [assumption | split; [| assumption] ].
eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
Qed.
......@@ -223,7 +223,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
clear; intros i; unfold mcup; tauto.
- rewrite ->assoc in HEq.
exists w''. exists (ra_proj rq · ra_proj rr).
{ apply wsat_not_empty in HEq. auto_valid. }
{ apply wsat_valid in HEq. auto_valid. }
split; [assumption | split].
+ unfold lt in HLe0; rewrite ->HSub, HSub', <- HLe0 in Hr; exists rq rr.
split; now auto.
......@@ -231,7 +231,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
clear; intros i; unfold mcup; tauto.
Qed.
Instance limit_preserving_res (P : RL.res -> Prop) : LimitPreserving P.
Instance LP_res (P : RL.res -> Prop) : LimitPreserving P.
Proof.
intros σ σc HPc; simpl. unfold discreteCompl.
now auto.
......
This diff is collapsed.
Require Import List.
Require Import ModuRes.PCM.
Require Import core_lang.
(******************************************************************)
......
......@@ -88,7 +88,6 @@ VFILES:=BI.v\
MetricCore.v\
MetricRec.v\
PCBUltInst.v\
PCM.v\
RA.v\
Predom.v\
PreoMet.v\
......
(** Partial commutative monoids. *)
Require Export Predom.
Require Import MetricCore.
Require Import PreoMet.
Class Associative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
assoc : forall t1 t2 t3, op t1 (op t2 t3) == op (op t1 t2) t3.
Class Commutative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
comm : forall t1 t2, op t1 t2 == op t2 t1.
Section Definitions.
Context (T : Type).
Local Instance eqT : Setoid T | 20000 := discreteType.
Class PCM_unit := pcm_unit : T.
Class PCM_op := pcm_op : option T -> option T -> option T.
Class PCM {TU : PCM_unit} {TOP : PCM_op}: Prop :=
mkPCM {
pcm_op_assoc :> Associative pcm_op;
pcm_op_comm :> Commutative pcm_op;
pcm_op_unit t : pcm_op (Some pcm_unit) t = t;
pcm_op_zero t : pcm_op None t = None
}.
End Definitions.
Notation "1" := (Some (pcm_unit _)) : pcm_scope.
Notation "0" := None : pcm_scope.
Notation "p · q" := (pcm_op _ p q) (at level 40, left associativity) : pcm_scope.
Delimit Scope pcm_scope with pcm.
(* FIXME having this with highest priority is really not a good idea. but necessary. *)
Instance pcm_eq T `{pcmT : PCM T} : Setoid T | 0 := eqT _.
(* PCMs with cartesian products of carriers. *)
Section Products.
Context S T `{pcmS : PCM S, pcmT : PCM T}.
Local Open Scope pcm_scope.
Global Instance pcm_unit_prod : PCM_unit (S * T) := (pcm_unit S, pcm_unit T).
Global Instance pcm_op_prod : PCM_op (S * T) :=
fun ost1 ost2 =>
match ost1, ost2 with
| Some (s1, t1), Some (s2, t2) =>
match Some s1 · Some s2, Some t1 · Some t2 with
| Some sr, Some tr => Some (sr, tr)
| _, _ => None
end
| _, _ => None
end.
Global Instance pcm_prod : PCM (S * T).
Proof.
split.
- intros [[s1 t1] |]; [| reflexivity].
intros [[s2 t2] |]; [| reflexivity].
intros [[s3 t3] |];
[| unfold pcm_op at 1 2, pcm_op_prod;
destruct (Some (s1, t1) · Some (s2, t2)) as [[s t] |]; simpl; tauto].
assert (HS := assoc (Some s1) (Some s2) (Some s3));
assert (HT := assoc (Some t1) (Some t2) (Some t3)).
unfold pcm_op, pcm_op_prod.
destruct (Some s1 · Some s2) as [s12 |];
destruct (Some s2 · Some s3) as [s23 |]; [.. | reflexivity].
+ destruct (Some t1 · Some t2) as [t12 |];
destruct (Some t2 · Some t3) as [t23 |]; [.. | reflexivity].
* destruct (Some s1 · Some s23) as [s |]; destruct (Some s12 · Some s3) as [s' |];
try (reflexivity || contradiction); simpl in HS; subst s'; [].
destruct (Some t1 · Some t23) as [t |]; destruct (Some t12 · Some t3) as [t' |];
try (reflexivity || contradiction); simpl in HT; subst t'; reflexivity.
* erewrite comm, pcm_op_zero in HT by apply _.
destruct (Some t12 · Some t3); [contradiction |].
destruct (Some s12 · Some s3); reflexivity.
* erewrite pcm_op_zero in HT by apply _.
destruct (Some t1 · Some t23); [contradiction |].
destruct (Some s1 · Some s23); reflexivity.
+ erewrite comm, pcm_op_zero in HS by apply _.
destruct (Some t1 · Some t2) as [t12 |]; [| reflexivity].
destruct (Some s12 · Some s3) as [s |]; [contradiction | reflexivity].
+ erewrite pcm_op_zero in HS by apply _.
destruct (Some t2 · Some t3) as [t23 |]; [| reflexivity].
destruct (Some s1 · Some s23); [contradiction | reflexivity].
- intros [[s1 t1] |] [[s2 t2] |]; try reflexivity; []; simpl morph; unfold pcm_op, pcm_op_prod.
assert (HS := comm (Some s1) (Some s2)); assert (HT := comm (Some t1) (Some t2)).
destruct (Some s1 · Some s2); destruct (Some s2 · Some s1); try (contradiction || exact I); [].
destruct (Some t1 · Some t2); destruct (Some t2 · Some t1); try (contradiction || exact I); [].
simpl in HS, HT; subst s0 t0; reflexivity.
- intros [[s t] |]; [| reflexivity]; unfold pcm_op, pcm_op_prod; simpl.
erewrite !pcm_op_unit by eassumption; reflexivity.
- intros st; reflexivity.
Qed.
End Products.
Section Order.
Context T `{pcmT : PCM T}.
Local Open Scope pcm_scope.
Global Instance pcm_op_equiv : Proper (equiv ==> equiv ==> equiv) (pcm_op T).
Proof.
intros [s1 |] [s2 |] EQs; try contradiction; [|];
[intros [t1 |] [t2 |] EQt; try contradiction; [| rewrite (comm (Some s1)), (comm (Some s2)) ] | intros t1 t2 _];
try (erewrite !pcm_op_zero by apply _; reflexivity); [].
simpl in EQs, EQt; subst t2 s2; reflexivity.
Qed.
Definition pcm_ord (t1 t2 : T) :=
exists td, Some td · Some t1 == Some t2.
Global Program Instance PCM_preo : preoType T | 0 := mkPOType pcm_ord.
Next Obligation.
split.
- intros x; eexists; erewrite pcm_op_unit by apply _; reflexivity.
- intros z yz xyz [y Hyz] [x Hxyz]; unfold pcm_ord.
rewrite <- Hyz, assoc in Hxyz; setoid_rewrite <- Hxyz.
destruct (Some x · Some y) as [xy |] eqn: Hxy; [eexists; reflexivity |].
erewrite pcm_op_zero in Hxyz by apply _; contradiction.
Qed.
Definition opcm_ord (t1 t2 : option T) :=
exists otd, otd · t1 == t2.
Global Program Instance opcm_preo : preoType (option T) :=
mkPOType opcm_ord.
Next Obligation.
split.
- intros r; exists 1; erewrite pcm_op_unit by apply _; reflexivity.
- intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
rewrite <- Hxyz, <- Hyz; symmetry; apply assoc.
Qed.
Global Instance equiv_pord_pcm : Proper (equiv ==> equiv ==> equiv) (pord (T := option T)).
Proof.
intros s1 s2 EQs t1 t2 EQt; split; intros [s HS].
- exists s; rewrite <- EQs, <- EQt; assumption.
- exists s; rewrite EQs, EQt; assumption.
Qed.
Global Instance pcm_op_monic : Proper (pord ==> pord ==> pord) (pcm_op _).
Proof.
intros x1 x2 [x EQx] y1 y2 [y EQy]; exists (x · y).
rewrite <- assoc, (comm y), <- assoc, assoc, (comm y1), EQx, EQy; reflexivity.
Qed.
Lemma ord_res_optRes r s :
(r s) <-> (Some r Some s).
Proof.
split; intros HR.
- destruct HR as [d EQ]; exists (Some d); assumption.
- destruct HR as [[d |] EQ]; [exists d; assumption |].
erewrite pcm_op_zero in EQ by apply _; contradiction.
Qed.
Lemma unit_min r : pcm_unit _ r.
Proof.
exists r; now erewrite comm, pcm_op_unit by apply _.
Qed.
End Order.
Section Exclusive.
Context (T: Type).
Local Open Scope pcm_scope.
Inductive pcm_res_ex: Type :=
| ex_own: T -> pcm_res_ex
| ex_unit: pcm_res_ex.
Global Instance pcm_unit_ex : PCM_unit pcm_res_ex := ex_unit.
Global Instance pcm_op_ex : PCM_op pcm_res_ex :=
fun ost1 ost2 =>
match ost1, ost2 with
| Some (ex_own s1), Some ex_unit => Some (ex_own s1)
| Some ex_unit, Some (ex_own s2) => Some (ex_own s2)
| Some ex_unit, Some ex_unit => Some ex_unit
| _, _ => None
end.
Global Instance pcm_ex : PCM pcm_res_ex.
Proof.
split.
- intros [[s1|]|] [[s2|]|] [[s3|]|]; reflexivity.
- intros [[s1|]|] [[s2|]|]; reflexivity.
- intros [[s1|]|]; reflexivity.
- intros [[s1|]|]; reflexivity.
Qed.
End Exclusive.
(* Package of a monoid as a module type (for use with other modules). *)
Module Type PCM_T.
Parameter res : Type.
Declare Instance res_op : PCM_op res.
Declare Instance res_unit : PCM_unit res.
Declare Instance res_pcm : PCM res.
End PCM_T.
(** Resource algebras: Commutative monoids with a decidable validity predicate. *)
Require Import Bool.
Require Export Predom.
Require Import Predom.
Require Import CSetoid.
Require Import MetricCore.
Require Import PreoMet.
......@@ -145,6 +146,12 @@ Section PositiveCarrier.
now erewrite ra_valid_unit by apply _.
Qed.
Lemma ra_proj_cancel r (VAL: r):
ra_proj (ra_mk_pos r (VAL:=VAL)) = r.
Proof.
reflexivity.
Qed.
Lemma ra_op_pos_valid t1 t2 t:
t1 · t2 == ra_proj t -> t1.
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment