Library iris.program_logic.weakestpre
From iris.program_logic Require Export pviewshifts pstepshifts.
From iris.program_logic Require Import wsat.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 100 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 100 (_ ∉_) ⇒ set_solver.
Local Hint Extern 100 (@subseteq coPset _ _ _) ⇒ set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
Record wp_go {Λ Σ} (E : coPset) (Φ Φfork : expr Λ → nat → iRes Λ Σ → iRes Λ Σ → Prop)
(k : nat) (σ1 : state Λ) (rf rfl rob: iRes Λ Σ) (e1 : expr Λ) := {
wf_safe : reducible e1 σ1;
wp_step e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef →
∃ r2 r2' rob2 rob2',
wsat k E σ2 (r2 ⋅ r2' ⋅ rf) (rob2 ⋅ rob2' ⋅ rfl) ∧
Φ e2 k r2 rob2 ∧
(∀ e', ef = Some e' → Φfork e' k r2' rob2') ∧
(ef = None → rob2' ≡{k}≡ ∅) ∧
rob ⤳_(k) rob2 ⋅ rob2'
}.
CoInductive wp_pre {Λ Σ} (E : coPset)
(Φ : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → iRes Λ Σ → Prop :=
| wp_pre_value n r rob v : (|={E}=> Φ v)%I n r rob → wp_pre E Φ (of_val v) n r rob
| wp_pre_step n r1 rob1 e1 :
to_val e1 = None →
(∀ k Ef σ1 rf rfl,
0 < k < n → E ⊥ Ef →
wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) (rob1 ⋅ rfl) →
wp_go (E ∪ Ef) (wp_pre E Φ)
(wp_pre ⊤ (λ _, uPred_stopped%I)) k σ1 rf rfl rob1 e1) →
wp_pre E Φ e1 n r1 rob1.
Program Definition wp_def {Λ Σ} (E : coPset) (e : expr Λ)
(Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
Next Obligation.
intros Λ Σ E e Φ n1 n2 r1 r2 rob; revert Φ E e n2 r1 r2 rob.
induction n1 as [n1 IH] using lt_wf_ind; intros Φ E e n2 r1 r1' rob.
destruct 1 as [|n1 r1 rob1 e1 ? Hgo].
- constructor; eauto using uPred_mono.
- intros [rf' Hr Hrl]. constructor; [done|intros k Ef σ1 rf rfl ???].
destruct (Hgo k Ef σ1 (rf' ⋅ rf) rfl) as [Hsafe Hstep];
rewrite ?assoc -?(dist_le _ _ _ _ Hr); auto;
first rewrite ?(dist_le _ _ _ _ Hrl); auto;
constructor; [done|].
intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&?&?&?&?&?); auto.
∃ r2, (r2' ⋅ rf'), rob2, rob2'; split_and?;
eauto 10 using (IH k), cmra_included_l, cmra_includedN_l.
by rewrite -assoc -assoc (assoc _ r2).
rewrite -(dist_le _ _ _ _ Hrl); eauto.
Qed.
Next Obligation. destruct 1; constructor; eauto using uPred_closed. Qed.
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.
Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
(at level 20, e, Φ at level 200,
format "'WP' e @ E {{ Φ } }") : uPred_scope.
Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
(at level 20, e, Φ at level 200,
format "'WP' e {{ Φ } }") : uPred_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp E e (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e @ E {{ v , Q } }") : uPred_scope.
Notation "'WP' e {{ v , Q } }" := (wp ⊤ e (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e {{ v , Q } }") : uPred_scope.
Section wp.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Global Instance wp_ne E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
Proof.
cut (∀ Φ Ψ, (∀ v, Φ v ≡{n}≡ Ψ v) →
∀ n' r rob, n' ≤ n → ✓{n'} r → ✓{n'} rob → wp E e Φ n' r rob → wp E e Ψ n' r rob).
{ rewrite wp_eq. intros help Φ Ψ HΦΨ. by do 2 split; apply help. }
rewrite wp_eq. intros Φ Ψ HΦΨ n' r rob; revert e r rob.
induction n' as [n' IH] using lt_wf_ind⇒ e r rob.
destruct 4 as [n' r rob v HpvsQ|n' r rob e1 ? Hgo].
{ constructor. by eapply pvs_ne, HpvsQ; eauto. }
constructor; [done|]=> k Ef σ1 rf rfl ???.
destruct (Hgo k Ef σ1 rf rfl) as [Hsafe Hstep]; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&?&?&?&?&?); auto.
∃ r2, r2', rob2, rob2'; split_and?; [|eapply IH| | |]; eauto.
Qed.
Global Instance wp_proper E e :
Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e).
Proof.
by intros Φ Φ' ?; apply equiv_dist⇒n; apply wp_ne⇒v; apply equiv_dist.
Qed.
Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
E1 ⊆ E2 → (∀ v, Φ v ⊢ Ψ v) → WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Ψ }}.
Proof.
rewrite wp_eq. intros HE HΦ; split⇒ n r rob.
revert e r rob; induction n as [n IH] using lt_wf_ind⇒ e r rob.
destruct 3 as [n' r rob v HpvsQ|n' r rob e1 ? Hgo].
{ constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
constructor; [done|]=> k Ef σ1 rf rfl ???.
assert (E2 ∪ Ef = E1 ∪ (E2 ∖ E1 ∪ Ef)) as HE'.
{ by rewrite assoc_L -union_difference_L. }
destruct (Hgo k ((E2 ∖ E1) ∪ Ef) σ1 rf rfl) as [Hsafe Hstep]; rewrite -?HE'; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&?&?&?&?&?); auto.
∃ r2, r2', rob2, rob2'; split_and?; [rewrite HE'|eapply IH| | |]; eauto.
Qed.
Lemma wp_zero E e Φ r rob : wp_def E e Φ 0 r rob.
Proof.
case EQ: (to_val e).
- rewrite -(of_to_val _ _ EQ). constructor. rewrite pvs_eq.
exact: pvs_zero.
- constructor; first done. intros ??????. exfalso. omega.
Qed.
Lemma wp_value_inv E Φ v n r rob: wp_def E (of_val v) Φ n r rob → pvs E E (Φ v) n r rob.
Proof.
by inversion 1 as [|???? He]; [|rewrite ?to_of_val in He]; simplify_eq.
Qed.
Lemma wp_step_inv E Ef Φ e k n σ r rob rf rfl :
to_val e = None → 0 < k < n → E ⊥ Ef →
wp_def E e Φ n r rob → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) (rob ⋅ rfl) →
wp_go (E ∪ Ef) (λ e, wp_def E e Φ) (λ e, wp_def ⊤ e (λ _, uPred_stopped%I)) k σ rf rfl rob e.
Proof.
intros He; destruct 3; [by rewrite ?to_of_val in He|eauto using wsat_weaken].
Qed.
Lemma wp_value' E Φ v : Φ v ⊢ WP of_val v @ E {{ Φ }}.
Proof. rewrite wp_eq. split⇒ n r; constructor; by apply pvs_intro. Qed.
Lemma pvs_wp E e Φ : (|={E}=> WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split⇒ n r rob ? ? Hvs.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
{ constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
split⇒ ?????; apply wp_value_inv. }
constructor; [done|]=> k Ef σ1 rf rfl ???.
rewrite pvs_eq in Hvs. destruct (Hvs (S k) Ef σ1 rf rfl) as (r'&Hwp&Hwsat); auto.
eapply wp_step_inv with (S k) r'; eauto.
Qed.
Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split⇒ n r rob; revert e r rob;
induction n as [n IH] using lt_wf_ind⇒ e r rob Hr Hrob HΦ.
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; [done|]=> k Ef σ1 rf rfl ???.
destruct (wp_step_inv E Ef (pvs E E ∘ Φ) e k n σ1 r rob rf rfl) as [? Hstep]; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&?&?&?&Hwp'&?); auto.
∃ r2, r2', rob2, rob2'; split_and?; [|apply (IH k)| | |]; auto.
Qed.
Lemma wp_atomic E1 E2 e Φ :
E2 ⊆ E1 → atomic e →
(|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
Proof.
rewrite wp_eq pvs_eq. intros ? He; split⇒ n r rl ?? Hvs.
destruct (Some_dec (to_val e)) as [[v <-%of_to_val]|].
- eapply wp_pre_value. rewrite pvs_eq.
intros k Ef σ rf rfl ???. destruct (Hvs k Ef σ rf rfl) as (r'&Hwp&?); auto.
apply wp_value_inv in Hwp. rewrite pvs_eq in Hwp.
destruct (Hwp k Ef σ rf rfl) as (r2'&HΦ&?); auto.
- apply wp_pre_step. done. intros k Ef σ1 rf rfl ???.
destruct (Hvs (S k) Ef σ1 rf rfl) as (r'&Hwp&?); auto.
destruct (wp_step_inv E2 Ef (pvs_def E2 E1 ∘ Φ) e k (S k) σ1 r' rl rf rfl)
as [Hsafe Hstep]; auto; [].
split; [done|]=> e2 σ2 ef ?.
destruct (Hstep e2 σ2 ef) as (r2&r2'&rl2&rl2'&?&Hwp'&?&?&?); clear Hsafe Hstep; auto.
destruct Hwp' as [k r2 rl2 v Hvs'|k r2 rl2 e2 Hgo];
[|destruct (He σ1 e2 σ2 ef); naive_solver].
rewrite -pvs_eq in Hvs'. apply pvs_trans in Hvs';auto. rewrite pvs_eq in Hvs'.
destruct (Hvs' k Ef σ2 (r2' ⋅ rf) (rl2' ⋅ rfl)) as (r3&[]); rewrite ?assoc; auto.
∃ r3, r2', rl2, rl2'; split_and?; eauto.
+ by rewrite -?assoc.
+ constructor; apply pvs_intro; auto.
Qed.
Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} ★ ⧆ R) ⊢ WP e @ E {{ v, Φ v ★ ⧆ R }}.
Proof.
rewrite wp_eq.
uPred.unseal; split; intros n r' rl' Hvalid Hvalidl (r&rR&rl&rRl&Hr&Hrl&Hwp&HaffR).
revert Hvalid Hvalidl. rewrite Hr Hrl; clear Hr Hrl; revert e r rl Hwp.
induction n as [n IH] using lt_wf_ind; intros e r1 rl1.
destruct 1 as [? r rl|n r rl e ? Hgo]=>??.
{ constructor. rewrite -uPred_sep_eq; apply pvs_frame_r; auto.
uPred.unseal; ∃ r, rR, rl, rRl; eauto. }
constructor; [done|]=> k Ef σ1 rf rfl ?? Hwsat.
destruct HaffR as (HR&Hempty).
destruct (Hgo k Ef σ1 (rR⋅rf) rfl) as [Hsafe Hstep]; auto.
{ rewrite (dist_le _ _ _ _ Hempty) ?right_id in Hwsat *; last lia.
by rewrite assoc. }
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rl2&rl2'&?&?&?&?&?); auto.
∃ (r2 ⋅ rR), r2', (rl2 ⋅ rRl), rl2'; split_and?; auto.
- rewrite (dist_le _ _ _ _ Hempty); last lia.
by rewrite ?right_id -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
- apply IH; eauto using uPred_closed.
split; eauto using uPred_closed, dist_le.
rewrite (dist_le _ _ _ _ Hempty) ?right_id; auto.
- rewrite (dist_le _ _ _ _ Hempty) ?right_id; auto.
Qed.
Lemma wp_frame_step_r E E1 E2 e Φ R :
to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
(WP e @ E {{ Φ }} ★ ⧆ |={E1,E2}=> ▷ |={E2,E1}=> R)
⊢ WP e @ E ∪ E1 {{ v, Φ v ★ ⧆ R }}.
Proof.
rewrite wp_eq pvs_eq⇒ He ??.
uPred.unseal; split; intros n r' rl' Hvalid Hvalidrl' (r&rR&rl&rRl&Hr&Hrl&Hwp&HR); cofe_subst.
constructor; [done|]=>k Ef σ1 rf rfl ?? Hws1.
destruct Hwp as [|n r rl e ? Hgo]; [by rewrite to_of_val in He|].
destruct HR as (HR&Hempty).
destruct (HR (S k) (E ∪ Ef) σ1 (r ⋅ rf) (rl ⋅ rfl)) as (s&Hvs&Hws2); auto.
{
eapply wsat_proper, Hws1; first by set_solver+.
- by rewrite ?assoc [rR ⋅ _]comm.
- by rewrite ?assoc [rRl ⋅ _]comm.
}
clear Hws1 HR.
destruct (Hgo k (E2 ∪ Ef) σ1 (s⋅rf) rfl) as [Hsafe Hstep]; auto.
{
rewrite (dist_le _ _ _ _ Hempty) ?left_id in Hws2 *; last lia; intros Hws2.
eapply wsat_proper, Hws2; first by set_solver+.
- by rewrite !assoc [s ⋅ _]comm.
- done.
}
clear Hgo.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rl2&rl2'&Hws3&?&?&?&?); auto. clear Hws2.
destruct (Hvs k (E ∪ Ef) σ2 (r2 ⋅ r2' ⋅ rf) (rl2 ⋅ rl2' ⋅ rfl)) as (t&HR&Hws4); auto.
{ rewrite (dist_le _ _ _ _ Hempty) ?left_id; last lia.
eapply wsat_proper, Hws3; first by set_solver+.
by rewrite !assoc [_ ⋅ s]comm !assoc. auto. }
clear Hvs Hws3.
∃ (r2 ⋅ t), r2', rl2, rl2'.
rewrite {1}(dist_le _ _ _ _ Hempty) ?left_id in Hws4 *; last lia; intros Hws4.
split_and?; auto.
- eapply wsat_proper, Hws4; first by set_solver+.
by rewrite !assoc [_ ⋅ t]comm.
auto.
- rewrite -uPred_sep_eq. move: wp_frame_r. rewrite wp_eq. uPred.unseal⇒Hframe.
apply Hframe; eauto. ∃ r2, t, rl2, (∅: iRes Λ Σ); split_and?; auto.
× rewrite ?right_id //=.
× move: wp_mask_frame_mono. rewrite wp_eq⇒Hmask.
eapply (Hmask E); by auto.
× split; auto. rewrite -(dist_le _ _ _ _ Hempty) //=. lia.
- rewrite (dist_le _ _ _ _ Hempty) ?right_id; last lia. auto.
Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split⇒ n r rl; revert e r rl;
induction n as [n IH] using lt_wf_ind⇒ e r rl ??.
destruct 1 as [|n r rl e ? Hgo].
{ rewrite -wp_eq. apply pvs_wp; rewrite ?wp_eq; done. }
constructor; auto using fill_not_val⇒ k Ef σ1 rf rfl ???.
destruct (Hgo k Ef σ1 rf rfl) as [Hsafe Hstep]; auto.
split.
{ destruct Hsafe as (e2&σ2&ef&?).
by ∃ (K e2), σ2, ef; apply fill_step. }
intros e2 σ2 ef ?.
destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto.
destruct (Hstep e2' σ2 ef) as (r2&r2'&rl2&rl2'&?&?&?&?&?); auto.
∃ r2, r2', rl2, rl2'; split_and?; try eapply IH; eauto.
Qed.
From iris.program_logic Require Import wsat.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 100 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 100 (_ ∉_) ⇒ set_solver.
Local Hint Extern 100 (@subseteq coPset _ _ _) ⇒ set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
Record wp_go {Λ Σ} (E : coPset) (Φ Φfork : expr Λ → nat → iRes Λ Σ → iRes Λ Σ → Prop)
(k : nat) (σ1 : state Λ) (rf rfl rob: iRes Λ Σ) (e1 : expr Λ) := {
wf_safe : reducible e1 σ1;
wp_step e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef →
∃ r2 r2' rob2 rob2',
wsat k E σ2 (r2 ⋅ r2' ⋅ rf) (rob2 ⋅ rob2' ⋅ rfl) ∧
Φ e2 k r2 rob2 ∧
(∀ e', ef = Some e' → Φfork e' k r2' rob2') ∧
(ef = None → rob2' ≡{k}≡ ∅) ∧
rob ⤳_(k) rob2 ⋅ rob2'
}.
CoInductive wp_pre {Λ Σ} (E : coPset)
(Φ : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → iRes Λ Σ → Prop :=
| wp_pre_value n r rob v : (|={E}=> Φ v)%I n r rob → wp_pre E Φ (of_val v) n r rob
| wp_pre_step n r1 rob1 e1 :
to_val e1 = None →
(∀ k Ef σ1 rf rfl,
0 < k < n → E ⊥ Ef →
wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) (rob1 ⋅ rfl) →
wp_go (E ∪ Ef) (wp_pre E Φ)
(wp_pre ⊤ (λ _, uPred_stopped%I)) k σ1 rf rfl rob1 e1) →
wp_pre E Φ e1 n r1 rob1.
Program Definition wp_def {Λ Σ} (E : coPset) (e : expr Λ)
(Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
Next Obligation.
intros Λ Σ E e Φ n1 n2 r1 r2 rob; revert Φ E e n2 r1 r2 rob.
induction n1 as [n1 IH] using lt_wf_ind; intros Φ E e n2 r1 r1' rob.
destruct 1 as [|n1 r1 rob1 e1 ? Hgo].
- constructor; eauto using uPred_mono.
- intros [rf' Hr Hrl]. constructor; [done|intros k Ef σ1 rf rfl ???].
destruct (Hgo k Ef σ1 (rf' ⋅ rf) rfl) as [Hsafe Hstep];
rewrite ?assoc -?(dist_le _ _ _ _ Hr); auto;
first rewrite ?(dist_le _ _ _ _ Hrl); auto;
constructor; [done|].
intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&?&?&?&?&?); auto.
∃ r2, (r2' ⋅ rf'), rob2, rob2'; split_and?;
eauto 10 using (IH k), cmra_included_l, cmra_includedN_l.
by rewrite -assoc -assoc (assoc _ r2).
rewrite -(dist_le _ _ _ _ Hrl); eauto.
Qed.
Next Obligation. destruct 1; constructor; eauto using uPred_closed. Qed.
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.
Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
(at level 20, e, Φ at level 200,
format "'WP' e @ E {{ Φ } }") : uPred_scope.
Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
(at level 20, e, Φ at level 200,
format "'WP' e {{ Φ } }") : uPred_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp E e (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e @ E {{ v , Q } }") : uPred_scope.
Notation "'WP' e {{ v , Q } }" := (wp ⊤ e (λ v, Q))
(at level 20, e, Q at level 200,
format "'WP' e {{ v , Q } }") : uPred_scope.
Section wp.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Global Instance wp_ne E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
Proof.
cut (∀ Φ Ψ, (∀ v, Φ v ≡{n}≡ Ψ v) →
∀ n' r rob, n' ≤ n → ✓{n'} r → ✓{n'} rob → wp E e Φ n' r rob → wp E e Ψ n' r rob).
{ rewrite wp_eq. intros help Φ Ψ HΦΨ. by do 2 split; apply help. }
rewrite wp_eq. intros Φ Ψ HΦΨ n' r rob; revert e r rob.
induction n' as [n' IH] using lt_wf_ind⇒ e r rob.
destruct 4 as [n' r rob v HpvsQ|n' r rob e1 ? Hgo].
{ constructor. by eapply pvs_ne, HpvsQ; eauto. }
constructor; [done|]=> k Ef σ1 rf rfl ???.
destruct (Hgo k Ef σ1 rf rfl) as [Hsafe Hstep]; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&?&?&?&?&?); auto.
∃ r2, r2', rob2, rob2'; split_and?; [|eapply IH| | |]; eauto.
Qed.
Global Instance wp_proper E e :
Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e).
Proof.
by intros Φ Φ' ?; apply equiv_dist⇒n; apply wp_ne⇒v; apply equiv_dist.
Qed.
Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
E1 ⊆ E2 → (∀ v, Φ v ⊢ Ψ v) → WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Ψ }}.
Proof.
rewrite wp_eq. intros HE HΦ; split⇒ n r rob.
revert e r rob; induction n as [n IH] using lt_wf_ind⇒ e r rob.
destruct 3 as [n' r rob v HpvsQ|n' r rob e1 ? Hgo].
{ constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
constructor; [done|]=> k Ef σ1 rf rfl ???.
assert (E2 ∪ Ef = E1 ∪ (E2 ∖ E1 ∪ Ef)) as HE'.
{ by rewrite assoc_L -union_difference_L. }
destruct (Hgo k ((E2 ∖ E1) ∪ Ef) σ1 rf rfl) as [Hsafe Hstep]; rewrite -?HE'; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&?&?&?&?&?); auto.
∃ r2, r2', rob2, rob2'; split_and?; [rewrite HE'|eapply IH| | |]; eauto.
Qed.
Lemma wp_zero E e Φ r rob : wp_def E e Φ 0 r rob.
Proof.
case EQ: (to_val e).
- rewrite -(of_to_val _ _ EQ). constructor. rewrite pvs_eq.
exact: pvs_zero.
- constructor; first done. intros ??????. exfalso. omega.
Qed.
Lemma wp_value_inv E Φ v n r rob: wp_def E (of_val v) Φ n r rob → pvs E E (Φ v) n r rob.
Proof.
by inversion 1 as [|???? He]; [|rewrite ?to_of_val in He]; simplify_eq.
Qed.
Lemma wp_step_inv E Ef Φ e k n σ r rob rf rfl :
to_val e = None → 0 < k < n → E ⊥ Ef →
wp_def E e Φ n r rob → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) (rob ⋅ rfl) →
wp_go (E ∪ Ef) (λ e, wp_def E e Φ) (λ e, wp_def ⊤ e (λ _, uPred_stopped%I)) k σ rf rfl rob e.
Proof.
intros He; destruct 3; [by rewrite ?to_of_val in He|eauto using wsat_weaken].
Qed.
Lemma wp_value' E Φ v : Φ v ⊢ WP of_val v @ E {{ Φ }}.
Proof. rewrite wp_eq. split⇒ n r; constructor; by apply pvs_intro. Qed.
Lemma pvs_wp E e Φ : (|={E}=> WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split⇒ n r rob ? ? Hvs.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
{ constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
split⇒ ?????; apply wp_value_inv. }
constructor; [done|]=> k Ef σ1 rf rfl ???.
rewrite pvs_eq in Hvs. destruct (Hvs (S k) Ef σ1 rf rfl) as (r'&Hwp&Hwsat); auto.
eapply wp_step_inv with (S k) r'; eauto.
Qed.
Lemma wp_pvs E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split⇒ n r rob; revert e r rob;
induction n as [n IH] using lt_wf_ind⇒ e r rob Hr Hrob HΦ.
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; [done|]=> k Ef σ1 rf rfl ???.
destruct (wp_step_inv E Ef (pvs E E ∘ Φ) e k n σ1 r rob rf rfl) as [? Hstep]; auto.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&?&?&?&Hwp'&?); auto.
∃ r2, r2', rob2, rob2'; split_and?; [|apply (IH k)| | |]; auto.
Qed.
Lemma wp_atomic E1 E2 e Φ :
E2 ⊆ E1 → atomic e →
(|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
Proof.
rewrite wp_eq pvs_eq. intros ? He; split⇒ n r rl ?? Hvs.
destruct (Some_dec (to_val e)) as [[v <-%of_to_val]|].
- eapply wp_pre_value. rewrite pvs_eq.
intros k Ef σ rf rfl ???. destruct (Hvs k Ef σ rf rfl) as (r'&Hwp&?); auto.
apply wp_value_inv in Hwp. rewrite pvs_eq in Hwp.
destruct (Hwp k Ef σ rf rfl) as (r2'&HΦ&?); auto.
- apply wp_pre_step. done. intros k Ef σ1 rf rfl ???.
destruct (Hvs (S k) Ef σ1 rf rfl) as (r'&Hwp&?); auto.
destruct (wp_step_inv E2 Ef (pvs_def E2 E1 ∘ Φ) e k (S k) σ1 r' rl rf rfl)
as [Hsafe Hstep]; auto; [].
split; [done|]=> e2 σ2 ef ?.
destruct (Hstep e2 σ2 ef) as (r2&r2'&rl2&rl2'&?&Hwp'&?&?&?); clear Hsafe Hstep; auto.
destruct Hwp' as [k r2 rl2 v Hvs'|k r2 rl2 e2 Hgo];
[|destruct (He σ1 e2 σ2 ef); naive_solver].
rewrite -pvs_eq in Hvs'. apply pvs_trans in Hvs';auto. rewrite pvs_eq in Hvs'.
destruct (Hvs' k Ef σ2 (r2' ⋅ rf) (rl2' ⋅ rfl)) as (r3&[]); rewrite ?assoc; auto.
∃ r3, r2', rl2, rl2'; split_and?; eauto.
+ by rewrite -?assoc.
+ constructor; apply pvs_intro; auto.
Qed.
Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} ★ ⧆ R) ⊢ WP e @ E {{ v, Φ v ★ ⧆ R }}.
Proof.
rewrite wp_eq.
uPred.unseal; split; intros n r' rl' Hvalid Hvalidl (r&rR&rl&rRl&Hr&Hrl&Hwp&HaffR).
revert Hvalid Hvalidl. rewrite Hr Hrl; clear Hr Hrl; revert e r rl Hwp.
induction n as [n IH] using lt_wf_ind; intros e r1 rl1.
destruct 1 as [? r rl|n r rl e ? Hgo]=>??.
{ constructor. rewrite -uPred_sep_eq; apply pvs_frame_r; auto.
uPred.unseal; ∃ r, rR, rl, rRl; eauto. }
constructor; [done|]=> k Ef σ1 rf rfl ?? Hwsat.
destruct HaffR as (HR&Hempty).
destruct (Hgo k Ef σ1 (rR⋅rf) rfl) as [Hsafe Hstep]; auto.
{ rewrite (dist_le _ _ _ _ Hempty) ?right_id in Hwsat *; last lia.
by rewrite assoc. }
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rl2&rl2'&?&?&?&?&?); auto.
∃ (r2 ⋅ rR), r2', (rl2 ⋅ rRl), rl2'; split_and?; auto.
- rewrite (dist_le _ _ _ _ Hempty); last lia.
by rewrite ?right_id -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
- apply IH; eauto using uPred_closed.
split; eauto using uPred_closed, dist_le.
rewrite (dist_le _ _ _ _ Hempty) ?right_id; auto.
- rewrite (dist_le _ _ _ _ Hempty) ?right_id; auto.
Qed.
Lemma wp_frame_step_r E E1 E2 e Φ R :
to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
(WP e @ E {{ Φ }} ★ ⧆ |={E1,E2}=> ▷ |={E2,E1}=> R)
⊢ WP e @ E ∪ E1 {{ v, Φ v ★ ⧆ R }}.
Proof.
rewrite wp_eq pvs_eq⇒ He ??.
uPred.unseal; split; intros n r' rl' Hvalid Hvalidrl' (r&rR&rl&rRl&Hr&Hrl&Hwp&HR); cofe_subst.
constructor; [done|]=>k Ef σ1 rf rfl ?? Hws1.
destruct Hwp as [|n r rl e ? Hgo]; [by rewrite to_of_val in He|].
destruct HR as (HR&Hempty).
destruct (HR (S k) (E ∪ Ef) σ1 (r ⋅ rf) (rl ⋅ rfl)) as (s&Hvs&Hws2); auto.
{
eapply wsat_proper, Hws1; first by set_solver+.
- by rewrite ?assoc [rR ⋅ _]comm.
- by rewrite ?assoc [rRl ⋅ _]comm.
}
clear Hws1 HR.
destruct (Hgo k (E2 ∪ Ef) σ1 (s⋅rf) rfl) as [Hsafe Hstep]; auto.
{
rewrite (dist_le _ _ _ _ Hempty) ?left_id in Hws2 *; last lia; intros Hws2.
eapply wsat_proper, Hws2; first by set_solver+.
- by rewrite !assoc [s ⋅ _]comm.
- done.
}
clear Hgo.
split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&rl2&rl2'&Hws3&?&?&?&?); auto. clear Hws2.
destruct (Hvs k (E ∪ Ef) σ2 (r2 ⋅ r2' ⋅ rf) (rl2 ⋅ rl2' ⋅ rfl)) as (t&HR&Hws4); auto.
{ rewrite (dist_le _ _ _ _ Hempty) ?left_id; last lia.
eapply wsat_proper, Hws3; first by set_solver+.
by rewrite !assoc [_ ⋅ s]comm !assoc. auto. }
clear Hvs Hws3.
∃ (r2 ⋅ t), r2', rl2, rl2'.
rewrite {1}(dist_le _ _ _ _ Hempty) ?left_id in Hws4 *; last lia; intros Hws4.
split_and?; auto.
- eapply wsat_proper, Hws4; first by set_solver+.
by rewrite !assoc [_ ⋅ t]comm.
auto.
- rewrite -uPred_sep_eq. move: wp_frame_r. rewrite wp_eq. uPred.unseal⇒Hframe.
apply Hframe; eauto. ∃ r2, t, rl2, (∅: iRes Λ Σ); split_and?; auto.
× rewrite ?right_id //=.
× move: wp_mask_frame_mono. rewrite wp_eq⇒Hmask.
eapply (Hmask E); by auto.
× split; auto. rewrite -(dist_le _ _ _ _ Hempty) //=. lia.
- rewrite (dist_le _ _ _ _ Hempty) ?right_id; last lia. auto.
Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split⇒ n r rl; revert e r rl;
induction n as [n IH] using lt_wf_ind⇒ e r rl ??.
destruct 1 as [|n r rl e ? Hgo].
{ rewrite -wp_eq. apply pvs_wp; rewrite ?wp_eq; done. }
constructor; auto using fill_not_val⇒ k Ef σ1 rf rfl ???.
destruct (Hgo k Ef σ1 rf rfl) as [Hsafe Hstep]; auto.
split.
{ destruct Hsafe as (e2&σ2&ef&?).
by ∃ (K e2), σ2, ef; apply fill_step. }
intros e2 σ2 ef ?.
destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto.
destruct (Hstep e2' σ2 ef) as (r2&r2'&rl2&rl2'&?&?&?&?&?); auto.
∃ r2, r2', rl2, rl2'; split_and?; try eapply IH; eauto.
Qed.
Import uPred.
Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
Proof. by apply wp_mask_frame_mono. Qed.
Global Instance wp_mono' E e :
Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ E e).
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
Lemma wp_strip_pvs E e P Φ :
(P ⊢ WP e @ E {{ Φ }}) → (|={E}=> P) ⊢ WP e @ E {{ Φ }}.
Proof. move=>->. by rewrite pvs_wp. Qed.
Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊢ WP e @ E {{ Φ }}.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
Lemma wp_value_pvs' E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ E {{ Φ }}.
Proof. intros. by rewrite -wp_pvs -wp_value'. Qed.
Lemma wp_value_pvs E Φ e v :
to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}.
Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
Lemma wp_frame_l E e Φ R : (⧆R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, ⧆R ★ Φ v }}.
Proof. setoid_rewrite (comm _ (⧆ R)%I); apply wp_frame_r. Qed.
Lemma wp_frame_step_r' E e Φ R :
to_val e = None → (WP e @ E {{ Φ }} ★ ⧆ ▷ R) ⊢ WP e @ E {{ v, Φ v ★ ⧆ R }}.
Proof.
intros. rewrite {2}(_ : E = E ∪ ∅); last by set_solver.
rewrite -(wp_frame_step_r E ∅ ∅); [|auto|set_solver..].
apply sep_mono_r, affine_mono. rewrite -!pvs_intro. done.
Qed.
Lemma wp_frame_step_l E E1 E2 e Φ R :
to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
(⧆(|={E1,E2}=> ▷ |={E2,E1}=> R) ★ WP e @ E {{ Φ }})
⊢ WP e @ (E ∪ E1) {{ v, ⧆ R ★ Φ v }}.
Proof.
rewrite [(⧆(|={E1,E2}=> _) ★ _)%I]comm; setoid_rewrite (comm _ (⧆ R)%I).
apply wp_frame_step_r.
Qed.
Lemma wp_frame_step_l' E e Φ R :
to_val e = None → (⧆ ▷ R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, ⧆ R ★ Φ v }}.
Proof.
rewrite (comm _ (⧆ ▷ R)%I); setoid_rewrite (comm _ (⧆ R)%I).
apply wp_frame_step_r'.
Qed.
Lemma wp_wand_l E e Φ Ψ :
⧆(∀ v, Φ v -★ Ψ v) ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
Proof.
rewrite wp_frame_l. apply wp_mono⇒ v. by rewrite (forall_elim v) affine_elim wand_elim_l.
Qed.
Lemma wp_wand_r E e Φ Ψ :
WP e @ E {{ Φ }} ★ ⧆(∀ v, Φ v -★ Ψ v) ⊢ WP e @ E {{ Ψ }}.
Proof. by rewrite comm wp_wand_l. Qed.
Lemma wp_mask_weaken E1 E2 e Φ :
E1 ⊆ E2 → WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Φ }}.
Proof. auto using wp_mask_frame_mono. Qed.
Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
Proof. by apply wp_mask_frame_mono. Qed.
Global Instance wp_mono' E e :
Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ E e).
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
Lemma wp_strip_pvs E e P Φ :
(P ⊢ WP e @ E {{ Φ }}) → (|={E}=> P) ⊢ WP e @ E {{ Φ }}.
Proof. move=>->. by rewrite pvs_wp. Qed.
Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊢ WP e @ E {{ Φ }}.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
Lemma wp_value_pvs' E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ E {{ Φ }}.
Proof. intros. by rewrite -wp_pvs -wp_value'. Qed.
Lemma wp_value_pvs E Φ e v :
to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}.
Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
Lemma wp_frame_l E e Φ R : (⧆R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, ⧆R ★ Φ v }}.
Proof. setoid_rewrite (comm _ (⧆ R)%I); apply wp_frame_r. Qed.
Lemma wp_frame_step_r' E e Φ R :
to_val e = None → (WP e @ E {{ Φ }} ★ ⧆ ▷ R) ⊢ WP e @ E {{ v, Φ v ★ ⧆ R }}.
Proof.
intros. rewrite {2}(_ : E = E ∪ ∅); last by set_solver.
rewrite -(wp_frame_step_r E ∅ ∅); [|auto|set_solver..].
apply sep_mono_r, affine_mono. rewrite -!pvs_intro. done.
Qed.
Lemma wp_frame_step_l E E1 E2 e Φ R :
to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
(⧆(|={E1,E2}=> ▷ |={E2,E1}=> R) ★ WP e @ E {{ Φ }})
⊢ WP e @ (E ∪ E1) {{ v, ⧆ R ★ Φ v }}.
Proof.
rewrite [(⧆(|={E1,E2}=> _) ★ _)%I]comm; setoid_rewrite (comm _ (⧆ R)%I).
apply wp_frame_step_r.
Qed.
Lemma wp_frame_step_l' E e Φ R :
to_val e = None → (⧆ ▷ R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ v, ⧆ R ★ Φ v }}.
Proof.
rewrite (comm _ (⧆ ▷ R)%I); setoid_rewrite (comm _ (⧆ R)%I).
apply wp_frame_step_r'.
Qed.
Lemma wp_wand_l E e Φ Ψ :
⧆(∀ v, Φ v -★ Ψ v) ★ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
Proof.
rewrite wp_frame_l. apply wp_mono⇒ v. by rewrite (forall_elim v) affine_elim wand_elim_l.
Qed.
Lemma wp_wand_r E e Φ Ψ :
WP e @ E {{ Φ }} ★ ⧆(∀ v, Φ v -★ Ψ v) ⊢ WP e @ E {{ Ψ }}.
Proof. by rewrite comm wp_wand_l. Qed.
Lemma wp_mask_weaken E1 E2 e Φ :
E1 ⊆ E2 → WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Φ }}.
Proof. auto using wp_mask_frame_mono. Qed.
Definition wp_fsa (e : expr Λ) : FSA Λ Σ (val Λ) := λ E, wp E e.
Global Arguments wp_fsa _ _ / _.
Global Instance wp_fsa_prf : AffineFrameShiftAssertion (atomic e) (wp_fsa e).
Proof.
rewrite /wp_fsa; split; auto using wp_mask_frame_mono, wp_atomic.
- intros E Φ. by rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ).
- intros. rewrite -{1}(affine_affine P) wp_frame_r.
by setoid_rewrite affine_elim.
Qed.
End wp.
Global Arguments wp_fsa _ _ / _.
Global Instance wp_fsa_prf : AffineFrameShiftAssertion (atomic e) (wp_fsa e).
Proof.
rewrite /wp_fsa; split; auto using wp_mask_frame_mono, wp_atomic.
- intros E Φ. by rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ).
- intros. rewrite -{1}(affine_affine P) wp_frame_r.
by setoid_rewrite affine_elim.
Qed.
End wp.