Commit c85f63e2 authored by Ralf Jung's avatar Ralf Jung

refactor wp adequacy: add and use a dedicated lemma for "preserving wptp"

parent 9b6f2c6e
Require Import world_prop core_lang lang masks.
Require Import world_prop core_lang masks.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
......@@ -10,7 +10,7 @@ Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
End IrisRes.
Module IrisCore (RL : PCM_T) (C : CORE_LANG).
Module Export L := Lang C.
Export C.
Module Export R := IrisRes RL C.
Module Export WP := WorldProp R.
......@@ -310,6 +310,13 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
| (x :: xs)%list => Some 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 pcm_op_unit by apply _ |].
now rewrite IHrs1, assoc.
Qed.
Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
Definition comp_map (m : nat -f> res) : option res := comp_list (cod m).
......
Require Import world_prop core_lang masks iris_vs.
Require Import ssreflect.
Require Import world_prop core_lang lang masks iris_vs.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Module IrisWP (RL : PCM_T) (C : CORE_LANG).
Module Export L := Lang C.
Module Export VS := IrisVS RL C.
Delimit Scope iris_scope with iris.
......@@ -22,11 +24,17 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
intros σ σc HC; apply HC.
Qed.
Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : value -n> Props) (r : res).
(* We use this type quite a bit, so give it and its instances names *)
Definition vPred := value -n> Props.
Global Instance vPred_type : Setoid vPred := _.
Global Instance vPred_metr : metric vPred := _.
Global Instance vPred_cmetr : cmetric vPred := _.
Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : vPred) (r : res).
Local Obligation Tactic := intros; eauto with typeclass_instances.
Definition wpFP safe m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
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) (Some r · rf) w' @ S k),
(forall (HV : is_value e),
......@@ -46,7 +54,8 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
(exists σ' ei ei' K, e = K [[ ei ]] /\ prim_step (ei, σ) (ei', σ')) \/
(exists e' K, e = K [[ fork e' ]])).
Program Definition wpF safe m : (expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props :=
(* Define the function wp will be a fixed-point of *)
Program Definition wpF safe m : (expr -n> vPred -n> Props) -n> (expr -n> vPred -n> Props) :=
n[(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.
......@@ -55,13 +64,13 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
[| now eauto with arith | ..]; 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 (Some r1')) in HE'.
rewrite ->assoc, (comm (Some r1')) in HE'.
destruct (Some rd · Some r1') as [r2' |] eqn: HR;
[| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
exists w'' r2'; split; [assumption | split; [| assumption] ].
eapply uni_pred, Hφ; [| eexists; rewrite <- HR]; reflexivity.
- specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
rewrite assoc, (comm (Some r1')) in HE'.
rewrite ->assoc, (comm (Some r1')) in HE'.
destruct k as [| k]; [exists w'' r1'; simpl wsat; tauto |].
destruct (Some rd · Some r1') as [r2' |] eqn: HR;
[| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
......@@ -69,7 +78,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
eapply uni_pred, HWP; [| eexists; rewrite <- HR]; 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 (Some rfk)), (comm (Some rret1)) in HE'.
rewrite ->assoc, <- (assoc (Some rfk)), (comm (Some rret1)) in HE'.
destruct (Some rd · Some rret1) as [rret2 |] eqn: HR;
[| apply wsat_not_empty in HE'; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
exists w'' rfk rret2; repeat (split; try assumption); [].
......@@ -220,7 +229,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
+ auto.
Qed.
Definition wp safe m : expr -n> (value -n> Props) -n> Props :=
Definition wp safe m : expr -n> vPred -n> Props :=
fixp (wpF safe m) (umconst (umconst )).
Definition ht safe m P e φ := (P wp safe m e φ).
......@@ -234,53 +243,39 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
Local Open Scope lang_scope.
Local Open Scope list_scope.
Inductive stepn : nat -> cfg -> cfg -> Prop :=
| stepn_O ρ : stepn O ρ ρ
| stepn_S ρ1 ρ2 ρ3 n
(HS : step ρ1 ρ2)
(HSN : stepn n ρ2 ρ3) :
stepn (S n) ρ1 ρ3.
(* weakest-pre for a threadpool *)
Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list res -> Prop :=
| wp_emp : wptp safe m w n nil nil
| wp_cons e r tp rs
(WPE : wp safe m e (umconst ) w n r)
(WPTP : wptp safe m w n tp rs) :
wptp safe m w n (e :: tp) (r :: rs).
Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list res -> 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)
(WPTP : wptp safe m w n tp rs φs) :
wptp safe m w n (e :: tp) (r :: rs) (φ :: φs).
(* Trivial lemmas about split over append *)
Lemma wptp_app safe m w n tp1 tp2 rs1 rs2
(HW1 : wptp safe m w n tp1 rs1)
(HW2 : wptp safe m w n tp2 rs2) :
wptp safe m w n (tp1 ++ tp2) (rs1 ++ rs2).
Lemma wptp_app safe m w n tp1 tp2 rs1 rs2 φs1 φs2
(HW1 : wptp safe m w n tp1 rs1 φs1)
(HW2 : wptp safe m w n tp2 rs2 φs2) :
wptp safe m w n (tp1 ++ tp2) (rs1 ++ rs2) (φs1 ++ φs2).
Proof.
induction HW1; [| constructor]; now trivial.
Qed.
Lemma wptp_app_tp safe m w n t1 t2 rs
(HW : wptp safe m w n (t1 ++ t2) rs) :
exists rs1 rs2, rs1 ++ rs2 = rs /\ wptp safe m w n t1 rs1 /\ wptp safe m w n t2 rs2.
Proof.
revert rs HW; induction t1; intros; inversion HW; simpl in *; subst; clear HW.
- exists (@nil res) (@nil res); now auto using wptp.
- exists (@nil res); simpl; now eauto using wptp.
- apply IHt1 in WPTP; destruct WPTP as [rs1 [rs2 [EQrs [WP1 WP2] ] ] ]; clear IHt1.
exists (r :: rs1) rs2; simpl; subst; now auto using wptp.
Qed.
Lemma comp_list_app rs1 rs2 :
comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
Lemma wptp_app_tp safe m w n t1 t2 rs φs
(HW : wptp safe m w n (t1 ++ t2) rs φs) :
exists rs1 rs2 φs1 φs2, rs1 ++ rs2 = rs /\ φs1 ++ φs2 = φs /\ wptp safe m w n t1 rs1 φs1 /\ wptp safe m w n t2 rs2 φs2.
Proof.
induction rs1; simpl comp_list; [now rewrite pcm_op_unit by apply _ |].
now rewrite IHrs1, assoc.
revert rs φs HW; induction t1; intros; inversion HW; simpl in *; subst; clear HW.
- do 4 eexists. split; [|split; [|split; now econstructor] ]; reflexivity.
- do 4 eexists. split; [|split; [|split; now eauto using wptp] ]; reflexivity.
- apply IHt1 in WPTP; destruct WPTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [WP1 WP2] ] ] ] ] ] ]; clear IHt1.
exists (r :: rs1) rs2 (φ :: φs1) φs2; simpl; subst; now auto using wptp.
Qed.
(* Closure under future worlds and smaller steps *)
Lemma wptp_closure safe m (w1 w2 : Wld) n1 n2 tp rs
Lemma wptp_closure safe m (w1 w2 : Wld) n1 n2 tp rs φs
(HSW : w1 w2) (HLe : n2 <= n1)
(HW : wptp safe m w1 n1 tp rs) :
wptp safe m w2 n2 tp rs.
(HW : wptp safe m w1 n1 tp rs φs) :
wptp safe m w2 n2 tp rs φs.
Proof.
induction HW; constructor; [| assumption].
eapply uni_pred; [eassumption | reflexivity |].
......@@ -295,99 +290,88 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
unfold wp; apply fixp_eq.
Qed.
Lemma adequate_tp safe m n k e e' tp tp' σ σ' φ w r rs
(HSN : stepn n (e :: tp, σ) (e' :: tp', σ'))
(HV : is_value e')
(HWE : wp safe m e φ w (n + S k) r)
(HWTP : wptp safe m w (n + S k) tp rs)
(HE : wsat σ m (Some r · comp_list rs) w @ n + S k) :
exists w' r',
w w' /\ φ (exist _ e' HV) w' (S k) r' /\ wsat σ' m (Some r') w' @ S k.
Lemma preserve_wptp safe m n k tp tp' σ σ' w rs φs
(HSN : stepn n (tp, σ) (tp', σ'))
(HWTP : wptp safe m w (n + S k) tp rs φs)
(HE : wsat σ m (comp_list rs) w @ n + S k) :
exists w' rs' φs',
w w' /\ wptp safe m w' (S k) tp' rs' (φs ++ φs') /\ wsat σ' m (comp_list rs') w' @ S k.
Proof.
revert e tp σ w r rs HSN HWE HWTP HE; induction n using wf_nat_ind; rename H into HInd.
intros; inversion HSN; subst; clear HSN.
(* e is a value *)
{ rename e' into e; clear HInd HWTP; simpl plus in *; rewrite unfold_wp in HWE.
edestruct (HWE w k) as [HVal _];
[reflexivity | unfold lt; reflexivity | apply mask_emp_disjoint
| rewrite mask_emp_union; eassumption |].
specialize (HVal HV); destruct HVal as [w' [r' [HSW [Hφ HE'] ] ] ].
rewrite mask_emp_union in HE'; destruct (Some r' · comp_list rs) as [r'' |] eqn: EQr.
- exists w' r''; split; [assumption | split; [| assumption] ].
eapply uni_pred, Hφ; [reflexivity |].
rewrite ord_res_optRes; exists (comp_list rs); rewrite comm, EQr; reflexivity.
- exfalso; eapply wsat_not_empty, HE'. reflexivity.
revert tp σ w rs φs HSN HWTP HE. induction n; intros; inversion HSN; subst; clear HSN.
(* no step is taken *)
{ exists w rs (@nil vPred). split; [reflexivity|]. split.
- rewrite List.app_nil_r. assumption.
- assumption.
}
rename n0 into n; specialize (HInd n (le_n _)); inversion HS; subst; clear HS.
inversion HS; subst; clear HS.
(* atomic step *)
{ destruct t1 as [| ee t1]; inversion H0; subst; clear H0.
(* step in e *)
- simpl in HSN0; rewrite unfold_wp in HWE; edestruct (HWE w (n + S k)) as [_ [HS _] ];
[reflexivity | apply le_n | apply mask_emp_disjoint | rewrite mask_emp_union; eassumption |].
edestruct HS as [w' [r' [HSW [HWE' HE'] ] ] ]; [reflexivity | eassumption | clear HS HWE HE].
rewrite mask_emp_union in HE'; setoid_rewrite HSW; eapply HInd; try eassumption.
eapply wptp_closure, HWTP; [assumption | now auto with arith].
(* step in a spawned thread *)
- apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [EQrs [HWTP1 HWTP2] ] ] ].
inversion HWTP2; subst; clear HWTP2; rewrite unfold_wp in WPE.
edestruct (WPE w (n + S k) (Some r · comp_list (rs1 ++ rs0))) as [_ [HS _] ];
[reflexivity | apply le_n | 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 r0)), <- assoc; apply pcm_op_equiv; [reflexivity |].
now rewrite assoc, (comm (Some r0)), <- assoc.
+ edestruct HS as [w' [r0' [HSW [WPE' HE'] ] ] ];
[reflexivity | eassumption | clear WPE HS].
setoid_rewrite HSW; eapply HInd; try eassumption; [| |].
* rewrite <- HSW; eapply uni_pred, HWE; [now auto with arith | reflexivity].
* apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
{ inversion H0; subst; clear H0.
apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [HWTP1 HWTP2] ] ] ] ] ] ].
inversion HWTP2; subst; clear HWTP2; rewrite ->unfold_wp in WPE.
edestruct (WPE w (n + S k) (comp_list (rs1 ++ rs0))) as [_ [HS _] ];
[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.
+ edestruct HS as [w' [r' [HSW [WPE' HE'] ] ] ];
[reflexivity | eassumption | clear WPE HS].
setoid_rewrite HSW. eapply IHn; clear IHn.
* eassumption.
* apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
constructor; [eassumption | eapply wptp_closure, WPTP; [assumption | now auto with arith] ].
* eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
rewrite assoc, (comm (Some r0')), <- assoc; apply pcm_op_equiv; [reflexivity |].
rewrite !comp_list_app; simpl comp_list.
now rewrite assoc, (comm (comp_list rs1)), <- assoc.
* 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.
}
(* fork *)
destruct t1 as [| ee t1]; inversion H; subst; clear H.
(* fork from e *)
- simpl in HSN0; rewrite unfold_wp in HWE; edestruct (HWE w (n + S k)) as [_ [_ [HF _] ] ];
[reflexivity | apply le_n | apply mask_emp_disjoint | rewrite mask_emp_union; eassumption |].
specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [HSW [HWE' [HWFK HE'] ] ] ] ] ].
clear HWE HE; setoid_rewrite HSW; eapply HInd with (rs := rs ++ [rfk]); try eassumption; [|].
+ apply wptp_app; [| now auto using wptp].
eapply wptp_closure, HWTP; [assumption | now auto with arith].
+ eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
rewrite (comm (Some rfk)), <- assoc; apply pcm_op_equiv; [reflexivity |].
rewrite comp_list_app; simpl comp_list; rewrite comm.
now erewrite (comm _ 1), pcm_op_unit by apply _.
(* fork from a spawned thread *)
- apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [EQrs [HWTP1 HWTP2] ] ] ].
inversion HWTP2; subst; clear HWTP2; rewrite unfold_wp in WPE.
edestruct (WPE w (n + S k) (Some r · comp_list (rs1 ++ rs0))) as [_ [_ [HF _] ] ];
[reflexivity | apply le_n | apply mask_emp_disjoint
| eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |] |].
+ rewrite assoc, (comm (Some r0)), <- assoc; apply pcm_op_equiv; [reflexivity |].
rewrite !comp_list_app; simpl comp_list; now rewrite assoc, (comm (Some r0)), <- assoc.
+ specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [HSW [WPE' [WPS HE'] ] ] ] ] ]; clear WPE.
setoid_rewrite HSW; eapply HInd; try eassumption; [| |].
* rewrite <- HSW; eapply uni_pred, HWE; [now auto with arith | reflexivity].
* apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
constructor; [eassumption | apply wptp_app; [| now eauto using wptp] ].
eapply wptp_closure, WPTP; [assumption | now auto with arith].
* eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
rewrite (assoc _ (Some r)), (comm _ (Some r)), <- assoc.
apply pcm_op_equiv; [reflexivity |].
rewrite (comm (Some rfk)), <- assoc, comp_list_app; simpl comp_list.
rewrite assoc, (comm _ (Some rret)), <- assoc.
apply pcm_op_equiv; [reflexivity |].
rewrite (comm (Some rfk)), !comp_list_app; simpl comp_list.
rewrite assoc; apply pcm_op_equiv; [reflexivity |].
now erewrite comm, pcm_op_unit by apply _.
Qed.
Lemma unit_min r : pcm_unit _ r.
inversion H; subst; clear H.
apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [HWTP1 HWTP2] ] ] ] ] ] ].
inversion HWTP2; subst; clear HWTP2; rewrite ->unfold_wp in WPE.
edestruct (WPE w (n + S k) (comp_list (rs1 ++ rs0))) as [_ [_ [HF _] ] ];
[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.
+ 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|].
rewrite List.app_assoc. split; eassumption.
* rewrite -List.app_assoc. apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
constructor; [eassumption|].
apply wptp_app; [eapply wptp_closure, WPTP; [assumption | now auto with arith] |].
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 _ 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.
Qed.
Lemma adequate_tp safe m n k e e' tp tp' σ σ' φ w r rs φs
(HSN : stepn n (e :: tp, σ) (e' :: tp', σ'))
(HV : is_value e')
(HWE : wp safe m e φ w (n + S k) r)
(HWTP : wptp safe m w (n + S k) tp rs φs)
(HE : wsat σ m (Some r · comp_list rs) w @ n + S k) :
exists w' r',
w w' /\ φ (exist _ e' HV) w' (S k) r' /\ wsat σ' m (Some r') w' @ S k.
Proof.
exists r; now erewrite comm, pcm_op_unit by apply _.
edestruct preserve_wptp as [w' [rs' [φs' [HSW' [HSWTP' HSWS'] ] ] ] ]; first eassumption.
- econstructor; eassumption.
- assumption.
- inversion HSWTP'; subst; clear HSWTP'.
rewrite ->unfold_wp in WPE.
edestruct (WPE w' k) as [HVal _];
[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 rs0) as [r''' |] eqn: EQr.
+ exists w'' r'''. split; [etransitivity; eassumption|].
split; [|rewrite <-mask_emp_union; assumption].
eapply uni_pred, Hφ''; [reflexivity|].
rewrite ord_res_optRes. exists (comp_list rs0). rewrite ->comm, EQr. reflexivity.
+ exfalso. eapply wsat_not_empty, HE''. reflexivity.
Qed.
(** This is a (relatively) generic adequacy statement for all postconditions; one can
......@@ -408,7 +392,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
- simpl comp_list; now erewrite comm, pcm_op_unit by apply _.
Qed.
Program Definition cons_pred (φ : value -=> Prop): value -n> Props :=
Program Definition cons_pred (φ : value -=> Prop): vPred :=
n[(fun v => pcmconst (mkUPred (fun n r => φ v) _))].
Next Obligation.
firstorder.
......@@ -423,14 +407,15 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
Qed.
(* Adequacy as stated in the paper: for observations of the return value *)
Theorem adequacy_obs safe m e (φ : value -=> Prop) n e' tp σ σ'
Theorem adequacy_obs safe m e (φ : value -=> Prop) e' tp σ σ'
(HT : valid (ht safe m (ownS σ) e (cons_pred φ)))
(HSN : stepn n ([e], σ) (e' :: tp, σ'))
(HSN : steps ([e], σ) (e' :: tp, σ'))
(HV : is_value e') :
φ (exist _ e' HV).
Proof.
edestruct (adequacy_post _ _ _ _ _ _ 0 _ _ _ _ fdEmpty (ex_own _ σ, pcm_unit _) HT HSN) as [w [r [H_wle [H_phi _] ] ] ].
- exists (pcm_unit _); now rewrite pcm_op_unit by apply _.
destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN.
edestruct (adequacy_post _ _ _ _ _ _ 0 _ _ _ _ fdEmpty (ex_own _ σ, pcm_unit _) HT HSN') as [w [r [H_wle [H_phi _] ] ] ].
- 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].
......@@ -450,10 +435,10 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
Existing Instance LP_isval.
Implicit Types (P Q R : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (φ : value -n> Props) (r : res).
Implicit Types (P Q R : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (φ : vPred) (r : res).
(** Ret **)
Program Definition eqV v : value -n> Props :=
Program Definition eqV v : vPred :=
n[(fun v' : value => v === v')].
Next Obligation.
intros v1 v2 EQv w n r; simpl in *; split; congruence.
......@@ -507,17 +492,17 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
ht safe m P e φ all (plugV safe m φ φ' K) ht safe m P (K [[ e ]]) φ'.
Proof.
intros wz nz rz [He HK] w HSw n r HLe _ HP.
specialize (He _ HSw _ _ HLe (unit_min _) HP).
rewrite HSw, <- HLe in HK; clear wz nz HSw HLe HP.
specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
rewrite ->HSw, <- HLe in HK; clear wz nz HSw HLe HP.
revert e w r He HK; induction n using wf_nat_ind; intros; rename H into IH.
rewrite unfold_wp in He; rewrite unfold_wp.
rewrite ->unfold_wp in He; rewrite unfold_wp.
destruct (is_value_dec e) as [HVal | HNVal]; [clear IH |].
- intros w'; intros; edestruct He as [HV _]; try eassumption; [].
clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ HE] ] ] ].
(* Fold the goal back into a wp *)
setoid_rewrite HSw'.
assert (HT : wp safe m (K [[ e ]]) φ' w'' (S k) r');
[| rewrite unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
[| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
clear HE; specialize (HK (exist _ e HVal)).
do 30 red in HK; unfold proj1_sig in HK.
apply HK; [etransitivity; eassumption | apply HLt | apply unit_min | assumption].
......@@ -561,26 +546,26 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
Qed.
Next Obligation.
intros v1 v2 EQv; unfold vs.
rewrite EQv; reflexivity.
rewrite ->EQv; reflexivity.
Qed.
Lemma htCons P P' φ φ' safe m e :
vs m m P P' ht safe m P' e φ' all (vsLift m m φ' φ) ht safe m P e φ.
Proof.
intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
specialize (HP _ HSw _ _ HLe (unit_min _) Hp); rewrite unfold_wp.
specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
rewrite <- HLe, HSw in He, Hφ; clear wz nz HSw HLe Hp.
intros w'; intros; edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [now rewrite mask_union_idem |].
clear HP HE; rewrite HSw in He; specialize (He w'' HSw' _ r' HLt (unit_min _) Hp').
clear HP HE; rewrite ->HSw in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
setoid_rewrite HSw'.
assert (HT : wp safe m e φ w'' (S k) r');
[| rewrite unfold_wp in HT; eapply HT; [reflexivity | apply le_n | eassumption | eassumption] ].
unfold lt in HLt; rewrite HSw, HSw', <- HLt in Hφ; clear - He Hφ.
[| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | apply le_n | eassumption | eassumption] ].
unfold lt in HLt; rewrite ->HSw, HSw', <- HLt in Hφ; clear - He Hφ.
(* Second phase of the proof: got rid of the preconditions,
now induction takes care of the evaluation. *)
rename r' into r; rename w'' into w.
revert w r e He Hφ; generalize (S k) as n; clear k; induction n using wf_nat_ind.
rename H into IH; intros; rewrite unfold_wp; rewrite unfold_wp in He.
rename H into IH; intros; rewrite ->unfold_wp; rewrite ->unfold_wp in He.
intros w'; intros; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
split; [intros HVal; clear HS HF IH HS' | split; intros; [clear HV HF HS' | split; [intros; clear HV HS HS' | clear HV HS HF ] ] ].
- clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ' HE] ] ] ].
......@@ -592,11 +577,11 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
try eassumption; clear HS.
do 2 eexists; split; [eassumption | split; [| eassumption] ].
apply IH; try assumption; [].
unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
- clear HE He; edestruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ]; [eassumption |].
clear HF; do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
apply IH; try assumption; [].
unfold lt in HLt; rewrite Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
- assumption.
Qed.
......@@ -606,7 +591,7 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
vs m m' P P' ht safe m' P' e φ' all (vsLift m' m φ' φ) ht safe m P e φ.
Proof.
intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
specialize (HP _ HSw _ _ HLe (unit_min _) Hp); rewrite unfold_wp.
specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
split; [intros HV; contradiction (atomic_not_value e) |].
edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [|]; clear HP.
{ intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
......@@ -614,21 +599,21 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
}
split; [| split; [intros; subst; contradiction (fork_not_atomic K e') |] ].
- intros; rewrite <- HLe, HSw in He, Hφ; clear wz nz HSw HLe Hp.
clear HE; rewrite HSw0 in He; specialize (He w'' HSw' _ r' HLt (unit_min _) Hp').
unfold lt in HLt; rewrite HSw0, <- HLt in Hφ; clear w n HSw0 HLt Hp'.
rewrite unfold_wp in He; edestruct He as [_ [HS _] ];
[reflexivity | apply le_n | rewrite HSub; eassumption | eassumption |].
clear HE; rewrite ->HSw0 in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
unfold lt in HLt; rewrite ->HSw0, <- HLt in Hφ; clear w n HSw0 HLt Hp'.
rewrite ->unfold_wp in He; edestruct He as [_ [HS _] ];
[reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
edestruct HS as [w [r'' [HSw [He' HE] ] ] ]; try eassumption; clear He HS HE'.
destruct k as [| k]; [exists w' r'; split; [reflexivity | split; [apply wpO | exact I] ] |].
assert (HNV : ~ is_value ei)
by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
rewrite fill_empty in *; rename ei into e.
rewrite ->fill_empty in *; rename ei into e.
setoid_rewrite HSw'; setoid_rewrite HSw.
assert (HVal := atomic_step _ _ _ _ HAt HStep).
rewrite HSw', HSw in Hφ; clear - HE He' Hφ HSub HVal HD.
rewrite unfold_wp in He'; edestruct He' as [HV _];
[reflexivity | apply le_n | rewrite HSub; eassumption | eassumption |].
rewrite ->HSw', HSw in Hφ; clear - HE He' Hφ HSub HVal HD.
rewrite ->unfold_wp in He'; edestruct He' as [HV _];
[reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
clear HE He'; specialize (HV HVal); destruct HV as [w' [r [HSw [Hφ' HE] ] ] ].
eapply Hφ in Hφ'; [| assumption | apply Le.le_n_Sn | apply unit_min].
clear Hφ; edestruct Hφ' as [w'' [r' [HSw' [Hφ HE'] ] ] ];
......@@ -638,18 +623,18 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
}
clear Hφ' HE; exists w'' r'; split;
[etransitivity; eassumption | split; [| eassumption] ].
clear - Hφ; rewrite unfold_wp; intros w; intros; split; [intros HVal' | split; intros; [intros; exfalso|split; [intros |] ] ].
clear - Hφ; rewrite ->unfold_wp; intros w; intros; split; [intros HVal' | split; intros; [intros; exfalso|split; [intros |] ] ].
+ do 2 eexists; split; [reflexivity | split; [| eassumption] ].
unfold lt in HLt; rewrite HLt, <- HSw.
unfold lt in HLt; rewrite ->HLt, <- HSw.
eapply φ, Hφ; [| apply le_n]; simpl; reflexivity.
+ eapply values_stuck; [.. | repeat eexists]; eassumption.
+ clear - HDec HVal; subst; assert (HT := fill_value _ _ HVal); subst.
rewrite fill_empty in HVal; now apply fork_not_value in