add an example that shows why exposing presampling tapes is good for …

…counter module

theories/coneris/examples/random_counter/client2.v

@@ -0,0 +1,89 @@
+From clutch.prelude Require Import fin.
+From clutch.coneris Require Import coneris par spawn.
+From clutch.coneris.examples Require Import random_counter.random_counter.
+
+Set Default Proof Using "Type*".
+
+Section client.
+  Context `{rc:random_counter} {L: counterG Σ}.
+  Definition con_prog : expr :=
+    let: "c" := new_counter #() in
+    let: "lbl" := allocate_tape #() in
+    (incr_counter_tape "c" "lbl");;
+    let: "v" := read_counter "c" in
+    incr_counter_tape "c" "lbl";;
+    let: "v'" := read_counter "c" - "v" in
+    #4*"v" + "v'"
+  .
+
+  Context `{!spawnG Σ}.
+
+  Lemma con_prog_spec P E N:
+    E ## ↑N -> 
+    {{{ |={E,∅}=>
+          ∃ ε (ε2 : fin 16%nat -> R),
+              ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
+              ⌜(SeriesC (λ n, 1 / 16 * ε2 n)%R <= ε)%R ⌝ ∗
+              (∀ n, ↯ (ε2 n) ={∅, E}=∗ P ε ε2 n ) }}}
+      con_prog 
+      {{{ (n:fin 16%nat), RET #(fin_to_nat n); ∃ ε ε2, P ε ε2 n }}}.
+  Proof.
+    iIntros (Hnotin Φ) "Hvs HΦ".
+    rewrite /con_prog.
+    wp_apply (new_counter_spec (L:=L) _ N with "[//]") as (c) "(%γ & #Hcounter & Hfrag)".
+    wp_pures.
+    wp_apply (allocate_tape_spec with "[$]") as (lbl) "Htape"; first done.
+    wp_pures.
+    iAssert (state_update ⊤ ⊤ (∃ ε ε2 (n1 n2:fin 4) n,
+                   ⌜(fin_to_nat n= 4*fin_to_nat n1 + fin_to_nat n2)%nat⌝ ∗
+                   counter_tapes lbl [fin_to_nat n1; fin_to_nat n2] ∗
+                   P ε ε2 n))%I with "[Hvs Htape]" as ">(%&%&%&%&%&%Heq&Htape&HP)".
+    { iDestruct (fupd_mask_frame_r with "[$]") as "Hvs"; first done.
+      rewrite union_empty_l_L.
+      iApply state_update_mono_fupd'; last iMod "Hvs" as "(%&%&Herr&%&%Hsum&Hvs)"; first done.
+      iMod (counter_tapes_presample _ _ _ _ _ _ _ (λ x, SeriesC (λ (y:fin 4), 1/4*  ε2 (fin_force _ (4*fin_to_nat x+ fin_to_nat y))))%R with "[//][$][$]") as "(%n &Herr & Htape)".
+      - done.
+      - intros. apply SeriesC_ge_0'. intros. apply Rmult_le_pos; [lra|naive_solver].
+      - rewrite SeriesC_finite_foldr/=.
+        rewrite !SeriesC_finite_foldr/=.
+        rewrite /fin_force/=.
+        rewrite SeriesC_finite_foldr/= in Hsum. lra.
+      - iMod (counter_tapes_presample _ _ _ _ _ _ _ (λ x, ε2 (fin_force _ (4*fin_to_nat n+ fin_to_nat x )))%R with "[//][$][$]") as "(%n' &Herr & Htape)".
+        + done.
+        + by intros.
+        + done.
+        + simpl.
+          iDestruct (fupd_mask_frame_r with "[Herr Hvs]") as "Hvs"; [|iApply ("Hvs" with "Herr") |]; first apply namespaces.coPset_disjoint_empty_l.
+          rewrite union_empty_l_L.
+          iMod "Hvs". iFrame.
+          iPureIntro.
+          pose proof fin_to_nat_lt n.
+          pose proof fin_to_nat_lt n'.
+          rewrite /fin_force; case_match; try lia.
+          rewrite fin_to_nat_to_fin. lia.
+    }
+    wp_apply (incr_counter_tape_spec_some _ _ _ _ (λ _, counter_content_frag γ 1 (fin_to_nat n1)) with "[$Hcounter $Htape Hfrag]"); try done.
+    { iIntros. by iMod (counter_content_update with "[$][$]") as "[$$]". }
+    iIntros (?) "[Htape Hfrag]".
+    wp_pures.
+    wp_apply (read_counter_spec _ _ _ _ (λ n, counter_content_frag _ _ _∗ ⌜(n=fin_to_nat n1)%nat⌝)%I with "[$Hcounter Hfrag]"); first done.
+    { iIntros.
+      iDestruct (counter_content_agree with "[$][$]") as "->".
+      by iFrame.
+    }
+    iIntros (?) "[Hfrag ->]".
+    wp_pures.
+    wp_apply (incr_counter_tape_spec_some _ _ _ _ (λ _, counter_content_frag γ 1 (fin_to_nat n1 + fin_to_nat n2)) with "[$Hcounter $Htape Hfrag]"); try done.
+    { iIntros. by iMod (counter_content_update with "[$][$]") as "[$$]". }
+    iIntros (?) "[Htape Hfrag]".
+    wp_pures.
+    wp_apply (read_counter_spec _ _ _ _ (λ n, counter_content_frag _ _ _∗ ⌜(n=fin_to_nat n1+fin_to_nat n2)%nat⌝)%I with "[$Hcounter Hfrag]"); first done.
+    { iIntros.
+      iDestruct (counter_content_agree with "[$][$]") as "->".
+      by iFrame.
+    }
+    iIntros (?) "[Hfrag ->]".
+    wp_pures. replace (4*_+_)%Z with (Z.of_nat (fin_to_nat n))%Z; first (iApply "HΦ"; by iFrame).
+    rewrite Heq. lia.
+  Qed.
+End client.