Skip to content

Commit

Permalink
NIT
Browse files Browse the repository at this point in the history
  • Loading branch information
@hei411
hei411 committed Sep 26, 2024
1 parent fb3f8f7 commit 9200128
Show file tree
Hide file tree
Showing 3 changed files with 101 additions and 92 deletions.
176 changes: 94 additions & 82 deletions theories/coneris/examples/random_counter/random_counter.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ Class random_counter `{!conerisGS Σ} := RandCounter
↯ ε ∗ counter_tapes_frag (L:=L) γ1 α 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', ⌜length ns' = num⌝ ∗ ↯ (ε2 ns') ∗ counter_tapes_frag (L:=L) γ1 α (ns++ns')={∅,E∖↑NS}=∗
(∀ ns', ↯ (ε2 ns') ∗ counter_tapes_frag (L:=L) γ1 α (ns++ns')={∅,E∖↑NS}=∗
T ε α ε2 num ns ns'
))-∗
wp_update E (∃ ε α ε2 num ns ns', T ε α ε2 num ns ns');
Expand All @@ -110,87 +110,99 @@ Class random_counter `{!conerisGS Σ} := RandCounter
}.


(* Section lemmas. *)
(* Context `{rc:random_counter} {L: counterG Σ}. *)
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): *)
(* ↑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 ∗ *)
(* □(∀ (ε ε': nonnegreal) (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 α [] *)
(* }}} *)
(* incr_counter_tape c #lbl:α @ E *)
(* {{{ (z:nat) (n:nat), RET (#z, #n); Q z n ∗ counter_tapes_frag (L:=L) γ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. *)
(* } *)
(* iApply (incr_counter_tape_spec_some _ _ _ _ _ _ (T n) (λ x, Q x n) with "[$Hα $HT]"); try done. *)
(* { by iSplit. } *)
(* iNext. *)
(* iIntros. iApply ("HΦ" with "[$]"). *)
(* Qed. *)
Lemma incr_counter_tape_spec_none N E c γ1 γ2 Q α:
↑N ⊆ E->
{{{ is_counter (L:=L) N c γ1 γ2 ∗
( |={E∖↑N, ∅}=>
∃ ε ε2,
↯ ε ∗ counter_tapes_frag (L:=L) γ1 α [] ∗
⌜(∀ n, 0<=ε2 n)%R⌝ ∗
⌜(((ε2 0%nat) + (ε2 1%nat)+ (ε2 2%nat)+ (ε2 3%nat))/4 <= ε)%R⌝ ∗
(∀ n, |={∅,E∖↑N}=>
∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖↑N, ∅}=∗
↯ (ε2 n) ∗ counter_tapes_frag (L:=L) γ1 α [] ={∅, E∖↑N}=∗
counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ε ε2
)
)
}}}
incr_counter_tape c #lbl:α @ E
{{{ (z n:nat), RET (#z, #n); ∃ ε ε2, Q z n ε ε2 }}}.
Proof.
iIntros (Hsubset Φ) "(#Hinv & Hvs) HΦ".
iMod (counter_presample_spec _ _
(λ ε α' ε2 num ns ns',
∃ n z,
⌜num=1%nat⌝ ∗ ⌜α'=α⌝ ∗ ⌜ns=[]⌝ ∗ ⌜ns'=[n]⌝ ∗
Q z n ε (λ x, ε2 [x])
)%I with "[//][-]") as "?"; try done.
Admitted.
(* { iMod "Hvs" as "(%ε & %ε2 & Herr &Hfrag & %Hpos & %Hineq & Hrest)". *)
(* iFrame. *)
(* intros ε Hε. specialize (Hineq ε Hε). *)
(* rewrite SeriesC_nat_bounded_fin SeriesC_finite_foldr /=. lra. *)
(* } *)
(* iApply (incr_counter_tape_spec_some _ _ _ _ _ _ (T n) (λ x, Q x n) with "[$Hα $HT]"); try done. *)
(* { by iSplit. } *)
(* iNext. *)
(* iIntros. iApply ("HΦ" with "[$]"). *)
(* 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): *)
(* ↑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 *)
(* }}} *)
(* 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 }}}. *)
(* 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]"). *)
(* - done. *)
(* - rewrite /ε2'. intros. *)
(* case_match; [naive_solver|lra]. *)
(* - rewrite /ε2'. simpl. intros. naive_solver. *)
(* - repeat iSplit; first done. *)
(* + iModIntro. *)
(* iIntros (εa εb n) "[(Herr &Hcontent) Herr_auth]". *)
(* destruct (n<=?3) eqn:H; last first. *)
(* { iLeft. iPureIntro. rewrite /ε2'. by rewrite H. } *)
(* iRight. *)
(* iFrame. *)
(* iDestruct (counter_error_ineq with "[$][$]") as "%". *)
(* iDestruct (counter_error_auth_valid with "[$]") as "%". *)
(* iDestruct (counter_error_frag_valid 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]". *)
(* iFrame. *)
(* iDestruct (counter_content_less_than with "[$][$]") as "%". *)
(* by iMod (counter_content_update with "[$][$]") as "[$ $]". *)
(* - iIntros (??) "[(%&%&?&?)?]". *)
(* iApply "HΦ". *)
(* iFrame. *)
(* rewrite /ε2'. case_match eqn: H2; first by iFrame. *)
(* apply leb_iff_conv in H2. lia. *)
(* 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): *)
(* ↑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 *)
(* }}} *)
(* 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 }}}. *)
(* 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]"). *)
(* - done. *)
(* - rewrite /ε2'. intros. *)
(* case_match; [naive_solver|lra]. *)
(* - rewrite /ε2'. simpl. intros. naive_solver. *)
(* - repeat iSplit; first done. *)
(* + iModIntro. *)
(* iIntros (εa εb n) "[(Herr &Hcontent) Herr_auth]". *)
(* destruct (n<=?3) eqn:H; last first. *)
(* { iLeft. iPureIntro. rewrite /ε2'. by rewrite H. } *)
(* iRight. *)
(* iFrame. *)
(* iDestruct (counter_error_ineq with "[$][$]") as "%". *)
(* iDestruct (counter_error_auth_valid with "[$]") as "%". *)
(* iDestruct (counter_error_frag_valid 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]". *)
(* iFrame. *)
(* iDestruct (counter_content_less_than with "[$][$]") as "%". *)
(* by iMod (counter_content_update with "[$][$]") as "[$ $]". *)
(* - iIntros (??) "[(%&%&?&?)?]". *)
(* iApply "HΦ". *)
(* iFrame. *)
(* rewrite /ε2'. case_match eqn: H2; first by iFrame. *)
(* apply leb_iff_conv in H2. lia. *)
(* Qed. *)

(* End lemmas. *)
End lemmas.
10 changes: 4 additions & 6 deletions theories/coneris/lib/hocap_flip.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ Class flip_spec `{!conerisGS Σ} := FlipSpec
∃ ε num ε2 α ns, ↯ ε ∗ flip_tapes_frag (L:=L) γ1 α ns ∗
⌜(∀ l, length l = num -> 0<=ε2 l)%R⌝ ∗
⌜(SeriesC (λ l, if length l =? num then ε2 l else 0) /(2^num) <= ε)%R⌝∗
(∀ ns', ⌜length ns' = num⌝ ∗ ↯ (ε2 ns') ∗ flip_tapes_frag (L:=L) γ1 α (ns ++ ns')
(∀ ns', ↯ (ε2 ns') ∗ flip_tapes_frag (L:=L) γ1 α (ns ++ ns')
={∅, E∖↑NS}=∗ T ε num ε2 α ns ns'))
-∗
wp_update E (∃ ε num ε2 α ns ns', T ε num ε2 α ns ns')
Expand Down Expand Up @@ -203,11 +203,9 @@ Section instantiate_flip.
+ eapply ex_seriesC_list_length. intros.
case_match; last done.
by rewrite -Nat.eqb_eq.
- iIntros (ls) "(H1&H2&H3)".
iMod ("Hvs'" with "[H1 $H2 H3]") as "?".
+ rewrite !fmap_length !fmap_app.
iSplitL "H1"; first done.
rewrite -!list_fmap_compose.
- iIntros (ls) "(H2&H3)".
iMod ("Hvs'" with "[$H2 H3]") as "?".
+ rewrite fmap_app. 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).
Expand Down
7 changes: 3 additions & 4 deletions theories/coneris/lib/hocap_rand.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ Class rand_spec `{!conerisGS Σ} := RandSpec
↯ ε ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns) ∗
⌜(∀ l, length l = num -> 0<= ε2 l)%R⌝ ∗
⌜(SeriesC (λ l, if bool_decide (l ∈ enum_uniform_fin_list tb num) then ε2 l else 0) /((S tb)^num) <= ε)%R⌝ ∗
(∀ ns', ⌜length ns' = num⌝ ∗ ↯ (ε2 ns') ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns ++ (fin_to_nat <$> ns'))
(∀ 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')
}.
Expand Down Expand Up @@ -212,7 +212,7 @@ Section impl.
{ simpl; lra. }
iMod (hocap_tapes_update with "[$][$]") as "[Hauth Hfrag]".
iMod ("Hrest" $! sample with "[$Herr $Hfrag]") as "HT".
{ iPureIntro; split; first done.
{ iPureIntro.
rewrite Forall_app; split; subst; first done.
eapply Forall_impl; first apply fin.fin_forall_leq.
simpl; intros; lia.
Expand Down Expand Up @@ -298,8 +298,7 @@ Section checks.
apply Rdiv_INR_ge_0.
* intros. repeat case_match; by simplify_eq.
* apply ex_seriesC_finite.
+
iIntros ([|?[|]]) "(%&?&?)"; try done.
+ iIntros ([|?[|]]) "(?&?)"; [by iDestruct (ec_contradict with "[$]") as "%"| |by iDestruct (ec_contradict with "[$]") as "%"].
iFrame.
iMod "Hclose".
iModIntro.
Expand Down

0 comments on commit 9200128

Please sign in to comment.