From d2d6f4f1e2fe461e65eb5010a114bbdc748bd27e Mon Sep 17 00:00:00 2001 From: Hei Li Date: Wed, 25 Sep 2024 15:27:54 +0200 Subject: [PATCH] FLIP --- theories/coneris/lib/flip_spec.v | 431 ------------------------------ theories/coneris/lib/hocap_flip.v | 254 ++++++++++++++++++ theories/coneris/lib/hocap_rand.v | 53 ++-- 3 files changed, 278 insertions(+), 460 deletions(-) delete mode 100644 theories/coneris/lib/flip_spec.v create mode 100644 theories/coneris/lib/hocap_flip.v diff --git a/theories/coneris/lib/flip_spec.v b/theories/coneris/lib/flip_spec.v deleted file mode 100644 index c5f1bd71..00000000 --- a/theories/coneris/lib/flip_spec.v +++ /dev/null @@ -1,431 +0,0 @@ -(* From clutch.coneris Require Import coneris. *) -(* From clutch.coneris Require Import flip hocap. *) - -(* Set Default Proof Using "Type*". *) - -(* Class flip_spec `{!conerisGS Σ} := FlipSpec *) -(* { *) -(* (** * Operations *) *) -(* flip_allocate_tape : val; *) -(* flip_tape : val; *) -(* (** * Ghost state *) *) -(* (** The assumptions about [Σ] *) *) -(* flipG : gFunctors → Type; *) -(* (** [name] is used to associate [locked] with [is_lock] *) *) -(* flip_error_name : Type; *) -(* flip_tape_name: Type; *) -(* (** * Predicates *) *) -(* is_flip {L : flipG Σ} (N:namespace) *) -(* (γ1: flip_error_name) (γ2: flip_tape_name): iProp Σ; *) -(* flip_error_auth {L : flipG Σ} (γ: flip_error_name) (x:R): iProp Σ; *) -(* flip_error_frag {L : flipG Σ} (γ: flip_error_name) (x:R): iProp Σ; *) -(* flip_tapes_auth {L : flipG Σ} (γ: flip_tape_name) (m:gmap loc (list bool)): iProp Σ; *) -(* flip_tapes_frag {L : flipG Σ} (γ: flip_tape_name) (α:loc) (ns:list bool): iProp Σ; *) -(* (** * General properties of the predicates *) *) -(* #[global] is_flip_persistent {L : flipG Σ} N γ1 γ2 :: *) -(* Persistent (is_flip (L:=L) N γ1 γ2); *) -(* #[global] flip_error_auth_timeless {L : flipG Σ} γ x :: *) -(* Timeless (flip_error_auth (L:=L) γ x); *) -(* #[global] flip_error_frag_timeless {L : flipG Σ} γ x :: *) -(* Timeless (flip_error_frag (L:=L) γ x); *) -(* #[global] flip_tapes_auth_timeless {L : flipG Σ} γ m :: *) -(* Timeless (flip_tapes_auth (L:=L) γ m); *) -(* #[global] flip_tapes_frag_timeless {L : flipG Σ} γ α ns :: *) -(* Timeless (flip_tapes_frag (L:=L) γ α ns); *) -(* #[global] flip_error_name_inhabited:: *) -(* Inhabited flip_error_name; *) -(* #[global] flip_tape_name_inhabited:: *) -(* Inhabited flip_tape_name; *) - -(* flip_error_auth_exclusive {L : flipG Σ} γ x1 x2: *) -(* flip_error_auth (L:=L) γ x1 -∗ flip_error_auth (L:=L) γ x2 -∗ False; *) -(* flip_error_frag_split {L : flipG Σ} γ (x1 x2:nonnegreal): *) -(* flip_error_frag (L:=L) γ x1 ∗ flip_error_frag (L:=L) γ x2 ⊣⊢ *) -(* flip_error_frag (L:=L) γ (x1+x2)%R ; *) -(* flip_error_auth_valid {L : flipG Σ} γ x: *) -(* flip_error_auth (L:=L) γ x -∗ ⌜(0<=x<1)%R⌝; *) -(* flip_error_frag_valid {L : flipG Σ} γ x: *) -(* flip_error_frag (L:=L) γ x -∗ ⌜(0<=x<1)%R⌝; *) -(* flip_error_ineq {L : flipG Σ} γ x1 x2: *) -(* flip_error_auth (L:=L) γ x1 -∗ flip_error_frag (L:=L) γ x2 -∗ ⌜(x2 <= x1)%R ⌝; *) -(* flip_error_decrease {L : flipG Σ} γ (x1 x2:nonnegreal): *) -(* flip_error_auth (L:=L) γ (x1 + x2)%NNR -∗ flip_error_frag (L:=L) γ x1 ==∗ flip_error_auth (L:=L) γ x2; *) -(* flip_error_increase {L : flipG Σ} γ (x1 x2:nonnegreal): *) -(* (x1+x2<1)%R -> ⊢ flip_error_auth (L:=L) γ x1 ==∗ *) -(* flip_error_auth (L:=L) γ (x1+x2) ∗ flip_error_frag (L:=L) γ x2; *) - -(* flip_tapes_auth_exclusive {L : flipG Σ} γ m m': *) -(* flip_tapes_auth (L:=L) γ m -∗ flip_tapes_auth (L:=L) γ m' -∗ False; *) -(* flip_tapes_frag_exclusive {L : flipG Σ} γ α ns ns': *) -(* flip_tapes_frag (L:=L) γ α ns -∗ flip_tapes_frag (L:=L) γ α ns' -∗ False; *) -(* flip_tapes_agree {L : flipG Σ} γ α m ns: *) -(* flip_tapes_auth (L:=L) γ m -∗ flip_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝; *) -(* flip_tapes_update {L : flipG Σ} γ α m ns n: *) -(* flip_tapes_auth (L:=L) γ m -∗ flip_tapes_frag (L:=L) γ α ns ==∗ *) -(* flip_tapes_auth (L:=L) γ (<[α := (ns ++[n])]> m) ∗ flip_tapes_frag (L:=L) γ α (ns ++ [n]); *) -(* flip_tapes_pop {L : flipG Σ} γ α m ns n: *) -(* flip_tapes_auth (L:=L) γ m -∗ flip_tapes_frag (L:=L) γ α (n::ns) ==∗ *) -(* flip_tapes_auth (L:=L) γ (<[α := (ns)]> m) ∗ flip_tapes_frag (L:=L) γ α (ns); *) - -(* (** * Program specs *) *) -(* flip_inv_create_spec {L : flipG Σ} N E ε: *) -(* ↯ ε -∗ *) -(* wp_update E (∃ γ1 γ2, is_flip (L:=L) N γ1 γ2 ∗ *) -(* flip_error_frag (L:=L) γ1 ε); *) - -(* flip_allocate_tape_spec {L: flipG Σ} N E γ1 γ2: *) -(* ↑N ⊆ E-> *) -(* {{{ is_flip (L:=L) N γ1 γ2 }}} *) -(* flip_allocate_tape #() @ E *) -(* {{{ (v:val), RET v; *) -(* ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ flip_tapes_frag (L:=L) γ2 α [] *) -(* }}}; *) -(* flip_tape_spec_some {L: flipG Σ} N E γ1 γ2 (P: iProp Σ) (Q:iProp Σ) (α:loc) (n:bool) ns: *) -(* ↑N⊆E -> *) -(* {{{ is_flip (L:=L) N γ1 γ2 ∗ *) -(* □ (∀ m, P ∗ *) -(* flip_tapes_auth (L:=L) γ2 m *) -(* ={E∖↑N}=∗ ⌜m!!α=Some (n::ns)⌝ ∗ Q ∗ flip_tapes_auth (L:=L) γ2 (<[α:=ns]> m)) ∗ *) -(* P *) -(* }}} *) -(* flip_tape #lbl:α @ E *) -(* {{{ RET #n; Q }}}; *) -(* flip_presample_spec {L: flipG Σ} NS E ns α *) -(* (ε2 : R -> list bool -> R) *) -(* (P : _ -> iProp Σ) num T γ1 γ2 ε: *) -(* ↑NS ⊆ E -> *) -(* (∀ ε l, 0<= ε -> length l = num -> 0<=ε2 ε l)%R -> *) -(* (∀ (ε:R), 0<= ε -> SeriesC (λ l, if length l =? num then ε2 ε l else 0) /(2^num) <= ε)%R-> *) -(* is_flip (L:=L) NS γ1 γ2 -∗ *) -(* (□∀ (ε ε':nonnegreal) n, (P ε ∗ flip_error_auth (L:=L) γ1 (ε + ε')%R) ={E∖↑NS}=∗ *) -(* (⌜(1<=ε2 ε n)%R⌝ ∨ (flip_error_auth (L:=L) γ1 (ε2 ε n + ε')%R ∗ T ε n))) *) -(* -∗ *) -(* P ε -∗ flip_tapes_frag (L:=L) γ2 α ns-∗ *) -(* wp_update E (∃ n, T ε n ∗ flip_tapes_frag (L:=L) γ2 α (ns++n)) *) -(* }. *) - -(* Section test. *) -(* Context `{F:flip_spec}. *) -(* Lemma flip_presample_spec_simple {L: flipG Σ} NS E ns α *) -(* (ε2 : R -> bool -> R) *) -(* (P : iProp Σ) T γ1 γ2: *) -(* ↑NS ⊆ E -> *) -(* (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> *) -(* (∀ (ε:R), 0<= ε -> (ε2 ε true + ε2 ε false)/2 <= ε)%R-> *) -(* is_flip (L:=L) NS γ1 γ2 -∗ *) -(* (□∀ (ε:R) n, (P ∗ flip_error_auth (L:=L) γ1 ε) ={E∖↑NS}=∗ *) -(* (⌜(1<=ε2 ε n)%R⌝ ∨ (flip_error_auth (L:=L) γ1 (ε2 ε n) ∗ T (n)))) *) -(* -∗ *) -(* P -∗ flip_tapes_frag (L:=L) γ2 α ns-∗ *) -(* wp_update E (∃ n, T (n) ∗ flip_tapes_frag (L:=L) γ2 α (ns++[n])). *) -(* Proof. *) -(* iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". *) -(* pose (ε2' ε l:= match l with *) -(* | [b]=> ε2 ε b *) -(* | _ => 1%R *) -(* end *) -(* ). *) -(* iMod (flip_presample_spec _ _ _ _ ε2' P 1%nat (λ l, match l with | [b] => T b | _ => False end )%I with "[//][][$][$]") as "(%l & [??])"; first done. *) -(* - rewrite /ε2'. *) -(* intros. repeat case_match; try done. naive_solver. *) -(* - intros. *) -(* etrans; last apply Hineq; try done. *) -(* erewrite (SeriesC_subset (λ x, x ∈ [[true]; [false]])); last first. *) -(* + intros ? H'. *) -(* case_match eqn:K; last done. *) -(* rewrite Nat.eqb_eq in K. *) -(* exfalso. *) -(* apply H'. *) -(* destruct a as [|[|] [|]]; try (simpl in *; done). *) -(* all: set_solver. *) -(* + rewrite SeriesC_list; last first. *) -(* { rewrite !NoDup_cons; repeat split; last apply NoDup_nil; set_solver. } *) -(* simpl. lra. *) -(* - iModIntro. iIntros (ε n) "?". *) -(* destruct n as [|b [|]]. *) -(* + iLeft. iPureIntro. *) -(* by rewrite /ε2'. *) -(* + iMod ("Hvs" $! ε b with "[$]") as "[% | ?]". *) -(* * iLeft. iPureIntro. by rewrite /ε2'. *) -(* * iRight. by rewrite /ε2'. *) -(* + iLeft. iPureIntro. *) -(* by rewrite /ε2'. *) -(* - repeat case_match; try done. *) -(* iModIntro. *) -(* iFrame. *) -(* Qed. *) -(* End test. *) - - -(* (** Instantiate flip *) *) -(* Class flipG1 Σ := FlipG1 { flipG1_error::hocap_errorGS Σ; *) -(* flipG1_tapes:: hocap_tapesGS Σ; *) -(* }. *) -(* Local Definition flip_inv_pred1 `{!conerisGS Σ, !hocap_errorGS Σ, !hocap_tapesGS Σ} γ1 γ2:= *) -(* (∃ (ε:R) (m:gmap loc (list bool)) , *) -(* ↯ ε ∗ ●↯ ε @ γ1 ∗ *) -(* ([∗ map] α ↦ t ∈ ((λ (ns:list bool), (1%nat, bool_to_nat<$>ns))<$>m), α ↪N ( t.1 ; t.2 )) ∗ *) -(* ●(((λ (ns:list bool), (1, bool_to_nat<$>ns))<$>m):gmap _ _)@γ2 *) -(* )%I. *) - -(* #[local] Program Definition flip_spec1 `{!conerisGS Σ}: flip_spec := *) -(* {| flip_allocate_tape:= (λ: <>, allocB); *) -(* flip_tape:= flipL; *) -(* flipG := flipG1; *) -(* flip_error_name := gname; *) -(* flip_tape_name := gname; *) -(* is_flip _ N γ1 γ2 := inv N (flip_inv_pred1 γ1 γ2); *) -(* flip_error_auth _ γ x := ●↯ x @ γ; *) -(* flip_error_frag _ γ x := ◯↯ x @ γ; *) -(* flip_tapes_auth _ γ m := (●((λ ns, (1, bool_to_nat<$>ns))<$>m)@γ)%I; *) -(* flip_tapes_frag _ γ α ns := (α◯↪N (1%nat;bool_to_nat<$> ns) @ γ)%I; *) -(* |}. *) - -(* Next Obligation. *) -(* simpl. *) -(* iIntros. *) -(* iApply (hocap_error_auth_exclusive with "[$][$]"). *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros. *) -(* iApply (hocap_error_frag_split). *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (?????) "H". *) -(* iApply (hocap_error_auth_valid with "[$]"). *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (?????) "H". *) -(* iApply (hocap_error_frag_valid with "[$]"). *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (??????) "H1 H2". *) -(* iApply (hocap_error_ineq with "[$][$]"). *) -(* Qed. *) -(* Next Obligation. *) -(* iIntros. *) -(* iApply (hocap_error_decrease with "[$][$]"). *) -(* Qed. *) -(* Next Obligation. *) -(* iIntros. *) -(* by iApply (hocap_error_increase with "[$]"). *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (??????) "H1 H2". *) -(* by iDestruct (ghost_map_auth_valid_2 with "[$][$]") as "[%H _]". *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (???????) "H1 H2". *) -(* iDestruct (ghost_map_elem_frac_ne with "[$][$]") as "%"; last done. *) -(* rewrite dfrac_op_own dfrac_valid_own. by intro. *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros. *) -(* iDestruct (hocap_tapes_agree with "[$][$]") as "%H". *) -(* iPureIntro. *) -(* rewrite lookup_fmap_Some in H. destruct H as (?&?&K). *) -(* simplify_eq. *) -(* rewrite K. *) -(* f_equal. *) -(* eapply fmap_inj; last done. *) -(* intros [][]?; by simplify_eq. *) -(* Qed. *) -(* Next Obligation. *) -(* iIntros. *) -(* iMod (hocap_tapes_presample with "[$][$]") as "[??]". *) -(* iModIntro. iFrame. *) -(* rewrite fmap_insert. *) -(* rewrite fmap_app; iFrame. *) -(* Qed. *) -(* Next Obligation. *) -(* iIntros. *) -(* iMod (hocap_tapes_pop with "[$][$]") as "[??]". *) -(* iModIntro. iFrame. *) -(* rewrite fmap_insert. *) -(* iFrame. *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (????? ε) "H1". *) -(* iApply fupd_wp_update. *) -(* iApply wp_update_ret. *) -(* iDestruct (ec_valid with "[$]") as "%". *) -(* unshelve iMod (hocap_error_alloc (mknonnegreal ε _)) as "(%γ1 & H2 & H3)"; simpl; [naive_solver..|]. *) -(* simpl. *) -(* iMod (hocap_tapes_alloc ∅) as "(%γ2 & H4 & H5)". *) -(* iMod (inv_alloc _ _ (flip_inv_pred1 γ1 γ2) with "[H1 H2 H4]"). *) -(* { iFrame. iNext. iExists ∅. *) -(* iFrame. *) -(* by rewrite fmap_empty. *) -(* } *) -(* by iFrame. *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (???????? Φ) "#Hinv HΦ". *) -(* wp_pures. *) -(* rewrite /allocB. *) -(* iInv "Hinv" as "(%&%&?&?&?&?)" "Hclose". *) -(* wp_apply (wp_alloc_tape); first done. *) -(* iIntros (α) "Hα". *) -(* iDestruct (hocap_tapes_notin with "[$][$]") as "%". *) -(* iMod (hocap_tapes_new _ _ α 1%nat [] with "[$]") as "[?H]"; first done. *) -(* iMod ("Hclose" with "[-H HΦ]"). *) -(* { iModIntro. *) -(* iExists _, (<[α:=([])]> m). *) -(* iFrame. *) -(* rewrite fmap_insert. *) -(* rewrite big_sepM_insert; [iFrame|done]. *) -(* } *) -(* iApply "HΦ". *) -(* by iFrame. *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (????????????? Φ) "(#Hinv & #Hvs & HP) HΦ". *) -(* rewrite /flipL. *) -(* wp_pures. *) -(* wp_bind (rand(_) _)%E. *) -(* iInv "Hinv" as ">(%&%&?&?&H3&?)" "Hclose". *) -(* iMod ("Hvs" with "[$]") as "(%&HQ&Hauth)". *) -(* erewrite <-(insert_delete m) at 1; last done. *) -(* rewrite fmap_insert. *) -(* rewrite big_sepM_insert; last first. *) -(* { rewrite fmap_delete. apply lookup_delete. } *) -(* iDestruct "H3" as "[Htape H3]". *) -(* simpl. *) -(* wp_apply (wp_rand_tape with "[$]") as "[Htape %]". *) -(* iMod ("Hclose" with "[- HΦ HQ]") as "_". *) -(* { iExists _, (<[α:=ns]> m). *) -(* iFrame. *) -(* rewrite <-(insert_delete m) at 2; last done. *) -(* rewrite insert_insert fmap_insert. *) -(* rewrite big_sepM_insert; first iFrame. *) -(* rewrite fmap_delete. *) -(* apply lookup_delete. *) -(* } *) -(* iModIntro. *) -(* wp_apply conversion.wp_int_to_bool as "_"; first done. *) -(* replace (Z_to_bool _) with n. *) -(* - iApply "HΦ"; iFrame. *) -(* - destruct n; simpl. *) -(* + rewrite Z_to_bool_neq_0; [done|lia]. *) -(* + by rewrite Z_to_bool_eq_0. *) -(* Qed. *) -(* Next Obligation. *) -(* simpl. *) -(* iIntros (????????????? Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". *) -(* iApply wp_update_state_step_coupl. *) -(* iIntros (σ ε) "((Hheap&Htapes)&Hε)". *) -(* iMod (inv_acc with "Hinv") as "[>(% & % & H1 & H2 & H3 & H4 ) Hclose]"; [done|]. *) -(* iDestruct (hocap_tapes_agree with "[$][$]") as "%K". *) -(* rewrite lookup_fmap_Some in K. destruct K as (?&M&?). *) -(* simplify_eq. *) -(* unshelve epose proof fmap_inj _ _ _ _ M as ->. *) -(* { intros [][]?; by simplify_eq. } *) -(* erewrite <-(insert_delete m) at 1; last done. *) -(* rewrite fmap_insert. *) -(* rewrite big_sepM_insert; last first. *) -(* { rewrite fmap_delete. apply lookup_delete. } *) -(* simpl. *) -(* iDestruct "H3" as "[Htape H3]". *) -(* iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%Heq)". *) -(* iDestruct (ec_supply_bound with "[$][$]") as "%". *) -(* iMod (ec_supply_decrease with "[$][$]") as (ε1' ε_rem -> Hε1') "Hε_supply". subst. *) -(* iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'". *) -(* assert (∀ (x: list (fin (2))), bool_to_nat <$> (nat_to_bool <$> (fin_to_nat <$> x)) = fin_to_nat <$> x) as Hrewrite. *) -(* { intros l. *) -(* rewrite -list_fmap_compose. *) -(* rewrite <-list_fmap_id. *) -(* apply list_fmap_ext. *) -(* intros ?? K. simpl. rewrite nat_to_bool_to_nat; first done. *) -(* apply list_lookup_fmap_inv in K as (x'&->&?). *) -(* pose proof fin_to_nat_lt x'. lia. } *) -(* iApply (state_step_coupl_iterM_state_adv_comp_con_prob_lang num α); first done. *) -(* unshelve iExists (λ x, mknonnegreal (if length x =? num then ε2 ε1' (nat_to_bool <$> (fin_to_nat <$> x)) else 1) _). *) -(* { case_match; last (simpl;lra). apply Hpos; first apply cond_nonneg. *) -(* rewrite !fmap_length. *) -(* by apply Nat.eqb_eq. *) -(* } *) -(* iSplit. *) -(* { iPureIntro. *) -(* simpl. *) -(* unshelve epose proof (Hineq ε1' _) as H'; first apply cond_nonneg. *) -(* etrans; last exact. *) -(* rewrite (Rdiv_def _ (2^_)) -SeriesC_scal_r. *) -(* etrans; last eapply (SeriesC_le_inj _ (λ x, Some (nat_to_bool <$> (fin_to_nat <$> x)))). *) -(* - apply SeriesC_le. *) -(* + simpl. intros n. *) -(* rewrite !fmap_length. *) -(* case_match. *) -(* * replace (1+1)%R with 2%R by lra. *) -(* rewrite -Rdiv_1_l. simpl. *) -(* split; last lra. *) -(* apply Rmult_le_pos. *) -(* -- apply Rcomplements.Rdiv_le_0_compat; first lra. *) -(* apply pow_lt; lra. *) -(* -- apply Hpos; first done. *) -(* rewrite !fmap_length. *) -(* by apply Nat.eqb_eq. *) -(* * lra. *) -(* + simpl. *) -(* apply (ex_seriesC_list_length _ num). *) -(* intros ?. rewrite !fmap_length. *) -(* case_match; last lra. *) -(* intros. by apply Nat.eqb_eq. *) -(* - intros. case_match; last lra. *) -(* apply Rmult_le_pos; first apply Hpos; simpl; auto. *) -(* + by apply Nat.eqb_eq. *) -(* + rewrite -Rdiv_1_l. *) -(* apply Rcomplements.Rdiv_le_0_compat; first lra. *) -(* apply pow_lt; lra. *) -(* - intros ??? <- K. *) -(* simplify_eq. *) -(* rewrite -!list_fmap_compose in K. *) -(* apply list_fmap_eq_inj in K; try done. *) -(* intros x x'. *) -(* repeat (inv_fin x; try intros x); *) -(* repeat (inv_fin x'; try intros x'); done. *) -(* - apply (ex_seriesC_list_length _ num). *) -(* intros ?. *) -(* case_match; last lra. *) -(* intros. by apply Nat.eqb_eq. *) -(* } *) -(* iIntros (sample) "<-". *) -(* destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' (nat_to_bool <$> (fin_to_nat <$> sample))))%R 1%R) as [Hdec|Hdec]; last first. *) -(* { apply Rnot_lt_ge, Rge_le in Hdec. *) -(* iApply state_step_coupl_ret_err_ge_1. *) -(* simpl. simpl in *. rewrite Nat.eqb_refl. lra. *) -(* } *) -(* iApply state_step_coupl_ret. *) -(* unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 ε1' (nat_to_bool <$> (fin_to_nat <$> sample))) _) with "Hε_supply") as "[Hε_supply Hε]". *) -(* { apply Hpos; first apply cond_nonneg. by rewrite !fmap_length. } *) -(* { simpl. done. } *) -(* simpl. *) -(* iMod (tapeN_update_append' _ _ _ _ sample with "[$][Htape]") as "[Htapes Htape]". *) -(* { by erewrite Heq. } *) -(* iMod (hocap_tapes_presample' _ _ _ _ _ (fin_to_nat <$> sample) with "[$][$]") as "[H4 Hfrag]". *) -(* iMod "Hclose'" as "_". *) -(* iMod ("Hvs" with "[$]") as "[%|[H2 HT]]". *) -(* { iExFalso. iApply (ec_contradict with "[$]"). exact. } *) -(* iMod ("Hclose" with "[$Hε $H2 Htape H3 H4]") as "_". *) -(* { iNext. *) -(* iExists (<[α:=(ns ++ (nat_to_bool<$>(fin_to_nat <$> sample)))]>m). *) -(* rewrite fmap_insert. *) -(* rewrite big_sepM_insert_delete Heq/=. *) -(* rewrite fmap_delete. iFrame. *) -(* rewrite fmap_app/=. *) -(* rewrite !Hrewrite. iFrame. *) -(* } *) -(* iApply fupd_mask_intro_subseteq; first set_solver. *) -(* iFrame. rewrite fmap_app/=Hrewrite. iFrame. *) -(* erewrite (nnreal_ext _ _); first done. *) -(* simpl. by rewrite Nat.eqb_refl. *) -(* Qed. *) diff --git a/theories/coneris/lib/hocap_flip.v b/theories/coneris/lib/hocap_flip.v new file mode 100644 index 00000000..68b4db4b --- /dev/null +++ b/theories/coneris/lib/hocap_flip.v @@ -0,0 +1,254 @@ +From clutch.coneris Require Import coneris. +From clutch.coneris Require Import flip hocap hocap_rand. + +Set Default Proof Using "Type*". + +Class flip_spec `{!conerisGS Σ} := FlipSpec +{ + (** * Operations *) + flip_allocate_tape : val; + flip_tape : val; + (** * Ghost state *) + (** The assumptions about [Σ] *) + flipG : gFunctors → Type; + (** [name] is used to associate [locked] with [is_lock] *) + flip_tape_name: Type; + (** * Predicates *) + is_flip {L : flipG Σ} (N:namespace) (γ2: flip_tape_name): iProp Σ; + flip_tapes_auth {L : flipG Σ} (γ: flip_tape_name) (m:gmap loc (list bool)): iProp Σ; + flip_tapes_frag {L : flipG Σ} (γ: flip_tape_name) (α:loc) (ns:list bool): iProp Σ; + (** * General properties of the predicates *) + #[global] is_flip_persistent {L : flipG Σ} N γ1 :: + Persistent (is_flip (L:=L) N γ1); + #[global] flip_tapes_auth_timeless {L : flipG Σ} γ m :: + Timeless (flip_tapes_auth (L:=L) γ m); + #[global] flip_tapes_frag_timeless {L : flipG Σ} γ α ns :: + Timeless (flip_tapes_frag (L:=L) γ α ns); + #[global] flip_tape_name_inhabited:: + Inhabited flip_tape_name; + + flip_tapes_auth_exclusive {L : flipG Σ} γ m m': + flip_tapes_auth (L:=L) γ m -∗ flip_tapes_auth (L:=L) γ m' -∗ False; + flip_tapes_frag_exclusive {L : flipG Σ} γ α ns ns': + flip_tapes_frag (L:=L) γ α ns -∗ flip_tapes_frag (L:=L) γ α ns' -∗ False; + flip_tapes_agree {L : flipG Σ} γ α m ns: + flip_tapes_auth (L:=L) γ m -∗ flip_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝; + flip_tapes_update {L : flipG Σ} γ α m ns ns': + flip_tapes_auth (L:=L) γ m -∗ flip_tapes_frag (L:=L) γ α ns ==∗ + flip_tapes_auth (L:=L) γ (<[α := ns']> m) ∗ flip_tapes_frag (L:=L) γ α ns'; + + (** * Program specs *) + flip_inv_create_spec {L : flipG Σ} N E: + ⊢ wp_update E (∃ γ1, is_flip (L:=L) N γ1); + + flip_allocate_tape_spec {L: flipG Σ} N E γ1: + ↑N ⊆ E-> + {{{ is_flip (L:=L) N γ1 }}} + flip_allocate_tape #() @ E + {{{ (v:val), RET v; + ∃ (α: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: + ↑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 + }}} + flip_tape #lbl:α @ E + {{{ RET #n; Q }}}; + + flip_presample_spec {L: flipG Σ} NS E ns α + (ε2 : list bool -> R) + (P : iProp Σ) num 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 ∗ + (∀ ns', ⌜length ns' = num⌝ ∗ ↯ (ε2 ns') ∗ flip_tapes_frag (L:=L) γ1 α (ns ++ ns') + ={∅, E∖↑NS}=∗ T ns'))) + -∗ + P -∗ + wp_update E (∃ n, T n) +}. + + +(** Instantiate flip *) +Section instantiate_flip. + Context `{H: conerisGS Σ, r1:@rand_spec Σ H}. + (* Class flipG1 Σ := FlipG1 { flipG1_tapes:: hocap_tapesGS Σ}. *) + (* Local Definition flip_inv_pred1 `{!hocap_tapesGS Σ} γ1:= *) + (* (∃ (m:gmap loc (list bool)) , *) + (* ([∗ map] α ↦ t ∈ ((λ (ns:list bool), (1%nat, bool_to_nat<$>ns))<$>m), rand_tapes_auth γ1 α ( t.1 ; t.2 )) ∗ *) + (* ●(((λ (ns:list bool), (1, bool_to_nat<$>ns))<$>m):gmap _ _)@γ2 *) + (* )%I. *) + + #[local] Program Definition flip_spec1 : flip_spec := + {| flip_allocate_tape:= (λ: <>, rand_allocate_tape #1%nat); + flip_tape:= (λ: "α", conversion.int_to_bool (rand_tape "α" #1%nat)); + flipG := randG; + flip_tape_name := rand_tape_name; + is_flip L N γ1 := is_rand (L:=L) N γ1; + flip_tapes_auth L γ m := rand_tapes_auth (L:=L) γ ((λ ns, (1, bool_to_nat<$>ns))<$>m); + flip_tapes_frag L γ α ns := rand_tapes_frag (L:=L) γ α (1, (fmap (FMap:=list_fmap) bool_to_nat ns)); + |}. + Next Obligation. + simpl. + iIntros (????) "H1 H2". + by iDestruct (rand_tapes_auth_exclusive with "[$][$]") as "?". + Qed. + Next Obligation. + simpl. + iIntros (?????) "H1 H2". + by iDestruct (rand_tapes_frag_exclusive with "[$][$]") as "?". + Qed. + Next Obligation. + simpl. + iIntros. + iDestruct (rand_tapes_agree with "[$][$]") as "%H'". + rewrite lookup_fmap_Some in H'. destruct H' as (?&?&K). + simplify_eq. + rewrite K. + iPureIntro. + f_equal. + eapply fmap_inj; last done. + intros [][]?; by simplify_eq. + Qed. + Next Obligation. + iIntros. + iMod (rand_tapes_update with "[$][$]") as "[??]"; last iFrame. + - simpl. + rewrite Forall_fmap. + apply Forall_true. + simpl. + intros []; simpl; lia. + - iModIntro. + rewrite fmap_insert; iFrame. + Qed. + Next Obligation. + simpl. + iIntros (???). + iApply rand_inv_create_spec. + Qed. + Next Obligation. + simpl. + iIntros. + wp_pures. + wp_apply rand_allocate_tape_spec; [exact|done..]. + Qed. + Next Obligation. + simpl. + iIntros (??????? n ? ? Φ) "(#Hinv & #Hvs & HP) HΦ". + wp_pures. + wp_apply (rand_tape_spec_some _ _ _ P Q with "[-HΦ]"); [done|..]. + - iSplit; first done. + iSplitR; last iFrame. + iModIntro. iIntros "HP". + iMod ("Hvs" with "[$]") as "[Hfrag Hvs']". + by iFrame. + - iIntros "HQ". + wp_apply conversion.wp_int_to_bool as "_"; first done. + replace (Z_to_bool _) with n; first by iApply "HΦ". + destruct n; 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|..]. + - intros. apply Hpos. + by rewrite !fmap_length. + - etrans; last exact. + replace 2%R with (INR 2); last (simpl; lra). + rewrite !Rdiv_def. + apply Rmult_le_compat_r. + { rewrite -Rdiv_1_l -pow_INR. apply Rdiv_INR_ge_0. } + etrans; last eapply (SeriesC_le_inj _ (λ l, Some ((λ x, nat_to_bool (fin_to_nat x)) <$> l))). + + apply Req_le_sym. + apply SeriesC_ext. + intros. simpl. rewrite fmap_length. + rewrite elem_of_enum_uniform_fin_list'. case_match; last lra. + rewrite -list_fmap_compose. + f_equal. + + intros. case_match; last lra. + apply Hpos. + by rewrite -Nat.eqb_eq. + + intros ??? H1 H2. + simplify_eq. + apply fmap_inj in H1; first done. + intros x y ?. + repeat (inv_fin x; simpl; try intros x); + by repeat (inv_fin y; simpl; try intros y). + + 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. + Qed. +End instantiate_flip. + +(* Section test. *) +(* Context `{F:flip_spec}. *) +(* Lemma flip_presample_spec_simple {L: flipG Σ} NS E ns α *) +(* (ε2 : R -> bool -> R) *) +(* (P : iProp Σ) T γ1 γ2: *) +(* ↑NS ⊆ E -> *) +(* (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> *) +(* (∀ (ε:R), 0<= ε -> (ε2 ε true + ε2 ε false)/2 <= ε)%R-> *) +(* is_flip (L:=L) NS γ1 γ2 -∗ *) +(* (□∀ (ε:R) n, (P ∗ flip_error_auth (L:=L) γ1 ε) ={E∖↑NS}=∗ *) +(* (⌜(1<=ε2 ε n)%R⌝ ∨ (flip_error_auth (L:=L) γ1 (ε2 ε n) ∗ T (n)))) *) +(* -∗ *) +(* P -∗ flip_tapes_frag (L:=L) γ2 α ns-∗ *) +(* wp_update E (∃ n, T (n) ∗ flip_tapes_frag (L:=L) γ2 α (ns++[n])). *) +(* Proof. *) +(* iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". *) +(* pose (ε2' ε l:= match l with *) +(* | [b]=> ε2 ε b *) +(* | _ => 1%R *) +(* end *) +(* ). *) +(* iMod (flip_presample_spec _ _ _ _ ε2' P 1%nat (λ l, match l with | [b] => T b | _ => False end )%I with "[//][][$][$]") as "(%l & [??])"; first done. *) +(* - rewrite /ε2'. *) +(* intros. repeat case_match; try done. naive_solver. *) +(* - intros. *) +(* etrans; last apply Hineq; try done. *) +(* erewrite (SeriesC_subset (λ x, x ∈ [[true]; [false]])); last first. *) +(* + intros ? H'. *) +(* case_match eqn:K; last done. *) +(* rewrite Nat.eqb_eq in K. *) +(* exfalso. *) +(* apply H'. *) +(* destruct a as [|[|] [|]]; try (simpl in *; done). *) +(* all: set_solver. *) +(* + rewrite SeriesC_list; last first. *) +(* { rewrite !NoDup_cons; repeat split; last apply NoDup_nil; set_solver. } *) +(* simpl. lra. *) +(* - iModIntro. iIntros (ε n) "?". *) +(* destruct n as [|b [|]]. *) +(* + iLeft. iPureIntro. *) +(* by rewrite /ε2'. *) +(* + iMod ("Hvs" $! ε b with "[$]") as "[% | ?]". *) +(* * iLeft. iPureIntro. by rewrite /ε2'. *) +(* * iRight. by rewrite /ε2'. *) +(* + iLeft. iPureIntro. *) +(* by rewrite /ε2'. *) +(* - repeat case_match; try done. *) +(* iModIntro. *) +(* iFrame. *) +(* Qed. *) +(* End test. *) diff --git a/theories/coneris/lib/hocap_rand.v b/theories/coneris/lib/hocap_rand.v index f290bf9c..8b985c73 100644 --- a/theories/coneris/lib/hocap_rand.v +++ b/theories/coneris/lib/hocap_rand.v @@ -55,16 +55,15 @@ Class rand_spec `{!conerisGS Σ} := RandSpec rand_tape_spec_some {L: randG Σ} N E γ2 (P: iProp Σ) (Q:iProp Σ) (α:loc) (n:nat) (tb:nat) ns: ↑N⊆E -> {{{ is_rand (L:=L) N γ2 ∗ - □ (∀ (m:gmap loc (nat * list nat)), P ∗ - rand_tapes_auth (L:=L) γ2 m - ={E∖↑N}=∗ ⌜m!!α=Some (tb, n::ns)⌝ ∗ Q ∗ rand_tapes_auth (L:=L) γ2 (<[α:=(tb, ns)]> m)) ∗ + (□ (P ={E∖↑N, ∅}=∗ rand_tapes_frag (L:=L) γ2 α (tb, n::ns) ∗ + (rand_tapes_frag (L:=L) γ2 α (tb, ns) ={∅, E∖↑N}=∗ Q))) ∗ ▷ 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 (ε:nonnegreal) : + (P : iProp Σ) num T γ2 (ε:R) : ↑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-> @@ -154,16 +153,21 @@ Section impl. wp_pures. wp_bind (rand(_) _)%E. iInv "Hinv" as ">(%&H3&H4)" "Hclose". - iMod ("Hvs" with "[$]") as "(%&HQ&Hauth)". + 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 ("Hclose" with "[- HΦ HQ]") as "_". - { iExists (<[α:=_]> m). - iFrame. - iApply "H3". by iNext. - } - by iApply "HΦ". + 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. @@ -230,16 +234,6 @@ End impl. Section checks. Context `{H: conerisGS Σ, r1:@rand_spec Σ H, L:randG Σ}. - Lemma wp_rand_alloc_tape NS (N:nat) E γ1 : - ↑NS ⊆ E -> - {{{ is_rand (L:=L) NS γ1 }}} rand_allocate_tape #N @ E {{{ α, RET #lbl:α; rand_tapes_frag (L:=L) γ1 α (N,[]) }}}. - Proof. - iIntros (Hsubset Φ) "#Hinv HΦ". - wp_apply (rand_allocate_tape_spec with "[//]"); first exact. - iIntros (?) "(%&->&?)". - by iApply "HΦ". - Qed. - Lemma wp_rand_tape_1 NS (N:nat) E γ1 n ns α: ↑NS ⊆ E -> {{{ is_rand (L:=L) NS γ1 ∗ ▷ rand_tapes_frag (L:=L) γ1 α (N, n :: ns) }}} @@ -249,15 +243,16 @@ Section checks. iIntros (Hsubset Φ) "(#Hinv &>Hfrag) HΦ". wp_apply (rand_tape_spec_some _ _ _ _ (⌜n<=N⌝ ∗ rand_tapes_frag _ _ _)%I with "[Hfrag]"); first exact. - iSplit; first done. iSplit; last iApply "Hfrag". - iModIntro. - iIntros (?) "[Hfrag Hauth]". - iDestruct (rand_tapes_agree with "[$][$]") as "%". - iDestruct (rand_tapes_valid with "[$Hfrag]") as "%K". - inversion K; subst. - iMod (rand_tapes_update _ _ _ _ (N, ns) with "[$][$]") as "[Hauth Hfrag]"; first done. - iFrame "Hauth". iModIntro. + iModIntro. iIntros "Hfrag". + iDestruct (rand_tapes_valid with "[$]") as "%H'". iFrame. - by iPureIntro. + iApply fupd_mask_intro; first set_solver. + iIntros "Hclose Hfrag". + iFrame. + iMod "Hclose". + iModIntro. + iPureIntro. + rewrite Forall_cons in H'. naive_solver. - iIntros "[??]". iApply "HΦ". iFrame. Qed.