From ef09370560cf28fc07bcf24828545192bbab8ce0 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 27 Sep 2024 16:12:47 +0200 Subject: [PATCH] Updated hocap rand and hocap flip. TODO: rand counter and its implementations --- .../coneris/examples/random_counter/impl1.v | 568 +++++++++--------- theories/coneris/lib/hocap_flip.v | 101 ++-- theories/coneris/lib/hocap_rand.v | 191 +++--- 3 files changed, 419 insertions(+), 441 deletions(-) diff --git a/theories/coneris/examples/random_counter/impl1.v b/theories/coneris/examples/random_counter/impl1.v index 03ab881e..22519878 100644 --- a/theories/coneris/examples/random_counter/impl1.v +++ b/theories/coneris/examples/random_counter/impl1.v @@ -1,298 +1,298 @@ -From iris.algebra Require Import frac_auth. -From iris.base_logic.lib Require Import invariants. -From clutch.coneris Require Import coneris hocap hocap_rand random_counter. +(* From iris.algebra Require Import frac_auth. *) +(* From iris.base_logic.lib Require Import invariants. *) +(* From clutch.coneris Require Import coneris hocap hocap_rand random_counter. *) -Set Default Proof Using "Type*". +(* Set Default Proof Using "Type*". *) -Section impl1. - Context `{H:conerisGS Σ, r1:@rand_spec Σ H, L:randG Σ, !inG Σ (frac_authR natR)}. +(* Section impl1. *) +(* Context `{H:conerisGS Σ, r1:@rand_spec Σ H, L:randG Σ, !inG Σ (frac_authR natR)}. *) - Definition new_counter1 : val:= λ: "_", ref #0. - 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_randG : randG Σ; - counterG1_frac_authR:: inG Σ (frac_authR natR) }. +(* Definition new_counter1 : val:= λ: "_", ref #0. *) +(* 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_randG : randG Σ; *) +(* counterG1_frac_authR:: inG Σ (frac_authR natR) }. *) - 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. +(* 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: - {{{ True }}} - new_counter1 #() @ E - {{{ (c:val), RET c; - ∃ γ1 γ2, is_counter1 N c γ1 γ2 ∗ own γ2 (◯F 0%nat) - }}}. - Proof. - rewrite /new_counter1. - iIntros (Φ) "_ HΦ". - wp_pures. - iMod (rand_inv_create_spec) as "(%γ1 & #Hinv)". - wp_alloc l as "Hl". - 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 _ _ (counter_inv_pred1 (#l) γ2) with "[$Hl $H5]") as "#Hinv'"; first done. - iApply "HΦ". - iFrame. - iModIntro. - iExists _. by iSplit. - Qed. +(* Lemma new_counter_spec1 E N: *) +(* {{{ True }}} *) +(* new_counter1 #() @ E *) +(* {{{ (c:val), RET c; *) +(* ∃ γ1 γ2, is_counter1 N c γ1 γ2 ∗ own γ2 (◯F 0%nat) *) +(* }}}. *) +(* Proof. *) +(* rewrite /new_counter1. *) +(* iIntros (Φ) "_ HΦ". *) +(* wp_pures. *) +(* iMod (rand_inv_create_spec) as "(%γ1 & #Hinv)". *) +(* wp_alloc l as "Hl". *) +(* 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 _ _ (counter_inv_pred1 (#l) γ2) with "[$Hl $H5]") as "#Hinv'"; first done. *) +(* iApply "HΦ". *) +(* iFrame. *) +(* iModIntro. *) +(* iExists _. by iSplit. *) +(* 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. *) - (* iModIntro. *) - (* wp_pures. *) - (* by iApply "HΦ". *) - (* 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. *) *) +(* (* iModIntro. *) *) +(* (* wp_pures. *) *) +(* (* by iApply "HΦ". *) *) +(* (* Qed. *) *) - Lemma allocate_tape_spec1 N E c γ1 γ2: - ↑N ⊆ E-> - {{{ is_counter1 N c γ1 γ2 }}} - allocate_tape1 #() @ E - {{{ (v:val), RET v; - ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, []) - }}}. - Proof. - iIntros (Hsubset Φ) "[#Hinv #Hinv'] HΦ". - rewrite /allocate_tape1. - wp_pures. - wp_apply rand_allocate_tape_spec; [by eapply nclose_subseteq'|done..]. - Qed. +(* Lemma allocate_tape_spec1 N E c γ1 γ2: *) +(* ↑N ⊆ E-> *) +(* {{{ is_counter1 N c γ1 γ2 }}} *) +(* allocate_tape1 #() @ E *) +(* {{{ (v:val), RET v; *) +(* ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, []) *) +(* }}}. *) +(* Proof. *) +(* iIntros (Hsubset Φ) "[#Hinv #Hinv'] HΦ". *) +(* rewrite /allocate_tape1. *) +(* wp_pures. *) +(* wp_apply rand_allocate_tape_spec; [by eapply nclose_subseteq'|done..]. *) +(* Qed. *) - Lemma incr_counter_tape_spec_some1 N E c γ1 γ2 (Q:nat->nat -> list nat -> iProp Σ) (α:loc) : - ↑N⊆E -> - {{{ is_counter1 N c γ1 γ2 ∗ - ( |={E∖ ↑N, ∅}=> - ∃ n ns, rand_tapes_frag (L:=L) γ1 α (3, n::ns) ∗ - (rand_tapes_frag (L:=L) γ1 α (3, ns) ={∅, E∖↑N}=∗ - ∀ (z:nat), own γ2 (●F z) - ={E∖↑N}=∗ - own γ2 (●F (z+n)) ∗ Q z n ns) - ) - }}} - incr_counter_tape1 c #lbl:α @ E - {{{ (z n:nat), RET (#z, #n); ∃ ns, Q z n ns}}}. - Proof. - iIntros (Hsubset Φ) "([#Hinv #Hinv'] & Hvs) HΦ". - rewrite /incr_counter_tape1. - wp_pures. - wp_apply (rand_tape_spec_some _ _ _ - (λ n ns, ∀ (z:nat), own γ2 (●F z)={E∖↑N}=∗ - own γ2 (●F (z+n)) ∗ Q z n ns)%I with "[Hvs]"); [by eapply nclose_subseteq'|iSplit; first done|..]. - - iMod (fupd_mask_subseteq (E ∖ ↑N)) as "Hclose". - + apply difference_mono_l. - by apply nclose_subseteq'. - + iMod "Hvs" as "(%n & %ns & Hfrag & Hrest)". - iModIntro. - iFrame. - iIntros "Hfrag". - iMod ("Hrest" with "[$]") as "Hrest". - by iMod "Hclose" as "_". - - iIntros (n) "(%ns & Hvs)". - wp_pures. - wp_bind (FAA _ _). - iInv "Hinv'" as ">(%&%&-> & ?&?)" "Hclose". - wp_faa. - 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 "[-HΦ HQ]") as "_"; first by iFrame. - iModIntro. - wp_pures. - iApply "HΦ". by iFrame. - Qed. +(* Lemma incr_counter_tape_spec_some1 N E c γ1 γ2 (Q:nat->nat -> list nat -> iProp Σ) (α:loc) : *) +(* ↑N⊆E -> *) +(* {{{ is_counter1 N c γ1 γ2 ∗ *) +(* ( |={E∖ ↑N, ∅}=> *) +(* ∃ n ns, rand_tapes_frag (L:=L) γ1 α (3, n::ns) ∗ *) +(* (rand_tapes_frag (L:=L) γ1 α (3, ns) ={∅, E∖↑N}=∗ *) +(* ∀ (z:nat), own γ2 (●F z) *) +(* ={E∖↑N}=∗ *) +(* own γ2 (●F (z+n)) ∗ Q z n ns) *) +(* ) *) +(* }}} *) +(* incr_counter_tape1 c #lbl:α @ E *) +(* {{{ (z n:nat), RET (#z, #n); ∃ ns, Q z n ns}}}. *) +(* Proof. *) +(* iIntros (Hsubset Φ) "([#Hinv #Hinv'] & Hvs) HΦ". *) +(* rewrite /incr_counter_tape1. *) +(* wp_pures. *) +(* wp_apply (rand_tape_spec_some _ _ _ *) +(* (λ n ns, ∀ (z:nat), own γ2 (●F z)={E∖↑N}=∗ *) +(* own γ2 (●F (z+n)) ∗ Q z n ns)%I with "[Hvs]"); [by eapply nclose_subseteq'|iSplit; first done|..]. *) +(* - iMod (fupd_mask_subseteq (E ∖ ↑N)) as "Hclose". *) +(* + apply difference_mono_l. *) +(* by apply nclose_subseteq'. *) +(* + iMod "Hvs" as "(%n & %ns & Hfrag & Hrest)". *) +(* iModIntro. *) +(* iFrame. *) +(* iIntros "Hfrag". *) +(* iMod ("Hrest" with "[$]") as "Hrest". *) +(* by iMod "Hclose" as "_". *) +(* - iIntros (n) "(%ns & Hvs)". *) +(* wp_pures. *) +(* wp_bind (FAA _ _). *) +(* iInv "Hinv'" as ">(%&%&-> & ?&?)" "Hclose". *) +(* wp_faa. *) +(* 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 "[-HΦ HQ]") as "_"; first by iFrame. *) +(* iModIntro. *) +(* wp_pures. *) +(* iApply "HΦ". by iFrame. *) +(* Qed. *) - Lemma counter_presample_spec1 NS E T γ1 γ2 c: - ↑NS ⊆ E -> - is_counter1 NS c γ1 γ2 -∗ - ( |={E∖↑NS,∅}=> - ∃ ε α ε2 num ns, - ↯ ε ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, ns) ∗ - ⌜(∀ n, 0<=ε2 n)%R⌝ ∗ - ⌜(SeriesC (λ l, if bool_decide (l∈fmap (λ x, fmap (FMap:=list_fmap) fin_to_nat x) (enum_uniform_fin_list 3%nat num)) then ε2 l else 0%R) / (4^num) <= ε)%R⌝ ∗ - (∀ ns', ↯ (ε2 ns') ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, ns++ns')={∅,E∖↑NS}=∗ - T ε α ε2 num ns ns' - ))-∗ - wp_update E (∃ ε α ε2 num ns ns', T ε α ε2 num ns ns'). - Proof. - iIntros (Hsubset) "[#Hinv #Hinv'] Hvs". - iMod (rand_presample_spec _ _ (λ ε num tb ε2 α ns ns', - ∃ ε2', ⌜∀ xs ys, fin_to_nat <$> xs = ys -> ε2 xs = ε2' ys⌝ ∗ - ⌜tb = 3⌝ ∗ T ε α ε2' num ns (fin_to_nat <$> ns'))%I with "[//][Hvs]") as "H"; first by apply nclose_subseteq'. - + iMod (fupd_mask_subseteq (E ∖ ↑NS)) as "Hclose". - { apply difference_mono_l. - by apply nclose_subseteq'. } - iMod "Hvs" as "(%ε & %α & %ε2 & %num & %ns & Herr & Hfrag & %Hpos & %Hineq & Hrest)". - iFrame. - iModIntro. - iExists num, (λ ls, ε2 (fin_to_nat <$> ls)). - repeat iSplit. - * done. - * iPureIntro. - etrans; last exact. - apply Req_le. - replace (INR 4) with 4%R; last (simpl; lra). - f_equal. - rewrite !SeriesC_list. - -- by rewrite foldr_fmap. - -- apply NoDup_fmap. - ++ apply list_fmap_eq_inj. - apply fin_to_nat_inj. - ++ apply NoDup_enum_uniform_fin_list. - -- apply NoDup_enum_uniform_fin_list. - * iIntros (ns') "[Herr Hfrag]". - iMod ("Hrest" with "[$]") as "HT". - iMod "Hclose" as "_". - iModIntro. - iFrame. - repeat iSplit; iPureIntro; last done. - by intros ??<-. - + iDestruct "H" as "(%ε & %num & %tb & %ε2 & %α & %ns & %ns' & %ε2' & % & -> & HT)". - iModIntro. iFrame. - Qed. +(* Lemma counter_presample_spec1 NS E T γ1 γ2 c: *) +(* ↑NS ⊆ E -> *) +(* is_counter1 NS c γ1 γ2 -∗ *) +(* ( |={E∖↑NS,∅}=> *) +(* ∃ ε α ε2 num ns, *) +(* ↯ ε ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, ns) ∗ *) +(* ⌜(∀ n, 0<=ε2 n)%R⌝ ∗ *) +(* ⌜(SeriesC (λ l, if bool_decide (l∈fmap (λ x, fmap (FMap:=list_fmap) fin_to_nat x) (enum_uniform_fin_list 3%nat num)) then ε2 l else 0%R) / (4^num) <= ε)%R⌝ ∗ *) +(* (∀ ns', ↯ (ε2 ns') ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, ns++ns')={∅,E∖↑NS}=∗ *) +(* T ε α ε2 num ns ns' *) +(* ))-∗ *) +(* wp_update E (∃ ε α ε2 num ns ns', T ε α ε2 num ns ns'). *) +(* Proof. *) +(* iIntros (Hsubset) "[#Hinv #Hinv'] Hvs". *) +(* iMod (rand_presample_spec _ _ (λ ε num tb ε2 α ns ns', *) +(* ∃ ε2', ⌜∀ xs ys, fin_to_nat <$> xs = ys -> ε2 xs = ε2' ys⌝ ∗ *) +(* ⌜tb = 3⌝ ∗ T ε α ε2' num ns (fin_to_nat <$> ns'))%I with "[//][Hvs]") as "H"; first by apply nclose_subseteq'. *) +(* + iMod (fupd_mask_subseteq (E ∖ ↑NS)) as "Hclose". *) +(* { apply difference_mono_l. *) +(* by apply nclose_subseteq'. } *) +(* iMod "Hvs" as "(%ε & %α & %ε2 & %num & %ns & Herr & Hfrag & %Hpos & %Hineq & Hrest)". *) +(* iFrame. *) +(* iModIntro. *) +(* iExists num, (λ ls, ε2 (fin_to_nat <$> ls)). *) +(* repeat iSplit. *) +(* * done. *) +(* * iPureIntro. *) +(* etrans; last exact. *) +(* apply Req_le. *) +(* replace (INR 4) with 4%R; last (simpl; lra). *) +(* f_equal. *) +(* rewrite !SeriesC_list. *) +(* -- by rewrite foldr_fmap. *) +(* -- apply NoDup_fmap. *) +(* ++ apply list_fmap_eq_inj. *) +(* apply fin_to_nat_inj. *) +(* ++ apply NoDup_enum_uniform_fin_list. *) +(* -- apply NoDup_enum_uniform_fin_list. *) +(* * iIntros (ns') "[Herr Hfrag]". *) +(* iMod ("Hrest" with "[$]") as "HT". *) +(* iMod "Hclose" as "_". *) +(* iModIntro. *) +(* iFrame. *) +(* repeat iSplit; iPureIntro; last done. *) +(* by intros ??<-. *) +(* + iDestruct "H" as "(%ε & %num & %tb & %ε2 & %α & %ns & %ns' & %ε2' & % & -> & HT)". *) +(* iModIntro. iFrame. *) +(* Qed. *) - Lemma read_counter_spec1 N E c γ1 γ2 Q: - ↑N ⊆ E -> - {{{ is_counter1 N c γ1 γ2 ∗ - (∀ (z:nat), own γ2 (●F z) ={E∖↑N}=∗ - own γ2 (●F z) ∗ Q z) +(* Lemma read_counter_spec1 N E c γ1 γ2 Q: *) +(* ↑N ⊆ E -> *) +(* {{{ 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 #Hinv'] & Hvs) HΦ". - rewrite /read_counter1. - wp_pure. - iInv "Hinv'" as ">( %l & %z & -> & H5 & H6)" "Hclose". - wp_load. - 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. +(* }}} *) +(* read_counter1 c @ E *) +(* {{{ (n':nat), RET #n'; Q n' *) +(* }}}. *) +(* Proof. *) +(* iIntros (Hsubset Φ) "([#Hinv #Hinv'] & Hvs) HΦ". *) +(* rewrite /read_counter1. *) +(* wp_pure. *) +(* iInv "Hinv'" as ">( %l & %z & -> & H5 & H6)" "Hclose". *) +(* wp_load. *) +(* 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. *) -End impl1. +(* End impl1. *) -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; - tape_name := rand_tape_name; - counter_name :=gname; - 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); - 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". - iDestruct (rand_tapes_auth_exclusive with "[$][$]") as "[]". -Qed. -Next Obligation. - simpl. - iIntros. - iDestruct (rand_tapes_frag_exclusive with "[$][$]") as "[]". -Qed. -Next Obligation. - simpl. - iIntros. - iDestruct (rand_tapes_agree with "[$][$]") as "%H". - iPureIntro. - apply lookup_fmap_Some in H as (?&?&?). - by simplify_eq. -Qed. -Next Obligation. - iIntros. - 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". - 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. - by apply nat_included. -Qed. -Next Obligation. - simpl. - iIntros. - rewrite frac_auth_frag_op. rewrite own_op. - iSplit; iIntros; iFrame. -Qed. -Next Obligation. - 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". - iMod (own_update_2 _ _ _ (_ ⋅ _) with "[$][$]") as "[$$]"; last done. - apply frac_auth_update. - apply nat_local_update. lia. -Qed. +(* 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; *) +(* tape_name := rand_tape_name; *) +(* counter_name :=gname; *) +(* 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); *) +(* 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". *) +(* iDestruct (rand_tapes_auth_exclusive with "[$][$]") as "[]". *) +(* Qed. *) +(* Next Obligation. *) +(* simpl. *) +(* iIntros. *) +(* iDestruct (rand_tapes_frag_exclusive with "[$][$]") as "[]". *) +(* Qed. *) +(* Next Obligation. *) +(* simpl. *) +(* iIntros. *) +(* iDestruct (rand_tapes_agree with "[$][$]") as "%H". *) +(* iPureIntro. *) +(* apply lookup_fmap_Some in H as (?&?&?). *) +(* by simplify_eq. *) +(* Qed. *) +(* Next Obligation. *) +(* iIntros. *) +(* 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". *) +(* 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. *) +(* by apply nat_included. *) +(* Qed. *) +(* Next Obligation. *) +(* simpl. *) +(* iIntros. *) +(* rewrite frac_auth_frag_op. rewrite own_op. *) +(* iSplit; iIntros; iFrame. *) +(* Qed. *) +(* Next Obligation. *) +(* 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". *) +(* iMod (own_update_2 _ _ _ (_ ⋅ _) with "[$][$]") as "[$$]"; last done. *) +(* apply frac_auth_update. *) +(* apply nat_local_update. lia. *) +(* Qed. *) diff --git a/theories/coneris/lib/hocap_flip.v b/theories/coneris/lib/hocap_flip.v index dab64a01..c31d5a29 100644 --- a/theories/coneris/lib/hocap_flip.v +++ b/theories/coneris/lib/hocap_flip.v @@ -49,27 +49,26 @@ Class flip_spec `{!conerisGS Σ} := FlipSpec ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ flip_tapes_frag (L:=L) γ1 α [] }}}; - flip_tape_spec_some {L: flipG Σ} N E γ1 (Q:bool -> list bool -> iProp Σ) (α:loc) : + flip_tape_spec_some {L: flipG Σ} N E γ1 (Q:bool -> list bool -> iProp Σ) (α:loc) n ns: ↑N⊆E -> - {{{ is_flip (L:=L) N γ1 ∗ - (|={E∖↑N, ∅}=> - ∃ n ns, flip_tapes_frag (L:=L) γ1 α (n::ns) ∗ - (flip_tapes_frag (L:=L) γ1 α ns ={∅, E∖↑N}=∗ Q n ns)) + {{{ is_flip (L:=L) N γ1 ∗ flip_tapes_frag (L:=L) γ1 α (n::ns) }}} flip_tape #lbl:α @ E - {{{ (n:bool), RET #n; ∃ ns, Q n ns}}}; + {{{ RET #n; flip_tapes_frag (L:=L) γ1 α ns }}}; - flip_presample_spec {L: flipG Σ} NS E T γ1: + 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 α ns, ↯ ε ∗ flip_tapes_frag (L:=L) γ1 α ns ∗ - ⌜(∀ l, length l = num -> 0<=ε2 l)%R⌝ ∗ - ⌜(SeriesC (λ l, if length l =? num then ε2 l else 0) /(2^num) <= ε)%R⌝∗ - (∀ ns', ↯ (ε2 ns') ∗ flip_tapes_frag (L:=L) γ1 α (ns ++ ns') - ={∅, E∖↑NS}=∗ T ε num ε2 α ns 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 ns', T ε num ε2 α ns ns') + wp_update E (∃ ε num ε2 ns', T ε num ε2 ns' ∗ + flip_tapes_frag (L:=L) γ1 α (ns ++ ns')) }. @@ -138,45 +137,33 @@ Section instantiate_flip. Qed. Next Obligation. simpl. - iIntros (???? Q ? ? Φ) "(#Hinv & Hvs) HΦ". + iIntros (???? Q ???? Φ) "(#Hinv & Hfrag) HΦ". wp_pures. - wp_apply (rand_tape_spec_some _ _ _ (λ n ns, ∃ b bs, ⌜n= bool_to_nat b⌝ ∗ - ⌜ns = bool_to_nat <$> bs⌝ ∗ - Q b bs - - )%I with "[-HΦ]"); [done|..]. - - iFrame. iSplit; first done. - iMod ("Hvs") as "(%b & %bs & Hfrag & Hrest)". - iFrame. - iModIntro. - iIntros "?". - iMod ("Hrest" with "[$]"). - by iFrame. - - iIntros (n) "(%&%&%&%&%&HQ)". + wp_apply (rand_tape_spec_some with "[-HΦ]"); [done|..]. + - by iFrame. + - iIntros "Hfrag". wp_apply conversion.wp_int_to_bool as "_"; first done. - iApply "HΦ". - subst. - iFrame. - replace (Z_to_bool _) with b; first iFrame. - destruct b; simpl. + 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 Hvs". - iMod (rand_presample_spec _ _ - (λ ε num tb ε2 α ns ns', - ∃ bs bs' ε2', ⌜tb = 1%nat⌝ ∗ ⌜fmap (FMap:= list_fmap) bool_to_nat bs = ns⌝ ∗ ⌜fmap (FMap:= list_fmap) bool_to_nat bs'=fin_to_nat <$> ns'⌝ ∗ + 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 bs' + T ε num ε2' bs' )%I - with "[][-]") as "(%&%&%&%&%&%&%&%&%&%&->&<-&%&%&HT)"; [exact|exact| |iModIntro; iFrame]. - iMod "Hvs" as "(%&%&%&%&%&Herr&Hfrag&%Hpos&%Hineq&Hvs')". + with "[//][$][-]") as "(%&%&%&%&[(%&%&%K&%&?)?])"; [exact| |iModIntro; iFrame]; last first. + { by rewrite fmap_app K. } + iMod "Hvs" as "(%&%&%&Herr &%Hpos&%Hineq &Hrest)". iFrame. - iModIntro. iExists num, (λ ls, ε2 (nat_to_bool<$>(fin_to_nat <$> ls))). - repeat iSplit; try iPureIntro. + iModIntro. + repeat iSplit; try iPureIntro. - intros. apply Hpos. by rewrite !fmap_length. - etrans; last exact. @@ -203,26 +190,24 @@ Section instantiate_flip. + eapply ex_seriesC_list_length. intros. case_match; last done. by rewrite -Nat.eqb_eq. - - iIntros (ls) "(H2&H3)". - iMod ("Hvs'" with "[$H2 H3]") as "?". - + rewrite fmap_app. rewrite -!list_fmap_compose. + - 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). - + iFrame. iPureIntro; repeat split; try done. - * rewrite -!list_fmap_compose. - erewrite (Forall_fmap_ext_1 (_∘_)); first done. - apply Forall_true. - intros x; by repeat (inv_fin x; simpl; try intros x). - * intros ?? <-. - f_equal. - rewrite -!list_fmap_compose. - rewrite -{1}(list_fmap_id xs). - erewrite (Forall_fmap_ext_1 (_∘_)); first done. - apply Forall_true. - intros []; simpl. - -- by rewrite nat_to_bool_neq_0. - -- by rewrite nat_to_bool_eq_0. + + intros ?? <-. + f_equal. + rewrite -!list_fmap_compose. + rewrite -{1}(list_fmap_id xs). + erewrite (Forall_fmap_ext_1 (_∘_)); first done. + apply Forall_true. + intros []; simpl. + ** by rewrite nat_to_bool_neq_0. + ** by rewrite nat_to_bool_eq_0. Qed. End instantiate_flip. diff --git a/theories/coneris/lib/hocap_rand.v b/theories/coneris/lib/hocap_rand.v index aee65851..bf7ab59b 100644 --- a/theories/coneris/lib/hocap_rand.v +++ b/theories/coneris/lib/hocap_rand.v @@ -50,26 +50,26 @@ Class rand_spec `{!conerisGS Σ} := RandSpec 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 (Q: nat ->list nat -> iProp Σ) (α:loc) (tb:nat) : + }}}; + rand_tape_spec_some {L: randG Σ} N E γ2 (α:loc) (tb:nat) n ns: ↑N⊆E -> {{{ is_rand (L:=L) N γ2 ∗ - (|={E∖↑N, ∅}=> ∃ n ns, rand_tapes_frag (L:=L) γ2 α (tb, n::ns) ∗ - (rand_tapes_frag (L:=L) γ2 α (tb, ns) ={∅, E∖↑N}=∗ Q n ns)) + rand_tapes_frag (L:=L) γ2 α (tb, n::ns) }}} rand_tape #lbl:α #tb @ E - {{{ (n:nat), RET #n; ∃ ns, Q n ns}}}; - rand_presample_spec {L: randG Σ} N E T γ2 : + {{{ 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, ∅}=> - ∃ ε num tb (ε2 : list (fin (S tb)) -> R) α ns, - ↯ ε ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns) ∗ + ∃ ε 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', ↯ (ε2 ns') ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns ++ (fin_to_nat <$> ns')) - ={∅, E∖↑N}=∗ T ε num tb ε2 α ns ns')) -∗ - wp_update E (∃ ε num tb ε2 α ns ns', T ε num tb ε2 α ns ns') + (∀ (ns':list (fin (S tb))), ↯ (ε2 ns') ={∅, E∖↑N}=∗ T ε num ε2 ns')) -∗ + wp_update E (∃ ε num ε2 ns', T ε num ε2 ns' ∗ + rand_tapes_frag (L:=L) γ2 α (tb, ns ++ (fin_to_nat <$> ns'))) }. Section impl. @@ -145,85 +145,81 @@ Section impl. Qed. Next Obligation. simpl. - iIntros (?????????? Φ) "(#Hinv & Hvs) HΦ". + iIntros (??????????? Φ) "(#Hinv & [Hvs %]) HΦ". wp_pures. - wp_bind (rand(_) _)%E. iInv "Hinv" as ">(%&H3&H4)" "Hclose". - iMod ("Hvs") as "(%n & %ns & [Hfrag %] & Hrest)". iDestruct (hocap_tapes_agree with "[$][$]") as "%". iDestruct (big_sepM_insert_acc with "[$]") as "[Htape H3]"; first done. simpl. wp_apply (wp_rand_tape with "[$]") as "[Htape %]". iMod (hocap_tapes_update with "[$][$]") as "[? Hfrag]". - iMod ("Hrest" with "[$Hfrag]") as "HQ". - - iPureIntro. by eapply Forall_inv_tail. - - iModIntro. - iMod ("Hclose" with "[- HQ HΦ]") as "_". - { iExists (<[α:=_]> m). - iFrame. - iApply "H3". by iNext. + iMod ("Hclose" with "[- Hfrag HΦ]") as "_". + { iExists (<[α:=_]> m). + iFrame. + iApply "H3". by iNext. } - iApply "HΦ". by iFrame. + iApply "HΦ". iFrame. + iPureIntro. by eapply Forall_inv_tail. Qed. Next Obligation. simpl. - iIntros (????????) "#Hinv 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 & %num & %tb & %ε2 & %α & %ns & Herr & [Hfrag %] & %Hpos & %Hineq & Hrest)". - iDestruct (hocap_tapes_agree with "[$][$]") as "%". - iDestruct (big_sepM_insert_acc with "[$]") as "[Htape H3]"; first done. - iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%Heq)". - 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 $Hfrag]") as "HT". - { iPureIntro. - rewrite Forall_app; split; subst; first done. - eapply Forall_impl; first apply fin.fin_forall_leq. - simpl; intros; lia. - } - iFrame. - iMod ("Hclose" with "[-Hsupply]") as "_". - { iNext. iFrame. by iApply "H3". } - iApply fupd_mask_intro_subseteq; first set_solver. - iApply ec_supply_eq; last done. - simpl. rewrite Nat.eqb_refl. lra. -Qed. + 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 & %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. @@ -237,19 +233,14 @@ Section checks. {{{ RET #(LitInt n); rand_tapes_frag (L:=L) γ1 α (N, ns) ∗ ⌜n <= N⌝ }}}. Proof. iIntros (Hsubset Φ) "(#Hinv &>Hfrag) HΦ". - wp_apply (rand_tape_spec_some _ _ _ (λ n' ns', ⌜n=n'/\ns=ns'⌝ ∗ ⌜n<=N⌝ ∗ rand_tapes_frag _ _ _)%I with "[Hfrag]"); first exact. - - iSplit; first done. - iDestruct (rand_tapes_valid with "[$]") as "%H'". - iFrame. - iApply fupd_mask_intro; first set_solver. - iIntros "Hclose Hfrag". + iDestruct (rand_tapes_valid with "[$]") as "%H'". + wp_apply (rand_tape_spec_some with "[Hfrag]"); first exact. + - by iFrame. + - iIntros. + iApply "HΦ". iFrame. - iMod "Hclose". - iModIntro. iPureIntro. rewrite Forall_cons in H'. naive_solver. - - iIntros (?) "(%&[-> ->]&%&?)". iApply "HΦ". - by iFrame. Qed. Local Opaque enum_uniform_fin_list. @@ -265,17 +256,17 @@ Section checks. iIntros (Hsubset Hpos Hineq) "#Hinv >Htape Herr". iDestruct (ec_valid with "[$]") as "%Hpos'". destruct Hpos' as [Hpos' ?]. - iMod (rand_presample_spec _ _ - (λ ε' (num':nat) tb' ε2' α' ns1 ns2, - ⌜ε1=ε'⌝ ∗ ⌜(1=num')%nat⌝ ∗ ⌜N=tb'⌝ ∗ + iMod (rand_presample_spec _ _ _ _ _ _ + (λ ε' (num':nat) ε2' ns2, + ⌜ε1=ε'⌝ ∗ ⌜(1=num')%nat⌝ ∗ ⌜∀ x y, fin_to_nat <$> x = fin_to_nat <$> y -> - ε2' x = (λ l, match l with |[x] => ε2 x | _ => 1%R end) y⌝∗ ⌜α=α'⌝ ∗ ⌜ns1=ns⌝ ∗ - ∃ (n:fin (S N)), ⌜fin_to_nat <$> ns2=[fin_to_nat n]⌝ ∗ ↯ (ε2 n) ∗ rand_tapes_frag γ1 α (N, ns ++ [fin_to_nat n]))%I - with "[//][- ]") as "(%&%&%&%&%&%&%&->&<-&->&%&->&->&%&%&?&?)". + ε2' x = (λ l, match l with |[x] => ε2 x | _ => 1%R end) y⌝ ∗ + ∃ (n:fin (S N)), ⌜fin_to_nat <$> ns2=[fin_to_nat n]⌝ ∗ ↯ (ε2 n))%I + with "[//][$ ][-]") as "H". - done. - - iFrame. - iApply fupd_mask_intro; first set_solver. + - iApply fupd_mask_intro; first set_solver. iIntros "Hclose". + iFrame. iExists 1, (λ l, match l with |[x] => ε2 x | _ => 1%R end). simpl. repeat iSplit. + iPureIntro. by intros [|?[|]]. @@ -298,7 +289,7 @@ Section checks. apply Rdiv_INR_ge_0. * intros. repeat case_match; by simplify_eq. * apply ex_seriesC_finite. - + iIntros ([|?[|]]) "(?&?)"; [by iDestruct (ec_contradict with "[$]") as "%"| |by iDestruct (ec_contradict with "[$]") as "%"]. + + iIntros ([|?[|]]) "?"; [by iDestruct (ec_contradict with "[$]") as "%"| |by iDestruct (ec_contradict with "[$]") as "%"]. iFrame. iMod "Hclose". iModIntro. @@ -307,7 +298,9 @@ Section checks. intros x y H'. apply list_fmap_eq_inj in H'; first by simplify_eq. apply fin_to_nat_inj. - - iModIntro. iFrame. + - iModIntro. + iDestruct "H" as "(%&%&%&%&[(%&%&%&%&->&?) ?])". + iFrame. Qed. End checks.