diff --git a/theories/coneris/error_rules.v b/theories/coneris/error_rules.v index defd65e9..571f9876 100644 --- a/theories/coneris/error_rules.v +++ b/theories/coneris/error_rules.v @@ -836,7 +836,7 @@ Lemma pgl_iterM_state N p σ α ns: pgl (iterM p (λ σ, state_step σ α) σ) (λ σ', ∃ ns' : list (fin (S N)), - ns' ∈ enum_uniform_list N p ∧ σ' = state_upd_tapes <[α:=(N; ns ++ ns')]> σ) 0. + ns' ∈ enum_uniform_fin_list N p ∧ σ' = state_upd_tapes <[α:=(N; ns ++ ns')]> σ) 0. Proof. intros H. rewrite /pgl. @@ -855,7 +855,7 @@ Proof. rewrite -dunifv_pos in H1. apply H0. exists x. - split; [by apply elem_of_enum_uniform_list|done]. + split; [by apply elem_of_enum_uniform_fin_list|done]. Qed. Lemma state_step_coupl_iterM_state_adv_comp_con_prob_lang (p:nat) α σ1 Z (ε ε_rem: nonnegreal) N ns: @@ -871,11 +871,11 @@ Proof. by apply elem_of_list_In, elem_of_list_In, elem_of_elements, elem_of_dom. } assert (0<=1 / S N ^ p)%R as Hineq. { apply Rcomplements.Rdiv_le_0_compat; first lra. apply pow_lt. apply pos_INR_S. } - (* R: predicate should hold iff tapes σ' at α is ns ++ [nx] where ns is in enum_uniform_list N p *) + (* R: predicate should hold iff tapes σ' at α is ns ++ [nx] where ns is in enum_uniform_fin_list N p *) unshelve iExists - (fun σ' : state => exists ns', ns' ∈ enum_uniform_list N p /\ σ' = (state_upd_tapes <[α:=(_; ns ++ ns') : tape]> σ1)), nnreal_zero, + (fun σ' : state => exists ns', ns' ∈ enum_uniform_fin_list N p /\ σ' = (state_upd_tapes <[α:=(_; ns ++ ns') : tape]> σ1)), nnreal_zero, (fun ρ => (ε_rem + - match ClassicalEpsilon.excluded_middle_informative (exists ns', ns' ∈ enum_uniform_list N p /\ ρ = (state_upd_tapes <[α:=(_; ns ++ ns') : tape]> σ1)) with + match ClassicalEpsilon.excluded_middle_informative (exists ns', ns' ∈ enum_uniform_fin_list N p /\ ρ = (state_upd_tapes <[α:=(_; ns ++ ns') : tape]> σ1)) with | left p => mknonnegreal (ε2 (epsilon p)) _ | _ => nnreal_zero end))%NNR. @@ -893,14 +893,14 @@ Proof. - apply Rlt_gt. apply pow_lt. pose proof pos_INR N; lra. - rewrite -S_INR; simpl in *; lra. } - rewrite elem_of_enum_uniform_list in H1. + rewrite elem_of_enum_uniform_fin_list in H1. etrans; last exact. etrans; last apply (SeriesC_ge_elem _ (epsilon e)). + rewrite S_INR. rewrite H1. by rewrite Nat.eqb_refl. + intros; case_match; last lra. apply Rmult_le_pos; try done. by simpl. - + apply (ex_seriesC_ext (λ n, if bool_decide (n∈enum_uniform_list N p) then (1 / S N ^ p * ε2 n)%R else 0%R)); last apply ex_seriesC_list. - intros. case_bool_decide as H'; rewrite elem_of_enum_uniform_list in H'. + + apply (ex_seriesC_ext (λ n, if bool_decide (n∈enum_uniform_fin_list N p) then (1 / S N ^ p * ε2 n)%R else 0%R)); last apply ex_seriesC_list. + intros. case_bool_decide as H'; rewrite elem_of_enum_uniform_fin_list in H'. * subst. by rewrite Nat.eqb_refl. * rewrite -Nat.eqb_neq in H'. by rewrite H'. - iPureIntro. @@ -912,13 +912,13 @@ Proof. by rewrite dmap_unfold_pmf -SeriesC_scal_r. } rewrite fubini_pos_seriesC'; last first. - + eapply (ex_seriesC_ext (λ a, if bool_decide (a ∈ enum_uniform_list N p) then _ else 0%R)); last apply ex_seriesC_list. + + eapply (ex_seriesC_ext (λ a, if bool_decide (a ∈ enum_uniform_fin_list N p) then _ else 0%R)); last apply ex_seriesC_list. intros n. case_bool_decide as H; first done. rewrite SeriesC_0; first done. intros x. rewrite dunifv_pmf bool_decide_eq_false_2; first lra. - by rewrite -elem_of_enum_uniform_list. + by rewrite -elem_of_enum_uniform_fin_list. + intros a. rewrite dunifv_pmf. eapply (ex_seriesC_ext (λ b, if bool_decide (b=state_upd_tapes <[α:=(N; ns ++ a)]> σ1) then _ else 0%R)); last apply ex_seriesC_singleton_dependent. @@ -927,11 +927,11 @@ Proof. + intros. repeat apply Rmult_le_pos; repeat case_match; simpl; try lra; try done. all: apply Rplus_le_le_0_compat; by try lra. - + erewrite (SeriesC_ext _ (λ n, (if bool_decide (n∈enum_uniform_list N p) then 1 / S N ^ p * ε2 n else 0) + (if bool_decide (n∈enum_uniform_list N p) then 1 / S N ^ p * ε_rem else 0)))%R. + + erewrite (SeriesC_ext _ (λ n, (if bool_decide (n∈enum_uniform_fin_list N p) then 1 / S N ^ p * ε2 n else 0) + (if bool_decide (n∈enum_uniform_fin_list N p) then 1 / S N ^ p * ε_rem else 0)))%R. * rewrite SeriesC_plus; [|apply ex_seriesC_list..]. - rewrite SeriesC_list_2; last apply NoDup_enum_uniform_list. - rewrite enum_uniform_list_length. - setoid_rewrite elem_of_enum_uniform_list'. + rewrite SeriesC_list_2; last apply NoDup_enum_uniform_fin_list. + rewrite enum_uniform_fin_list_length. + setoid_rewrite elem_of_enum_uniform_fin_list'. rewrite Rplus_0_l. rewrite Rplus_comm. apply Rplus_le_compat; last done. rewrite -pow_INR. simpl. @@ -951,7 +951,7 @@ Proof. case_match; last first. { exfalso. apply n. naive_solver. } rewrite dunifv_pmf. - rewrite bool_decide_eq_true_2; last by apply elem_of_enum_uniform_list. + rewrite bool_decide_eq_true_2; last by apply elem_of_enum_uniform_fin_list. rewrite -pow_INR. simpl. pose proof epsilon_correct _ e as H'. simpl in H'. replace (epsilon e) with l; try lra. @@ -962,7 +962,7 @@ Proof. intros. rewrite dunifv_pmf. rewrite bool_decide_eq_false_2; first lra. - by rewrite -elem_of_enum_uniform_list. + by rewrite -elem_of_enum_uniform_fin_list. - simpl. iPureIntro. eapply pgl_mon_pred; last first. @@ -970,7 +970,7 @@ Proof. + done. - iIntros (σ2 [ns' [Helem ->]]). pose proof Helem as Helem'. - rewrite elem_of_enum_uniform_list in Helem. rewrite <- Helem. + rewrite elem_of_enum_uniform_fin_list in Helem. rewrite <- Helem. iMod ("H" with "[]") as "H"; first done. case_match; last first. + (* contradiction *) @@ -1001,16 +1001,16 @@ Proof. * intros. split; repeat case_match; try rewrite S_INR; simpl; try rewrite Rmult_1_r; try lra. all: apply Rmult_le_pos; last done. all: rewrite -S_INR; apply Rdiv_INR_ge_0. - * eapply (ex_seriesC_ext (λ x, if (bool_decide (x∈enum_uniform_list N 1%nat)) then + * eapply (ex_seriesC_ext (λ x, if (bool_decide (x∈enum_uniform_fin_list N 1%nat)) then match x with |[x'] => (1 / S N * ε2 x')%R | _ => 0 end else 0)); last apply ex_seriesC_list. intros [|n[|]]. -- rewrite bool_decide_eq_false_2; first done. - by rewrite elem_of_enum_uniform_list. + by rewrite elem_of_enum_uniform_fin_list. -- rewrite bool_decide_eq_true_2; first done. - by rewrite elem_of_enum_uniform_list. + by rewrite elem_of_enum_uniform_fin_list. -- rewrite bool_decide_eq_false_2; first done. - by rewrite elem_of_enum_uniform_list. + by rewrite elem_of_enum_uniform_fin_list. + intros; apply Rmult_le_pos; last by simpl. apply Rdiv_INR_ge_0. + intros. repeat case_match; by simplify_eq. @@ -1151,6 +1151,46 @@ Qed. iFrame. Qed. + Lemma state_update_presample_exp E α N ns (ε1 : R) (ε2 : fin (S N) → R) : + (∀ n, 0<=ε2 n)%R -> + (SeriesC (λ n, 1 / (S N) * ε2 n)%R <= ε1)%R → + α ↪N (N; ns) -∗ ↯ ε1 -∗ state_update E (∃ n, α ↪N (N; ns ++ [fin_to_nat n]) ∗ ↯ (ε2 n)). + Proof. + rewrite state_update_unseal/state_update_def. + iIntros (Hpos Hsum) "Hα Hε". + iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]". + iDestruct "Hα" as (ns') "(%Hmap & Hα)". + iDestruct (ghost_map_lookup with "Htapes Hα") as "%Hlookup". + iDestruct (ec_supply_bound with "Hε_supply Hε") as %Hε1_ub. + iMod (ec_supply_decrease with "Hε_supply Hε") as (ε1' ε_rem -> Hε1') "Hε_supply". + iApply fupd_mask_intro; [set_solver|]. + iIntros "Hclose". + subst. + iApply (state_step_coupl_state_adv_comp_con_prob_lang); first done. + iExists (λ x, mknonnegreal (ε2 x) _). + iSplit; first done. + iIntros (sample). + destruct (Rlt_decision (ε_rem + (ε2 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 *. lra. + } + unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 sample) _) with "Hε_supply") as "[Hε_supply Hε]"; first done. + { simplify_eq. simpl. done. } + iMod (ghost_map_update ((N; ns' ++ [sample]) : tape) with "Htapes Hα") as "[Htapes Hα]". + (* iSpecialize ("Hwp" $! sample). *) + (* rewrite pgl_wp_unfold /pgl_wp_pre. *) + (* simpl. *) + remember {| heap := heap (σ1); tapes := (<[α:=(N; ns' ++ [sample])]> (tapes σ1)) |} as σ2. + rewrite /=. + iModIntro. + iApply state_step_coupl_ret. + iMod "Hclose". + iFrame. + iPureIntro. rewrite fmap_app; by f_equal. + Qed. + + Lemma wp_couple_empty_tape_adv_comp E α N (ε1 : R) (ε2 : nat → R) : (∀ (n:nat), 0<= ε2 n)%R -> (SeriesC (λ n, if (bool_decide (n≤N)) then 1 / (S N) * ε2 n else 0%R)%R <= ε1)%R → diff --git a/theories/coneris/examples/parallel_add.v b/theories/coneris/examples/parallel_add.v index fd2aa1cd..111c754a 100644 --- a/theories/coneris/examples/parallel_add.v +++ b/theories/coneris/examples/parallel_add.v @@ -239,7 +239,7 @@ Section attempt1. own γ1 (●E b1) ∗ own γ2 (●E b2) ∗ l ↦ #z ∗ ↯ err ∗ ⌜ (nonneg err = 1- Rpower 2%R (INR flip_num-2))%R⌝ ∗ - ⌜(flip_num = bool_to_nat (ssrbool.isSome b1) +bool_to_nat (ssrbool.isSome b2))%nat⌝∗ + ⌜(flip_num = bool_to_nat (ssrbool.isSome b1) +bool_to_nat (ssrbool.isSome b2))%nat⌝∗ ⌜(z = bool_to_Z (is_Some_true b1) + bool_to_Z (is_Some_true b2))%Z⌝ . @@ -314,7 +314,7 @@ Section attempt1. iMod (ghost_var_update' _ (Some true) with "[$Hγ1●][$]") as "[Hγ1● Hγ1◯]". iMod ("Hclose" with "[Hγ1● Hγ2● Hl Herr]") as "_"; last done. iNext. iExists _, _, _, (mknonnegreal _ _ ), _. iFrame; simpl. - repeat iSplit; iPureIntro; [done|done|lia]. + repeat iSplit; iPureIntro; [done|done|lia]. } { rewrite /flipL. wp_pures. @@ -356,7 +356,7 @@ Section attempt1. iMod (ghost_var_update' _ (Some true) with "[$Hγ2●][$]") as "[Hγ2● Hγ2◯]". iMod ("Hclose" with "[Hγ1● Hγ2● Hl Herr]") as "_"; last done. iNext. iExists _, _, _, (mknonnegreal _ _ ), _. iFrame; simpl. - repeat iSplit; iPureIntro; [done|done|lia]. + repeat iSplit; iPureIntro; [done|done|lia]. } iIntros (??) "[Hγ1◯ Hγ2◯]". iNext. wp_pures. @@ -370,7 +370,7 @@ Section attempt1. Unshelve. all: try lra. all: simpl; try apply cond_nonneg. - all: apply resource_nonneg. + all: apply resource_nonneg. Qed. (** This time we use the property of flip being logically atomic *) @@ -435,7 +435,7 @@ Section attempt1. replace 1%R with (INR 1) by done. apply le_INR. rewrite /bool_to_nat; case_match; lia. - } + } destruct b; last first. { iIntros. iExFalso. iApply ec_contradict; last done. simpl. lra. } simpl. @@ -497,7 +497,7 @@ Section attempt1. replace 1%R with (INR 1) by done. apply le_INR. rewrite /bool_to_nat; case_match; lia. - } + } destruct b; last first. { iIntros. iExFalso. iApply ec_contradict; last done. simpl. lra. } simpl. @@ -542,220 +542,220 @@ Section attempt1. Qed. End attempt1. -Section attempt2. - Context `{!conerisGS Σ, !spawnG Σ, !hocap_errorGS Σ, !inG Σ (excl_authR ZR), !inG Σ (excl_authR (optionO boolO))}. (* A hocap style spec for half_FAA*) Definition loc_nroot:=nroot.@"loc". Definition both_nroot:=nroot.@"both". - Definition loc_inv (l:loc) γ:= - inv loc_nroot (∃ (z:Z), l↦#z ∗ own γ (●E z)). - - Lemma wp_half_FAA E - (ε2 : R -> bool -> R) - (P Q : iProp Σ) (T : bool -> iProp Σ) γ1 γ2 (l:loc): - ↑hocap_error_nroot ⊆ E -> - ↑loc_nroot ⊆ E -> - (∀ ε b, 0<= ε -> 0<= ε2 ε b)%R-> - (∀ (ε:R), 0<=ε -> (((ε2 ε true) + (ε2 ε false))/2 <= (ε)))%R → - {{{ error_inv γ1 ∗ loc_inv l γ2 ∗ - □(∀ (ε:R) (b : bool), P ∗ ●↯ ε @ γ1 ={E∖↑hocap_error_nroot}=∗ (⌜(1<=ε2 ε b)%R⌝∨●↯ (ε2 ε b) @ γ1 ∗ T b) ) ∗ - □ (∀ (b:bool) (z:Z), T b ∗ own γ2 (●E z) ={E∖↑loc_nroot}=∗ - if b then own γ2 (●E(z+1)%Z)∗ Q else own γ2 (●E(z))∗ Q ) ∗ - P }}} half_FAA l @ E {{{ (v: val), RET v; Q }}}. - Proof. - iIntros (Hsubset1 Hsubset2 ? Hineq Φ) "(#Hinv1 & #Hinv2 & #Hchange1 & #Hchange2 & HP) HΦ". - rewrite /half_FAA. - wp_apply (wp_hocap_flip_adv_comp _ ε2 P with "[-HΦ]"); [done|..]. - - intros. naive_solver. - - simpl. intros; naive_solver. - - by repeat iSplit. - - iIntros. destruct b. - + wp_pures. iInv "Hinv2" as "(%&?&?)" "Hclose". - wp_faa. - iMod ("Hchange2" with "[$]") as "[??]". - iMod ("Hclose" with "[$]"). - by iApply "HΦ". - + iInv "Hinv2" as "(%&?&?)" "Hclose". - wp_pure. - iMod ("Hchange2" with "[$]") as "[??]". - iMod ("Hclose" with "[$]"). - by iApply "HΦ". - Qed. - - Lemma parallel_add_spec'': - {{{ ↯ (3/4) }}} - parallel_add - {{{ (z:Z), RET #z; ⌜(z=2)⌝ }}}. - Proof. - iIntros (Φ) "Herr HΦ". - rewrite /parallel_add. - wp_alloc l as "Hl". - wp_pures. - rewrite -/(half_FAA l). - (** Allocate hocap error*) - unshelve iMod (hocap_error_alloc (mknonnegreal (3/4) _)) as "(%γ1 & Hεauth & Hεfrag)". - { lra. } - simpl. - (** Allocate hocap heap *) - iMod (own_alloc ((●E 0) ⋅ (◯E 0))) as "[%γ2 [Hauth_loc Hfrag_loc]]". - { by apply excl_auth_valid. } - (** Allocate hocap for tracking contributions *) - iMod (own_alloc ((●E None) ⋅ (◯E None))) as "[%γ3 [Hauth_a Hfrag_a]]". - { by apply excl_auth_valid. } - iMod (own_alloc ((●E None) ⋅ (◯E None))) as "[%γ4 [Hauth_b Hfrag_b]]". - { by apply excl_auth_valid. } - (** Allocate error invariants *) - iMod (inv_alloc hocap_error_nroot _ ((∃ (ε:R), ↯ ε ∗ ●↯ ε @ γ1)) with "[Herr Hεauth]") as "#Hεinv". - { iExists (mknonnegreal (3/4) _); iFrame. - Unshelve. lra. } - (** Allocate location inv *) - iMod (inv_alloc loc_nroot _ (∃ (z:Z), l↦#z ∗ own γ2 (●E z) - ) with "[Hl Hauth_loc]") as "#Hlocinv". - { iFrame. } - iMod (inv_alloc both_nroot _ - (∃ (z:Z) (a b:option bool), own γ2 (◯E z) ∗ - own γ3 (●E a) ∗ - own γ4 (●E b) ∗ - ⌜(z=bool_to_Z (is_Some_true a) + bool_to_Z (is_Some_true b))%Z⌝ ∗ - ◯↯ (1-Rpower 2 (IZR (bool_to_Z (bool_decide (is_Some a)))+IZR (bool_to_Z (bool_decide (is_Some b)))-2))%R@ γ1) - with "[Hfrag_loc Hεfrag Hauth_a Hauth_b]") as "#Hinvboth". - { iFrame. simpl. iModIntro. iSplitR; first by iPureIntro. - replace (1-_)%R with (3/4)%R; first done. - replace (Rpower _ _) with (1/4)%R; try lra. - replace (0+0-2)%R with (-2)%R by lra. - rewrite Rpower_Ropp/ Rpower. replace (IPR 2) with (INR 2); last done. - rewrite -ln_pow; last lra. - rewrite exp_ln; lra. - } - wp_apply (wp_par (λ _, own γ3 (◯E (Some true)))(λ _, own γ4 (◯E (Some true))) with "[Hfrag_a][Hfrag_b]"). - - (* first branch *) - wp_apply (wp_half_FAA _ (λ x b, - match ClassicalEpsilon.excluded_middle_informative (1/2<=x)%R - with - | left P => if b then (2*x - 1)%R else 1%R - | _ => x - end ) (own γ3 (◯E None)) - (own γ3 (◯E (Some true))) - (λ b, ⌜b=true⌝ ∗ (own γ3 (◯E (Some false))))%I γ1 γ2 l with "[$Hfrag_a]"); [done|done|..]. - + intros; repeat case_match; lra. - + intros. case_match; simpl; lra. - + repeat iSplit. - * done. - * done. - * iModIntro. iIntros (ε res) "[Hfrag_a Hεauth]". - iInv both_nroot as ">(%z & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". - iDestruct (hocap_error_agree with "[$][$]") as "%K". - iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". - simpl in *. - case_match; last first. - { exfalso. apply n. - simpl in *. - rewrite K. - assert (Rpower 2 (0+IZR (bool_to_Z (bool_decide (is_Some b))) - 2) <= 1/2)%R; try lra. - replace (_/_)%R with (/2) by lra. - rewrite -{3}(Rpower_1 2); last lra. - rewrite -Rpower_Ropp. - apply Rle_Rpower; first lra. - case_bool_decide; simpl; lra. - } - iMod (ghost_var_update' _ (Some false) with "[$Hauth_a][$]") as "[Hauth_a Hfrag_a]". - iMod (hocap_error_update _ (mknonnegreal _ _)with "[$][$]") as "[Hεauth Hεfrag]". - simpl. - iMod ("Hclose" with "[Hloc_frag Hauth_a Hauth_b Hεfrag]"); iFrame; first done. - simpl. case_match; last first. - { iLeft. done. } - iRight. iFrame. iModIntro; iSplitL; last done. - simpl. rewrite K. - iApply (hocap_error_irrel with "[$]"). - rewrite !Rpower_plus Rpower_O; last lra. - rewrite Rpower_1; lra. - * iModIntro. - iIntros (??) "[[-> Hfrag_a] Hauth_loc]". - iInv both_nroot as ">(% & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". - iDestruct (ghost_var_agreeZ with "[$][$]") as "->". - iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". - iMod (ghost_var_updateZ with "[$][$]") as "[Hauth_loc Hfrag_loc]". - iMod (ghost_var_update' _ (Some true) with "[$Hauth_a][$]") as "[Hauth_a Hfrag_a]". - simpl. - iMod ("Hclose" with "[$Hfrag_loc $Hauth_a $Hauth_b $Hεfrag]") as "_"; first done. - iFrame. simpl. - iModIntro. - replace (0+_+1)%Z with (1+bool_to_Z (is_Some_true b)); [done|lia]. - + iIntros. done. - - (* first branch *) - wp_apply (wp_half_FAA _ (λ x b, - match ClassicalEpsilon.excluded_middle_informative (1/2<=x)%R - with - | left P => if b then (2*x - 1)%R else 1%R - | _ => x - end ) (own γ4 (◯E None)) - (own γ4 (◯E (Some true))) - (λ b, ⌜b=true⌝ ∗ (own γ4 (◯E (Some false))))%I γ1 γ2 l with "[$Hfrag_b]"); [done|done|..]. - + intros; repeat case_match; lra. - + intros. case_match; simpl; lra. - + repeat iSplit. - * done. - * done. - * iModIntro. iIntros (ε res) "[Hfrag_b Hεauth]". - iInv both_nroot as ">(%z & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". - iDestruct (hocap_error_agree with "[$][$]") as "%K". - iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". - simpl in *. - case_match; last first. - { exfalso. apply n. - simpl in *. - rewrite K. - assert (Rpower 2 (IZR (bool_to_Z (bool_decide (is_Some a)))+0 - 2) <= 1/2)%R; try lra. - replace (_/_)%R with (/2) by lra. - rewrite -{3}(Rpower_1 2); last lra. - rewrite -Rpower_Ropp. - apply Rle_Rpower; first lra. - case_bool_decide; simpl; lra. - } - iMod (ghost_var_update' _ (Some false) with "[$Hauth_b][$]") as "[Hauth_b Hfrag_b]". - iMod (hocap_error_update _ (mknonnegreal _ _)with "[$][$]") as "[Hεauth Hεfrag]". - simpl. - iMod ("Hclose" with "[Hloc_frag Hauth_a Hauth_b Hεfrag]"); iFrame; first done. - simpl. case_match; last first. - { iLeft. done. } - iRight. iFrame. iModIntro; iSplitL; last done. - simpl. rewrite K. - iApply (hocap_error_irrel with "[$]"). - rewrite !Rpower_plus Rpower_O; last lra. - rewrite Rpower_1; lra. - * iModIntro. - iIntros (??) "[[-> Hfrag_a] Hauth_loc]". - iInv both_nroot as ">(% & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". - iDestruct (ghost_var_agreeZ with "[$][$]") as "->". - iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". - iMod (ghost_var_updateZ with "[$][$]") as "[Hauth_loc Hfrag_loc]". - iMod (ghost_var_update' _ (Some true) with "[$Hauth_b][$]") as "[Hauth_b Hfrag_b]". - simpl. - iMod ("Hclose" with "[$Hfrag_loc $Hauth_a $Hauth_b $Hεfrag]") as "_"; first done. - iFrame. simpl. - iModIntro. - replace (_+0+1)%Z with (bool_to_Z (is_Some_true a)+1); [done|lia]. - + iIntros. done. - - iIntros (??) "[Hfrag_a Hfrag_b]". iModIntro. wp_pures. - iInv loc_nroot as ">(%&Hl&Hloc_auth)" "Hclose". - iInv both_nroot as ">(%&%&%&Hloc_frag&Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose'". - iDestruct (ghost_var_agreeZ with "[$][$]") as "->". - iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". - iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". - simpl. - wp_load. - iMod ("Hclose'" with "[$Hloc_frag $Hauth_a $Hauth_b $Hεfrag]"); first done. - iModIntro. - iMod ("Hclose" with "[Hl Hloc_auth]"); first by iFrame. - by iApply "HΦ". - Unshelve. - all: simpl; try lra. - + replace (1+_-2)%R with (INR (bool_to_nat (bool_decide (is_Some b)))-1)%R; first apply resource_nonneg. - case_bool_decide; simpl; lra. - + replace (_+1-2)%R with (INR (bool_to_nat (bool_decide (is_Some a)))-1)%R; first apply resource_nonneg. - case_bool_decide; simpl; lra. - Qed. -End attempt2. +(* Section attempt2. *) +(* Context `{!conerisGS Σ, !spawnG Σ, !hocap_errorGS Σ, !inG Σ (excl_authR ZR), !inG Σ (excl_authR (optionO boolO))}. *) + + (* Definition loc_inv (l:loc) γ:= *) + (* inv loc_nroot (∃ (z:Z), l↦#z ∗ own γ (●E z)). *) +(* Lemma wp_half_FAA E *) +(* (ε2 : R -> bool -> R) *) +(* (P Q : iProp Σ) (T : bool -> iProp Σ) γ1 γ2 (l:loc): *) +(* ↑hocap_error_nroot ⊆ E -> *) +(* ↑loc_nroot ⊆ E -> *) +(* (∀ ε b, 0<= ε -> 0<= ε2 ε b)%R-> *) +(* (∀ (ε:R), 0<=ε -> (((ε2 ε true) + (ε2 ε false))/2 <= (ε)))%R → *) +(* {{{ error_inv γ1 ∗ loc_inv l γ2 ∗ *) +(* □(∀ (ε:R) (b : bool), P ∗ ●↯ ε @ γ1 ={E∖↑hocap_error_nroot}=∗ (⌜(1<=ε2 ε b)%R⌝∨●↯ (ε2 ε b) @ γ1 ∗ T b) ) ∗ *) +(* □ (∀ (b:bool) (z:Z), T b ∗ own γ2 (●E z) ={E∖↑loc_nroot}=∗ *) +(* if b then own γ2 (●E(z+1)%Z)∗ Q else own γ2 (●E(z))∗ Q ) ∗ *) +(* P }}} half_FAA l @ E {{{ (v: val), RET v; Q }}}. *) +(* Proof. *) +(* iIntros (Hsubset1 Hsubset2 ? Hineq Φ) "(#Hinv1 & #Hinv2 & #Hchange1 & #Hchange2 & HP) HΦ". *) +(* rewrite /half_FAA. *) +(* wp_apply (wp_hocap_flip_adv_comp _ ε2 P with "[-HΦ]"); [done|..]. *) +(* - intros. naive_solver. *) +(* - simpl. intros; naive_solver. *) +(* - by repeat iSplit. *) +(* - iIntros. destruct b. *) +(* + wp_pures. iInv "Hinv2" as "(%&?&?)" "Hclose". *) +(* wp_faa. *) +(* iMod ("Hchange2" with "[$]") as "[??]". *) +(* iMod ("Hclose" with "[$]"). *) +(* by iApply "HΦ". *) +(* + iInv "Hinv2" as "(%&?&?)" "Hclose". *) +(* wp_pure. *) +(* iMod ("Hchange2" with "[$]") as "[??]". *) +(* iMod ("Hclose" with "[$]"). *) +(* by iApply "HΦ". *) +(* Qed. *) + +(* Lemma parallel_add_spec'': *) +(* {{{ ↯ (3/4) }}} *) +(* parallel_add *) +(* {{{ (z:Z), RET #z; ⌜(z=2)⌝ }}}. *) +(* Proof. *) +(* iIntros (Φ) "Herr HΦ". *) +(* rewrite /parallel_add. *) +(* wp_alloc l as "Hl". *) +(* wp_pures. *) +(* rewrite -/(half_FAA l). *) +(* (** Allocate hocap error*) *) +(* unshelve iMod (hocap_error_alloc (mknonnegreal (3/4) _)) as "(%γ1 & Hεauth & Hεfrag)". *) +(* { lra. } *) +(* simpl. *) +(* (** Allocate hocap heap *) *) +(* iMod (own_alloc ((●E 0) ⋅ (◯E 0))) as "[%γ2 [Hauth_loc Hfrag_loc]]". *) +(* { by apply excl_auth_valid. } *) +(* (** Allocate hocap for tracking contributions *) *) +(* iMod (own_alloc ((●E None) ⋅ (◯E None))) as "[%γ3 [Hauth_a Hfrag_a]]". *) +(* { by apply excl_auth_valid. } *) +(* iMod (own_alloc ((●E None) ⋅ (◯E None))) as "[%γ4 [Hauth_b Hfrag_b]]". *) +(* { by apply excl_auth_valid. } *) +(* (** Allocate error invariants *) *) +(* iMod (inv_alloc hocap_error_nroot _ ((∃ (ε:R), ↯ ε ∗ ●↯ ε @ γ1)) with "[Herr Hεauth]") as "#Hεinv". *) +(* { iExists (mknonnegreal (3/4) _); iFrame. *) +(* Unshelve. lra. } *) +(* (** Allocate location inv *) *) +(* iMod (inv_alloc loc_nroot _ (∃ (z:Z), l↦#z ∗ own γ2 (●E z) *) +(* ) with "[Hl Hauth_loc]") as "#Hlocinv". *) +(* { iFrame. } *) +(* iMod (inv_alloc both_nroot _ *) +(* (∃ (z:Z) (a b:option bool), own γ2 (◯E z) ∗ *) +(* own γ3 (●E a) ∗ *) +(* own γ4 (●E b) ∗ *) +(* ⌜(z=bool_to_Z (is_Some_true a) + bool_to_Z (is_Some_true b))%Z⌝ ∗ *) +(* ◯↯ (1-Rpower 2 (IZR (bool_to_Z (bool_decide (is_Some a)))+IZR (bool_to_Z (bool_decide (is_Some b)))-2))%R@ γ1) *) +(* with "[Hfrag_loc Hεfrag Hauth_a Hauth_b]") as "#Hinvboth". *) +(* { iFrame. simpl. iModIntro. iSplitR; first by iPureIntro. *) +(* replace (1-_)%R with (3/4)%R; first done. *) +(* replace (Rpower _ _) with (1/4)%R; try lra. *) +(* replace (0+0-2)%R with (-2)%R by lra. *) +(* rewrite Rpower_Ropp/ Rpower. replace (IPR 2) with (INR 2); last done. *) +(* rewrite -ln_pow; last lra. *) +(* rewrite exp_ln; lra. *) +(* } *) +(* wp_apply (wp_par (λ _, own γ3 (◯E (Some true)))(λ _, own γ4 (◯E (Some true))) with "[Hfrag_a][Hfrag_b]"). *) +(* - (* first branch *) *) +(* wp_apply (wp_half_FAA _ (λ x b, *) +(* match ClassicalEpsilon.excluded_middle_informative (1/2<=x)%R *) +(* with *) +(* | left P => if b then (2*x - 1)%R else 1%R *) +(* | _ => x *) +(* end ) (own γ3 (◯E None)) *) +(* (own γ3 (◯E (Some true))) *) +(* (λ b, ⌜b=true⌝ ∗ (own γ3 (◯E (Some false))))%I γ1 γ2 l with "[$Hfrag_a]"); [done|done|..]. *) +(* + intros; repeat case_match; lra. *) +(* + intros. case_match; simpl; lra. *) +(* + repeat iSplit. *) +(* * done. *) +(* * done. *) +(* * iModIntro. iIntros (ε res) "[Hfrag_a Hεauth]". *) +(* iInv both_nroot as ">(%z & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". *) +(* iDestruct (hocap_error_agree with "[$][$]") as "%K". *) +(* iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". *) +(* simpl in *. *) +(* case_match; last first. *) +(* { exfalso. apply n. *) +(* simpl in *. *) +(* rewrite K. *) +(* assert (Rpower 2 (0+IZR (bool_to_Z (bool_decide (is_Some b))) - 2) <= 1/2)%R; try lra. *) +(* replace (_/_)%R with (/2) by lra. *) +(* rewrite -{3}(Rpower_1 2); last lra. *) +(* rewrite -Rpower_Ropp. *) +(* apply Rle_Rpower; first lra. *) +(* case_bool_decide; simpl; lra. *) +(* } *) +(* iMod (ghost_var_update' _ (Some false) with "[$Hauth_a][$]") as "[Hauth_a Hfrag_a]". *) +(* iMod (hocap_error_update _ (mknonnegreal _ _)with "[$][$]") as "[Hεauth Hεfrag]". *) +(* simpl. *) +(* iMod ("Hclose" with "[Hloc_frag Hauth_a Hauth_b Hεfrag]"); iFrame; first done. *) +(* simpl. case_match; last first. *) +(* { iLeft. done. } *) +(* iRight. iFrame. iModIntro; iSplitL; last done. *) +(* simpl. rewrite K. *) +(* iApply (hocap_error_irrel with "[$]"). *) +(* rewrite !Rpower_plus Rpower_O; last lra. *) +(* rewrite Rpower_1; lra. *) +(* * iModIntro. *) +(* iIntros (??) "[[-> Hfrag_a] Hauth_loc]". *) +(* iInv both_nroot as ">(% & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". *) +(* iDestruct (ghost_var_agreeZ with "[$][$]") as "->". *) +(* iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". *) +(* iMod (ghost_var_updateZ with "[$][$]") as "[Hauth_loc Hfrag_loc]". *) +(* iMod (ghost_var_update' _ (Some true) with "[$Hauth_a][$]") as "[Hauth_a Hfrag_a]". *) +(* simpl. *) +(* iMod ("Hclose" with "[$Hfrag_loc $Hauth_a $Hauth_b $Hεfrag]") as "_"; first done. *) +(* iFrame. simpl. *) +(* iModIntro. *) +(* replace (0+_+1)%Z with (1+bool_to_Z (is_Some_true b)); [done|lia]. *) +(* + iIntros. done. *) +(* - (* first branch *) *) +(* wp_apply (wp_half_FAA _ (λ x b, *) +(* match ClassicalEpsilon.excluded_middle_informative (1/2<=x)%R *) +(* with *) +(* | left P => if b then (2*x - 1)%R else 1%R *) +(* | _ => x *) +(* end ) (own γ4 (◯E None)) *) +(* (own γ4 (◯E (Some true))) *) +(* (λ b, ⌜b=true⌝ ∗ (own γ4 (◯E (Some false))))%I γ1 γ2 l with "[$Hfrag_b]"); [done|done|..]. *) +(* + intros; repeat case_match; lra. *) +(* + intros. case_match; simpl; lra. *) +(* + repeat iSplit. *) +(* * done. *) +(* * done. *) +(* * iModIntro. iIntros (ε res) "[Hfrag_b Hεauth]". *) +(* iInv both_nroot as ">(%z & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". *) +(* iDestruct (hocap_error_agree with "[$][$]") as "%K". *) +(* iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". *) +(* simpl in *. *) +(* case_match; last first. *) +(* { exfalso. apply n. *) +(* simpl in *. *) +(* rewrite K. *) +(* assert (Rpower 2 (IZR (bool_to_Z (bool_decide (is_Some a)))+0 - 2) <= 1/2)%R; try lra. *) +(* replace (_/_)%R with (/2) by lra. *) +(* rewrite -{3}(Rpower_1 2); last lra. *) +(* rewrite -Rpower_Ropp. *) +(* apply Rle_Rpower; first lra. *) +(* case_bool_decide; simpl; lra. *) +(* } *) +(* iMod (ghost_var_update' _ (Some false) with "[$Hauth_b][$]") as "[Hauth_b Hfrag_b]". *) +(* iMod (hocap_error_update _ (mknonnegreal _ _)with "[$][$]") as "[Hεauth Hεfrag]". *) +(* simpl. *) +(* iMod ("Hclose" with "[Hloc_frag Hauth_a Hauth_b Hεfrag]"); iFrame; first done. *) +(* simpl. case_match; last first. *) +(* { iLeft. done. } *) +(* iRight. iFrame. iModIntro; iSplitL; last done. *) +(* simpl. rewrite K. *) +(* iApply (hocap_error_irrel with "[$]"). *) +(* rewrite !Rpower_plus Rpower_O; last lra. *) +(* rewrite Rpower_1; lra. *) +(* * iModIntro. *) +(* iIntros (??) "[[-> Hfrag_a] Hauth_loc]". *) +(* iInv both_nroot as ">(% & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". *) +(* iDestruct (ghost_var_agreeZ with "[$][$]") as "->". *) +(* iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". *) +(* iMod (ghost_var_updateZ with "[$][$]") as "[Hauth_loc Hfrag_loc]". *) +(* iMod (ghost_var_update' _ (Some true) with "[$Hauth_b][$]") as "[Hauth_b Hfrag_b]". *) +(* simpl. *) +(* iMod ("Hclose" with "[$Hfrag_loc $Hauth_a $Hauth_b $Hεfrag]") as "_"; first done. *) +(* iFrame. simpl. *) +(* iModIntro. *) +(* replace (_+0+1)%Z with (bool_to_Z (is_Some_true a)+1); [done|lia]. *) +(* + iIntros. done. *) +(* - iIntros (??) "[Hfrag_a Hfrag_b]". iModIntro. wp_pures. *) +(* iInv loc_nroot as ">(%&Hl&Hloc_auth)" "Hclose". *) +(* iInv both_nroot as ">(%&%&%&Hloc_frag&Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose'". *) +(* iDestruct (ghost_var_agreeZ with "[$][$]") as "->". *) +(* iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". *) +(* iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". *) +(* simpl. *) +(* wp_load. *) +(* iMod ("Hclose'" with "[$Hloc_frag $Hauth_a $Hauth_b $Hεfrag]"); first done. *) +(* iModIntro. *) +(* iMod ("Hclose" with "[Hl Hloc_auth]"); first by iFrame. *) +(* by iApply "HΦ". *) +(* Unshelve. *) +(* all: simpl; try lra. *) +(* + replace (1+_-2)%R with (INR (bool_to_nat (bool_decide (is_Some b)))-1)%R; first apply resource_nonneg. *) +(* case_bool_decide; simpl; lra. *) +(* + replace (_+1-2)%R with (INR (bool_to_nat (bool_decide (is_Some a)))-1)%R; first apply resource_nonneg. *) +(* case_bool_decide; simpl; lra. *) +(* Qed. *) +(* End attempt2. *) Definition half_FAA' (l:loc) α:= diff --git a/theories/coneris/examples/random_counter/impl1.v b/theories/coneris/examples/random_counter/impl1.v index 64261d43..4436b9ec 100644 --- a/theories/coneris/examples/random_counter/impl1.v +++ b/theories/coneris/examples/random_counter/impl1.v @@ -1,344 +1,249 @@ From iris.algebra Require Import frac_auth. From iris.base_logic.lib Require Import invariants. -From clutch.coneris Require Import coneris hocap random_counter. +From clutch.coneris Require Import coneris hocap hocap_rand random_counter. Set Default Proof Using "Type*". Section impl1. + Context `{H:conerisGS Σ, r1:@rand_spec Σ H, L:randG Σ, !inG Σ (frac_authR natR)}. Definition new_counter1 : val:= λ: "_", ref #0. - Definition incr_counter1 : val := λ: "l", let: "n" := rand #3 in (FAA "l" "n", "n"). - Definition allocate_tape1 : val := λ: "_", AllocTape #3. - Definition incr_counter_tape1 :val := λ: "l" "α", let: "n" := rand("α") #3 in (FAA "l" "n", "n"). + Definition allocate_tape1 : val := λ: "_", rand_allocate_tape #3%nat. + Definition incr_counter_tape1 :val := λ: "l" "α", let: "n" := rand_tape "α" #3%nat in (FAA "l" "n", "n"). Definition read_counter1 : val := λ: "l", !"l". - Class counterG1 Σ := CounterG1 { counterG1_error::hocap_errorGS Σ; - counterG1_tapes:: hocap_tapesGS Σ; + Class counterG1 Σ := CounterG1 { counterG1_randG : randG Σ; counterG1_frac_authR:: inG Σ (frac_authR natR) }. - - Context `{!conerisGS Σ, !hocap_errorGS Σ, !hocap_tapesGS Σ, !inG Σ (frac_authR natR)}. - Definition counter_inv_pred1 (c:val) γ1 γ2 γ3:= - (∃ (ε:R) m (l:loc) (z:nat), - ↯ ε ∗ ●↯ ε @ γ1 ∗ - ([∗ map] α ↦ t ∈ m, α ↪N ( t.1 ; t.2 )) ∗ ●m@γ2 ∗ - ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ3 (●F z) + + Definition counter_inv_pred1 c γ2 := (∃ (l:loc) (z:nat), ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ2 (●F z) )%I. + Definition is_counter1 N (c:val) γ1 γ2:= + (is_rand (L:=L) (N.@"rand") γ1 ∗ + inv (N.@"counter") (counter_inv_pred1 c γ2) )%I. - Lemma new_counter_spec1 E ε N: - {{{ ↯ ε }}} + Lemma new_counter_spec1 E N: + {{{ True }}} new_counter1 #() @ E {{{ (c:val), RET c; - ∃ γ1 γ2 γ3, inv N (counter_inv_pred1 c γ1 γ2 γ3) ∗ - ◯↯ε @ γ1 ∗ own γ3 (◯F 0%nat) + ∃ γ1 γ2, is_counter1 N c γ1 γ2 ∗ own γ2 (◯F 0%nat) }}}. Proof. rewrite /new_counter1. - iIntros (Φ) "Hε HΦ". + iIntros (Φ) "_ HΦ". wp_pures. + iMod (rand_inv_create_spec) as "(%γ1 & #Hinv)". wp_alloc l as "Hl". - iDestruct (ec_valid with "[$]") as "%". - unshelve iMod (hocap_error_alloc (mknonnegreal ε _)) as "[%γ1 [H1 H2]]". - { lra. } - simpl. - iMod (hocap_tapes_alloc (∅:gmap _ _)) as "[%γ2 [H3 H4]]". - iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as "[%γ3[H5 H6]]". + iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as "[%γ2[H5 H6]]". { by apply frac_auth_valid. } replace (#0) with (#0%nat) by done. - iMod (inv_alloc N _ (counter_inv_pred1 (#l) γ1 γ2 γ3) with "[$Hε $Hl $H1 $H3 $H5]") as "#Hinv". - { iSplit; last done. by iApply big_sepM_empty. } + iMod (inv_alloc _ _ (counter_inv_pred1 (#l) γ2) with "[$Hl $H5]") as "#Hinv'"; first done. iApply "HΦ". - iExists _, _, _. by iFrame. - Qed. - - (** Not used in instantiating type class*) - Lemma incr_counter_spec1 E N c γ1 γ2 γ3 (ε2:R -> nat -> R) (P: iProp Σ) (T: nat -> iProp Σ) (Q: nat->nat->iProp Σ): - ↑N ⊆ E-> - (∀ ε n, 0<= ε -> 0<= ε2 ε n)%R-> - (∀ (ε:R), 0<=ε -> ((ε2 ε 0%nat) + (ε2 ε 1%nat)+ (ε2 ε 2%nat)+ (ε2 ε 3%nat))/4 <= ε)%R → - {{{ inv N (counter_inv_pred1 c γ1 γ2 γ3) ∗ - □(∀ (ε:R) (n : nat), P ∗ ●↯ ε @ γ1 ={E∖↑N}=∗ (⌜(1<=ε2 ε n)%R⌝∨●↯ (ε2 ε n) @ γ1 ∗ T n) ) ∗ - □ (∀ (n z:nat), T n ∗ own γ3 (●F z) ={E∖↑N}=∗ - own γ3 (●F(z+n)%nat)∗ Q z n) ∗ - P - }}} - incr_counter1 c @ E - {{{ (n:nat) (z:nat), RET (#z, #n); Q z n }}}. - Proof. - iIntros (Hsubset Hpos Hineq Φ) "(#Hinv & #Hvs1 & #Hvs2 & HP) HΦ". - rewrite /incr_counter1. - wp_pures. - wp_bind (rand _)%E. - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - iDestruct (ec_valid with "[$]") as "[%K1 %K2]". - wp_apply (wp_couple_rand_adv_comp1' _ _ _ _ (λ x, ε2 ε (fin_to_nat x)) with "[$]"). - { intros. naive_solver. } - { rewrite SeriesC_finite_foldr; specialize (Hineq ε K1). simpl; lra. } - iIntros (n) "H1". - iMod ("Hvs1" with "[$]") as "[%|[H2 HT]]". - { iExFalso. iApply ec_contradict; last done. done. } - iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. - iModIntro. wp_pures. - clear -Hsubset. - wp_bind (FAA _ _). - iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - wp_faa. - iMod ("Hvs2" with "[$]") as "[H6 HQ]". - replace (#(z+n)) with (#(z+n)%nat); last first. - { by rewrite Nat2Z.inj_add. } - iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. + iFrame. iModIntro. - wp_pures. - by iApply "HΦ". + iExists _. by iSplit. Qed. - Lemma allocate_tape_spec1 N E c γ1 γ2 γ3: + (* (** Not used in instantiating type class*) *) + (* Lemma incr_counter_spec1 E N c γ1 γ2 γ3 (ε2:R -> nat -> R) (P: iProp Σ) (T: nat -> iProp Σ) (Q: nat->nat->iProp Σ): *) + (* ↑N ⊆ E-> *) + (* (∀ ε n, 0<= ε -> 0<= ε2 ε n)%R-> *) + (* (∀ (ε:R), 0<=ε -> ((ε2 ε 0%nat) + (ε2 ε 1%nat)+ (ε2 ε 2%nat)+ (ε2 ε 3%nat))/4 <= ε)%R → *) + (* {{{ inv N (counter_inv_pred1 c γ1 γ2 γ3) ∗ *) + (* □(∀ (ε:R) (n : nat), P ∗ ●↯ ε @ γ1 ={E∖↑N}=∗ (⌜(1<=ε2 ε n)%R⌝∨●↯ (ε2 ε n) @ γ1 ∗ T n) ) ∗ *) + (* □ (∀ (n z:nat), T n ∗ own γ3 (●F z) ={E∖↑N}=∗ *) + (* own γ3 (●F(z+n)%nat)∗ Q z n) ∗ *) + (* P *) + (* }}} *) + (* incr_counter1 c @ E *) + (* {{{ (n:nat) (z:nat), RET (#z, #n); Q z n }}}. *) + (* Proof. *) + (* iIntros (Hsubset Hpos Hineq Φ) "(#Hinv & #Hvs1 & #Hvs2 & HP) HΦ". *) + (* rewrite /incr_counter1. *) + (* wp_pures. *) + (* wp_bind (rand _)%E. *) + (* iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) + (* iDestruct (ec_valid with "[$]") as "[%K1 %K2]". *) + (* wp_apply (wp_couple_rand_adv_comp1' _ _ _ _ (λ x, ε2 ε (fin_to_nat x)) with "[$]"). *) + (* { intros. naive_solver. } *) + (* { rewrite SeriesC_finite_foldr; specialize (Hineq ε K1). simpl; lra. } *) + (* iIntros (n) "H1". *) + (* iMod ("Hvs1" with "[$]") as "[%|[H2 HT]]". *) + (* { iExFalso. iApply ec_contradict; last done. done. } *) + (* iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. *) + (* iModIntro. wp_pures. *) + (* clear -Hsubset. *) + (* wp_bind (FAA _ _). *) + (* iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) + (* wp_faa. *) + (* iMod ("Hvs2" with "[$]") as "[H6 HQ]". *) + (* replace (#(z+n)) with (#(z+n)%nat); last first. *) + (* { by rewrite Nat2Z.inj_add. } *) + (* iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. *) + (* iModIntro. *) + (* wp_pures. *) + (* by iApply "HΦ". *) + (* Qed. *) + + Lemma allocate_tape_spec1 N E c γ1 γ2: ↑N ⊆ E-> - {{{ inv N (counter_inv_pred1 c γ1 γ2 γ3) }}} + {{{ is_counter1 N c γ1 γ2 }}} allocate_tape1 #() @ E {{{ (v:val), RET v; - ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ α ◯↪N (3%nat; []) @ γ2 + ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, []) }}}. Proof. - iIntros (Hsubset Φ) "#Hinv HΦ". + iIntros (Hsubset Φ) "[#Hinv #Hinv'] HΦ". rewrite /allocate_tape1. wp_pures. - wp_alloctape α as "Hα". - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - iDestruct (hocap_tapes_notin with "[$][$]") as "%". - iMod (hocap_tapes_new with "[$]") as "[H4 H7]"; first done. - iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Hα]") as "_". - { iNext. iSplitL; last done. - rewrite big_sepM_insert; [simpl; iFrame|done]. - } - iApply "HΦ". - by iFrame. + wp_apply rand_allocate_tape_spec; [by eapply nclose_subseteq'|done..]. Qed. - Lemma incr_counter_tape_spec_some1 N E c γ1 γ2 γ3 (P: iProp Σ) (Q:nat->iProp Σ) (α:loc) (n:nat) ns: - ↑N⊆E -> - {{{ inv N (counter_inv_pred1 c γ1 γ2 γ3) ∗ - □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗ - own γ3 (●F(z+n)%nat)∗ Q z) ∗ - P ∗ α ◯↪N (3%nat; n::ns) @ γ2 + Lemma incr_counter_tape_spec_some1 N E c γ1 γ2 (Q:nat->iProp Σ) (α:loc) n ns: + ↑N⊆E -> + {{{ is_counter1 N c γ1 γ2 ∗ + rand_tapes_frag (L:=L) γ1 α (3, n::ns) ∗ + ( ∀ (z:nat), own γ2 (●F z) ={E∖↑N}=∗ + own γ2 (●F (z+n)) ∗ Q z) + }}} incr_counter_tape1 c #lbl:α @ E - {{{ (z:nat), RET (#z, #n); Q z ∗ α ◯↪N (3%nat; ns) @ γ2}}}. + {{{ (z:nat), RET (#z, #n); rand_tapes_frag (L:=L) γ1 α (3, ns) ∗ + Q z }}}. Proof. - iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP & Hα) HΦ". + iIntros (Hsubset Φ) "([#Hinv #Hinv'] & Hfrag & Hvs) HΦ". rewrite /incr_counter_tape1. wp_pures. - wp_bind (rand(_) _)%E. - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - iDestruct (hocap_tapes_agree with "[$][$]") as "%". - erewrite <-(insert_delete m) at 1; last done. - rewrite big_sepM_insert; last apply lookup_delete. - simpl. - iDestruct "H3" as "[Htape H3]". - wp_apply (wp_rand_tape with "[$]"). - iIntros "[Htape %]". - iMod (hocap_tapes_pop with "[$][$]") as "[H4 Hα]". - iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". - { iSplitL; last done. - erewrite <-(insert_delete m) at 2; last done. - iNext. - rewrite insert_insert. - rewrite big_sepM_insert; last apply lookup_delete. iFrame. - } - iModIntro. + wp_apply (rand_tape_spec_some with "[$]") as "Hfrag"; first by eapply nclose_subseteq'. wp_pures. - clear -Hsubset. wp_bind (FAA _ _). - iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + iInv "Hinv'" as ">(%&%&-> & ?&?)" "Hclose". wp_faa. - iMod ("Hvs" with "[$]") as "[H6 HQ]". - replace (#(z+n)) with (#(z+n)%nat); last first. - { by rewrite Nat2Z.inj_add. } - iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. - iModIntro. wp_pures. - iApply "HΦ". - by iFrame. - Qed. - - Lemma counter_presample_spec1 NS E ns α - (ε2 : R -> nat -> R) - (P : iProp Σ) T γ1 γ2 γ3 c: - ↑NS ⊆ E -> - (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> - (∀ (ε:R), 0<= ε ->SeriesC (λ n, if (bool_decide (n≤3%nat)) then 1 / (S 3%nat) * ε2 ε n else 0%R)%R <= ε)%R-> - inv NS (counter_inv_pred1 c γ1 γ2 γ3) -∗ - (□∀ (ε:R) n, (P ∗ ●↯ ε@ γ1) ={E∖↑NS}=∗ - (⌜(1<=ε2 ε n)%R⌝ ∨(●↯ (ε2 ε n) @ γ1 ∗ T (n)))) - -∗ - P -∗ α ◯↪N (3%nat; ns) @ γ2 -∗ - wp_update E (∃ n, T (n) ∗ α◯↪N (3%nat; ns++[n]) @ γ2). - Proof. - 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 & -> & H5 & H6) Hclose]"; [done|]. - iDestruct (hocap_tapes_agree with "[$][$]") as "%". - erewrite <-(insert_delete m) at 1; last done. - rewrite big_sepM_insert; last apply lookup_delete. - simpl. - iDestruct "H3" as "[Htape H3]". - iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%)". - 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'". - iApply state_step_coupl_state_adv_comp_con_prob_lang; first done. - unshelve iExists (λ x, mknonnegreal (ε2 ε1' x) _). - { apply Hpos. apply cond_nonneg. } - iSplit. - { iPureIntro. - unshelve epose proof (Hineq ε1' _) as H1; first apply cond_nonneg. - by rewrite SeriesC_nat_bounded_fin in H1. } - iIntros (sample). - - destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' 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 *. lra. - } - iApply state_step_coupl_ret. - unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 ε1' sample) _) with "Hε_supply") as "[Hε_supply Hε]". - { apply Hpos. apply cond_nonneg. } - { simpl. done. } - iMod (tapeN_update_append _ _ _ _ sample with "[$][$]") as "[Htapes Htape]". - 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 $H5 $H6]") as "_". - { iNext. iSplit; last done. - rewrite big_sepM_insert_delete; iFrame. - } - iApply fupd_mask_intro_subseteq; first set_solver. - iFrame. - Qed. + iMod (fupd_mask_subseteq (E ∖ ↑N)) as "Hclose'". + + apply difference_mono_l. + by apply nclose_subseteq'. + + iMod ("Hvs" with "[$]") as "[? HQ]". + iMod "Hclose'" as "_". + rewrite -Nat2Z.inj_add. + iMod ("Hclose" with "[-HQ Hfrag HΦ]") as "_"; first by iFrame. + iModIntro. + wp_pures. + iApply "HΦ". by iFrame. + Qed. - Lemma read_counter_spec1 N E c γ1 γ2 γ3 P Q: + Lemma counter_tapes_presample1 N E γ1 γ2 c α ns ε (ε2 : fin 4%nat -> R): + ↑N ⊆ E -> + (∀ x, 0<=ε2 x)%R -> + (SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R -> + is_counter1 N c γ1 γ2 -∗ + rand_tapes_frag (L:=L) γ1 α (3%nat, ns) -∗ + ↯ ε -∗ + state_update E (∃ n, ↯ (ε2 n) ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, ns++[fin_to_nat n])). + Proof. + iIntros (Hsubset Hpos Hineq) "[#Hinv #Hinv'] Hfrag Herr". + iMod (rand_tapes_presample with "[//][$][$]") as "(%&$&$)"; try done; first by apply nclose_subseteq'. + etrans; last exact. + apply Req_le. + apply SeriesC_ext; intros. simpl. lra. + Qed. + + Lemma read_counter_spec1 N E c γ1 γ2 Q: ↑N ⊆ E -> - {{{ inv N (counter_inv_pred1 c γ1 γ2 γ3) ∗ - □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗ - own γ3 (●F z)∗ Q z) - ∗ P + {{{ is_counter1 N c γ1 γ2 ∗ + (∀ (z:nat), own γ2 (●F z) ={E∖↑N}=∗ + own γ2 (●F z) ∗ Q z) + }}} read_counter1 c @ E {{{ (n':nat), RET #n'; Q n' }}}. Proof. - iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP) HΦ". + iIntros (Hsubset Φ) "([#Hinv #Hinv'] & Hvs) HΦ". rewrite /read_counter1. wp_pure. - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + iInv "Hinv'" as ">( %l & %z & -> & H5 & H6)" "Hclose". wp_load. - iMod ("Hvs" with "[$]") as "[H6 HQ]". - iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]"); first done. + iMod (fupd_mask_subseteq (E ∖ ↑N)) as "Hclose'". + { apply difference_mono_l. + by apply nclose_subseteq'. } + iMod ("Hvs" with "[$]") as "[? HQ]". + iMod "Hclose'" as "_". + iMod ("Hclose" with "[-HQ HΦ]"); first by iFrame. iApply ("HΦ" with "[$]"). - Qed. - + Qed. End impl1. -Program Definition random_counter1 `{!conerisGS Σ}: random_counter := +Program Definition random_counter1 `{!conerisGS Σ, F:rand_spec}: random_counter := {| new_counter := new_counter1; allocate_tape:= allocate_tape1; incr_counter_tape := incr_counter_tape1; read_counter:=read_counter1; counterG := counterG1; - error_name := gname; - tape_name := gname; + tape_name := rand_tape_name; counter_name :=gname; - is_counter _ N c γ1 γ2 γ3 := inv N (counter_inv_pred1 c γ1 γ2 γ3); - counter_error_auth _ γ x := ●↯ x @ γ; - counter_error_frag _ γ x := ◯↯ x @ γ; - counter_tapes_auth _ γ m := (●((λ ns, (3, ns))<$>m)@γ)%I; - counter_tapes_frag _ γ α ns := (α◯↪N (3%nat;ns) @ γ)%I; + is_counter _ N c γ1 γ2 := is_counter1 (L:=counterG1_randG) N c γ1 γ2; + counter_tapes_auth _ γ m := rand_tapes_auth (L:=counterG1_randG) γ ((λ ns, (3, ns))<$>m); + counter_tapes_frag _ γ α ns := rand_tapes_frag (L:= counterG1_randG)γ α (3%nat, ns); counter_content_auth _ γ z := own γ (●F z); counter_content_frag _ γ f z := own γ (◯F{f} z); + counter_tapes_presample _ := counter_tapes_presample1; new_counter_spec _ := new_counter_spec1; allocate_tape_spec _ :=allocate_tape_spec1; incr_counter_tape_spec_some _ :=incr_counter_tape_spec_some1; - counter_presample_spec _ :=counter_presample_spec1; read_counter_spec _ :=read_counter_spec1 |}. Next Obligation. simpl. - iIntros (??????) "(%&<-&H1)(%&<-&H2)". - iCombine "H1 H2" gives "%H". by rewrite excl_auth.excl_auth_auth_op_valid in H. -Qed. -Next Obligation. - simpl. - iIntros (??????) "(%&<-&H1)(%&<-&H2)". - iCombine "H1 H2" gives "%H". by rewrite excl_auth.excl_auth_frag_op_valid in H. -Qed. -Next Obligation. - simpl. - iIntros (?????) "H". - iApply (hocap_error_auth_pos with "[$]"). -Qed. -Next Obligation. - simpl. - iIntros (?????) "H". - iApply (hocap_error_frag_pos with "[$]"). -Qed. -Next Obligation. - simpl. - iIntros (??????) "H1 H2". - iApply (hocap_error_agree with "[$][$]"). -Qed. -Next Obligation. - simpl. iIntros (???????) "??". - iApply (hocap_error_update with "[$][$]"). + iIntros (?????????) "H1 H2". + iDestruct (rand_tapes_auth_exclusive with "[$][$]") as "[]". 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. + iIntros. + iDestruct (rand_tapes_frag_exclusive with "[$][$]") as "[]". Qed. Next Obligation. simpl. iIntros. - iDestruct (hocap_tapes_agree with "[$][$]") as "%H". + iDestruct (rand_tapes_agree with "[$][$]") as "%H". iPureIntro. - rewrite lookup_fmap_Some in H. destruct H as (?&?&?). + apply lookup_fmap_Some in H as (?&?&?). by simplify_eq. Qed. Next Obligation. iIntros. - iMod (hocap_tapes_presample with "[$][$]") as "[??]". - iModIntro. iFrame. - by rewrite fmap_insert. + iDestruct (rand_tapes_valid with "[$]") as "$". +Qed. +Next Obligation. + simpl. + iIntros. + iMod (rand_tapes_update with "[$][$]") as "[??]"; last iFrame; first done. + by rewrite fmap_insert. Qed. Next Obligation. simpl. - iIntros (??????) "H1 H2". + iIntros (?????????) "H1 H2". iCombine "H1 H2" gives "%H". by rewrite auth_auth_op_valid in H. Qed. Next Obligation. - simpl. iIntros (???? z z' ?) "H1 H2". + simpl. iIntros (??????? z z' ?) "H1 H2". iCombine "H1 H2" gives "%H". apply frac_auth_included_total in H. iPureIntro. by apply nat_included. Qed. Next Obligation. simpl. - iIntros (????????). - rewrite frac_auth_frag_op. by rewrite own_op. + iIntros. + rewrite frac_auth_frag_op. rewrite own_op. + iSplit; iIntros; iFrame. Qed. Next Obligation. - simpl. iIntros (??????) "H1 H2". + simpl. iIntros (?????????) "H1 H2". iCombine "H1 H2" gives "%H". iPureIntro. by apply frac_auth_agree_L in H. Qed. Next Obligation. - simpl. iIntros (????????) "H1 H2". + simpl. iIntros (???????????) "H1 H2". iMod (own_update_2 _ _ _ (_ ⋅ _) with "[$][$]") as "[$$]"; last done. apply frac_auth_update. apply nat_local_update. lia. diff --git a/theories/coneris/examples/random_counter/impl2.v b/theories/coneris/examples/random_counter/impl2.v index 86efae3d..b4dfec13 100644 --- a/theories/coneris/examples/random_counter/impl2.v +++ b/theories/coneris/examples/random_counter/impl2.v @@ -1,470 +1,436 @@ From iris.algebra Require Import frac_auth. From iris.base_logic.lib Require Import invariants. -From clutch.coneris Require Import coneris hocap random_counter. -From clutch Require Import uniform_list. +From clutch.coneris Require Import coneris hocap random_counter hocap_flip. Set Default Proof Using "Type*". Local Definition expander (l:list nat):= - l ≫= (λ x, [Nat.div2 x; Nat.b2n (Nat.odd x)]). - -Class hocap_tapesGS' (Σ : gFunctors) := Hocap_tapesGS' { - hocap_tapesGS_inG' :: ghost_mapG Σ loc (bool* list nat) - }. -Definition hocap_tapesΣ' := ghost_mapΣ loc (bool *list nat). - -Notation "α ◯↪N ( b , ns ) @ γ":= (α ↪[ γ ] (b, ns))%I - (at level 20) : bi_scope. - -Notation "● m @ γ" := (ghost_map_auth γ 1 m) (at level 20) : bi_scope. + l ≫= (λ x, [2<=?x; (Nat.odd x)]). +Local Lemma expander_eta x: x<4->(Z.of_nat x= Z.of_nat 2*Z.b2z (2<=? x)%nat + Z.b2z (Nat.odd x))%Z. +Proof. + destruct x as [|[|[|[|]]]]; last lia; intros; simpl; lia. +Qed. -Section tapes_lemmas. - Context `{!conerisGS Σ, !hocap_tapesGS' Σ}. +Local Lemma expander_inj l1 l2: Forall (λ x, x<4) l1 -> + Forall (λ y, y<4) l2 -> + expander l1 = expander l2 -> + l1 = l2. +Proof. + rewrite /expander. + revert l2. + induction l1 as [|x xs IH]. + - simpl. + by intros [] ???. + - simpl. + intros [|y ys]; simpl; first done. + rewrite !Forall_cons. + rewrite /Nat.odd. + intros [K1 H1] [K2 H2] H. + simplify_eq. + f_equal; last naive_solver. + repeat (destruct x as [|x]; try lia); + repeat (destruct y as [|y]; try lia); + simpl in *; simplify_eq. +Qed. - Lemma hocap_tapes_alloc' m: - ⊢ |==>∃ γ, (● m @ γ) ∗ [∗ map] k↦v ∈ m, (k ◯↪N (v.1, v.2) @ γ). - Proof. - iMod ghost_map_alloc as (γ) "[??]". - iFrame. iModIntro. - iApply big_sepM_mono; last done. - by iIntros (?[??]). - Qed. +Local Fixpoint decoder (l:list bool) := + match l with + |[] => Some [] + | b::b'::ls => + res← decoder ls; + Some (((bool_to_nat b)*2+(bool_to_nat b'))::res) + | _ => None +end. - Lemma hocap_tapes_agree' m b γ k ns: - (● m @ γ) -∗ (k ◯↪N (b, ns) @ γ) -∗ ⌜ m!!k = Some (b, ns) ⌝. - Proof. - iIntros "H1 H2". - by iCombine "H1 H2" gives "%". - Qed. +(* Lemma decoder_unfold l: *) +(* decoder l = *) +(* match l with *) +(* |[] => Some [] *) +(* | b::b'::ls => *) +(* res← decoder ls; *) +(* Some (((bool_to_nat b)*2+(bool_to_nat b'))::res) *) +(* | _ => None end. *) +(* Proof. *) +(* induction l; by rewrite {1}/decoder. *) +(* Qed. *) - Lemma hocap_tapes_new' γ m k ns b: - m!!k=None -> ⊢ (● m @ γ) ==∗ (● (<[k:=(b, ns)]>m) @ γ) ∗ (k ◯↪N (b, ns) @ γ). - Proof. - iIntros (Hlookup) "H". - by iApply ghost_map_insert. - Qed. +Local Lemma decoder_correct bs ns: decoder bs = Some ns -> expander ns = bs. +Proof. + revert bs. + induction ns. + - intros bs H. simpl. destruct bs as [|?[|??]]; try done. + simpl in *. + rewrite bind_Some in H. + destruct H as (?&?&?). + simplify_eq. + - intros [|b[|b' ?]]; simpl; try done. + intros H. + rewrite bind_Some in H. + destruct H as (?&?&?). + simplify_eq. + repeat f_equal; last naive_solver; destruct b; destruct b'; done. +Qed. + + +Local Lemma decoder_inj x y z: decoder x = Some z -> decoder y = Some z -> x= y. +Proof. + intros H1 H2. + apply decoder_correct in H1, H2. + by subst. +Qed. - Lemma hocap_tapes_presample' b γ m k ns n: - (● m @ γ) -∗ (k ◯↪N (b, ns) @ γ) ==∗ (● (<[k:=(b, ns++[n])]>m) @ γ) ∗ (k ◯↪N (b, ns++[n]) @ γ). - Proof. - iIntros "H1 H2". - iApply (ghost_map_update with "[$][$]"). - Qed. +Local Lemma decoder_ineq bs xs: decoder bs = Some xs -> Forall (λ x : nat, x < 4) xs. +Proof. + revert bs. + induction xs; first by (intros; apply Forall_nil). + intros [|b[|b'?]] H; try simplify_eq. + rewrite bind_Some in H. + destruct H as (?&?&?). + simplify_eq. + rewrite Forall_cons. + split; last naive_solver. + destruct b, b'; simpl; lia. +Qed. - Lemma hocap_tapes_pop1' γ m k ns: - (● m @ γ) -∗ (k ◯↪N (true, ns) @ γ) ==∗ (● (<[k:=(false, ns)]>m) @ γ) ∗ (k ◯↪N (false, ns) @ γ). - Proof. - iIntros "H1 H2". - iApply (ghost_map_update with "[$][$]"). - Qed. - - Lemma hocap_tapes_pop2' γ m k ns n: - (● m @ γ) -∗ (k ◯↪N (false, n::ns) @ γ) ==∗ (● (<[k:=(true, ns)]>m) @ γ) ∗ (k ◯↪N (true, ns) @ γ). - Proof. - iIntros "H1 H2". - iApply (ghost_map_update with "[$][$]"). - Qed. +Local Lemma decoder_None p bs : length bs = p -> decoder bs = None -> ¬ ∃ num, length bs = 2 * num. +Proof. + revert bs. + induction (lt_wf p) as [x ? IH]. + destruct x. + - intros []??; simplify_eq. + - intros [|?[|??]]; intros Hlen H'; simplify_eq. + + simpl in *. simplify_eq. + intros (num&?). + destruct num; lia. + + simpl in *. + simplify_eq. + rewrite bind_None in H'. + destruct H' as [|(?&?&?)]; last done. + unshelve epose proof IH (length l) _ l _ _ as H1; try lia; try done. + intros (num & ?). apply H1. + exists (num-1). lia. +Qed. - Lemma hocap_tapes_notin' α N ns m (f:(bool*list nat)-> nat) g: - α ↪N (N; ns) -∗ ([∗ map] α0↦t ∈ m, α0 ↪N (f t; g t)) -∗ ⌜m!!α=None ⌝. - Proof. - destruct (m!!α) eqn:Heqn; last by iIntros. - iIntros "Hα Hmap". - iDestruct (big_sepM_lookup with "[$]") as "?"; first done. - iExFalso. - iApply (tapeN_tapeN_contradict with "[$][$]"). - Qed. +Local Lemma decoder_Some_length bs xs: decoder bs = Some xs -> length bs = 2 * length xs. +Proof. + revert bs. + induction xs as [|x xs IH]; intros [|?[|??]] H; simpl in *; simplify_eq; try done. + - rewrite bind_Some in H. + destruct H as (?&?&?). + simplify_eq. + - rewrite bind_Some in H. + destruct H as (?&?&?). + simplify_eq. + f_equal. rewrite IH; [lia|done]. +Qed. -End tapes_lemmas. Section impl2. - + Context `{F: flip_spec Σ}. Definition new_counter2 : val:= λ: "_", ref #0. - Definition incr_counter2 : val := λ: "l", let: "n" := rand #1 in - let: "n'" := rand #1 in - let: "x" := #2 * "n" + "n'" in - (FAA "l" "x", "x"). - Definition allocate_tape2 : val := λ: "_", AllocTape #1. - Definition incr_counter_tape2 :val := λ: "l" "α", let: "n" := rand("α") #1 in - let: "n'" := rand("α") #1 in + (* Definition incr_counter2 : val := λ: "l", let: "n" := rand #1 in *) + (* let: "n'" := rand #1 in *) + (* let: "x" := #2 * "n" + "n'" in *) + (* (FAA "l" "x", "x"). *) + Definition allocate_tape2 : val := flip_allocate_tape. + Definition incr_counter_tape2 :val := λ: "l" "α", let: "n" := + conversion.bool_to_int (flip_tape "α") + in + let: "n'" := + conversion.bool_to_int (flip_tape "α") + in let: "x" := #2 * "n" + "n'" in (FAA "l" "x", "x"). Definition read_counter2 : val := λ: "l", !"l". - Class counterG2 Σ := CounterG2 { counterG2_error::hocap_errorGS Σ; - counterG2_tapes:: hocap_tapesGS' Σ; - counterG2_frac_authR:: inG Σ (frac_authR natR) }. + Class counterG2 Σ := CounterG2 { (* counterG2_tapes:: hocap_tapesGS' Σ; *) + counterG2_frac_authR:: inG Σ (frac_authR natR); + counterG2_flipG: flipG Σ + }. - Context `{!conerisGS Σ, !hocap_errorGS Σ, !hocap_tapesGS' Σ, !inG Σ (frac_authR natR)}. + Context `{L:!flipG Σ, !inG Σ (frac_authR natR)}. - Definition counter_inv_pred2 (c:val) γ1 γ2 γ3:= - (∃ (ε:R) (m:gmap loc (bool*list nat)) (l:loc) (z:nat), - ↯ ε ∗ ●↯ ε @ γ1 ∗ - ([∗ map] α ↦ t ∈ m, α ↪N ( 1%nat ; if t.1:bool then expander t.2 else drop 1%nat (expander t.2)) ) - ∗ ●m@γ2 ∗ - ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ3 (●F z) + Definition counter_inv_pred2 (c:val) γ := + (∃ (l:loc) (z:nat), + ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ (●F z) + )%I. + + Definition is_counter2 N (c:val) γ1 γ2:= + (is_flip (L:=L) (N.@"flip") γ1 ∗ + inv (N.@"counter") (counter_inv_pred2 c γ2) )%I. - Lemma new_counter_spec2 E ε N: - {{{ ↯ ε }}} + Lemma new_counter_spec2 E N: + {{{ True }}} new_counter2 #() @ E {{{ (c:val), RET c; - ∃ γ1 γ2 γ3, inv N (counter_inv_pred2 c γ1 γ2 γ3) ∗ - ◯↯ε @ γ1 ∗ own γ3 (◯F 0%nat) + ∃ γ1 γ2, is_counter2 N c γ1 γ2 ∗ own γ2 (◯F 0%nat) }}}. Proof. rewrite /new_counter2. - iIntros (Φ) "Hε HΦ". + iIntros (Φ) "_ HΦ". wp_pures. + iMod (flip_inv_create_spec) as "(%γ1 & #Hinv)". wp_alloc l as "Hl". - iDestruct (ec_valid with "[$]") as "%". - unshelve iMod (hocap_error_alloc (mknonnegreal ε _)) as "[%γ1 [H1 H2]]". - { lra. } - simpl. - iMod (hocap_tapes_alloc' (∅:gmap _ _)) as "[%γ2 [H3 H4]]". - iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as "[%γ3[H5 H6]]". + iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as "[%γ2[H5 H6]]". { by apply frac_auth_valid. } replace (#0) with (#0%nat) by done. - iMod (inv_alloc N _ (counter_inv_pred2 (#l) γ1 γ2 γ3) with "[$Hε $Hl $H1 $H3 $H5]") as "#Hinv". - { iSplit; last done. by iApply big_sepM_empty. } + iMod (inv_alloc _ _ (counter_inv_pred2 (#l) γ2) with "[$Hl $H5]") as "#Hinv'"; first done. iApply "HΦ". - iExists _, _, _. by iFrame. + iFrame. + iModIntro. + iExists _. by iSplit. Qed. (** This lemma is not possible as only one view shift*) - Lemma incr_counter_spec2 E N c γ1 γ2 γ3 (ε2:R -> nat -> R) (P: iProp Σ) (T: nat -> iProp Σ) (Q: nat->nat->iProp Σ): - ↑N ⊆ E-> - (∀ ε n, 0<= ε -> 0<= ε2 ε n)%R-> - (∀ (ε:R), 0<=ε -> ((ε2 ε 0%nat) + (ε2 ε 1%nat)+ (ε2 ε 2%nat)+ (ε2 ε 3%nat))/4 <= ε)%R → - {{{ inv N (counter_inv_pred2 c γ1 γ2 γ3) ∗ - □(∀ (ε:R) (n : nat), P ∗ ●↯ ε @ γ1 ={E∖↑N}=∗ (⌜(1<=ε2 ε n)%R⌝∨●↯ (ε2 ε n) @ γ1 ∗ T n) ) ∗ - □ (∀ (n z:nat), T n ∗ own γ3 (●F z) ={E∖↑N}=∗ - own γ3 (●F(z+n)%nat)∗ Q z n) ∗ - P - }}} - incr_counter2 c @ E - {{{ (n:nat) (z:nat), RET (#z, #n); Q z n }}}. - Proof. - iIntros (Hsubset Hpos Hineq Φ) "(#Hinv & #Hvs1 & #Hvs2 & HP) HΦ". - rewrite /incr_counter2. - wp_pures. - wp_bind (rand _)%E. - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - (** cant do two view shifts! *) - Abort. + (* Lemma incr_counter_spec2 E N c γ1 γ2 γ3 (ε2:R -> nat -> R) (P: iProp Σ) (T: nat -> iProp Σ) (Q: nat->nat->iProp Σ): *) + (* ↑N ⊆ E-> *) + (* (∀ ε n, 0<= ε -> 0<= ε2 ε n)%R-> *) + (* (∀ (ε:R), 0<=ε -> ((ε2 ε 0%nat) + (ε2 ε 1%nat)+ (ε2 ε 2%nat)+ (ε2 ε 3%nat))/4 <= ε)%R → *) + (* {{{ inv N (counter_inv_pred2 c γ1 γ2 γ3) ∗ *) + (* □(∀ (ε:R) (n : nat), P ∗ ●↯ ε @ γ1 ={E∖↑N}=∗ (⌜(1<=ε2 ε n)%R⌝∨●↯ (ε2 ε n) @ γ1 ∗ T n) ) ∗ *) + (* □ (∀ (n z:nat), T n ∗ own γ3 (●F z) ={E∖↑N}=∗ *) + (* own γ3 (●F(z+n)%nat)∗ Q z n) ∗ *) + (* P *) + (* }}} *) + (* incr_counter2 c @ E *) + (* {{{ (n:nat) (z:nat), RET (#z, #n); Q z n }}}. *) + (* Proof. *) + (* iIntros (Hsubset Hpos Hineq Φ) "(#Hinv & #Hvs1 & #Hvs2 & HP) HΦ". *) + (* rewrite /incr_counter2. *) + (* wp_pures. *) + (* wp_bind (rand _)%E. *) + (* iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) + (* (** cant do two view shifts! *) *) + (* Abort. *) - Lemma allocate_tape_spec2 N E c γ1 γ2 γ3: + Lemma allocate_tape_spec2 N E c γ1 γ2: ↑N ⊆ E-> - {{{ inv N (counter_inv_pred2 c γ1 γ2 γ3) }}} + {{{ is_counter2 N c γ1 γ2 }}} allocate_tape2 #() @ E {{{ (v:val), RET v; - ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ α ◯↪N (true, []) @ γ2 + ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ (flip_tapes_frag (L:=L) γ1 α (expander []) ∗ ⌜Forall (λ x, x<4) []⌝) }}}. Proof. - iIntros (Hsubset Φ) "#Hinv HΦ". + iIntros (Hsubset Φ) "[#Hinv #Hinv'] HΦ". rewrite /allocate_tape2. wp_pures. - wp_alloctape α as "Hα". - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - iDestruct (hocap_tapes_notin' with "[$][$]") as "%". - iMod (hocap_tapes_new' _ _ _ _ true with "[$]") as "[H4 H7]"; first done. - replace ([]) with (expander []) by done. - iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Hα]") as "_". - { iNext. iSplitL; last done. - rewrite big_sepM_insert; [iFrame|done]. - } + wp_apply flip_allocate_tape_spec; [by eapply nclose_subseteq'|done|..]. + iIntros (?) "(%&->&?)". iApply "HΦ". - by iFrame. + iFrame. + iPureIntro. split; first done. + by apply Forall_nil. Qed. - - Lemma incr_counter_tape_spec_some2 N E c γ1 γ2 γ3 (P: iProp Σ) (Q:nat->iProp Σ) (α:loc) (n:nat) ns: + + Lemma incr_counter_tape_spec_some2 N E c γ1 γ2 (Q:nat->iProp Σ) (α:loc) n ns: ↑N⊆E -> - {{{ inv N (counter_inv_pred2 c γ1 γ2 γ3) ∗ - □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗ - own γ3 (●F(z+n)%nat)∗ Q z) ∗ - P ∗ α ◯↪N (true, n::ns) @ γ2 + {{{ is_counter2 N c γ1 γ2 ∗ + (flip_tapes_frag (L:=L) γ1 α (expander (n::ns)) ∗ ⌜Forall (λ x, x<4) (n::ns)⌝) ∗ + ( ∀ (z:nat), own γ2 (●F z) ={E∖↑N}=∗ + own γ2 (●F (z+n)) ∗ Q z) + }}} incr_counter_tape2 c #lbl:α @ E - {{{ (z:nat), RET (#z, #n); Q z ∗ α ◯↪N (true, ns) @ γ2}}}. + {{{ (z:nat), RET (#z, #n); + (flip_tapes_frag (L:=L) γ1 α (expander ns) ∗ ⌜Forall (λ x, x<4) ns⌝) ∗ Q z }}}. Proof. - iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP & Hα) HΦ". + iIntros (Hsubset Φ) "((#Hinv & #Hinv') & [Hα %] & Hvs) HΦ". rewrite /incr_counter_tape2. wp_pures. - wp_bind (rand(_) _)%E. - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - iDestruct (hocap_tapes_agree' with "[$][$]") as "%". - erewrite <-(insert_delete m) at 1; last done. - rewrite big_sepM_insert; last apply lookup_delete. - simpl. - iDestruct "H3" as "[Htape H3]". - wp_apply (wp_rand_tape with "[$]"). - iIntros "[Htape %H1]". - iMod (hocap_tapes_pop1' with "[$][$]") as "[H4 Hα]". - iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". - { iSplitL; last done. - erewrite <-(insert_delete m) at 2; last done. - iNext. - rewrite insert_insert. - rewrite big_sepM_insert; last apply lookup_delete. iFrame. - } - iModIntro. + wp_apply (flip_tape_spec_some with "[$]") as "Hα". + { by apply nclose_subseteq'. } + wp_apply (conversion.wp_bool_to_int) as "_"; first done. wp_pures. - clear -Hsubset H1. - wp_bind (rand(_) _)%E. - iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - iDestruct (hocap_tapes_agree' with "[$][$]") as "%". - erewrite <-(insert_delete m) at 1; last done. - rewrite big_sepM_insert; last apply lookup_delete. - simpl. - iDestruct "H3" as "[Htape H3]". - wp_apply (wp_rand_tape with "[$]"). - iIntros "[Htape %H2]". - iMod (hocap_tapes_pop2' with "[$][$]") as "[H4 Hα]". - iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". - { iSplitL; last done. - erewrite <-(insert_delete m) at 2; last done. - iNext. - rewrite insert_insert. - rewrite big_sepM_insert; last apply lookup_delete. iFrame. - } - iModIntro. + wp_apply (flip_tape_spec_some with "[$]") as "Hα". + { by apply nclose_subseteq'. } + wp_apply (conversion.wp_bool_to_int) as "_"; first done. wp_pures. - clear -Hsubset H1 H2. wp_bind (FAA _ _). - iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - wp_faa. + iInv "Hinv'" as ">(%&%&->&?&?)" "Hclose". + wp_faa. simpl. + iMod (fupd_mask_subseteq (E ∖ ↑N)) as "Hclose'". + { apply difference_mono; [done|by apply nclose_subseteq']. } iMod ("Hvs" with "[$]") as "[H6 HQ]". + replace 2%Z with (Z.of_nat 2%nat) by done. + replace (_*_+_)%Z with (Z.of_nat n); last first. + { assert (n<4). + - by eapply (@Forall_inv _ (λ x, x<4)). + - by apply expander_eta. + } replace (#(z+n)) with (#(z+n)%nat); last first. { by rewrite Nat2Z.inj_add. } - replace 2%Z with (Z.of_nat 2%nat) by done. - rewrite -Nat2Z.inj_mul -Nat2Z.inj_add -Nat.div2_odd -Nat2Z.inj_add. - iMod ("Hclose" with "[$H1 $H2 $H3 $H4 H5 $H6]") as "_"; first by iFrame. - iModIntro. wp_pures. + iMod "Hclose'" as "_". + iMod ("Hclose" with "[-HΦ HQ Hα]") as "_"; first by iFrame. + iModIntro. + wp_pures. iApply "HΦ". - by iFrame. + iFrame. + iPureIntro. + by eapply Forall_inv_tail. Qed. - Lemma counter_presample_spec2 NS E ns α - (ε2 : R -> nat -> R) - (P : iProp Σ) T γ1 γ2 γ3 c: - ↑NS ⊆ E -> - (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> - (∀ (ε:R), 0<= ε ->SeriesC (λ n, if (bool_decide (n≤3%nat)) then 1 / (S 3%nat) * ε2 ε n else 0%R)%R <= ε)%R-> - inv NS (counter_inv_pred2 c γ1 γ2 γ3) -∗ - (□∀ (ε:R) n, (P ∗ ●↯ ε@ γ1) ={E∖↑NS}=∗ - (⌜(1<=ε2 ε n)%R⌝ ∨(●↯ (ε2 ε n) @ γ1 ∗ T (n)))) - -∗ - P -∗ α ◯↪N (true, ns) @ γ2 -∗ - wp_update E (∃ n, T (n) ∗ α◯↪N (true, ns++[n]) @ γ2). + Lemma counter_tapes_presample2 N E γ1 γ2 c α ns ε (ε2 : fin 4%nat -> R): + ↑N ⊆ E -> + (∀ x, 0<=ε2 x)%R -> + (SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R -> + is_counter2 N c γ1 γ2 -∗ + (flip_tapes_frag (L:=L) γ1 α (expander ns) ∗ ⌜Forall (λ x, x<4) ns⌝) -∗ + ↯ ε -∗ + state_update E (∃ n, ↯ (ε2 n) ∗ + (flip_tapes_frag (L:=L) γ1 α (expander (ns++[fin_to_nat n])) ∗ ⌜Forall (λ x, x<4) (ns++[fin_to_nat n])⌝)). Proof. - 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 & -> & H5 & H6) Hclose]"; [done|]. - iDestruct (hocap_tapes_agree' with "[$][$]") as "%". - erewrite <-(insert_delete m) at 1; last done. - rewrite big_sepM_insert; last apply lookup_delete. - simpl. - iDestruct "H3" as "[Htape H3]". - iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%H1)". - 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'". - iApply (state_step_coupl_iterM_state_adv_comp_con_prob_lang 2%nat); first done. - pose (f (l:list (fin 2)) := (match l with - | x::[x'] => 2*fin_to_nat x + fin_to_nat x' - | _ => 0 - end)). - unshelve iExists - (λ l, mknonnegreal (ε2 ε1' (f l) ) _). - { apply Hpos; simpl. auto. } - simpl. - iSplit. - { iPureIntro. - etrans; last apply Hineq; last auto. - pose (k:=(λ n, 1 / ((1 + 1) * ((1 + 1) * 1)) * ε2 ε1' (f n))%R). - erewrite (SeriesC_ext _ (λ x, if bool_decide (x ∈ enum_uniform_list 1%nat 2%nat) - then k x else 0%R))%R; last first. - - intros. case_bool_decide as K. - + rewrite elem_of_enum_uniform_list in K. by rewrite K /k. - + rewrite elem_of_enum_uniform_list in K. - case_match eqn:K'; [by rewrite Nat.eqb_eq in K'|done]. - - rewrite SeriesC_list; last apply NoDup_enum_uniform_list. - rewrite /k /=. rewrite SeriesC_nat_bounded'/=. lra. - } - iIntros (sample ?). - destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' (f 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 *. lra. - } - iApply state_step_coupl_ret. - unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 ε1' (f sample)) _) with "Hε_supply") as "[Hε_supply Hε]". - { apply Hpos. apply cond_nonneg. } - { simpl. done. } - assert (Nat.div2 (f sample)<2)%nat as K1. - { rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound. rewrite /f. - simpl. repeat case_match; try lia. pose proof fin_to_nat_lt t. pose proof fin_to_nat_lt t0. lia. - } - rewrite -H1. - iMod (tapeN_update_append _ _ _ _ (nat_to_fin K1) with "[$][$]") as "[Htapes Htape]". - assert (Nat.b2n (Nat.odd (f sample))<2)%nat as K2. - { edestruct (Nat.odd _); simpl; lia. } - rewrite -(list_fmap_singleton (fin_to_nat)) -fmap_app. - iMod (tapeN_update_append _ _ _ _ (nat_to_fin K2) with "[$][$]") as "[Htapes Htape]". - iMod (hocap_tapes_presample' _ _ _ _ _ (f sample) with "[$][$]") as "[H4 Hfrag]". - iMod "Hclose'" as "_". - iMod ("Hvs" with "[$]") as "[%|[H2 HT]]". - { iExFalso. iApply (ec_contradict with "[$]"). exact. } - rewrite insert_insert. - rewrite fmap_app -!app_assoc /=. - assert (([nat_to_fin K1;nat_to_fin K2]) = sample) as K. - { destruct sample as [|x xs]; first done. - destruct xs as [|x' xs]; first done. - destruct xs as [|]; last done. - pose proof fin_to_nat_lt x. pose proof fin_to_nat_lt x'. - repeat f_equal; apply fin_to_nat_inj; rewrite fin_to_nat_to_fin. - - rewrite /f. rewrite Nat.div2_div. - rewrite Nat.mul_comm Nat.div_add_l; last lia. rewrite Nat.div_small; lia. - - rewrite /f. rewrite Nat.add_comm Nat.odd_add_even. - + destruct (fin_to_nat x') as [|[|]]; simpl; lia. - + by econstructor. - } - iMod ("Hclose" with "[$Hε $H2 Htape H3 $H4 $H5 $H6]") as "_". - { iNext. iSplit; last done. - rewrite big_sepM_insert_delete; iFrame. - simpl. rewrite !fin_to_nat_to_fin. - rewrite /expander bind_app -/(expander ns). simpl. by rewrite H1. - } - iApply fupd_mask_intro_subseteq; first set_solver. - rewrite K. - iFrame. + iIntros (Hsubset Hpos Hineq) "[#Hinv #Hinv'] [Hfrag %Hforall] Herr". + iMod (flip_tapes_presample _ _ _ _ _ _ (λ b, 1/2 *if b then (ε2 2%fin + ε2 3%fin) else (ε2 0%fin + ε2 1%fin))%R with "[//][$][$]") as "(%b & Herr & Hfrag)"; first by apply nclose_subseteq'. + { intros []; apply Rmult_le_pos; try lra. + all: by apply Rplus_le_le_0_compat. } + { etrans; last exact. + rewrite SeriesC_finite_foldr/=. lra. } + destruct b. + - iMod (flip_tapes_presample _ _ _ _ _ _ (λ b, if b then ε2 3%fin else ε2 2%fin)%R with "[//][$][$]") as "(%b & Herr & Hfrag)"; first by apply nclose_subseteq'. + { intros []; by try lra. } + { simpl. lra. } + destruct b. + + iFrame. rewrite /expander bind_app -!app_assoc/=. + rewrite Nat.OddT_odd; last (constructor 1 with (x:=1); lia). iFrame. + iPureIntro. + rewrite Forall_app; naive_solver. + + iFrame. rewrite /expander bind_app -!app_assoc/=. + rewrite Nat.odd_2. iFrame. + iPureIntro. + rewrite Forall_app; naive_solver. + - iMod (flip_tapes_presample _ _ _ _ _ _ (λ b, if b then ε2 1%fin else ε2 0%fin)%R with "[//][$][$]") as "(%b & Herr & Hfrag)"; first by apply nclose_subseteq'. + { intros []; by try lra. } + { simpl. lra. } + destruct b. + + iFrame. rewrite /expander bind_app -!app_assoc/=. + rewrite Nat.OddT_odd; last (constructor 1 with (x:=0); lia). iFrame. + iPureIntro. + rewrite Forall_app; naive_solver. + + iFrame. rewrite /expander bind_app -!app_assoc/=. + rewrite Nat.odd_0. iFrame. + iPureIntro. + rewrite Forall_app; split; first done. + rewrite Forall_singleton. lia. Qed. - - Lemma read_counter_spec2 N E c γ1 γ2 γ3 P Q: + + Lemma read_counter_spec2 N E c γ1 γ2 Q: ↑N ⊆ E -> - {{{ inv N (counter_inv_pred2 c γ1 γ2 γ3) ∗ - □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗ - own γ3 (●F z)∗ Q z) - ∗ P + {{{ is_counter2 N c γ1 γ2 ∗ + (∀ (z:nat), own γ2 (●F z) ={E∖↑N}=∗ + own γ2 (●F z) ∗ Q z) + }}} read_counter2 c @ E {{{ (n':nat), RET #n'; Q n' }}}. Proof. - iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP) HΦ". + iIntros (Hsubset Φ) "((#Hinv & #Hinv') & Hvs) HΦ". rewrite /read_counter2. wp_pure. - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + iInv "Hinv'" as ">(%l&%z & -> & Hloc & Hcont)" "Hclose". wp_load. - iMod ("Hvs" with "[$]") as "[H6 HQ]". - iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]"); first done. - iApply ("HΦ" with "[$]"). + iMod (fupd_mask_subseteq (E ∖ ↑N)) as "Hclose'". + { apply difference_mono_l. by apply nclose_subseteq'. } + iMod ("Hvs" with "[$]") as "[Hcont HQ]". + iMod "Hclose'". + iMod ("Hclose" with "[ $Hloc $Hcont]"); first done. + iApply "HΦ". by iFrame. Qed. End impl2. -Program Definition random_counter2 `{!conerisGS Σ}: random_counter := +Program Definition counterG2_to_flipG `{conerisGS Σ, !flip_spec, !counterG2 Σ} : flipG Σ. +Proof. + eapply counterG2_flipG. +Qed. + +Program Definition random_counter2 `{flip_spec Σ}: random_counter := {| new_counter := new_counter2; allocate_tape:= allocate_tape2; incr_counter_tape := incr_counter_tape2; read_counter:=read_counter2; counterG := counterG2; - error_name := gname; - tape_name := gname; + tape_name := flip_tape_name; counter_name :=gname; - is_counter _ N c γ1 γ2 γ3 := inv N (counter_inv_pred2 c γ1 γ2 γ3); - counter_error_auth _ γ x := ●↯ x @ γ; - counter_error_frag _ γ x := ◯↯ x @ γ; - counter_tapes_auth _ γ m := (●((λ ns, (true, ns))<$>m)@γ)%I; - counter_tapes_frag _ γ α ns := (α◯↪N (true, ns) @ γ)%I; + is_counter _ N c γ1 γ2 := is_counter2 N c γ1 γ2; + counter_tapes_auth K γ m := (flip_tapes_auth (L:=counterG2_to_flipG) γ ((λ ns, expander ns)<$>m) ∗ ⌜map_Forall (λ _ ns, Forall (λ x, x<4) ns) m⌝)%I; + counter_tapes_frag K γ α ns := (flip_tapes_frag (L:=counterG2_to_flipG) γ α (expander ns) ∗ ⌜Forall (λ x, x<4) ns⌝)%I; counter_content_auth _ γ z := own γ (●F z); counter_content_frag _ γ f z := own γ (◯F{f} z); + counter_tapes_presample _ := counter_tapes_presample2; new_counter_spec _ := new_counter_spec2; allocate_tape_spec _ :=allocate_tape_spec2; incr_counter_tape_spec_some _ :=incr_counter_tape_spec_some2; - counter_presample_spec _ :=counter_presample_spec2; read_counter_spec _ :=read_counter_spec2 |}. Next Obligation. simpl. - iIntros (??????) "(%&<-&H1)(%&<-&H2)". - iCombine "H1 H2" gives "%H". by rewrite excl_auth.excl_auth_auth_op_valid in H. -Qed. -Next Obligation. - simpl. - iIntros (??????) "(%&<-&H1)(%&<-&H2)". - iCombine "H1 H2" gives "%H". by rewrite excl_auth.excl_auth_frag_op_valid in H. + iIntros (???????) "[H1 ?] [H2 ?]". + iApply (flip_tapes_auth_exclusive with "[$][$]"). Qed. Next Obligation. simpl. - iIntros (?????) "H". - iApply (hocap_error_auth_pos with "[$]"). + iIntros (????????) "[??] [??]". + iApply (flip_tapes_frag_exclusive with "[$][$]"). Qed. Next Obligation. simpl. - iIntros (?????) "H". - iApply (hocap_error_frag_pos with "[$]"). + iIntros (????????) "[Hauth %H0] [Hfrag %]". + iDestruct (flip_tapes_agree γ α ((λ ns0 : list nat, expander ns0) <$> m) (expander ns) with "[$][$]") as "%K". + iPureIntro. + rewrite lookup_fmap_Some in K. destruct K as (?&K1&?). + replace ns with x; first done. + apply expander_inj; try done. + by eapply map_Forall_lookup_1 in H0. Qed. Next Obligation. simpl. - iIntros (??????) "H1 H2". - iApply (hocap_error_agree with "[$][$]"). -Qed. -Next Obligation. - simpl. iIntros (???????) "??". - iApply (hocap_error_update with "[$][$]"). + iIntros (???????) "[? %]". + iPureIntro. + eapply Forall_impl; first done. + simpl. lia. Qed. Next Obligation. simpl. - iIntros (??????) "H1 H2". - by iDestruct (ghost_map_auth_valid_2 with "[$][$]") as "[%H _]". + iIntros (??????????) "[H1 %] [H2 %]". + iMod (flip_tapes_update with "[$][$]") as "[??]". + iFrame. + iModIntro. + rewrite fmap_insert. iFrame. + iPureIntro. split. + - apply map_Forall_insert_2; last done. + eapply Forall_impl; first done. simpl; lia. + - eapply Forall_impl; first done. + simpl; lia. 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. + iCombine "H1 H2" gives "%K". by rewrite auth_auth_op_valid in K. Qed. Next Obligation. - simpl. - iIntros. - iDestruct (hocap_tapes_agree' with "[$][$]") as "%H". - rewrite lookup_fmap_Some in H. destruct H as (?&?&?). - by simplify_eq. -Qed. -Next Obligation. - iIntros. - iDestruct (hocap_tapes_presample' with "[$][$]") as ">[? $]". - by rewrite fmap_insert. -Qed. -Next Obligation. - simpl. - iIntros (??????) "H1 H2". - iCombine "H1 H2" gives "%H". by rewrite auth_auth_op_valid in H. -Qed. -Next Obligation. - simpl. iIntros (???? z z' ?) "H1 H2". - iCombine "H1 H2" gives "%H". - apply frac_auth_included_total in H. iPureIntro. + simpl. iIntros (????? z z' ?) "H1 H2". + iCombine "H1 H2" gives "%K". + apply frac_auth_included_total in K. iPureIntro. by apply nat_included. Qed. Next Obligation. simpl. - iIntros (????????). + iIntros (?????????). rewrite frac_auth_frag_op. by rewrite own_op. Qed. Next Obligation. - simpl. iIntros (??????) "H1 H2". - iCombine "H1 H2" gives "%H". + simpl. iIntros (???????) "H1 H2". + iCombine "H1 H2" gives "%K". iPureIntro. - by apply frac_auth_agree_L in H. + by apply frac_auth_agree_L in K. Qed. Next Obligation. - simpl. iIntros (????????) "H1 H2". + simpl. iIntros (?????????) "H1 H2". iMod (own_update_2 _ _ _ (_ ⋅ _) with "[$][$]") as "[$$]"; last done. apply frac_auth_update. apply nat_local_update. lia. Qed. - + diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index 0abb395d..45799aa6 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -1,404 +1,297 @@ From iris.algebra Require Import frac_auth. From iris.base_logic.lib Require Import invariants. -From clutch.coneris Require Import coneris hocap random_counter. +From clutch.coneris Require Import coneris hocap hocap_rand random_counter. Set Default Proof Using "Type*". Section filter. - Definition filter_f (n:nat):= bool_decide (n<4)%nat. + Definition filter_f (n:nat):= (n<4)%nat. Definition filtered_list (l:list _) := filter filter_f l. -End filter. -Section lemmas. - Context `{!conerisGS Σ}. - Lemma hocap_tapes_notin3 α N ns (m:gmap loc (nat*list nat)) : - α ↪N (N; ns) -∗ ([∗ map] α↦t ∈ m,∃ (ls:list nat), ⌜ (filter filter_f ls) = t.2⌝ ∗ α ↪N ( 4%nat ; ls)) -∗ ⌜m!!α=None ⌝. + Lemma Forall_filter_f ns: + Forall (λ x : nat, x ≤ 3) ns -> filter filter_f ns = ns. Proof. - destruct (m!!α) eqn:Heqn; last by iIntros. - iIntros "Hα Hmap". - iDestruct (big_sepM_lookup with "[$]") as "(%&%&?)"; first done. - iExFalso. - iApply (tapeN_tapeN_contradict with "[$][$]"). - Qed. -End lemmas. + induction ns; first done. + intros H. + rewrite Forall_cons in H. destruct H. + rewrite filter_cons_True; first f_equal; first naive_solver. + rewrite /filter_f. lia. + Qed. +End filter. Section impl3. + Context `{H:conerisGS Σ, r1:@rand_spec Σ H, L:randG Σ, !inG Σ (frac_authR natR)}. Definition new_counter3 : val:= λ: "_", ref #0. - Definition allocate_tape3 : val := λ: "_", AllocTape #4. + Definition allocate_tape3 : val := λ: "_", rand_allocate_tape #4%nat. Definition incr_counter_tape3 :val := rec: "f" "l" "α":= - let: "n" := rand("α") #4 in + let: "n" := rand_tape "α" #4%nat in if: "n" < #4 then (FAA "l" "n", "n") else "f" "l" "α". Definition read_counter3 : val := λ: "l", !"l". - Class counterG3 Σ := CounterG3 { counterG2_error::hocap_errorGS Σ; - counterG2_tapes:: hocap_tapesGS Σ; - counterG2_frac_authR:: inG Σ (frac_authR natR) }. + Class counterG3 Σ := CounterG3 { counterG3_randG:randG Σ; + counterG3_frac_authR:: inG Σ (frac_authR natR) }. - Context `{!conerisGS Σ, !hocap_errorGS Σ, !hocap_tapesGS Σ, !inG Σ (frac_authR natR)}. - Definition counter_inv_pred3 (c:val) γ1 γ2 γ3:= - (∃ (ε:R) (m:gmap loc (nat * list nat)) (l:loc) (z:nat), - ↯ ε ∗ ●↯ ε @ γ1 ∗ - ([∗ map] α ↦ t ∈ m, ∃ (ls:list nat), ⌜ (filter filter_f ls) = t.2⌝ ∗ α ↪N ( 4%nat ; ls) ) - ∗ ●m@γ2 ∗ - ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ3 (●F z) - )%I. + Definition counter_inv_pred3 (c:val) γ2:= (∃ (l:loc) (z:nat), ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ2 (●F z) )%I. - Lemma new_counter_spec3 E ε N: - {{{ ↯ ε }}} + Definition is_counter3 N (c:val) γ1 γ2:= + ((is_rand (L:=L) (N.@"rand") γ1) ∗ + inv (N.@"counter") (counter_inv_pred3 c γ2))%I. + + Lemma new_counter_spec3 E N: + {{{ True }}} new_counter3 #() @ E {{{ (c:val), RET c; - ∃ γ1 γ2 γ3, inv N (counter_inv_pred3 c γ1 γ2 γ3) ∗ - ◯↯ε @ γ1 ∗ own γ3 (◯F 0%nat) + ∃ γ1 γ2, is_counter3 N c γ1 γ2 ∗ own γ2 (◯F 0%nat) }}}. Proof. rewrite /new_counter3. - iIntros (Φ) "Hε HΦ". + iIntros (Φ) "_ HΦ". wp_pures. + iMod (rand_inv_create_spec) as "(%γ1 & #Hinv)". wp_alloc l as "Hl". - iDestruct (ec_valid with "[$]") as "%". - unshelve iMod (hocap_error_alloc (mknonnegreal ε _)) as "[%γ1 [H1 H2]]". - { lra. } - simpl. - iMod (hocap_tapes_alloc (∅:gmap _ _)) as "[%γ2 [H3 H4]]". - iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as "[%γ3[H5 H6]]". + iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as "[%γ2[H5 H6]]". { by apply frac_auth_valid. } replace (#0) with (#0%nat) by done. - iMod (inv_alloc N _ (counter_inv_pred3 (#l) γ1 γ2 γ3) with "[$Hε $Hl $H1 $H3 $H5]") as "#Hinv". - { iSplit; last done. by iApply big_sepM_empty. } + iMod (inv_alloc _ _ (counter_inv_pred3 (#l) γ2) with "[$Hl $H5]") as "#Hinv'"; first done. iApply "HΦ". - iExists _, _, _. by iFrame. + iFrame. + iModIntro. + iExists _. by iSplit. Qed. - Lemma allocate_tape_spec3 N E c γ1 γ2 γ3: + Lemma allocate_tape_spec3 N E c γ1 γ2: ↑N ⊆ E-> - {{{ inv N (counter_inv_pred3 c γ1 γ2 γ3) }}} + {{{ is_counter3 N c γ1 γ2 }}} allocate_tape3 #() @ E {{{ (v:val), RET v; - ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ α ◯↪N (3%nat; []) @ γ2 + ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ (∃ ls, ⌜filter filter_f ls = []⌝ ∗ rand_tapes_frag (L:=L) γ1 α (4, ls)) }}}. Proof. - iIntros (Hsubset Φ) "#Hinv HΦ". + iIntros (Hsubset Φ) "[#Hinv #Hinv'] HΦ". rewrite /allocate_tape3. wp_pures. - wp_alloctape α as "Hα". - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - iDestruct (hocap_tapes_notin3 with "[$][$]") as "%". - iMod (hocap_tapes_new with "[$]") as "[H4 H7]"; first done. - iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Hα]") as "_". - { iNext. iSplitL; last done. - rewrite big_sepM_insert; [simpl; iFrame|done]. - by rewrite filter_nil. - } + wp_apply rand_allocate_tape_spec as (v) "(%α & -> & Hfrag)"; [by eapply nclose_subseteq'|done|]. iApply "HΦ". by iFrame. Qed. - Lemma incr_counter_tape_spec_some3 N E c γ1 γ2 γ3 (P: iProp Σ) (Q:nat->iProp Σ) (α:loc) (n:nat) ns: - ↑N⊆E -> - {{{ inv N (counter_inv_pred3 c γ1 γ2 γ3) ∗ - □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗ - own γ3 (●F(z+n)%nat)∗ Q z) ∗ - P ∗ α ◯↪N (3%nat; n::ns) @ γ2 + Lemma incr_counter_tape_spec_some3 N E c γ1 γ2 (Q:nat->iProp Σ) (α:loc) n ns: + ↑N⊆E -> + {{{ is_counter3 N c γ1 γ2 ∗ + (∃ ls, ⌜filter filter_f ls = n::ns⌝ ∗ rand_tapes_frag (L:=L) γ1 α (4, ls)) ∗ + ( ∀ (z:nat), own γ2 (●F z) ={E∖↑N}=∗ + own γ2 (●F (z+n)) ∗ Q z) + }}} incr_counter_tape3 c #lbl:α @ E - {{{ (z:nat), RET (#z, #n); Q z ∗ α ◯↪N (3%nat; ns) @ γ2}}}. + {{{ (z:nat), RET (#z, #n); + (∃ ls, ⌜filter filter_f ls = ns⌝ ∗ rand_tapes_frag (L:=L) γ1 α (4, ls)) ∗ + Q z }}}. Proof. - iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP & Hα) HΦ". + iIntros (Hsubset Φ) "([#Hinv #Hinv'] & (%ls & %Hfilter & Hfrag) & Hvs) HΦ". rewrite /incr_counter_tape3. - iLöb as "IH". + iLöb as "IH" forall (ls Hfilter Φ) "Hfrag". wp_pures. - wp_bind (rand(_) _)%E. - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". - iDestruct (hocap_tapes_agree with "[$][$]") as "%". - erewrite <-(insert_delete m) at 1; last done. - rewrite big_sepM_insert; last apply lookup_delete. - simpl. - iDestruct "H3" as "[(%ls & %Hls & Htape) H3]". - destruct ls as [|x ls]. - { rewrite filter_nil in Hls. simplify_eq. } - wp_apply (wp_rand_tape with "[$]") as "[Htape %Hineq]". - rewrite Nat.le_lteq in Hineq. - destruct Hineq as [? | ->]. - - (* first value is valid *) - iMod (hocap_tapes_pop with "[$][$]") as "[H4 Hα]". - rewrite filter_cons /filter_f in Hls. - rewrite bool_decide_eq_true_2 in Hls; last done. simpl in *. - simplify_eq. - iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". - { iSplitL; last done. - erewrite <-(insert_delete m) at 2; last done. - iNext. - rewrite insert_insert. - rewrite big_sepM_insert; last apply lookup_delete. by iFrame. - } - iModIntro. - wp_pures. - rewrite bool_decide_eq_true_2; last lia. - clear -Hsubset. - wp_pures. + destruct ls as [|hd ls]; first simplify_eq. + wp_apply (rand_tape_spec_some with "[$]") as "Hfrag"; first by eapply nclose_subseteq'. + wp_pures. + case_bool_decide as K. + - wp_pures. wp_bind (FAA _ _). - iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + iInv "Hinv'" as ">(%&%&-> & ?&?)" "Hclose". wp_faa. - iMod ("Hvs" with "[$]") as "[H6 HQ]". - replace (#(z+n)) with (#(z+n)%nat); last first. - { by rewrite Nat2Z.inj_add. } - iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. - iModIntro. wp_pures. - iApply "HΦ". - by iFrame. - - (* we get a 5, do iLöb induction *) - rewrite filter_cons /filter_f in Hls. - rewrite bool_decide_eq_false_2 in Hls; last lia. simpl in *. - iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". - { iSplitL; last done. - erewrite <-(insert_delete m) at 2; last done. - iNext. - rewrite big_sepM_insert; last apply lookup_delete. by iFrame. - } - iModIntro. - do 4 wp_pure. - by iApply ("IH" with "[$][$]"). - Qed. + iMod (fupd_mask_subseteq (E ∖ ↑N)) as "Hclose'". + + apply difference_mono_l. + by apply nclose_subseteq'. + + iMod ("Hvs" with "[$]") as "[? HQ]". + iMod "Hclose'" as "_". + rewrite -Nat2Z.inj_add. + rewrite filter_cons_True in Hfilter; last (rewrite /filter_f; lia). + simplify_eq. + iMod ("Hclose" with "[-HQ Hfrag HΦ]") as "_"; first by iFrame. + iModIntro. + wp_pures. + iApply "HΦ". by iFrame. + - wp_pure. + iApply ("IH" with "[][$][$][$]"). + iPureIntro. + rewrite filter_cons_False in Hfilter; first done. + rewrite /filter_f. lia. + Qed. - Lemma counter_presample_spec3 NS E ns α - (ε2 : R -> nat -> R) - (P : iProp Σ) T γ1 γ2 γ3 c: - ↑NS ⊆ E -> - (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> - (∀ (ε:R), 0<= ε ->SeriesC (λ n, if (bool_decide (n≤3%nat)) then 1 / (S 3%nat) * ε2 ε n else 0%R)%R <= ε)%R-> - inv NS (counter_inv_pred3 c γ1 γ2 γ3) -∗ - (□∀ (ε:R) n, (P ∗ ●↯ ε@ γ1) ={E∖↑NS}=∗ - (⌜(1<=ε2 ε n)%R⌝ ∨(●↯ (ε2 ε n) @ γ1 ∗ T (n)))) - -∗ - P -∗ α ◯↪N (3%nat; ns) @ γ2 -∗ - wp_update E (∃ n, T (n) ∗ α◯↪N (3%nat; ns++[n]) @ γ2). + Lemma counter_tapes_presample3 N E γ1 γ2 c α ns ε (ε2 : fin 4%nat -> R): + ↑N ⊆ E -> + (∀ x, 0<=ε2 x)%R -> + (SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R -> + is_counter3 N c γ1 γ2 -∗ + (∃ ls, ⌜filter filter_f ls = ns⌝ ∗ rand_tapes_frag (L:=L) γ1 α (4, ls)) -∗ + ↯ ε -∗ + state_update E (∃ n, ↯ (ε2 n) ∗ + (∃ ls, ⌜filter filter_f ls = (ns++[fin_to_nat n])⌝ ∗ rand_tapes_frag (L:=L) γ1 α (4, ls))). Proof. - iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". - iMod wp_update_epsilon_err as "(%epsilon_err&%H&?)". - iApply wp_update_state_step_coupl. - iRevert "HP Hfrag". - iApply (ec_ind_amp _ 5%R with "[][$]"); [done|lra|]. + iIntros (Hsubset Hpos Hineq) "[#Hinv #Hinv'] Hfrag Herr". + iMod (state_update_epsilon_err) as "(%ep & %Heps & Heps)". + iRevert "Hfrag Herr". + iApply (ec_ind_amp _ (5/4)%R with "[][$]"); try lra. + clear ep Heps. iModIntro. - clear epsilon_err H. - iIntros (epsilon_err ?) "#IH Hepsilon_err HP Hfrag". - iIntros (σ ε) "((Hheap&Htapes)&Hε)". - iMod (inv_acc with "Hinv") as "[>(%ε0 & % & % & % & H1 & H2 & H3 & H4 & -> & H5 & H6) Hclose]"; [done|]. - iDestruct (hocap_tapes_agree with "[$][$]") as "%". - erewrite <-(insert_delete m) at 1; last done. - rewrite big_sepM_insert; last apply lookup_delete. - simpl. - iDestruct "H3" as "[(%ls & %Hls & Htape) H3]". - iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%)". - iDestruct (ec_valid with "H1") as "%". - iDestruct (ec_combine with "[$]") as "Htotal". - 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'". - pose (ε2' := λ (x:nat), (if bool_decide (x<=3)%nat then ε2 ε0 x else - if bool_decide (x=4)%nat then ε0 + 5 * epsilon_err - else 0)%R - ). - iApply state_step_coupl_state_adv_comp_con_prob_lang; first done. - assert (forall x, 0<=ε2' x)%R. - { intros. rewrite /ε2'. repeat case_bool_decide; try done; first naive_solver. - apply Rplus_le_le_0_compat; simpl; [naive_solver|lra]. } - unshelve iExists (λ x, mknonnegreal (ε2' x) _); auto. - iSplit. - { iPureIntro. - unshelve epose proof (Hineq ε0 _) as H'; first (by naive_solver). - rewrite SeriesC_nat_bounded_fin in H'. - replace (INR 5%nat) with 5%R by (simpl; lra). - replace (INR 4%nat) with 4%R in H' by (simpl; lra). - rewrite /=/ε2' Hε1'. - rewrite SeriesC_finite_foldr/=. - rewrite SeriesC_finite_foldr/= in H'. - lra. + iIntros (eps Heps) "#IH Heps (%ls & %Hfilter & Hfrag) Herr". + iDestruct (ec_valid with "[$]") as "%". + iCombine "Heps Herr" as "Herr'". + iMod (rand_tapes_presample _ _ _ _ _ _ _ + (λ x, match decide (fin_to_nat x < 4)%nat with + | left p => ε2 (nat_to_fin p) + | _ => ε + 5/4*eps + end + )%R with "[//][$][$]") as "(%n & Herr & Hfrag)"; first by apply nclose_subseteq'. + { intros. case_match; first done. + apply Rplus_le_le_0_compat; first naive_solver. + apply Rmult_le_pos; lra. } - iIntros (sample). - simpl. - destruct (Rlt_decision (nonneg ε_rem + (ε2' 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 *. lra. + { rewrite SeriesC_finite_foldr/=. + rewrite SeriesC_finite_foldr/= in Hineq. + lra. } - destruct (Nat.lt_total (fin_to_nat sample) 4%nat) as [|[|]]. - - (* we sample a value less than 4*) - iApply state_step_coupl_ret. - unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2' sample) _) with "Hε_supply") as "[Hε_supply Hε]"; auto. - iMod (tapeN_update_append _ _ _ _ sample with "[$][$]") as "[Htapes Htape]". - iMod (hocap_tapes_presample _ _ _ _ _ (fin_to_nat sample) with "[$][$]") as "[H4 Hfrag]". - iMod "Hclose'" as "_". - iMod ("Hvs" $! _ (fin_to_nat sample)%nat with "[$]") as "[%|[H2 HT]]". - { iExFalso. iApply (ec_contradict with "[$]"). - simpl. - rewrite /ε2'. - by rewrite bool_decide_eq_true_2; last lia. - } - simpl. - iMod ("Hclose" with "[$Hε H2 Htape H3 $H4 $H5 $H6]") as "_". - { iNext. - rewrite /ε2'. rewrite bool_decide_eq_true_2; last lia. - iFrame. - rewrite big_sepM_insert_delete; iFrame. simpl. iPureIntro. - split; last done. - rewrite filter_app. f_equal. - rewrite filter_cons. - rewrite decide_True; first done. - rewrite /filter_f. by apply bool_decide_pack. - } - iApply fupd_mask_intro_subseteq; first set_solver. + case_match eqn :K. + - (* accept *) + iFrame. + iPureIntro. + rewrite filter_app; f_equal; first done. + rewrite filter_cons /filter_f filter_nil K. + f_equal. by rewrite fin_to_nat_to_fin. + - iDestruct (ec_split with "[$]") as "[Hε Heps]"; first lra. + { apply Rmult_le_pos; lra. } + iApply ("IH" with "[$][Hfrag][$]"). iFrame. - - (* we sampled a 4, and hence löb *) - unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2' sample) _) with "Hε_supply") as "[Hε_supply Hε]"; auto. - iMod (tapeN_update_append _ _ _ _ sample with "[$][$]") as "[Htapes Htape]". - iMod "Hclose'" as "_". - simpl. - rewrite {2}/ε2'. - rewrite bool_decide_eq_false_2; last lia. - rewrite bool_decide_eq_true_2; last lia. - iDestruct (ec_split with "[$]") as "[Hε Hampl]"; simpl; [naive_solver|lra|]. - simpl. - iMod ("Hclose" with "[$Hε $H2 Htape H3 $H4 $H5 $H6]") as "_". - { iNext. - rewrite (big_sepM_delete _ m); [iFrame|done]. - simpl. iPureIntro; split; last done. - rewrite filter_app filter_cons decide_False; simpl. - - by rewrite filter_nil app_nil_r. - - rewrite /filter_f. case_bool_decide; [lia|auto]. - } - iDestruct ("IH" with "[$][$][$]") as "IH'". - by iMod ("IH'" $! (state_upd_tapes <[_:=_]> _) with "[$]") as "IH'". - - pose proof fin_to_nat_lt sample; lia. + iPureIntro. + rewrite filter_app. + rewrite filter_cons_False; first by rewrite filter_nil app_nil_r. + rewrite /filter_f. lia. Qed. - - Lemma read_counter_spec3 N E c γ1 γ2 γ3 P Q: + + Lemma read_counter_spec3 N E c γ1 γ2 Q: ↑N ⊆ E -> - {{{ inv N (counter_inv_pred3 c γ1 γ2 γ3) ∗ - □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗ - own γ3 (●F z)∗ Q z) - ∗ P + {{{ is_counter3 N c γ1 γ2 ∗ + (∀ (z:nat), own γ2 (●F z) ={E∖↑N}=∗ + own γ2 (●F z) ∗ Q z) + }}} read_counter3 c @ E {{{ (n':nat), RET #n'; Q n' }}}. Proof. - iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP) HΦ". + iIntros (Hsubset Φ) "([#Hinv #Hinv'] & Hvs) HΦ". rewrite /read_counter3. wp_pure. - iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + iInv "Hinv'" as ">( %l & %z & -> & H5 & H6)" "Hclose". wp_load. - iMod ("Hvs" with "[$]") as "[H6 HQ]". - iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]"); first done. + iMod (fupd_mask_subseteq (E ∖ ↑N)) as "Hclose'". + { apply difference_mono_l. + by apply nclose_subseteq'. } + iMod ("Hvs" with "[$]") as "[? HQ]". + iMod "Hclose'" as "_". + iMod ("Hclose" with "[-HQ HΦ]"); first by iFrame. iApply ("HΦ" with "[$]"). - Qed. + Qed. -End impl3. - +End impl3. -Program Definition random_counter3 `{!conerisGS Σ}: random_counter := +Program Definition random_counter3 `{F:rand_spec}: random_counter := {| new_counter := new_counter3; allocate_tape:= allocate_tape3; incr_counter_tape := incr_counter_tape3; read_counter:=read_counter3; counterG := counterG3; - error_name := gname; - tape_name := gname; + tape_name := rand_tape_name; counter_name :=gname; - is_counter _ N c γ1 γ2 γ3 := inv N (counter_inv_pred3 c γ1 γ2 γ3); - counter_error_auth _ γ x := ●↯ x @ γ; - counter_error_frag _ γ x := ◯↯ x @ γ; - counter_tapes_auth _ γ m := (●((λ ns, (3, ns))<$>m)@γ)%I; - counter_tapes_frag _ γ α ns := (α◯↪N (3%nat;ns) @ γ)%I; + is_counter _ N c γ1 γ2 := is_counter3 N c γ1 γ2; + counter_tapes_auth _ γ m := (∃ (m':gmap loc (nat*list nat)), + ⌜(dom m = dom m')⌝ ∗ + ⌜∀ l xs' tb, m'!!l=Some (tb, xs') → tb = 4 ∧ m!!l=Some (filter filter_f xs')⌝ ∗ + rand_tapes_auth (L:=counterG3_randG) γ m')%I; + counter_tapes_frag _ γ α ns := + (∃ ls, ⌜filter filter_f ls = ns⌝ ∗ rand_tapes_frag (L:=counterG3_randG) γ α (4, ls))%I; counter_content_auth _ γ z := own γ (●F z); counter_content_frag _ γ f z := own γ (◯F{f} z); + counter_tapes_presample _ := counter_tapes_presample3; new_counter_spec _ := new_counter_spec3; allocate_tape_spec _ :=allocate_tape_spec3; incr_counter_tape_spec_some _ :=incr_counter_tape_spec_some3; - counter_presample_spec _ :=counter_presample_spec3; read_counter_spec _ :=read_counter_spec3 |}. + Next Obligation. simpl. - iIntros (??????) "(%&<-&H1)(%&<-&H2)". - iCombine "H1 H2" gives "%H". by rewrite excl_auth.excl_auth_auth_op_valid in H. + iIntros (???????) "(%&%&%&?) (%&%&%&?)". + iApply (rand_tapes_auth_exclusive with "[$][$]"). Qed. Next Obligation. simpl. - iIntros (??????) "(%&<-&H1)(%&<-&H2)". - iCombine "H1 H2" gives "%H". by rewrite excl_auth.excl_auth_frag_op_valid in H. + iIntros (????????) "(%&%&?) (%&%&?)". + iApply (rand_tapes_frag_exclusive with "[$][$]"). Qed. Next Obligation. simpl. - iIntros (?????) "H". - iApply (hocap_error_auth_pos with "[$]"). + iIntros (????????) "(%&%&%K&?) (%&%&?)". + iDestruct (rand_tapes_agree γ α with "[$][$]") as "%K'". + iPureIntro. + apply K in K'. subst. naive_solver. Qed. Next Obligation. simpl. - iIntros (?????) "H". - iApply (hocap_error_frag_pos with "[$]"). + iIntros (???????) "(%&%&?)". + iPureIntro. + subst. + induction ls; first done. + rewrite filter_cons. + case_decide as H; last done. + rewrite Forall_cons_iff; split; last done. + rewrite /filter_f in H. lia. Qed. Next Obligation. simpl. - iIntros (??????) "H1 H2". - iApply (hocap_error_agree with "[$][$]"). -Qed. -Next Obligation. - simpl. iIntros (???????) "??". - iApply (hocap_error_update with "[$][$]"). + iIntros (??????????) "(%&%&%&?) (%&%&?)". + iMod (rand_tapes_update _ _ _ _ (_,ns') with "[$][$]") as "[??]"; last iFrame. + - eapply Forall_impl; first done. simpl; lia. + - iPureIntro. split; [split; first (rewrite !dom_insert_L; set_solver)|]. + + intros ? xs' ? K. + rewrite lookup_insert_Some in K. + destruct K as [[??]|[??]]; simplify_eq. + * split; first done. + rewrite lookup_insert_Some; left. + split; first done. + by erewrite Forall_filter_f. + * rewrite lookup_insert_ne; last done. + naive_solver. + + by apply Forall_filter_f. 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. + iCombine "H1 H2" gives "%K". by rewrite auth_auth_op_valid in K. Qed. Next Obligation. - simpl. - iIntros. - iDestruct (hocap_tapes_agree with "[$][$]") as "%H". - iPureIntro. - rewrite lookup_fmap_Some in H. destruct H as (?&?&?). - by simplify_eq. -Qed. -Next Obligation. - iIntros. - iMod (hocap_tapes_presample with "[$][$]") as "[??]". - iModIntro. iFrame. - by rewrite fmap_insert. -Qed. -Next Obligation. - simpl. - iIntros (??????) "H1 H2". - iCombine "H1 H2" gives "%H". by rewrite auth_auth_op_valid in H. -Qed. -Next Obligation. - simpl. iIntros (???? z z' ?) "H1 H2". - iCombine "H1 H2" gives "%H". - apply frac_auth_included_total in H. iPureIntro. + simpl. iIntros (????? z z' ?) "H1 H2". + iCombine "H1 H2" gives "%K". + apply frac_auth_included_total in K. iPureIntro. by apply nat_included. Qed. Next Obligation. simpl. - iIntros (????????). + iIntros (?????????). rewrite frac_auth_frag_op. by rewrite own_op. Qed. Next Obligation. - simpl. iIntros (??????) "H1 H2". - iCombine "H1 H2" gives "%H". + simpl. iIntros (???????) "H1 H2". + iCombine "H1 H2" gives "%K". iPureIntro. - by apply frac_auth_agree_L in H. + by apply frac_auth_agree_L in K. Qed. Next Obligation. - simpl. iIntros (????????) "H1 H2". + simpl. iIntros (?????????) "H1 H2". iMod (own_update_2 _ _ _ (_ ⋅ _) with "[$][$]") as "[$$]"; last done. apply frac_auth_update. apply nat_local_update. lia. Qed. - diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v index b2a86280..263b66a7 100644 --- a/theories/coneris/examples/random_counter/random_counter.v +++ b/theories/coneris/examples/random_counter/random_counter.v @@ -14,25 +14,18 @@ Class random_counter `{!conerisGS Σ} := RandCounter (** The assumptions about [Σ] *) counterG : gFunctors → Type; (** [name] is used to associate [locked] with [is_lock] *) - error_name : Type; tape_name: Type; counter_name: Type; (** * Predicates *) is_counter {L : counterG Σ} (N:namespace) (counter: val) - (γ1: error_name) (γ2: tape_name) (γ3: counter_name): iProp Σ; - counter_error_auth {L : counterG Σ} (γ: error_name) (x:R): iProp Σ; - counter_error_frag {L : counterG Σ} (γ: error_name) (x:R): iProp Σ; + (γ1: tape_name) (γ2: counter_name): iProp Σ; counter_tapes_auth {L : counterG Σ} (γ: tape_name) (m:gmap loc (list nat)): iProp Σ; counter_tapes_frag {L : counterG Σ} (γ: tape_name) (α:loc) (ns:list nat): iProp Σ; counter_content_auth {L : counterG Σ} (γ: counter_name) (z:nat): iProp Σ; counter_content_frag {L : counterG Σ} (γ: counter_name) (f:frac) (z:nat): iProp Σ; (** * General properties of the predicates *) - #[global] is_counter_persistent {L : counterG Σ} N c γ1 γ2 γ3 :: - Persistent (is_counter (L:=L) N c γ1 γ2 γ3); - #[global] counter_error_auth_timeless {L : counterG Σ} γ x :: - Timeless (counter_error_auth (L:=L) γ x); - #[global] counter_error_frag_timeless {L : counterG Σ} γ x :: - Timeless (counter_error_frag (L:=L) γ x); + #[global] is_counter_persistent {L : counterG Σ} N c γ1 γ2 :: + Persistent (is_counter (L:=L) N c γ1 γ2); #[global] counter_tapes_auth_timeless {L : counterG Σ} γ m :: Timeless (counter_tapes_auth (L:=L) γ m); #[global] counter_tapes_frag_timeless {L : counterG Σ} γ α ns :: @@ -41,30 +34,27 @@ Class random_counter `{!conerisGS Σ} := RandCounter Timeless (counter_content_auth (L:=L) γ z); #[global] counter_content_frag_timeless {L : counterG Σ} γ f z :: Timeless (counter_content_frag (L:=L) γ f z); - - counter_error_auth_exclusive {L : counterG Σ} γ x1 x2: - counter_error_auth (L:=L) γ x1 -∗ counter_error_auth (L:=L) γ x2 -∗ False; - counter_error_frag_exclusive {L : counterG Σ} γ x1 x2: - counter_error_frag (L:=L) γ x1 -∗ counter_error_frag (L:=L) γ x2 -∗ False; - counter_error_auth_pos {L : counterG Σ} γ x: - counter_error_auth (L:=L) γ x -∗ ⌜(0<=x)%R⌝; - counter_error_auth_frag {L : counterG Σ} γ x: - counter_error_frag (L:=L) γ x -∗ ⌜(0<=x)%R⌝; - counter_error_agree {L : counterG Σ} γ x1 x2: - counter_error_auth (L:=L) γ x1 -∗ counter_error_frag (L:=L) γ x2 -∗ ⌜x1 = x2 ⌝; - counter_error_update {L : counterG Σ} γ x1 x2 (x3:nonnegreal): - counter_error_auth (L:=L) γ x1 -∗ counter_error_frag (L:=L) γ x2 ==∗ - counter_error_auth (L:=L) γ x3 ∗ counter_error_frag (L:=L) γ x3; - + counter_tapes_auth_exclusive {L : counterG Σ} γ m m': counter_tapes_auth (L:=L) γ m -∗ counter_tapes_auth (L:=L) γ m' -∗ False; counter_tapes_frag_exclusive {L : counterG Σ} γ α ns ns': counter_tapes_frag (L:=L) γ α ns -∗ counter_tapes_frag (L:=L) γ α ns' -∗ False; counter_tapes_agree {L : counterG Σ} γ α m ns: - counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝; - counter_tapes_update {L : counterG Σ} γ α m ns n: + counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝; + counter_tapes_valid {L : counterG Σ} γ α ns: + counter_tapes_frag (L:=L) γ α ns -∗ ⌜Forall (λ n, n<=3)%nat ns⌝; + counter_tapes_update {L : counterG Σ} γ α m ns ns': + Forall (λ x, x<=3%nat) ns'-> counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns ==∗ - counter_tapes_auth (L:=L) γ (<[α := (ns ++[n])]> m) ∗ counter_tapes_frag (L:=L) γ α (ns ++ [n]); + counter_tapes_auth (L:=L) γ (<[α := ns']> m) ∗ counter_tapes_frag (L:=L) γ α (ns'); + counter_tapes_presample {L:counterG Σ} N E γ1 γ2 c α ns ε (ε2 : fin 4%nat -> R): + ↑N ⊆ E -> + (∀ x, 0<=ε2 x)%R -> + (SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R -> + is_counter(L:=L) N c γ1 γ2 -∗ + counter_tapes_frag (L:=L) γ1 α (ns) -∗ + ↯ ε -∗ + state_update E (∃ n, ↯ (ε2 n) ∗ counter_tapes_frag (L:=L) γ1 α (ns ++ [fin_to_nat n])); counter_content_auth_exclusive {L : counterG Σ} γ z1 z2: counter_content_auth (L:=L) γ z1 -∗ counter_content_auth (L:=L) γ z2 -∗ False; @@ -80,46 +70,35 @@ Class random_counter `{!conerisGS Σ} := RandCounter counter_content_auth (L:=L) γ (z1+z3)%nat ∗ counter_content_frag (L:=L) γ f (z2+z3)%nat; (** * Program specs *) - new_counter_spec {L : counterG Σ} E ε N: - {{{ ↯ ε }}} new_counter #() @E - {{{ c, RET c; ∃ γ1 γ2 γ3, is_counter (L:=L) N c γ1 γ2 γ3 ∗ - counter_error_frag (L:=L) γ1 ε ∗ - counter_content_frag (L:=L) γ3 1%Qp 0%nat + new_counter_spec {L : counterG Σ} E N: + {{{ True }}} new_counter #() @E + {{{ c, RET c; ∃ γ1 γ2, is_counter (L:=L) N c γ1 γ2 ∗ + counter_content_frag (L:=L) γ2 1%Qp 0%nat }}}; - allocate_tape_spec {L: counterG Σ} N E c γ1 γ2 γ3: + allocate_tape_spec {L: counterG Σ} N E c γ1 γ2: ↑N ⊆ E-> - {{{ is_counter (L:=L) N c γ1 γ2 γ3 }}} + {{{ is_counter (L:=L) N c γ1 γ2 }}} allocate_tape #() @ E {{{ (v:val), RET v; - ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ counter_tapes_frag (L:=L) γ2 α [] + ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ counter_tapes_frag (L:=L) γ1 α [] }}}; - incr_counter_tape_spec_some {L: counterG Σ} N E c γ1 γ2 γ3 (P: iProp Σ) (Q:nat->iProp Σ) (α:loc) (n:nat) ns: - ↑N⊆E -> - {{{ is_counter (L:=L) N c γ1 γ2 γ3 ∗ - □ (∀ (z:nat), P ∗ counter_content_auth (L:=L) γ3 z ={E∖↑N}=∗ - counter_content_auth (L:=L) γ3 (z+n)%nat ∗ Q z) ∗ - P ∗ counter_tapes_frag (L:=L) γ2 α (n::ns) + incr_counter_tape_spec_some {L: counterG Σ} N E c γ1 γ2 (Q:nat->iProp Σ) (α:loc) n ns: + ↑N⊆E -> + {{{ is_counter (L:=L) N c γ1 γ2 ∗ + counter_tapes_frag (L:=L) γ1 α (n::ns) ∗ + ( ∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖↑N}=∗ + counter_content_auth (L:=L) γ2 (z+n) ∗ Q z) + }}} incr_counter_tape c #lbl:α @ E - {{{ (z:nat), RET (#z, #n); Q z ∗ counter_tapes_frag (L:=L) γ2 α ns}}}; - counter_presample_spec {L: counterG Σ} NS E ns α - (ε2 : R -> nat -> R) - (P : iProp Σ) T γ1 γ2 γ3 c: - ↑NS ⊆ E -> - (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> - (∀ (ε:R), 0<= ε ->SeriesC (λ n, if (bool_decide (n≤3%nat)) then 1 / (S 3%nat) * ε2 ε n else 0%R)%R <= ε)%R-> - is_counter (L:=L) NS c γ1 γ2 γ3 -∗ - (□∀ (ε:R) n, (P ∗ counter_error_auth (L:=L) γ1 ε) ={E∖↑NS}=∗ - (⌜(1<=ε2 ε n)%R⌝ ∨ (counter_error_auth (L:=L) γ1 (ε2 ε n) ∗ T (n)))) - -∗ - P -∗ counter_tapes_frag (L:=L) γ2 α ns-∗ - wp_update E (∃ n, T (n) ∗ counter_tapes_frag (L:=L) γ2 α (ns++[n])); - read_counter_spec {L: counterG Σ} N E c γ1 γ2 γ3 P Q: + {{{ (z:nat), RET (#z, #n); counter_tapes_frag (L:=L) γ1 α ns ∗ + Q z }}}; + read_counter_spec {L: counterG Σ} N E c γ1 γ2 Q: ↑N ⊆ E -> - {{{ is_counter (L:=L) N c γ1 γ2 γ3 ∗ - □ (∀ (z:nat), P ∗ counter_content_auth (L:=L) γ3 z ={E∖↑N}=∗ - counter_content_auth (L:=L) γ3 z∗ Q z) - ∗ P + {{{ is_counter (L:=L) N c γ1 γ2 ∗ + (∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖↑N}=∗ + counter_content_auth (L:=L) γ2 z∗ Q z) + }}} read_counter c @ E {{{ (n':nat), RET #n'; Q n' @@ -130,83 +109,114 @@ Class random_counter `{!conerisGS Σ} := RandCounter Section lemmas. Context `{rc:random_counter} {L: counterG Σ}. - Lemma incr_counter_tape_spec_none N E c γ1 γ2 γ3 (ε2:R -> nat -> R) (P: iProp Σ) (T: nat -> iProp Σ) (Q: nat -> nat -> iProp Σ)(α:loc): + Lemma incr_counter_tape_spec_none N E c γ1 γ2 Q α: ↑N ⊆ E-> - (∀ ε n, 0<= ε -> 0<= ε2 ε n)%R-> - (∀ (ε:R), 0<=ε -> ((ε2 ε 0%nat) + (ε2 ε 1%nat)+ (ε2 ε 2%nat)+ (ε2 ε 3%nat))/4 <= ε)%R → - {{{ is_counter (L:=L) N c γ1 γ2 γ3 ∗ - □(∀ (ε:R) (n : nat), P ∗ counter_error_auth (L:=L) γ1 ε - ={E∖↑N}=∗ (⌜(1<=ε2 ε n)%R⌝∨ counter_error_auth (L:=L) γ1 (ε2 ε n) ∗ T n) ) ∗ - □ (∀ (n:nat) (z:nat), T n ∗ counter_content_auth (L:=L) γ3 z ={E∖↑N}=∗ - counter_content_auth (L:=L) γ3 (z+n)%nat ∗ Q z n) ∗ - P ∗ counter_tapes_frag (L:=L) γ2 α [] + {{{ is_counter (L:=L) N c γ1 γ2 ∗ + counter_tapes_frag (L:=L) γ1 α [] ∗ + ( |={E∖↑N, ∅}=> + ∃ ε ε2, + ↯ ε ∗ + ⌜(∀ n, 0<=ε2 n)%R⌝ ∗ + ⌜(((ε2 0%nat) + (ε2 1%nat)+ (ε2 2%nat)+ (ε2 3%nat))/4 <= ε)%R⌝ ∗ + (∀ n, ↯ (ε2 n) ={∅, E∖↑N}=∗ + ∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖↑N}=∗ + counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ε ε2 + ) + ) + }}} incr_counter_tape c #lbl:α @ E - {{{ (z:nat) (n:nat), RET (#z, #n); Q z n ∗ counter_tapes_frag (L:=L) γ2 α [] }}}. + {{{ (z n:nat), RET (#z, #n); counter_tapes_frag (L:=L) γ1 α [] ∗ + ∃ ε ε2, Q z n ε ε2 }}}. Proof. - iIntros (Hsubset Hpos Hineq Φ) "(#Hinv & #Hvs1 & #Hvs2 & HP & Hα) HΦ". - iMod (counter_presample_spec with "[//][//][$][$]") as "(%&HT&Hα)"; try done. - { intros ε Hε. specialize (Hineq ε Hε). - rewrite SeriesC_nat_bounded_fin SeriesC_finite_foldr /=. lra. + iIntros (Hsubset Φ) "(#Hinv & Hfrag & Hvs) HΦ". + iApply (state_update_wp _ (∃ ε ε2 n, + counter_tapes_frag γ1 α [n] ∗ + ∀ z : nat, + counter_content_auth γ2 z ={E ∖ ↑N}=∗ counter_content_auth γ2 (z + n) ∗ Q z n ε ε2) with "[Hvs Hfrag][HΦ]"); last first. + { iIntros "(%ε&%ε2&%n&?&?)". + wp_apply (incr_counter_tape_spec_some _ _ _ _ _ (λ z, Q z n ε ε2) with "[-HΦ]"); [exact|iFrame|]; first by iSplit. + iIntros (?) "[??]". + iApply "HΦ". + iFrame. } - iApply (incr_counter_tape_spec_some _ _ _ _ _ _ (T n) (λ x, Q x n) with "[$Hα $HT]"); try done. - { by iSplit. } - iNext. - iIntros. iApply ("HΦ" with "[$]"). + iMod (fupd_mask_frame _ (↑N) (E∖↑N) ∅ with "[Hvs]") as "H"; first set_solver. + - iMod "Hvs" as "H". + iModIntro. + (* mask change *) + rewrite left_id_L. + replace (_∖(_∖_)) with ((nclose N)); first (iModIntro; iExact "H"). + rewrite difference_difference_r_L. set_solver. + - iDestruct "H" as "(%ε & %ε2 & Herr & %Hpos & %Hineq & Hrest)". + iMod (counter_tapes_presample _ _ _ _ _ _ _ _ (λ x, ε2 (fin_to_nat x)) with "[//][$][$Herr]") as "(%n & Herr & ?)"; try done. + { rewrite SeriesC_finite_foldr/=. lra. } + iModIntro. + iMod (fupd_mask_frame _ (E) ∅ (E∖↑N) with "[Hrest Herr]") as "H"; first set_solver. + + iMod ("Hrest" with "[$]") as "H". iModIntro. + replace (_∖_∪_) with E; first (iModIntro; iExact "H"). + by rewrite difference_empty_L union_comm_L -union_difference_L. + + iModIntro. iFrame. Qed. - - Lemma incr_counter_tape_spec_none' N E c γ1 γ2 γ3 ε (ε2:R -> nat -> R)(α:loc) (ns:list nat) (q:Qp) (z:nat): + + Lemma incr_counter_tape_spec_none' N E c γ1 γ2 ε (ε2:nat -> R)(α:loc) (ns:list nat) (q:Qp) (z:nat): ↑N ⊆ E-> - (∀ ε n, 0<= ε -> 0<= ε2 ε n)%R-> - (∀ (ε:R), 0<=ε -> ((ε2 ε 0%nat) + (ε2 ε 1%nat)+ (ε2 ε 2%nat)+ (ε2 ε 3%nat))/4 <= ε)%R → - {{{ is_counter (L:=L) N c γ1 γ2 γ3 ∗ - counter_error_frag (L:=L) γ1 ε ∗ - counter_tapes_frag (L:=L) γ2 α [] ∗ - counter_content_frag (L:=L) γ3 q z + (∀ n, 0<= ε2 n)%R-> + (((ε2 0%nat) + (ε2 1%nat)+ (ε2 2%nat)+ (ε2 3%nat))/4 <= ε)%R → + {{{ is_counter (L:=L) N c γ1 γ2 ∗ + ↯ ε ∗ + counter_tapes_frag (L:=L) γ1 α [] ∗ + counter_content_frag (L:=L) γ2 q z }}} incr_counter_tape c #lbl:α @ E {{{ (z':nat) (n:nat), RET (#z', #n); ⌜(0<=n<4)%nat⌝ ∗ ⌜(z<=z')%nat⌝ ∗ - counter_error_frag (L:=L) γ1 (ε2 ε n) ∗ - counter_tapes_frag (L:=L) γ2 α [] ∗ - counter_content_frag (L:=L) γ3 q (z+n)%nat }}}. + ↯(ε2 n) ∗ + counter_tapes_frag (L:=L) γ1 α [] ∗ + counter_content_frag (L:=L) γ2 q (z+n)%nat }}}. Proof. iIntros (Hsubset Hpos Hineq Φ) "(#Hinv & Herr & Htapes & Hcontent) HΦ". - pose (ε2' := (λ ε x, if (x<=?3)%nat then ε2 ε x else 1%R)). - wp_apply (incr_counter_tape_spec_none _ _ _ _ _ _ ε2' - (counter_error_frag γ1 ε ∗ counter_content_frag γ3 q z)%I - (λ n, ⌜0<=n<4⌝ ∗ counter_error_frag γ1 (ε2' ε n) ∗ counter_content_frag γ3 q z)%I - (λ z' n, ⌜0<=n<4⌝ ∗ ⌜z<=z'⌝ ∗ counter_error_frag γ1 (ε2' ε n) ∗ counter_content_frag γ3 q (z+n)%nat)%I - with "[$Herr $Htapes $Hcontent]"). + pose (ε2' := (λ x, if (x<=?3)%nat then ε2 x else 1%R)). + wp_apply (incr_counter_tape_spec_none _ _ _ _ _ + (λ z' n ε' ε2'', ⌜0<=n<4⌝ ∗ ⌜z<=z'⌝ ∗ ⌜ε=ε'⌝ ∗ ⌜ε2''=ε2'⌝ ∗ + ↯ (ε2' n) ∗ + counter_content_frag (L:=L) γ2 q (z+n)%nat + )%I + with "[-HΦ]"). - done. - - rewrite /ε2'. intros. - case_match; [naive_solver|lra]. - - rewrite /ε2'. simpl. intros. naive_solver. - - repeat iSplit; first done. - + iModIntro. - iIntros (ε' n) "[(Herr &Hcontent) Herr_auth]". - destruct (n<=?3) eqn:H; last first. - { iLeft. iPureIntro. rewrite /ε2'. by rewrite H. } - iRight. - iFrame. - iDestruct (counter_error_agree with "[$][$]") as "->". - iDestruct (counter_error_auth_pos with "[$]") as "%". - unshelve iMod (counter_error_update _ _ _ (mknonnegreal (ε2' ε n) _) with "[$][$]") as "[$$]". - { rewrite /ε2' H. - naive_solver. } - iPureIntro. split; first lia. - apply leb_complete in H. lia. - + iModIntro. - iIntros (??) "[(%&Herr & Hcontent) Hcontent_auth]". + - iSplit; first done. + iFrame. + iApply fupd_mask_intro; first set_solver. + iIntros "Hclose". + iFrame. + iExists ε2'. + repeat iSplit. + + iPureIntro. rewrite /ε2'. intros; case_match; [naive_solver|lra]. + + done. + + iIntros (n) "Hfrag". + iMod "Hclose". + iModIntro. + iIntros (?) "?". + rewrite /ε2'. + case_match eqn:H; last by (iDestruct (ec_contradict with "[$]") as "%"). iFrame. + apply leb_complete in H. iDestruct (counter_content_less_than with "[$][$]") as "%". - by iMod (counter_content_update with "[$][$]") as "[$ $]". - - iIntros (??) "[(%&%&?&?)?]". + iMod (counter_content_update with "[$][$]") as "[??]". + iFrame. + iPureIntro; repeat split; try done; lia. + - iIntros (z' n) "[Hfrag (%ε' & %ε2'' & % & % &-> & -> & Herr & Hfrag' )]". iApply "HΦ". iFrame. - rewrite /ε2'. case_match eqn: H2; first by iFrame. - apply leb_iff_conv in H2. lia. + iSplit; first done. + iSplit; first done. + iApply ec_eq; last done. + rewrite /ε2'. + case_match eqn :K; first done. + exfalso. + apply leb_complete_conv in K. + lia. Qed. End lemmas. + diff --git a/theories/coneris/lib/hocap.v b/theories/coneris/lib/hocap.v index 3b56af31..df41f837 100644 --- a/theories/coneris/lib/hocap.v +++ b/theories/coneris/lib/hocap.v @@ -1,25 +1,244 @@ (** * Hocap specs *) From stdpp Require Import namespaces. From iris Require Import excl_auth invariants list. -From clutch.coneris Require Import coneris flip. +From clutch.coneris Require Import coneris. Set Default Proof Using "Type*". -Definition hocap_error_nroot:= nroot.@ "error". -Definition hocap_error_RA := excl_authR NNRO. - -Class hocap_errorGS (Σ : gFunctors) := Hocap_errorGS { - hocap_errorGS_inG :: inG Σ (hocap_error_RA); -}. - +(* Definition hocap_error_nroot:= nroot.@ "error". *) +(* Definition hocap_error_RA := authR nonnegrealR. *) + +(* Class hocap_errorGS (Σ : gFunctors) := Hocap_errorGS { *) +(* hocap_errorGS_inG :: inG Σ (hocap_error_RA); *) +(* }. *) + + +(* Definition hocap_errorΣ := #[GFunctor (hocap_error_RA)]. *) + +(* Notation "'●↯' ε '@' γ" := (∃ (x : nonnegreal), ⌜x.(nonneg) = ε%R⌝ ∗ own γ (● x))%I *) +(* (at level 1). *) +(* Notation "'◯↯' ε '@' γ" := (∃ (x : nonnegreal), ⌜x.(nonneg) = ε%R⌝ ∗ own γ (◯ x))%I *) +(* (at level 1). *) + + +(* Section error_lemmas. *) +(* Context `{!conerisGS Σ, !hocap_errorGS Σ}. *) + +(* Lemma hocap_error_auth_exclusive b b' γ: *) +(* ●↯ b @ γ -∗ ●↯ b' @ γ -∗ False. *) +(* Proof. *) +(* iIntros "[%[% H1]] [%[% H2]]". *) +(* iCombine "H1 H2" gives "%H1". *) +(* compute in H1. destruct H1. *) +(* exfalso. *) +(* apply H1. done. *) +(* Qed. *) + +(* Lemma hocap_error_frag_split (b b':nonnegreal) γ: *) +(* ◯↯ b @ γ ∗ ◯↯ b' @ γ ⊣⊢ ◯↯ (b+b') @ γ. *) +(* Proof. *) +(* iSplit. *) +(* - iIntros "[[%x1[% H1]] [%x2[% H2]]]". *) +(* iExists (x1 + x2)%NNR. *) +(* iSplit; [simpl; simpl in *; iPureIntro; lra|]. *) +(* rewrite auth_frag_op own_op. iFrame. *) +(* - iIntros "[%x [% H]]". *) +(* simpl in *. *) +(* replace x with (b+b')%NNR; last (apply nnreal_ext; simpl; lra). *) +(* rewrite auth_frag_op own_op. *) +(* by iDestruct "H" as "[$ $]". *) +(* Qed. *) + +(* (* Helpful lemmas *) *) +(* Lemma hocap_error_auth_valid (b:R) γ: *) +(* (●↯ b @ γ) -∗ ⌜(0<=b<1)%R⌝. *) +(* Proof. *) +(* iIntros "[%x[<- H]]". *) +(* iDestruct (own_valid with "[$]") as "%H". *) +(* iPureIntro. *) +(* rewrite auth_auth_valid in H. *) +(* destruct x. *) +(* compute in H. *) +(* split; simpl; lra. *) +(* Qed. *) + +(* Lemma hocap_error_frag_valid (b:R) γ: *) +(* (◯↯ b @ γ) -∗ ⌜(0<=b<1)%R⌝. *) +(* Proof. *) +(* iIntros "[%[<- H]]". *) +(* iDestruct (own_valid with "[$]") as "%H". *) +(* iPureIntro. *) +(* rewrite auth_frag_valid in H. *) +(* destruct x. *) +(* compute in H. *) +(* split; simpl; lra. *) +(* Qed. *) + +(* Lemma hocap_error_alloc (ε:nonnegreal): *) +(* (ε<1)%R -> ⊢ |==>∃ γ, (●↯ ε @ γ) ∗ (◯↯ ε @ γ). *) +(* Proof. *) +(* intros H. *) +(* iMod (own_alloc (● ε ⋅ ◯ ε)) as "[% [??]]". *) +(* - apply auth_both_valid_2. *) +(* + compute. destruct ε; simpl in H. lra. *) +(* + apply nonnegreal_included; lra. *) +(* - by eauto with iFrame. *) +(* Qed. *) + +(* Lemma hocap_error_ineq γ (b c:R) : *) +(* (●↯ b @ γ) -∗ (◯↯ c @ γ) -∗ ⌜ (c<=b)%R ⌝. *) +(* Proof. *) +(* iIntros "[% [<- Hγ●]] [% [<-Hγ◯]]". *) +(* iCombine "Hγ● Hγ◯" gives "%Hop". *) +(* by eapply auth_both_valid_discrete in Hop as [Hlt%nonnegreal_included ?]. *) +(* Qed. *) + +(* Lemma hocap_error_decrease γ (b' b:R) : *) +(* (●↯ (b) @ γ) -∗ (◯↯ b' @ γ) ==∗ (●↯ (b-b') @ γ). *) +(* Proof. *) +(* iIntros "H1 H2". *) +(* simpl. *) +(* iDestruct (hocap_error_ineq with "[$][$]") as "%". *) +(* iDestruct "H1" as "[%x [% H1]]". *) +(* iDestruct "H2" as "[%x' [% H2]]". *) +(* iMod (own_update_2 with "H1 H2") as "Hown". *) +(* { unshelve eapply (auth_update_dealloc _ _ ((x-x') _)%NNR), nonnegreal_local_update. *) +(* - lra. *) +(* - apply cond_nonneg. *) +(* - apply nnreal_ext =>/=. lra. } *) +(* iFrame. simpl. iPureIntro. *) +(* by subst. *) +(* Qed. *) + + +(* Lemma hocap_error_increase γ (b:R) (b':nonnegreal) : *) +(* (b+b'<1)%R -> ⊢ (●↯ b @ γ) ==∗ (●↯ (b+b')%R @ γ) ∗ (◯↯ b' @ γ). *) +(* Proof. *) +(* iIntros (Hineq) "[%x [% H]]". *) +(* iMod (own_update with "H") as "[$ $]"; last (iPureIntro; split; last done). *) +(* - apply auth_update_alloc. *) +(* apply (local_update_unital_discrete _ _ (x+b')%NNR) => z H1 H2. *) +(* split. *) +(* + destruct x, b'. compute. simpl in *. lra. *) +(* + apply nnreal_ext. simpl. *) +(* rewrite Rplus_comm. *) +(* apply Rplus_eq_compat_l. *) +(* simpl in *. rewrite H2. simpl. lra. *) +(* - simpl. lra. *) +(* Qed. *) + +(* Lemma hocap_error_auth_irrel γ (b c:R) : *) +(* (b=c)%R -> (●↯ b @ γ) -∗ (●↯ c @ γ). *) +(* Proof. *) +(* iIntros (->) "$". *) +(* Qed. *) + +(* Lemma hocap_error_frag_irrel γ (b c:R) : *) +(* (b=c)%R -> (◯↯ b @ γ) -∗ (◯↯ c @ γ). *) +(* Proof. *) +(* iIntros (->) "$". *) +(* Qed. *) -Definition hocap_errorΣ := #[GFunctor (excl_authR (nonnegrealUR))]. +(* End error_lemmas. *) -Notation "'●↯' ε '@' γ" := (∃ (x : nonnegreal), ⌜x.(nonneg) = ε%R⌝ ∗ own γ (●E x))%I - (at level 1). -Notation "'◯↯' ε '@' γ" := (∃ (x : nonnegreal), ⌜x.(nonneg) = ε%R⌝ ∗ own γ (◯E x))%I - (at level 1). +(* Section hocap_error_coupl. *) +(* Context `{conerisGS Σ}. *) +(* Context (tb:nat). *) +(* Local Canonical Structure finO := leibnizO (fin (S tb)). *) +(* Local Canonical Structure RO := leibnizO R. *) +(* Local Canonical Structure ε2O := leibnizO (list (fin(S tb))->R). *) + +(* Definition hocap_error_coupl_pre Z Φ : (R * R * list (nat * (list (fin (S tb)) -> R) * (list (fin (S tb)))) -> iProp Σ) := *) +(* (λ x, *) +(* let '(ε, ε_initial, ls) := x in *) +(* (Z ε ε_initial ls)∨ *) +(* ∃ num ε2, *) +(* ⌜(∀ l, 0<=ε2 l)%R⌝ ∗ *) +(* ⌜(SeriesC (λ l, if bool_decide (length l = num) then ε2 l else 0)/((S tb)^num) <= ε)%R⌝ ∗ *) +(* (∀ ns, Φ (ε2 ns, ε_initial, ls ++ [(num, ε2, ns)])) *) +(* )%I. *) + +(* Local Instance hocap_error_coupl_pre_ne Z Φ : *) +(* NonExpansive (hocap_error_coupl_pre Z Φ). *) +(* Proof. *) +(* solve_contractive. *) +(* Qed. *) + +(* Local Instance hocap_error_coupl_pre_mono Z : BiMonoPred (hocap_error_coupl_pre Z). *) +(* Proof. *) +(* split; last apply _. *) +(* iIntros (Φ Ψ HNEΦ HNEΨ) "#Hwand". *) +(* iIntros ([[??]?]) "[H|(%&%&%&%&H)]". *) +(* - by iLeft. *) +(* - iRight. *) +(* iExists _, _. *) +(* repeat iSplit; try done. *) +(* iIntros. by iApply "Hwand". *) +(* Qed. *) + +(* Definition hocap_error_coupl' Z := bi_least_fixpoint (hocap_error_coupl_pre Z). *) +(* Definition hocap_error_coupl ε_current ε_initial ls Z := hocap_error_coupl' Z (ε_current, ε_initial, ls). *) + +(* Lemma hocap_error_coupl_unfold ε ε_initial ls Z : *) +(* hocap_error_coupl ε ε_initial ls Z ≡ *) +(* ((Z ε ε_initial ls)∨ *) +(* ∃ num ε2, *) +(* ⌜(∀ l, 0<=ε2 l)%R⌝ ∗ *) +(* ⌜(SeriesC (λ l, if bool_decide (length l = num) then ε2 l else 0)/((S tb)^num) <= ε)%R⌝ ∗ *) +(* (∀ ns, hocap_error_coupl (ε2 ns) ε_initial (ls ++ [(num, ε2, ns)]) Z))%I. *) +(* Proof. *) +(* rewrite /hocap_error_coupl/hocap_error_coupl' least_fixpoint_unfold//. Qed. *) + +(* Lemma hocap_error_coupl_ret ε ε_initial ls Z: *) +(* Z ε ε_initial ls -∗ hocap_error_coupl ε ε_initial ls Z. *) +(* Proof. *) +(* iIntros. rewrite hocap_error_coupl_unfold. by iLeft. *) +(* Qed. *) + +(* Lemma hocap_error_coupl_rec ε ε_initial ls Z: *) +(* (∃ num ε2, *) +(* ⌜(∀ l, 0<=ε2 l)%R⌝ ∗ *) +(* ⌜(SeriesC (λ l, if bool_decide (length l = num) then ε2 l else 0)/((S tb)^num) <= ε)%R⌝ ∗ *) +(* (∀ ns, hocap_error_coupl (ε2 ns) ε_initial (ls ++ [(num, ε2, ns)]) Z)) -∗ hocap_error_coupl ε ε_initial ls Z. *) +(* Proof. *) +(* iIntros. rewrite hocap_error_coupl_unfold. by iRight. *) +(* Qed. *) + +(* Lemma hocap_error_coupl_ind (Ψ Z : R -> R -> list (nat * (list (fin (S tb)) -> R) * (list (fin (S tb))))->iProp Σ): *) +(* ⊢ (□ (∀ ε ε_initial ls, *) +(* hocap_error_coupl_pre Z (λ '(ε', ε_initial', ls'), *) +(* Ψ ε' ε_initial' ls' ∧ hocap_error_coupl ε' ε_initial' ls' Z)%I (ε, ε_initial, ls) -∗ Ψ ε ε_initial ls) → *) +(* ∀ ε ε_initial ls, hocap_error_coupl ε ε_initial ls Z -∗ Ψ ε ε_initial ls)%I. *) +(* Proof. *) +(* iIntros "#IH" (ε ε_initial ls) "H". *) +(* set (Ψ' := (λ '(ε, ε_initial, ls), Ψ ε ε_initial ls) : (prodO _ _->iProp Σ)). *) +(* assert (NonExpansive Ψ') by solve_contractive. *) +(* iApply (least_fixpoint_ind _ Ψ' with "[] H"). *) +(* iIntros "!#" ([[??]?]) "H". by iApply "IH". *) +(* Qed. *) + +(* Lemma hocap_error_coupl_bind ε ε_initial ls Z1 Z2 : *) +(* (∀ ε' ε_initial' ls', Z1 ε' ε_initial' ls' -∗ hocap_error_coupl ε' ε_initial' ls' Z2) -∗ *) +(* hocap_error_coupl ε ε_initial ls Z1 -∗ *) +(* hocap_error_coupl ε ε_initial ls Z2. *) +(* Proof. *) +(* iIntros "HZ H". *) +(* iRevert "HZ". *) +(* iRevert (ε ε_initial ls) "H". *) +(* iApply hocap_error_coupl_ind. *) +(* iIntros "!#" (ε ε_initial ls) "[H|H] HZ". *) +(* - by iApply "HZ". *) +(* - iApply hocap_error_coupl_rec. *) +(* iDestruct "H" as "(%&%&%&%&Hrest)". *) +(* iExists _,_. repeat iSplit; try done. *) +(* iIntros (?). *) +(* iDestruct ("Hrest" $! _) as "[Hrest _]". *) +(* by iApply "Hrest". *) +(* Qed. *) + +(* End hocap_error_coupl. *) + Definition hocap_tapes_nroot:=nroot.@"tapes". Class hocap_tapesGS (Σ : gFunctors) := Hocap_tapesGS { hocap_tapesGS_inG :: ghost_mapG Σ loc (nat*list nat) @@ -31,53 +250,6 @@ Notation "α ◯↪N ( M ; ns ) @ γ":= (α ↪[ γ ] (M,ns))%I Notation "● m @ γ" := (ghost_map_auth γ 1 m) (at level 20) : bi_scope. -Section error_lemmas. - Context `{!conerisGS Σ, !hocap_errorGS Σ}. - (* Helpful lemmas *) - Lemma hocap_error_auth_pos (b:R) γ: - (●↯ b @ γ) -∗ ⌜(0<=b)%R⌝. - Proof. - by iIntros "[%[<- H]]". - Qed. - - Lemma hocap_error_frag_pos (b:R) γ: - (◯↯ b @ γ) -∗ ⌜(0<=b)%R⌝. - Proof. - by iIntros "[%[<- H]]". - Qed. - - Lemma hocap_error_alloc (ε:nonnegreal): - ⊢ |==>∃ γ, (●↯ ε @ γ) ∗ (◯↯ ε @ γ). - Proof. - iMod (own_alloc (●E ε ⋅ ◯E ε)) as "[% [??]]". - - by apply excl_auth_valid. - - by eauto with iFrame. - Qed. - - Lemma hocap_error_agree γ (b c:R) : - (●↯ b @ γ) -∗ (◯↯ c @ γ) -∗ ⌜ b = c ⌝. - Proof. - iIntros "[% [<- Hγ●]] [% [<-Hγ◯]]". - by iCombine "Hγ● Hγ◯" gives %<-%excl_auth_agree_L. - Qed. - - Lemma hocap_error_update γ (b':nonnegreal) (b c:R) : - (●↯ b @ γ) -∗ (◯↯ c @ γ) ==∗ (●↯ b' @ γ) ∗ (◯↯ b' @ γ). - Proof. - iIntros "[% [<- Hγ●]] [% [<-Hγ◯]]". - iMod (own_update_2 _ _ _ (_ ⋅ _) with "Hγ● Hγ◯") as "[$$]". - { by apply excl_auth_update. } - done. - Qed. - - Lemma hocap_error_irrel γ (b c:R) : - (b=c)%R -> (●↯ b @ γ) -∗ (●↯ c @ γ). - Proof. - iIntros (->) "$". - Qed. - -End error_lemmas. - Section tapes_lemmas. Context `{!conerisGS Σ, !hocap_tapesGS Σ}. @@ -104,166 +276,13 @@ Section tapes_lemmas. by iApply ghost_map_insert. Qed. - Lemma hocap_tapes_presample γ m k N ns n: - (● m @ γ) -∗ (k ◯↪N (N; ns) @ γ) ==∗ (● (<[k:=(N,ns++[n])]>m) @ γ) ∗ (k ◯↪N (N; ns++[n]) @ γ). + Lemma hocap_tapes_update γ m k N N' ns ns': + (● m @ γ) -∗ (k ◯↪N (N; ns) @ γ) ==∗ (● (<[k:=(N',ns')]>m) @ γ) ∗ (k ◯↪N (N'; ns') @ γ). Proof. iIntros "H1 H2". - iApply (ghost_map_update with "[$][$]"). - Qed. - - Lemma hocap_tapes_pop γ m k N ns n: - (● m @ γ) -∗ (k ◯↪N (N; n::ns) @ γ) ==∗ (● (<[k:=(N,ns)]>m) @ γ) ∗ (k ◯↪N (N; ns) @ γ). - Proof. - iIntros "H1 H2". - iApply (ghost_map_update with "[$][$]"). + iApply (ghost_map_update with "[$][$]"). Qed. + - Lemma hocap_tapes_notin α N ns m (f:(nat*list nat)-> nat) g: - α ↪N (N; ns) -∗ ([∗ map] α0↦t ∈ m, α0 ↪N (f t; g t)) -∗ ⌜m!!α=None ⌝. - Proof. - destruct (m!!α) eqn:Heqn; last by iIntros. - iIntros "Hα Hmap". - iDestruct (big_sepM_lookup with "[$]") as "?"; first done. - iExFalso. - iApply (tapeN_tapeN_contradict with "[$][$]"). - Qed. - - (** * TODO add*) End tapes_lemmas. -Section HOCAP. - - Context `{!conerisGS Σ, !hocap_errorGS Σ}. - - Definition error_inv (γ :gname):= - inv hocap_error_nroot (∃ (ε:R), ↯ ε ∗ ●↯ ε @ γ). - - Lemma wp_hocap_rand_adv_comp (N : nat) z E - (ε2 : R -> fin (S N) -> R) - (P : iProp Σ) (Q : (fin (S N)) -> iProp Σ) γ: - TCEq N (Z.to_nat z) → - ↑hocap_error_nroot ⊆ E -> - (∀ ε n, (0<=ε -> 0<=ε2 ε n))%R -> - (∀ (ε:R), 0<=ε ->SeriesC (λ n, (1 / (S N)) * (ε2 ε n))%R <= (ε))%R → - {{{ error_inv γ∗ - □(∀ (ε:R) (n : fin (S N)), P ∗ ●↯ ε @ γ ={E∖↑hocap_error_nroot}=∗ - (⌜(1<=ε2 ε n)%R⌝ ∨(●↯ (ε2 ε n) @ γ ∗ Q (n))) ) ∗ - P }}} rand #z @ E {{{ n, RET #n; Q (n)}}}. - Proof. - iIntros (-> Hsubset ? Hineq) "%Φ [#Hinv [#Hchange HP]] HΦ". - iInv "Hinv" as ">(%ε & Hε & Hauth)" "Hclose". - iDestruct (ec_valid with "[$]") as "%". - wp_apply (wp_couple_rand_adv_comp1' _ _ _ _ (ε2 ε) with "[$]"); [naive_solver|naive_solver|]. - iIntros (n) "Hε". - iMod ("Hchange" $! _ n with "[$]") as "[%|[Hauth HQ]]"; last first. - { iMod ("Hclose" with "[Hauth Hε]") as "_". - - unshelve iExists (mknonnegreal _ _); last iFrame. - naive_solver. - - by iApply "HΦ". } - iExFalso. - by iApply (ec_contradict with "[$]"). - Qed. - - Lemma wp_hocap_flip_adv_comp E - (ε2 : R -> bool -> R) - (P : iProp Σ) (Q : bool -> iProp Σ) γ: - ↑hocap_error_nroot ⊆ E -> - (∀ ε b, 0<=ε -> 0<=ε2 ε b)%R -> - (∀ (ε:R), 0<=ε -> (((ε2 ε true) + (ε2 ε false))/2 <= (ε)))%R → - {{{ error_inv γ∗ - □(∀ (ε:R) (b : bool), P ∗ ●↯ ε @ γ ={E∖↑hocap_error_nroot}=∗ (⌜(1<=ε2 ε b)%R⌝ ∨ ●↯ (ε2 ε b) @ γ ∗ Q (b)) ) ∗ - P }}} flip @ E {{{ (b:bool), RET #b; Q (b)}}}. - Proof. - iIntros (Hsubset ? Hineq) "%Φ [#Hinv [#Hchange HP]] HΦ". - rewrite /flip/flipL. - wp_pures. - wp_apply (wp_hocap_rand_adv_comp _ _ _ (λ ε x, if fin_to_nat x =? 1%nat then ε2 ε true else ε2 ε false) P (λ x, Q (fin_to_nat x =? 1%nat)) with "[-HΦ]"); [done|..]. - - intros; case_match; naive_solver. - - intros ε. rewrite SeriesC_finite_foldr; simpl. specialize (Hineq ε). lra. - - iFrame. iSplitR; first iExact "Hinv". - iModIntro. - iIntros (ε n) "H". - iMod ("Hchange" $! _ (fin_to_nat n =? 1%nat)with "[$]") as "[%|[Hε HQ]]". - + iModIntro. iLeft. iPureIntro. by case_match. - + iModIntro. iRight. iFrame. by case_match. - - iIntros. - wp_apply (conversion.wp_int_to_bool); first done. - iIntros "_". - iApply "HΦ". - inv_fin n; simpl; first done. - intros n; inv_fin n; simpl; first done. - intros n; inv_fin n. - Qed. - - (** With tapes *) - Context `{!hocap_tapesGS Σ}. - - Definition tapes_inv (γ :gname):= - inv hocap_tapes_nroot (∃ m, ●m@γ ∗ [∗ map] α ↦ t ∈ m, α ↪N ( t.1 ; t.2 ) ). - Lemma wp_hocap_presample_adv_comp (N : nat) z E ns α - (ε2 : R -> fin (S N) -> R) - (P : iProp Σ) (Q : val-> iProp Σ) T γ γ': - TCEq N (Z.to_nat z) → - ↑hocap_error_nroot ⊆ E -> - ↑hocap_tapes_nroot ⊆ E -> - (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> - (∀ (ε:R), 0<= ε -> SeriesC (λ n, (1 / (S N)) * (ε2 ε n))%R <= ε)%R → - error_inv γ -∗ tapes_inv γ' -∗ - (□∀ (ε:R) m, (⌜m!!α = Some (N, ns)⌝ ∗ P ∗ ●↯ ε @ γ ∗ ●m@γ') - ={E∖↑hocap_error_nroot∖↑hocap_tapes_nroot}=∗ - ∃ n, (⌜(1<=ε2 ε n)%R⌝ ∨(●↯ (ε2 ε n) @ γ ∗ ●(<[α := (N, ns ++ [fin_to_nat n])]>m) @ γ' ∗ T (n)))) - -∗ P -∗ α ◯↪N (N; ns) @ γ' -∗ - wp_update E (∃ n, T (n) ∗ α◯↪N (N; ns++[fin_to_nat n]) @ γ'). - Proof. - iIntros (-> Hval Hsubset Hubset' Hineq) "#Hinv #Hinv' #Hshift HP Htape". - iApply fupd_wp_update. - iInv "Hinv" as ">(%ε' & Hε & Hauth)" "Hclose". - iInv "Hinv'" as ">(%m & Hm & Hmauth)" "Hclose'". - iDestruct (ec_valid with "[$]") as "%". - iApply wp_update_mono_fupd. iApply fupd_frame_l. - iSplitL "Hε". - - iApply (wp_update_presample_exp _ α _ ns ε' (ε2 ε) with "[$Hε]"). - + naive_solver. - + naive_solver. - + admit. - - iMod ("Hclose'" with "[$]"). - Abort. - - (* iApply (wp_presample_adv_comp); [done|exact|..]. *) - (* iApply fupd_frame_l. *) - (* - *) - (* Abort. *) - - - -End HOCAP. - -Section HOCAP_alt. - Context `{!conerisGS Σ}. - - Lemma wp_flip_exp_hocap (P : iProp Σ) (Q : bool → iProp Σ) E1 E2 : - □ (P ={E1, E2}=∗ - ∃ ε1 ε2, ⌜(( (ε2 true) + (ε2 false))/2 <= ε1)%R⌝ ∗ - ⌜(∀ b, 0<=ε2 b)%R⌝ ∗ - ↯ ε1 ∗ (∀ (b : bool), ↯ (ε2 b) ={E2, E1}=∗ Q b)) -∗ - {{{ P }}} flip @ E1 {{{ (b : bool), RET #b; Q b}}}. - Proof. - iIntros "#Hvs". iIntros (Ψ) "!# HP HΨ". - rewrite /flip /flipL. - wp_pures. - wp_bind (rand _)%E. - iMod ("Hvs" with "HP") as (ε1 ε2) "(% & % & Hε1 & HQ)". - set (ε2' := ε2 ∘ fin_to_bool). - iApply (wp_couple_rand_adv_comp1' _ _ _ _ ε2' with "Hε1"). - { intros; rewrite /ε2'. simpl. done. } - { rewrite SeriesC_finite_foldr /ε2' /=. lra. } - iIntros "!>" (n) "Hε2". - assert (ε2' n = ε2 (Z_to_bool n)) as ->. - { inv_fin n; [eauto|]. intros n. inv_fin n; [eauto|]. intros n. inv_fin n. } - iMod ("HQ" with "Hε2") as "HQ". iModIntro. - wp_apply (conversion.wp_int_to_bool); [done|]. - iIntros "_". - by iApply "HΨ". - Qed. - -End HOCAP_alt. diff --git a/theories/coneris/lib/hocap_flip.v b/theories/coneris/lib/hocap_flip.v new file mode 100644 index 00000000..3df2d429 --- /dev/null +++ b/theories/coneris/lib/hocap_flip.v @@ -0,0 +1,243 @@ +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'; + flip_tapes_presample {L:flipG Σ} N E γ α ns ε (ε2 : bool -> R): + ↑N ⊆ E -> + (∀ x, 0<=ε2 x)%R -> + ((ε2 true + ε2 false)/2 <= ε)%R -> + is_flip (L:=L) N γ -∗ + flip_tapes_frag (L:=L) γ α (ns) -∗ + ↯ ε -∗ + state_update E (∃ n, ↯ (ε2 n) ∗ flip_tapes_frag (L:=L) γ α (ns ++ [n])); + + (** * 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 (α:loc) n ns: + ↑N⊆E -> + {{{ is_flip (L:=L) N γ1 ∗ flip_tapes_frag (L:=L) γ1 α (n::ns) + }}} + flip_tape #lbl:α @ E + {{{ RET #n; flip_tapes_frag (L:=L) γ1 α ns }}}; + + (* flip_presample_spec {L: flipG Σ} NS E γ1 α ns T: *) + (* ↑NS ⊆ E -> *) + (* is_flip (L:=L) NS γ1 -∗ *) + (* flip_tapes_frag (L:=L) γ1 α ns -∗ *) + (* (|={E∖↑NS, ∅}=> *) + (* ∃ ε num ε2, ↯ ε ∗ *) + (* ⌜(∀ l, length l = num -> 0<=ε2 l)%R⌝ ∗ *) + (* ⌜(SeriesC (λ l, if length l =? num then ε2 l else 0) /(2^num) <= ε)%R⌝∗ *) + (* (∀ ns', ↯ (ε2 ns') *) + (* ={∅, E∖↑NS}=∗ T ε num ε2 ns')) *) + (* -∗ *) + (* wp_update E (∃ ε num ε2 ns', flip_tapes_frag (L:=L) γ1 α (ns ++ ns') ∗ T ε num ε2 ns') *) +}. + + +(** Instantiate flip *) +Section instantiate_flip. + Context `{H: conerisGS Σ, r1:@rand_spec Σ H}. + + #[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 (???????????) "#Hinv Hfrag Hε". + iMod (rand_tapes_presample _ _ _ _ _ _ _ (λ x, ε2 (nat_to_bool (fin_to_nat x)))with "[$][$][$]") as "(%n&?&?)"; try done. + - rewrite SeriesC_finite_foldr/=. + rewrite nat_to_bool_eq_0 nat_to_bool_neq_0; last lia. + lra. + - iFrame. + iModIntro. + rewrite fmap_app. + by repeat (inv_fin n; try (intros n)); simpl. + 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 (???? ???? Φ) "(#Hinv & Hfrag) HΦ". + wp_pures. + wp_apply (rand_tape_spec_some with "[-HΦ]"); [done|..]. + - by iFrame. + - iIntros "Hfrag". + 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 (?????? T ?) "#Hinv Hfrag Hvs". *) + (* iMod (rand_presample_spec _ _ _ _ _ _ *) + (* (λ ε num ε2 ns', *) + (* ∃ bs' ε2', ⌜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' *) + (* )%I *) + (* with "[//][$][-]") as "(%&%&%&%&?&%&%&%K&%&?)"; [exact| |iModIntro; iFrame]; last first. *) + (* { by rewrite fmap_app K. } *) + (* iMod "Hvs" as "(%&%&%&Herr &%Hpos&%Hineq &Hrest)". *) + (* iFrame. *) + (* iExists num, (λ ls, ε2 (nat_to_bool<$>(fin_to_nat <$> ls))). *) + (* iModIntro. *) + (* repeat iSplit; try iPureIntro. *) + (* - 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. *) + (* - iIntros (ls) "H2". *) + (* iMod ("Hrest" with "[$H2 ]") as "?". *) + (* iFrame. *) + (* iModIntro. *) + (* iSplit; iPureIntro. *) + (* + 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. + +Section test. + Context `{F:flip_spec}. + Lemma flip_presample_spec_simple {L: flipG Σ} NS E γ1 α ns ε ε2: + ↑NS ⊆ E -> + (∀ n, 0<=ε2 n)%R -> + ((ε2 true + ε2 false)/2<=ε)%R -> + is_flip (L:=L) NS γ1 -∗ + flip_tapes_frag (L:=L) γ1 α ns -∗ + ↯ ε -∗ + wp_update E (∃ b, flip_tapes_frag (L:=L) γ1 α (ns ++ [b]) ∗ ↯ (ε2 b)). + Proof. + iIntros (Hsubset Hpos Hineq) "#Hinv Hfrag Herr". + iApply wp_update_state_update. + iMod (flip_tapes_presample with "[$][$][$]") as "(%&?&?)"; try done. + by iFrame. + Qed. +End test. diff --git a/theories/coneris/lib/hocap_rand.v b/theories/coneris/lib/hocap_rand.v new file mode 100644 index 00000000..4e7f9073 --- /dev/null +++ b/theories/coneris/lib/hocap_rand.v @@ -0,0 +1,363 @@ +(** * Hocap rand specs *) +From clutch.coneris Require Import coneris hocap. + +Set Default Proof Using "Type*". + +Class rand_spec `{!conerisGS Σ} := RandSpec +{ + (** * Operations *) + rand_allocate_tape : val; + rand_tape : val; + (** * Ghost state *) + (** The assumptions about [Σ] *) + randG : gFunctors → Type; + + rand_tape_name: Type; + (** * Predicates *) + is_rand {L : randG Σ} (N:namespace) + (γ1: rand_tape_name) : iProp Σ; + rand_tapes_auth {L : randG Σ} (γ: rand_tape_name) (m:gmap loc (nat * list nat)): iProp Σ; + rand_tapes_frag {L : randG Σ} (γ: rand_tape_name) (α:loc) (ns: (nat * list nat)): iProp Σ; + (** * General properties of the predicates *) + #[global] is_rand_persistent {L : randG Σ} N γ1 :: + Persistent (is_rand (L:=L) N γ1); + #[global] rand_tapes_auth_timeless {L : randG Σ} γ m :: + Timeless (rand_tapes_auth (L:=L) γ m); + #[global] rand_tapes_frag_timeless {L : randG Σ} γ α ns :: + Timeless (rand_tapes_frag (L:=L) γ α ns); + #[global] rand_tape_name_inhabited :: + Inhabited rand_tape_name; + + rand_tapes_auth_exclusive {L : randG Σ} γ m m': + rand_tapes_auth (L:=L) γ m -∗ rand_tapes_auth (L:=L) γ m' -∗ False; + rand_tapes_frag_exclusive {L : randG Σ} γ α ns ns': + rand_tapes_frag (L:=L) γ α ns -∗ rand_tapes_frag (L:=L) γ α ns' -∗ False; + rand_tapes_agree {L : randG Σ} γ α m ns: + rand_tapes_auth (L:=L) γ m -∗ rand_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝; + rand_tapes_valid {L : randG Σ} γ2 α tb ns: + rand_tapes_frag (L:=L) γ2 α (tb, ns) -∗ ⌜Forall (λ n, n<=tb)%nat ns⌝ ; + rand_tapes_update {L : randG Σ} γ α m ns ns': + Forall (λ x, x<=ns'.1) ns'.2 -> + rand_tapes_auth (L:=L) γ m -∗ rand_tapes_frag (L:=L) γ α ns ==∗ + rand_tapes_auth (L:=L) γ (<[α := ns']> m) ∗ rand_tapes_frag (L:=L) γ α ns'; + rand_tapes_presample {L:randG Σ} N E γ α tb ns ε (ε2 : fin (S tb) -> R): + ↑N ⊆ E -> + (∀ x, 0<=ε2 x)%R -> + (SeriesC (λ n, 1 / (S tb) * ε2 n)%R <= ε)%R -> + is_rand(L:=L) N γ -∗ + rand_tapes_frag (L:=L) γ α (tb, ns) -∗ + ↯ ε -∗ + state_update E (∃ n, ↯ (ε2 n) ∗ rand_tapes_frag (L:=L) γ α (tb, ns ++ [fin_to_nat n])); + + + (** * Program specs *) + rand_inv_create_spec {L : randG Σ} N E: + ⊢ wp_update E (∃ γ1, is_rand (L:=L) N γ1); + rand_allocate_tape_spec {L: randG Σ} N E (tb:nat) γ2: + ↑N ⊆ E-> + {{{ is_rand (L:=L) N γ2 }}} + rand_allocate_tape #tb @ E + {{{ (v:val), RET v; + ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ rand_tapes_frag (L:=L) γ2 α (tb, []) + }}}; + rand_tape_spec_some {L: randG Σ} N E γ2 (α:loc) (tb:nat) n ns: + ↑N⊆E -> + {{{ is_rand (L:=L) N γ2 ∗ + rand_tapes_frag (L:=L) γ2 α (tb, n::ns) + }}} + rand_tape #lbl:α #tb @ E + {{{ RET #n; rand_tapes_frag (L:=L) γ2 α (tb, ns) }}}; + (* rand_presample_spec {L: randG Σ} N E γ2 α (tb:nat) ns T: *) + (* ↑N ⊆ E -> *) + (* is_rand (L:=L) N γ2 -∗ *) + (* rand_tapes_frag (L:=L) γ2 α (tb, ns) -∗ *) + (* (|={E∖↑N, ∅}=> *) + (* ∃ ε, *) + (* ↯ ε ∗ *) + (* hocap_error_coupl tb ε ε [] *) + (* (λ ε_final ε_initial ls, *) + (* ↯ ε_final ={∅, E∖↑N}=∗ T ε_final ε_initial ls *) + (* ) *) + (* ) -∗ *) + (* wp_update E (∃ ε_final ε_initial (ls:list _), *) + (* rand_tapes_frag (L:=L) γ2 α (tb, ns ++ (fin_to_nat <$> (mbind (MBind := list_bind) snd ls))) ∗ *) + (* T ε_final ε_initial ls) *) + + (* rand_presample_spec {L: randG Σ} N E γ2 α (tb:nat) ns T: *) + (* ↑N ⊆ E -> *) + (* is_rand (L:=L) N γ2 -∗ *) + (* rand_tapes_frag (L:=L) γ2 α (tb, ns) -∗ *) + (* (|={E∖↑N, ∅}=> *) + (* ∃ ε num (ε2 : list (fin (S tb)) -> R), *) + (* ↯ ε ∗ *) + (* ⌜(∀ 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':list (fin (S tb))), ↯ (ε2 ns') ={∅, E∖↑N}=∗ T ε num ε2 ns')) -∗ *) + (* wp_update E (∃ ε num ε2 ns', rand_tapes_frag (L:=L) γ2 α (tb, ns ++ (fin_to_nat <$> ns')) ∗ *) + (* T ε num ε2 ns') *) +}. + +Section impl. + Local Opaque INR. + (* (** Instantiate rand *) *) + Class randG1 Σ := RandG1 { + flipG1_tapes:: hocap_tapesGS Σ; + }. + Local Definition rand_inv_pred1 `{!conerisGS Σ, !hocap_tapesGS Σ} γ2:= + (∃ (m:gmap loc (nat * list nat)) , + ([∗ map] α ↦ t ∈ m, α ↪N ( t.1 ; t.2 )) ∗ + ●m@γ2 + )%I. + + #[local] Program Definition rand_spec1 `{!conerisGS Σ}: rand_spec := + {| rand_allocate_tape:= (λ: "N", alloc "N"); + rand_tape:= (λ: "α" "N", rand("α") "N"); + randG := randG1; + rand_tape_name := gname; + is_rand _ N γ2 := inv N (rand_inv_pred1 γ2); + rand_tapes_auth _ γ m := (●m@γ)%I; + rand_tapes_frag _ γ α ns := (α ◯↪N (ns.1; ns.2) @ γ ∗ ⌜Forall (λ x, x<=ns.1) ns.2⌝)%I; + |}. + 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 (??????[]) "?[? %]". + by iDestruct (hocap_tapes_agree with "[$][$]") as "%". + Qed. + Next Obligation. + simpl. + by iIntros (???????) "[? $]". + Qed. + Next Obligation. + iIntros (??????[][]?) "?[? %]". + iMod (hocap_tapes_update with "[$][$]") as "[??]". + by iFrame. + Qed. + Next Obligation. + simpl. + iIntros (??????????????) "#H1 [H2 %] H3". + iInv "H1" as ">(%&?&?)" "Hclose". + iDestruct (hocap_tapes_agree with "[$][$]") as "%". + iDestruct (big_sepM_insert_acc with "[$]") as "[Htape H]"; first done. + iMod (state_update_presample_exp with "[$][$]") as "(%n & Htape & ?)"; try exact. + iMod (hocap_tapes_update with "[$][$]") as "[? ?]". + iModIntro. iFrame. + iMod ("Hclose" with "[-]"). + { iNext. iFrame. by iApply "H". } + iPureIntro. rewrite Forall_app. split; first done. + apply Forall_singleton. + pose proof fin_to_nat_lt n. simpl in *. lia. + Qed. + Next Obligation. + simpl. + iIntros (?????). + iApply fupd_wp_update_ret. + iMod (hocap_tapes_alloc ∅) as "(%γ2 & H4 & H5)". + iMod (inv_alloc _ _ (rand_inv_pred1 γ2) with "[-]"). + { iFrame. by iNext. } + by iFrame. + Qed. + Next Obligation. + simpl. + iIntros (???????? Φ) "#Hinv HΦ". + wp_pures. + iInv "Hinv" as "(%&?&?)" "Hclose". + wp_apply (wp_alloc_tape); first done. + iIntros (α) "Hα". + iDestruct (hocap_tapes_notin with "[$][$]") as "%". + iMod (hocap_tapes_new _ _ α tb [] with "[$]") as "[?H]"; first done. + iMod ("Hclose" with "[-H HΦ]"). + { iModIntro. iFrame. + rewrite big_sepM_insert; [iFrame|done]. + } + iApply "HΦ". + by iFrame. + Qed. + Next Obligation. + simpl. + iIntros (??????????? Φ) "(#Hinv & [Hvs %]) HΦ". + wp_pures. + iInv "Hinv" as ">(%&H3&H4)" "Hclose". + 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 ("Hclose" with "[- Hfrag HΦ]") as "_". + { iExists (<[α:=_]> m). + iFrame. + iApply "H3". by iNext. + } + iApply "HΦ". iFrame. + iPureIntro. by eapply Forall_inv_tail. + Qed. + (* Next Obligation. *) + (* simpl. *) + (* iIntros (???????????) "#Hinv [Hfrag %] Hvs". *) + (* iApply wp_update_state_step_coupl. *) + (* iIntros (σ1 ε_supply) "((Hheap&Htapes)&Hε)". *) + (* iMod (inv_acc with "Hinv") as "[>(% & H3 & H4 ) Hclose]"; [done|]. *) + (* iMod "Hvs" as "(%err & Herr & Hcoupl)". *) + (* Admitted. *) + + (* iMod "Hvs" as "(%err & %num & %ε2 & Herr & %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)". *) + (* iDestruct (ec_supply_bound with "[$][$]") as "%". *) + (* iMod (ec_supply_decrease with "[$][$]") as (ε'' ε_rem -> Heq') "Hε_supply". *) + (* iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'". *) + (* (* unshelve epose (ε_rem := mknonnegreal (ε_supply-ε) _). *) *) + (* (* { simpl in *. lra. } *) *) + (* (* replace (ε_supply) with (ε_rem + ε)%NNR; last first. *) *) + (* (* { rewrite /ε_rem. apply nnreal_ext. simpl. lra. } *) *) + (* iApply (state_step_coupl_iterM_state_adv_comp_con_prob_lang num α); first done. *) + (* unshelve iExists (λ x, mknonnegreal (if length x =? num then ε2 x else 1)%R _). *) + (* { case_match; last (simpl;lra). apply Hpos. by rewrite -Nat.eqb_eq. } *) + (* iSplit. *) + (* { iPureIntro. *) + (* simpl. rewrite Heq'. etrans; last exact. *) + (* rewrite (Rdiv_def (SeriesC _)(S tb ^num)%R) -SeriesC_scal_r. *) + (* apply SeriesC_le; last apply ex_seriesC_scal_r, ex_seriesC_list. *) + (* intros. rewrite elem_of_enum_uniform_fin_list'. *) + (* case_match; last lra. *) + (* split; last lra. *) + (* apply Rmult_le_pos; last (apply Hpos; by rewrite -Nat.eqb_eq). *) + (* rewrite -pow_INR. apply Rdiv_INR_ge_0. *) + (* } *) + (* iIntros (sample) "<-". *) + (* destruct (Rlt_decision (nonneg ε_rem + (ε2 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. *) + (* simpl. simpl in *. *) + (* rewrite -Heq. *) + (* iMod (tapeN_update_append' _ _ _ _ sample with "[$][$]") as "[Htapes Htape]". *) + (* iMod "Hclose'" as "_". *) + (* unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 sample) _) with "[$]") as "[Hsupply Herr]". *) + (* { naive_solver. } *) + (* { simpl; lra. } *) + (* iMod (hocap_tapes_update with "[$][$]") as "[Hauth Hfrag]". *) + (* iMod ("Hrest" $! sample with "[$Herr]") as "HT". *) + (* iFrame. *) + (* iMod ("Hclose" with "[-Hsupply]") as "_". *) + (* { iNext. iFrame. by iApply "H3". } *) + (* iApply fupd_mask_intro_subseteq; first set_solver. *) + (* iSplit. *) + (* - iApply ec_supply_eq; last done. *) + (* simpl. rewrite Nat.eqb_refl. lra. *) + (* - iPureIntro. *) + (* rewrite Forall_app; split; subst; first done. *) + (* eapply Forall_impl; first apply fin.fin_forall_leq. *) + (* simpl; intros; lia. *) + (* Qed. *) + +End impl. + +Section checks. + Context `{H: conerisGS Σ, r1:@rand_spec Σ H, L:randG Σ}. + + 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) }}} + rand_tape #lbl:α #N@ E + {{{ RET #(LitInt n); rand_tapes_frag (L:=L) γ1 α (N, ns) ∗ ⌜n <= N⌝ }}}. + Proof. + iIntros (Hsubset Φ) "(#Hinv &>Hfrag) HΦ". + iDestruct (rand_tapes_valid with "[$]") as "%H'". + wp_apply (rand_tape_spec_some with "[Hfrag]"); first exact. + - by iFrame. + - iIntros. + iApply "HΦ". + iFrame. + iPureIntro. + rewrite Forall_cons in H'. naive_solver. + Qed. + + Local Opaque enum_uniform_fin_list. + + (* Lemma rand_presample_single_spec N E γ2 α (tb:nat) ns T: *) + (* ↑N ⊆ E -> *) + (* is_rand (L:=L) N γ2 -∗ *) + (* rand_tapes_frag (L:=L) γ2 α (tb, ns) -∗ *) + (* (|={E∖↑N, ∅}=> *) + (* ∃ ε (ε2 : fin (S tb) -> R), *) + (* ↯ ε ∗ *) + (* ⌜(∀ x, 0<= ε2 x)%R⌝ ∗ *) + (* ⌜(SeriesC ε2 /((S tb)) <= ε)%R⌝ ∗ *) + (* (∀ x, ↯ (ε2 x) ={∅, E∖↑N}=∗ T ε ε2 x)) -∗ *) + (* wp_update E (∃ ε ε2 x, rand_tapes_frag (L:=L) γ2 α (tb, ns ++ [fin_to_nat x]) ∗ *) + (* T ε ε2 x). *) + (* Proof. *) + (* iIntros (Hsubset) "#Hinv Hfrag Hvs". *) + (* iApply wp_update_state_step_coupl. *) + (* iIntros (??) "[??]". *) + (* iMod (rand_presample_spec _ _ _ _ _ _ (λ ε' num ε2' ns2, *) + (* ∃ x, ⌜ns2 = [x]⌝ ∗ T ε' (λ x, ε2' ([x])) x *) + (* ) with "[//][$][-]")%I as "H"; first done; last first. *) + (* - iDestruct "H" as "(%&%&%&%&Hfrag &%&%&HT)". *) + (* subst. *) + (* by iFrame. *) + (* - iMod "Hvs" as "(%&%ε2&$&%Hpos & %Hineq & Hrest)". *) + (* iModIntro. *) + (* iExists 1, (λ ls, match ls with |[x] => ε2 x | _ => 1 end)%R. *) + (* repeat iSplit. *) + (* + iPureIntro. by intros [|?[|]]. *) + (* + iPureIntro. etrans; last eapply Hineq. *) + (* rewrite !Rdiv_def pow_1. *) + (* apply Rmult_le_compat_r. *) + (* { rewrite -Rdiv_1_l. *) + (* apply Rdiv_INR_ge_0. } *) + (* etrans; last eapply (SeriesC_le_inj _ (λ l, match l with |[x] => Some x | _ => None end)). *) + (* * 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. *) + (* done. *) + (* * done. *) + (* * intros. repeat case_match; by simplify_eq. *) + (* * apply ex_seriesC_finite. *) + (* + iIntros ([|?[|]]) "?"; [by iDestruct (ec_contradict with "[$]") as "%"| |by iDestruct (ec_contradict with "[$]") as "%"]. *) + (* iFrame. *) + (* iMod ("Hrest" with "[$]"). *) + (* by iFrame. *) + (* Qed. *) + + + 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 -> + (SeriesC (λ n, (1 / (S N)) * ε2 n)%R <= ε1)%R → + is_rand (L:=L) NS γ1 -∗ + ▷ rand_tapes_frag (L:=L) γ1 α (N, ns) -∗ + ↯ ε1 -∗ + wp_update E (∃ n, ↯ (ε2 n) ∗ rand_tapes_frag (L:=L) γ1 α (N, ns ++[fin_to_nat n]))%I. + Proof. + iIntros (Hsubset Hpos Hineq) "#Hinv >Htape Herr". + iDestruct (ec_valid with "[$]") as "%Hpos'". + destruct Hpos' as [Hpos' ?]. + iApply wp_update_state_update. + by iApply (rand_tapes_presample with "[$][$][$]"). + Qed. + + +End checks. diff --git a/theories/coneris/primitive_laws.v b/theories/coneris/primitive_laws.v index c2d4bc20..c1eae4b0 100644 --- a/theories/coneris/primitive_laws.v +++ b/theories/coneris/primitive_laws.v @@ -127,7 +127,37 @@ Section tape_interface. iFrame. by rewrite fmap_app. Qed. + + Lemma tapeN_update_append' α N m (ns ns':list (fin (S N))): + tapes_auth 1 m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth 1 (<[α:=(N; ns ++ ns')]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ (fin_to_nat <$> ns')). + Proof. + iIntros "? (%&%&?)". + iMod (ghost_map_update with "[$][$]") as "[??]". + iFrame. + by rewrite fmap_app. + Qed. + Lemma tapeN_ineq α N ns: + α↪N (N; ns) -∗ ⌜Forall (λ n, n<=N)%nat ns⌝. + Proof. + iIntros "(% & <- & H)". + iPureIntro. + eapply Forall_impl. + - apply fin.fin_forall_leq. + - simpl. intros. + lia. + Qed. + + Lemma hocap_tapes_notin α N ns m (f:(nat*list nat)-> nat) g: + α ↪N (N; ns) -∗ ([∗ map] α0↦t ∈ m, α0 ↪N (f t; g t)) -∗ ⌜m!!α=None ⌝. + Proof. + destruct (m!!α) eqn:Heqn; last by iIntros. + iIntros "Hα Hmap". + iDestruct (big_sepM_lookup with "[$]") as "?"; first done. + iExFalso. + iApply (tapeN_tapeN_contradict with "[$][$]"). + Qed. + (* Lemma spec_tapeN_to_empty l M : (l ↪ₛN ( M ; [] ) -∗ l ↪ₛ ( M ; [] )). diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v index e3472ce7..2b7197e7 100644 --- a/theories/coneris/wp_update.v +++ b/theories/coneris/wp_update.v @@ -71,6 +71,14 @@ Section wp_update. iMod "H". by iApply "H". Qed. + Lemma fupd_wp_update_ret E P: + (|={E}=> P) ⊢ wp_update E P. + Proof. + iIntros "H". + iApply fupd_wp_update. + by iApply wp_update_ret. + Qed. + Lemma wp_update_frame_l R E P : R ∗ wp_update E P ⊢ wp_update E (P ∗ R). Proof. @@ -193,6 +201,11 @@ Section wp_update. iApply HP. iFrame. Qed. + Global Instance is_except_0_wp_update E Q : IsExcept0 (wp_update E Q). + Proof. + by rewrite /IsExcept0 -{2}fupd_wp_update -except_0_fupd -fupd_intro. + Qed. + Global Instance elim_modal_fupd_wp p E P Q : ElimModal True p false (|={E}=> P) P (wp_update E Q) (wp_update E Q). Proof. @@ -225,3 +238,316 @@ Section wp_update. End wp_update. +Section state_update. + Context `{!conerisGS Σ}. + Definition state_update_def E P:= + (∀ σ1 ε1, + state_interp σ1 ∗ err_interp ε1 ={E, ∅}=∗ + state_step_coupl σ1 ε1 (λ σ2 ε2, + |={∅, E}=> state_interp σ2 ∗ err_interp ε2 ∗ P + ) + )%I. + + Local Definition state_update_aux : seal (@state_update_def). Proof. by eexists. Qed. + Definition state_update := state_update_aux.(unseal). + Lemma state_update_unseal : state_update = state_update_def. + Proof. rewrite -state_update_aux.(seal_eq) //. Qed. + + Lemma wp_update_state_update E P: + state_update E P -∗ wp_update E P. + Proof. + rewrite state_update_unseal/state_update_def. + iIntros. + by iApply wp_update_state_step_coupl. + Qed. + + Lemma state_update_ret E P: + P -∗ state_update E P. + Proof. + rewrite state_update_unseal/state_update_def. + iIntros. + iApply fupd_mask_intro; first set_solver. + iIntros "Hclose". + iApply state_step_coupl_ret. + iMod "Hclose". + iFrame. by iModIntro. + Qed. + + Global Instance from_modal_state_update_state_update P E : + FromModal True modality_id (state_update E P) (state_update E P) P. + Proof. iIntros (_) "HP /=". by iApply state_update_ret. Qed. + + Lemma state_update_mono_fupd E1 E2 P: + E1 ⊆ E2 -> (|={E2,E1}=> state_update E1 (|={E1, E2}=> P)) -∗ state_update E2 P. + Proof. + rewrite state_update_unseal/state_update_def. + iIntros (Hsubseteq) "Hvs". + iIntros (σ1 ε1) "[H1 H2]". + iMod ("Hvs" with "[$]") as ">?". + iModIntro. + iApply (state_step_coupl_mono with "[][$]"). + iIntros (??) ">(?&?&>?)". by iFrame. + Qed. + + + Lemma state_update_mono E P Q: + (P={E}=∗Q) -∗ state_update E P -∗ state_update E Q. + Proof. + rewrite state_update_unseal/state_update_def. + iIntros "Hvs H". + iIntros (σ1 ε1) "[H1 H2]". + iMod ("H" with "[$]") as "?". + iModIntro. + iApply (state_step_coupl_mono with "[Hvs][$]"). + iIntros (??) ">(?&?&?)". + iFrame. + by iApply "Hvs". + Qed. + + Lemma state_update_mono_fupd' E1 E2 P: + E1 ⊆ E2 -> (state_update E1 P) -∗ state_update E2 P. + Proof. + iIntros. + iApply state_update_mono_fupd; first done. + iApply fupd_mask_intro; first done. + iIntros "Hclose". + iApply (state_update_mono with "[Hclose][$]"). + iIntros. + iModIntro. + by iMod "Hclose". + Qed. + + Lemma state_update_fupd E P: + (|={E}=> state_update E P) -∗ state_update E P. + Proof. + iIntros "H". + iApply state_update_mono_fupd; first done. + iMod "H". + iApply state_update_mono; last done. + by iIntros. + Qed. + + + Lemma state_update_epsilon_err E: + ⊢ state_update E (∃ ε, ⌜(0<ε)%R⌝ ∗ ↯ ε). + Proof. + rewrite state_update_unseal/state_update_def. + iIntros (? ε) "[Hstate Herr]". + iApply fupd_mask_intro; first set_solver. + iIntros "Hclose". + iApply state_step_coupl_ampl'. + iIntros (ε' ?). + iApply state_step_coupl_ret. + assert (ε<=ε')%R as H' by lra. + pose (diff :=((ε' - ε) H')%NNR). + replace (ε') with (ε + diff)%NNR; last (apply nnreal_ext; rewrite /diff; simpl; lra). + iMod (ec_supply_increase _ diff with "[$]") as "[??]". + { rewrite /diff. simpl. lra. } + iFrame. iMod "Hclose". iPureIntro. + rewrite /diff. + simpl. + lra. + Qed. + + Lemma state_update_fupd_change E1 E2 P Q: + (|={E1, E2}=> P) -∗ (P-∗ state_update E2 (|={E2, E1}=> Q)) -∗ state_update E1 Q. + Proof. + iIntros "H1 H2". + rewrite state_update_unseal/state_update_def. + iIntros (??) "[??]". + iMod "H1". + iMod ("H2" with "[$][$]") as "H2". + iModIntro. + iApply state_step_coupl_mono; last done. + simpl. + iIntros (??) ">(?&?&>?)". + by iFrame. + Qed. + + Global Instance elim_modal_bupd_state_update p E P Q : + ElimModal True p false (|==> P) P (state_update E Q) (state_update E Q). + Proof. + intros ?. + rewrite bi.intuitionistically_if_elim/=. + iIntros "[H1 H2]". + iApply state_update_fupd. + iMod "H1". + iModIntro. + by iApply "H2". + Qed. + + Global Instance elim_modal_fupd_state_update p E1 E2 P Q : + ElimModal (True) p false + (|={E1,E2}=> P) P + (state_update E1 Q) (state_update E2 (|={E2, E1}=> Q)). + Proof. + intros ?. + rewrite bi.intuitionistically_if_elim/=. + iIntros "[??]". + iApply (state_update_fupd_change with "[$][$]"). + Qed. + + Lemma state_update_bind E P Q: + state_update E P ∗ (P -∗ state_update E Q) ⊢ state_update E Q. + Proof. + rewrite state_update_unseal/state_update_def. + iIntros "[H1 H2]" (??) "[??]". + iMod ("H1" with "[$]") as "H1". + iModIntro. + iApply (state_step_coupl_bind with "[H2][$]"). + iIntros (??) "H1". + iApply fupd_state_step_coupl. + iMod "H1" as "(?&?&?)". + by iMod ("H2" with "[$][$]"). + Qed. + + Global Instance elim_modal_state_update_state_update p E1 E2 P Q : + ElimModal (E1 ⊆ E2) p false (state_update E1 Q) Q (state_update E2 P) (state_update E2 P). + Proof. + iIntros (?) "[H1 H2]". + rewrite bi.intuitionistically_if_elim. + iApply state_update_mono_fupd; first exact. + iApply fupd_mask_intro; first exact; iIntros "Hclose". + iApply state_update_bind; iFrame. + iIntros. + iApply (state_update_fupd_change with "[$]"). + iIntros. + iDestruct ("H2" with "[$]") as "H". + iApply (state_update_mono); last done. + iIntros. + iModIntro. + by iApply fupd_mask_intro_subseteq. + Qed. + + Global Instance elim_modal_state_update_wp_update p E1 E2 P Q : + ElimModal (E1 ⊆ E2) p false (state_update E1 Q) Q (wp_update E2 P) (wp_update E2 P). + Proof. + (* rewrite state_update_unseal/state_update_def. *) + iIntros (?) "[H1 H2]". + iApply (wp_update_bind). + iFrame. + iApply wp_update_state_update. + iIntros. + iApply state_update_mono_fupd; first exact. + iApply fupd_mask_intro; first done. + iIntros "Hclose". + destruct p; simpl. + - iDestruct (bi.intuitionistically_elim with "[$]") as "H1". + iMod "H1". + iMod "Hclose" as "_". + iModIntro. + by iApply fupd_mask_intro_subseteq. + - iMod "H1". + iMod "Hclose" as "_". + iModIntro. + by iApply fupd_mask_intro_subseteq. + Qed. + + Global Instance elim_modal_state_update_wp e Φ p E1 E2 P : + ElimModal (E1 ⊆ E2) p false (state_update E1 P) P (WP e @ E2 {{ Φ }}) (WP e @ E2 {{ Φ }}). + Proof. + destruct p. + all: iIntros (?); simpl; iIntros "[H1 H2]". + 1: iDestruct (bi.intuitionistically_elim with "[$]") as "H1". + all: iDestruct (state_update_mono_fupd with "[H1]") as "H1"; first exact; + last (iDestruct (wp_update_state_update with "[$]") as "H1"; iMod "H1"; by iApply "H2"). + all: iApply fupd_mask_intro; first exact; iIntros "Hclose"; iMod "H1"; iModIntro; by iMod "Hclose". + Qed. + + Lemma state_update_wp E P e Φ: + (state_update E P) -∗ (P -∗ WP e @ E {{Φ}}) -∗ WP e @ E {{Φ}}. + Proof. + iIntros ">? H". + by iApply "H". + Qed. + + Global Instance is_except_0_state_update E Q : IsExcept0 (state_update E Q). + Proof. + rewrite /IsExcept0. + iIntros. + iApply (state_update_fupd E Q). by rewrite -except_0_fupd -fupd_intro. + Qed. + + Lemma state_update_frame_l R E P : + R ∗ state_update E P ⊢ state_update E (P ∗ R). + Proof. + iIntros "[HR H]". + iMod "H". + iModIntro. + iFrame. + Qed. + + Global Instance frame_state_update p E R P Q: + Frame p R P Q → Frame p R (state_update E P) (state_update E Q). + Proof. + rewrite /Frame=> HR. + rewrite state_update_frame_l. + iIntros ">[??]". + iModIntro. + iApply HR; iFrame. + Qed. + + Global Instance from_pure_bupd_state_update b E P φ : + FromPure b P φ → FromPure b (state_update E P) φ. + Proof. + rewrite /FromPure=> HP. + iIntros "H !>". + by iApply HP. + Qed. + + Global Instance into_wand_state_update p q E R P Q : + IntoWand false false R P Q → IntoWand p q (state_update E R) (state_update E P) (state_update E Q). + Proof. + rewrite /IntoWand /= => HR. + rewrite !bi.intuitionistically_if_elim. + iIntros ">HR >HP !>". iApply (HR with "HR HP"). + Qed. + + Global Instance into_wand_bupd_persistent_state_update p q E R P Q : + IntoWand false q R P Q → IntoWand p q (state_update E R) P (state_update E Q). + Proof. + rewrite /IntoWand /= => HR. rewrite bi.intuitionistically_if_elim. + iIntros ">HR HP !>". + iApply (HR with "HR HP"). + Qed. + + Global Instance into_wand_bupd_args_state_update p q E R P Q : + IntoWand p false R P Q → IntoWand' p q R (state_update E P) (state_update E Q). + Proof. + rewrite /IntoWand' /IntoWand /= => ->. + rewrite bi.intuitionistically_if_elim. + iIntros "Hw HP". + iMod "HP". + iModIntro. + by iApply "Hw". + Qed. + + Global Instance from_sep_bupd_state_update E P Q1 Q2 : + FromSep P Q1 Q2 → FromSep (state_update E P) (state_update E Q1) (state_update E Q2). + Proof. + rewrite /FromSep=> HP. + iIntros "[>HQ1 >HQ2] !>". + iApply HP. iFrame. + Qed. + + Global Instance from_exist_state_update {B} P E (Φ : B → iProp Σ) : + FromExist P Φ → FromExist (state_update E P) (λ b, state_update E (Φ b))%I. + Proof. + rewrite /FromExist => HP. + iIntros "[%x >Hx] !>". + iApply HP. eauto. + Qed. + + Global Instance into_forall_state_update {B} P E (Φ : B → iProp Σ) : + IntoForall P Φ → IntoForall (state_update E P) (λ b, state_update E (Φ b))%I. + Proof. + rewrite /IntoForall=>HP. + iIntros "> H" (b) "!>". + iApply (HP with "H"). + Qed. + + Global Instance from_assumption_state_update p E P Q : + FromAssumption p P Q → KnownRFromAssumption p P (state_update E Q). + Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. iApply state_update_ret. Qed. + +End state_update. diff --git a/theories/prelude/fin.v b/theories/prelude/fin.v index 5bf91240..67d0c0a7 100644 --- a/theories/prelude/fin.v +++ b/theories/prelude/fin.v @@ -161,8 +161,20 @@ Section fin. rewrite f_inv_cancel_r //. Qed. - - + Lemma nat_list_to_fin_list xs N: + Forall (λ x, x < N) xs -> ∃ (xs' : list (fin N)), fin_to_nat <$> xs' = xs. + Proof. + induction xs. + - intros. by exists []. + - rewrite Forall_cons_iff. + intros [P H]. + apply IHxs in H. + destruct H as [xs' <-]. + eexists (nat_to_fin P :: _). + simpl. f_equal. + by rewrite fin_to_nat_to_fin. + Qed. + (* Adapted from Coq standard library FinFun *) Definition bFunNM n m (f:nat->nat) := forall x, x < n -> f x < m. diff --git a/theories/prelude/stdpp_ext.v b/theories/prelude/stdpp_ext.v index e8cf0184..a11247ae 100644 --- a/theories/prelude/stdpp_ext.v +++ b/theories/prelude/stdpp_ext.v @@ -371,6 +371,22 @@ Section list. a ∈ l1 ∧ b ∈ l2 → (a, b) ∈ list_prod l1 l2. Proof. apply elem_of_list_prod. Qed. + Lemma fmap_inj (f:A -> B) (l1 l2: list A): + Inj (=) (=) f -> f<$>l1=f<$>l2 -> l1 = l2. + Proof. + intros H. + revert l2. + induction l1. + - intros ? K. simpl in *. + by erewrite fmap_nil_inv. + - intros l2 K. + rewrite fmap_cons in K. + destruct l2. + + rewrite fmap_nil in K. simplify_eq. + + rewrite fmap_cons in K. + by simplify_eq. + Qed. + End list. Tactic Notation "case_match" "in" ident(H) "eqn" ":" ident(Hd) := diff --git a/theories/prelude/uniform_list.v b/theories/prelude/uniform_list.v index 5a946068..bec7bc0f 100644 --- a/theories/prelude/uniform_list.v +++ b/theories/prelude/uniform_list.v @@ -4,19 +4,19 @@ Require Import Coq.Program.Equality. Set Default Proof Using "Type*". Section uniform_list. - Variables N:nat. + Context `{Hfinite: Finite A}. Fixpoint enum_uniform_list (p:nat):= match p with | O => [[]] | S p' => - x ← enum (fin (S N)); + x ← enum (A); y ← enum_uniform_list p'; mret (x::y) end. Lemma enum_uniform_list_S (p:nat) : enum_uniform_list (S p) = - x ← enum (fin (S N)); + x ← enum A; y ← enum_uniform_list p; mret (x::y). Proof. @@ -31,7 +31,8 @@ Section uniform_list. + simpl. rewrite elem_of_list_singleton. by intros ->. + rewrite enum_uniform_list_S. rewrite elem_of_list_bind. elim. intros x. rewrite elem_of_list_bind. do 2 elim. intros y. - intros [?%elem_of_list_ret H%IHp]. subst. done. + intros [?%elem_of_list_ret ?]. subst. + simpl. intros. f_equal. naive_solver. - revert l; induction p; intros l. + simpl. set_unfold. intros ?%nil_length_inv. naive_solver. + destruct l as [|t l'] eqn:Heqn; first done. @@ -51,7 +52,7 @@ Section uniform_list. - symmetry; by rewrite Nat.eqb_neq. Qed. - Lemma bind_length1 {A:Type} (l:list (list A)) a: + Lemma bind_length1 (l:list (list A)) a: length (l ≫= λ y, mret (a :: y)) = length l. Proof. induction l. @@ -60,7 +61,7 @@ Section uniform_list. rewrite app_length. simpl. f_equal. done. Qed. - Lemma bind_length2 {A:Type} (l1 : list A) l2: + Lemma bind_length2 (l1 : list A) l2: length (l1 ≫= λ x, l2 ≫= λ y, mret (x :: y)) = length l1 * length l2. Proof. revert l2. @@ -73,14 +74,13 @@ Section uniform_list. Qed. Lemma enum_uniform_list_length p: - length (enum_uniform_list p) = (S N)^p. + length (enum_uniform_list p) = (length (enum A))^p. Proof. induction p. - done. - rewrite enum_uniform_list_S. rewrite bind_length2. rewrite IHp. - rewrite length_enum_fin. rewrite Nat.pow_succ_r'. lia. Qed. @@ -100,3 +100,44 @@ Section uniform_list. Qed. End uniform_list. + + +Section uniform_fin_list. + Variables N:nat. + + Definition enum_uniform_fin_list:= + enum_uniform_list (A:=fin (S N)). + + Lemma enum_uniform_fin_list_S (p:nat) : + enum_uniform_fin_list (S p) = + x ← enum (fin (S N)); + y ← enum_uniform_fin_list p; + mret (x::y). + Proof. + simpl. done. + Qed. + + Lemma elem_of_enum_uniform_fin_list l p: + l ∈ enum_uniform_fin_list p <-> length l = p. + Proof. + apply elem_of_enum_uniform_list. + Qed. + + Lemma elem_of_enum_uniform_fin_list' l p: + bool_decide (l∈enum_uniform_fin_list p) = (length l =? p). + Proof. + apply elem_of_enum_uniform_list'. + Qed. + + Lemma enum_uniform_fin_list_length p: + length (enum_uniform_fin_list p) = (S N)^p. + Proof. + by rewrite enum_uniform_list_length length_enum_fin. + Qed. + + Lemma NoDup_enum_uniform_fin_list p: + NoDup (enum_uniform_fin_list p). + Proof. + apply NoDup_enum_uniform_list. + Qed. +End uniform_fin_list. diff --git a/theories/prob/countable_sum.v b/theories/prob/countable_sum.v index 19a24450..7d872fe7 100644 --- a/theories/prob/countable_sum.v +++ b/theories/prob/countable_sum.v @@ -2,7 +2,7 @@ From Coq Require Import Reals Psatz. From Coquelicot Require Import Series Hierarchy Lim_seq Rbar Lub. From stdpp Require Import option. From stdpp Require Export countable finite gmap. -From clutch.prelude Require Import base Reals_ext Coquelicot_ext Series_ext stdpp_ext classical fin. +From clutch.prelude Require Import base Reals_ext Coquelicot_ext Series_ext stdpp_ext classical fin uniform_list. Set Default Proof Using "Type*". Import Hierarchy. @@ -710,6 +710,21 @@ Section filter. End filter. +Lemma ex_seriesC_list_length `{Finite A} (f:list A -> R) num: + (forall x, (0≠f x)%R -> length x = num) -> + ex_seriesC f. +Proof. + intros. + eapply (ex_seriesC_ext (λ x, if bool_decide(x∈enum_uniform_list num) then f x else 0))%R. + - intros n. + case_bool_decide as K; first done. + destruct (Req_dec (f n) 0); first done. + exfalso. + apply K. apply elem_of_enum_uniform_list. + naive_solver. + - apply ex_seriesC_list. +Qed. + Lemma SeriesC_Series_nat (f : nat → R) : SeriesC f = Series f. Proof. diff --git a/theories/prob/distribution.v b/theories/prob/distribution.v index 193aaa72..50ca8f5d 100644 --- a/theories/prob/distribution.v +++ b/theories/prob/distribution.v @@ -2247,8 +2247,8 @@ Section uniform. End uniform. -(** Uniform lists *) -Section uniform_lists. +(** Uniform fin lists *) +Section uniform_fin_lists. Program Definition dunifv (N p: nat): distr (list (fin (S N))) := MkDistr (λ x, if (bool_decide (length x = p)) then /(S N^p)%nat else 0) _ _ _. Next Obligation. @@ -2264,19 +2264,19 @@ Section uniform_lists. intros. eapply ex_seriesC_ext; last apply ex_seriesC_list. simpl. intros. erewrite bool_decide_ext; first done. - by erewrite elem_of_enum_uniform_list. + by erewrite elem_of_enum_uniform_fin_list. Qed. Next Obligation. intros N p. erewrite SeriesC_ext. - - erewrite SeriesC_list_2; last apply NoDup_enum_uniform_list. - rewrite enum_uniform_list_length. + - erewrite SeriesC_list_2; last apply NoDup_enum_uniform_fin_list. + rewrite enum_uniform_fin_list_length. erewrite Rinv_l; first done. apply not_0_INR. apply Nat.pow_nonzero. lia. - intros. erewrite bool_decide_ext; first done. - by erewrite elem_of_enum_uniform_list. + by erewrite elem_of_enum_uniform_fin_list. Qed. Lemma dunifv_pmf N p v: @@ -2287,15 +2287,15 @@ Section uniform_lists. SeriesC (dunifv N p) = 1. Proof. erewrite SeriesC_ext. - - erewrite SeriesC_list_2; last apply NoDup_enum_uniform_list. - rewrite enum_uniform_list_length. + - erewrite SeriesC_list_2; last apply NoDup_enum_uniform_fin_list. + rewrite enum_uniform_fin_list_length. erewrite Rinv_l; first done. apply not_0_INR. apply Nat.pow_nonzero. lia. - intros. rewrite /dunifv_pmf. erewrite bool_decide_ext; first done. - by erewrite elem_of_enum_uniform_list. + by erewrite elem_of_enum_uniform_fin_list. Qed. Lemma dunifv_pos N p v: @@ -2316,7 +2316,7 @@ Section uniform_lists. done. Qed. -End uniform_lists. +End uniform_fin_lists. Ltac inv_distr := repeat