From f7b3c8964298cb01393e86be07a7648ba5577a97 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Fri, 13 Sep 2024 15:32:29 +0200
Subject: [PATCH 1/4] stronger adequacy theorem

---
 theories/base_logic/error_credits.v           | 12 +++++++++++
 theories/coneris/adequacy.v                   | 21 ++++++++++++++++++-
 .../coneris/examples/random_counter/impl3.v   |  5 +++++
 3 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 theories/coneris/examples/random_counter/impl3.v

diff --git a/theories/base_logic/error_credits.v b/theories/base_logic/error_credits.v
index 0055c586..42a2e1b3 100644
--- a/theories/base_logic/error_credits.v
+++ b/theories/base_logic/error_credits.v
@@ -367,6 +367,18 @@ Section error_credit_theory.
     CombineSepAs (↯ r1) (↯ r2) (↯ (r1 + r2)) | 0.
   Proof. rewrite /CombineSepAs ec_combine //. Qed.
 
+  (* epsilon err *)
+  Definition epsilon_err :=  (∃ x, ⌜(0<x)%R⌝ ∗ ↯ x)%I.
+
+  Lemma epsilon_err_dup : epsilon_err -∗ epsilon_err ∗ epsilon_err.
+  Proof.
+    iIntros "(%&%&H)".
+    replace (x) with (x/2+x/2)%R; last lra.
+    iDestruct (ec_split with "[$]") as "[??]"; [lra..|].
+    iFrame.
+    iPureIntro. lra.
+  Qed.      
+
 End error_credit_theory.
 
 Lemma ec_alloc `{!ecGpreS Σ} (n : nonnegreal) :
diff --git a/theories/coneris/adequacy.v b/theories/coneris/adequacy.v
index 28e97e23..6efdc3c3 100644
--- a/theories/coneris/adequacy.v
+++ b/theories/coneris/adequacy.v
@@ -330,4 +330,23 @@ Proof.
   by eapply wp_pgl.
 Qed.
 
-(* TODO limit stronger adequacy*)
+Theorem wp_pgl_lim_with_epsilon Σ `{conerisGpreS Σ} `{Countable sch_int_state} (ζ : sch_int_state)
+  (e : expr) (σ : state) (ε : R) (sch: scheduler con_prob_lang_mdp sch_int_state) φ `{!TapeOblivious sch_int_state sch}:
+  0 <= ε →
+  (∀ `{conerisGS Σ}, ⊢ epsilon_err -∗ ↯ ε -∗ WP e {{ v, ⌜φ v⌝ }}) →
+  pgl (sch_lim_exec sch (ζ, ([e], σ))) φ ε.
+Proof.
+  intros ? Hwp.
+  apply pgl_epsilon_limit; first lra.
+  intros ε' Hineq. 
+  apply pgl_closed_lim; first done.
+  intros.
+  eapply wp_pgl; [done..|lra|intros].
+  iIntros "H".
+  specialize (Hwp _).
+  replace (ε') with (ε + (ε'-ε))%R; last lra.
+  iDestruct (ec_split with "[$]") as "[H1 H2]"; [lra..|].
+  iApply (Hwp with "[-H1]H1").
+  iExists _. iFrame.
+  iPureIntro; lra.
+Qed.
diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v
new file mode 100644
index 00000000..b255f6c6
--- /dev/null
+++ b/theories/coneris/examples/random_counter/impl3.v
@@ -0,0 +1,5 @@
+From iris.algebra Require Import frac_auth.
+From iris.base_logic.lib Require Import invariants.
+From clutch.coneris Require Import coneris hocap random_counter.
+
+Set Default Proof Using "Type*".

From 2ca312a45d6bb8aec39619c9d504b639aa970753 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Fri, 13 Sep 2024 15:36:01 +0200
Subject: [PATCH 2/4] NIT

---
 theories/coneris/examples/random_counter/impl2.v | 4 ----
 theories/coneris/examples/random_counter/impl3.v | 1 +
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/theories/coneris/examples/random_counter/impl2.v b/theories/coneris/examples/random_counter/impl2.v
index e0b1283e..8d670968 100644
--- a/theories/coneris/examples/random_counter/impl2.v
+++ b/theories/coneris/examples/random_counter/impl2.v
@@ -77,10 +77,6 @@ Section tapes_lemmas.
 
 End tapes_lemmas.
 
-Section lemmas.
-  Context `{hocap_tapesGS' Σ}.
-End lemmas.
-
 Section impl2.
 
   Definition new_counter2 : val:= λ: "_", ref #0.
diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v
index b255f6c6..e50f2f51 100644
--- a/theories/coneris/examples/random_counter/impl3.v
+++ b/theories/coneris/examples/random_counter/impl3.v
@@ -3,3 +3,4 @@ From iris.base_logic.lib Require Import invariants.
 From clutch.coneris Require Import coneris hocap random_counter.
 
 Set Default Proof Using "Type*".
+

From b0c80653a0c3d65cf9a33bad690045eb7b77c683 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Fri, 13 Sep 2024 16:02:04 +0200
Subject: [PATCH 3/4] NIT

---
 .../coneris/examples/random_counter/impl1.v   | 15 +++--
 .../coneris/examples/random_counter/impl2.v   | 58 +++++++++----------
 .../coneris/examples/random_counter/impl3.v   | 21 +++++++
 .../examples/random_counter/random_counter.v  | 40 ++++++-------
 4 files changed, 80 insertions(+), 54 deletions(-)

diff --git a/theories/coneris/examples/random_counter/impl1.v b/theories/coneris/examples/random_counter/impl1.v
index 5d9b70ab..64261d43 100644
--- a/theories/coneris/examples/random_counter/impl1.v
+++ b/theories/coneris/examples/random_counter/impl1.v
@@ -251,8 +251,8 @@ Program Definition random_counter1 `{!conerisGS Σ}: random_counter :=
     is_counter _ N c γ1 γ2 γ3 := inv N (counter_inv_pred1 c γ1 γ2 γ3);
     counter_error_auth _ γ x := ●↯ x @ γ;
     counter_error_frag _ γ x := ◯↯ x @ γ;
-    counter_tapes_auth _ γ m := (●m@γ)%I;
-    counter_tapes_frag _ γ α N ns := (α◯↪N (N;ns) @ γ)%I;
+    counter_tapes_auth _ γ m := (●((λ ns, (3, ns))<$>m)@γ)%I;
+    counter_tapes_frag _ γ α ns := (α◯↪N (3%nat;ns) @ γ)%I;
     counter_content_auth _ γ z := own γ (●F z);
     counter_content_frag _ γ f z := own γ (◯F{f} z);
     new_counter_spec _ := new_counter_spec1;
@@ -297,18 +297,23 @@ Next Obligation.
 Qed.
 Next Obligation.
   simpl. 
-  iIntros (?????????) "H1 H2".
+  iIntros (???????) "H1 H2".
   iDestruct (ghost_map_elem_frac_ne with "[$][$]") as "%"; last done.
   rewrite dfrac_op_own dfrac_valid_own. by intro.
 Qed.
 Next Obligation.
   simpl.
   iIntros.
-  iApply (hocap_tapes_agree with "[$][$]").
+  iDestruct (hocap_tapes_agree with "[$][$]") as "%H".
+  iPureIntro.
+  rewrite lookup_fmap_Some in H. destruct H as (?&?&?).
+  by simplify_eq.
 Qed.
 Next Obligation.
   iIntros.
-  iApply (hocap_tapes_presample with "[$][$]").
+  iMod (hocap_tapes_presample with "[$][$]") as "[??]".
+  iModIntro. iFrame.
+  by rewrite fmap_insert. 
 Qed.
 Next Obligation.
   simpl.
diff --git a/theories/coneris/examples/random_counter/impl2.v b/theories/coneris/examples/random_counter/impl2.v
index 8d670968..86efae3d 100644
--- a/theories/coneris/examples/random_counter/impl2.v
+++ b/theories/coneris/examples/random_counter/impl2.v
@@ -9,11 +9,11 @@ Local Definition expander (l:list nat):=
   l ≫= (λ x, [Nat.div2 x; Nat.b2n (Nat.odd x)]).
 
 Class hocap_tapesGS' (Σ : gFunctors) := Hocap_tapesGS' {
-  hocap_tapesGS_inG' :: ghost_mapG Σ loc (bool* (nat*list nat))
+  hocap_tapesGS_inG' :: ghost_mapG Σ loc (bool* list nat)
                                          }.
-Definition hocap_tapesΣ' := ghost_mapΣ loc (bool*(nat*list nat)).
+Definition hocap_tapesΣ' := ghost_mapΣ loc (bool *list nat).
 
-Notation "α ◯↪N ( b ,  M ; ns ) @ γ":= (α ↪[ γ ] (b, (M,ns)))%I
+Notation "α ◯↪N ( b , ns ) @ γ":= (α ↪[ γ ] (b, ns))%I
                                     (at level 20) : bi_scope.
 
 Notation "● m @ γ" := (ghost_map_auth γ 1 m) (at level 20) : bi_scope.
@@ -22,50 +22,50 @@ Section tapes_lemmas.
   Context `{!conerisGS Σ, !hocap_tapesGS' Σ}.
 
   Lemma hocap_tapes_alloc' m:
-    ⊢ |==>∃ γ, (● m @ γ) ∗ [∗ map] k↦v ∈ m, (k ◯↪N (v.1, v.2.1; v.2.2) @ γ).
+    ⊢ |==>∃ γ, (● m @ γ) ∗ [∗ map] k↦v ∈ m, (k ◯↪N (v.1, v.2) @ γ).
   Proof.
     iMod ghost_map_alloc as (γ) "[??]".
     iFrame. iModIntro.
     iApply big_sepM_mono; last done.
-    by iIntros (?[?[??]]).
+    by iIntros (?[??]).
   Qed.
 
-  Lemma hocap_tapes_agree' m b γ k N ns:
-    (● m @ γ) -∗ (k ◯↪N (b, N; ns) @ γ) -∗ ⌜ m!!k = Some (b, (N, ns)) ⌝.
+  Lemma hocap_tapes_agree' m b γ k ns:
+    (● m @ γ) -∗ (k ◯↪N (b, ns) @ γ) -∗ ⌜ m!!k = Some (b, ns) ⌝.
   Proof.
     iIntros "H1 H2".
     by iCombine "H1 H2" gives "%".
   Qed.
 
-  Lemma hocap_tapes_new' γ m k N ns b:
-    m!!k=None -> ⊢ (● m @ γ) ==∗ (● (<[k:=(b, (N,ns))]>m) @ γ) ∗ (k ◯↪N (b, N; ns) @ γ).
+  Lemma hocap_tapes_new' γ m k ns b:
+    m!!k=None -> ⊢ (● m @ γ) ==∗ (● (<[k:=(b, ns)]>m) @ γ) ∗ (k ◯↪N (b, ns) @ γ).
   Proof.
     iIntros (Hlookup) "H".
     by iApply ghost_map_insert.
   Qed.
 
-  Lemma hocap_tapes_presample' b γ m k N ns n:
-    (● m @ γ) -∗ (k ◯↪N (b, N; ns) @ γ) ==∗ (● (<[k:=(b, (N,ns++[n]))]>m) @ γ) ∗ (k ◯↪N (b, N; ns++[n]) @ γ).
+  Lemma hocap_tapes_presample' b γ m k ns n:
+    (● m @ γ) -∗ (k ◯↪N (b, ns) @ γ) ==∗ (● (<[k:=(b, ns++[n])]>m) @ γ) ∗ (k ◯↪N (b, ns++[n]) @ γ).
   Proof.
     iIntros "H1 H2".
     iApply (ghost_map_update with "[$][$]").
   Qed.
 
-  Lemma hocap_tapes_pop1' γ m k N ns:
-    (● m @ γ) -∗ (k ◯↪N (true, N; ns) @ γ) ==∗ (● (<[k:=(false, (N,ns))]>m) @ γ) ∗ (k ◯↪N (false, N; ns) @ γ).
+  Lemma hocap_tapes_pop1' γ m k ns:
+    (● m @ γ) -∗ (k ◯↪N (true, ns) @ γ) ==∗ (● (<[k:=(false, ns)]>m) @ γ) ∗ (k ◯↪N (false, ns) @ γ).
   Proof.
     iIntros "H1 H2".
     iApply (ghost_map_update with "[$][$]").
   Qed.
   
-  Lemma hocap_tapes_pop2' γ m k N ns n:
-    (● m @ γ) -∗ (k ◯↪N (false, N; n::ns) @ γ) ==∗ (● (<[k:=(true, (N,ns))]>m) @ γ) ∗ (k ◯↪N (true, N; ns) @ γ).
+  Lemma hocap_tapes_pop2' γ m k ns n:
+    (● m @ γ) -∗ (k ◯↪N (false, n::ns) @ γ) ==∗ (● (<[k:=(true, ns)]>m) @ γ) ∗ (k ◯↪N (true, ns) @ γ).
   Proof.
     iIntros "H1 H2".
     iApply (ghost_map_update with "[$][$]").
   Qed.
 
-  Lemma hocap_tapes_notin' α N ns m (f:(bool*(nat*list nat))-> nat) g:
+  Lemma hocap_tapes_notin' α N ns m (f:(bool*list nat)-> nat) g:
     α ↪N (N; ns) -∗ ([∗ map] α0↦t ∈ m, α0 ↪N (f t; g t)) -∗ ⌜m!!α=None ⌝.
   Proof.
     destruct (m!!α) eqn:Heqn; last by iIntros.
@@ -98,9 +98,9 @@ Section impl2.
   
   
   Definition counter_inv_pred2 (c:val) γ1 γ2 γ3:=
-    (∃ (ε:R) (m:gmap loc (bool*(nat * list nat))) (l:loc) (z:nat),
+    (∃ (ε:R) (m:gmap loc (bool*list nat)) (l:loc) (z:nat),
         ↯ ε ∗ ●↯ ε @ γ1 ∗
-        ([∗ map] α ↦ t ∈ m, α ↪N ( t.2.1 `div` 2%nat ; if t.1:bool then expander t.2.2 else drop 1%nat (expander t.2.2)) )
+        ([∗ map] α ↦ t ∈ m, α ↪N ( 1%nat ; if t.1:bool then expander t.2 else drop 1%nat (expander t.2)) )
         ∗ ●m@γ2 ∗  
         ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ3 (●F z)
     )%I.
@@ -159,7 +159,7 @@ Section impl2.
     {{{ inv N (counter_inv_pred2 c γ1 γ2 γ3) }}}
       allocate_tape2 #() @ E
       {{{ (v:val), RET v;
-          ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ α ◯↪N (true, 3%nat; []) @ γ2
+          ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ α ◯↪N (true,  []) @ γ2
       }}}.
   Proof.
     iIntros (Hsubset Φ) "#Hinv HΦ".
@@ -168,7 +168,7 @@ Section impl2.
     wp_alloctape α as "Hα".
     iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose".
     iDestruct (hocap_tapes_notin' with "[$][$]") as "%".
-    iMod (hocap_tapes_new' _ _ _ 3%nat _ true with "[$]") as "[H4 H7]"; first done.
+    iMod (hocap_tapes_new' _ _ _ _ true with "[$]") as "[H4 H7]"; first done.
     replace ([]) with (expander []) by done.
     iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Hα]") as "_".
     { iNext. iSplitL; last done.
@@ -183,10 +183,10 @@ Section impl2.
     {{{ inv N (counter_inv_pred2 c γ1 γ2 γ3) ∗
         □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗
                           own γ3 (●F(z+n)%nat)∗ Q z) ∗
-        P ∗ α ◯↪N (true, 3%nat; n::ns) @ γ2
+        P ∗ α ◯↪N (true, n::ns) @ γ2
     }}}
       incr_counter_tape2 c #lbl:α @ E
-      {{{ (z:nat), RET (#z, #n); Q z ∗ α ◯↪N (true, 3%nat; ns) @ γ2}}}.
+      {{{ (z:nat), RET (#z, #n); Q z ∗ α ◯↪N (true, ns) @ γ2}}}.
   Proof.
     iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP & Hα) HΦ".
     rewrite /incr_counter_tape2.
@@ -255,8 +255,8 @@ Section impl2.
     (□∀ (ε:R) n, (P ∗ ●↯ ε@ γ1) ={E∖↑NS}=∗
         (⌜(1<=ε2 ε n)%R⌝ ∨(●↯ (ε2 ε n) @ γ1 ∗ T (n))))
         -∗
-    P -∗ α ◯↪N (true, 3%nat; ns) @ γ2 -∗
-        wp_update E (∃ n, T (n) ∗ α◯↪N (true, 3%nat; ns++[n]) @ γ2).
+    P -∗ α ◯↪N (true, ns) @ γ2 -∗
+        wp_update E (∃ n, T (n) ∗ α◯↪N (true, ns++[n]) @ γ2).
   Proof.
     iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag".
     iApply wp_update_state_step_coupl.
@@ -313,7 +313,7 @@ Section impl2.
     { edestruct (Nat.odd _); simpl; lia.  }
     rewrite -(list_fmap_singleton (fin_to_nat)) -fmap_app.
     iMod (tapeN_update_append _ _ _ _ (nat_to_fin K2) with "[$][$]") as "[Htapes Htape]".
-    iMod (hocap_tapes_presample' _ _ _ _ _ _ (f sample) with "[$][$]") as "[H4 Hfrag]".
+    iMod (hocap_tapes_presample' _ _ _ _ _ (f sample) with "[$][$]") as "[H4 Hfrag]".
     iMod "Hclose'" as "_".
     iMod ("Hvs" with "[$]") as "[%|[H2 HT]]".
     { iExFalso. iApply (ec_contradict with "[$]"). exact. }
@@ -377,8 +377,8 @@ Program Definition random_counter2 `{!conerisGS Σ}: random_counter :=
     is_counter _ N c γ1 γ2 γ3 := inv N (counter_inv_pred2 c γ1 γ2 γ3);
     counter_error_auth _ γ x := ●↯ x @ γ;
     counter_error_frag _ γ x := ◯↯ x @ γ;
-    counter_tapes_auth _ γ m := (●((λ '(n,ns), (true, (n, ns)))<$>m)@γ)%I;
-    counter_tapes_frag _ γ α N ns := (α◯↪N (true, N; ns) @ γ)%I;
+    counter_tapes_auth _ γ m := (●((λ ns, (true, ns))<$>m)@γ)%I;
+    counter_tapes_frag _ γ α ns := (α◯↪N (true, ns) @ γ)%I;
     counter_content_auth _ γ z := own γ (●F z);
     counter_content_frag _ γ f z := own γ (◯F{f} z);
     new_counter_spec _ := new_counter_spec2;
@@ -423,7 +423,7 @@ Next Obligation.
 Qed.
 Next Obligation.
   simpl.
-  iIntros (?????????) "H1 H2".
+  iIntros (???????) "H1 H2".
   iDestruct (ghost_map_elem_frac_ne with "[$][$]") as "%"; last done.
   rewrite dfrac_op_own dfrac_valid_own. by intro.
 Qed.
@@ -431,7 +431,7 @@ Next Obligation.
   simpl.
   iIntros.
   iDestruct (hocap_tapes_agree' with "[$][$]") as "%H".
-  rewrite lookup_fmap_Some in H. destruct H as ([??]&?&?).
+  rewrite lookup_fmap_Some in H. destruct H as (?&?&?).
   by simplify_eq.
 Qed.
 Next Obligation.
diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v
index e50f2f51..6c951c6a 100644
--- a/theories/coneris/examples/random_counter/impl3.v
+++ b/theories/coneris/examples/random_counter/impl3.v
@@ -4,3 +4,24 @@ From clutch.coneris Require Import coneris hocap random_counter.
 
 Set Default Proof Using "Type*".
 
+Section filter.
+  Definition filter_f (n:fin 4%nat):= bool_decide (fin_to_nat n<4)%nat.
+  Definition filtered_list (l:list _) := filter filter_f l.
+End filter.
+
+Section impl3.
+
+  Definition new_counter3 : val:= λ: "_", ref #0.
+  Definition allocate_tape3 : val := λ: "_", AllocTape #4.
+  Definition incr_counter_tape3 :val := rec: "f" "l" "α":=
+                                          let: "n" := rand("α") #4 in
+                                          if: "n" < #4
+                                          then (FAA "l" "n", "n")
+                                          else "f" "l" "α".
+  Definition read_counter3 : val := λ: "l", !"l".
+  Class counterG3 Σ := CounterG3 { counterG2_error::hocap_errorGS Σ;
+                                   counterG2_tapes:: hocap_tapesGS Σ;
+                                   counterG2_frac_authR:: inG Σ (frac_authR natR) }.
+
+  Context `{!conerisGS Σ, !hocap_errorGS Σ, !hocap_tapesGS Σ, !inG Σ (frac_authR natR)}.
+End impl3. 
diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v
index 35ca36db..b2a86280 100644
--- a/theories/coneris/examples/random_counter/random_counter.v
+++ b/theories/coneris/examples/random_counter/random_counter.v
@@ -22,8 +22,8 @@ Class random_counter `{!conerisGS Σ} := RandCounter
     (γ1: error_name) (γ2: tape_name) (γ3: counter_name): iProp Σ;
   counter_error_auth {L : counterG Σ} (γ: error_name) (x:R): iProp Σ;
   counter_error_frag {L : counterG Σ} (γ: error_name) (x:R): iProp Σ;
-  counter_tapes_auth {L : counterG Σ} (γ: tape_name) (m:gmap loc (nat*list nat)): iProp Σ;
-  counter_tapes_frag {L : counterG Σ} (γ: tape_name) (α:loc) (N:nat) (ns:list nat): iProp Σ;
+  counter_tapes_auth {L : counterG Σ} (γ: tape_name) (m:gmap loc (list nat)): iProp Σ;
+  counter_tapes_frag {L : counterG Σ} (γ: tape_name) (α:loc) (ns:list nat): iProp Σ;
   counter_content_auth {L : counterG Σ} (γ: counter_name) (z:nat): iProp Σ;
   counter_content_frag {L : counterG Σ} (γ: counter_name) (f:frac) (z:nat): iProp Σ;
   (** * General properties of the predicates *)
@@ -35,8 +35,8 @@ Class random_counter `{!conerisGS Σ} := RandCounter
     Timeless (counter_error_frag (L:=L) γ x);
   #[global] counter_tapes_auth_timeless {L : counterG Σ} γ m ::
     Timeless (counter_tapes_auth (L:=L) γ m);
-  #[global] counter_tapes_frag_timeless {L : counterG Σ} γ α N ns ::
-    Timeless (counter_tapes_frag (L:=L) γ α N ns);
+  #[global] counter_tapes_frag_timeless {L : counterG Σ} γ α ns ::
+    Timeless (counter_tapes_frag (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 ::
@@ -58,13 +58,13 @@ Class random_counter `{!conerisGS Σ} := RandCounter
 
   counter_tapes_auth_exclusive {L : counterG Σ} γ m m':
   counter_tapes_auth (L:=L) γ m -∗ counter_tapes_auth (L:=L) γ m' -∗ False;
-  counter_tapes_frag_exclusive {L : counterG Σ} γ α N N' ns ns':
-  counter_tapes_frag (L:=L) γ α N ns -∗ counter_tapes_frag (L:=L) γ α N' ns' -∗ False;
-  counter_tapes_agree {L : counterG Σ} γ α m N ns:
-    counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α N ns -∗ ⌜ m!! α = Some (N, ns) ⌝;
-  counter_tapes_update {L : counterG Σ} γ α m N ns n:
-    counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α N ns ==∗
-    counter_tapes_auth (L:=L) γ (<[α := (N, ns ++[n])]> m) ∗ counter_tapes_frag (L:=L) γ α N (ns ++ [n]);
+  counter_tapes_frag_exclusive {L : counterG Σ} γ α ns ns':
+  counter_tapes_frag (L:=L) γ α ns -∗ counter_tapes_frag (L:=L) γ α ns' -∗ False;
+  counter_tapes_agree {L : counterG Σ} γ α m ns:
+    counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝;
+  counter_tapes_update {L : counterG Σ} γ α m ns n:
+    counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns ==∗
+    counter_tapes_auth (L:=L) γ (<[α := (ns ++[n])]> m) ∗ counter_tapes_frag (L:=L) γ α (ns ++ [n]);
 
   counter_content_auth_exclusive {L : counterG Σ} γ z1 z2:
     counter_content_auth (L:=L) γ z1 -∗ counter_content_auth (L:=L) γ z2 -∗ False;
@@ -91,17 +91,17 @@ Class random_counter `{!conerisGS Σ} := RandCounter
     {{{ is_counter (L:=L) N c γ1 γ2 γ3 }}}
       allocate_tape #() @ E
       {{{ (v:val), RET v;
-          ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ counter_tapes_frag (L:=L) γ2 α 3%nat []
+          ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ counter_tapes_frag (L:=L) γ2 α []
       }}};
   incr_counter_tape_spec_some {L: counterG Σ} N E c γ1 γ2 γ3 (P: iProp Σ) (Q:nat->iProp Σ) (α:loc) (n:nat) ns:
     ↑N⊆E -> 
     {{{ is_counter (L:=L) N c γ1 γ2 γ3 ∗
         □ (∀ (z:nat), P ∗ counter_content_auth (L:=L) γ3 z ={E∖↑N}=∗
                           counter_content_auth (L:=L) γ3 (z+n)%nat ∗ Q z) ∗
-        P ∗ counter_tapes_frag (L:=L) γ2 α 3%nat (n::ns)
+        P ∗ counter_tapes_frag (L:=L) γ2 α (n::ns)
     }}}
       incr_counter_tape c #lbl:α @ E
-                                 {{{ (z:nat), RET (#z, #n); Q z ∗ counter_tapes_frag (L:=L) γ2 α 3%nat ns}}};
+                                 {{{ (z:nat), RET (#z, #n); Q z ∗ counter_tapes_frag (L:=L) γ2 α ns}}};
   counter_presample_spec {L: counterG Σ} NS E ns α
      (ε2 : R -> nat -> R)
     (P : iProp Σ) T γ1 γ2 γ3 c:
@@ -112,8 +112,8 @@ Class random_counter `{!conerisGS Σ} := RandCounter
     (□∀ (ε:R) n, (P ∗ counter_error_auth (L:=L) γ1 ε) ={E∖↑NS}=∗
         (⌜(1<=ε2 ε n)%R⌝ ∨ (counter_error_auth (L:=L) γ1 (ε2 ε n)  ∗ T (n)))) 
         -∗
-    P -∗ counter_tapes_frag (L:=L) γ2 α 3%nat ns-∗
-        wp_update E (∃ n, T (n) ∗ counter_tapes_frag (L:=L) γ2 α 3%nat (ns++[n]));
+    P -∗ counter_tapes_frag (L:=L) γ2 α ns-∗
+        wp_update E (∃ n, T (n) ∗ counter_tapes_frag (L:=L) γ2 α (ns++[n]));
   read_counter_spec {L: counterG Σ} N E c γ1 γ2 γ3 P Q:
     ↑N ⊆ E ->
     {{{  is_counter (L:=L) N c γ1 γ2 γ3  ∗
@@ -139,10 +139,10 @@ Section lemmas.
                            ={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 α 3%nat []
+        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 α 3%nat [] }}}.
+                                 {{{ (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.
@@ -161,7 +161,7 @@ Section lemmas.
     (∀ (ε: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 α 3%nat [] ∗
+        counter_tapes_frag (L:=L) γ2 α [] ∗
         counter_content_frag (L:=L) γ3 q z 
     }}}
       incr_counter_tape c #lbl:α @ E
@@ -169,7 +169,7 @@ Section lemmas.
                                        RET (#z', #n); ⌜(0<=n<4)%nat⌝ ∗
                                                       ⌜(z<=z')%nat⌝ ∗
                                                      counter_error_frag (L:=L) γ1 (ε2 ε n) ∗
-                                                     counter_tapes_frag (L:=L) γ2 α 3%nat [] ∗
+                                                     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Φ".

From ba371e5baf1c98397ff0b79daade701f9ef047e7 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Mon, 16 Sep 2024 10:34:42 +0200
Subject: [PATCH 4/4] generate error credit from thin air + drop value
 restriction in wp_update

---
 theories/base_logic/error_credits.v           | 12 -----
 theories/coneris/adequacy.v                   | 54 ++++++++++---------
 theories/coneris/ectx_lifting.v               |  3 +-
 theories/coneris/error_rules.v                | 31 +++++------
 theories/coneris/examples/parallel_add.v      |  4 +-
 .../coneris/examples/random_counter/impl3.v   |  1 +
 theories/coneris/lib/flip.v                   | 10 ++--
 theories/coneris/lifting.v                    |  9 ++--
 theories/coneris/weakestpre.v                 | 42 ++++++++++++---
 theories/coneris/wp_update.v                  | 40 ++++++++++----
 10 files changed, 122 insertions(+), 84 deletions(-)

diff --git a/theories/base_logic/error_credits.v b/theories/base_logic/error_credits.v
index 42a2e1b3..0055c586 100644
--- a/theories/base_logic/error_credits.v
+++ b/theories/base_logic/error_credits.v
@@ -367,18 +367,6 @@ Section error_credit_theory.
     CombineSepAs (↯ r1) (↯ r2) (↯ (r1 + r2)) | 0.
   Proof. rewrite /CombineSepAs ec_combine //. Qed.
 
-  (* epsilon err *)
-  Definition epsilon_err :=  (∃ x, ⌜(0<x)%R⌝ ∗ ↯ x)%I.
-
-  Lemma epsilon_err_dup : epsilon_err -∗ epsilon_err ∗ epsilon_err.
-  Proof.
-    iIntros "(%&%&H)".
-    replace (x) with (x/2+x/2)%R; last lra.
-    iDestruct (ec_split with "[$]") as "[??]"; [lra..|].
-    iFrame.
-    iPureIntro. lra.
-  Qed.      
-
 End error_credit_theory.
 
 Lemma ec_alloc `{!ecGpreS Σ} (n : nonnegreal) :
diff --git a/theories/coneris/adequacy.v b/theories/coneris/adequacy.v
index 6efdc3c3..805b234e 100644
--- a/theories/coneris/adequacy.v
+++ b/theories/coneris/adequacy.v
@@ -63,13 +63,22 @@ Section adequacy.
     iRevert (σ ε) "H".
     iApply state_step_coupl_ind.
     iModIntro.
-    iIntros (??) "[%|[>(_&_&%)|(%R&%μ&%&%&%Herasable&%&%Hineq&%Hpgl&H)]]".
+    iIntros (??) "[%|[>(_&_&%)|[H|(%R&%μ&%&%&%Herasable&%&%Hineq&%Hpgl&H)]]]".
     - iPureIntro. by apply pgl_1.
     - iApply fupd_mask_intro; first done.
       iIntros "_".
       iPureIntro.
       erewrite sch_exec_is_final; last done.
       eapply pgl_mon_grading; last apply pgl_dret; auto.
+    - iApply (fupd_mono _ _ (⌜_⌝)%I).
+      { iPureIntro.
+        intros H'.
+        apply pgl_epsilon_limit; last exact.
+        by apply Rle_ge. 
+      }
+      iIntros (ε' ?).
+      unshelve iDestruct ("H" $! (mknonnegreal ε' _) with "[]") as "[H _]"; [|done..].
+      pose proof cond_nonneg ε. lra.
     - erewrite <-Herasable; last done.
       iApply (fupd_mono _ _ (⌜_⌝)%I).
       { iPureIntro.
@@ -91,11 +100,20 @@ Section adequacy.
   Proof.
     iRevert (σ ε).
     iApply state_step_coupl_ind.
-    iIntros "!>" (σ ε) "[%|[?|(%&%μ&%&%&%Herasable&%&%&%&H)]] Hcont".
+    iIntros "!>" (σ ε) "[%|[?|[H|(%&%μ&%&%&%Herasable&%&%&%&H)]]] Hcont".
     - iApply step_fupdN_intro; first done.
       iPureIntro.
       by apply pgl_1.
     - by iMod ("Hcont" with "[$]").
+    - iApply (step_fupdN_mono _ _ _ (⌜(∀ ε', _)⌝)).
+      { iPureIntro.
+        intros.
+        apply pgl_epsilon_limit; [simpl; by apply Rle_ge|done].
+      }
+      iIntros (ε' ?).
+      unshelve iDestruct ("H" $! (mknonnegreal ε' _) with "[]") as "[H _]";
+        [pose proof cond_nonneg ε; simpl in *; lra|done|simpl].
+      iApply ("H" with "[$]").
     - rewrite -Herasable.
       iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
       { iPureIntro.
@@ -121,11 +139,20 @@ Section adequacy.
     intros ???.
     iRevert (σ ε).
     iApply state_step_coupl_ind.
-    iIntros "!>" (σ ε) "[%|[?|(%&%μ&%&%&%&%&%&%&H)]] Hcont".
+    iIntros "!>" (σ ε) "[%|[?|[H|(%&%μ&%&%&%&%&%&%&H)]]] Hcont".
     - iApply step_fupdN_intro; first done.
       iPureIntro.
       by apply pgl_1.
     - by iMod ("Hcont" with "[$]").
+    - iApply (step_fupdN_mono _ _ _ (⌜(∀ ε', _)⌝)).
+      { iPureIntro.
+        intros.
+        apply pgl_epsilon_limit; [simpl; by apply Rle_ge|done].
+      }
+      iIntros (ε' ?).
+      unshelve iDestruct ("H" $! (mknonnegreal ε' _) with "[]") as "[H _]";
+        [pose proof cond_nonneg ε; simpl in *; lra|done|simpl].
+      iApply ("H" with "[$]").
     - unshelve erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim_sch_erasable _ _ _ _ _ _ _ μ _ _ _ _)); [done..|].
       iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
       { iPureIntro.
@@ -329,24 +356,3 @@ Proof.
   intros.
   by eapply wp_pgl.
 Qed.
-
-Theorem wp_pgl_lim_with_epsilon Σ `{conerisGpreS Σ} `{Countable sch_int_state} (ζ : sch_int_state)
-  (e : expr) (σ : state) (ε : R) (sch: scheduler con_prob_lang_mdp sch_int_state) φ `{!TapeOblivious sch_int_state sch}:
-  0 <= ε →
-  (∀ `{conerisGS Σ}, ⊢ epsilon_err -∗ ↯ ε -∗ WP e {{ v, ⌜φ v⌝ }}) →
-  pgl (sch_lim_exec sch (ζ, ([e], σ))) φ ε.
-Proof.
-  intros ? Hwp.
-  apply pgl_epsilon_limit; first lra.
-  intros ε' Hineq. 
-  apply pgl_closed_lim; first done.
-  intros.
-  eapply wp_pgl; [done..|lra|intros].
-  iIntros "H".
-  specialize (Hwp _).
-  replace (ε') with (ε + (ε'-ε))%R; last lra.
-  iDestruct (ec_split with "[$]") as "[H1 H2]"; [lra..|].
-  iApply (Hwp with "[-H1]H1").
-  iExists _. iFrame.
-  iPureIntro; lra.
-Qed.
diff --git a/theories/coneris/ectx_lifting.v b/theories/coneris/ectx_lifting.v
index de449b65..02840b53 100644
--- a/theories/coneris/ectx_lifting.v
+++ b/theories/coneris/ectx_lifting.v
@@ -17,7 +17,6 @@ Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
 Local Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd {E Φ} e1 s :
-  to_val e1 = None →
   (∀ σ1 ε1,
     state_interp σ1 ∗ err_interp ε1
     ={E,∅}=∗
@@ -38,7 +37,7 @@ Lemma wp_lift_head_step_fupd {E Φ} e1 s :
   )
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd_glm; [done|].
+  iIntros "H". iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "Hσε".
   iMod ("H" with "Hσε") as "[% H]"; iModIntro; auto.
 Qed.
diff --git a/theories/coneris/error_rules.v b/theories/coneris/error_rules.v
index fd7ab48a..defd65e9 100644
--- a/theories/coneris/error_rules.v
+++ b/theories/coneris/error_rules.v
@@ -162,7 +162,7 @@ Lemma wp_rand_err (N : nat) (z : Z) (m : fin (S N)) E Φ s :
   ⊢ WP rand #z @ s; E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -214,7 +214,7 @@ Lemma wp_rand_err_nat (N : nat) (z : Z) (m : nat) E Φ s :
   ⊢ WP rand #z @ s; E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -262,7 +262,7 @@ Lemma wp_rand_err_list_nat (N : nat) (z : Z) (ns : list nat) E Φ :
   ⊢ WP rand #z @ E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -308,7 +308,7 @@ Lemma wp_rand_err_list_int (N : nat) (z : Z) (zs : list Z) E Φ :
   ⊢ WP rand #z @ E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -407,7 +407,7 @@ Lemma wp_couple_rand_adv_comp (N : nat) z E (ε1 : R) (ε2 : fin (S N) -> R) :
   {{{ ↯ ε1 }}} rand #z @ E {{{ n, RET #n; ↯ (ε2 n) }}}.
 Proof.
   iIntros (-> Hineq (r & Hε2) Hε1 Ψ) "Herr HΨ".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε_now) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -1020,13 +1020,12 @@ Proof.
 Qed. 
 
 Lemma wp_presample (N : nat) E e 𝛼 Φ ns :
-  to_val e = None →
   ▷ 𝛼 ↪N (N;ns) ∗
   (∀ n, 𝛼 ↪N (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (He) "(>H𝛼&Hwp)".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iIntros "(>H𝛼&Hwp)".
+  iApply wp_lift_step_fupd_glm.
   iIntros (𝜎 ε) "((Hheap&Htapes)&Hε)".
   iDestruct "H𝛼" as (ns') "(%Hmap & H𝛼)".
   iDestruct (ghost_map_lookup with "Htapes H𝛼") as %Hlookup.
@@ -1045,7 +1044,7 @@ Proof.
   iMod "Hclose'" as "_".
   iSpecialize ("Hwp" $! (fin_to_nat n) with "[H𝛼]").
   { iExists _. iFrame. iPureIntro. rewrite fmap_app; by f_equal. }
-  rewrite !pgl_wp_unfold /pgl_wp_pre /= He.
+  rewrite !pgl_wp_unfold /pgl_wp_pre /=.
   iSpecialize ("Hwp" $! (state_upd_tapes <[𝛼:=(N; ns' ++ [n]):tape]> 𝜎) ε).
   iMod ("Hwp" with "[Hheap Htapes Hε]") as "Hwp".
   { replace (nnreal_zero + ε)%NNR with ε by (apply nnreal_ext; simpl; lra).
@@ -1059,7 +1058,6 @@ Qed.
 
 
 Lemma wp_presample_adv_comp (N : nat) E e α Φ ns (ε1 : R) (ε2 : fin (S N) -> R) :
-  to_val e = None →
   (∀ n, 0<=ε2 n)%R ->
   (SeriesC (λ n, (1 / (S N)) * ε2 n)%R <= ε1)%R →
   ▷α ↪N (N; ns) ∗
@@ -1067,8 +1065,8 @@ Lemma wp_presample_adv_comp (N : nat) E e α Φ ns (ε1 : R) (ε2 : fin (S N) ->
   (∀ n, ↯ (ε2 n) ∗ α ↪N (N; ns ++ [fin_to_nat n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (Hσ_red Hpos Hsum) "(>Hα & Hε & Hwp)".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iIntros (Hpos Hsum) "(>Hα & Hε & Hwp)".
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
   iDestruct "Hα" as (ns') "(%Hmap & Hα)".
   iDestruct (ghost_map_lookup with "Htapes Hα") as "%Hlookup".
@@ -1093,7 +1091,7 @@ Proof.
   rewrite pgl_wp_unfold /pgl_wp_pre.
   simpl.
   remember {| heap := heap (σ1); tapes := (<[α:=(N; ns' ++ [sample])]> (tapes σ1)) |} as σ2.
-  rewrite /= Hσ_red /=.
+  rewrite /=.
   iSpecialize ("Hwp" with "[Hε Hα]"); first iFrame.
   { iPureIntro. rewrite fmap_app; by f_equal. }
   iSpecialize ("Hwp" $! σ2 _).
@@ -1110,9 +1108,8 @@ Qed.
     α ↪N (N; ns) -∗ wp_update E (∃ n, α ↪N (N; ns ++ [n])).
   Proof.
     rewrite wp_update_unseal.
-    iIntros "Hα" (e Φ Hv) "Hwp".
+    iIntros "Hα" (e Φ) "Hwp".
     iApply wp_presample.
-    { rewrite Hv //. }
     iFrame. iIntros (n) "Hα".
     iApply ("Hwp" with "[$Hα]").
   Qed.
@@ -1123,8 +1120,8 @@ Qed.
     α ↪N (N; ns) ∗ ↯ ε1 -∗ wp_update E (∃ n, α ↪N (N; ns ++ [fin_to_nat n]) ∗ ↯ (ε2 n)).
   Proof.
     rewrite wp_update_unseal.
-    iIntros (? ?) "[Hα Hε1]". iIntros (e Φ Hv) "Hwp".
-    iApply (wp_presample_adv_comp _ _ _ _ _ _ _ ε2); [rewrite Hv//|done|done|..].
+    iIntros (? ?) "[Hα Hε1]". iIntros (e Φ) "Hwp".
+    iApply (wp_presample_adv_comp _ _ _ _ _ _ _ ε2); [done|done|..].
     iFrame. iIntros (n) "[Hα Hε2]".
     iApply ("Hwp" with "[$Hα $Hε2]").
   Qed.
diff --git a/theories/coneris/examples/parallel_add.v b/theories/coneris/examples/parallel_add.v
index 91fe184a..fd2aa1cd 100644
--- a/theories/coneris/examples/parallel_add.v
+++ b/theories/coneris/examples/parallel_add.v
@@ -817,12 +817,12 @@ Section attempt3.
     { iFrame. }
     iDestruct "Hfrag_loc" as "[Hfrac_a Hfrac_b]".
     (** presample *)
-    wp_apply (wp_presample_bool_adv_comp _ _ _ _ _ _ (λ b, if b then nnreal_half else nnreal_one)); [done|..]; last iFrame "Hα Herr".
+    wp_apply (wp_presample_bool_adv_comp _ _ _ _ _ _ (λ b, if b then nnreal_half else nnreal_one)); last iFrame "Hα Herr".
     { intros; case_match; simpl; lra. }
     { simpl; lra. }
     iIntros ([|]) "[Herr Hα]"; last first.
     { iExFalso. by iApply ec_contradict. }
-    wp_apply (wp_presample_bool_adv_comp _ _ _ _ _ _ (λ b, if b then nnreal_zero else nnreal_one)); [done|..]; last iFrame "Hα' Herr".
+    wp_apply (wp_presample_bool_adv_comp _ _ _ _ _ _ (λ b, if b then nnreal_zero else nnreal_one)); last iFrame "Hα' Herr".
     { intros; case_match; simpl; lra. }
     { simpl; lra. }
     iIntros ([|]) "[? Hα']"; last first.
diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v
index 6c951c6a..e6c7c8ad 100644
--- a/theories/coneris/examples/random_counter/impl3.v
+++ b/theories/coneris/examples/random_counter/impl3.v
@@ -24,4 +24,5 @@ Section impl3.
                                    counterG2_frac_authR:: inG Σ (frac_authR natR) }.
 
   Context `{!conerisGS Σ, !hocap_errorGS Σ, !hocap_tapesGS Σ, !inG Σ (frac_authR natR)}.
+  
 End impl3. 
diff --git a/theories/coneris/lib/flip.v b/theories/coneris/lib/flip.v
index 65b07319..e53d6efe 100644
--- a/theories/coneris/lib/flip.v
+++ b/theories/coneris/lib/flip.v
@@ -186,7 +186,6 @@ Section specs.
   Qed.
 
   Lemma wp_presample_bool_adv_comp E e α Φ bs (ε1 : R) (ε2 : bool -> R) :
-    to_val e = None →
     (∀ b, (0<=ε2 b)%R) -> 
     (((ε2 true) + (ε2 false))/2 <= ε1)%R →
     ▷α ↪B bs ∗
@@ -194,9 +193,9 @@ Section specs.
     (∀ b, ↯ (ε2 b) ∗ α ↪B (bs ++ [b]) -∗ WP e @ E {{ Φ }})
     ⊢ WP e @ E {{ Φ }}.
   Proof.
-    iIntros (Hval ? Hineq) "(>Hα & Herr & HΦ)".
+    iIntros (? Hineq) "(>Hα & Herr & HΦ)".
     rewrite tape_conversion_bool_nat.
-    wp_apply (wp_presample_adv_comp 1%nat _ _ _ _ _ _ (λ x, ε2 (fin_to_nat x =? 1%nat)));  [done| | |iFrame].
+    wp_apply (wp_presample_adv_comp 1%nat _ _ _ _ _ _ (λ x, ε2 (fin_to_nat x =? 1%nat)));  [ | |iFrame].
     - intros; done. 
     - rewrite SeriesC_finite_foldr; simpl. etrans; last exact. lra.
     - iIntros (n) "[Herr Hα]".
@@ -208,14 +207,13 @@ Section specs.
   Qed.
 
   Lemma wp_presample_bool E e α Φ bs :
-    to_val e = None →
     ▷α ↪B bs ∗
     (∀ b, α ↪B (bs ++ [b]) -∗ WP e @ E {{ Φ }})
     ⊢ WP e @ E {{ Φ }}.
   Proof.
-    iIntros (Hval) "(>Hα & HΦ)".
+    iIntros "(>Hα & HΦ)".
     rewrite tape_conversion_bool_nat.
-    wp_apply (wp_presample 1%nat); [done|iFrame].
+    wp_apply (wp_presample 1%nat); iFrame.
     iIntros (n) "Hα".
     iApply ("HΦ" $! (n=? 1%nat)).
     iFrame.
diff --git a/theories/coneris/lifting.v b/theories/coneris/lifting.v
index 1dc01f17..4a69eb54 100644
--- a/theories/coneris/lifting.v
+++ b/theories/coneris/lifting.v
@@ -16,7 +16,6 @@ Section lifting.
   #[local] Open Scope R.
 
   Lemma wp_lift_step_fupd_glm E Φ e1 s :
-    to_val e1 = None →
     (∀ σ1 ε1,
      state_interp σ1 ∗ err_interp ε1 ={E, ∅}=∗
      state_step_coupl σ1 ε1
@@ -34,13 +33,13 @@ Section lifting.
        ))
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    by rewrite pgl_wp_unfold /pgl_wp_pre =>->.
+    by rewrite pgl_wp_unfold /pgl_wp_pre. 
   Qed.
 
 
 
   Lemma wp_lift_step_fupd E Φ e1 s :
-    to_val e1 = None →
+    to_val e1 = None ->
     (∀ σ1, state_interp σ1
            ={E,∅}=∗
            ⌜reducible e1 σ1⌝ ∗
@@ -49,8 +48,8 @@ Section lifting.
        state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s ; ⊤ {{ fork_post }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    iIntros (?) "H".
-    iApply wp_lift_step_fupd_glm; [done|].
+    iIntros (H) "H".
+    iApply wp_lift_step_fupd_glm.
     iIntros (σ1 ε) "[Hσ Hε]".
     iMod ("H" with "Hσ") as "[%Hs H]". iModIntro.
     iApply state_step_coupl_ret.
diff --git a/theories/coneris/weakestpre.v b/theories/coneris/weakestpre.v
index 9fe1bd7f..5e3cc2ac 100644
--- a/theories/coneris/weakestpre.v
+++ b/theories/coneris/weakestpre.v
@@ -39,6 +39,7 @@ Section modalities.
       let '(σ1, ε) := x in
       ⌜(1<=ε)%R⌝ ∨
         Z σ1 ε ∨
+        (∀ (ε':nonnegreal), ⌜(ε<ε')%R⌝ -∗ Φ (σ1, ε')) ∨
       (∃ R μ (ε1 : nonnegreal) (ε2 : state con_prob_lang -> nonnegreal),
           ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
@@ -58,10 +59,14 @@ Section modalities.
   Proof.
     split; [|apply _].
     iIntros (Φ Ψ HNEΦ HNEΨ) "#Hwand".
-    iIntros ([??]) "[H|[?|(%&%&%&%&%&%&%&%&H)]]".
+    iIntros ([??]) "[H|[?|[H|(%&%&%&%&%&%&%&%&H)]]]".
     - by iLeft.
     - iRight; by iLeft.
-    - do 2 iRight.
+    - iRight; iRight; iLeft.
+      iIntros (??).
+      iApply "Hwand".
+      by iApply "H".
+    - do 3 iRight.
       repeat iExists _; repeat (iSplit; [done|]).
       iIntros (??).
       iApply "Hwand".
@@ -74,7 +79,8 @@ Section modalities.
   Lemma state_step_coupl_unfold σ1 ε Z :
     state_step_coupl σ1 ε Z ≡
       (⌜(1 <= ε)%R⌝ ∨
-      (Z σ1 ε) ∨
+         (Z σ1 ε) ∨
+         (∀ ε', ⌜(ε<ε')%R⌝ -∗ state_step_coupl σ1 ε' Z) ∨
       (∃ R μ (ε1 : nonnegreal) (ε2 : state con_prob_lang -> nonnegreal),
           ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
@@ -91,6 +97,23 @@ Section modalities.
     Z σ1 ε -∗ state_step_coupl σ1 ε Z.
   Proof. iIntros. rewrite state_step_coupl_unfold. by iRight; iLeft. Qed.
 
+  Lemma state_step_coupl_ampl σ1 Z ε:
+    (∀ ε', ⌜(ε<ε')%R⌝ -∗ state_step_coupl σ1 ε' Z) -∗ state_step_coupl σ1 ε Z.
+  Proof. iIntros. rewrite state_step_coupl_unfold.
+         do 2 iRight; by iLeft.
+  Qed. 
+
+  Lemma state_step_coupl_ampl' σ1 Z ε:
+    (∀ ε', ⌜(ε<ε'<1)%R⌝ -∗ state_step_coupl σ1 ε' Z) -∗ state_step_coupl σ1 ε Z.
+  Proof.
+    iIntros "H".
+    iApply state_step_coupl_ampl.
+    iIntros (ε' ?).
+    destruct (Rlt_or_le ε' 1)%R.
+    - iApply "H". iPureIntro. lra.
+    - by iApply state_step_coupl_ret_err_ge_1. 
+  Qed. 
+
   Lemma state_step_coupl_rec σ1 (ε : nonnegreal) Z :
     (∃ R μ (ε1 : nonnegreal) (ε2 : state con_prob_lang -> nonnegreal),
           ⌜ sch_erasable (λ t _ _ sch, TapeOblivious t sch) μ σ1 ⌝ ∗
@@ -99,7 +122,7 @@ Section modalities.
           ⌜pgl μ R ε1⌝ ∗
           ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ state_step_coupl σ2 (ε2 σ2) Z)%I
     ⊢ state_step_coupl σ1 ε Z.
-  Proof. iIntros "H". rewrite state_step_coupl_unfold. iRight; iRight. done. Qed.
+  Proof. iIntros "H". rewrite state_step_coupl_unfold. repeat iRight. done. Qed.
 
   Lemma state_step_coupl_ind (Ψ Z : state con_prob_lang → nonnegreal → iProp Σ) :
     ⊢ (□ (∀ σ ε,
@@ -143,9 +166,12 @@ Section modalities.
     iRevert (σ1 ε) "Hs".
     iApply state_step_coupl_ind.
     iIntros "!#" (σ ε)
-      "[% | [? | (% & % & % & % & % & % & % & % & H)]] Hw".
+      "[% | [? | [H|(% & % & % & % & % & % & % & % & H)]]] Hw".
     - iApply state_step_coupl_ret_err_ge_1. lra.
     - iApply state_step_coupl_ret. by iApply "Hw".
+    - iApply state_step_coupl_ampl.
+      iIntros (??).
+      by iApply "H".
     - iApply state_step_coupl_rec.
       repeat iExists _.
       repeat iSplit; try done.
@@ -179,9 +205,13 @@ Section modalities.
     iRevert (σ1 ε) "Hs".
     iApply state_step_coupl_ind.
     iIntros "!#" (σ ε)
-      "[% | [H | (% & % & % & % & % & % & % & % & H)]] HZ".
+      "[% | [H | [H|(% & % & % & % & % & % & % & % & H)]]] HZ".
     - by iApply state_step_coupl_ret_err_ge_1.
     - iApply ("HZ" with "H").
+    - iApply state_step_coupl_ampl.
+      iIntros (??).
+      iDestruct ("H" with "[//]") as "[H _]".
+      by iApply "H".
     - iApply state_step_coupl_rec.
       repeat iExists _.
       repeat iSplit; try done.
diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v
index 1644ffe6..c183bffa 100644
--- a/theories/coneris/wp_update.v
+++ b/theories/coneris/wp_update.v
@@ -12,27 +12,26 @@ Section wp_update.
   Context `{!conerisGS Σ}.
 
   Definition wp_update_def (E : coPset) (P : iProp Σ) : iProp Σ :=
-    ∀ e Φ, ⌜TCEq (to_val e) None⌝ -∗ (P -∗ WP e @ E {{ Φ }}) -∗ WP e @ E {{ Φ }}.
+    ∀ e Φ, (P -∗ WP e @ E {{ Φ }}) -∗ WP e @ E {{ Φ }}.
   Local Definition wp_update_aux : seal (@wp_update_def). Proof. by eexists. Qed.
   Definition wp_update := wp_update_aux.(unseal).
   Lemma wp_update_unseal : wp_update = wp_update_def.
   Proof. rewrite -wp_update_aux.(seal_eq) //. Qed.
 
   Global Instance elim_modal_wp_update_wp p e E P Φ :
-    ElimModal (TCEq (to_val e) None) p false (wp_update E P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+    ElimModal (True) p false (wp_update E P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
   Proof.
     rewrite /ElimModal bi.intuitionistically_if_elim => Hv.
     rewrite wp_update_unseal.
     iIntros "[Hu Hw]".
-    iApply "Hu"; [|done].
-    rewrite Hv //.
+    by iApply "Hu". 
   Qed.
 
   Lemma wp_update_ret E P :
     P ⊢ wp_update E P.
   Proof.
     rewrite wp_update_unseal.
-    iIntros "HP" (e Φ Hv) "Hwp".
+    iIntros "HP" (e Φ) "Hwp".
     iApply ("Hwp" with "HP").
   Qed.
 
@@ -40,7 +39,7 @@ Section wp_update.
     wp_update E P ∗ (P -∗ wp_update E Q) ⊢ wp_update E Q.
   Proof.
     rewrite {3}wp_update_unseal.
-    iIntros "[HP HQ]" (e Φ Hv) "Hwp".
+    iIntros "[HP HQ]" (e Φ) "Hwp".
     iMod "HP".
     iMod ("HQ" with "HP") as "HQ".
     by iApply "Hwp".
@@ -50,7 +49,7 @@ Section wp_update.
     wp_update E P ∗ (P ={E}=∗ Q) ⊢ wp_update E Q.
   Proof.
     rewrite {2}wp_update_unseal.
-    iIntros "[HP Hwand]" (e Φ Hv) "Hwp".
+    iIntros "[HP Hwand]" (e Φ) "Hwp".
     iMod "HP".
     iMod ("Hwand" with "HP") as "HQ".
     by iApply "Hwp".
@@ -68,7 +67,7 @@ Section wp_update.
     (|={E}=> wp_update E P) ⊢ wp_update E P.
   Proof.
     rewrite wp_update_unseal.
-    iIntros "H" (e Φ Hv) "Hwp".
+    iIntros "H" (e Φ) "Hwp".
     iMod "H". by iApply "H".
   Qed.
 
@@ -82,7 +81,7 @@ Section wp_update.
 
   Lemma wp_update_unfold E (P:iProp Σ):
      wp_update E P ⊣⊢
-     (∀ e Φ, ⌜TCEq (to_val e) None⌝ -∗ (P -∗ WP e @ E {{ Φ }}) -∗ WP e @ E {{ Φ }}).
+     (∀ e Φ, (P -∗ WP e @ E {{ Φ }}) -∗ WP e @ E {{ Φ }}).
   Proof.
     by rewrite wp_update_unseal.
   Qed.
@@ -95,7 +94,7 @@ Section wp_update.
   Proof.
     iIntros "H".
     rewrite wp_update_unseal/wp_update_def.
-    iIntros (???) "H'".
+    iIntros (??) "H'".
     iApply state_step_coupl_pgl_wp.
     iIntros (??) "[??]".
     iMod ("H" with "[$]") as "H".
@@ -109,6 +108,27 @@ Section wp_update.
     by iApply "H'".
   Qed.
 
+  Lemma wp_update_epsilon_err E:
+    ⊢ wp_update E (∃ ε, ⌜(0<ε)%R⌝ ∗ ↯ ε).
+  Proof.
+    iApply wp_update_state_step_coupl.
+    iIntros (? ε) "[Hstate Herr]".
+    iApply fupd_mask_intro; first set_solver.
+    iIntros "Hclose".
+    iApply state_step_coupl_ampl'.
+    iIntros (ε' ?).
+    iApply state_step_coupl_ret.
+    assert (ε<=ε')%R as H' by lra.
+    pose (diff :=((ε' - ε) H')%NNR).
+    replace (ε') with (ε + diff)%NNR; last (apply nnreal_ext; rewrite /diff; simpl; lra).
+    iMod (ec_supply_increase _ diff with "[$]") as "[??]".
+    { rewrite /diff. simpl. lra. }
+    iFrame. iMod "Hclose". iPureIntro.
+    rewrite /diff.
+    simpl.
+    lra.
+  Qed.
+  
   Global Instance from_modal_wp_update_wp_update P E :
     FromModal True modality_id (wp_update E P) (wp_update E P) P.
   Proof. iIntros (_) "HP /=". by iApply wp_update_ret. Qed.