Commit 0846921f authored by Ralf Jung's avatar Ralf Jung

re-establish robust safety

parent 76dddf93
Set Automatic Coercions Import. Set Automatic Coercions Import.
Require Import ssreflect ssrfun ssrbool eqtype. Require Import ssreflect ssrfun ssrbool eqtype.
Require Import core_lang masks iris_wp. 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.
Delimit Scope mask_scope with mask. Module Unsafety (RL : RA_T) (C : CORE_LANG).
Module Unsafety (RL : PCM_T) (C : CORE_LANG).
Module Export Iris := IrisWP RL C. Module Export Iris := IrisWP RL C.
Local Open Scope mask_scope. (* clobbers == *) Local Open Scope mask_scope.
Local Open Scope pcm_scope. Local Open Scope ra_scope.
Local Open Scope type_scope. (* so == means setoid equality *)
Local Open Scope bi_scope. Local Open Scope bi_scope.
Local Open Scope lang_scope. Local Open Scope lang_scope.
Local Open Scope iris_scope. Local Open Scope iris_scope.
(* PDS: Why isn't this inferred automatically? If necessary, move this to ris_core.v *)
Global Program Instance res_preorder : PreOrder (pcm_ord res) := @preoPO res (PCM_preo res).
(* PDS: Move to iris_core.v *) (* PDS: Move to iris_core.v *)
Lemma ownL_timeless {r : option RL.res} : Lemma ownL_timeless {r : RL.res} :
valid(timeless(ownL r)). valid(timeless(ownL r)).
Proof. intros w n _ w' k r' HSW HLE; now destruct r. Qed. Proof. intros w n _ w' k r' HSW HLE. auto. Qed.
(* PDS: Hoist, somewhere. *) (* PDS: Hoist, somewhere. *)
Program Definition restrictV (Q : expr -n> Props) : vPred := Program Definition restrictV (Q : expr -n> Props) : vPred :=
...@@ -41,7 +35,7 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG). ...@@ -41,7 +35,7 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG).
move=> Hm; exfalso; exact: HD. move=> Hm; exfalso; exact: HD.
Qed. Qed.
Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : res) (w : Wld) (σ : state). Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres) (w : Wld) (σ : state).
(* PDS: Move to iris_wp.v *) (* PDS: Move to iris_wp.v *)
Lemma htUnsafe {m P e Q} : ht true m P e Q ht false m P e Q. Lemma htUnsafe {m P e Q} : ht true m P e Q ht false m P e Q.
...@@ -70,9 +64,10 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG). ...@@ -70,9 +64,10 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG).
(BI.and (BI.impl p q) (BI.impl q p)). (BI.and (BI.impl p q) (BI.impl q p)).
Notation "P ↔ Q" := (iffBI P Q) (at level 95, no associativity) : iris_scope. Notation "P ↔ Q" := (iffBI P Q) (at level 95, no associativity) : iris_scope.
Notation "p * q" := (BI.sc p q) (at level 40, left associativity) : iris_scope. Notation "p * q" := (BI.sc p q) (at level 40, left associativity) : iris_scope. (* RJ: there's already notation for this in iris_core? *)
Notation "a ⊑%pcm b" := (pcm_ord _ a b) (at level 70, no associativity) : pcm_scope. (* RJ commented out for now, should not be necessary *)
(*Notation "a ⊑%pcm b" := ( _ a b) (at level 70, no associativity) : pcm_scope.*)
Lemma wpO {safe m e Q w r} : wp safe m e Q w O r. Lemma wpO {safe m e Q w r} : wp safe m e Q w O r.
Proof. Proof.
...@@ -82,10 +77,12 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG). ...@@ -82,10 +77,12 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG).
Qed. Qed.
(* Easier to apply (with SSR, at least) than wsat_not_empty. *) (* Easier to apply (with SSR, at least) than wsat_not_empty. *)
(* RJ: Commented out, does not have a multi-zero equivalent
Lemma wsat_nz {σ m w k} : ~ wsat σ m 0 w (S k) tt. Lemma wsat_nz {σ m w k} : ~ wsat σ m 0 w (S k) tt.
Proof. by move=> [rs [HD _] ]; exact: HD. Qed. Proof. by move=> [rs [HD _] ]; exact: HD. Qed. *)
(* Leibniz equality arise from SSR's case tactic. *) (* Leibniz equality arise from SSR's case tactic.
RJ: I could use this ;-) move to CSetoid? *)
Lemma equivP {T : Type} `{eqT : Setoid T} {a b : T} : a = b -> a == b. Lemma equivP {T : Type} `{eqT : Setoid T} {a b : T} : a = b -> a == b.
Proof. by move=>->; reflexivity. Qed. Proof. by move=>->; reflexivity. Qed.
...@@ -108,7 +105,7 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG). ...@@ -108,7 +105,7 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG).
Ltac propsM H := solve [ done | apply (propsM H); solve [ done | reflexivity | omega ] ]. Ltac propsM H := solve [ done | apply (propsM H); solve [ done | reflexivity | omega ] ].
Lemma wsatM {σ m} {r : option res} {w n k} Lemma wsatM {σ m} {r : res} {w n k}
(HW : wsat σ m r w @ n) (HLe : k <= n) : (HW : wsat σ m r w @ n) (HLe : k <= n) :
wsat σ m r w @ k. wsat σ m r w @ k.
Proof. by exact: (uni_pred _ _ _ _ _ HLe). Qed. Proof. by exact: (uni_pred _ _ _ _ _ HLe). Qed.
...@@ -213,11 +210,11 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG). ...@@ -213,11 +210,11 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG).
have {Hei} Hei: (E ei) w' (S k) rei by propsM Hei. have {Hei} Hei: (E ei) w' (S k) rei by propsM Hei.
have HSw': w' w' by reflexivity. have HSw': w' w' by reflexivity.
have HLe: S k <= S k by omega. have HLe: S k <= S k by omega.
have H1ei: pcm_unit _ rei by exact: unit_min. have H1ei: ra_pos_unit rei by apply: unit_min.
have HLt': k < S k by omega. have HLt': k < S k by omega.
move: HW; rewrite move: HW; rewrite
{1}mask_full_union -{1}(mask_full_union mask_emp) {1}mask_full_union -{1}(mask_full_union mask_emp)
-pcm_op_assoc -assoc
=> HW. => HW.
case: (atomic_dec ei) => HA; last first. case: (atomic_dec ei) => HA; last first.
...@@ -229,8 +226,9 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG). ...@@ -229,8 +226,9 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG).
move: {He HLe H1ei Hei} (He _ HSw' _ _ HLe H1ei Hei) => He. move: {He HLe H1ei Hei} (He _ HSw' _ _ HLe H1ei Hei) => He.
move: {HD} (mask_emp_disjoint (mask_full mask_full)) => HD. 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: {He HSw' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [w'' [r' [HSw' [Hei' HW] ] ] ].
move: HW; rewrite pcm_op_assoc. move: HW; rewrite assoc. move=>HW.
case Hα: (Some r' · Some rK)=>[α |] => HW; last by exfalso; exact: (wsat_nz HW). pose α := (ra_proj r' · ra_proj rK).
{ clear -HW. apply wsat_valid in HW. auto_valid. }
have {HSw} HSw: w w'' by transitivity w'. have {HSw} HSw: w w'' by transitivity w'.
exists w'' α; split; [done| split]; last first. exists w'' α; split; [done| split]; last first.
+ by move: HW; rewrite 2! mask_full_union => HW; wsatM HW. + by move: HW; rewrite 2! mask_full_union => HW; wsatM HW.
...@@ -260,9 +258,9 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG). ...@@ -260,9 +258,9 @@ Module Unsafety (RL : PCM_T) (C : CORE_LANG).
move: HV; rewrite -(fill_empty ei') => HV. move: HV; rewrite -(fill_empty ei') => HV.
move: {Hv} (Hv HV) => [w''' [rei' [HSw'' [Hei' HW] ] ] ]. move: {Hv} (Hv HV) => [w''' [rei' [HSw'' [Hei' HW] ] ] ].
(* now IH *) (* now IH *)
move: HW; rewrite pcm_op_assoc. move: HW; rewrite assoc. move=>HW.
case Hα: (Some rei' · _) => [α |] HW; last first. pose α := (ra_proj rei' · ra_proj rK).
- rewrite pcm_op_zero in HW; exfalso; exact: (wsat_nz HW). { clear -HW. apply wsat_valid in HW. auto_valid. }
exists w''' α. split; first by transitivity w''. exists w''' α. split; first by transitivity w''.
split; last by rewrite mask_full_union -(mask_full_union mask_emp). split; last by rewrite mask_full_union -(mask_full_union mask_emp).
rewrite/= in Hei'; rewrite fill_empty -Hk' in Hei' * => {Hk'}. rewrite/= in Hei'; rewrite fill_empty -Hk' in Hei' * => {Hk'}.
......
...@@ -199,8 +199,8 @@ Section Order. ...@@ -199,8 +199,8 @@ Section Order.
Definition pra_ord (t1 t2 : ra_pos T) := Definition pra_ord (t1 t2 : ra_pos T) :=
exists td, td · (ra_proj t1) == (ra_proj t2). exists td, td · (ra_proj t1) == (ra_proj t2).
Global Program Instance pRA_preo : preoType (ra_pos T) | 0 := mkPOType pra_ord. Global Instance pra_ord_preo: PreOrder pra_ord.
Next Obligation. Proof.
split. split.
- intros x; exists 1. simpl. erewrite ra_op_unit by apply _; reflexivity. - intros x; exists 1. simpl. erewrite ra_op_unit by apply _; reflexivity.
- intros z yz xyz [y Hyz] [x Hxyz]; unfold pra_ord. - intros z yz xyz [y Hyz] [x Hxyz]; unfold pra_ord.
...@@ -208,6 +208,8 @@ Section Order. ...@@ -208,6 +208,8 @@ Section Order.
exists (x · y). reflexivity. exists (x · y). reflexivity.
Qed. Qed.
Global Program Instance pRA_preo : preoType (ra_pos T) | 0 := mkPOType pra_ord.
Global Instance equiv_pord_pra : Proper (equiv ==> equiv ==> equiv) (pord (T := ra_pos T)). Global Instance equiv_pord_pra : Proper (equiv ==> equiv ==> equiv) (pord (T := ra_pos T)).
Proof. Proof.
intros s1 s2 EQs t1 t2 EQt; split; intros [s HS]. intros s1 s2 EQs t1 t2 EQt; split; intros [s HS].
...@@ -223,13 +225,16 @@ Section Order. ...@@ -223,13 +225,16 @@ Section Order.
Definition ra_ord (t1 t2 : T) := Definition ra_ord (t1 t2 : T) :=
exists t, t · t1 == t2. exists t, t · t1 == t2.
Global Program Instance ra_preo : preoType T := mkPOType ra_ord.
Next Obligation. Global Instance ra_ord_preo: PreOrder ra_ord.
Proof.
split. split.
- intros r; exists 1; erewrite ra_op_unit by apply _; reflexivity. - intros r; exists 1; erewrite ra_op_unit by apply _; reflexivity.
- intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y). - intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
rewrite <- Hxyz, <- Hyz; symmetry; apply assoc. rewrite <- Hxyz, <- Hyz; symmetry; apply assoc.
Qed. Qed.
Global Program Instance ra_preo : preoType T := mkPOType ra_ord.
Global Instance equiv_pord_ra : Proper (equiv ==> equiv ==> equiv) (pord (T := T)). Global Instance equiv_pord_ra : Proper (equiv ==> equiv ==> equiv) (pord (T := T)).
Proof. 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