Commit aafa826d authored by Ralf Jung's avatar Ralf Jung

seal wp and pvs

parent c59e1f85
...@@ -14,7 +14,6 @@ Implicit Types P Q : iProp Λ Σ. ...@@ -14,7 +14,6 @@ Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ iProp Λ Σ. Implicit Types Φ : val Λ iProp Λ Σ.
Implicit Types Φs : list (val Λ iProp Λ Σ). Implicit Types Φs : list (val Λ iProp Λ Σ).
Implicit Types m : iGst Λ Σ. Implicit Types m : iGst Λ Σ.
Transparent uPred_holds.
Notation wptp n := (Forall3 (λ e Φ r, uPred_holds (wp e Φ) n r)). Notation wptp n := (Forall3 (λ e Φ r, uPred_holds (wp e Φ) n r)).
Lemma wptp_le Φs es rs n n' : Lemma wptp_le Φs es rs n n' :
...@@ -32,6 +31,7 @@ Proof. ...@@ -32,6 +31,7 @@ Proof.
{ by intros; exists rs, []; rewrite right_id_L. } { by intros; exists rs, []; rewrite right_id_L. }
intros (Φs1&?&rs1&?&->&->&?& intros (Φs1&?&rs1&?&->&->&?&
(Φ&Φs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?. (Φ&Φs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?.
rewrite wp_eq in Hwp.
destruct (wp_step_inv Φ e1 (k + n) (S (k + n)) σ1 r destruct (wp_step_inv Φ e1 (k + n) (S (k + n)) σ1 r
(big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck. (big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck.
{ by rewrite right_id_L -big_op_cons Permutation_middle. } { by rewrite right_id_L -big_op_cons Permutation_middle. }
...@@ -41,7 +41,8 @@ Proof. ...@@ -41,7 +41,8 @@ Proof.
- destruct (IH (Φs1 ++ Φ :: Φs2 ++ [λ _, True%I]) - destruct (IH (Φs1 ++ Φ :: Φs2 ++ [λ _, True%I])
(rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Φs'&?&?). (rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Φs'&?&?).
{ apply Forall3_app, Forall3_cons, { apply Forall3_app, Forall3_cons,
Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le. } Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le; [|];
rewrite wp_eq; eauto. }
{ by rewrite -Permutation_middle /= (assoc (++)) { by rewrite -Permutation_middle /= (assoc (++))
(comm (++)) /= assoc big_op_app. } (comm (++)) /= assoc big_op_app. }
exists rs', ([λ _, True%I] ++ Φs'); split; auto. exists rs', ([λ _, True%I] ++ Φs'); split; auto.
...@@ -49,6 +50,7 @@ Proof. ...@@ -49,6 +50,7 @@ Proof.
- apply (IH (Φs1 ++ Φ :: Φs2) (rs1 ++ r2 r2' :: rs2)). - apply (IH (Φs1 ++ Φ :: Φs2) (rs1 ++ r2 r2' :: rs2)).
{ rewrite /option_list right_id_L. { rewrite /option_list right_id_L.
apply Forall3_app, Forall3_cons; eauto using wptp_le. apply Forall3_app, Forall3_cons; eauto using wptp_le.
rewrite wp_eq.
apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. } apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. }
by rewrite -Permutation_middle /= big_op_app. by rewrite -Permutation_middle /= big_op_app.
Qed. Qed.
...@@ -90,7 +92,8 @@ Proof. ...@@ -90,7 +92,8 @@ Proof.
as (rs2&Qs&Hwptp&?); auto. as (rs2&Qs&Hwptp&?); auto.
{ by rewrite -(ht_mask_weaken E ). } { by rewrite -(ht_mask_weaken E ). }
inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst. inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
move: Hwp. uPred.unseal=> /wp_value_inv Hwp. move: Hwp. rewrite wp_eq. uPred.unseal=> /wp_value_inv Hwp.
rewrite pvs_eq in Hwp.
destruct (Hwp (big_op rs) 2 σ2) as [r' []]; rewrite ?right_id_L; auto. destruct (Hwp (big_op rs) 2 σ2) as [r' []]; rewrite ?right_id_L; auto.
Qed. Qed.
Lemma ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 : Lemma ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
...@@ -106,6 +109,7 @@ Proof. ...@@ -106,6 +109,7 @@ Proof.
(Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto. (Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto.
destruct (wp_step_inv Φ' e2 1 2 σ2 r2 (big_op (delete i rs2))); destruct (wp_step_inv Φ' e2 1 2 σ2 r2 (big_op (delete i rs2)));
rewrite ?right_id_L ?big_op_delete; auto. rewrite ?right_id_L ?big_op_delete; auto.
by rewrite -wp_eq.
Qed. Qed.
Theorem ht_adequacy_safe E Φ e1 t2 σ1 m σ2 : Theorem ht_adequacy_safe E Φ e1 t2 σ1 m σ2 :
m m
......
...@@ -27,7 +27,8 @@ Lemma wp_lift_step E1 E2 ...@@ -27,7 +27,8 @@ Lemma wp_lift_step E1 E2
( φ e2 σ2 ef ownP σ2) - |={E1,E2}=> || e2 @ E2 {{ Φ }} wp_fork ef) ( φ e2 σ2 ef ownP σ2) - |={E1,E2}=> || e2 @ E2 {{ Φ }} wp_fork ef)
|| e1 @ E2 {{ Φ }}. || e1 @ E2 {{ Φ }}.
Proof. Proof.
intros ? He Hsafe Hstep. uPred.unseal; split=> n r ? Hvs; constructor; auto. intros ? He Hsafe Hstep. rewrite pvs_eq wp_eq.
uPred.unseal; split=> n r ? Hvs; constructor; auto.
intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1') intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'. as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
destruct (wsat_update_pst k (E1 Ef) σ1 σ1' r1 (r2 rf)) as [-> Hws']. destruct (wsat_update_pst k (E1 Ef) σ1 σ1' r1 (r2 rf)) as [-> Hws'].
...@@ -47,7 +48,8 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 : ...@@ -47,7 +48,8 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef) ( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef σ1 = σ2 φ e2 ef)
( e2 ef, φ e2 ef || e2 @ E {{ Φ }} wp_fork ef) || e1 @ E {{ Φ }}. ( e2 ef, φ e2 ef || e2 @ E {{ Φ }} wp_fork ef) || e1 @ E {{ Φ }}.
Proof. Proof.
intros He Hsafe Hstep; uPred.unseal; split=> n r ? Hwp; constructor; auto. intros He Hsafe Hstep; rewrite wp_eq; uPred.unseal.
split=> n r ? Hwp; constructor; auto.
intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia. intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst. intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto. destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
......
...@@ -9,8 +9,7 @@ Local Hint Extern 10 (✓{_} _) => ...@@ -9,8 +9,7 @@ Local Hint Extern 10 (✓{_} _) =>
| H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
end; solve_validN. end; solve_validN.
(* TODO: Consider sealing this, like all the definitions in upred.v. *) Program Definition pvs_def {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
{| uPred_holds n r1 := rf k Ef σ, {| uPred_holds n r1 := rf k Ef σ,
0 < k n (E1 E2) Ef = 0 < k n (E1 E2) Ef =
wsat k (E1 Ef) σ (r1 rf) wsat k (E1 Ef) σ (r1 rf)
...@@ -25,7 +24,12 @@ Next Obligation. ...@@ -25,7 +24,12 @@ Next Obligation.
exists (r' r3); rewrite -assoc; split; last done. exists (r' r3); rewrite -assoc; split; last done.
apply uPred_weaken with k r'; eauto using cmra_included_l. apply uPred_weaken with k r'; eauto using cmra_included_l.
Qed. Qed.
Arguments pvs {_ _} _ _ _%I : simpl never.
Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
Definition pvs := proj1_sig pvs_aux.
Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
Arguments pvs {_ _} _ _ _%I.
Instance: Params (@pvs) 4. Instance: Params (@pvs) 4.
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I) Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
...@@ -43,6 +47,7 @@ Transparent uPred_holds. ...@@ -43,6 +47,7 @@ Transparent uPred_holds.
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2). Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Proof. Proof.
rewrite pvs_eq.
intros P Q HPQ; split=> n' r1 ??; simpl; split; intros HP rf k Ef σ ???; intros P Q HPQ; split=> n' r1 ??; simpl; split; intros HP rf k Ef σ ???;
destruct (HP rf k Ef σ) as (r2&?&?); auto; destruct (HP rf k Ef σ) as (r2&?&?); auto;
exists r2; split_and?; auto; apply HPQ; eauto. exists r2; split_and?; auto; apply HPQ; eauto.
...@@ -52,18 +57,18 @@ Proof. apply ne_proper, _. Qed. ...@@ -52,18 +57,18 @@ Proof. apply ne_proper, _. Qed.
Lemma pvs_intro E P : P |={E}=> P. Lemma pvs_intro E P : P |={E}=> P.
Proof. Proof.
split=> n r ? HP rf k Ef σ ???; exists r; split; last done. rewrite pvs_eq. split=> n r ? HP rf k Ef σ ???; exists r; split; last done.
apply uPred_weaken with n r; eauto. apply uPred_weaken with n r; eauto.
Qed. Qed.
Lemma pvs_mono E1 E2 P Q : P Q (|={E1,E2}=> P) (|={E1,E2}=> Q). Lemma pvs_mono E1 E2 P Q : P Q (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. Proof.
intros HPQ; split=> n r ? HP rf k Ef σ ???. rewrite pvs_eq. intros HPQ; split=> n r ? HP rf k Ef σ ???.
destruct (HP rf k Ef σ) as (r2&?&?); eauto. destruct (HP rf k Ef σ) as (r2&?&?); eauto.
exists r2; eauto using uPred_in_entails. exists r2; eauto using uPred_in_entails.
Qed. Qed.
Lemma pvs_timeless E P : TimelessP P ( P) (|={E}=> P). Lemma pvs_timeless E P : TimelessP P ( P) (|={E}=> P).
Proof. Proof.
rewrite uPred.timelessP_spec=> HP. rewrite pvs_eq uPred.timelessP_spec=> HP.
uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia. uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
exists r; split; last done. exists r; split; last done.
apply HP, uPred_weaken with n r; eauto using cmra_validN_le. apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
...@@ -71,19 +76,19 @@ Qed. ...@@ -71,19 +76,19 @@ Qed.
Lemma pvs_trans E1 E2 E3 P : Lemma pvs_trans E1 E2 E3 P :
E2 E1 E3 (|={E1,E2}=> |={E2,E3}=> P) (|={E1,E3}=> P). E2 E1 E3 (|={E1,E2}=> |={E2,E3}=> P) (|={E1,E3}=> P).
Proof. Proof.
intros ?; split=> n r1 ? HP1 rf k Ef σ ???. rewrite pvs_eq. intros ?; split=> n r1 ? HP1 rf k Ef σ ???.
destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto. destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
Qed. Qed.
Lemma pvs_mask_frame E1 E2 Ef P : Lemma pvs_mask_frame E1 E2 Ef P :
Ef (E1 E2) = (|={E1,E2}=> P) (|={E1 Ef,E2 Ef}=> P). Ef (E1 E2) = (|={E1,E2}=> P) (|={E1 Ef,E2 Ef}=> P).
Proof. Proof.
intros ?; split=> n r ? HP rf k Ef' σ ???. rewrite pvs_eq. intros ?; split=> n r ? HP rf k Ef' σ ???.
destruct (HP rf k (EfEf') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto. destruct (HP rf k (EfEf') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
by exists r'; rewrite -(assoc_L _). by exists r'; rewrite -(assoc_L _).
Qed. Qed.
Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) Q) (|={E1,E2}=> P Q). Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) Q) (|={E1,E2}=> P Q).
Proof. Proof.
uPred.unseal; split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???. rewrite pvs_eq. uPred.unseal; split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
destruct (HP (r2 rf) k Ef σ) as (r'&?&?); eauto. destruct (HP (r2 rf) k Ef σ) as (r'&?&?); eauto.
{ by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. } { by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
exists (r' r2); split; last by rewrite -assoc. exists (r' r2); split; last by rewrite -assoc.
...@@ -91,7 +96,7 @@ Proof. ...@@ -91,7 +96,7 @@ Proof.
Qed. Qed.
Lemma pvs_openI i P : ownI i P (|={{[i]},}=> P). Lemma pvs_openI i P : ownI i P (|={{[i]},}=> P).
Proof. Proof.
uPred.unseal; split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia. rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia.
apply ownI_spec in Hinv; last auto. apply ownI_spec in Hinv; last auto.
destruct (wsat_open k Ef σ (r rf) i P) as (rP&?&?); auto. destruct (wsat_open k Ef σ (r rf) i P) as (rP&?&?); auto.
{ rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. } { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
...@@ -100,7 +105,7 @@ Proof. ...@@ -100,7 +105,7 @@ Proof.
Qed. Qed.
Lemma pvs_closeI i P : (ownI i P P) (|={,{[i]}}=> True). Lemma pvs_closeI i P : (ownI i P P) (|={,{[i]}}=> True).
Proof. Proof.
uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia. rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
exists ; split; [done|]. exists ; split; [done|].
rewrite left_id; apply wsat_close with P r. rewrite left_id; apply wsat_close with P r.
- apply ownI_spec, uPred_weaken with (S n) r; auto. - apply ownI_spec, uPred_weaken with (S n) r; auto.
...@@ -111,7 +116,7 @@ Qed. ...@@ -111,7 +116,7 @@ Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ Prop) : Lemma pvs_ownG_updateP E m (P : iGst Λ Σ Prop) :
m ~~>: P ownG m (|={E}=> m', P m' ownG m'). m ~~>: P ownG m (|={E}=> m', P m' ownG m').
Proof. Proof.
intros Hup%option_updateP'. rewrite pvs_eq. intros Hup%option_updateP'.
uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia. uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
destruct (wsat_update_gst k (E Ef) σ r rf (Some m) P) as (m'&?&?); eauto. destruct (wsat_update_gst k (E Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
{ apply cmra_includedN_le with (S n); auto. } { apply cmra_includedN_le with (S n); auto. }
...@@ -121,7 +126,7 @@ Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)} ...@@ -121,7 +126,7 @@ Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
E (P : iGst Λ Σ Prop) : E (P : iGst Λ Σ Prop) :
~~>: P True (|={E}=> m', P m' ownG m'). ~~>: P True (|={E}=> m', P m' ownG m').
Proof. Proof.
intros Hup; uPred.unseal; split=> -[|n] r ? _ rf [|k] Ef σ ???; try lia. rewrite pvs_eq. intros Hup; uPred.unseal; split=> -[|n] r ? _ rf [|k] Ef σ ???; try lia.
destruct (wsat_update_gst k (E Ef) σ r rf P) as (m'&?&?); eauto. destruct (wsat_update_gst k (E Ef) σ r rf P) as (m'&?&?); eauto.
{ apply cmra_empty_leastN. } { apply cmra_empty_leastN. }
{ apply cmra_updateP_compose_l with (Some ), option_updateP with P; { apply cmra_updateP_compose_l with (Some ), option_updateP with P;
...@@ -130,7 +135,7 @@ Proof. ...@@ -130,7 +135,7 @@ Proof.
Qed. Qed.
Lemma pvs_allocI E P : ¬set_finite E P (|={E}=> i, (i E) ownI i P). Lemma pvs_allocI E P : ¬set_finite E P (|={E}=> i, (i E) ownI i P).
Proof. Proof.
intros ?; rewrite /ownI; uPred.unseal. rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia. split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto. destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
{ apply uPred_weaken with n r; eauto. } { apply uPred_weaken with n r; eauto. }
......
...@@ -30,8 +30,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset) ...@@ -30,8 +30,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
wp_go (E Ef) (wp_pre E Φ) wp_go (E Ef) (wp_pre E Φ)
(wp_pre (λ _, True%I)) k rf e1 σ1) (wp_pre (λ _, True%I)) k rf e1 σ1)
wp_pre E Φ e1 n r1. wp_pre E Φ e1 n r1.
(* TODO: Consider sealing this, like all the definitions in upred.v. *) Program Definition wp_def {Λ Σ} (E : coPset) (e : expr Λ)
Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
(Φ : val Λ iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}. (Φ : val Λ iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
Next Obligation. Next Obligation.
intros Λ Σ E e Φ n r1 r2 Hwp Hr. intros Λ Σ E e Φ n r1 r2 Hwp Hr.
...@@ -50,6 +49,12 @@ Next Obligation. ...@@ -50,6 +49,12 @@ Next Obligation.
exists r2, (r2' rf'); split_and?; eauto 10 using (IH k), cmra_included_l. exists r2, (r2' rf'); split_and?; eauto 10 using (IH k), cmra_included_l.
by rewrite -!assoc (assoc _ r2). by rewrite -!assoc (assoc _ r2).
Qed. Qed.
(* Perform sealing. *)
Definition wp_aux : { x | x = @wp_def }. by eexists. Qed.
Definition wp := proj1_sig wp_aux.
Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.
Arguments wp {_ _} _ _ _.
Instance: Params (@wp) 4. Instance: Params (@wp) 4.
Notation "|| e @ E {{ Φ } }" := (wp E e Φ) Notation "|| e @ E {{ Φ } }" := (wp E e Φ)
...@@ -72,8 +77,8 @@ Global Instance wp_ne E e n : ...@@ -72,8 +77,8 @@ Global Instance wp_ne E e n :
Proof. Proof.
cut ( Φ Ψ, ( v, Φ v {n} Ψ v) cut ( Φ Ψ, ( v, Φ v {n} Ψ v)
n' r, n' n {n'} r wp E e Φ n' r wp E e Ψ n' r). n' r, n' n {n'} r wp E e Φ n' r wp E e Ψ n' r).
{ intros help Φ Ψ HΦΨ. by do 2 split; apply help. } { rewrite wp_eq. intros help Φ Ψ HΦΨ. by do 2 split; apply help. }
intros Φ Ψ HΦΨ n' r; revert e r. rewrite wp_eq. intros Φ Ψ HΦΨ n' r; revert e r.
induction n' as [n' IH] using lt_wf_ind=> e r. induction n' as [n' IH] using lt_wf_ind=> e r.
destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo]. destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo].
{ constructor. by eapply pvs_ne, HpvsQ; eauto. } { constructor. by eapply pvs_ne, HpvsQ; eauto. }
...@@ -91,7 +96,7 @@ Qed. ...@@ -91,7 +96,7 @@ Qed.
Lemma wp_mask_frame_mono E1 E2 e Φ Ψ : Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
E1 E2 ( v, Φ v Ψ v) || e @ E1 {{ Φ }} || e @ E2 {{ Ψ }}. E1 E2 ( v, Φ v Ψ v) || e @ E1 {{ Φ }} || e @ E2 {{ Ψ }}.
Proof. Proof.
intros HE HΦ; split=> n r. rewrite wp_eq. intros HE HΦ; split=> n r.
revert e r; induction n as [n IH] using lt_wf_ind=> e r. revert e r; induction n as [n IH] using lt_wf_ind=> e r.
destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo]. destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
{ constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. } { constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
...@@ -105,31 +110,34 @@ Proof. ...@@ -105,31 +110,34 @@ Proof.
Qed. Qed.
Lemma wp_value_inv E Φ v n r : Lemma wp_value_inv E Φ v n r :
|| of_val v @ E {{ Φ }}%I n r (|={E}=> Φ v)%I n r. wp_def E (of_val v) Φ n r pvs E E (Φ v) n r.
Proof. Proof.
by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq. by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq.
Qed. Qed.
Lemma wp_step_inv E Ef Φ e k n σ r rf : Lemma wp_step_inv E Ef Φ e k n σ r rf :
to_val e = None 0 < k < n E Ef = to_val e = None 0 < k < n E Ef =
|| e @ E {{ Φ }}%I n r wsat (S k) (E Ef) σ (r rf) wp_def E e Φ n r wsat (S k) (E Ef) σ (r rf)
wp_go (E Ef) (λ e, wp E e Φ) (λ e, wp e (λ _, True%I)) k rf e σ. wp_go (E Ef) (λ e, wp_def E e Φ) (λ e, wp_def e (λ _, True%I)) k rf e σ.
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed. Proof.
intros He; destruct 3; [by rewrite ?to_of_val in He|eauto].
Qed.
Lemma wp_value' E Φ v : Φ v || of_val v @ E {{ Φ }}. Lemma wp_value' E Φ v : Φ v || of_val v @ E {{ Φ }}.
Proof. split=> n r; constructor; by apply pvs_intro. Qed. Proof. rewrite wp_eq. split=> n r; constructor; by apply pvs_intro. Qed.
Lemma pvs_wp E e Φ : (|={E}=> || e @ E {{ Φ }}) || e @ E {{ Φ }}. Lemma pvs_wp E e Φ : (|={E}=> || e @ E {{ Φ }}) || e @ E {{ Φ }}.
Proof. Proof.
split=> n r ? Hvs. rewrite wp_eq. split=> n r ? Hvs.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|]. destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
{ constructor; eapply pvs_trans', pvs_mono, Hvs; eauto. { constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
split=> ???; apply wp_value_inv. } split=> ???; apply wp_value_inv. }
constructor; [done|]=> rf k Ef σ1 ???. constructor; [done|]=> rf k Ef σ1 ???.
destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto. rewrite pvs_eq in Hvs. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
eapply wp_step_inv with (S k) r'; eauto. eapply wp_step_inv with (S k) r'; eauto.
Qed. Qed.
Lemma wp_pvs E e Φ : || e @ E {{ λ v, |={E}=> Φ v }} || e @ E {{ Φ }}. Lemma wp_pvs E e Φ : || e @ E {{ λ v, |={E}=> Φ v }} || e @ E {{ Φ }}.
Proof. Proof.
split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ. rewrite wp_eq. split=> n r; revert e r;
induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|]. destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
{ constructor; apply pvs_trans', (wp_value_inv _ (pvs E E Φ)); auto. } { constructor; apply pvs_trans', (wp_value_inv _ (pvs E E Φ)); auto. }
constructor; [done|]=> rf k Ef σ1 ???. constructor; [done|]=> rf k Ef σ1 ???.
...@@ -142,16 +150,16 @@ Lemma wp_atomic E1 E2 e Φ : ...@@ -142,16 +150,16 @@ Lemma wp_atomic E1 E2 e Φ :
E2 E1 atomic e E2 E1 atomic e
(|={E1,E2}=> || e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) || e @ E1 {{ Φ }}. (|={E1,E2}=> || e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) || e @ E1 {{ Φ }}.
Proof. Proof.
intros ? He; split=> n r ? Hvs; constructor; eauto using atomic_not_val. rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs; constructor.
intros rf k Ef σ1 ???. eauto using atomic_not_val. intros rf k Ef σ1 ???.
destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
destruct (wp_step_inv E2 Ef (pvs E2 E1 Φ) e k (S k) σ1 r' rf) destruct (wp_step_inv E2 Ef (pvs_def E2 E1 Φ) e k (S k) σ1 r' rf)
as [Hsafe Hstep]; auto using atomic_not_val. as [Hsafe Hstep]; auto using atomic_not_val; [].
split; [done|]=> e2 σ2 ef ?. split; [done|]=> e2 σ2 ef ?.
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto. destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto.
destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo]; destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo];
[|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver]. [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
apply pvs_trans in Hvs'; auto. rewrite -pvs_eq in Hvs'. apply pvs_trans in Hvs';auto. rewrite pvs_eq in Hvs'.
destruct (Hvs' (r2' rf) k Ef σ2) as (r3&[]); rewrite ?assoc; auto. destruct (Hvs' (r2' rf) k Ef σ2) as (r3&[]); rewrite ?assoc; auto.
exists r3, r2'; split_and?; last done. exists r3, r2'; split_and?; last done.
- by rewrite -assoc. - by rewrite -assoc.
...@@ -159,8 +167,8 @@ Proof. ...@@ -159,8 +167,8 @@ Proof.
Qed. Qed.
Lemma wp_frame_r E e Φ R : (|| e @ E {{ Φ }} R) || e @ E {{ λ v, Φ v R }}. Lemma wp_frame_r E e Φ R : (|| e @ E {{ Φ }} R) || e @ E {{ λ v, Φ v R }}.
Proof. Proof.
uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid. rewrite wp_eq. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
rewrite Hr; clear Hr; revert e r Hwp. revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp.
induction n as [n IH] using lt_wf_ind; intros e r1. induction n as [n IH] using lt_wf_ind; intros e r1.
destruct 1 as [|n r e ? Hgo]=>?. destruct 1 as [|n r e ? Hgo]=>?.
{ constructor. rewrite -uPred_sep_eq; apply pvs_frame_r; auto. { constructor. rewrite -uPred_sep_eq; apply pvs_frame_r; auto.
...@@ -178,7 +186,7 @@ Qed. ...@@ -178,7 +186,7 @@ Qed.
Lemma wp_frame_later_r E e Φ R : Lemma wp_frame_later_r E e Φ R :
to_val e = None (|| e @ E {{ Φ }} R) || e @ E {{ λ v, Φ v R }}. to_val e = None (|| e @ E {{ Φ }} R) || e @ E {{ λ v, Φ v R }}.
Proof. Proof.
intros He; uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?). rewrite wp_eq. intros He; uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
revert Hvalid; rewrite Hr; clear Hr. revert Hvalid; rewrite Hr; clear Hr.
destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|]. destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega. constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega.
...@@ -187,15 +195,17 @@ Proof. ...@@ -187,15 +195,17 @@ Proof.
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 rR), r2'; split_and?; auto. exists (r2 rR), r2'; split_and?; auto.
- by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR). - by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
- rewrite -uPred_sep_eq. - rewrite -uPred_sep_eq. move:(wp_frame_r). rewrite wp_eq=>Hframe.
apply wp_frame_r; [auto|uPred.unseal; exists r2, rR; split_and?; auto]. apply Hframe; [auto|uPred.unseal; exists r2, rR; split_and?; auto].
eapply uPred_weaken with n rR; eauto. eapply uPred_weaken with n rR; eauto.
Qed. Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ : Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
|| e @ E {{ λ v, || K (of_val v) @ E {{ Φ }} }} || K e @ E {{ Φ }}. || e @ E {{ λ v, || K (of_val v) @ E {{ Φ }} }} || K e @ E {{ Φ }}.
Proof. Proof.
split=> n r; revert e r;