diff --git a/theories/coneris/examples/random_counter3/client.v b/theories/coneris/examples/random_counter3/client.v
new file mode 100644
index 00000000..0125ecd4
--- /dev/null
+++ b/theories/coneris/examples/random_counter3/client.v
@@ -0,0 +1,215 @@
+From iris.algebra Require Import excl_auth cmra.
+From iris.base_logic.lib Require Import invariants.
+From clutch.coneris Require Import coneris par spawn.
+From clutch.coneris.examples Require Import random_counter3.random_counter.
+
+Local Open Scope Z.
+
+Set Default Proof Using "Type*".
+Section lemmas.
+  Context `{!inG Σ (excl_authR (option natO))}.
+
+  (* Helpful lemmas *)
+  Lemma ghost_var_alloc b :
+    ⊢ |==> ∃ γ, own γ (●E b) ∗ own γ (◯E b).
+  Proof.
+    iMod (own_alloc (●E b ⋅ ◯E b)) as (γ) "[??]".
+    - by apply excl_auth_valid.
+    - by eauto with iFrame.
+  Qed.
+
+  Lemma ghost_var_agree γ b c :
+    own γ (●E b) -∗ own γ (◯E c) -∗ ⌜ b = c ⌝.
+  Proof.
+    iIntros "Hγ● Hγ◯".
+    by iCombine "Hγ● Hγ◯" gives %->%excl_auth_agree_L.
+  Qed.
+
+  Lemma ghost_var_update γ b' b c :
+    own γ (●E b) -∗ own γ (◯E c) ==∗ own γ (●E b') ∗ own γ (◯E b').
+  Proof.
+    iIntros "Hγ● Hγ◯".
+    iMod (own_update_2 _ _ _ (●E b' ⋅ ◯E b') with "Hγ● Hγ◯") as "[$$]".
+    { by apply excl_auth_update. }
+    done.
+  Qed.
+End lemmas.
+
+Section client.
+  Context `{rc:random_counter} {L: counterG Σ}.
+  Definition con_prog : expr :=
+    let: "c" := new_counter #() in
+    ((incr_counter "c") |||
+    incr_counter "c" 
+    ) ;;
+    read_counter "c"
+  .
+
+  Definition one_positive n1 n2:=
+    match (n1, n2) with
+    | (Some (S _), _) | (_, Some (S _)) => true
+    | _ => false
+    end.
+
+  Definition counter_nroot:=nroot.@"counter".
+  Definition inv_nroot:=nroot.@"inv".
+  
+  Context `{!spawnG Σ, !inG Σ (excl_authR (option natO)), !inG Σ (excl_authR (boolO))}.
+
+  Definition con_prog_inv (γ1 γ2: gname): iProp Σ :=
+    ∃ (n1 n2 : option nat) ,
+      let p:= one_positive n1 n2 in
+      own γ1 (●E n1) ∗ own γ2 (●E n2) ∗
+      if p
+      then ↯ 0%R
+      else
+        ∃ (flip_num:nat),
+          ↯ (Rpower 4%R (INR flip_num-2))%R ∗
+          ⌜(flip_num = bool_to_nat (bool_decide (n1=Some 0%nat)) +bool_to_nat (bool_decide (n2=Some 0%nat)))%nat⌝.
+
+  Lemma Rpower_4_2: (Rpower 4 2 = 16)%R.
+  Proof.
+    replace 2%R with (1+1)%R by lra.
+    rewrite Rpower_plus Rpower_1; lra.
+  Qed.
+  
+  Lemma con_prog_spec:
+    {{{ ↯ (1/16) }}}
+      con_prog
+      {{{ (n:nat), RET #n; ⌜(0<n)%nat⌝ }}}.
+  Proof.
+    iIntros (Φ) "Hε HΦ".
+    rewrite /con_prog.
+    wp_apply (new_counter_spec (L:=L) _ counter_nroot with "[//]") as (c) "(%γ & #Hcounter & Hfrag)".
+    replace (1)%Qp with (1/2+1/2)%Qp; last compute_done.
+    replace 0%nat with (0+0)%nat by lia.
+    rewrite -(counter_content_frag_combine).
+    iDestruct "Hfrag" as "[Hc1 Hc2]".
+    wp_pures.
+    iMod (ghost_var_alloc None) as (γ1) "[Hauth1 Hfrag1]".
+    iMod (ghost_var_alloc None) as (γ2) "[Hauth2 Hfrag2]".
+    iMod (inv_alloc inv_nroot _ (con_prog_inv γ1 γ2) with "[Hauth1 Hauth2 Hε]") as "#Hinv".
+    { iModIntro. iFrame. iExists _. iSplit; last done.
+      simpl. replace (0-2)%R with (-2)%R by lra.
+      rewrite Rpower_Ropp Rpower_4_2.
+      iApply (ec_eq with "[$]").
+      lra.
+    }
+    wp_apply (wp_par (λ _, ∃ (n:nat), own γ1 (◯E (Some n)) ∗ counter_content_frag γ (1/2) n)%I
+                (λ _, ∃ (n:nat), own γ2 (◯E (Some n)) ∗ counter_content_frag γ (1/2) n)%I with "[Hfrag1 Hc1][Hfrag2 Hc2]").
+    - wp_apply (incr_counter_spec _ _ _ _ (λ _ _, ∃ n : nat, own γ1 (◯E (Some n)) ∗ counter_content_frag γ (1 / 2) n )%I with "[$Hcounter Hfrag1 Hc1]"); [done| |by iIntros].
+      iMod (state_update_inv_acc' with "[$]") as "[>(%n1 & %n2 & Hauth1 & Hauth2 & Herr) Hvs]"; first done.
+      iDestruct (ghost_var_agree with "[$Hauth1][$]") as "->".
+      iApply state_update_mask_intro; first set_solver.
+      iIntros "Hclose".
+      case_match eqn:H.
+      + iFrame. iExists  (λ _, 0%R).
+        repeat iSplit.
+        * done.
+        * iPureIntro; rewrite SeriesC_0; intros; lra.
+        * iIntros (n) "Herr".
+          iMod (ghost_var_update _ (Some (fin_to_nat n)) with "[$Hauth1][$]") as "[Hauth1 Hfrag1]".
+          iMod "Hclose".
+          simpl. iFrame.
+          iMod ("Hvs" with "[-Hfrag1 Hc1]"); iFrame.
+          -- case_match; first done.
+             destruct n as [|]; destruct n2 as [[]|]; simplify_eq.
+          -- iModIntro. iIntros (z) "Hauth1".
+             iMod (counter_content_update with "[$][$]") as "[$ ?]".
+             by iFrame.
+      + iDestruct "Herr" as "(%&Herr&->)/=". iFrame.
+        iExists (λ x, if 0<? fin_to_nat x then 0%R else (Rpower 4 (1+(bool_to_nat (bool_decide (n2 = Some 0%nat)) - 2))))%R. repeat iSplit; try iPureIntro.
+        * intros. case_match; first done. rewrite /Rpower. left. apply exp_pos.
+        * rewrite SeriesC_finite_foldr/=.
+          rewrite Rpower_plus Rpower_1; lra.
+        * iIntros (n) "Herr".
+          iMod (ghost_var_update _ (Some (fin_to_nat n)) with "[$Hauth1][$]") as "[Hauth1 Hfrag1]".
+          simpl. iFrame.
+          iMod "Hclose".
+          simpl. iFrame.
+          iMod ("Hvs" with "[-Hfrag1 Hc1]"); iFrame.
+          -- case_match eqn:H0.
+             ++ case_match; first done.
+                destruct (fin_to_nat n) as [|]; destruct n2 as [[|]|]; simplify_eq.
+             ++ case_match.
+                { destruct (fin_to_nat n) as [|]; destruct n2 as [[|]|]; simplify_eq. }
+                iExists _. iSplit; last done.
+                iApply (ec_eq with "[$]").
+                f_equal.
+                rewrite plus_INR. 
+                assert (fin_to_nat n = 0)%nat as ->; simpl; last lra.
+                apply Z.ltb_ge in H0. lia.
+          -- iModIntro. iIntros (z) "Hauth".
+             iMod (counter_content_update with "[$][$]") as "[$ ?]".
+             by iFrame.
+    - wp_apply (incr_counter_spec _ _ _ _ (λ _ _, ∃ n : nat, own γ2 (◯E (Some n)) ∗ counter_content_frag γ (1 / 2) n )%I with "[$Hcounter Hfrag2 Hc2]"); [done| |by iIntros].
+      iMod (state_update_inv_acc' with "[$]") as "[>(%n1 & %n2 & Hauth1 & Hauth2 & Herr) Hvs]"; first done.
+      iDestruct (ghost_var_agree with "[$Hauth2][$]") as "->".
+      iApply state_update_mask_intro; first set_solver.
+      iIntros "Hclose".
+      case_match eqn:H.
+      + iFrame. iExists (λ _, 0%R). repeat iSplit; try iPureIntro.
+        * done.
+        *  rewrite SeriesC_0; intros; lra.
+        * iIntros (n) "Herr".
+          iMod (ghost_var_update _ (Some (fin_to_nat n)) with "[$Hauth2][$]") as "[Hauth2 Hfrag2]".
+          iMod "Hclose".
+          simpl. iFrame.
+          iMod ("Hvs" with "[-Hfrag2 Hc2]"); iFrame.
+          -- case_match; first done.
+             destruct n as [|]; destruct n1 as [[]|]; simplify_eq.
+          -- iModIntro. iIntros (z) "Hauth1".
+             iMod (counter_content_update with "[$][$]") as "[$ ?]".
+             by iFrame.
+      + iDestruct "Herr" as "(%&Herr&->)/=". iFrame.
+        iExists (λ x, if 0<? fin_to_nat x then 0%R else (Rpower 4 (1+((bool_to_nat (bool_decide (n1 = Some 0)) + 0)%nat - 2))))%R. repeat iSplit; try iPureIntro.
+        * intros. case_match; first done. rewrite /Rpower. left. apply exp_pos.
+        * rewrite SeriesC_finite_foldr/=.
+          rewrite Rpower_plus Rpower_1/=; lra.
+        * iIntros (n) "Herr".
+          iMod (ghost_var_update _ (Some (fin_to_nat n)) with "[$Hauth2][$]") as "[Hauth2 Hfrag2]".
+          simpl. iFrame.
+          iMod "Hclose".
+          simpl. iFrame.
+          iMod ("Hvs" with "[-Hfrag2 Hc2]"); iFrame.
+          -- case_match eqn:H0.
+             ++ case_match; first done.
+                destruct (fin_to_nat n) as [|]; destruct n1 as [[|]|]; simplify_eq.
+             ++ case_match.
+                { destruct (fin_to_nat n) as [|]; destruct n1 as [[|]|]; simplify_eq. }
+                iExists _. iSplit; last done.
+                iApply (ec_eq with "[$]").
+                f_equal.
+                rewrite !plus_INR. 
+                assert (fin_to_nat n = 0)%nat as ->; simpl; last lra.
+                apply Z.ltb_ge in H0. lia. 
+          -- iModIntro. iIntros (z) "Hauth".
+             iMod (counter_content_update with "[$][$]") as "[$ ?]".
+             by iFrame.
+    - iIntros (??) "[(%n1 & Hfrag1 & Hc1)(%n2 & Hfrag2 & Hc2)]".
+      iNext. wp_pures.
+      iCombine "Hc1 Hc2" as "Hc".
+      rewrite counter_content_frag_combine.
+      replace (1/2+1/2)%Qp with 1%Qp; last compute_done.
+      iAssert (|={⊤}=> ⌜(n1+n2>0)%nat⌝)%I with "[Hfrag1 Hfrag2]" as ">%".
+      { iInv "Hinv" as ">(%&%&Hauth1&Hauth2&Herr)".
+        iDestruct (ghost_var_agree with "[$Hauth1][$]") as "->".
+        iDestruct (ghost_var_agree with "[$Hauth2][$]") as "->".
+        rewrite /con_prog_inv.
+        destruct n1, n2 as [|]; [simpl|simpl; iModIntro; iFrame; iSplitL "Herr"; iModIntro; try (iPureIntro; lia); done..]; last first.
+        iDestruct "Herr" as "(%&Herr&->)".
+        simpl. replace (_+_-_)%R with 0%R by lra.
+        rewrite Rpower_O; last lra.
+        by iDestruct (ec_contradict with "[$]") as "[]".
+      }
+      wp_apply (read_counter_spec _ _ _ _ (λ n, ⌜(n>0)%nat⌝)%I with "[$Hcounter Hc]"); first done.
+      { iIntros.
+        iDestruct (counter_content_agree with "[$][$]") as "<-".
+        iFrame. iModIntro. iPureIntro. lia.
+      }
+      iIntros.
+      iApply "HΦ".
+      iPureIntro; lia.
+  Qed.
+  
+End client.
diff --git a/theories/coneris/examples/random_counter3/impl1.v b/theories/coneris/examples/random_counter3/impl1.v
new file mode 100644
index 00000000..6cc9f463
--- /dev/null
+++ b/theories/coneris/examples/random_counter3/impl1.v
@@ -0,0 +1,221 @@
+From iris.algebra Require Import frac_auth.
+From iris.base_logic.lib Require Import invariants.
+From clutch.coneris Require Import coneris hocap_rand random_counter3.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_tape (rand_allocate_tape #3%nat) #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:=
+    (
+    inv (N) (counter_inv_pred1 c γ1)
+    )%I.
+
+  Lemma new_counter_spec1 E N:
+    {{{ True }}}
+      new_counter1 #() @ E
+      {{{ (c:val), RET c;
+          ∃ γ1, is_counter1 N c γ1 ∗ own γ1 (◯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 "[%γ1[H5 H6]]".
+    { by apply frac_auth_valid. }
+    replace (#0) with (#0%nat) by done.
+    iMod (inv_alloc _ _ (counter_inv_pred1 (#l) γ1) with "[$Hl $H5]") as "#Hinv'"; first done.
+    iApply "HΦ".
+    iFrame.
+    by iModIntro.
+  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 counter_tapes_presample1 N E γ1 c α ε (ε2 : fin 4%nat -> R):
+    (∀ x, 0<=ε2 x)%R ->
+    (SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ->
+    is_counter1 N c γ1 -∗
+    rand_tapes (L:=L) α (3%nat, []) -∗
+    ↯ ε  -∗
+    state_update E E (∃ n, ↯ (ε2 n) ∗ rand_tapes (L:=L) α (3%nat, [fin_to_nat n])).
+  Proof.
+    iIntros (Hpos Hineq) "#Hinv Hfrag Herr".
+    iMod (rand_tapes_presample with "[$][$]") as "(%&$&$)"; try done.
+    etrans; last exact.
+    apply Req_le.
+    apply SeriesC_ext; intros. simpl. lra.
+  Qed.
+
+
+  Lemma incr_counter_spec1 N E c γ1 (Q:nat->nat->iProp Σ)  :
+    ↑N⊆E ->
+    {{{ is_counter1 N c γ1 ∗
+        state_update E ∅
+          (∃ ε (ε2 : fin 4%nat -> R),
+              ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
+              ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
+              (∀ n, ↯ (ε2 n) -∗ state_update ∅ E
+          (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
+                      own γ1 (●F (z+n)%nat) ∗ Q z n)))
+    }}}
+      incr_counter1 c @ E
+                                 {{{ (z n:nat), RET (#z, #n); Q z n }}}.
+  Proof.
+    iIntros (Hineq Φ) "[#Hinv Hvs] HΦ".
+    rewrite /incr_counter1.
+    wp_pures.
+    wp_apply (rand_allocate_tape_spec with "[//]") as (α) "Htape".
+    iAssert (state_update E E (∃ n, rand_tapes (L:=L) α (3%nat, [fin_to_nat n]) ∗
+                                    (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q z n)
+            ))%I with "[Hvs Htape]" as ">(%n & Htape &Hvs)".
+    { iMod "Hvs" as "(%&%&?&%&%&Hvs)".
+      iMod (counter_tapes_presample1 with "[$][$][$]") as "(%&?&?)"; [done..|].
+      iMod ("Hvs" with "[$]").
+      iModIntro.
+      iFrame.
+    }
+    wp_apply (rand_tape_spec_some with "[$]") as "Htape".
+    wp_pures.
+    wp_bind (FAA _ _)%E.
+    iInv "Hinv" as ">( %l & %z & -> & H5 & H6)" "Hclose".
+    wp_faa.
+    iMod ("Hvs" with "[$]") as "[? HQ]".
+    rewrite -Nat2Z.inj_add.
+    iMod ("Hclose" with "[-HQ HΦ]"); first by iFrame.
+    iModIntro. wp_pures.
+    iApply ("HΦ" with "[$]").
+  Qed.
+  
+  
+  Lemma read_counter_spec1 N E c γ1 Q:
+    ↑N ⊆ E ->
+    {{{  is_counter1 N c γ1 ∗
+         (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
+                     own γ1 (●F z) ∗ Q z)
+        
+    }}}
+      read_counter1 c @ E
+      {{{ (n':nat), RET #n'; Q n'
+      }}}.
+  Proof.
+    iIntros (Hsubset Φ) "(#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.
+
+Program Definition random_counter1 `{!conerisGS Σ, F:rand_spec}: random_counter :=
+  {| new_counter := new_counter1;
+    incr_counter := incr_counter1;
+    read_counter:=read_counter1;
+    counterG := counterG1;
+    (* tape_name := rand_tape_name; *)
+    counter_name :=gname;
+    is_counter _ N c γ1 := is_counter1 N c γ1;
+    (* counter_tapes_auth _ γ m :=  rand_tapes_auth (L:=counterG1_randG) γ ((λ ns, (3, ns))<$>m); *)
+    (* counter_tapes _  α n := rand_tapes (L:= counterG1_randG) α (3%nat, match n with | Some x => [x] | None=> [] end); *)
+    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 (L:=counterG1_randG);
+    incr_counter_spec _ :=incr_counter_spec1 (L:=counterG1_randG);
+    read_counter_spec _ :=read_counter_spec1 (L:=counterG1_randG)
+  |}.
+(* Next Obligation. *)
+(*   simpl. *)
+(*   iIntros. *)
+(*   iDestruct (rand_tapes_exclusive with "[$][$]") as "[]". *)
+(* Qed. *)
+(* Next Obligation. *)
+(*   iIntros. *)
+(*   iDestruct (rand_tapes_valid with "[$]") as "$". *)
+(* Qed. *)
+Next Obligation.
+  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/examples/random_counter3/impl2.v b/theories/coneris/examples/random_counter3/impl2.v
new file mode 100644
index 00000000..a4d9f417
--- /dev/null
+++ b/theories/coneris/examples/random_counter3/impl2.v
@@ -0,0 +1,435 @@
+From iris.algebra Require Import frac_auth.
+From iris.base_logic.lib Require Import invariants.
+From clutch.coneris Require Import coneris random_counter3.random_counter hocap_flip.
+
+Set Default Proof Using "Type*".
+
+Local Definition expander (l:list nat):=
+  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.
+
+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.
+
+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 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. *)
+
+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.
+
+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.
+
+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.
+
+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.
+
+
+Section impl2.
+  Context `{F: flip_spec Σ}.
+  Definition new_counter2 : val:= λ: "_", ref #0.
+  Definition incr_counter2 :val := λ: "l", let: "α" := (flip_allocate_tape #()) in
+                                           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_tapes:: hocap_tapesGS' Σ; *)
+                                   counterG2_frac_authR:: inG Σ (frac_authR natR);
+                                   counterG2_flipG: flipG Σ
+                         }.
+  
+  Context `{L:!flipG Σ, !inG Σ (frac_authR natR)}.
+  
+  
+  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:=
+    ((* is_flip (L:=L) (N.@"flip") γ1 ∗ *)
+    inv (N) (counter_inv_pred2 c γ1)
+    )%I.
+
+  Lemma new_counter_spec2 E N:
+    {{{ True }}}
+      new_counter2 #() @ E
+      {{{ (c:val), RET c;
+          ∃ γ1, is_counter2 N c γ1 ∗ own γ1 (◯F 0%nat)
+      }}}.
+  Proof.
+    rewrite /new_counter2.
+    iIntros (Φ) "_ HΦ".
+    wp_pures.
+    (* iMod (flip_inv_create_spec) as "(%γ1 & #Hinv)". *)
+    wp_alloc l as "Hl".
+    iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as "[%γ1[H5 H6]]".
+    { by apply frac_auth_valid. }
+    replace (#0) with (#0%nat) by done.
+    iMod (inv_alloc _ _ (counter_inv_pred2 (#l) γ1) with "[$Hl $H5]") as "#Hinv'"; first done.
+    iApply "HΦ".
+    iFrame.
+    by iModIntro.
+  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 allocate_tape_spec2 N E c γ1: *)
+  (*   ↑N ⊆ E-> *)
+  (*   {{{ is_counter2 N c γ1 }}} *)
+  (*     allocate_tape2 #() @ E *)
+  (*     {{{ (v:val), RET v; (flip_tapes (L:=L) v (expander []) ∗ ⌜Forall (λ x, x<4) []⌝) *)
+  (*     }}}. *)
+  (* Proof. *)
+  (*   iIntros (Hsubset Φ) "#Hinv HΦ".     *)
+  (*   rewrite /allocate_tape2. *)
+  (*   wp_pures. *)
+  (*   wp_apply flip_allocate_tape_spec; first done. *)
+  (*   iIntros (?) "?". *)
+  (*   iApply "HΦ". *)
+  (*   iFrame. *)
+  (*   iPureIntro.  *)
+  (*   by apply Forall_nil. *)
+  (* Qed. *)
+
+  
+  Lemma counter_tapes_presample2 N E γ1 c α ε (ε2 : fin 4%nat -> R):
+    (∀ x, 0<=ε2 x)%R ->
+    (SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ->
+    is_counter2 N c γ1  -∗
+    (flip_tapes (L:=L) α (expander []) ∗ ⌜Forall (λ x, x<4) []⌝) -∗
+    ↯ ε  -∗
+    state_update E E (∃ n, ↯ (ε2 n) ∗
+                         (flip_tapes (L:=L) α (expander ([fin_to_nat n])) ∗ ⌜Forall (λ x, x<4) ([fin_to_nat n])⌝)).
+  Proof.
+    iIntros (Hpos Hineq) "#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)".
+    { 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)".
+      { intros []; by try lra. }
+      { simpl. lra. }
+      destruct b.
+      + iFrame. rewrite /expander  -!app_assoc/=.
+        rewrite Nat.OddT_odd; last (constructor 1 with (x:=1); lia). iFrame.
+        iPureIntro. naive_solver.
+      + iFrame. rewrite /expander -!app_assoc/=.
+        rewrite Nat.odd_2. iFrame.
+        iPureIntro. naive_solver.
+    - iMod (flip_tapes_presample _ _ _ _  (λ b, if b then ε2 1%fin else ε2 0%fin)%R with "[$][$]") as "(%b & Herr & Hfrag)".
+      { intros []; by try lra. }
+      { simpl. lra. }
+      destruct b.
+      + iFrame. rewrite /expander -!app_assoc/=.
+        rewrite Nat.OddT_odd; last (constructor 1 with (x:=0); lia). iFrame.
+        iPureIntro. naive_solver.
+      + iFrame. rewrite /expander -!app_assoc/=.
+        rewrite Nat.odd_0. iFrame.
+        iPureIntro. constructor; [lia|constructor]. 
+  Qed.
+    
+Lemma incr_counter_spec2 N E c γ1 (Q:nat->nat->iProp Σ)  :
+    ↑N⊆E ->
+    {{{ is_counter2 N c γ1 ∗
+        state_update E ∅
+          (∃ ε (ε2 : fin 4%nat -> R),
+              ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
+              ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
+              (∀ n, ↯ (ε2 n) -∗ state_update ∅ E
+          (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
+                    own γ1 (●F (z+n)%nat) ∗ Q z n)))
+    }}}
+      incr_counter2 c @ E
+      {{{ (z n:nat), RET (#z, #n); Q z n }}}.
+  Proof.
+    iIntros (Hsubset Φ) "(#Hinv & Hvs) HΦ".
+    rewrite /incr_counter2.
+    wp_pures.
+    wp_apply flip_allocate_tape_spec as (α) "Htape"; first done.
+    wp_pures.
+    iAssert (state_update E E (∃ n, (flip_tapes (L:=L) α (expander ([fin_to_nat n])) ∗ ⌜Forall (λ x, x<4) ([fin_to_nat n])⌝) ∗
+                                    (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q z n)
+            ))%I with "[Hvs Htape]" as ">(%n & (Htape&%) &Hvs)".
+    { iMod "Hvs" as "(%&%&?&%&%&Hvs)".
+      iMod (counter_tapes_presample2 with "[$][Htape][$]") as "(%&?&(?&%))"; [try done..|].
+      - simpl. iFrame. iPureIntro. by rewrite Forall_nil.
+      - iMod ("Hvs" with "[$]").
+        iModIntro.
+        by iFrame.
+    }
+    wp_apply (flip_tape_spec_some with "[$]") as "Hα".
+    wp_apply (conversion.wp_bool_to_int) as "_"; first done.
+    wp_pures.
+    wp_apply (flip_tape_spec_some with "[$]") as "Hα".
+    wp_apply (conversion.wp_bool_to_int) as "_"; first done.
+    wp_pures.
+    wp_bind (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. }
+    (* iMod "Hclose'" as "_". *)
+    iMod ("Hclose" with "[-HΦ HQ Hα]") as "_"; first by iFrame.
+    iModIntro.
+    wp_pures.
+    iApply "HΦ".
+    iFrame.
+    by iPureIntro.
+  Qed.
+
+  
+  Lemma read_counter_spec2 N E c γ1 Q:
+    ↑N ⊆ E ->
+    {{{  is_counter2 N c γ1 ∗
+         (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
+                    own γ1 (●F z) ∗ Q z)
+        
+    }}}
+      read_counter2 c @ E
+      {{{ (n':nat), RET #n'; Q n'
+      }}}.
+  Proof.
+    iIntros (Hsubset Φ) "(#Hinv & Hvs) HΦ".
+    rewrite /read_counter2.
+    wp_pure.
+    iInv "Hinv" as ">(%l&%z  & -> & Hloc & Hcont)" "Hclose".
+    wp_load.
+    (* 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 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;
+    incr_counter := incr_counter2;
+    read_counter:=read_counter2;
+    counterG := counterG2;
+    (* tape_name := flip_tape_name; *)
+    counter_name :=gname;
+    is_counter _ N c γ1 := is_counter2 N c γ1;
+    (* 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 K α n := (flip_tapes (L:=counterG2_to_flipG) α (expander (match n with |Some x => [x] |None => [] end)) ∗ ⌜Forall (λ x, x<4) (match n with |Some x => [x] |None => [] end)⌝)%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 (L:=counterG2_to_flipG);
+    incr_counter_spec _ :=incr_counter_spec2 (L:=counterG2_to_flipG);
+    read_counter_spec _ :=read_counter_spec2 (L:=counterG2_to_flipG)
+  |}.
+(* Next Obligation. *)
+(*   simpl. *)
+(*   iIntros (???????) "[H1 ?] [H2 ?]". *)
+(*   iApply (flip_tapes_auth_exclusive with "[$][$]"). *)
+(* Qed. *)
+(* Next Obligation. *)
+(*   simpl. *)
+(*   iIntros (???????) "[??] [??]". *)
+(*   iApply (flip_tapes_exclusive with "[$][$]"). *)
+(* Qed. *)
+(* Next Obligation. *)
+(*   simpl. *)
+(*   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 (??????) "[? %]". *)
+(*   iPureIntro. *)
+(*   eapply Forall_impl; first done. *)
+(*   simpl. lia. *)
+(* Qed. *)
+(* Next Obligation. *)
+(*   simpl. *)
+(*   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".
+  iCombine "H1 H2" gives "%K". by rewrite auth_auth_op_valid in K.
+Qed.
+Next Obligation.
+  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 (?????????).
+  rewrite frac_auth_frag_op. by rewrite own_op.
+Qed.
+Next Obligation.
+  simpl. iIntros (???????) "H1 H2".
+  iCombine "H1 H2" gives "%K".
+  iPureIntro.
+  by apply frac_auth_agree_L in K.
+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/examples/random_counter3/impl3.v b/theories/coneris/examples/random_counter3/impl3.v
new file mode 100644
index 00000000..c3a9ff7b
--- /dev/null
+++ b/theories/coneris/examples/random_counter3/impl3.v
@@ -0,0 +1,306 @@
+From iris.algebra Require Import frac_auth.
+From iris.base_logic.lib Require Import invariants.
+From clutch.coneris Require Import coneris hocap_rand random_counter3.random_counter.
+
+Set Default Proof Using "Type*".
+
+Section filter.
+  Definition filter_f (n:nat):= (n<4)%nat.
+  Definition filtered_list (l:list _) := filter filter_f l.
+
+  Lemma Forall_filter_f ns:
+    Forall (λ x : nat, x ≤ 3) ns -> filter filter_f ns = ns.
+  Proof.
+    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 incr_counter3 :val := λ: "l",
+                                     let: "α" :=  (rand_allocate_tape #4%nat) in
+                                     (rec: "f" "α " :=
+                                          let: "n" := rand_tape "α" #4%nat in
+                                          if: "n" < #4
+                                          then (FAA "l" "n", "n")
+                                          else "f" "α") "α".
+  Definition read_counter3 : val := λ: "l", !"l".
+  Class counterG3 Σ := CounterG3 { counterG3_randG:randG Σ;
+                                   counterG3_frac_authR:: inG Σ (frac_authR natR) }.
+
+  Definition counter_inv_pred3 (c:val) γ2:= (∃ (l:loc) (z:nat), ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ2 (●F z) )%I.
+
+  Definition is_counter3 N (c:val) γ1:=
+    (inv N (counter_inv_pred3 c γ1))%I.
+
+  Lemma new_counter_spec3 E N:
+    {{{ True }}}
+      new_counter3 #() @ E
+      {{{ (c:val), RET c;
+          ∃ γ1, is_counter3 N c γ1 ∗ own γ1 (◯F 0%nat)
+      }}}.
+  Proof.
+    rewrite /new_counter3.
+    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 "[%γ1[H5 H6]]".
+    { by apply frac_auth_valid. }
+    replace (#0) with (#0%nat) by done.
+    iMod (inv_alloc _ _ (counter_inv_pred3 (#l) γ1) with "[$Hl $H5]") as "#Hinv'"; first done.
+    iApply "HΦ".
+    iFrame.
+    by iModIntro.
+  Qed.
+
+  (* Lemma allocate_tape_spec3 N E c γ1: *)
+  (*   ↑N ⊆ E-> *)
+  (*   {{{ is_counter3 N c γ1 }}} *)
+  (*     allocate_tape3 #() @ E *)
+  (*     {{{ (v:val), RET v; (∃ ls, ⌜filter filter_f ls = []⌝ ∗ rand_tapes (L:=L) v (4, ls)) *)
+  (*     }}}. *)
+  (* Proof. *)
+  (*   iIntros (Hsubset Φ) "#Hinv HΦ". *)
+  (*   rewrite /allocate_tape3. *)
+  (*   wp_pures. *)
+  (*   wp_apply rand_allocate_tape_spec; first done. *)
+  (*   iIntros. *)
+  (*   iApply "HΦ". *)
+  (*   by iFrame. *)
+  (* Qed. *)
+
+  
+
+  Lemma counter_tapes_presample3 N E γ1 c α ε (ε2 : fin 4%nat -> R):
+    (∀ x, 0<=ε2 x)%R ->
+    (SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ->
+    is_counter3 N c γ1 -∗
+    (∃ ls, ⌜filter filter_f ls = []⌝ ∗ rand_tapes (L:=L) α (4, ls)) -∗
+    ↯ ε  -∗
+    state_update E E (∃ n, ↯ (ε2 n) ∗
+                         (∃ ls, ⌜filter filter_f ls = ([fin_to_nat n])⌝ ∗ rand_tapes (L:=L) α (4, ls))).
+  Proof.
+    iIntros (Hpos Hineq) "#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.
+    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)". 
+    { intros. case_match; first done.
+      apply Rplus_le_le_0_compat; first naive_solver.
+      apply Rmult_le_pos; lra.
+    }
+    { rewrite SeriesC_finite_foldr/=.
+      rewrite SeriesC_finite_foldr/= in Hineq.
+      lra.
+    }
+    case_match eqn :K.
+    - (* accept *)
+      iFrame.
+      iPureIntro.
+      rewrite filter_app Hfilter. 
+      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.
+      iPureIntro.
+      rewrite filter_app.
+      rewrite filter_cons_False; first by rewrite filter_nil app_nil_r.
+      rewrite /filter_f. lia.
+  Qed.
+  
+  Lemma incr_counter_spec3 N E c γ1 (Q:nat->nat->iProp Σ)  :
+    ↑N⊆E ->
+    {{{ is_counter3 N c γ1 ∗
+        state_update E ∅
+          (∃ ε (ε2 : fin 4%nat -> R),
+              ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
+              ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
+              (∀ n, ↯ (ε2 n) -∗ state_update ∅ E
+          (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
+                    own γ1 (●F (z+n)%nat) ∗ Q z n)))
+           
+    }}}
+      incr_counter3 c @ E
+      {{{ (z n:nat), RET (#z, #n); Q z n }}}.
+  Proof.
+    iIntros (Hsubset Φ) "(#Hinv & Hvs) HΦ".
+    rewrite /incr_counter3.
+    wp_pures.
+    wp_apply rand_allocate_tape_spec as (α) "Htape"; first done.
+    do 3 wp_pure.
+    iAssert (state_update E E (∃ n,
+                   (∃ ls, ⌜filter filter_f ls = ([fin_to_nat n])⌝ ∗ rand_tapes (L:=L) α (4, ls)) ∗
+                                    (∀ z : nat, own γ1 (●F z) ={E ∖ ↑N}=∗ own γ1 (●F (z + n)) ∗ Q z n)
+            ))%I with "[Hvs Htape]" as ">(%n & Htape &Hvs)".
+    { iMod "Hvs" as "(%&%&?&%&%&Hvs)".
+      iMod (counter_tapes_presample3 with "[$][$Htape][$]") as "(%&?&?)"; [try done..|].
+      iMod ("Hvs" with "[$]").
+      iModIntro.
+      iFrame.
+    }
+    iDestruct "Htape" as "(%ls & %Hfilter &Hfrag)".
+    iLöb as "IH" forall (ls Hfilter Φ) "Hfrag".
+    wp_pures.
+    destruct ls as [|hd ls]; first simplify_eq.
+    wp_apply (rand_tape_spec_some with "[$]") as "Hfrag". 
+    wp_pures.
+    case_bool_decide as K.
+    - wp_pures.
+      wp_bind (FAA _ _).
+      iInv "Hinv" as ">(%&%&-> & ?&?)" "Hclose".
+      wp_faa.
+      iMod ("Hvs" with "[$]") as "[? HQ]".
+      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 read_counter_spec3 N E c γ1 Q:
+    ↑N ⊆ E ->
+    {{{  is_counter3 N c γ1 ∗
+         (∀ (z:nat), own γ1 (●F z) ={E∖↑N}=∗
+                     own γ1 (●F z) ∗ Q z)
+        
+    }}}
+      read_counter3 c @ E
+      {{{ (n':nat), RET #n'; Q n'
+      }}}.
+  Proof.
+    iIntros (Hsubset Φ) "(#Hinv & Hvs) HΦ".
+    rewrite /read_counter3.
+    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 impl3.
+
+Program Definition random_counter3 `{F:rand_spec}: random_counter :=
+  {| new_counter := new_counter3;
+    incr_counter := incr_counter3;
+    read_counter:=read_counter3;
+    counterG := counterG3;
+    (* tape_name := rand_tape_name; *)
+    counter_name :=gname;
+    is_counter _ N c γ1 := is_counter3 N c γ1;
+    (* 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 _ α n := *)
+    (*   (∃ ls, ⌜filter filter_f ls = (match n with |Some x => [x] | None => [] end)⌝ ∗ rand_tapes (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 (L:=counterG3_randG) ;
+    incr_counter_spec _ :=incr_counter_spec3 (L:=counterG3_randG);
+    read_counter_spec _ :=read_counter_spec3 (L:=counterG3_randG) 
+  |}.
+(* Next Obligation. *)
+(*   simpl. *)
+(*   iIntros (???????) "(%&%&%&?) (%&%&%&?)". *)
+(*   iApply (rand_tapes_auth_exclusive with "[$][$]"). *)
+(* Qed. *)
+(* Next Obligation. *)
+(*   simpl. *)
+(*   iIntros (???????) "(%&%&?) (%&%&?)". *)
+(*   iApply (rand_tapes_exclusive with "[$][$]"). *)
+(* Qed. *)
+(* Next Obligation. *)
+(*   simpl. *)
+(*   iIntros (????????) "(%&%&%K&?) (%&%&?)". *)
+(*   iDestruct (rand_tapes_agree γ α with "[$][$]") as "%K'". *)
+(*   iPureIntro. *)
+(*   apply K in K'. subst. naive_solver. *)
+(* Qed. *)
+(* Next Obligation. *)
+(*   simpl. *)
+(*   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 (??????????) "(%&%&%&?) (%&%&?)". *)
+(*   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".
+  iCombine "H1 H2" gives "%K". by rewrite auth_auth_op_valid in K.
+Qed.
+Next Obligation.
+  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 (?????????).
+  rewrite frac_auth_frag_op. by rewrite own_op.
+Qed.
+Next Obligation.
+  simpl. iIntros (???????) "H1 H2".
+  iCombine "H1 H2" gives "%K".
+  iPureIntro.
+  by apply frac_auth_agree_L in K.
+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/examples/random_counter3/random_counter.v b/theories/coneris/examples/random_counter3/random_counter.v
new file mode 100644
index 00000000..0b8027df
--- /dev/null
+++ b/theories/coneris/examples/random_counter3/random_counter.v
@@ -0,0 +1,193 @@
+From clutch.coneris Require Import coneris.
+
+Set Default Proof Using "Type*".
+
+Class random_counter `{!conerisGS Σ} := RandCounter
+{
+  (** * Operations *)
+  new_counter : val;
+  (* incr_counter : val; *)
+  incr_counter : val;
+  read_counter : val;
+  (** * Ghost state *)
+  (** The assumptions about [Σ] *)
+  counterG : gFunctors → Type;
+  (** [name] is used to associate [locked] with [is_lock] *)
+  (* tape_name: Type; *)
+  counter_name: Type;
+  (** * Predicates *)
+  is_counter {L : counterG Σ} (N:namespace) (counter: val) (γ: counter_name): iProp Σ;
+  (* counter_tapes_auth {L : counterG Σ} (γ: tape_name) (m:gmap loc (list nat)): iProp Σ; *)
+  (* counter_tapes {L : counterG Σ} (α:val) (n:option 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 ::
+    Persistent (is_counter (L:=L) N c γ1);
+  (* #[global] counter_tapes_auth_timeless {L : counterG Σ} γ m :: *)
+  (*   Timeless (counter_tapes_auth (L:=L) γ m); *)
+  (* #[global] counter_tapes_timeless {L : counterG Σ} α ns :: *)
+  (*   Timeless (counter_tapes (L:=L) α ns); *)
+  #[global] counter_content_auth_timeless {L : counterG Σ} γ z ::
+    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_tapes_exclusive {L : counterG Σ} α ns ns': *)
+  (* counter_tapes (L:=L) α ns -∗ counter_tapes (L:=L) α ns' -∗ False; *)
+  (* counter_tapes_valid {L : counterG Σ} α ns: *)
+  (* counter_tapes (L:=L) α ns -∗ ⌜Forall (λ n, n<=3)%nat ns⌝; *)
+                                
+  (* counter_tapes_presample {L:counterG Σ} N E γ c α ε (ε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 γ  -∗ *)
+  (* counter_tapes (L:=L) α None -∗ *)
+  (* ↯ ε  -∗ *)
+  (* state_update E E (∃ n, ↯ (ε2 n) ∗ counter_tapes (L:=L) α (Some (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;
+  counter_content_less_than {L : counterG Σ} γ z z' f:
+  counter_content_auth (L:=L) γ z -∗ counter_content_frag (L:=L) γ f z' -∗ ⌜(z'<=z)%nat ⌝;
+  counter_content_frag_combine {L:counterG Σ} γ f f' z z':
+    (counter_content_frag (L:=L) γ f z ∗ counter_content_frag (L:=L) γ f' z')%I ≡
+    counter_content_frag (L:=L) γ (f+f')%Qp (z+z')%nat;
+  counter_content_agree {L : counterG Σ} γ z z':
+    counter_content_auth (L:=L) γ z -∗ counter_content_frag (L:=L) γ 1%Qp z' -∗ ⌜(z'=z)%nat ⌝;
+  counter_content_update {L : counterG Σ} γ f z1 z2 z3:
+    counter_content_auth (L:=L) γ z1 -∗ counter_content_frag (L:=L) γ f z2 ==∗
+    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:
+  {{{ True }}} new_counter #() @E
+    {{{ c, RET c; ∃ γ1, is_counter (L:=L) N c γ1 ∗
+                           counter_content_frag (L:=L) γ1 1%Qp 0%nat
+    }}};
+  incr_counter_spec {L: counterG Σ} N E c γ1 (Q:nat->nat->iProp Σ)  :
+    ↑N⊆E ->
+    {{{ is_counter (L:=L) N c γ1 ∗
+        state_update E ∅
+          (∃ ε (ε2 : fin 4%nat -> R),
+              ↯ ε ∗ ⌜(∀ x, 0<=ε2 x)%R⌝∗
+              ⌜(SeriesC (λ n, 1 / 4 * ε2 n)%R <= ε)%R ⌝ ∗
+              (∀ n, ↯ (ε2 n) -∗ state_update ∅ E
+          (∀ (z:nat), counter_content_auth (L:=L) γ1 z ={E∖↑N}=∗
+                      counter_content_auth (L:=L) γ1 (z+n) ∗ Q z n)))
+           
+    }}}
+      incr_counter c @ E
+                                 {{{ (z n:nat), RET (#z, #n); Q z n }}}; 
+  read_counter_spec {L: counterG Σ} N E c γ1 Q:
+    ↑N ⊆ E ->
+    {{{  is_counter (L:=L) N c γ1 ∗
+         (∀ (z:nat), counter_content_auth (L:=L) γ1 z ={E∖↑N}=∗
+                    counter_content_auth (L:=L) γ1 z∗ Q z)
+        
+    }}}
+      read_counter c @ E
+      {{{ (n':nat), RET #n'; Q n'
+      }}}
+}.
+
+
+Section lemmas.
+  Context `{rc:random_counter} {L: counterG Σ}.
+  
+(*   Lemma incr_counter_tape_spec_none N E c γ1 Q α: *)
+(*     ↑N ⊆ E-> *)
+(*     {{{ is_counter (L:=L) N c γ1 ∗ *)
+(*         counter_tapes (L:=L) α [] ∗ *)
+(*         ( |={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) γ1 z ={E∖↑N}=∗ *)
+(*                               counter_content_auth (L:=L) γ1 (z+n) ∗ Q z n ε ε2 *)
+(*                     ) *)
+(*               ) *)
+               
+(*     }}} *)
+(*       incr_counter_tape c α @ E *)
+(*                                  {{{ (z n:nat), RET (#z, #n); counter_tapes (L:=L) α [] ∗ *)
+(*                                                             ∃ ε ε2, Q z n ε ε2 }}}. *)
+(*   Proof. *)
+(*     iIntros (Hsubset Φ) "(#Hinv & Hfrag & Hvs) HΦ". *)
+(*     iApply (state_update_wp _ (∃ ε ε2 n, *)
+(*                   counter_tapes α [n] ∗ *)
+(*                   ∀ z : nat, *)
+(*                                  counter_content_auth γ1 z ={E ∖ ↑N}=∗ counter_content_auth γ1 (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. *)
+(*     } *)
+(*     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. } *)
+(*       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_spec_seq N E c γ1 ε (ε2:nat -> R) (q:Qp) (z:nat):
+    ↑N ⊆ E->
+    (∀ 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 ∗
+        ↯ ε ∗
+        counter_content_frag (L:=L) γ1 q z
+    }}}
+      incr_counter c  @ E
+                                 {{{ (z':nat) (n:nat),
+                                       RET (#z', #n); ⌜(0<=n<4)%nat⌝ ∗
+                                                      ⌜(z<=z')%nat⌝ ∗
+                                                      ↯(ε2 n) ∗
+                                                     counter_content_frag (L:=L) γ1 q (z+n)%nat }}}.
+  Proof.
+    iIntros (Hsubset Hpos Hineq Φ) "(#Hinv & Herr & Hcontent) HΦ".
+    pose (ε2' := (λ x, if (x<=?3)%nat then ε2 x else 1%R)).
+    wp_apply (incr_counter_spec _ _ _ _
+                (λ z' n , ⌜0<=n<4⌝ ∗ ⌜z<=z'⌝ ∗
+                          ↯ (ε2 n) ∗
+                                 counter_content_frag (L:=L) γ1 q (z+n)%nat
+                )%I
+               with "[-HΦ]").
+    - done.
+    - iSplit; first done.
+      iApply state_update_mask_intro; first set_solver.
+      iIntros "Hclose".
+      iFrame.
+      iExists (λ x, ε2 (fin_to_nat x)); repeat iSplit; try done.
+      + rewrite SeriesC_finite_foldr/=. iPureIntro. lra.
+      + iIntros (?) "?".
+        iMod "Hclose". iModIntro.
+        iIntros (?) "?".
+        iDestruct (counter_content_less_than with "[$][$]") as "%".
+        iMod (counter_content_update with "[$][$]") as "[??]".
+        iFrame.
+        iModIntro.
+        iPureIntro; repeat split; try done; try lia.
+        apply fin_to_nat_lt.
+    - iIntros (z' n) "(% & % & Herr & Hfrag' )".
+      iApply "HΦ".
+      iFrame.
+      by iSplit.
+  Qed.
+  
+End lemmas.
+
diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v
index c8cf913f..350d7042 100644
--- a/theories/coneris/wp_update.v
+++ b/theories/coneris/wp_update.v
@@ -288,7 +288,6 @@ Section state_update.
     iApply (state_step_coupl_mono with "[][$]").
     iIntros (??) ">(?&?&?)". by iFrame.
   Qed.
-
   
   Lemma state_update_mono E1 E2 P Q:
     (P={E2}=∗Q) -∗ state_update E1 E2 P -∗ state_update E1 E2 Q.
@@ -390,6 +389,20 @@ Section state_update.
     iIntros "[??]".
     iApply (state_update_fupd_change with "[$][$]").
   Qed.
+
+  
+  Lemma state_update_mask_intro E1 E2 P:
+    E2 ⊆ E1 -> (state_update E2 E1 emp -∗ P) -∗ state_update E1 E2 P.
+  Proof.
+    iIntros (?) "H".
+    iApply state_update_mono_fupd; first exact.
+    iApply fupd_mask_intro; first done.
+    iIntros "K".
+    iModIntro.
+    iApply "H".
+    iMod "K".
+    by iModIntro.
+  Qed.
   
   Lemma state_update_bind E1 E2 E3 P Q:
     state_update E1 E2 P ∗ (P -∗ state_update E2 E3 Q) ⊢ state_update E1 E3 Q.
@@ -571,6 +584,16 @@ Section state_update.
     iMod ("H" with "[$]") as "[??]".
     iFrame. by iMod ("Hclose" with "[$]") as "_".
   Qed.
+
+  Lemma state_update_inv_acc' E I N:
+    ↑N ⊆ E -> inv N I -∗ state_update E (E ∖↑N) (▷ I ∗ (▷ I -∗ state_update (E∖↑N) E True)).
+  Proof.
+    iIntros (Hsubset) "#Hinv".
+    iDestruct (inv_acc with "[$]") as ">(H&Hvs)"; first exact.
+    iModIntro. iFrame.
+    iIntros.
+    by iMod ("Hvs" with "[$]").
+  Qed.
   
   Context {A : cmra} `{i : inG Σ A}.
   Lemma state_update_ra_alloc E (a:A):