From 2347013be470d8d928f346ca90bd2e88b3ea5f03 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 23 Jan 2024 17:33:03 +0100 Subject: [PATCH 1/2] Add lemma on total_ub_lift and termination ineq --- theories/prob/union_bounds.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/theories/prob/union_bounds.v b/theories/prob/union_bounds.v index 645ec7b6..4c2321c7 100644 --- a/theories/prob/union_bounds.v +++ b/theories/prob/union_bounds.v @@ -912,4 +912,16 @@ Section total_ub_theory. done. Qed. + Lemma total_ub_lift_termination_ineq (μ : distr A) f ε: + total_ub_lift μ f ε -> 1 - ε <= SeriesC μ. + Proof. + intros H2. + assert (∀ x, Decision (f x)). + { intros. apply make_decision. } + trans (prob μ (λ x, bool_decide (f x))). + - apply H2. intros. by apply bool_decide_eq_true_2. + - apply SeriesC_le; last apply pmf_ex_seriesC. + intros n; case_bool_decide; pose proof (pmf_pos (μ) n); lra. + Qed. + End total_ub_theory. From 34f7954e7226058ca37d16d23fa2d36f6007a709 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Wed, 24 Jan 2024 14:37:14 +0100 Subject: [PATCH 2/2] strengthened adequacy! --- theories/ub_logic/total_adequacy.v | 240 +++++++++++++++--------- theories/ub_logic/ub_total_weakestpre.v | 25 +++ 2 files changed, 172 insertions(+), 93 deletions(-) diff --git a/theories/ub_logic/total_adequacy.v b/theories/ub_logic/total_adequacy.v index f8ccf43e..5f431abd 100644 --- a/theories/ub_logic/total_adequacy.v +++ b/theories/ub_logic/total_adequacy.v @@ -6,18 +6,18 @@ From clutch.prob Require Import distribution union_bounds. Import uPred. -Lemma twp_step_fupd_ineq_prim_step (e : language.expr prob_lang) σ (ε ε1:nonnegreal) (ε2: language.cfg prob_lang -> nonnegreal) R: +Lemma twp_step_fupd_total_ub_lift_prim_step (e : language.expr prob_lang) σ (ε ε1:nonnegreal) (ε2: language.cfg prob_lang -> nonnegreal) R P: reducible e σ -> (∃ r, ∀ ρ : language.cfg prob_lang, ε2 ρ <= r) -> ε1 + SeriesC (λ ρ, prim_step e σ ρ * ε2 ρ) <= ε -> ub_lift (prim_step e σ) R ε1 -> - (∀ e, R e → 1 - ε2 e <= SeriesC (lim_exec e)) -> - 1 - ε <= SeriesC (λ a, step (e, σ) a * SeriesC (lim_exec a)). + (∀ e, R e → 1 - ε2 e <= prob (lim_exec e) P) -> + 1 - ε <= SeriesC (λ a, step (e, σ) a * prob (lim_exec a) P). Proof. intros Hred Hbound Hsum Hub H. simpl. assert (1 - (ε1 + SeriesC (λ ρ, prim_step e σ ρ * ε2 ρ)) <= - SeriesC (λ a, prim_step e σ a * SeriesC (lim_exec a))) as Hint; last first. + SeriesC (λ a, prim_step e σ a * prob (lim_exec a) P)) as Hint; last first. { etrans; last exact. apply Rminus_le. lra. } rewrite Rcomplements.Rle_minus_l Rplus_comm Rplus_assoc. rewrite <-SeriesC_plus; last first. @@ -25,8 +25,8 @@ Proof. - instantiate (1 := prim_step e σ). apply pmf_ex_seriesC. - intros. split. - + by apply Rmult_le_pos. - + rewrite <-Rmult_1_r. by apply Rmult_le_compat_l. + + apply Rmult_le_pos; try done. apply prob_ge_0. + + rewrite <-Rmult_1_r. apply Rmult_le_compat_l; first done. apply prob_le_1. } { destruct Hbound as [r ?]. eapply ex_seriesC_le; last first. - instantiate (1 := λ ρ, prim_step e σ ρ * r). @@ -42,8 +42,8 @@ Proof. assert (forall ρ, Decision (R ρ)) as Hdec. { intros. apply make_decision. } rewrite (SeriesC_ext _ - (λ ρ, (if bool_decide(R ρ) then prim_step e σ ρ * (ε2 ρ + SeriesC (lim_exec ρ)) else 0)+ - if bool_decide (~R ρ) then prim_step e σ ρ * (ε2 ρ + SeriesC (lim_exec ρ)) else 0 + (λ ρ, (if bool_decide(R ρ) then prim_step e σ ρ * (ε2 ρ + prob (lim_exec ρ) P) else 0)+ + if bool_decide (~R ρ) then prim_step e σ ρ * (ε2 ρ + prob (lim_exec ρ) P) else 0 )); last first. { intros. repeat case_bool_decide; try done. - by rewrite Rplus_0_r. @@ -52,27 +52,27 @@ Proof. rewrite SeriesC_plus; last first. { eapply ex_seriesC_filter_pos. - intros. apply Rmult_le_pos; first done. - apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. + apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. - destruct Hbound as [r?]. eapply ex_seriesC_ext; last first. + eapply pmf_ex_seriesC_mult_fn. shelve. + intros. simpl. f_equal. Unshelve. exists (r+1). intros; split. - * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. - * by apply Rplus_le_compat. + * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. + * apply Rplus_le_compat; try done. apply prob_le_1. } { eapply ex_seriesC_filter_pos. - intros. apply Rmult_le_pos; first done. - apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. + apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. - destruct Hbound as [r?]. eapply ex_seriesC_ext; last first. + eapply pmf_ex_seriesC_mult_fn. shelve. + intros. simpl. f_equal. Unshelve. exists (r+1). intros; split. - * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. - * by apply Rplus_le_compat. + * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. + * apply Rplus_le_compat; try done. apply prob_le_1. } trans (ε1 + (SeriesC @@ -80,7 +80,7 @@ Proof. if bool_decide (R x) then prim_step e σ x else 0) + SeriesC (λ x : expr * state, - if bool_decide (¬ R x) then prim_step e σ x * (ε2 x + SeriesC (lim_exec x)) else 0))). + if bool_decide (¬ R x) then prim_step e σ x * (ε2 x + prob (lim_exec x) P) else 0))). 2:{ apply Rplus_le_compat_l. apply Rplus_le_compat_r. apply SeriesC_le. - intros. case_bool_decide; last done. @@ -90,11 +90,11 @@ Proof. rewrite Rplus_comm. by rewrite <-Rcomplements.Rle_minus_l. - apply ex_seriesC_filter_pos. + intros. apply Rmult_le_pos; [apply pmf_pos|]. - apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. + apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. + apply pmf_ex_seriesC_mult_fn. destruct Hbound as [r?]. exists (r+1). intros; split. - * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. - * by apply Rplus_le_compat. + * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. + * apply Rplus_le_compat; try done. apply prob_le_1. } trans (ε1 + (SeriesC (λ x : expr * state, if bool_decide (R x) then prim_step e σ x else 0))); last first. @@ -102,7 +102,7 @@ Proof. apply Rplus_le_compat_l. apply SeriesC_ge_0'. intros. case_bool_decide; try lra. apply Rmult_le_pos; [apply pmf_pos|]. - apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. + apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. } rewrite /ub_lift in Hub. assert (prob (prim_step e σ) (∽(λ ρ, bool_decide(R ρ)))%P <= ε1). @@ -125,18 +125,18 @@ Proof. apply K. apply Hred. Qed. -Lemma twp_step_fupd_ineq_state_step (e : language.expr prob_lang) σ l (ε ε1:nonnegreal) (ε2: _ -> nonnegreal) R: +Lemma twp_step_fupd_total_ub_lift_state_step (e : language.expr prob_lang) σ l (ε ε1:nonnegreal) (ε2: _ -> nonnegreal) R P: l ∈ language.get_active σ -> (∃ r, ∀ ρ : language.cfg prob_lang, ε2 ρ <= r) -> ε1 + SeriesC (λ ρ, language.state_step σ l ρ * ε2 (e, ρ)) <= ε -> ub_lift (language.state_step σ l) R ε1 -> - (∀ s, R s → 1 - ε2 (e, s) <= SeriesC (lim_exec (e, s))) -> - 1 - ε <= SeriesC (λ a, state_step σ l a * SeriesC (lim_exec (e, a))). + (∀ s, R s → 1 - ε2 (e, s) <= prob (lim_exec (e, s)) P) -> + 1 - ε <= SeriesC (λ a, state_step σ l a * prob (lim_exec (e, a)) P). Proof. -intros Hred Hbound Hsum Hub H. + intros Hred Hbound Hsum Hub H. simpl. assert (1 - (ε1 + SeriesC (λ ρ, state_step σ l ρ * ε2 (e, ρ))) <= - SeriesC (λ a, state_step σ l a * SeriesC (lim_exec (e, a)))) as Hint; last first. + SeriesC (λ a, state_step σ l a * prob (lim_exec (e, a)) P)) as Hint; last first. { etrans; last exact. rewrite -Ropp_minus_distr -(Ropp_minus_distr (_+_)). apply Ropp_le_cancel. rewrite !Ropp_involutive Rcomplements.Rle_minus_l. rewrite Rplus_assoc Rplus_opp_l Rplus_0_r. done. @@ -147,8 +147,8 @@ intros Hred Hbound Hsum Hub H. - instantiate (1 := state_step σ l). apply pmf_ex_seriesC. - intros. split. - + by apply Rmult_le_pos. - + rewrite <-Rmult_1_r. by apply Rmult_le_compat_l. + + apply Rmult_le_pos; try done. apply prob_ge_0. + + rewrite <-Rmult_1_r. apply Rmult_le_compat_l; try done. apply prob_le_1. } { destruct Hbound as [r ?]. eapply ex_seriesC_le; last first. - instantiate (1 := λ ρ, state_step σ l ρ * r). @@ -164,8 +164,8 @@ intros Hred Hbound Hsum Hub H. assert (forall ρ, Decision (R ρ)) as Hdec. { intros. apply make_decision. } rewrite (SeriesC_ext _ - (λ ρ, (if bool_decide(R ρ) then state_step σ l ρ * (ε2 (e, ρ) + SeriesC (lim_exec (e, ρ))) else 0)+ - if bool_decide (~R ρ) then state_step σ l ρ * (ε2 (e, ρ) + SeriesC (lim_exec (e, ρ))) else 0 + (λ ρ, (if bool_decide(R ρ) then state_step σ l ρ * (ε2 (e, ρ) + prob (lim_exec (e, ρ)) P) else 0)+ + if bool_decide (~R ρ) then state_step σ l ρ * (ε2 (e, ρ) + prob (lim_exec (e, ρ)) P) else 0 )); last first. { intros. repeat case_bool_decide; try done. - by rewrite Rplus_0_r. @@ -174,27 +174,27 @@ intros Hred Hbound Hsum Hub H. rewrite SeriesC_plus; last first. { eapply ex_seriesC_filter_pos. - intros. apply Rmult_le_pos; first done. - apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. + apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. - destruct Hbound as [r?]. eapply ex_seriesC_ext; last first. + eapply pmf_ex_seriesC_mult_fn. shelve. + intros. simpl. f_equal. Unshelve. exists (r+1). intros; split. - * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. - * by apply Rplus_le_compat. + * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. + * apply Rplus_le_compat; try done. apply prob_le_1. } { eapply ex_seriesC_filter_pos. - intros. apply Rmult_le_pos; first done. - apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. + apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. - destruct Hbound as [r?]. eapply ex_seriesC_ext; last first. + eapply pmf_ex_seriesC_mult_fn. shelve. + intros. simpl. f_equal. Unshelve. exists (r+1). intros; split. - * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. - * by apply Rplus_le_compat. + * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. + * apply Rplus_le_compat; try done. apply prob_le_1. } trans (ε1 + (SeriesC @@ -202,7 +202,7 @@ intros Hred Hbound Hsum Hub H. if bool_decide (R x) then state_step σ l x else 0) + SeriesC (λ x, - if bool_decide (¬ R x) then state_step σ l x * (ε2 (e, x) + SeriesC (lim_exec (e, x))) else 0))). + if bool_decide (¬ R x) then state_step σ l x * (ε2 (e, x) + prob (lim_exec (e, x)) P) else 0))). 2:{ apply Rplus_le_compat_l. apply Rplus_le_compat_r. apply SeriesC_le. - intros. case_bool_decide; last done. @@ -212,11 +212,11 @@ intros Hred Hbound Hsum Hub H. rewrite Rplus_comm. by rewrite <-Rcomplements.Rle_minus_l. - apply ex_seriesC_filter_pos. + intros. apply Rmult_le_pos; [apply pmf_pos|]. - apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. + apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. + apply pmf_ex_seriesC_mult_fn. destruct Hbound as [r?]. exists (r+1). intros; split. - * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. - * by apply Rplus_le_compat. + * apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. + * apply Rplus_le_compat; try done. apply prob_le_1. } trans (ε1 + (SeriesC (λ x, if bool_decide (R x) then state_step σ l x else 0))); last first. @@ -224,7 +224,7 @@ intros Hred Hbound Hsum Hub H. apply Rplus_le_compat_l. apply SeriesC_ge_0'. intros. case_bool_decide; try lra. apply Rmult_le_pos; [apply pmf_pos|]. - apply Rplus_le_le_0_compat; [apply cond_nonneg|apply pmf_SeriesC_ge_0]. + apply Rplus_le_le_0_compat; [apply cond_nonneg|apply prob_ge_0]. } rewrite /ub_lift in Hub. assert (prob (state_step σ l) (∽(λ ρ, bool_decide(R ρ)))%P <= ε1). @@ -250,51 +250,58 @@ Qed. Section adequacy. Context `{!ub_clutchGS Σ}. - - Theorem twp_step_fupd (e : expr) (σ : state) (ε : nonnegreal) φ : + + Theorem twp_step_fupd_total_ub_lift (e : expr) (σ : state) (ε : nonnegreal) φ : state_interp σ ∗ err_interp (ε) ∗ WP e [{ v, ⌜φ v⌝ }] ⊢ - |={⊤,∅}=> ⌜(1 - ε <= SeriesC (lim_exec (e, σ)))%R⌝. + |={⊤,∅}=> ⌜total_ub_lift (lim_exec (e, σ)) φ ε⌝. Proof. iIntros "(Hstate & Herr & Htwp)". iRevert (σ ε) "Hstate Herr". - pose proof (ub_twp_ind' ⊤ () (λ e _, ∀ (a : state) (a0 : nonnegreal), - state_interp a -∗ err_interp a0 ={⊤,∅}=∗ ⌜1 - a0 <= SeriesC (lim_exec (e, a))⌝)%I) as H. iApply H. + pose proof (ub_twp_ind_simple ⊤ () (λ e, ∀ (a : state) (a0 : nonnegreal), + state_interp a -∗ err_interp a0 ={⊤,∅}=∗ ⌜total_ub_lift (lim_exec (e, a)) φ a0⌝)%I) as H. iApply H. 2: { destruct twp_default. done. } clear H e. iModIntro. - iIntros (e Φ) "H". + iIntros (e) "H". iIntros (σ ε) "Hs Hec". rewrite /ub_twp_pre. case_match. - - iApply fupd_mask_intro; first done. iIntros "_". + - iMod "H" as "%". + iApply fupd_mask_intro; first done. iIntros "_". iPureIntro. + intros P HP. rewrite /prob. etrans. - 2:{ eapply SeriesC_ge_elem; last done. intros. apply pmf_pos. } + 2:{ eapply SeriesC_ge_elem; last apply ex_seriesC_filter_bool_pos; try done. + intros. destruct (P x); try lra. apply pmf_pos. } erewrite (lim_exec_term 0). - { simpl. rewrite H. rewrite dret_1_1; last done. destruct ε. simpl. lra. } + { simpl. rewrite H. rewrite dret_1_1; last done. destruct ε. simpl. + rewrite HP; try lra. done. } simpl. rewrite H. by rewrite dret_mass. - iSpecialize ("H" $! σ ε with "[$]"). iMod "H". iRevert (H). - iApply (exec_ub_strong_ind (λ ε e σ, ⌜language.to_val e = None⌝ ={∅}=∗ ⌜1 - ε <= SeriesC (lim_exec (e, σ))⌝)%I with "[][$H]"). + iApply (exec_ub_strong_ind (λ ε e σ, ⌜language.to_val e = None⌝ ={∅}=∗ ⌜total_ub_lift (lim_exec (e, σ)) φ ε⌝)%I with "[][$H]"). iModIntro. clear e σ ε. iIntros (e σ ε) "H %Hval". iDestruct "H" as "[H|[H|[H|H]]]". + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hineq & %Hub & H)". rewrite lim_exec_step step_or_final_no_final. 2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. } - rewrite dbind_mass. + rewrite {2}/total_ub_lift. + iIntros (P HP). + setoid_rewrite prob_dbind. iAssert (∀ ρ2 : language.expr prob_lang * language.state prob_lang, ⌜R ρ2⌝ ={∅}=∗ let '(e2, σ2) := ρ2 in - |={∅}=> ⌜1 - ε2 <= SeriesC (lim_exec (e2, σ2))⌝)%I with "[H]" as "H". + |={∅}=> ⌜total_ub_lift (lim_exec (e2, σ2)) φ ε2⌝)%I with "[H]" as "H". { iIntros (ρ2) "%Hρ2". iMod ("H" $! ρ2 Hρ2) as "H". destruct ρ2. iMod "H" as "(?&?&H)". iMod ("H" with "[$][$]"). iModIntro. iModIntro. done. } - iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - ε2 <= SeriesC (lim_exec e)⌝)%I). - { iIntros (H). iPureIntro. - eapply (twp_step_fupd_ineq_prim_step _ _ _ _ (λ _, ε2)); try done. + iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - ε2 <= prob (lim_exec e) P⌝)%I). + { + iIntros (HR). iPureIntro. + eapply (twp_step_fupd_total_ub_lift_prim_step _ _ _ _ (λ _, ε2)); try done. - exists ε. intros. trans (ε1 + ε2); last lra. destruct ε1, ε2. simpl. lra. - rewrite SeriesC_scal_r. etrans; last exact Hineq. pose proof (pmf_SeriesC (prim_step e σ)). @@ -306,25 +313,34 @@ Section adequacy. } iIntros (a HR). iMod ("H" $! a (HR)) as "H". destruct a. - iApply "H". + iMod "H" as "%". + iPureIntro. + by apply H. + iDestruct "H" as "(%R & %ε1 & %ε2 & %Hred & %Hbound & %Hineq & %Hub & H)". rewrite lim_exec_step step_or_final_no_final. 2: { rewrite /is_final. rewrite -eq_None_not_Some. simpl. by eapply reducible_not_val. } - rewrite dbind_mass. iAssert (∀ ρ2 : language.expr prob_lang * language.state prob_lang, ⌜R ρ2⌝ ={∅}=∗ let '(e2, σ2) := ρ2 in - |={∅}=> ⌜1 - (ε2 ρ2) <= SeriesC (lim_exec (e2, σ2))⌝)%I with "[H]" as "H". + |={∅}=> ⌜total_ub_lift (lim_exec (e2, σ2)) φ (ε2 ρ2)⌝)%I with "[H]" as "H". { iIntros (ρ2) "%Hρ2". iMod ("H" $! ρ2 Hρ2) as "H". destruct ρ2. iMod "H" as "(?&?&H)". iMod ("H" with "[$][$]"). iModIntro. iModIntro. done. } - iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - (ε2 e) <= SeriesC (lim_exec e)⌝)%I). - { iIntros (H). iPureIntro. by eapply twp_step_fupd_ineq_prim_step. } + rewrite {2}/total_ub_lift. + iIntros (P HP). + setoid_rewrite prob_dbind. + iApply (fupd_mono _ _ (⌜∀ e, R e -> 1 - (ε2 e) <= prob (lim_exec e) P⌝)%I). + { + iIntros (HR). iPureIntro. + by eapply twp_step_fupd_total_ub_lift_prim_step. + } iIntros (a HR). iMod ("H" $! a (HR)) as "H". destruct a. - iApply "H". + iMod "H" as "%". + iPureIntro. + by apply H. + remember (language.get_active σ) as l. assert (l ⊆ language.get_active σ) as Hsubseteq by set_solver. clear Heql. @@ -335,28 +351,30 @@ Section adequacy. 2:{ iApply "IH"; try done. iPureIntro. set_solver. } iDestruct "H" as "(%R & %ε1 & %ε2 & %Hineq & %Hub & H)". iAssert (∀ σ2 : language.state prob_lang, - ⌜R σ2⌝ ={∅}=∗ ⌜1 - ε2 <= SeriesC (lim_exec (e, σ2))⌝)%I with "[H]" as "H". + ⌜R σ2⌝ ={∅}=∗ ⌜total_ub_lift (lim_exec (e, σ2)) φ ε2⌝)%I with "[H]" as "H". { iIntros. iMod ("H" $! σ2 (H)) as "H". iDestruct "H" as "[H _]". iApply "H". done. } - iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 <= SeriesC (lim_exec (e, s))⌝)%I). - { iIntros (H). iPureIntro. rewrite (erasure.lim_exec_eq_erasure [l]); last set_solver. - simpl. erewrite SeriesC_ext; last by (intros; rewrite dret_id_right). - rewrite dbind_mass. - erewrite SeriesC_ext. - - eapply (twp_step_fupd_ineq_state_step _ _ _ _ _ (λ _, ε2)); try done. - + set_solver. - + exists ε. intros. trans (ε1 + ε2); last lra. destruct ε1, ε2. simpl. lra. - + rewrite SeriesC_scal_r. etrans; last exact Hineq. + rewrite {2}/total_ub_lift. + iIntros (P HP). + iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 <= prob (lim_exec (e, s)) P⌝)%I). + { + iIntros. iPureIntro. + rewrite (erasure.lim_exec_eq_erasure [l]); last set_solver. + simpl. + rewrite prob_dbind. + erewrite SeriesC_ext; last by rewrite dret_id_right. + eapply (twp_step_fupd_total_ub_lift_state_step _ _ _ _ _ (λ _, ε2)); try done. + + set_solver. + + exists ε. intros. trans (ε1 + ε2); last lra. destruct ε1, ε2. simpl. lra. + + rewrite SeriesC_scal_r. etrans; last exact Hineq. pose proof (pmf_SeriesC (language.state_step σ l)). cut (SeriesC (language.state_step σ l) * ε2 <= ε2). -- intros; lra. -- rewrite <-Rmult_1_l. apply Rmult_le_compat_r. ++ apply cond_nonneg. ++ exact. - - intros. by simpl. } - iIntros (a HR). iMod ("H" $! a (HR)) as "H". - destruct a. - iApply "H". + iIntros (a HR). iMod ("H" $! a (HR)) as "%H". + iPureIntro. by apply H. + remember (language.get_active σ) as l. assert (l ⊆ language.get_active σ) as Hsubseteq by set_solver. clear Heql. @@ -367,28 +385,31 @@ Section adequacy. 2:{ iApply "IH"; try done. iPureIntro. set_solver. } iDestruct "H" as "(%R & %ε1 & %ε2 & %Hbound & %Hineq & %Hub & H)". iAssert (∀ σ2 : language.state prob_lang, - ⌜R σ2⌝ ={∅}=∗ ⌜1 - (ε2 (e, σ2)) <= SeriesC (lim_exec (e, σ2))⌝)%I with "[H]" as "H". + ⌜R σ2⌝ ={∅}=∗ ⌜total_ub_lift (lim_exec (e, σ2)) φ (ε2 (e, σ2))⌝)%I with "[H]" as "H". { iIntros. iMod ("H" $! σ2 (H)) as "H". iDestruct "H" as "[H _]". iApply "H". done. } - iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 (e, s) <= SeriesC (lim_exec (e, s))⌝)%I). - { iIntros (H). iPureIntro. rewrite (erasure.lim_exec_eq_erasure [l]); last set_solver. - simpl. erewrite SeriesC_ext; last by (intros; rewrite dret_id_right). - rewrite dbind_mass. - erewrite SeriesC_ext. - - eapply twp_step_fupd_ineq_state_step; try done. - set_solver. - - intros; simpl. done. - } - iIntros (a HR). iMod ("H" $! a (HR)) as "H". - destruct a. - iApply "H". + rewrite {2}/total_ub_lift. + iIntros (P HP). + iApply (fupd_mono _ _ (⌜∀ s, R s -> 1 - ε2 (e, s) <= prob (lim_exec (e, s)) P⌝)%I). + { + iIntros. iPureIntro. + rewrite (erasure.lim_exec_eq_erasure [l]); last set_solver. + simpl. + rewrite prob_dbind. + erewrite SeriesC_ext; last by rewrite dret_id_right. + eapply twp_step_fupd_total_ub_lift_state_step; try done. + set_solver. + } + iIntros (a HR). iMod ("H" $! a (HR)) as "%H". + iPureIntro. by apply H. Qed. + End adequacy. - -Theorem twp_mass_lim_exec Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ : + +Theorem twp_total_ub_lift Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ : (∀ `{ub_clutchGS Σ}, ⊢ € ε -∗ WP e [{ v, ⌜φ v⌝ }]) → - (1 - ε <= SeriesC (lim_exec (e, σ)))%R. + total_ub_lift (lim_exec (e, σ)) φ ε. Proof. intros Hwp. eapply (step_fupdN_soundness_no_lc _ 0 0) => Hinv. @@ -397,11 +418,22 @@ Proof. iMod (ghost_map_alloc σ.(tapes)) as "[%γT [Ht _]]". iMod ec_alloc as (?) "[? ?]". set (HclutchGS := HeapG Σ _ _ _ γH γT _). - epose proof (twp_step_fupd e σ ε φ). + epose proof (twp_step_fupd_total_ub_lift e σ ε φ). iApply fupd_wand_r. iSplitL. - iApply H1. iFrame. by iApply Hwp. - - iIntros "%". iApply step_fupdN_intro; first done. done. -Qed. + - iIntros "%". iApply step_fupdN_intro; first done. done. +Qed. + + +Theorem twp_mass_lim_exec Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ : + (∀ `{ub_clutchGS Σ}, ⊢ € ε -∗ WP e [{ v, ⌜φ v⌝ }]) → + (1 - ε <= SeriesC (lim_exec (e, σ)))%R. +Proof. + intros Hwp. + eapply total_ub_lift_termination_ineq. + by eapply twp_total_ub_lift. +Qed. + Theorem twp_union_bound_lim Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ : (∀ `{ub_clutchGS Σ}, ⊢ € ε -∗ WP e [{ v, ⌜φ v⌝ }]) → @@ -418,6 +450,28 @@ Proof. Qed. (** limit rules *) + +Theorem twp_total_ub_lift_limit Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ : + (∀ `{ub_clutchGS Σ}, (∀ ε' : nonnegreal, ε' > ε -> ⊢ € ε' -∗ WP e [{ v, ⌜φ v⌝ }])) → + total_ub_lift (lim_exec (e, σ)) φ ε. +Proof. + intros H'. rewrite /total_ub_lift. + intros. + apply real_le_limit. + intros. + replace (1-_-_) with (1 - (ε+ε0)) by lra. + assert (0<=ε+ε0) as Hεsum. + { trans ε; try lra. by destruct ε. } + pose (mknonnegreal (ε+ε0) Hεsum) as NNRε0. + assert (ε+ε0 = (NNRbar_to_real (NNRbar.Finite (NNRε0)))) as Heq. + { by simpl. } + rewrite Heq. + eapply twp_total_ub_lift; try done. + intros. iIntros "He". + iApply H'; last done. + simpl. destruct ε; simpl; lra. +Qed. + Theorem twp_mass_lim_exec_limit Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ : (∀ `{ub_clutchGS Σ}, (∀ ε' : nonnegreal, ε' > ε -> ⊢ € ε' -∗ WP e [{ v, ⌜φ v⌝ }])) → (1 - ε <= SeriesC (lim_exec (e, σ)))%R. diff --git a/theories/ub_logic/ub_total_weakestpre.v b/theories/ub_logic/ub_total_weakestpre.v index d271263c..4e752209 100644 --- a/theories/ub_logic/ub_total_weakestpre.v +++ b/theories/ub_logic/ub_total_weakestpre.v @@ -126,6 +126,31 @@ Section ub_twp. { by iApply "H". } by iDestruct "H" as "[_?]". Qed. + + Lemma ub_twp_ind_simple E s Ψ Φ e: + (∀ n e, Proper (dist n) (Ψ e)) → + □ (∀ e, ub_twp_pre (λ _ e _, Ψ e) E e Φ -∗ Ψ e) -∗ + WP e @ s; E [{ Φ }] -∗ Ψ e. + Proof. + iIntros (HΨ) "#IH Htwp". + iRevert "IH". + iApply (ub_twp_ind _ (λ E e Φ, _) with "[]Htwp"). + { intros. intros ???. + rewrite /ub_twp_pre. repeat f_equiv. + } + clear. + iModIntro. + iIntros (e E Φ) "H #IH". + iApply "IH". + rewrite {2 4}/ub_twp_pre. case_match; first done. + iIntros (σ ε) "[Hs He]". + iMod ("H" with "[$]") as "H". + iModIntro. + iApply (exec_ub_mono_pred with "[]H"). + iIntros ([] []) "H". + iMod "H". iModIntro. iDestruct "H" as "(?&?&H)". + iFrame. iApply "H". done. + Qed. Lemma ub_twp_value_fupd' s E Φ v : WP of_val v @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v. Proof. rewrite ub_twp_unfold /ub_twp_pre to_of_val. auto. Qed.