From cbdb96984851e630d27d75ec0de4dfd5829a6c73 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 26 Sep 2024 13:42:27 +0200 Subject: [PATCH] Better spec --- theories/coneris/lib/hocap_flip.v | 104 +++++++++++++------- theories/coneris/lib/hocap_rand.v | 154 ++++++++++++++++-------------- 2 files changed, 150 insertions(+), 108 deletions(-) diff --git a/theories/coneris/lib/hocap_flip.v b/theories/coneris/lib/hocap_flip.v index 68b4db4b..cca4352f 100644 --- a/theories/coneris/lib/hocap_flip.v +++ b/theories/coneris/lib/hocap_flip.v @@ -49,29 +49,29 @@ Class flip_spec `{!conerisGS Σ} := FlipSpec ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ flip_tapes_frag (L:=L) γ1 α [] }}}; - flip_tape_spec_some {L: flipG Σ} N E γ1 (P: iProp Σ) (Q:iProp Σ) (α:loc) (n:bool) ns: + flip_tape_spec_some {L: flipG Σ} N E γ1 (P: iProp Σ) (Q:bool -> list bool -> iProp Σ) (α:loc) : ↑N⊆E -> {{{ is_flip (L:=L) N γ1 ∗ - (□ (P ={E∖↑N, ∅}=∗ flip_tapes_frag (L:=L) γ1 α (n::ns) ∗ - (flip_tapes_frag (L:=L) γ1 α ns ={∅, E∖↑N}=∗ Q))) ∗ + (□ (P ={E∖↑N, ∅}=∗ + ∃ n ns, flip_tapes_frag (L:=L) γ1 α (n::ns) ∗ + (flip_tapes_frag (L:=L) γ1 α ns ={∅, E∖↑N}=∗ Q n ns))) ∗ ▷ P }}} flip_tape #lbl:α @ E - {{{ RET #n; Q }}}; + {{{ (n:bool), RET #n; ∃ ns, Q n ns}}}; - flip_presample_spec {L: flipG Σ} NS E ns α - (ε2 : list bool -> R) - (P : iProp Σ) num T γ1 ε: + flip_presample_spec {L: flipG Σ} NS E (P : iProp Σ) T γ1: ↑NS ⊆ E -> - (∀ l, length l = num -> 0<=ε2 l)%R -> - (SeriesC (λ l, if length l =? num then ε2 l else 0) /(2^num) <= ε)%R-> is_flip (L:=L) NS γ1 -∗ - (□ (P ={E∖↑NS, ∅}=∗ ↯ ε ∗ flip_tapes_frag (L:=L) γ1 α ns ∗ + (□ (P ={E∖↑NS, ∅}=∗ + ∃ ε num ε2 α ns, ↯ ε ∗ flip_tapes_frag (L:=L) γ1 α ns ∗ + ⌜(∀ l, length l = num -> 0<=ε2 l)%R⌝ ∗ + ⌜(SeriesC (λ l, if length l =? num then ε2 l else 0) /(2^num) <= ε)%R⌝∗ (∀ ns', ⌜length ns' = num⌝ ∗ ↯ (ε2 ns') ∗ flip_tapes_frag (L:=L) γ1 α (ns ++ ns') - ={∅, E∖↑NS}=∗ T ns'))) + ={∅, E∖↑NS}=∗ T ε num ε2 α ns ns'))) -∗ P -∗ - wp_update E (∃ n, T n) + wp_update E (∃ ε num ε2 α ns ns', T ε num ε2 α ns ns') }. @@ -140,26 +140,48 @@ Section instantiate_flip. Qed. Next Obligation. simpl. - iIntros (??????? n ? ? Φ) "(#Hinv & #Hvs & HP) HΦ". + iIntros (????? Q ? ? Φ) "(#Hinv & #Hvs & HP) HΦ". wp_pures. - wp_apply (rand_tape_spec_some _ _ _ P Q with "[-HΦ]"); [done|..]. - - iSplit; first done. - iSplitR; last iFrame. + wp_apply (rand_tape_spec_some _ _ _ P (λ n ns, ∃ b bs, ⌜n= bool_to_nat b⌝ ∗ + ⌜ns = bool_to_nat <$> bs⌝ ∗ + Q b bs + + )%I with "[-HΦ]"); [done|..]. + - iFrame. iSplit; first done. iModIntro. iIntros "HP". - iMod ("Hvs" with "[$]") as "[Hfrag Hvs']". - by iFrame. - - iIntros "HQ". + iMod ("Hvs" with "[$]") as "(%b & %bs & Hfrag & Hrest)". + iFrame. + iModIntro. + iIntros "?". + iMod ("Hrest" with "[$]"). + by iFrame. + - iIntros (n) "(%&%&%&%&%&HQ)". wp_apply conversion.wp_int_to_bool as "_"; first done. - replace (Z_to_bool _) with n; first by iApply "HΦ". - destruct n; simpl. + iApply "HΦ". + subst. + iFrame. + replace (Z_to_bool _) with b; first iFrame. + destruct b; simpl. + rewrite Z_to_bool_neq_0; lia. + rewrite Z_to_bool_eq_0; lia. Qed. Next Obligation. simpl. - iIntros (??????????? Hsubset Hpos Hineq) "#Hinv #Hvs HP". - iMod (rand_presample_spec _ _ _ _ 1%nat (λ ls, ε2 (nat_to_bool <$>(fin_to_nat <$> ls))) P - _ (λ ls, T (nat_to_bool <$> (fin_to_nat <$> ls))) with "[][][$]") as "(%&?)"; [exact|..]. + iIntros (???? T ??) "#Hinv #Hvs HP". + iMod (rand_presample_spec _ _ P + (λ ε num tb ε2 α ns ns', + ∃ bs bs' ε2', ⌜tb = 1%nat⌝ ∗ ⌜fmap (FMap:= list_fmap) bool_to_nat bs = ns⌝ ∗ ⌜fmap (FMap:= list_fmap) bool_to_nat bs'=fin_to_nat <$> ns'⌝ ∗ + ⌜∀ xs ys, fmap (FMap:= list_fmap) bool_to_nat xs = fmap (FMap:= list_fmap)fin_to_nat ys -> ε2' xs = ε2 ys⌝ ∗ + T ε num ε2' α bs bs' + )%I + with "[][][$]") as "(%&%&%&%&%&%&%&%&%&%&->&<-&%&%&HT)"; [exact|exact| |iModIntro; iFrame]. + iModIntro. + iIntros "HP". + iMod ("Hvs" with "[$]") as "(%&%&%&%&%&Herr&Hfrag&%Hpos&%Hineq&Hvs')". + iFrame. + iModIntro. + iExists num, (λ ls, ε2 (nat_to_bool<$>(fin_to_nat <$> ls))). + repeat iSplit; try iPureIntro. - intros. apply Hpos. by rewrite !fmap_length. - etrans; last exact. @@ -186,18 +208,28 @@ Section instantiate_flip. + eapply ex_seriesC_list_length. intros. case_match; last done. by rewrite -Nat.eqb_eq. - - done. - - iModIntro. iIntros "HP". iMod ("Hvs" with "[$]") as "($&$&Hvs')". - iModIntro. - iIntros (ls) "(H1&H2&H3)". - iMod ("Hvs'" with "[H1 $H2 H3]") as "?"; last done. - iSplitL "H1". - + by rewrite !fmap_length. - + rewrite fmap_app -!list_fmap_compose. - erewrite (Forall_fmap_ext_1 (_∘_)); first done. - apply Forall_true. - intros x; by repeat (inv_fin x; simpl; try intros x). - - iModIntro. iFrame. + - iIntros (ls) "(H1&H2&H3)". + iMod ("Hvs'" with "[H1 $H2 H3]") as "?". + + rewrite !fmap_length !fmap_app. + iSplitL "H1"; first done. + rewrite -!list_fmap_compose. + erewrite (Forall_fmap_ext_1 (_∘_)); first done. + apply Forall_true. + intros x; by repeat (inv_fin x; simpl; try intros x). + + iFrame. iPureIntro; repeat split; try done. + * rewrite -!list_fmap_compose. + erewrite (Forall_fmap_ext_1 (_∘_)); first done. + apply Forall_true. + intros x; by repeat (inv_fin x; simpl; try intros x). + * intros ?? <-. + f_equal. + rewrite -!list_fmap_compose. + rewrite -{1}(list_fmap_id xs). + erewrite (Forall_fmap_ext_1 (_∘_)); first done. + apply Forall_true. + intros []; simpl. + -- by rewrite nat_to_bool_neq_0. + -- by rewrite nat_to_bool_eq_0. Qed. End instantiate_flip. diff --git a/theories/coneris/lib/hocap_rand.v b/theories/coneris/lib/hocap_rand.v index 83211ce5..42a7ed6f 100644 --- a/theories/coneris/lib/hocap_rand.v +++ b/theories/coneris/lib/hocap_rand.v @@ -51,28 +51,28 @@ Class rand_spec `{!conerisGS Σ} := RandSpec {{{ (v:val), RET v; ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ rand_tapes_frag (L:=L) γ2 α (tb, []) }}}; - rand_tape_spec_some {L: randG Σ} N E γ2 (P: iProp Σ) (Q:iProp Σ) (α:loc) (n:nat) (tb:nat) ns: + rand_tape_spec_some {L: randG Σ} N E γ2 (P: iProp Σ) (Q: nat ->list nat -> iProp Σ) (α:loc) (tb:nat) : ↑N⊆E -> {{{ is_rand (L:=L) N γ2 ∗ - (□ (P ={E∖↑N, ∅}=∗ rand_tapes_frag (L:=L) γ2 α (tb, n::ns) ∗ - (rand_tapes_frag (L:=L) γ2 α (tb, ns) ={∅, E∖↑N}=∗ Q))) ∗ + (□ (P ={E∖↑N, ∅}=∗ ∃ n ns, rand_tapes_frag (L:=L) γ2 α (tb, n::ns) ∗ + (rand_tapes_frag (L:=L) γ2 α (tb, ns) ={∅, E∖↑N}=∗ Q n ns))) ∗ ▷ P }}} rand_tape #lbl:α #tb @ E - {{{ RET #n; Q }}}; - rand_presample_spec {L: randG Σ} N E ns α (tb:nat) - (ε2 : list (fin (S tb)) -> R) - (P : iProp Σ) num T γ2 (ε:R) : + {{{ (n:nat), RET #n; ∃ ns, Q n ns}}}; + rand_presample_spec {L: randG Σ} N E (P : iProp Σ) T γ2 : ↑N ⊆ E -> - (∀ l, length l = num -> 0<= ε2 l)%R -> - (SeriesC (λ l, if bool_decide (l ∈ enum_uniform_fin_list tb num) then ε2 l else 0) /((S tb)^num) <= ε)%R-> is_rand (L:=L) N γ2 -∗ - (□ (P ={E∖↑N, ∅}=∗ ↯ ε ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns) ∗ + (□ (P ={E∖↑N, ∅}=∗ + ∃ ε num tb (ε2 : list (fin (S tb)) -> R) α ns, + ↯ ε ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns) ∗ + ⌜(∀ l, length l = num -> 0<= ε2 l)%R⌝ ∗ + ⌜(SeriesC (λ l, if bool_decide (l ∈ enum_uniform_fin_list tb num) then ε2 l else 0) /((S tb)^num) <= ε)%R⌝ ∗ (∀ ns', ⌜length ns' = num⌝ ∗ ↯ (ε2 ns') ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns ++ (fin_to_nat <$> ns')) - ={∅, E∖↑N}=∗ T ns'))) + ={∅, E∖↑N}=∗ T ε num tb ε2 α ns ns'))) -∗ P -∗ - wp_update E (∃ n, T n) + wp_update E (∃ ε num tb ε2 α ns ns', T ε num tb ε2 α ns ns') }. Section impl. @@ -147,34 +147,34 @@ Section impl. by iFrame. Qed. Next Obligation. - simpl. - iIntros (????????????? Φ) "(#Hinv & #Hvs & HP) HΦ". - wp_pures. - wp_bind (rand(_) _)%E. - iInv "Hinv" as ">(%&H3&H4)" "Hclose". - iMod ("Hvs" with "[$]") as "([Hfrag %] & Hrest)". - iDestruct (hocap_tapes_agree with "[$][$]") as "%". - iDestruct (big_sepM_insert_acc with "[$]") as "[Htape H3]"; first done. - simpl. - wp_apply (wp_rand_tape with "[$]") as "[Htape %]". - iMod (hocap_tapes_update with "[$][$]") as "[? Hfrag]". - iMod ("Hrest" with "[$Hfrag]") as "HQ". - - iPureIntro. by eapply Forall_inv_tail. - - iModIntro. - iMod ("Hclose" with "[- HQ HΦ]") as "_". - { iExists (<[α:=_]> m). - iFrame. - iApply "H3". by iNext. + simpl. + iIntros (??????????? Φ) "(#Hinv & #Hvs & HP) HΦ". + wp_pures. + wp_bind (rand(_) _)%E. + iInv "Hinv" as ">(%&H3&H4)" "Hclose". + iMod ("Hvs" with "[$]") as "(%n & %ns & [Hfrag %] & Hrest)". + iDestruct (hocap_tapes_agree with "[$][$]") as "%". + iDestruct (big_sepM_insert_acc with "[$]") as "[Htape H3]"; first done. + simpl. + wp_apply (wp_rand_tape with "[$]") as "[Htape %]". + iMod (hocap_tapes_update with "[$][$]") as "[? Hfrag]". + iMod ("Hrest" with "[$Hfrag]") as "HQ". + - iPureIntro. by eapply Forall_inv_tail. + - iModIntro. + iMod ("Hclose" with "[- HQ HΦ]") as "_". + { iExists (<[α:=_]> m). + iFrame. + iApply "H3". by iNext. } - by iApply "HΦ". -Qed. -Next Obligation. - simpl. - iIntros (?????????????? Hsubset Hpos Hineq) "#Hinv #Hvs HP ". + iApply "HΦ". by iFrame. + Qed. + Next Obligation. + simpl. + iIntros (?????????) "#Hinv #Hvs HP ". iApply wp_update_state_step_coupl. iIntros (σ1 ε_supply) "((Hheap&Htapes)&Hε)". iMod (inv_acc with "Hinv") as "[>(% & H3 & H4 ) Hclose]"; [done|]. - iMod ("Hvs" with "[$]") as "(Herr & [Hfrag %] & Hrest)". + iMod ("Hvs" with "[$]") as "(%err & %num & %tb & %ε2 & %α & %ns & Herr & [Hfrag %] & %Hpos & %Hineq & Hrest)". iDestruct (hocap_tapes_agree with "[$][$]") as "%". iDestruct (big_sepM_insert_acc with "[$]") as "[Htape H3]"; first done. iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%Heq)". @@ -240,7 +240,7 @@ Section checks. {{{ RET #(LitInt n); rand_tapes_frag (L:=L) γ1 α (N, ns) ∗ ⌜n <= N⌝ }}}. Proof. iIntros (Hsubset Φ) "(#Hinv &>Hfrag) HΦ". - wp_apply (rand_tape_spec_some _ _ _ _ (⌜n<=N⌝ ∗ rand_tapes_frag _ _ _)%I with "[Hfrag]"); first exact. + wp_apply (rand_tape_spec_some _ _ _ _ (λ n' ns', ⌜n=n'/\ns=ns'⌝ ∗ ⌜n<=N⌝ ∗ rand_tapes_frag _ _ _)%I with "[Hfrag]"); first exact. - iSplit; first done. iSplit; last iApply "Hfrag". iModIntro. iIntros "Hfrag". iDestruct (rand_tapes_valid with "[$]") as "%H'". @@ -252,10 +252,11 @@ Section checks. iModIntro. iPureIntro. rewrite Forall_cons in H'. naive_solver. - - iIntros "[??]". iApply "HΦ". - iFrame. + - iIntros (?) "(%&[-> ->]&%&?)". iApply "HΦ". + by iFrame. Qed. + Local Opaque enum_uniform_fin_list. Lemma wp_presample_adv_comp_rand_tape (N : nat) NS E α ns (ε1 : R) (ε2 : fin (S N) -> R) γ1: ↑NS ⊆ E -> (∀ n, 0<=ε2 n)%R -> @@ -268,43 +269,52 @@ Section checks. iIntros (Hsubset Hpos Hineq) "#Hinv >Htape Herr". iDestruct (ec_valid with "[$]") as "%Hpos'". destruct Hpos' as [Hpos' ?]. - iMod (rand_presample_spec _ _ _ _ _ (λ l, match l with - | [x] => ε2 x - | _ => 1%R - end - ) - (rand_tapes_frag (L:=L) γ1 α (N, ns) ∗ ↯ ε1) 1%nat - (λ ls, ∃ n, ⌜ls=[n]⌝ ∗ ↯ (ε2 n) ∗ rand_tapes_frag γ1 α (N, ns ++ [fin_to_nat n]))%I - _ (mknonnegreal ε1 Hpos') - with "[//][][$Htape $Herr]") as "(%l&%sample & -> & Herr &Htape)". + iMod (rand_presample_spec _ _ + (rand_tapes_frag (L:=L) γ1 α (N, ns) ∗ ↯ ε1) + (λ ε' (num':nat) tb' ε2' α' ns1 ns2, + ⌜ε1=ε'⌝ ∗ ⌜(1=num')%nat⌝ ∗ ⌜N=tb'⌝ ∗ + ⌜∀ x y, fin_to_nat <$> x = fin_to_nat <$> y -> + ε2' x = (λ l, match l with |[x] => ε2 x | _ => 1%R end) y⌝∗ ⌜α=α'⌝ ∗ ⌜ns1=ns⌝ ∗ + ∃ (n:fin (S N)), ⌜fin_to_nat <$> ns2=[fin_to_nat n]⌝ ∗ ↯ (ε2 n) ∗ rand_tapes_frag γ1 α (N, ns ++ [fin_to_nat n]))%I + with "[//][][$Htape $Herr]") as "(%&%&%&%&%&%&%&->&<-&->&%&->&->&%&%&?&?)". - done. - - by intros [|?[|]]. - - etrans; last eapply Hineq. - etrans; last eapply (SeriesC_le_inj _ (λ l, match l with |[x] => Some x | _ => None end)). - + rewrite Rdiv_def -SeriesC_scal_r. apply Req_le_sym. - apply SeriesC_ext. - intros. case_match; subst. - * rewrite bool_decide_eq_false_2; first (simpl;lra). - by rewrite elem_of_enum_uniform_fin_list. - * case_match; last first. - { rewrite bool_decide_eq_false_2; first (simpl;lra). - by rewrite elem_of_enum_uniform_fin_list. } - rewrite bool_decide_eq_true_2; last by apply elem_of_enum_uniform_fin_list. - simpl. - rewrite Rdiv_def Rmult_1_r; lra. - + intros. apply Rmult_le_pos; last done. - apply Rdiv_INR_ge_0. - + intros. repeat case_match; by simplify_eq. - + apply ex_seriesC_finite. - iModIntro. - iIntros "(?&?)". - simpl. iFrame. + iIntros "[Hfrag Herr]". + iFrame. iApply fupd_mask_intro; first set_solver. iIntros "Hclose". - iIntros ([|?[|]]) "(%&?&?)"; try done. - iMod "Hclose". - iFrame. - by iModIntro. + iExists 1, (λ l, match l with |[x] => ε2 x | _ => 1%R end). simpl. + repeat iSplit. + + iPureIntro. by intros [|?[|]]. + + iPureIntro. etrans; last eapply Hineq. + etrans; last eapply (SeriesC_le_inj _ (λ l, match l with |[x] => Some x | _ => None end)). + * rewrite Rdiv_def -SeriesC_scal_r. apply Req_le_sym. + apply SeriesC_ext. + intros. case_match; subst. + -- rewrite bool_decide_eq_false_2; first (simpl;lra). + by rewrite elem_of_enum_uniform_fin_list. + -- case_match; last first. + { rewrite bool_decide_eq_false_2; first (simpl;lra). + subst. + by rewrite elem_of_enum_uniform_fin_list. + } + rewrite bool_decide_eq_true_2; last by apply elem_of_enum_uniform_fin_list. + simpl. + rewrite Rdiv_def Rmult_1_r; lra. + * intros. apply Rmult_le_pos; last done. + apply Rdiv_INR_ge_0. + * intros. repeat case_match; by simplify_eq. + * apply ex_seriesC_finite. + + + iIntros ([|?[|]]) "(%&?&?)"; try done. + iFrame. + iMod "Hclose". + iModIntro. + repeat iSplit; try done. + iPureIntro. + intros x y H'. + apply list_fmap_eq_inj in H'; first by simplify_eq. + apply fin_to_nat_inj. - iModIntro. iFrame. Qed.