From e485559bdc4b66da04c9dbeb5c2c5696dfbda2ee Mon Sep 17 00:00:00 2001
From: Alejandro Aguirre <alejandro@cs.au.dk>
Date: Fri, 13 Oct 2023 11:07:00 +0200
Subject: [PATCH 01/37] Nit

---
 theories/prelude/Reals_ext.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/prelude/Reals_ext.v b/theories/prelude/Reals_ext.v
index 7a65987f..1dc513c1 100644
--- a/theories/prelude/Reals_ext.v
+++ b/theories/prelude/Reals_ext.v
@@ -19,6 +19,9 @@ Proof. intros ???. eapply Rgt_trans. Qed.
 #[global] Instance Rlt_Transitive: Transitive Rlt.
 Proof. intros ???. eapply Rlt_trans. Qed.
 
+#[global] Instance Req_decision (r1 r2 : R) : Decision (r1 = r2).
+Proof. destruct (Rle_dec r1 r2); destruct (Rle_dec r2 r1);
+ [left | right | right |]; lra. Qed.
 #[global] Instance Rgt_decision (r1 r2 : R) : Decision (Rgt r1 r2).
 Proof. apply Rgt_dec. Qed.
 #[global] Instance Rge_decision (r1 r2 : R) : Decision (Rge r1 r2).

From c592873294f19c9b214a7f21d9b8b5d315958ec0 Mon Sep 17 00:00:00 2001
From: Lars Birkedal <birkedal@cs.au.dk>
Date: Tue, 19 Dec 2023 15:13:24 +0100
Subject: [PATCH 02/37] some notes added

---
 theories/tpref_logic/examples/galton_watson_tree.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/tpref_logic/examples/galton_watson_tree.v b/theories/tpref_logic/examples/galton_watson_tree.v
index fa1b2669..1d349fc2 100644
--- a/theories/tpref_logic/examples/galton_watson_tree.v
+++ b/theories/tpref_logic/examples/galton_watson_tree.v
@@ -79,6 +79,7 @@ Section task_loop_spec.
       iIntros (f) "[Hq Hf]".
       wp_pures.
       iApply (rwp_couple_tape _ (λ m s, s = n + m)%nat); [|iFrame "Hspec Hα"].
+      (* Notice how the model step in the preceding line introduces a later in the goal. *)
       { iIntros (σ Hσ).
         rewrite /state_step /=.
         rewrite bool_decide_eq_true_2; [|by eapply elem_of_dom_2].
@@ -88,6 +89,7 @@ Section task_loop_spec.
         apply Rcoupl_dret; eauto. }
       rewrite {2}/task_spec /tc_opaque.
       iIntros "!>" (m ? ->) "Hspec Hα /=".
+      (* Notice how the above line strips a later from the goal and the Loeb induction hyptothesis. *)
       iSpecialize ("Hf" with "Hq Hα Hna").
       wp_apply (rwp_wand with "Hf").
       iIntros (v) "(Hna & Hq & Hα)".
@@ -108,6 +110,7 @@ Section task_loop_spec.
     wp_rec. wp_pures.
     iModIntro. iFrame.
     iIntros "!> %n %m Hq Hα Hna".
+    (* Notice how the above line strips later from the goal and the Loeb IH since task_spec has a later in front *)
     wp_pures.
     wp_apply ("Hc" with "Hα"); iIntros "Hα".
     wp_pures.

From 29f6f219d03b09d8e52c456b54ab64f32e503e37 Mon Sep 17 00:00:00 2001
From: Alejandro Aguirre <alejandro@cs.au.dk>
Date: Fri, 22 Dec 2023 17:34:40 +0100
Subject: [PATCH 03/37] WIP on amortized error for hash

---
 theories/ub_logic/cf_hash.v | 397 ++++++++++++++++++++++++++++++++++++
 1 file changed, 397 insertions(+)
 create mode 100644 theories/ub_logic/cf_hash.v

diff --git a/theories/ub_logic/cf_hash.v b/theories/ub_logic/cf_hash.v
new file mode 100644
index 00000000..e91512ce
--- /dev/null
+++ b/theories/ub_logic/cf_hash.v
@@ -0,0 +1,397 @@
+From clutch.ub_logic Require Export ub_clutch hash lib.map.
+From clutch.prelude Require Export sum_n_ext.
+Import Hierarchy.
+Set Default Proof Using "Type*".
+
+Module coll_free_hash.
+
+  Context `{!ub_clutchGS Σ}.
+
+  (*
+
+     A module implementing a "collision-free hash" with constant amortized
+     error. The hash keeps track of a threshold R, a current
+     hash size S such that (S < R) and a size of value space VS. On every
+     query on a new element, it samples uniformly from (0,...,VS-1). Once S
+     reaches R, the hash is resized, so that L becomes R, R becomes 4R
+     and S becomes 4S (e.g., we could sample two extra bits to keep uniformity).
+     This guarantees a constant amortized error cost of (2*R0)/VS0 assuming
+     on initialization S = 0, R = R0 and VS = VS0. This is not a tight bound,
+     it is chosen to work nicely with powers of 2, so there is some extra
+     unused error credits
+  *)
+
+  Variable init_val_size : nat.
+  Variable init_r : nat.
+
+  Definition compute_cf_hash : val :=
+    λ: "hm" "vs" "s" "r" "v",
+      match: get "hm" "v" with
+      | SOME "b" => "b"
+      | NONE =>
+          let: "val_size" := !"vs" in
+          let: "b" := rand ("val_size" - #1) in
+          set "hm" "v" "b";;
+          "s" <- !"s"+#1;;
+          if: !"s" = !"r" then
+            "r" <- #4 * !"r";;
+            "vs" <- #4 * !"val_size";;
+            "b"
+         else "b"
+      end.
+
+  Definition compute_cf_hash_specialized hm vs s r : val :=
+    λ: "v",
+      match: get hm "v" with
+      | SOME "b" => "b"
+      | NONE =>
+          let: "val_size" := !vs in
+          let: "b" := rand ("val_size" - #1) in
+          set hm "v" "b";;
+          s <- !s+#1;;
+          if: !s = !r then
+            r <- #4 * !r;;
+            vs <- #4 * "val_size" ;;
+            "b"
+         else "b"
+      end.
+
+  Definition init_cf_hash_state : val := init_map.
+
+  Definition init_cf_hash : val :=
+    λ: "_",
+      let: "hm" := init_cf_hash_state #() in
+      let: "vs" := ref (#init_val_size) in
+      let: "s" := ref (#0) in
+      let: "r" := ref (#init_r) in
+      compute_cf_hash "hm" "vs" "s" "r".
+
+
+  Definition coll_free (m : gmap nat Z) :=
+    forall k1 k2,
+      is_Some (m !! k1) ->
+      is_Some (m !! k2) ->
+      m !!! k1 = m !!! k2 ->
+      k1 = k2.
+
+  Lemma coll_free_insert (m : gmap nat Z) (n : nat) (z : Z) :
+    m !! n = None ->
+    coll_free m ->
+    Forall (λ x, z ≠ snd x) (gmap_to_list m) ->
+    coll_free (<[ n := z ]>m).
+  Proof.
+    intros Hnone Hcoll HForall.
+    intros k1 k2 Hk1 Hk2 Heq.
+    apply lookup_insert_is_Some' in Hk1.
+    apply lookup_insert_is_Some' in Hk2.
+    destruct (decide (n = k1)).
+    - destruct (decide (n = k2)); simplify_eq; auto.
+      destruct Hk2 as [|Hk2]; auto.
+      rewrite lookup_total_insert in Heq.
+      rewrite lookup_total_insert_ne // in Heq.
+      apply lookup_lookup_total in Hk2.
+      rewrite -Heq in Hk2.
+      eapply (Forall_iff (uncurry ((λ (k : nat) (v : Z), z ≠ v)))) in HForall; last first.
+      { intros (?&?); eauto. }
+      eapply map_Forall_to_list in HForall.
+      rewrite /map_Forall in HForall.
+      eapply HForall in Hk2; congruence.
+    - destruct (decide (n = k2)); simplify_eq; auto.
+      {
+        destruct Hk1 as [|Hk1]; auto.
+        rewrite lookup_total_insert in Heq.
+        rewrite lookup_total_insert_ne // in Heq.
+        apply lookup_lookup_total in Hk1.
+        rewrite Heq in Hk1.
+        eapply (Forall_iff (uncurry ((λ (k : nat) (v : Z), z ≠ v)))) in HForall; last first.
+        { intros (?&?); eauto. }
+        eapply map_Forall_to_list in HForall.
+        rewrite /map_Forall in HForall.
+        eapply HForall in Hk1; congruence.
+      }
+      rewrite ?lookup_total_insert_ne // in Heq.
+      destruct Hk1 as [|Hk1]; try congruence; [].
+      destruct Hk2 as [|Hk2]; try congruence; [].
+      apply Hcoll; eauto.
+  Qed.
+
+  (*
+     The representation predicate stores, alongside the
+     values for all the variables keeping track of the
+     hash size and threshold, a reserve of error credits,
+     such that when the actual error becomes larger than
+     the constant amortized amount of error credits we
+     get on every insertion, we are still able to pay
+     for the totalerror
+  *)
+
+  Definition cf_hashfun f m (vsval sval rval : nat) ε: iProp Σ :=
+    ∃ (hm vs s r : loc),
+      € ε ∗
+      vs ↦ #vsval ∗ s ↦ #sval ∗ r ↦ #rval ∗
+      ⌜ f = compute_cf_hash_specialized #hm #vs #s #r⌝ ∗
+      map_list hm ((λ b, LitV (LitInt b)) <$> m) ∗
+      ⌜ sval < rval ⌝ ∗
+      ⌜ sval = (length (gmap_to_list m)) ⌝ ∗
+      ⌜(ε + (rval - sval)*(2*init_r)/(init_val_size) >=
+          sum_n_m (λ x, x/vsval) sval (rval-1) )%R ⌝ ∗
+      ⌜ coll_free m ⌝.
+
+  (*
+    The management of the potential is kept abstract by the following
+    two lemmas. These allow us to update our error resources after every
+    insertion while ensuring that what we get afterwards is still a valid
+    collision-free hash. The actual math is in here, after proving these
+    the proof of the specifications is straightforward
+  *)
+
+  Lemma cf_update_potential (vsval sval rval : nat) ε :
+    (sval + 1 < rval)%nat ->
+      € ε -∗
+      ⌜ (ε + (rval - sval)*(2*init_r)/(init_val_size) >=
+          sum_n_m (λ x, x/vsval) sval (rval - 1))%R ⌝%I -∗
+      € (nnreal_div (nnreal_nat (2*init_r)) (nnreal_nat(init_val_size))) -∗
+      ∃ (ε' : nonnegreal),
+      € ε' ∗
+      € (nnreal_div (nnreal_nat sval) (nnreal_nat vsval)) ∗
+      ⌜(ε' + (rval - (sval + 1))*(2*init_r)/(init_val_size) >=
+          sum_n_m (λ x, x/vsval) (sval + 1) (rval - 1))%R ⌝.
+  Proof.
+    intro Hsval.
+    iIntros "Herr1".
+    iIntros "%Hsum".
+    iIntros "Herr2".
+  Admitted.
+
+
+  Lemma cf_update_potential_resize (vsval sval rval : nat) ε :
+    (sval + 1 = rval)%nat ->
+      € ε -∗
+      ⌜ (ε + (2*init_r)/(init_val_size) >= ((rval - 1)/vsval))%R ⌝%I -∗
+      € (nnreal_div (nnreal_nat (2*init_r)) (nnreal_nat(init_val_size))) -∗
+      € nnreal_zero ∗
+      € (nnreal_div (nnreal_nat sval) (nnreal_nat vsval)) ∗
+      ⌜((4 * rval - (sval + 1))*(2*init_r)/(init_val_size) >=
+          sum_n_m (λ x, x/4*vsval) (sval + 1) (4*rval - 1))%R ⌝.
+  Admitted.
+
+
+  Lemma wp_insert_no_coll E f m (vsval sval rval: nat) ε (n : nat) :
+    m !! n = None →
+    0 < vsval ->
+    (sval + 1 < rval)%nat ->
+    {{{ cf_hashfun f m vsval sval rval ε ∗
+          € (nnreal_div (nnreal_nat (2*init_r)) (nnreal_nat(init_val_size))) }}}
+      f #n @ E
+    {{{ (v : Z), RET #v;
+        ∃ ε',
+          cf_hashfun f (<[ n := v ]>m) vsval (sval+1) rval ε' }}}.
+  Proof.
+    iIntros (Hlookup Hvsval_pos Hineq Φ) "(Hhash & Herr) HΦ".
+    iDestruct "Hhash" as (hm vs s r)
+                           "(Herr2 & Hvs & Hs & Hr & -> & Hmap & %Hlsr & %Hlen & Htot_err & %Hcf)".
+    rewrite /compute_cf_hash_specialized.
+    wp_pures.
+    wp_apply (wp_get with "[$]").
+    iIntros (vret) "(Hhash&->)".
+    rewrite lookup_fmap Hlookup /=. wp_pures.
+    wp_load. wp_pures.
+    wp_bind (rand _)%E.
+    wp_apply (wp_rand_err_list_int _ (vsval - 1) (map (λ p, snd p) (gmap_to_list m))); auto.
+    rewrite map_length -Hlen.
+    iPoseProof (cf_update_potential _ _ _ _ _
+                 with "[Herr2 //] [Htot_err //] [Herr //]")
+      as (ε') "(Herr3 & Herr4 & %Hupdp)".
+    Unshelve.
+    2:{ auto. }
+    replace (nnreal_nat ((Z.to_nat (vsval - 1)) + 1)) with
+              (nnreal_nat vsval); last first.
+    { f_equal.
+      destruct vsval; [ |lia].
+      simpl in Hvsval_pos.
+      lra.
+    }
+    iFrame.
+    iIntros "%x %HForall".
+    wp_pures.
+    wp_apply (wp_set with "Hhash").
+    iIntros "Hlist".
+    wp_pures.
+    wp_load.
+    wp_pures.
+    wp_store.
+    wp_load.
+    wp_load.
+    wp_pures.
+    rewrite bool_decide_eq_false_2; last first.
+    {
+      intro H.
+      inversion H.
+      lia.
+    }
+    wp_pures.
+    iModIntro.
+    iApply "HΦ".
+    iExists ε'.
+    rewrite /cf_hashfun.
+    iExists hm, vs, s, r.
+    (* Is there a way to avoid having to apply this coercion? *)
+    assert (#(sval + 1)%nat = #(sval + 1)) as Hsval.
+    {
+      do 2 f_equal. lia.
+    }
+    rewrite Hsval.
+    iFrame.
+    iSplit.
+    - auto.
+    - iSplit.
+      + rewrite fmap_insert //.
+      + iSplit.
+        * iPureIntro.
+          apply lt_INR in Hineq.
+          lra.
+        * iSplit.
+          -- iPureIntro.
+             etrans; last first.
+             ** eapply Permutation_length.
+                symmetry.
+                (* FIXME : Why can it not infer typeclassses ? *)
+                eapply (@map_to_list_insert _ _ _ _ _ _ _ _ _ _
+                          (gmap_finmap)); eauto.
+             ** simpl.
+                rewrite -Hlen. lia.
+          -- iSplit.
+             ++ iPureIntro.
+                rewrite plus_INR /= //.
+             ++ iPureIntro.
+                apply coll_free_insert; auto.
+                apply (Forall_map (λ p : nat * Z, p.2)) in HForall; auto.
+ Qed.
+
+
+  Lemma wp_insert_no_coll_resize E f m (vsval sval rval: nat) ε (n : nat) :
+    m !! n = None →
+    0 < vsval ->
+    (sval + 1 = rval)%nat ->
+    {{{ cf_hashfun f m vsval sval rval ε ∗
+          € (nnreal_div (nnreal_nat (2*init_r)) (nnreal_nat(init_val_size))) }}}
+      f #n @ E
+    {{{ (v : Z), RET #v;
+          cf_hashfun f (<[ n := v ]>m) (Nat.mul 4 vsval) rval (Nat.mul 4 rval) nnreal_zero }}}.
+  Proof.
+    iIntros (Hlookup Hvsval_pos Heq Φ) "(Hhash & Herr) HΦ".
+    iDestruct "Hhash" as (hm vs s r)
+                           "(Herr2 & Hvs & Hs & Hr & -> & Hmap & %Hlsr & %Hlen & %Htot_err & %Hcf)".
+    rewrite /compute_cf_hash_specialized.
+    wp_pures.
+    wp_apply (wp_get with "[$]").
+    iIntros (vret) "(Hhash&->)".
+    rewrite lookup_fmap Hlookup. wp_pures.
+    wp_load. wp_pures.
+    wp_bind (rand _)%E.
+    wp_apply (wp_rand_err_list_int _ (vsval - 1) (map (λ p, snd p) (gmap_to_list m))); auto.
+    rewrite map_length -Hlen.
+    iPoseProof (cf_update_potential_resize vsval sval rval _ _
+                 with "[Herr2 //] [] [Herr //]")
+      as "(Herr3 & Herr4 & %Hupdp)".
+    Unshelve.
+    {
+      iPureIntro.
+      rewrite -Heq plus_INR /= in Htot_err.
+      rewrite Nat.add_sub sum_n_n in Htot_err.
+      rewrite -Heq /=.
+      rewrite plus_INR /=.
+      rewrite /Rminus Rplus_assoc Rplus_minus Rmult_1_l in Htot_err.
+      setoid_rewrite Htot_err.
+      lra.
+    }
+    2:{ auto. }
+    replace (nnreal_nat ((Z.to_nat (vsval - 1)) + 1)) with
+              (nnreal_nat vsval); last first.
+    { f_equal.
+      destruct vsval; [ |lia].
+      simpl in Hvsval_pos.
+      lra.
+    }
+    iFrame.
+    iIntros "%x %HForall".
+    wp_pures.
+    wp_apply (wp_set with "Hhash").
+    iIntros "Hlist".
+    wp_pures.
+    wp_load.
+    wp_pures.
+    wp_store.
+    wp_load.
+    wp_load.
+    wp_pures.
+    rewrite bool_decide_eq_true_2; last first.
+    {
+      do 2 f_equal.
+      lia.
+    }
+    wp_pures.
+    wp_load.
+    wp_pures.
+    wp_store.
+    wp_pures.
+    wp_store.
+    iModIntro.
+    iApply "HΦ".
+    rewrite /cf_hashfun.
+    iExists hm, vs, s, r.
+    (* Is there a way to avoid having to apply this coercion? *)
+    assert (#(sval + 1)%nat = #(sval + 1)) as Hsval.
+    {
+      do 2 f_equal. lia.
+    }
+    iFrame.
+    iSplitL "Hvs".
+    {
+      replace (#(4 * vsval)%nat) with (#(4 * vsval)); auto.
+      do 2 f_equal; lia.
+    }
+    iSplitL "Hs".
+    {
+      replace (#(rval)) with (#(sval+1)); auto.
+      do 2 f_equal; lia.
+    }
+    iSplitL "Hr".
+    {
+      replace (#(4 * rval)%nat) with (#(4 * rval)); auto.
+      do 2 f_equal; lia.
+    }
+    iSplit.
+    - auto.
+    - iSplit.
+      + rewrite fmap_insert //.
+      + iSplit.
+        * iPureIntro.
+          rewrite mult_INR.
+          Search Rlt.
+          rewrite <- (Rmult_1_l rval) at 1.
+          apply Rmult_lt_compat_r.
+          -- eapply Rle_lt_trans; eauto.
+             apply pos_INR.
+          -- simpl. lra.
+        * iSplit.
+          -- iPureIntro.
+             etrans; last first.
+             ** eapply Permutation_length.
+                symmetry.
+                (* FIXME : Why can it not infer typeclassses ? *)
+                eapply (@map_to_list_insert _ _ _ _ _ _ _ _ _ _
+                          (gmap_finmap)); eauto.
+             ** simpl.
+                rewrite -Hlen. lia.
+          -- iSplit.
+             ++ iPureIntro.
+                rewrite <- Heq at 3.
+                (* This is true, just annoying to prove *)
+                admit.
+             ++ iPureIntro.
+                apply coll_free_insert; auto.
+                apply (Forall_map (λ p : nat * Z, p.2)) in HForall; auto.
+ Admitted.
+
+End coll_free_hash.

From 35c492c4e13234e59fed96c8dff3e96f439a79fc Mon Sep 17 00:00:00 2001
From: Alejandro Aguirre <alejandro@cs.au.dk>
Date: Fri, 22 Dec 2023 18:13:10 +0100
Subject: [PATCH 04/37] Trying to fix build

---
 theories/ub_logic/cf_hash.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/ub_logic/cf_hash.v b/theories/ub_logic/cf_hash.v
index e91512ce..6954d6da 100644
--- a/theories/ub_logic/cf_hash.v
+++ b/theories/ub_logic/cf_hash.v
@@ -1,7 +1,5 @@
 From clutch.ub_logic Require Export ub_clutch hash lib.map.
-From clutch.prelude Require Export sum_n_ext.
 Import Hierarchy.
-Set Default Proof Using "Type*".
 
 Module coll_free_hash.
 

From 3ffa8104259b5a1a00e0a3d0649b908db09b5525 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Sun, 24 Dec 2023 15:17:23 -0500
Subject: [PATCH 05/37] wp_presample rule

---
 theories/ub_logic/ub_rules.v | 56 ++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 8b6f6f55..120c4ea9 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -538,4 +538,60 @@ Proof.
   reflexivity.
 Admitted.
 
+
+
+(** * Approximate Lifting *)
+(* see ARcoupl_state_state  *)
+Lemma ub_lift_state (N : nat) 𝜎 𝛼 ns (ε : nonnegreal) :
+  𝜎.(tapes) !! 𝛼 = Some (N; ns) →
+  ub_lift
+    (state_step 𝜎 𝛼)
+    (fun 𝜎' => exists (n : fin (S N)), 𝜎' = state_upd_tapes <[𝛼 := (N; ns ++ [n])]> 𝜎)
+    ε.
+Proof.
+
+
+
+Admitted.
+
+(** adapted from wp_couple_tapes in the relational logic *)
+Lemma wp_presample (N : nat) E e 𝛼 ns Φ :
+  to_val e = None →
+  (∀ σ', reducible e σ') →
+  ▷ 𝛼 ↪ (N; ns) ∗
+  (∀ (n : fin (S N)), 𝛼 ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
+  ⊢ WP e @ E {{ Φ }}.
+Proof.
+    iIntros (He Hred) "(>H𝛼&Hwp)".
+    iApply wp_lift_step_fupd_exec_ub; [done|].
+    iIntros (𝜎 ε) "((Hheap&Htapes)&Hε)".
+    iDestruct (ghost_map_lookup with "Htapes H𝛼") as %Hlookup.
+    iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'".
+    iSplitR; [done|].
+    (* now we need to prove an exec_ub, we should be able to do this with a state step. *)
+    replace ε with (nnreal_zero + ε)%NNR by (apply nnreal_ext; simpl; lra).
+    iApply exec_ub_state_step.
+    { rewrite /= /get_active.
+      by apply elem_of_list_In, elem_of_list_In, elem_of_elements, elem_of_dom. }
+    iExists _.
+    iSplit.
+    { iPureIntro. apply ub_lift_state, Hlookup. }
+    iIntros (𝜎') "[%n %H𝜎']".
+    (* now we have to prove the exec_ub about 𝜎', we should be able to do this with the wp *)
+    (* first: udpate the resources *)
+    iDestruct (ghost_map_lookup with "Htapes H𝛼") as %?%lookup_total_correct.
+    iMod (ghost_map_update ((N; ns ++ [n]) : tape) with "Htapes H𝛼") as "[Htapes H𝛼]".
+    iMod "Hclose'" as "_". (* ?? *)
+    iSpecialize ("Hwp" $! n with "H𝛼").
+    rewrite !ub_wp_unfold /ub_wp_pre /= He.
+    iSpecialize ("Hwp" $! 𝜎' ε).
+    iMod ("Hwp" with "[Hheap Htapes Hε]") as "(?&Hwp)".
+    { replace (nnreal_zero + ε)%NNR with ε by (apply nnreal_ext; simpl; lra).
+      rewrite H𝜎'.
+      iFrame.
+    }
+    iModIntro. iApply "Hwp".
+Qed.
+
+
 End rules.

From dc9736d808a8cafa2df8dd73bbe076e348308f1b Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Sun, 24 Dec 2023 16:15:30 -0500
Subject: [PATCH 06/37] last admit in wp_presample

---
 theories/ub_logic/ub_rules.v | 30 +++++++++++++++++++++++-------
 1 file changed, 23 insertions(+), 7 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 120c4ea9..73502a45 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -541,18 +541,34 @@ Admitted.
 
 
 (** * Approximate Lifting *)
-(* see ARcoupl_state_state  *)
-Lemma ub_lift_state (N : nat) 𝜎 𝛼 ns (ε : nonnegreal) :
+(* FIXME: clean up *)
+Lemma ub_lift_state (N : nat) 𝜎 𝛼 ns :
   𝜎.(tapes) !! 𝛼 = Some (N; ns) →
   ub_lift
     (state_step 𝜎 𝛼)
     (fun 𝜎' => exists (n : fin (S N)), 𝜎' = state_upd_tapes <[𝛼 := (N; ns ++ [n])]> 𝜎)
-    ε.
+    nnreal_zero.
 Proof.
-
-
-
-Admitted.
+  rewrite /ub_lift.
+  intros Htapes P Hp.
+  apply Req_le_sym; simpl.
+  rewrite /prob SeriesC_0; auto.
+  intros 𝜎'.
+  remember (negb (P 𝜎')) as K; destruct K; auto.
+  rewrite /state_step.
+  case_bool_decide.
+  2: { exfalso. apply H. by apply elem_of_dom. }
+  intros.
+  replace (lookup_total 𝛼 (tapes 𝜎)) with (N; ns).
+  2: { rewrite (lookup_total_correct _ _ (existT N ns)); auto.  }
+  apply dmap_unif_zero.
+  intros n Hcont.
+  apply diff_true_false.
+  specialize Hp with 𝜎'.
+  rewrite -Hp; [| by exists n].
+  replace false with (negb true) by auto.
+  by rewrite HeqK negb_involutive.
+Qed.
 
 (** adapted from wp_couple_tapes in the relational logic *)
 Lemma wp_presample (N : nat) E e 𝛼 ns Φ :

From b9386d5b60d2d5cd090ba0b75e67d56ac9761667 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 25 Dec 2023 10:00:55 -0500
Subject: [PATCH 07/37] update ub_weakestpre with advanced composition for
 state steps (1 admit)

---
 theories/ub_logic/ub_rules.v      |  14 ++++
 theories/ub_logic/ub_weakestpre.v | 118 ++++++++++++++++++++++++++----
 2 files changed, 119 insertions(+), 13 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 73502a45..09c38518 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -610,4 +610,18 @@ Proof.
 Qed.
 
 
+Lemma wp_presample_adv_comp (N : nat) 𝛼 ns z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
+  TCEq N (Z.to_nat z) →
+  to_val e = None →
+  (∀ σ', reducible e σ') →
+  SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
+  ▷ 𝛼 ↪ (N; ns) ∗
+  € ε1 ∗
+  (∀ (n : fin (S N)), € (ε2 n) ∗ 𝛼 ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
+  ⊢ WP e @ E {{ Φ }}.
+Proof.
+Admitted.
+
+
+
 End rules.
diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 9afd876e..03781ff1 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -59,8 +59,15 @@ Section exec_ub.
       ([∨ list] α ∈ get_active σ1,
       (* We allow an explicit weakening of the grading, but maybe it is not needed *)
         (∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ ub_lift (state_step σ1 α) R ε1 ⌝ ∗
-              ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ Φ (ε2,((e1, σ2)))))
-    )%I.
+              ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ Φ (ε2,((e1, σ2))))) ∨
+      (* [state_step] with adv composition*)
+      ([∨ list] α ∈ get_active σ1,
+        (∃ R (ε1 : nonnegreal) (ε2 : cfg Λ -> nonnegreal),
+          ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
+          ⌜ (ε1 + SeriesC (λ ρ, (state_step σ1 α ρ) * ε2 (e1, ρ)) <= ε)%R ⌝ ∗
+          ⌜ub_lift (state_step σ1 α) R ε1⌝ ∗
+              ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ Φ (ε2 (e1, σ2), (e1, σ2)))))%I.
+
 
   (* TODO: Define this globally, it appears in error credits too *)
   Canonical Structure NNRO := leibnizO nonnegreal.
@@ -79,10 +86,10 @@ Section exec_ub.
     iIntros (Φ Ψ HNEΦ HNEΨ) "#Hwand".
     rewrite /exec_ub_pre.
     iIntros ((ε&(e1 & σ1))) "Hexec".
-    iDestruct "Hexec" as "[H | [H | H]]".
+    iDestruct "Hexec" as "[H | [H | [H | H]]]".
     - by iLeft.
     - by iRight; iLeft.
-    - iRight; iRight.
+    - iRight; iRight; iLeft.
       iInduction (get_active σ1) as [| l] "IH" forall "H".
       { rewrite big_orL_nil //. }
       rewrite !big_orL_cons.
@@ -93,6 +100,18 @@ Section exec_ub.
         iSplit; [try done|].
         iIntros. iApply "Hwand". by iApply "HΦ".
       + iRight. by iApply "IH".
+    - iRight; iRight; iRight.
+      iInduction (get_active σ1) as [| l] "IH" forall "H".
+      { rewrite big_orL_nil //. }
+      rewrite !big_orL_cons.
+      iDestruct "H" as "[(% & % & % & % & %Hsum & Hlift & HΦ) | H]".
+      + iLeft. iExists R2.
+        iExists ε1. iExists _.
+        iSplit; [try done|].
+        iSplit; [try done|].
+        iSplit; [try done|].
+        iIntros. iApply "Hwand". by iApply "HΦ".
+      + iRight. by iApply "IH".
   Qed.
 
   Definition exec_ub' Z := bi_least_fixpoint (exec_ub_pre Z).
@@ -108,7 +127,13 @@ Section exec_ub.
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z (ε2 ρ2) ρ2 ) ∨
       ([∨ list] α ∈ get_active σ1,
         (∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ ub_lift (state_step σ1 α) R ε1 ⌝ ∗
-              ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z ε2 )))%I.
+              ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z ε2 )) ∨
+      ([∨ list] α ∈ get_active σ1,
+        (∃ R (ε1 : nonnegreal) (ε2 : cfg Λ -> nonnegreal),
+          ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
+          ⌜ (ε1 + SeriesC (λ ρ, (state_step σ1 α ρ) * ε2 (e1, ρ)) <= ε)%R ⌝ ∗
+          ⌜ub_lift (state_step σ1 α) R ε1⌝ ∗
+              ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z (ε2 (e1, σ2)))))%I.
   Proof. rewrite /exec_ub/exec_ub' least_fixpoint_unfold //. Qed.
 
   Local Definition cfgO := (prodO (exprO Λ) (stateO Λ)).
@@ -126,7 +151,7 @@ Section exec_ub.
     iPoseProof (least_fixpoint_ind (exec_ub_pre Z) Φ with "[]") as "H"; last first.
     { iApply ("H" with "H_ub"). }
     iIntros "!#" ([ε'' [? σ']]). rewrite /exec_ub_pre.
-    iIntros "[ (% & % & % & % & H) | [ (% & % & % & % & % & % & H) | H] ] %ε3 %Hleq' /="; simpl in Hleq'.
+    iIntros "[ (% & % & % & % & H) | [ (% & % & % & % & % & % & H) | [ H | H ]]] %ε3 %Hleq' /="; simpl in Hleq'.
     - rewrite least_fixpoint_unfold.
       iLeft. iExists _,_,_.
       iSplit; [|done].
@@ -137,7 +162,7 @@ Section exec_ub.
       1,3,4:done.
       iPureIntro; etrans; done.
     - rewrite least_fixpoint_unfold.
-      iRight; iRight.
+      iRight; iRight; iLeft.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
@@ -150,6 +175,21 @@ Section exec_ub.
         iApply ("H" with "[//]").
         iPureIntro. simpl; lra.
       + iRight. by iApply ("IH" with "Ht").
+    - rewrite least_fixpoint_unfold.
+      iRight; iRight; iRight.
+      iInduction (get_active σ') as [| l] "IH".
+      { rewrite big_orL_nil //. }
+      rewrite 2!big_orL_cons.
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hleq2 & %Hub & %Hlift & H )) | Ht]".
+      + iLeft.
+        iExists R2. iExists ε1. iExists ε2.
+        iSplit; [auto|].
+        iSplit; [ iPureIntro; lra | ].
+        iSplit; [ done | ].
+        iIntros.
+        iApply ("H" with "[//]").
+        iPureIntro. simpl; lra.
+      + iRight. by iApply ("IH" with "Ht").
   Qed.
 
 
@@ -169,7 +209,7 @@ Section exec_ub.
     iPoseProof (least_fixpoint_iter (exec_ub_pre Z1) Φ with "[]") as "H"; last first.
     { by iApply ("H" with "H_ub"). }
     iIntros "!#" ([ε'' [? σ']]). rewrite /exec_ub_pre.
-    iIntros "[ (% & % & % & % & % & H) | [ (% & % & % & % & % & % & H) | H] ] HZ /=".
+    iIntros "[ (% & % & % & % & % & H) | [ (% & % & % & % & % & % & H) | [H | H]] ] HZ /=".
     - rewrite least_fixpoint_unfold.
       iLeft. iExists _,_,_.
       iSplit; [done|].
@@ -189,7 +229,7 @@ Section exec_ub.
       iIntros ([] (?&?)). iMod ("H" with "[//]").
       iModIntro. iApply "HZ". eauto.
     - rewrite least_fixpoint_unfold.
-      iRight; iRight.
+      iRight; iRight; iLeft.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
@@ -200,6 +240,19 @@ Section exec_ub.
         iIntros.
         by iApply ("H" with "[//]").
       + iRight. by iApply ("IH" with "Ht").
+    - rewrite least_fixpoint_unfold.
+      iRight; iRight; iRight.
+      iInduction (get_active σ') as [| l] "IH".
+      { rewrite big_orL_nil //. }
+      rewrite 2!big_orL_cons.
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (% & % & % & H)) | Ht]".
+      + iLeft. iExists R2. iExists ε1. iExists ε2.
+        iSplit; [auto | ].
+        iSplit; [iPureIntro; lra | ].
+        iSplit; [done | ].
+        iIntros.
+        by iApply ("H" with "[//]").
+      + iRight. by iApply ("IH" with "Ht").
   Qed.
 
   Lemma exec_ub_mono (Z1 Z2 : nonnegreal -> cfg Λ → iProp Σ) e1 σ1 (ε1 ε2 : nonnegreal) :
@@ -242,7 +295,7 @@ Section exec_ub.
                  with "[]") as "H"; last first.
     { iIntros (?). iApply ("H" $! (_, (_, _)) with "Hub [//]"). }
     iIntros "!#" ([ε' [? σ']]). rewrite /exec_ub_pre.
-    iIntros "[(% & % & % & % & % & H) | [ (% & % & % & (%r & %Hr) & % & % & H) | H]] %Hv'".
+    iIntros "[(% & % & % & % & % & H) | [ (% & % & % & (%r & %Hr) & % & % & H) | [H|H]]] %Hv'".
     - rewrite least_fixpoint_unfold.
       iLeft. simpl.
       iExists (λ '(e2, σ2), ∃ e2', e2 = K e2' ∧ R2 (e2', σ2)),_,_.
@@ -355,7 +408,7 @@ Section exec_ub.
         by rewrite Haux.
        Unshelve. auto.
     - rewrite least_fixpoint_unfold /=.
-      iRight; iRight.
+      iRight; iRight; iLeft.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
@@ -366,7 +419,21 @@ Section exec_ub.
         iSplit; [done|].
         iIntros. by iApply ("H" with "[//]").
       + iRight. by iApply ("IH" with "Ht").
-  Qed.
+    - rewrite least_fixpoint_unfold /=.
+      iRight; iRight; iRight.
+      iInduction (get_active σ') as [| l] "IH".
+      { rewrite big_orL_nil //. }
+      rewrite 2!big_orL_cons.
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hleq & %Hub & %Hlift & H)) | Ht]".
+      + iLeft.
+        iExists _,_,_.
+        iSplit; [done|].
+        (* is this still true??? I think I'll need to adapt the adv_comp case in more detail *)
+        iSplit; [admit|].
+        iSplit; [done|].
+        iIntros. admit.
+      + iRight. by iApply ("IH" with "Ht").
+  Admitted.
 
   Lemma exec_ub_prim_step e1 σ1 Z (ε : nonnegreal) :
     (∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
@@ -428,7 +495,7 @@ Section exec_ub.
     iIntros (?) "H".
     iDestruct "H" as (?) "H".
     rewrite {1}exec_ub_unfold.
-    iRight; iRight.
+    iRight; iRight; iLeft.
     iApply big_orL_elem_of; eauto.
     iExists R2.
     iExists ε.
@@ -438,6 +505,31 @@ Section exec_ub.
     simpl. lra.
   Qed.
 
+
+
+  (* for state steps that consume zero error *)
+  Lemma exec_ub_state_adv_comp' α e1 σ1 Z (ε : nonnegreal) :
+    (α ∈ get_active σ1 ->
+     (∃ R (ε2 : cfg Λ -> nonnegreal),
+        ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
+        ⌜ (SeriesC (λ ρ, (state_step σ1 α ρ) * ε2 (e1, ρ)) = ε)%R ⌝ ∗
+        ⌜ub_lift (state_step σ1 α) R nnreal_zero⌝ ∗
+        ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z (ε2 (e1, σ2)))
+      ⊢ exec_ub e1 σ1 Z ε)%I.
+  Proof.
+    iIntros (?) "(% & % & % & %Hε & % & H)".
+    rewrite {1}exec_ub_unfold.
+    iRight; iRight; iRight.
+    iApply big_orL_elem_of; eauto.
+    iExists _,nnreal_zero,_.
+    iSplit; [auto|].
+    iSplit.
+    { iPureIntro. apply Req_le. rewrite Hε /=. lra. }
+    iSplit; [done|done].
+  Qed.
+
+
+
 (*
   Lemma exec_ub_reducible e σ Z1 Z2 ε1 ε2 :
     (exec_ub e σ Z1 ε1)  ={∅}=∗ ⌜irreducible e σ⌝ -∗ (exec_ub e σ Z2 ε2).

From 34972b203bf2bb0e33aefe8e869cefdf756c20fb Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 25 Dec 2023 10:07:03 -0500
Subject: [PATCH 08/37] stub adequacy (to compile)

---
 theories/ub_logic/adequacy.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/ub_logic/adequacy.v b/theories/ub_logic/adequacy.v
index d81ca8b6..5668089f 100644
--- a/theories/ub_logic/adequacy.v
+++ b/theories/ub_logic/adequacy.v
@@ -69,7 +69,7 @@ Section adequacy.
     }
     clear.
     iIntros "!#" ([ε'' [e1 σ1]]). rewrite /Φ/F/exec_ub_pre.
-    iIntros "[ (%R & %ε1 & %ε2 & % & %Hlift & H)| [ (%R & %ε1 & %ε2 & (%r & %Hr) & % & %Hlift & H)| H]] %Hv".
+    iIntros "[ (%R & %ε1 & %ε2 & % & %Hlift & H)| [ (%R & %ε1 & %ε2 & (%r & %Hr) & % & %Hlift & H)| [H|H]]] %Hv".
     - iApply step_fupdN_mono.
       { apply pure_mono.
         eapply UB_mon_grading; eauto. }
@@ -111,7 +111,8 @@ Section adequacy.
       rewrite big_orL_cons.
       iDestruct "H" as "[H | Ht]"; [done|].
       by iApply "IH".
-  Qed.
+   - admit.
+  Admitted.
 
   Theorem wp_refRcoupl_step_fupdN (e : expr) (σ : state) (ε : nonnegreal) n φ  :
     state_interp σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢

From c832c4d3037929b3d98c1bdf3d81807d140f3e40 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Wed, 27 Dec 2023 11:51:50 -0500
Subject: [PATCH 09/37] exec modality change in adequacy

---
 theories/ub_logic/adequacy.v | 30 ++++++++++++++++++++++++++++--
 1 file changed, 28 insertions(+), 2 deletions(-)

diff --git a/theories/ub_logic/adequacy.v b/theories/ub_logic/adequacy.v
index 5668089f..004367ba 100644
--- a/theories/ub_logic/adequacy.v
+++ b/theories/ub_logic/adequacy.v
@@ -106,13 +106,39 @@ Section adequacy.
           erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim _ _ _ _ _ Hα)); eauto.
           eapply ub_lift_dbind; eauto; [apply cond_nonneg | ].
           apply cond_nonneg.
+        - iIntros (??).
+          by iMod ("H" with "[//] [//]") as "W". }
+      iInduction (language.get_active σ1) as [| α] "IH"; [done|].
+      rewrite big_orL_cons.
+      iDestruct "H" as "[H | Ht]"; [done|].
+      by iApply "IH".
+   - rewrite exec_Sn_not_final; [|eauto].
+      iDestruct (big_orL_mono _ (λ _ _,
+                     |={∅}▷=>^(S n)
+                       ⌜ub_lift (prim_step e1 σ1 ≫= exec n) φ ε''⌝)%I
+                  with "H") as "H".
+      { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hε'' & %Hleq & %Hlift & H)".
+        replace (prim_step e1 σ1) with (step (e1, σ1)) => //.
+        rewrite -exec_Sn_not_final; [|eauto].
+        iApply (step_fupdN_mono _ _ _
+                  (⌜∀ σ2 , R2 σ2 → ub_lift (exec (S n) (e1, σ2)) φ (ε2 (e1, σ2))⌝)%I).
+        - iIntros (?). iPureIntro.
+          rewrite /= /get_active in Hα.
+          apply elem_of_elements, elem_of_dom in Hα as [bs Hα].
+
+          erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim _ _ _ _ _ Hα)); eauto.
+          apply (UB_mon_grading _ _
+                   (ε1 + (SeriesC (λ ρ : language.state prob_lang, language.state_step σ1 α ρ * ε2 (e1, ρ))))) => //.
+          eapply ub_lift_dbind_adv; eauto; [by destruct ε1|].
+          destruct Hε'' as [r Hr]; exists r.
+          intros a.
+          split; [by destruct (ε2 _) | by apply Hr].
         - iIntros (??). by iMod ("H" with "[//] [//]"). }
       iInduction (language.get_active σ1) as [| α] "IH"; [done|].
       rewrite big_orL_cons.
       iDestruct "H" as "[H | Ht]"; [done|].
       by iApply "IH".
-   - admit.
-  Admitted.
+  Qed.
 
   Theorem wp_refRcoupl_step_fupdN (e : expr) (σ : state) (ε : nonnegreal) n φ  :
     state_interp σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢

From 3e4f240395bd9ab6d7d46049809377d15b6e5c09 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Wed, 27 Dec 2023 11:53:53 -0500
Subject: [PATCH 10/37] cleanup adequacy

---
 theories/ub_logic/adequacy.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/ub_logic/adequacy.v b/theories/ub_logic/adequacy.v
index 004367ba..c07c3edc 100644
--- a/theories/ub_logic/adequacy.v
+++ b/theories/ub_logic/adequacy.v
@@ -106,8 +106,7 @@ Section adequacy.
           erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim _ _ _ _ _ Hα)); eauto.
           eapply ub_lift_dbind; eauto; [apply cond_nonneg | ].
           apply cond_nonneg.
-        - iIntros (??).
-          by iMod ("H" with "[//] [//]") as "W". }
+        - iIntros (??). by iMod ("H" with "[//] [//]"). }
       iInduction (language.get_active σ1) as [| α] "IH"; [done|].
       rewrite big_orL_cons.
       iDestruct "H" as "[H | Ht]"; [done|].

From 886dedf43b262d5cad866699669f88a00301b4c6 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Wed, 27 Dec 2023 14:22:39 -0500
Subject: [PATCH 11/37] complete exec_ub_bind

---
 theories/ub_logic/ub_weakestpre.v | 65 +++++++++++++++++++++++++------
 1 file changed, 53 insertions(+), 12 deletions(-)

diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 03781ff1..3b2a2b91 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -295,7 +295,7 @@ Section exec_ub.
                  with "[]") as "H"; last first.
     { iIntros (?). iApply ("H" $! (_, (_, _)) with "Hub [//]"). }
     iIntros "!#" ([ε' [? σ']]). rewrite /exec_ub_pre.
-    iIntros "[(% & % & % & % & % & H) | [ (% & % & % & (%r & %Hr) & % & % & H) | [H|H]]] %Hv'".
+    iIntros "[(% & % & % & % & % & H) | [ (% & % & % & (%r & %Hr) & % & % & H) | [H | H]]] %Hv'".
     - rewrite least_fixpoint_unfold.
       iLeft. simpl.
       iExists (λ '(e2, σ2), ∃ e2', e2 = K e2' ∧ R2 (e2', σ2)),_,_.
@@ -419,21 +419,62 @@ Section exec_ub.
         iSplit; [done|].
         iIntros. by iApply ("H" with "[//]").
       + iRight. by iApply ("IH" with "Ht").
-    - rewrite least_fixpoint_unfold /=.
+    - rewrite least_fixpoint_unfold; simpl.
       iRight; iRight; iRight.
-      iInduction (get_active σ') as [| l] "IH".
+      (* from above (combine?)*)
+      destruct (partial_inv_fun K) as (Kinv & HKinv).
+      assert (forall e e', Kinv e' = Some e -> K e = e') as HKinv1; [intros; by apply HKinv |].
+      assert (forall e e', Kinv e = None -> K e' ≠ e) as HKinv2; [intros; by apply HKinv |].
+      assert (forall e, Kinv (K e) = Some e) as HKinv3.
+      { intro e.
+        destruct (Kinv (K e)) eqn:H3.
+        - apply HKinv1 in H3. f_equal. by apply fill_inj.
+        - eapply (HKinv2 _ e) in H3. done. }
+      iInduction (get_active σ') as [| l ls] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
-      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hleq & %Hub & %Hlift & H)) | Ht]".
-      + iLeft.
-        iExists _,_,_.
-        iSplit; [done|].
-        (* is this still true??? I think I'll need to adapt the adv_comp case in more detail *)
-        iSplit; [admit|].
-        iSplit; [done|].
-        iIntros. admit.
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hub & %Hleq & %Hlift & H)) | Ht]".
+      + set (ε3 := (λ '(e,σ), from_option (λ e', ε2 (e',σ)) nnreal_zero (Kinv e))).
+        assert (forall e2 σ2, ε3 (K e2, σ2) = ε2 (e2, σ2)) as Haux.
+        { intros e2 σ2. rewrite /ε3 HKinv3 //. }
+        iLeft.
+        iExists R2,_,ε3.
+        iSplit.
+        { iPureIntro.
+          destruct Hub as [r Hr]; exists r.
+          intros (e&σ). rewrite /ε3.
+          destruct (Kinv e); simpl; try real_solver.
+          etrans; [ | eapply (Hr (e, σ)); eauto]. apply cond_nonneg.
+        }
+        iSplit; [| iSplit].
+        2: { iPureIntro; done. }
+        * iPureIntro.
+          etrans; [ | apply Hleq].
+          apply Rplus_le_compat_l.
+          apply SeriesC_le; last first.
+          { destruct Hub as [r Hr].
+            apply (ex_seriesC_le _ (λ ρ, (state_step σ' l ρ * r)%R)).
+            - intros; split.
+              + apply Rmult_le_pos; [apply pmf_pos | by destruct (ε2 _ )].
+              + apply Rmult_le_compat_l; auto; apply pmf_pos.
+            - apply ex_seriesC_scal_r.
+              apply pmf_ex_seriesC.
+          }
+          intros 𝜎; simpl.
+          split.
+          ** apply Rmult_le_pos; auto; apply cond_nonneg.
+          ** rewrite HKinv3 /=. lra.
+        * rewrite /Φ.
+          iIntros (σ).
+          iSpecialize ("H" $! σ).
+          iIntros "Hr"; iSpecialize ("H" with "Hr").
+          iMod "H"; iModIntro.
+          rewrite /ε3 HKinv3 /=.
+          iApply "H".
+          by simpl in Hv'.
       + iRight. by iApply ("IH" with "Ht").
-  Admitted.
+  Qed.
+
 
   Lemma exec_ub_prim_step e1 σ1 Z (ε : nonnegreal) :
     (∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗

From ef562ed56bf16baf2b6b16ae854b806eb1871f6d Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Thu, 28 Dec 2023 23:08:05 -0500
Subject: [PATCH 12/37] wip

---
 theories/ub_logic/ub_rules.v | 156 ++++++++++++++++++++++++++++++++++-
 1 file changed, 153 insertions(+), 3 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 09c38518..366be32e 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -392,6 +392,7 @@ Proof.
   solve_red.
   iApply exec_ub_adv_comp; simpl.
   iDestruct (ec_split_supply with "Hε Herr") as (ε3) "%Hε3".
+  (* ε3 is the amount of credit supply left outside of ε1 *)
   rewrite Hε3.
   set (foo := (λ (ρ : expr * state),
                 ε3 +
@@ -610,18 +611,167 @@ Proof.
 Qed.
 
 
-Lemma wp_presample_adv_comp (N : nat) 𝛼 ns z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
+
+
+Definition compute_ε2_in_state (ρ : expr * state) N z (ε2 : fin (S N) -> nonnegreal) (_ : TCEq N (Z.to_nat z)) : nonnegreal.
+refine(
+  match ρ with
+  | (Val (LitV (LitInt n)), σ) =>
+      if bool_decide (0 <= n)%Z
+      then match (lt_dec (Z.to_nat n) (S (Z.to_nat z))) with
+             | left H => ε2 (@Fin.of_nat_lt (Z.to_nat n) _ _)
+             | _ => nnreal_zero
+            end
+      else nnreal_zero
+  | _ => nnreal_zero
+  end).
+  eapply Nat.le_trans.
+  - apply Nat.le_succ_l, H.
+  - apply Nat.eq_le_incl, eq_S. symmetry. by apply TCEq_eq.
+Defined.
+
+Lemma SeriesC_singleton_dependent `{Countable A} (a : A) (v : A -> nonnegreal) :
+  SeriesC (λ n, if bool_decide (n = a) then v n else nnreal_zero) = nonneg (v a).
+Proof. (* proven in other branch *)
+Admitted.
+
+
+
+Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
   to_val e = None →
   (∀ σ', reducible e σ') →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
-  ▷ 𝛼 ↪ (N; ns) ∗
+  ▷ α ↪ (N; ns) ∗
   € ε1 ∗
-  (∀ (n : fin (S N)), € (ε2 n) ∗ 𝛼 ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
+  (∀ (n : fin (S N)), € (ε2 n) ∗ α ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
+  iIntros (? Hred Hσ_red Hsum) "(Hα & Hε & Hwp)".
+  iApply wp_lift_step_fupd_exec_ub; [done|].
+  iIntros (σ1 ε_now) "[Hσ_interp Hε_interp]".
+  iApply fupd_mask_intro; [set_solver|].
+  iIntros "Hclose'".
+  iSplitR; [auto|].
+  iApply (exec_ub_state_adv_comp' α); simpl.
+  { (* should be able to prove α is active since we have α ↪ _ right? *) admit. }
+  (* split supply by ε1*)
+  iDestruct (ec_split_supply with "Hε_interp Hε") as (ε3) "%Hε3".
+  rewrite Hε3.
+
+  (* R: predicate should hold iff tapes σ' at α is ns ++ [n] *)
+
+  iExists (fun σ' : state => exists n : fin (S N), σ' = (state_upd_tapes <[α:=(N; ns ++ [n]) : tape]> σ1)).
+  (* ε2: lifted version of ε2 to states *)
+  iExists (fun ρ => (ε3 + compute_ε2_in_state ρ N z ε2 H)%NNR).
+
+  (* upper bound *)
+  iSplit.
+  { iPureIntro. exists (ε3 + (nnreal_nat (S N)) * ε1)%NNR.
+    intros [e' σ'].
+    apply Rplus_le_compat_l.
+    rewrite /compute_ε2_in_state.
+    assert (H' : (0 <= (S N)* ε1)%R).
+    { apply Rmult_le_pos.
+      - apply pos_INR.
+      - by destruct ε1. }
+    destruct e'; try apply H'.
+    destruct v; try apply H'.
+    destruct l; try apply H'.
+    case_bool_decide; try apply H'.
+    destruct (lt_dec _ _); try apply H'.
+    remember (nat_to_fin _) as F.
+    Opaque nnreal_nat. simpl.
+    rewrite -Hsum -SeriesC_scal_l.
+    rewrite -(SeriesC_singleton_dependent F ε2).
+    apply SeriesC_le.
+    - intros.
+      case_bool_decide.
+      (* could be a lot simpler *)
+      + split.
+        * by destruct (ε2 _).
+        * Set Printing Coercions.
+          rewrite -(Rmult_1_l (ε2 n0)) -Rmult_assoc -Rmult_assoc.
+          apply Rmult_le_compat_r.
+          ** by destruct (ε2 _); simpl.
+          ** rewrite Rmult_1_r.
+             rewrite /Rdiv Rmult_comm Rmult_1_l.
+             Transparent nnreal_nat. simpl.
+             rewrite Rinv_l; try lra.
+             destruct N; try lra.
+             rewrite S_INR.
+             rewrite /not; intros.
+             assert (K : (0 <= INR N)%R) by apply pos_INR.
+             lra. (* yikes lol *)
+      + split; simpl; try lra.
+        rewrite Rmult_assoc Rmult_1_l -Rmult_assoc.
+        rewrite Rinv_r.
+          * apply Rmult_le_pos; try lra.
+            by destruct (ε2 _); simpl.
+          * rewrite /not; intros.
+            assert (K : (0 <= INR N)%R) by apply pos_INR.
+            destruct N.
+            ** lra.
+            ** lra.
+    - apply ex_seriesC_finite.
+  }
+
+  iSplit.
+  { iPureIntro.
+    rewrite /compute_ε2_in_state /=.
+    setoid_rewrite Rmult_plus_distr_l.
+    admit. (* what am I even using ε3 for again??? *)
+  }
+
+  assert (Htape_state: tapes σ1 !! α = Some (N; ns)) by admit.
+
+  (* lifted lookup on tapes *)
+  iSplit.
+  {
+    iPureIntro.
+    eapply UB_mon_pred; last first.
+    - apply ub_lift_state. apply Htape_state.
+    - done.
+  }
+
+  (* finally update the wp *)
+  iIntros ((e2 & σ2)) "[%n Hn1]"; simplify_eq.
+  (* I should be able to use Hwp here, since we've now chosen a sample *)
+  (* I need to get rid of that exec modality somehow, anyways. *)
+  iSpecialize ("Hwp" $! n).
+  rewrite /compute_ε2_in_state /=.
+  admit.
 Admitted.
 
+(*
 
+  iSplit.
+  iIntros ((e2 & σ2)) "%H".
+  destruct H as (n & Hn1); simplify_eq.
+  rewrite /foo /=.
+  rewrite bool_decide_eq_true_2; last first.
+  {
+    by zify.
+  }
+  case_match.
+  2:{
+    destruct n0.
+    rewrite Nat2Z.id.
+    apply fin_to_nat_lt.
+  }
+  iMod (ec_decrease_supply with "Hε Herr") as "Hε2".
+  do 2 iModIntro.
+  iMod "Hclose'".
+  iFrame.
+  iMod (ec_increase_supply _ (ε2 (nat_to_fin l)) with "Hε2") as "[Hε2 Hfoo]".
+  iFrame. iModIntro. wp_pures.
+  iModIntro. iApply "HΨ".
+  assert (nat_to_fin l = n) as ->; [|done].
+  apply fin_to_nat_inj.
+  rewrite fin_to_nat_to_fin.
+  rewrite Nat2Z.id.
+  reflexivity.
+Admitted.
+*)
 
 End rules.

From c976b36d1bdb377eebb9d5cb5bfff29e0ca56038 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 29 Dec 2023 08:30:41 -0500
Subject: [PATCH 13/37] wip

---
 theories/ub_logic/ub_rules.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 366be32e..9d933918 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -632,9 +632,7 @@ Defined.
 
 Lemma SeriesC_singleton_dependent `{Countable A} (a : A) (v : A -> nonnegreal) :
   SeriesC (λ n, if bool_decide (n = a) then v n else nnreal_zero) = nonneg (v a).
-Proof. (* proven in other branch *)
-Admitted.
-
+Proof. (* proven in other branch *) Admitted.
 
 
 Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :

From 9c5d45d34063f9f10eced2f590b318df9c04eb89 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Sat, 30 Dec 2023 10:25:16 -0500
Subject: [PATCH 14/37] prove mean constraint implies upper bound property

---
 theories/ub_logic/ub_rules.v | 41 +++++++++++++++++++++++++++++++-----
 1 file changed, 36 insertions(+), 5 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 9d933918..046fac2e 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -377,6 +377,40 @@ Proof.
   done.
 Qed.
 
+(* FIXME: merge me from other branch *)
+Lemma SeriesC_singleton_dependent `{Countable A} (a : A) (v : A -> nonnegreal) :
+  SeriesC (λ n, if bool_decide (n = a) then v n else nnreal_zero) = nonneg (v a).
+Proof.  Admitted.
+
+Lemma mean_constraint_ub (N : nat) (ε2 : fin (S N) -> nonnegreal) ε1 :
+  SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) ->
+  (exists r, ∀ n, (ε2 n <= r)%R).
+Proof.
+  intros Hsum.
+  exists (nnreal_nat (S N) * ε1)%NNR.
+  intros n.
+  Opaque nnreal_nat.
+  rewrite /= -Hsum.
+  rewrite SeriesC_scal_l -Rmult_assoc -(Rmult_1_l (nonneg (ε2 _))).
+  apply Rmult_le_compat; try lra.
+  - by apply cond_nonneg.
+  - rewrite /Rdiv Rmult_1_l.
+    rewrite /= Rinv_r; try lra.
+    Transparent nnreal_nat.
+    rewrite /nnreal_nat.
+    (* simpl does too much here and I can't figure out how to stop it *)
+    replace (nonneg {| nonneg := INR (S N); cond_nonneg := _ |}) with (INR (S N)); [| by simpl ].
+    apply not_0_INR.
+    auto.
+  - rewrite -(SeriesC_singleton_dependent _ ε2).
+    apply SeriesC_le.
+    + intros n'.
+      assert (H : (0 <= (nonneg (ε2 n')))%R) by apply cond_nonneg.
+      rewrite /nnreal_zero /=.
+      case_bool_decide; try lra.
+    + apply ex_seriesC_finite.
+Qed.
+
 
 Lemma wp_couple_rand_adv_comp (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
@@ -392,7 +426,7 @@ Proof.
   solve_red.
   iApply exec_ub_adv_comp; simpl.
   iDestruct (ec_split_supply with "Hε Herr") as (ε3) "%Hε3".
-  (* ε3 is the amount of credit supply left outside of ε1 *)
+  (* ε3 is the amount of credit supply left outside of ε1 (?) *)
   rewrite Hε3.
   set (foo := (λ (ρ : expr * state),
                 ε3 +
@@ -630,9 +664,6 @@ refine(
   - apply Nat.eq_le_incl, eq_S. symmetry. by apply TCEq_eq.
 Defined.
 
-Lemma SeriesC_singleton_dependent `{Countable A} (a : A) (v : A -> nonnegreal) :
-  SeriesC (λ n, if bool_decide (n = a) then v n else nnreal_zero) = nonneg (v a).
-Proof. (* proven in other branch *) Admitted.
 
 
 Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
@@ -645,7 +676,7 @@ Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 :
   (∀ (n : fin (S N)), € (ε2 n) ∗ α ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? Hred Hσ_red Hsum) "(Hα & Hε & Hwp)".
+  iIntros (-> Hred Hσ_red Hsum) "(Hα & Hε & Hwp)".
   iApply wp_lift_step_fupd_exec_ub; [done|].
   iIntros (σ1 ε_now) "[Hσ_interp Hε_interp]".
   iApply fupd_mask_intro; [set_solver|].

From c1a897d2811d0b878f34f424bbac70a7bef31b8b Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Sat, 30 Dec 2023 10:50:34 -0500
Subject: [PATCH 15/37] simplify upper bound proof

---
 theories/ub_logic/ub_rules.v | 70 ++++++++++++------------------------
 1 file changed, 22 insertions(+), 48 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 046fac2e..278a130a 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -382,7 +382,7 @@ Lemma SeriesC_singleton_dependent `{Countable A} (a : A) (v : A -> nonnegreal) :
   SeriesC (λ n, if bool_decide (n = a) then v n else nnreal_zero) = nonneg (v a).
 Proof.  Admitted.
 
-Lemma mean_constraint_ub (N : nat) (ε2 : fin (S N) -> nonnegreal) ε1 :
+Lemma mean_constraint_ub (N : nat) ε1 (ε2 : fin (S N) -> nonnegreal) :
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) ->
   (exists r, ∀ n, (ε2 n <= r)%R).
 Proof.
@@ -412,6 +412,10 @@ Proof.
 Qed.
 
 
+Lemma match_nonneg_coercions (n : nonnegreal) : NNRbar_to_real (NNRbar.Finite n) = nonneg n.
+Proof. by simpl. Qed.
+
+
 Lemma wp_couple_rand_adv_comp (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
   (exists r, ∀ n, (ε2 n <= r)%R) →
@@ -689,60 +693,30 @@ Proof.
   rewrite Hε3.
 
   (* R: predicate should hold iff tapes σ' at α is ns ++ [n] *)
-
-  iExists (fun σ' : state => exists n : fin (S N), σ' = (state_upd_tapes <[α:=(N; ns ++ [n]) : tape]> σ1)).
+  iExists (fun σ' : state => exists n : fin _, σ' = (state_upd_tapes <[α:=(_; ns ++ [n]) : tape]> σ1)).
   (* ε2: lifted version of ε2 to states *)
-  iExists (fun ρ => (ε3 + compute_ε2_in_state ρ N z ε2 H)%NNR).
+  iExists (fun ρ => (ε3 + compute_ε2_in_state ρ _ z ε2 _)%NNR).
 
   (* upper bound *)
   iSplit.
-  { iPureIntro. exists (ε3 + (nnreal_nat (S N)) * ε1)%NNR.
+  { iPureIntro.
+    destruct (mean_constraint_ub _ _ _ Hsum) as [r Hr].
+    assert (Hr_nnonneg : (0 <= r)%R).
+    { eapply Rle_trans; [|apply (Hr 0%fin)].
+      rewrite match_nonneg_coercions.
+      apply cond_nonneg. }
+    eexists (ε3 + r)%R.
     intros [e' σ'].
     apply Rplus_le_compat_l.
     rewrite /compute_ε2_in_state.
-    assert (H' : (0 <= (S N)* ε1)%R).
-    { apply Rmult_le_pos.
-      - apply pos_INR.
-      - by destruct ε1. }
-    destruct e'; try apply H'.
-    destruct v; try apply H'.
-    destruct l; try apply H'.
-    case_bool_decide; try apply H'.
-    destruct (lt_dec _ _); try apply H'.
-    remember (nat_to_fin _) as F.
-    Opaque nnreal_nat. simpl.
-    rewrite -Hsum -SeriesC_scal_l.
-    rewrite -(SeriesC_singleton_dependent F ε2).
-    apply SeriesC_le.
-    - intros.
-      case_bool_decide.
-      (* could be a lot simpler *)
-      + split.
-        * by destruct (ε2 _).
-        * Set Printing Coercions.
-          rewrite -(Rmult_1_l (ε2 n0)) -Rmult_assoc -Rmult_assoc.
-          apply Rmult_le_compat_r.
-          ** by destruct (ε2 _); simpl.
-          ** rewrite Rmult_1_r.
-             rewrite /Rdiv Rmult_comm Rmult_1_l.
-             Transparent nnreal_nat. simpl.
-             rewrite Rinv_l; try lra.
-             destruct N; try lra.
-             rewrite S_INR.
-             rewrite /not; intros.
-             assert (K : (0 <= INR N)%R) by apply pos_INR.
-             lra. (* yikes lol *)
-      + split; simpl; try lra.
-        rewrite Rmult_assoc Rmult_1_l -Rmult_assoc.
-        rewrite Rinv_r.
-          * apply Rmult_le_pos; try lra.
-            by destruct (ε2 _); simpl.
-          * rewrite /not; intros.
-            assert (K : (0 <= INR N)%R) by apply pos_INR.
-            destruct N.
-            ** lra.
-            ** lra.
-    - apply ex_seriesC_finite.
+    destruct e'; try (simpl; lra).
+    destruct v; try (simpl; lra).
+    destruct l; try (simpl; lra).
+    case_bool_decide; try (simpl; lra).
+    destruct (lt_dec _ _); try (simpl; lra).
+    remember (nat_to_fin _) as n'.
+    rewrite -match_nonneg_coercions.
+    apply (Hr n').
   }
 
   iSplit.

From c8eb5b065fc8240a77f0bfd8303f75fae4eee095 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Sat, 30 Dec 2023 13:30:33 -0500
Subject: [PATCH 16/37] checkpoint: before chaning exec_ub again

---
 theories/ub_logic/ub_rules.v      | 99 ++++++++++++++++++++++++-------
 theories/ub_logic/ub_weakestpre.v |  4 +-
 2 files changed, 81 insertions(+), 22 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 278a130a..aa41ed0f 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -669,32 +669,49 @@ refine(
 Defined.
 
 
+Lemma compute_ε2_in_state_expr e σ N z ε2 H :
+  to_val e = None ->
+  compute_ε2_in_state (e, σ) N z ε2 H = nnreal_zero.
+Proof.
+  intros; rewrite /compute_ε2_in_state; simpl.
+  case_match; auto.
+  simplify_eq.
+Qed.
+
 
 Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
   to_val e = None →
   (∀ σ', reducible e σ') →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
-  ▷ α ↪ (N; ns) ∗
+  α ↪ (N; ns) ∗
   € ε1 ∗
   (∀ (n : fin (S N)), € (ε2 n) ∗ α ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (-> Hred Hσ_red Hsum) "(Hα & Hε & Hwp)".
   iApply wp_lift_step_fupd_exec_ub; [done|].
-  iIntros (σ1 ε_now) "[Hσ_interp Hε_interp]".
+  iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
+  iDestruct (ghost_map_lookup with "Htapes Hα") as %Hlookup.
+  iDestruct (ec_supply_bound with "Hε_supply Hε") as %Hε1_ub.
+
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
   iSplitR; [auto|].
   iApply (exec_ub_state_adv_comp' α); simpl.
-  { (* should be able to prove α is active since we have α ↪ _ right? *) admit. }
-  (* split supply by ε1*)
-  iDestruct (ec_split_supply with "Hε_interp Hε") as (ε3) "%Hε3".
-  rewrite Hε3.
+  { rewrite /get_active.
+    by apply elem_of_list_In, elem_of_list_In, elem_of_elements, elem_of_dom. }
+
+  (* split supply by ε1 (why? is this necessary since I'm not weakening the amount of
+     credit in my exec_ub_state_adv_comp'? )
+     I guess we could be weakening the supply in any case? confusing. *)
+  (* is it because the second obligation needs exact equality? *)
+  (* I tu*)
+  iDestruct (ec_split_supply with "Hε_supply Hε") as (ε3) "%Hε_supply".
+  rewrite Hε_supply.
 
   (* R: predicate should hold iff tapes σ' at α is ns ++ [n] *)
   iExists (fun σ' : state => exists n : fin _, σ' = (state_upd_tapes <[α:=(_; ns ++ [n]) : tape]> σ1)).
-  (* ε2: lifted version of ε2 to states *)
   iExists (fun ρ => (ε3 + compute_ε2_in_state ρ _ z ε2 _)%NNR).
 
   (* upper bound *)
@@ -705,7 +722,7 @@ Proof.
     { eapply Rle_trans; [|apply (Hr 0%fin)].
       rewrite match_nonneg_coercions.
       apply cond_nonneg. }
-    eexists (ε3 + r)%R.
+    exists (ε3 + r)%R.
     intros [e' σ'].
     apply Rplus_le_compat_l.
     rewrite /compute_ε2_in_state.
@@ -722,28 +739,70 @@ Proof.
   iSplit.
   { iPureIntro.
     rewrite /compute_ε2_in_state /=.
-    setoid_rewrite Rmult_plus_distr_l.
-    admit. (* what am I even using ε3 for again??? *)
-  }
+    (* so we have this gigantic sum over all states
+       the state_step factor should eliminate all of those except S N of them
+       which are of the form ρ with a new value on α
+
+
+       this gets us the factor of (1/(S N))
+
+       the second factor is nonzero only in the cases where
+       e is the value #n with 0 ≤ n, in which case it becomes
+       ε2
 
-  assert (Htape_state: tapes σ1 !! α = Some (N; ns)) by admit.
+      by Hsum, the total is ε1
+
+      then we need ε1 ≤ ε_now, which we can get without splitting into
+      ε1 and ε3 with ec_supply_bounnd (above)
+
+     *)
+
+    admit.
+  }
 
   (* lifted lookup on tapes *)
   iSplit.
   {
     iPureIntro.
     eapply UB_mon_pred; last first.
-    - apply ub_lift_state. apply Htape_state.
+    - apply ub_lift_state. apply Hlookup.
     - done.
   }
 
-  (* finally update the wp *)
-  iIntros ((e2 & σ2)) "[%n Hn1]"; simplify_eq.
-  (* I should be able to use Hwp here, since we've now chosen a sample *)
-  (* I need to get rid of that exec modality somehow, anyways. *)
-  iSpecialize ("Hwp" $! n).
-  rewrite /compute_ε2_in_state /=.
-  admit.
+  iIntros ((heap2 & tapes2)) "[%sample %Hsample]"; simplify_eq.
+  rewrite compute_ε2_in_state_expr; auto. (* sus *)
+
+
+  (* decrease the supply to ε1 (to get rid of the € ε1) and then increase it to ε2.
+     the decrease is probably not needed lol *)
+  iDestruct (ec_split_supply with "Hε_supply Hε") as (εrem) "%Hεrem".
+  simplify_eq.
+  iMod (ec_decrease_supply with "Hε_supply Hε") as "Hε_supply".
+  iMod (ec_increase_supply _ (ε2 sample) with "Hε_supply") as "[Hε_supply Hε]".
+  iSpecialize ("Hwp" $! sample).
+  (* FIXME I'm getting weird unification errors I don't understand so I'll just
+    curry Hwp by admits *)
+  (* iMod (ghost_map_update ((Z.to_nat z; ns ++ [sample]) : tape) with "Htapes Hα") as "[Htapes H𝛼]". *)
+  iMod (ghost_map_update ((Z.to_nat z; ns ++ [sample]) : tape) with "Htapes Hα") as "[Htapes Hα]".
+
+
+  rewrite ub_wp_unfold /ub_wp_pre.
+  (* then we should be able to specialize using the updated ghost state.. *)
+  iAssert (⌜ (common.language.to_val e) = None ⌝)%I as "%X". { auto. }
+  rewrite X; clear X.
+
+  iAssert (state_interp (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample]) : tape]> σ1)) with "[Hheap Htapes]" as "Hσ1".
+  { rewrite /state_interp; iFrame. }
+  iAssert (err_interp (εrem + ε2 sample)%NNR ) with "[Hε_supply]" as "Hε_supply".
+  { rewrite /err_interp; iFrame. }
+  iSpecialize ("Hwp" with "[Hε Hα]").
+  {  iFrame. }
+  iSpecialize ("Hwp" $! {| heap := heap2; tapes := tapes2 |} (εrem + ε2 sample)%NNR).
+  iSpecialize ("Hwp" with "[Hσ1 Hε_supply]").
+  { rewrite Hsample. iFrame. }
+
+  (* oh no-- the nnreal_zero is wrong! it needs to be at least (εrem + r) *)
+
 Admitted.
 
 (*
diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 3b2a2b91..66408d6c 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -553,7 +553,7 @@ Section exec_ub.
     (α ∈ get_active σ1 ->
      (∃ R (ε2 : cfg Λ -> nonnegreal),
         ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
-        ⌜ (SeriesC (λ ρ, (state_step σ1 α ρ) * ε2 (e1, ρ)) = ε)%R ⌝ ∗
+        ⌜ (SeriesC (λ ρ, (state_step σ1 α ρ) * ε2 (e1, ρ)) <= ε)%R ⌝ ∗
         ⌜ub_lift (state_step σ1 α) R nnreal_zero⌝ ∗
         ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z (ε2 (e1, σ2)))
       ⊢ exec_ub e1 σ1 Z ε)%I.
@@ -565,7 +565,7 @@ Section exec_ub.
     iExists _,nnreal_zero,_.
     iSplit; [auto|].
     iSplit.
-    { iPureIntro. apply Req_le. rewrite Hε /=. lra. }
+    { iPureIntro. by rewrite /= Rplus_0_l. }
     iSplit; [done|done].
   Qed.
 

From 860f3c5c2dba45ee76e386098a2ce910a9c1a7bb Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Sat, 30 Dec 2023 13:34:00 -0500
Subject: [PATCH 17/37] update to compile

---
 theories/ub_logic/ub_rules.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index aa41ed0f..67f2ec52 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -775,8 +775,6 @@ Proof.
 
   (* decrease the supply to ε1 (to get rid of the € ε1) and then increase it to ε2.
      the decrease is probably not needed lol *)
-  iDestruct (ec_split_supply with "Hε_supply Hε") as (εrem) "%Hεrem".
-  simplify_eq.
   iMod (ec_decrease_supply with "Hε_supply Hε") as "Hε_supply".
   iMod (ec_increase_supply _ (ε2 sample) with "Hε_supply") as "[Hε_supply Hε]".
   iSpecialize ("Hwp" $! sample).
@@ -793,6 +791,8 @@ Proof.
 
   iAssert (state_interp (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample]) : tape]> σ1)) with "[Hheap Htapes]" as "Hσ1".
   { rewrite /state_interp; iFrame. }
+
+  (*
   iAssert (err_interp (εrem + ε2 sample)%NNR ) with "[Hε_supply]" as "Hε_supply".
   { rewrite /err_interp; iFrame. }
   iSpecialize ("Hwp" with "[Hε Hα]").
@@ -800,6 +800,7 @@ Proof.
   iSpecialize ("Hwp" $! {| heap := heap2; tapes := tapes2 |} (εrem + ε2 sample)%NNR).
   iSpecialize ("Hwp" with "[Hσ1 Hε_supply]").
   { rewrite Hsample. iFrame. }
+*)
 
   (* oh no-- the nnreal_zero is wrong! it needs to be at least (εrem + r) *)
 

From cc86a36e05c5217144d43c9177084917f12845d2 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Sat, 30 Dec 2023 15:44:10 -0500
Subject: [PATCH 18/37] full sketch of wp_presample_adv_comp

---
 theories/ub_logic/ub_rules.v | 131 ++++++++++++++++++-----------------
 1 file changed, 67 insertions(+), 64 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 67f2ec52..eab06efb 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -1,5 +1,5 @@
 (** * Union bound rules  *)
-From stdpp Require Import namespaces.
+From stdpp Require Import namespaces finite.
 From iris.proofmode Require Import proofmode.
 From clutch.prelude Require Import stdpp_ext.
 From clutch.prob_lang Require Import notation tactics metatheory.
@@ -650,7 +650,7 @@ Qed.
 
 
 
-
+(* old (broken?) version *)
 Definition compute_ε2_in_state (ρ : expr * state) N z (ε2 : fin (S N) -> nonnegreal) (_ : TCEq N (Z.to_nat z)) : nonnegreal.
 refine(
   match ρ with
@@ -679,6 +679,27 @@ Proof.
 Qed.
 
 
+Check (fun (s : state) => s.(tapes)).
+Check (fun α z ns sample=> (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample]) : tape]> )).
+Check (fun σ σ' α z ns N => (exists s : fin _, σ' = (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s]) : tape]> σ))).
+Check (fun σ σ' α z ns N =>
+            match exists_dec (fun s : fin _ => σ' = (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s]) : tape]> σ)) with
+                | left H => _ H
+                | right H => nnreal_zero
+              end).
+
+(* I'll admit this for now to see if the rest of the proof works  *)
+
+(* really this should not depend on the expr at all :/*)
+
+Definition compute_ε2 (σ : state) (ρ : cfg) α N ns (ε2 : fin (S N) -> nonnegreal) : nonnegreal :=
+  match finite.find (fun s => state_upd_tapes <[α:=(N; ns ++ [s]) : tape]> σ = snd ρ) with
+    | Some s => ε2 s
+    | None => nnreal_zero
+  end.
+
+
+
 Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
   to_val e = None →
@@ -712,7 +733,7 @@ Proof.
 
   (* R: predicate should hold iff tapes σ' at α is ns ++ [n] *)
   iExists (fun σ' : state => exists n : fin _, σ' = (state_upd_tapes <[α:=(_; ns ++ [n]) : tape]> σ1)).
-  iExists (fun ρ => (ε3 + compute_ε2_in_state ρ _ z ε2 _)%NNR).
+  iExists (fun ρ => (ε3 + compute_ε2 σ1 ρ α _ ns ε2)%NNR).
 
   (* upper bound *)
   iSplit.
@@ -725,15 +746,13 @@ Proof.
     exists (ε3 + r)%R.
     intros [e' σ'].
     apply Rplus_le_compat_l.
-    rewrite /compute_ε2_in_state.
-    destruct e'; try (simpl; lra).
-    destruct v; try (simpl; lra).
-    destruct l; try (simpl; lra).
-    case_bool_decide; try (simpl; lra).
-    destruct (lt_dec _ _); try (simpl; lra).
-    remember (nat_to_fin _) as n'.
-    rewrite -match_nonneg_coercions.
-    apply (Hr n').
+    destruct_decide
+      (exists_dec (fun s : fin _ => σ' = (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s]) : tape]> σ1))).
+    + destruct H as [s Hs].
+      rewrite /compute_ε2.
+      (* should be provale from here *)
+      admit.
+    + admit.
   }
 
   iSplit.
@@ -743,20 +762,14 @@ Proof.
        the state_step factor should eliminate all of those except S N of them
        which are of the form ρ with a new value on α
 
+       so the series is reduced to S N terms, and each _should_ be 1/S N.
 
-       this gets us the factor of (1/(S N))
-
-       the second factor is nonzero only in the cases where
-       e is the value #n with 0 ≤ n, in which case it becomes
-       ε2
-
-      by Hsum, the total is ε1
+       then for each state, the second term will be (ε2 s)
 
-      then we need ε1 ≤ ε_now, which we can get without splitting into
-      ε1 and ε3 with ec_supply_bounnd (above)
+       by Hsum, the total is ε1
 
+       conclude by 0 <= ε3
      *)
-
     admit.
   }
 
@@ -770,17 +783,25 @@ Proof.
   }
 
   iIntros ((heap2 & tapes2)) "[%sample %Hsample]"; simplify_eq.
-  rewrite compute_ε2_in_state_expr; auto. (* sus *)
-
-
+  (* we should be able to get ε2 from compute_ε2 now *)
+  replace (compute_ε2 _ _ _ _ _ _) with (ε2 sample); last first.
+  { rewrite Hsample /compute_ε2 /=.
+    remember (λ s : fin (S (Z.to_nat z)),
+         state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s])]> σ1 = state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample])]> σ1)
+        as F.
+    assert (FS: F sample).
+    { rewrite HeqF /=; done. }
+    assert (HD:  ∀ x : fin (S (Z.to_nat z)), Decision (F x) ).
+    { intros. rewrite HeqF. admit. (* ok *)}
+    destruct (@find_is_Some _ _ _ F HD sample FS) as [s' [Hs' Fs']].
+    (* fixable *)
+    admit.
+  }
   (* decrease the supply to ε1 (to get rid of the € ε1) and then increase it to ε2.
-     the decrease is probably not needed lol *)
+     the decrease is probably not needed I think? *)
   iMod (ec_decrease_supply with "Hε_supply Hε") as "Hε_supply".
   iMod (ec_increase_supply _ (ε2 sample) with "Hε_supply") as "[Hε_supply Hε]".
   iSpecialize ("Hwp" $! sample).
-  (* FIXME I'm getting weird unification errors I don't understand so I'll just
-    curry Hwp by admits *)
-  (* iMod (ghost_map_update ((Z.to_nat z; ns ++ [sample]) : tape) with "Htapes Hα") as "[Htapes H𝛼]". *)
   iMod (ghost_map_update ((Z.to_nat z; ns ++ [sample]) : tape) with "Htapes Hα") as "[Htapes Hα]".
 
 
@@ -792,49 +813,31 @@ Proof.
   iAssert (state_interp (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample]) : tape]> σ1)) with "[Hheap Htapes]" as "Hσ1".
   { rewrite /state_interp; iFrame. }
 
-  (*
-  iAssert (err_interp (εrem + ε2 sample)%NNR ) with "[Hε_supply]" as "Hε_supply".
+  iAssert (err_interp (ε3 + ε2 sample)%NNR ) with "[Hε_supply]" as "Hε_supply".
   { rewrite /err_interp; iFrame. }
   iSpecialize ("Hwp" with "[Hε Hα]").
   {  iFrame. }
-  iSpecialize ("Hwp" $! {| heap := heap2; tapes := tapes2 |} (εrem + ε2 sample)%NNR).
+  iSpecialize ("Hwp" $! {| heap := heap2; tapes := tapes2 |} (ε3 + ε2 sample)%NNR).
   iSpecialize ("Hwp" with "[Hσ1 Hε_supply]").
   { rewrite Hsample. iFrame. }
-*)
 
-  (* oh no-- the nnreal_zero is wrong! it needs to be at least (εrem + r) *)
+  clear.
 
-Admitted.
+  remember (exec_ub e {| heap := heap2; tapes := tapes2 |}
+              (λ (ε0 : nonnegreal) '(e2, σ2), ▷ (|={∅,E}=> state_interp σ2 ∗ err_interp ε0 ∗ WP e2 @ E {{ v, Φ v }}))
+              (ε3 + ε2 sample)%NNR)%I as EUB.
+  rewrite -HeqEUB.
 
-(*
+  iAssert (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝ ={∅,E}=∗ emp)%I with "[Hclose']" as "W".
+  { iIntros. iFrame. }
 
-  iSplit.
-  iIntros ((e2 & σ2)) "%H".
-  destruct H as (n & Hn1); simplify_eq.
-  rewrite /foo /=.
-  rewrite bool_decide_eq_true_2; last first.
-  {
-    by zify.
-  }
-  case_match.
-  2:{
-    destruct n0.
-    rewrite Nat2Z.id.
-    apply fin_to_nat_lt.
-  }
-  iMod (ec_decrease_supply with "Hε Herr") as "Hε2".
-  do 2 iModIntro.
-  iMod "Hclose'".
-  iFrame.
-  iMod (ec_increase_supply _ (ε2 (nat_to_fin l)) with "Hε2") as "[Hε2 Hfoo]".
-  iFrame. iModIntro. wp_pures.
-  iModIntro. iApply "HΨ".
-  assert (nat_to_fin l = n) as ->; [|done].
-  apply fin_to_nat_inj.
-  rewrite fin_to_nat_to_fin.
-  rewrite Nat2Z.id.
-  reflexivity.
-Admitted.
-*)
+  iPoseProof (fupd_trans_frame E ∅ E EUB (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝))%I as "Z".
+  iSpecialize ("Z" with "[W Hwp]").
+  {  iFrame. }
+  iApply fupd_mask_mono; last done.
 
+  (* oh damn! this can't be proven. can we only take this step when E = ∅? *)
+  admit.
+
+Admitted.
 End rules.

From 929b5026da38064f2ddedd90ecc1bf9f0b01d56b Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Tue, 2 Jan 2024 11:15:51 -0500
Subject: [PATCH 19/37] progress on adv composition for tapes

---
 theories/ub_logic/ub_rules.v | 131 +++++++++++++++++------------------
 1 file changed, 65 insertions(+), 66 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index eab06efb..1650c7e7 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -701,6 +701,7 @@ Definition compute_ε2 (σ : state) (ρ : cfg) α N ns (ε2 : fin (S N) -> nonne
 
 
 Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
+  E = ∅ -> (* can this really only be proven when E = ∅ or can we improve this? *)
   TCEq N (Z.to_nat z) →
   to_val e = None →
   (∀ σ', reducible e σ') →
@@ -710,30 +711,25 @@ Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 :
   (∀ (n : fin (S N)), € (ε2 n) ∗ α ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (-> Hred Hσ_red Hsum) "(Hα & Hε & Hwp)".
+  iIntros (? -> Hred Hσ_red Hsum) "(Hα & Hε & Hwp)".
   iApply wp_lift_step_fupd_exec_ub; [done|].
   iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
   iDestruct (ghost_map_lookup with "Htapes Hα") as %Hlookup.
   iDestruct (ec_supply_bound with "Hε_supply Hε") as %Hε1_ub.
-
   iApply fupd_mask_intro; [set_solver|].
-  iIntros "Hclose'".
+  iIntros "Hclose".
   iSplitR; [auto|].
   iApply (exec_ub_state_adv_comp' α); simpl.
   { rewrite /get_active.
-    by apply elem_of_list_In, elem_of_list_In, elem_of_elements, elem_of_dom. }
-
-  (* split supply by ε1 (why? is this necessary since I'm not weakening the amount of
-     credit in my exec_ub_state_adv_comp'? )
-     I guess we could be weakening the supply in any case? confusing. *)
-  (* is it because the second obligation needs exact equality? *)
-  (* I tu*)
-  iDestruct (ec_split_supply with "Hε_supply Hε") as (ε3) "%Hε_supply".
+    apply elem_of_list_In, elem_of_list_In, elem_of_elements, elem_of_dom.
+    done. }
+  iDestruct (ec_split_supply with "Hε_supply Hε") as (ε_rem) "%Hε_supply".
   rewrite Hε_supply.
 
   (* R: predicate should hold iff tapes σ' at α is ns ++ [n] *)
-  iExists (fun σ' : state => exists n : fin _, σ' = (state_upd_tapes <[α:=(_; ns ++ [n]) : tape]> σ1)).
-  iExists (fun ρ => (ε3 + compute_ε2 σ1 ρ α _ ns ε2)%NNR).
+  iExists
+    (fun σ' : state => exists n : fin _, σ' = (state_upd_tapes <[α:=(_; ns ++ [n]) : tape]> σ1)),
+    (fun ρ => (ε_rem + compute_ε2 σ1 ρ α _ ns ε2)%NNR).
 
   (* upper bound *)
   iSplit.
@@ -743,16 +739,11 @@ Proof.
     { eapply Rle_trans; [|apply (Hr 0%fin)].
       rewrite match_nonneg_coercions.
       apply cond_nonneg. }
-    exists (ε3 + r)%R.
+    exists (ε_rem + r)%R.
     intros [e' σ'].
     apply Rplus_le_compat_l.
-    destruct_decide
-      (exists_dec (fun s : fin _ => σ' = (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s]) : tape]> σ1))).
-    + destruct H as [s Hs].
-      rewrite /compute_ε2.
-      (* should be provale from here *)
-      admit.
-    + admit.
+    rewrite /compute_ε2.
+    destruct (finite.find _); auto; apply Hr.
   }
 
   iSplit.
@@ -782,62 +773,70 @@ Proof.
     - done.
   }
 
-  iIntros ((heap2 & tapes2)) "[%sample %Hsample]"; simplify_eq.
-  (* we should be able to get ε2 from compute_ε2 now *)
-  replace (compute_ε2 _ _ _ _ _ _) with (ε2 sample); last first.
-  { rewrite Hsample /compute_ε2 /=.
-    remember (λ s : fin (S (Z.to_nat z)),
-         state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s])]> σ1 = state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample])]> σ1)
-        as F.
-    assert (FS: F sample).
-    { rewrite HeqF /=; done. }
-    assert (HD:  ∀ x : fin (S (Z.to_nat z)), Decision (F x) ).
-    { intros. rewrite HeqF. admit. (* ok *)}
-    destruct (@find_is_Some _ _ _ F HD sample FS) as [s' [Hs' Fs']].
-    (* fixable *)
-    admit.
-  }
-  (* decrease the supply to ε1 (to get rid of the € ε1) and then increase it to ε2.
-     the decrease is probably not needed I think? *)
+  iIntros ((heap2 & tapes2)) "[%sample %Hsample]".
   iMod (ec_decrease_supply with "Hε_supply Hε") as "Hε_supply".
   iMod (ec_increase_supply _ (ε2 sample) with "Hε_supply") as "[Hε_supply Hε]".
-  iSpecialize ("Hwp" $! sample).
   iMod (ghost_map_update ((Z.to_nat z; ns ++ [sample]) : tape) with "Htapes Hα") as "[Htapes Hα]".
+  iSpecialize ("Hwp" $! sample).
 
-
+  (* open the WP and specialize it to get the goal *)
   rewrite ub_wp_unfold /ub_wp_pre.
-  (* then we should be able to specialize using the updated ghost state.. *)
   iAssert (⌜ (common.language.to_val e) = None ⌝)%I as "%X". { auto. }
   rewrite X; clear X.
+  (* then we should be able to specialize using the updated ghost state.. *)
 
-  iAssert (state_interp (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample]) : tape]> σ1)) with "[Hheap Htapes]" as "Hσ1".
-  { rewrite /state_interp; iFrame. }
-
-  iAssert (err_interp (ε3 + ε2 sample)%NNR ) with "[Hε_supply]" as "Hε_supply".
-  { rewrite /err_interp; iFrame. }
-  iSpecialize ("Hwp" with "[Hε Hα]").
-  {  iFrame. }
-  iSpecialize ("Hwp" $! {| heap := heap2; tapes := tapes2 |} (ε3 + ε2 sample)%NNR).
-  iSpecialize ("Hwp" with "[Hσ1 Hε_supply]").
-  { rewrite Hsample. iFrame. }
-
-  clear.
-
-  remember (exec_ub e {| heap := heap2; tapes := tapes2 |}
-              (λ (ε0 : nonnegreal) '(e2, σ2), ▷ (|={∅,E}=> state_interp σ2 ∗ err_interp ε0 ∗ WP e2 @ E {{ v, Φ v }}))
-              (ε3 + ε2 sample)%NNR)%I as EUB.
-  rewrite -HeqEUB.
 
-  iAssert (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝ ={∅,E}=∗ emp)%I with "[Hclose']" as "W".
-  { iIntros. iFrame. }
+  iAssert (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝ ={∅,E}=∗ emp)%I with "[Hclose]" as "W".
+  { iIntros; iFrame. }
+
+  iPoseProof (fupd_trans_frame E ∅ E _ (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝))%I as "HR".
+  iSpecialize ("HR" with "[Hwp Hheap Hε_supply Hε Htapes Hα W]").
+  { iFrame.
+    iApply ("Hwp" with "[Hε Hα]"). { iFrame. }
+
+    rewrite /state_interp /=.
+    rewrite /state_upd_tapes in Hsample.
+    (* FIXME is there a tactic to turn record equality into equalities for all its fields? *)
+    assert (Heqt : tapes2 = <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1)).
+    { assert (H' : {| heap := heap2; tapes := tapes2 |}.(tapes) =
+                   {| heap := heap σ1; tapes := <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1) |}.(tapes))
+          by (f_equal; apply Hsample).
+      by simpl in H'. }
+    assert (Heqh : heap2 = heap σ1).
+    { assert (H' : {| heap := heap2; tapes := tapes2 |}.(heap) =
+                   {| heap := heap σ1; tapes := <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1) |}.(heap))
+          by (f_equal; apply Hsample).
+      by simpl in H'. }
+    rewrite Heqt Heqh.
+    iFrame. }
+
+  rewrite Hsample /compute_ε2 /=.
+  destruct (@find_is_Some _ _ _
+               (λ s : fin (S (Z.to_nat z)), state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s])]> σ1 = state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample])]> σ1)
+               _ sample eq_refl)
+            as [r [Hfind Hr]].
+  rewrite Hfind.
+  replace r with sample; last first.
+  { rewrite /state_upd_tapes in Hr.
+    (* again: I want to destruct this equality *)
+    assert (Heqt : <[α:=(Z.to_nat z; ns ++ [r])]> (tapes σ1) = <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1)).
+    { assert (H' : {| heap := heap σ1; tapes := <[α:=(Z.to_nat z; ns ++ [r])]> (tapes σ1) |}.(tapes) =
+                   {| heap := heap σ1; tapes := <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1) |}.(tapes))
+          by (f_equal; apply Hr).
+      by simpl in H'. }
+    apply (insert_inv (tapes σ1) α) in Heqt.
+    (* is there a way around using clasical theorem here?
+       Search ((_; ?X) = (_; ?Y)) (?X = ?Y).
+       apply eq_sigT_eq_dep in Heqt.
+       apply eq_dep_non_dep in Heqt. *)
+    apply classic_proof_irrel.PIT.EqdepTheory.inj_pair2 in Heqt.
+    apply app_inv_head in Heqt.
+    by inversion Heqt. }
 
-  iPoseProof (fupd_trans_frame E ∅ E EUB (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝))%I as "Z".
-  iSpecialize ("Z" with "[W Hwp]").
-  {  iFrame. }
   iApply fupd_mask_mono; last done.
 
-  (* oh damn! this can't be proven. can we only take this step when E = ∅? *)
-  admit.
-
+  (* I can't see where this could be improved in the proof, but I also see no reason why it could't.
+      (related to the prophecy counterexample? idk. )*)
+  set_solver.
 Admitted.
 End rules.

From 1eed3e7462bf1f9e00b7d5be36647a90bc447232 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Tue, 2 Jan 2024 11:37:10 -0500
Subject: [PATCH 20/37] simplify proof

---
 theories/ub_logic/ub_rules.v | 50 +++++++++++++++++-------------------
 1 file changed, 23 insertions(+), 27 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 1650c7e7..58655f99 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -747,8 +747,21 @@ Proof.
   }
 
   iSplit.
-  { iPureIntro.
-    rewrite /compute_ε2_in_state /=.
+  { iPureIntro. simpl.
+    (* apply Rle_plus_l; [|apply cond_nonneg]. *)
+
+    Check state_step_support_equiv_rel.
+    (* we want to split the sum based on state_step_rel (and then invert state_step_rel)*)
+    Search SeriesC.
+
+
+
+
+
+    Search (state_step).
+    Locate state_step_rel.
+
+
     (* so we have this gigantic sum over all states
        the state_step factor should eliminate all of those except S N of them
        which are of the form ρ with a new value on α
@@ -758,8 +771,6 @@ Proof.
        then for each state, the second term will be (ε2 s)
 
        by Hsum, the total is ε1
-
-       conclude by 0 <= ε3
      *)
     admit.
   }
@@ -785,29 +796,16 @@ Proof.
   rewrite X; clear X.
   (* then we should be able to specialize using the updated ghost state.. *)
 
-
-  iAssert (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝ ={∅,E}=∗ emp)%I with "[Hclose]" as "W".
+  iAssert (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝ ={∅,E}=∗ emp)%I with "[Hclose]" as "HcloseW".
   { iIntros; iFrame. }
 
   iPoseProof (fupd_trans_frame E ∅ E _ (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝))%I as "HR".
-  iSpecialize ("HR" with "[Hwp Hheap Hε_supply Hε Htapes Hα W]").
+  iSpecialize ("HR" with "[Hwp Hheap Hε_supply Hε Htapes Hα HcloseW]").
   { iFrame.
     iApply ("Hwp" with "[Hε Hα]"). { iFrame. }
-
     rewrite /state_interp /=.
     rewrite /state_upd_tapes in Hsample.
-    (* FIXME is there a tactic to turn record equality into equalities for all its fields? *)
-    assert (Heqt : tapes2 = <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1)).
-    { assert (H' : {| heap := heap2; tapes := tapes2 |}.(tapes) =
-                   {| heap := heap σ1; tapes := <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1) |}.(tapes))
-          by (f_equal; apply Hsample).
-      by simpl in H'. }
-    assert (Heqh : heap2 = heap σ1).
-    { assert (H' : {| heap := heap2; tapes := tapes2 |}.(heap) =
-                   {| heap := heap σ1; tapes := <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1) |}.(heap))
-          by (f_equal; apply Hsample).
-      by simpl in H'. }
-    rewrite Heqt Heqh.
+    inversion Hsample.
     iFrame. }
 
   rewrite Hsample /compute_ε2 /=.
@@ -819,13 +817,9 @@ Proof.
   replace r with sample; last first.
   { rewrite /state_upd_tapes in Hr.
     (* again: I want to destruct this equality *)
-    assert (Heqt : <[α:=(Z.to_nat z; ns ++ [r])]> (tapes σ1) = <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1)).
-    { assert (H' : {| heap := heap σ1; tapes := <[α:=(Z.to_nat z; ns ++ [r])]> (tapes σ1) |}.(tapes) =
-                   {| heap := heap σ1; tapes := <[α:=(Z.to_nat z; ns ++ [sample])]> (tapes σ1) |}.(tapes))
-          by (f_equal; apply Hr).
-      by simpl in H'. }
+    inversion Hr as [Heqt].
     apply (insert_inv (tapes σ1) α) in Heqt.
-    (* is there a way around using clasical theorem here?
+    (* FIXME is there a way around using clasical theorem here?
        Search ((_; ?X) = (_; ?Y)) (?X = ?Y).
        apply eq_sigT_eq_dep in Heqt.
        apply eq_dep_non_dep in Heqt. *)
@@ -835,8 +829,10 @@ Proof.
 
   iApply fupd_mask_mono; last done.
 
-  (* I can't see where this could be improved in the proof, but I also see no reason why it could't.
+  (* FIXME I can't see where this could be improved in the proof, but I also see no reason why it could't.
       (related to the prophecy counterexample? idk. )*)
   set_solver.
 Admitted.
+
+
 End rules.

From 0b9d6787c02e7dd765283513994849b259f81625 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Tue, 2 Jan 2024 12:44:23 -0500
Subject: [PATCH 21/37] (wip)

---
 theories/ub_logic/ub_rules.v | 39 +++++++++++++++++++++++++++---------
 1 file changed, 29 insertions(+), 10 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 58655f99..b963ca2e 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -692,6 +692,7 @@ Check (fun σ σ' α z ns N =>
 
 (* really this should not depend on the expr at all :/*)
 
+
 Definition compute_ε2 (σ : state) (ρ : cfg) α N ns (ε2 : fin (S N) -> nonnegreal) : nonnegreal :=
   match finite.find (fun s => state_upd_tapes <[α:=(N; ns ++ [s]) : tape]> σ = snd ρ) with
     | Some s => ε2 s
@@ -699,7 +700,6 @@ Definition compute_ε2 (σ : state) (ρ : cfg) α N ns (ε2 : fin (S N) -> nonne
   end.
 
 
-
 Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   E = ∅ -> (* can this really only be proven when E = ∅ or can we improve this? *)
   TCEq N (Z.to_nat z) →
@@ -754,22 +754,41 @@ Proof.
     (* we want to split the sum based on state_step_rel (and then invert state_step_rel)*)
     Search SeriesC.
 
+    remember (fun ρ : state => _) as Body.
 
+    (* FIXME there must be a better way to define this *)
+    (* should tapes_insert be a cannonical instance? *)
+    pose P := fun ρ => (exists s : fin _, ρ = state_upd_tapes <[α:=(_ ; ns ++ [s]) : tape]> σ1).
+    assert (Pdec : forall ρ : state, Decision (P tapes_insert ρ)).
+    { intros ρ.
+      rewrite /P.
+      apply exists_dec.
+      intros; apply state_eq_dec.
+    }
+    pose Body' :=
+      (fun ρ : _ =>
+          if (@bool_decide (P tapes_insert ρ) (Pdec ρ))
+             then Body ρ
+             else 0%R).
+    rewrite (SeriesC_ext _ Body'); last first.
+    { intros s.
+      rewrite /Body' /P /=.
+      case_bool_decide; [auto|].
+      (* should be provable *)
+      admit.
+    }
+    rewrite /Body' /P.
 
+    (* how to we show that there are exactly S N states which satisfy P, and
+       that body is ε1/(S N) for all of them? *)
+    (* NEED: lemma to take a  series over different indices (with an injection or something? )*)
 
-
+    Check state_step_rel.
     Search (state_step).
-    Locate state_step_rel.
-
-
-    (* so we have this gigantic sum over all states
-       the state_step factor should eliminate all of those except S N of them
-       which are of the form ρ with a new value on α
 
+    (*
        so the series is reduced to S N terms, and each _should_ be 1/S N.
-
        then for each state, the second term will be (ε2 s)
-
        by Hsum, the total is ε1
      *)
     admit.

From 29724d5942a32c92da4f63cda3d2713b9df1c93f Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Tue, 2 Jan 2024 16:31:35 -0500
Subject: [PATCH 22/37] skeleton of adv comp SeriesC goal

---
 theories/ub_logic/ub_rules.v | 82 ++++++++++++++++++++++++++++++++++--
 1 file changed, 78 insertions(+), 4 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index b963ca2e..61d31163 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -748,12 +748,74 @@ Proof.
 
   iSplit.
   { iPureIntro. simpl.
-    (* apply Rle_plus_l; [|apply cond_nonneg]. *)
+    rewrite -Hsum.
 
-    Check state_step_support_equiv_rel.
-    (* we want to split the sum based on state_step_rel (and then invert state_step_rel)*)
-    Search SeriesC.
+    (* first: deal with the ε_rem term *)
+    setoid_rewrite Rmult_plus_distr_l.
+    rewrite SeriesC_plus; [|admit|admit]. (* existence *)
+
+    rewrite -Rplus_comm; apply Rplus_le_compat; last first.
+    { (* true because state_step is a pmf so is lt 1 *)
+      rewrite SeriesC_scal_r -{2}(Rmult_1_l (nonneg ε_rem)).
+      apply Rmult_le_compat; try auto; [apply cond_nonneg | lra]. }
+
+
+    (* now we make an injection: we rewrite the lhs series to use a from_option *)
+    pose f := (fun n : fin _ => 1 / S (Z.to_nat z) * ε2 n)%R.
+    rewrite (SeriesC_ext
+               (λ x : state, state_step σ1 α x * compute_ε2 σ1 (e, x) α (Z.to_nat z) ns ε2)%R
+               (fun x : state => from_option f 0
+                                (finite.find (fun n => state_upd_tapes <[α:=(_; ns ++ [n]) : tape]> σ1 = x ))%R));
+      last first.
+    { intros n.
+      rewrite /compute_ε2.
+      destruct (finite.find _) as [sf|].
+      - rewrite /= /f.
+        (* we will need the assumption that ε2 sf = 0 later, or we will get stuck
+           maybe this is what we should destruct instead of finite.find?
+           I need to get evidence from somewhere and the destruct is not giving me that rn
+           either way... pretty sure this is provable
+         *)
+        Check (ε2 sf = nnreal_zero)%R.
+
+        (*
+        apply Rmult_eq_compat_r.
+        rewrite /state_step.
+        Set Printing Coercions.
+        rewrite bool_decide_true; last first.
+        { rewrite elem_of_dom Hlookup /= /is_Some.
+          by exists (Z.to_nat z; ns). }
+        rewrite (lookup_total_correct _ _ (Z.to_nat z; ns)); auto.
+        Opaque Z.to_nat.
+        rewrite /state_upd_tapes.
+        rewrite /dunifP /dunif.
+
+        }
+
+
+      rewrite /nnreal_zero; simpl. *)
+        admit.
+      - admit. }
+
+    apply SeriesC_le_inj.
+    - (* f is nonnegative *)
+      intros.
+      apply Rmult_le_pos.
+      + rewrite /Rdiv.
+        apply Rmult_le_pos; try lra.
+        apply Rlt_le, Rinv_0_lt_compat, pos_INR_S.
+      + apply cond_nonneg.
+    - (* injection *)
+      intros σ' σ'' σ''' HF1 HF2.
+      rewrite /state_upd_tapes /= in HF1.
+      rewrite -HF2 in HF1.
+      admit.
+    - (* existence *)
+      admit.
 
+
+
+    (*
     remember (fun ρ : state => _) as Body.
 
     (* FIXME there must be a better way to define this *)
@@ -770,6 +832,10 @@ Proof.
           if (@bool_decide (P tapes_insert ρ) (Pdec ρ))
              then Body ρ
              else 0%R).
+
+    Check SeriesC_le_inj.
+
+
     rewrite (SeriesC_ext _ Body'); last first.
     { intros s.
       rewrite /Body' /P /=.
@@ -777,12 +843,19 @@ Proof.
       (* should be provable *)
       admit.
     }
+
+
+    Check (SeriesC_le_inj)
+
+
+
     rewrite /Body' /P.
 
     (* how to we show that there are exactly S N states which satisfy P, and
        that body is ε1/(S N) for all of them? *)
     (* NEED: lemma to take a  series over different indices (with an injection or something? )*)
 
+    Check state_step_support_equiv_rel.
     Check state_step_rel.
     Search (state_step).
 
@@ -792,6 +865,7 @@ Proof.
        by Hsum, the total is ε1
      *)
     admit.
+    *)
   }
 
   (* lifted lookup on tapes *)

From c19ee401e26f1382eb3640422ad210fdcd35fb78 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Tue, 2 Jan 2024 18:05:19 -0500
Subject: [PATCH 23/37] closed proof of advanced composition on tapes

---
 theories/ub_logic/ub_rules.v | 145 ++++++++++++++---------------------
 1 file changed, 58 insertions(+), 87 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 61d31163..3c5b9d54 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -384,10 +384,11 @@ Proof.  Admitted.
 
 Lemma mean_constraint_ub (N : nat) ε1 (ε2 : fin (S N) -> nonnegreal) :
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) ->
-  (exists r, ∀ n, (ε2 n <= r)%R).
+  (exists r, (0 <= r)%R /\ ∀ n,(ε2 n <= r)%R).
 Proof.
   intros Hsum.
   exists (nnreal_nat (S N) * ε1)%NNR.
+  split. { apply Rmult_le_pos; apply cond_nonneg. }
   intros n.
   Opaque nnreal_nat.
   rewrite /= -Hsum.
@@ -734,16 +735,16 @@ Proof.
   (* upper bound *)
   iSplit.
   { iPureIntro.
-    destruct (mean_constraint_ub _ _ _ Hsum) as [r Hr].
+    destruct (mean_constraint_ub _ _ _ Hsum) as [r [Hr_nonneg Hr_ub]].
     assert (Hr_nnonneg : (0 <= r)%R).
-    { eapply Rle_trans; [|apply (Hr 0%fin)].
+    { eapply Rle_trans; [|apply (Hr_ub 0%fin)].
       rewrite match_nonneg_coercions.
       apply cond_nonneg. }
     exists (ε_rem + r)%R.
     intros [e' σ'].
     apply Rplus_le_compat_l.
     rewrite /compute_ε2.
-    destruct (finite.find _); auto; apply Hr.
+    destruct (finite.find _); auto; apply Hr_ub.
   }
 
   iSplit.
@@ -752,14 +753,24 @@ Proof.
 
     (* first: deal with the ε_rem term *)
     setoid_rewrite Rmult_plus_distr_l.
-    rewrite SeriesC_plus; [|admit|admit]. (* existence *)
+    rewrite SeriesC_plus.
+
+    2: { apply ex_seriesC_scal_r, pmf_ex_seriesC. }
+    2: { apply pmf_ex_seriesC_mult_fn.
+         destruct (mean_constraint_ub _ _ _ Hsum) as [r [Hr_nonneg Hr_ub]].
+         exists r; intros; split.
+          - apply cond_nonneg.
+          - rewrite /compute_ε2.
+            destruct (finite.find _).
+            + apply Hr_ub.
+            + simpl; apply Hr_nonneg.
+    }
 
     rewrite -Rplus_comm; apply Rplus_le_compat; last first.
     { (* true because state_step is a pmf so is lt 1 *)
       rewrite SeriesC_scal_r -{2}(Rmult_1_l (nonneg ε_rem)).
       apply Rmult_le_compat; try auto; [apply cond_nonneg | lra]. }
 
-
     (* now we make an injection: we rewrite the lhs series to use a from_option *)
     pose f := (fun n : fin _ => 1 / S (Z.to_nat z) * ε2 n)%R.
     rewrite (SeriesC_ext
@@ -769,33 +780,47 @@ Proof.
       last first.
     { intros n.
       rewrite /compute_ε2.
-      destruct (finite.find _) as [sf|].
-      - rewrite /= /f.
-        (* we will need the assumption that ε2 sf = 0 later, or we will get stuck
-           maybe this is what we should destruct instead of finite.find?
-           I need to get evidence from somewhere and the destruct is not giving me that rn
-           either way... pretty sure this is provable
-         *)
-        Check (ε2 sf = nnreal_zero)%R.
-
-        (*
+      remember (finite.find _) as F.
+      destruct F as [sf|].
+      - Opaque INR.
+        symmetry in HeqF.
+        apply find_Some in HeqF.
+        simpl in HeqF; rewrite -HeqF.
+        rewrite /from_option /f.
         apply Rmult_eq_compat_r.
+        rewrite /state_upd_tapes /=.
+        rewrite /pmf.
         rewrite /state_step.
-        Set Printing Coercions.
         rewrite bool_decide_true; last first.
         { rewrite elem_of_dom Hlookup /= /is_Some.
           by exists (Z.to_nat z; ns). }
         rewrite (lookup_total_correct _ _ (Z.to_nat z; ns)); auto.
-        Opaque Z.to_nat.
-        rewrite /state_upd_tapes.
-        rewrite /dunifP /dunif.
-
-        }
-
-
-      rewrite /nnreal_zero; simpl. *)
-        admit.
-      - admit. }
+        rewrite /dmap /dbind /dbind_pmf /pmf.
+        rewrite /= SeriesC_scal_l -{1}(Rmult_1_r (1 / _))%R.
+        rewrite /Rdiv Rmult_1_l; apply Rmult_eq_compat_l.
+        (* then show that this series is 0 unless a = sf *)
+        rewrite /dret /dret_pmf.
+        rewrite -{2}(SeriesC_singleton sf 1%R).
+        apply SeriesC_ext; intros.
+        symmetry.
+        case_bool_decide; simplify_eq.
+        + rewrite bool_decide_true; auto.
+        + rewrite bool_decide_false; auto.
+          rewrite /not; intros K.
+          rewrite /not in H0; apply H0.
+          rewrite /state_upd_tapes in K.
+
+          assert (R1 : ((Z.to_nat z; ns ++ [sf]) : tape) = (Z.to_nat z; ns ++ [n0])).
+          { apply (insert_inv (tapes σ1) α).
+            by inversion K.
+          }
+
+          (* FIXME: same problem as below: is classical logic really necessary here? *)
+          apply classic_proof_irrel.PIT.EqdepTheory.inj_pair2, app_inv_head in R1.
+          by inversion R1.
+          Transparent INR.
+      - rewrite /from_option /INR /=. lra.
+    }
 
     apply SeriesC_le_inj.
     - (* f is nonnegative *)
@@ -806,66 +831,12 @@ Proof.
         apply Rlt_le, Rinv_0_lt_compat, pos_INR_S.
       + apply cond_nonneg.
     - (* injection *)
-      intros σ' σ'' σ''' HF1 HF2.
-      rewrite /state_upd_tapes /= in HF1.
-      rewrite -HF2 in HF1.
-      admit.
+      intros ? ? ? HF1 HF2.
+      apply find_Some in HF1.
+      apply find_Some in HF2.
+      by rewrite -HF1 -HF2.
     - (* existence *)
-      admit.
-
-
-
-    (*
-    remember (fun ρ : state => _) as Body.
-
-    (* FIXME there must be a better way to define this *)
-    (* should tapes_insert be a cannonical instance? *)
-    pose P := fun ρ => (exists s : fin _, ρ = state_upd_tapes <[α:=(_ ; ns ++ [s]) : tape]> σ1).
-    assert (Pdec : forall ρ : state, Decision (P tapes_insert ρ)).
-    { intros ρ.
-      rewrite /P.
-      apply exists_dec.
-      intros; apply state_eq_dec.
-    }
-    pose Body' :=
-      (fun ρ : _ =>
-          if (@bool_decide (P tapes_insert ρ) (Pdec ρ))
-             then Body ρ
-             else 0%R).
-
-    Check SeriesC_le_inj.
-
-
-    rewrite (SeriesC_ext _ Body'); last first.
-    { intros s.
-      rewrite /Body' /P /=.
-      case_bool_decide; [auto|].
-      (* should be provable *)
-      admit.
-    }
-
-
-    Check (SeriesC_le_inj)
-
-
-
-    rewrite /Body' /P.
-
-    (* how to we show that there are exactly S N states which satisfy P, and
-       that body is ε1/(S N) for all of them? *)
-    (* NEED: lemma to take a  series over different indices (with an injection or something? )*)
-
-    Check state_step_support_equiv_rel.
-    Check state_step_rel.
-    Search (state_step).
-
-    (*
-       so the series is reduced to S N terms, and each _should_ be 1/S N.
-       then for each state, the second term will be (ε2 s)
-       by Hsum, the total is ε1
-     *)
-    admit.
-    *)
+      apply ex_seriesC_finite.
   }
 
   (* lifted lookup on tapes *)
@@ -925,7 +896,7 @@ Proof.
   (* FIXME I can't see where this could be improved in the proof, but I also see no reason why it could't.
       (related to the prophecy counterexample? idk. )*)
   set_solver.
-Admitted.
+Qed.
 
 
 End rules.

From f9abebfd6d32915fb7d6dc3128d8f2d82ef944b2 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Wed, 3 Jan 2024 09:42:37 -0500
Subject: [PATCH 24/37] import work on planner rule

---
 theories/prob/countable_sum.v         |  22 ++
 theories/ub_logic/seq_amplification.v | 287 ++++++++++++++++++++++++++
 theories/ub_logic/ub_rules.v          | 183 +++++++++++++++-
 3 files changed, 485 insertions(+), 7 deletions(-)
 create mode 100644 theories/ub_logic/seq_amplification.v

diff --git a/theories/prob/countable_sum.v b/theories/prob/countable_sum.v
index a243649d..a7554fdb 100644
--- a/theories/prob/countable_sum.v
+++ b/theories/prob/countable_sum.v
@@ -391,14 +391,36 @@ Section filter.
       exfalso. apply Hneq. symmetry. by apply encode_inv_Some_nat.
   Qed.
 
+  (* same proof as is_seriesC_singleton but stronger *)
+  Lemma is_seriesC_singleton_dependent (a : A) v :
+    is_seriesC (λ (n : A), if bool_decide (n = a) then v n else 0) (v a).
+  Proof.
+    rewrite /is_seriesC.
+    eapply is_series_ext; [|apply (is_series_singleton (encode_nat a))].
+    intros n =>/=. rewrite /countable_sum.
+    case_bool_decide as Hneq=>/=; subst.
+    - rewrite encode_inv_encode_nat //= bool_decide_eq_true_2 //.
+    - destruct (encode_inv_nat _) eqn:Heq=>//=.
+      case_bool_decide; [|done]; subst.
+      exfalso. apply Hneq. symmetry. by apply encode_inv_Some_nat.
+  Qed.
+
   Lemma ex_seriesC_singleton (a : A) v :
     ex_seriesC (λ (n : A), if bool_decide (n = a) then v else 0).
   Proof. eexists. eapply is_seriesC_singleton. Qed.
 
+  Lemma ex_seriesC_singleton_dependent (a : A) v :
+    ex_seriesC (λ (n : A), if bool_decide (n = a) then v n else 0).
+  Proof. eexists. eapply is_seriesC_singleton_dependent. Qed.
+
   Lemma SeriesC_singleton (a : A) v :
     SeriesC (λ n, if bool_decide (n = a) then v else 0) = v.
   Proof. apply is_series_unique, is_seriesC_singleton. Qed.
 
+  Lemma SeriesC_singleton_dependent (a : A) v :
+    SeriesC (λ n, if bool_decide (n = a) then v n else 0) = v a.
+  Proof. apply is_series_unique, is_seriesC_singleton_dependent. Qed.
+
   Lemma is_seriesC_singleton_inj (b : B) (f : A → B) v `{Inj A B (=) (=) f} :
     (∃ a, f a = b) →
     is_seriesC (λ (a : A), if bool_decide (f a = b) then v else 0) v.
diff --git a/theories/ub_logic/seq_amplification.v b/theories/ub_logic/seq_amplification.v
new file mode 100644
index 00000000..22b769b6
--- /dev/null
+++ b/theories/ub_logic/seq_amplification.v
@@ -0,0 +1,287 @@
+(** * Calculation for the Sequential Amplification Rile *)
+From stdpp Require Import namespaces.
+From iris.proofmode Require Import proofmode.
+From clutch.prelude Require Import stdpp_ext NNRbar.
+From clutch.app_rel_logic Require Import lifting ectx_lifting.
+From clutch.prob_lang Require Import lang notation tactics metatheory.
+Require Import Lra.
+
+
+Section seq_ampl.
+  Local Open Scope R.
+  Implicit Types N l i : nat.
+  Implicit Types ε : nonnegreal.
+
+
+  Lemma pow_pos N : (0 < N)%nat -> forall w, (0 < w)%nat -> 0 < ((S N)^w - 1).
+  Proof.
+    intros w HN Hw.
+    apply (Rplus_lt_reg_r 1).
+    rewrite Rplus_assoc Rplus_opp_l Rplus_0_l Rplus_0_r.
+    apply Rlt_pow_R1; [apply lt_1_INR|]; lia.
+  Qed.
+
+  Lemma pow_nz N : (0 < N)%nat -> forall w, (w > 0)%nat -> ((S N)^w - 1) ≠ 0.
+  Proof.
+    intros.
+    apply Rgt_not_eq; apply Rlt_gt.
+    apply pow_pos; lia.
+  Qed.
+
+
+
+  (* well-formedness for k *)
+  (* well-formedness of k doesn't depend on the proof => OK to use proof irrelevence *)
+  Record kwf N l : Set := mk_kwf { N_lb : (0 < N)%nat; l_lb: (0 < l)%nat }.
+  Lemma kwf_ext N l (x : kwf N l) (y : kwf N l) : x = y.
+  Proof. destruct x; destruct y. Admitted.
+
+  (** amplification factor on our error *)
+  Definition k N l (kwf : kwf N l) : R := 1 + 1 / ((S N)^l - 1).
+
+
+  Lemma lt_1_k N l kwf : 1 < k N l kwf.
+  Proof.
+    destruct kwf as [Hn Hl].
+    remember {| N_lb := _; l_lb := _|} as kwf.
+    rewrite /k /Rdiv.
+    apply (Rmult_lt_reg_r ((S N)^l-1)); [by apply pow_pos|].
+    rewrite Rmult_plus_distr_r Rmult_assoc Rinv_l; [|by apply pow_nz].
+    lra.
+  Qed.
+
+  Lemma k_pos N l kwf : 0 < k N l kwf.
+  Proof. apply (Rlt_trans _ 1); [lra|apply lt_1_k; auto]. Qed.
+
+
+  (* well-formedness for fR *)
+  Record fRwf N l i : Set := mk_fRwf { k_wf : (kwf N l) ; i_ub : (i <= l)%nat }.
+  Lemma fRwf_dec_i N l i (fRbS : fRwf N l (S i)) : fRwf N l i.
+  Proof. destruct fRbS. apply mk_fRwf; auto; lia. Qed.
+  Lemma fRwf_upper N l : kwf N l -> fRwf N l l.
+  Proof. intros. apply mk_fRwf; auto. Qed.
+  Lemma fRwf_lower N l : kwf N l -> fRwf N l 0.
+  Proof. intros. apply mk_fRwf; auto. lia. Qed.
+  Lemma fRwf_ext N l i (x : fRwf N l i) (y : fRwf N l i) : x = y.
+  Proof. destruct x; destruct y. Admitted.
+
+
+  (** remainder factor on error after step i *)
+  Fixpoint fR N l i (fRwf : fRwf N l i) : R.
+    refine ((match i as m return (i = m) -> R with
+              0%nat    => fun _ => 1%nat
+            | (S i') => fun H => ((S N) * (fR N l i' _) - (k N l (fRwf.(k_wf N l i))) * N)
+            end) (eq_refl i)).
+    apply fRwf_dec_i; by rewrite -H.
+  Defined.
+
+  (* closed form 1: easy to do induction over i *)
+  Lemma fR_closed_1 N l i fRwf: (fR N l i fRwf) = (1 - (k N l (fRwf.(k_wf N l i)))) * (S N)^i + (k N l (fRwf.(k_wf N l i))).
+  Proof.
+    destruct fRwf as [[Hn Hl] Hi].
+    remember {| k_wf := _; i_ub := _|} as fRwf.
+
+    induction i as [|i' IH].
+    - simpl; lra.
+    - Opaque INR.
+      simpl fR. rewrite IH; [|lia|intros; apply fRwf_ext].
+      remember (k N l (k_wf N l i' (fRwf_dec_i N l i' fRwf))) as K.
+      replace (k N l (k_wf N l (S i') fRwf)) with K.
+      rewrite Rmult_plus_distr_l.
+      rewrite Rmult_comm Rmult_assoc (Rmult_comm  _ (S _)) tech_pow_Rmult.
+      rewrite /Rminus Rplus_assoc.
+      apply Rplus_eq_compat_l.
+      rewrite S_INR.
+      lra.
+  Qed.
+
+  (* closed forn 2: easy to bound *)
+  Lemma fR_closed_2 N l i fRwf: (fR N l i fRwf) = 1 - (((S N)^i - 1) / ((S N)^l - 1)).
+  Proof.
+    destruct fRwf as [[Hn Hl] Hi].
+    remember {| k_wf := _; i_ub := _|} as fRwf.
+    rewrite fR_closed_1.
+    rewrite /k /=. lra.
+  Qed.
+
+  (* much easier to prove this using closed form 2 *)
+  Lemma fR_nonneg N l i fRwf : 0 <= (fR N l i fRwf).
+  Proof.
+    destruct fRwf as [[Hn Hl] Hi].
+    remember {| k_wf := _; i_ub := _ |} as fRwf.
+    rewrite fR_closed_2.
+    rewrite /Rdiv.
+    apply (Rmult_le_reg_r (S N^l - 1)).
+    - rewrite /Rminus.
+      apply (Rplus_lt_reg_r 1).
+      rewrite Rplus_0_l Rplus_assoc Rplus_opp_l Rplus_0_r.
+      apply Rlt_pow_R1; [apply lt_1_INR|]; lia.
+    - rewrite Rmult_0_l.
+      rewrite Rmult_plus_distr_r /Rdiv Rmult_1_l.
+      rewrite Ropp_mult_distr_l_reverse.
+      rewrite Rmult_assoc Rinv_l; [|apply pow_nz; lia].
+      rewrite Rmult_1_r.
+      apply (Rplus_le_reg_r (S N^i - 1)).
+      rewrite Rplus_assoc Rplus_opp_l Rplus_0_l Rplus_0_r.
+      apply Rplus_le_compat_r.
+      apply Rle_pow; try lia.
+      apply Rlt_le.
+      apply lt_1_INR.
+      lia.
+  Qed.
+
+  (* fR will have the mean property we need *)
+  Lemma fR_mean N l i fRwf :
+    (S N) * (fR N l i (fRwf_dec_i N l i fRwf)) = N * (k N l (fRwf.(k_wf N l (S i)))) +  fR N l (S i) fRwf .
+  Proof. intros. rewrite /fR /=. lra. Qed.
+
+  (** Remaining error at each step *)
+  Program Definition εR N l i (ε : posreal) fRwf : nonnegreal
+    := mknonnegreal (ε * fR N l i fRwf) _.
+  Next Obligation.
+    intros.
+    apply Rmult_le_pos.
+      - apply Rlt_le. apply cond_pos.
+      - by apply fR_nonneg.
+  Qed.
+
+  Lemma εR_ext N l i (ε : posreal) fRwf1 fRwf2 : (εR N l i ε fRwf1 = εR N l i ε fRwf2).
+  Proof. f_equal. apply fRwf_ext. Qed.
+
+  Program Definition εAmp N l (ε : posreal) kwf : nonnegreal
+    := mknonnegreal (ε.(pos) * k N l kwf) _.
+  Next Obligation.
+    intros; simpl.
+    destruct ε; rewrite /RIneq.nonneg.
+    apply Rmult_le_pos.
+    - apply Rlt_le. auto.
+    - apply Rlt_le. apply k_pos.
+  Qed.
+
+  Program Definition εAmp_iter N l d (ε : posreal) kwf : posreal
+    := mkposreal (ε.(pos) * (k N l kwf)^d) _.
+  Next Obligation.
+    intros; simpl.
+    destruct ε; rewrite /RIneq.nonneg.
+    apply Rmult_lt_0_compat.
+    - auto.
+    - apply pow_lt. apply k_pos.
+  Qed.
+
+  Lemma εAmp_iter_cmp N l d (ε : posreal) kwf :
+    εAmp N l (εAmp_iter N l d ε kwf) kwf = pos_to_nn (εAmp_iter N l (S d) ε kwf).
+  Proof.
+    apply nnreal_ext.
+    rewrite /εAmp_iter /εAmp /pos_to_nn /=.
+    lra.
+  Qed.
+
+  Lemma εAmp_amplification N l (ε : posreal) kwf : ε < (εAmp N l ε kwf).
+  Proof.
+    rewrite /εAmp /=.
+    replace (pos ε) with (pos ε * 1) by apply Rmult_1_r.
+    rewrite Rmult_assoc.
+    apply Rmult_lt_compat_l.
+    - apply cond_pos.
+    - rewrite Rmult_1_l. apply lt_1_k; auto.
+  Qed.
+
+
+  (** Distribution for amplification at step i *)
+  Definition εDistr N l i (ε : posreal) target fRwf : (fin (S N)) -> nonnegreal
+    := fun sample => if (bool_decide (sample = target))
+                    then (εR N l (S i) ε fRwf)
+                    else (εAmp N l ε (fRwf.(k_wf N l (S i)))).
+
+
+  (** Mean lemma for calls to amplification *)
+  Lemma εDistr_mean N l i (ε : posreal) target fRwf :
+       SeriesC (λ n : fin (S N), (1 / INR (S N) * nonneg (εDistr N l i ε target fRwf n))%R)
+    = (εR N l i ε (fRwf_dec_i N l i fRwf)).
+  Proof.
+    destruct fRwf as [[Hn Hl] Hi].
+    remember {| k_wf := _; i_ub := _ |} as fRwf.
+
+    remember (fun n : fin _ => 1 / INR (S N) * nonneg (εDistr N l i ε target fRwf n))%R as body.
+    (* we want to exclude the n=target case, and then it's a constant *)
+
+    assert (body_pos : ∀ a : fin _, 0 <= body a).
+    { intro a.
+      rewrite Heqbody.
+      apply Rmult_le_pos.
+      - apply Rle_mult_inv_pos; [lra|apply lt_0_INR; lia].
+      - destruct εDistr. simpl; lra. }
+    rewrite (SeriesC_split_elem body target body_pos); try (apply ex_seriesC_finite).
+    simpl.
+
+    (* FIXME: Revisit that thing about rewriting under the function
+        setoid something?
+        Then we don't need the dependent versions of the function in this case
+
+     *)
+
+    (* this will come up a bunch *)
+    assert (HSN : not (@eq R (INR (S N)) (IZR Z0))).
+    { rewrite S_INR. apply Rgt_not_eq. apply Rcomplements.INRp1_pos. }
+
+
+    (* Evaluate the first series *)
+    replace (SeriesC (λ a : fin _, if bool_decide (a = target) then body a else 0))
+       with (1 / INR (S N) * (εR N l (S i) ε fRwf)); last first.
+    { rewrite SeriesC_singleton_dependent.
+      rewrite Heqbody /εDistr.
+      rewrite bool_decide_true; try auto. }
+
+    (* Evaluate the second series *)
+    replace (SeriesC (λ a : fin _, if bool_decide (not (a = target)) then body a else 0))
+       with (N  * / INR (S N) * (εAmp N l ε (fRwf.(k_wf N l (S i))))); last first.
+    { apply (Rplus_eq_reg_l (1 * / INR (S N) * (εAmp N l ε (fRwf.(k_wf N l (S i)))))).
+      (* simplify the LHS *)
+      do 2 rewrite Rmult_assoc.
+      rewrite -Rmult_plus_distr_r.
+      rewrite Rplus_comm -S_INR -Rmult_assoc Rinv_r; try auto.
+      do 2 rewrite Rmult_1_l.
+
+
+      (* turn the first term on the RHS into a singleton series, and combine into constant series *)
+      rewrite -(SeriesC_singleton target  (/ INR (S N) * _)).
+      rewrite -SeriesC_plus; try (apply ex_seriesC_finite).
+      rewrite -(SeriesC_ext (fun x : fin (S N) => / INR (S N) * (εAmp N l ε (fRwf.(k_wf N l (S i)))))); last first.
+      { (* series are extensionally equal*)
+        intros n.
+        case_bool_decide.
+        - rewrite bool_decide_false; auto. lra.
+        - rewrite bool_decide_true; auto.
+          rewrite Heqbody /εDistr.
+          rewrite bool_decide_false; auto.
+          rewrite Rplus_0_l /Rdiv Rmult_1_l.
+          apply Rmult_eq_compat_l.
+          by simpl nonneg. }
+
+      (* compute the finite series *)
+      rewrite SeriesC_finite_mass fin_card.
+      rewrite -Rmult_assoc Rinv_r; try auto.
+      lra.
+    }
+
+    (* Multiply everything by S N*)
+    apply (Rmult_eq_reg_l (INR (S N))); [| apply not_0_INR;lia].
+    rewrite Rmult_plus_distr_l -Rmult_assoc /Rdiv.
+    rewrite Rmult_1_l Rinv_r; [| apply not_0_INR;lia].
+    rewrite Rmult_1_l.
+    rewrite -Rmult_assoc (Rmult_comm _ ( / INR (S N))) -Rmult_assoc.
+    rewrite Rinv_r; [| apply not_0_INR;lia].
+    rewrite Rmult_1_l.
+
+    (* Turn everything into fR and k by dividing out 𝜀*)
+    rewrite /εR. Opaque fR. simpl nonneg.
+    do 2 rewrite (Rmult_comm (INR _)) Rmult_assoc.
+    rewrite -Rmult_plus_distr_l.
+    apply Rmult_eq_compat_l.
+
+    (* apply fR_mean and conclude *)
+    rewrite (Rmult_comm _ (INR (S N))).
+    rewrite (fR_mean N); try lia.
+    lra.
+  Qed.
+End seq_ampl.
diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 3c5b9d54..5724810d 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -377,10 +377,9 @@ Proof.
   done.
 Qed.
 
-(* FIXME: merge me from other branch *)
-Lemma SeriesC_singleton_dependent `{Countable A} (a : A) (v : A -> nonnegreal) :
-  SeriesC (λ n, if bool_decide (n = a) then v n else nnreal_zero) = nonneg (v a).
-Proof.  Admitted.
+(* FIXME: where should this go (if anywhere?) *)
+Lemma match_nonneg_coercions (n : nonnegreal) : NNRbar_to_real (NNRbar.Finite n) = nonneg n.
+Proof. by simpl. Qed.
 
 Lemma mean_constraint_ub (N : nat) ε1 (ε2 : fin (S N) -> nonnegreal) :
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) ->
@@ -403,7 +402,8 @@ Proof.
     replace (nonneg {| nonneg := INR (S N); cond_nonneg := _ |}) with (INR (S N)); [| by simpl ].
     apply not_0_INR.
     auto.
-  - rewrite -(SeriesC_singleton_dependent _ ε2).
+  - rewrite -match_nonneg_coercions.
+    rewrite -(SeriesC_singleton_dependent _ ε2).
     apply SeriesC_le.
     + intros n'.
       assert (H : (0 <= (nonneg (ε2 n')))%R) by apply cond_nonneg.
@@ -413,8 +413,6 @@ Proof.
 Qed.
 
 
-Lemma match_nonneg_coercions (n : nonnegreal) : NNRbar_to_real (NNRbar.Finite n) = nonneg n.
-Proof. by simpl. Qed.
 
 
 Lemma wp_couple_rand_adv_comp (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
@@ -899,4 +897,175 @@ Proof.
 Qed.
 
 
+(*
+Lemma ec_spend_irrel ε1 ε2 : (ε1.(nonneg) = ε2.(nonneg)) → € ε1 -∗ € ε2.
+Proof.
+  iIntros (?) "?".
+  replace ε1 with ε2; first by iFrame.
+  by apply nnreal_ext.
+Qed.
+
+Lemma ec_spend_1 ε1 : (1 <= ε1.(nonneg))%R → € ε1 -∗ False.
+Proof. Admitted.
+
+(** advanced composition on one tape *)
+(* not really sure what this lemma will look like in the real version? *)
+Lemma presample_adv_comp (N : nat) α ns (ε : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
+  SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε) →
+  (α ↪ (N; ns) ∗ € ε) -∗ (∃ s, (α ↪ (N; ns ++ [s])) ∗ €(ε2 s)).
+Proof. Admitted.
+
+Lemma amplification_depth N L (ε : posreal) (kwf : kwf N L) : exists n : nat, (1 <= ε * (k N L kwf) ^ n)%R.
+Proof.
+  (* shouldn't be too hard, it's the log *)
+Admitted.
+
+
+Lemma lookup_ex {A} (n : nat) (L : list A) : (n < length L)%nat -> exists x, (L !! n) = Some x.
+Proof.
+  (* can't figure out how to do this with existing lemmas! *)
+  intros HL.
+  destruct L as [|h H]; [simpl in HL; lia|].
+  generalize dependent H. generalize dependent h.
+  induction n as [|n' IH].
+  - intros h ? ?. exists h; by simpl.
+  - intros h H HL.
+    rewrite cons_length in HL; apply Arith_prebase.lt_S_n in HL.
+    destruct H as [|h' H']; [simpl in HL; lia|].
+    replace ((h :: h' :: H') !! S n') with ((h' :: H') !! n'); last by simpl.
+    by apply IH.
+Qed.
+
+
+(* whenever i is strictly less than l (ie, (S i) <= l) we can amplify *)
+(* we'll need another rule for spending?, but that should be simple *)
+Lemma presample_amplify' N L kwf prefix (suffix_total suffix_remaining : list (fin (S N))) 𝛼 (ε : posreal) :
+  ⊢ ⌜ L = length suffix_total ⌝ →
+    ⌜ (0 < L)%nat ⌝ →
+    𝛼 ↪ (N; prefix) -∗
+    (€ (pos_to_nn ε)) -∗
+    ∀ (i : nat),
+      (∀ (HL : (i <= L)%nat),
+          (∃ junk, 𝛼 ↪ (N; prefix ++ junk) ∗ €(εAmp N L ε kwf)) ∨
+          ((𝛼 ↪ (N; prefix ++ (take i suffix_total))) ∗
+            € (εR N L i ε (mk_fRwf N L i kwf HL)))).
+Proof.
+  iIntros (Htotal HLpos) "Htape Hcr_initial"; iIntros (i).
+  iInduction i as [|i'] "IH" forall (suffix_remaining).
+  - iIntros (HL).
+    iRight. iSplitL "Htape".
+    + rewrite take_0 -app_nil_end. iFrame.
+    + iApply ec_spend_irrel; last iFrame.
+      rewrite /εR /fR /pos_to_nn /=; lra.
+  - iIntros "%HL".
+    assert (HL' : (i' <= L)%nat) by lia.
+    iSpecialize ("IH" $! _ with "Htape Hcr_initial").
+    iSpecialize ("IH" $! HL').
+    iDestruct "IH" as "[[%junk(Htape&Hcr)]|(Htape&Hcr)]".
+    + iLeft; iExists junk; iFrame.
+    +
+      (* we need to do something different dependning on if (S i') is L? No. in that case we still need 1 amp*)
+      assert (Hi' : (i' < length suffix_total)%nat) by lia.
+      destruct (lookup_ex i' suffix_total Hi') as [target Htarget].
+      rewrite (take_S_r _ _ target); [|apply Htarget].
+      pose M := (εDistr_mean N L i' ε target (mk_fRwf N L (S i') kwf HL)).
+      iPoseProof (presample_adv_comp N 𝛼
+                   (prefix ++ take i' suffix_total)
+                   (εR N L i' ε (fRwf_dec_i N L i' _)) (εDistr N L i' ε target _) M) as "PS".
+      replace {| k_wf := kwf; i_ub := HL' |} with(fRwf_dec_i N L i' {| k_wf := kwf; i_ub := HL |});
+        last by apply fRwf_ext.
+      iSpecialize ("PS" with "[Htape Hcr]"); first iFrame.
+      iDestruct "PS" as "[%s (Htape&Hcr)]".
+      (* NOW we can destruct and decide if we're left or right *)
+      rewrite /εDistr.
+      case_bool_decide.
+      * iRight. rewrite H app_assoc. iFrame.
+      * iLeft. iExists (take i' suffix_total ++ [s]).
+        replace (k_wf N L (S i') {| k_wf := kwf; i_ub := HL |}) with kwf; last by apply kwf_ext.
+        rewrite -app_assoc; iFrame.
+    Unshelve. auto.
+Qed.
+
+(* do one step in the amplification sequence *)
+Lemma presample_amplify N L prefix suffix 𝛼 (ε : posreal) (kwf: kwf N L) :
+  L = (length suffix) ->
+  € (pos_to_nn ε) -∗
+  (𝛼 ↪ (N; prefix)) -∗
+  (𝛼 ↪ (N; prefix ++ suffix) ∨ (∃ junk, 𝛼 ↪ (N; prefix ++ junk) ∗ €(εAmp N L ε kwf))).
+Proof.
+  iIntros (Hl) "Hcr Htape".
+
+  destruct suffix as [|s0 sr].
+  - iLeft. rewrite -app_nil_end. iFrame.
+  - remember (s0 :: sr) as suffix.
+    assert (Hl_pos : (0 < L)%nat).
+    { rewrite Hl Heqsuffix cons_length. lia. }
+    iPoseProof (presample_amplify' N L _ prefix suffix suffix 𝛼 ε $! Hl Hl_pos) as "X".
+    iSpecialize ("X" with "Htape Hcr").
+    iSpecialize ("X" $! L (le_n L)).
+    iDestruct "X" as "[H|(H&_)]".
+    + iRight. iApply "H".
+    + iLeft. rewrite Hl firstn_all. iFrame.
+Qed.
+
+
+Lemma seq_amplify N L d prefix suffix 𝛼 (ε : posreal) (kwf: kwf N L) :
+  L = (length suffix) ->
+  € (pos_to_nn ε) -∗
+  (𝛼 ↪ (N; prefix)) -∗
+  (∃ junk,
+      𝛼 ↪ (N; prefix ++ junk ++ suffix) ∨ 𝛼 ↪ (N; prefix ++ junk) ∗ €(pos_to_nn (εAmp_iter N L d ε kwf))).
+Proof.
+  iIntros (HL) "Hcr Htape".
+  iInduction (d) as [|d'] "IH".
+  - iExists []; rewrite app_nil_r. iRight. iFrame.
+    iApply ec_spend_irrel; last auto.
+    by rewrite /εAmp_iter /pos_to_nn /= Rmult_1_r.
+  - iDestruct ("IH" with "Hcr Htape") as "[%junk [Hlucky|(Htape&Hcr)]]".
+    + iExists junk; iLeft; iFrame.
+    + rewrite -εAmp_iter_cmp.
+      iPoseProof (presample_amplify N L (prefix ++ junk) suffix 𝛼 (εAmp_iter N L d' ε kwf)) as "X"; try auto.
+      iDestruct ("X" with "Hcr Htape") as "[Hlucky|[%junk' (Htape&Hcr)]]".
+      * iExists junk; iLeft. rewrite -app_assoc; iFrame.
+      * iExists (junk ++ junk'); iRight.
+        rewrite app_assoc; iFrame.
+Qed.
+
+
+Lemma presample_planner_pos N prefix suffix 𝛼 ε (HN : (0 < N)%nat) (HL : (0 < (length suffix))%nat) (Hε : (0 < ε)%R) :
+  € ε -∗
+  (𝛼 ↪ (N; prefix)) -∗
+  (∃ junk, 𝛼 ↪ (N; prefix ++ junk ++ suffix)).
+Proof.
+  iIntros "Hcr Htape".
+  (* make the interface match the other coupling rules *)
+  remember (length suffix) as L.
+  assert (kwf : kwf N L). { apply mk_kwf; lia. }
+  pose ε' := mkposreal ε.(nonneg) Hε.
+  replace ε with (pos_to_nn ε'); last first.
+  { rewrite /ε' /pos_to_nn. by apply nnreal_ext. }
+
+  destruct (amplification_depth N L ε' kwf) as [d Hdepth].
+  iDestruct ((seq_amplify N L d prefix suffix 𝛼 ε' kwf) with "Hcr Htape") as "[%junk [?|(_&Hcr)]]"; auto.
+  iExFalso; iApply ec_spend_1; last iFrame.
+  Set Printing Coercions.
+  rewrite /pos_to_nn /εAmp_iter /=.
+  replace (nonneg ε) with (pos ε') by auto.
+  done.
+Qed.
+
+Lemma presample_planner N prefix suffix 𝛼 ε (Hε : (0 < ε)%R) :
+  € ε -∗
+  (𝛼 ↪ (S N; prefix)) -∗
+  (∃ junk, 𝛼 ↪ (S N; prefix ++ junk ++ suffix)).
+Proof.
+  destruct suffix as [|h R].
+  - iIntros "_ Htape". iExists []. do 2 (rewrite -app_nil_end); iFrame.
+  - remember (h :: R) as suffix.
+    iApply presample_planner_pos; auto; try lia.
+    rewrite Heqsuffix cons_length.
+    lia.
+Qed.
+*)
+
 End rules.

From 9fc16b8a7bc64415e0379fd16980c44f04cb3a9e Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Wed, 3 Jan 2024 13:46:54 -0500
Subject: [PATCH 25/37] finish porting planner rule to WP

---
 theories/ub_logic/ub_rules.v | 202 ++++++++++++++++++++---------------
 1 file changed, 113 insertions(+), 89 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 5724810d..69aaeba1 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -4,8 +4,7 @@ From iris.proofmode Require Import proofmode.
 From clutch.prelude Require Import stdpp_ext.
 From clutch.prob_lang Require Import notation tactics metatheory.
 From clutch.prob_lang Require Export lang.
-From clutch.ub_logic Require Export lifting ectx_lifting primitive_laws proofmode.
-
+From clutch.ub_logic Require Export lifting ectx_lifting primitive_laws proofmode seq_amplification.
 
 Section metatheory.
 
@@ -897,22 +896,15 @@ Proof.
 Qed.
 
 
-(*
 Lemma ec_spend_irrel ε1 ε2 : (ε1.(nonneg) = ε2.(nonneg)) → € ε1 -∗ € ε2.
 Proof.
   iIntros (?) "?".
-  replace ε1 with ε2; first by iFrame.
-  by apply nnreal_ext.
+  replace ε1 with ε2; [iFrame|by apply nnreal_ext].
 Qed.
 
-Lemma ec_spend_1 ε1 : (1 <= ε1.(nonneg))%R → € ε1 -∗ False.
-Proof. Admitted.
 
-(** advanced composition on one tape *)
-(* not really sure what this lemma will look like in the real version? *)
-Lemma presample_adv_comp (N : nat) α ns (ε : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
-  SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε) →
-  (α ↪ (N; ns) ∗ € ε) -∗ (∃ s, (α ↪ (N; ns ++ [s])) ∗ €(ε2 s)).
+(* FIXME make this a wp rule *)
+Lemma ec_spend_1 ε1 : (1 <= ε1.(nonneg))%R → € ε1 -∗ False.
 Proof. Admitted.
 
 Lemma amplification_depth N L (ε : posreal) (kwf : kwf N L) : exists n : nat, (1 <= ε * (k N L kwf) ^ n)%R.
@@ -939,47 +931,53 @@ Qed.
 
 (* whenever i is strictly less than l (ie, (S i) <= l) we can amplify *)
 (* we'll need another rule for spending?, but that should be simple *)
-Lemma presample_amplify' N L kwf prefix (suffix_total suffix_remaining : list (fin (S N))) 𝛼 (ε : posreal) :
-  ⊢ ⌜ L = length suffix_total ⌝ →
-    ⌜ (0 < L)%nat ⌝ →
-    𝛼 ↪ (N; prefix) -∗
-    (€ (pos_to_nn ε)) -∗
-    ∀ (i : nat),
-      (∀ (HL : (i <= L)%nat),
-          (∃ junk, 𝛼 ↪ (N; prefix ++ junk) ∗ €(εAmp N L ε kwf)) ∨
-          ((𝛼 ↪ (N; prefix ++ (take i suffix_total))) ∗
-            € (εR N L i ε (mk_fRwf N L i kwf HL)))).
+Lemma presample_amplify' N z L e E Φ kwf prefix (suffix_total suffix_remaining : list (fin (S N))) α (ε : posreal) :
+  E = ∅ ->
+  TCEq N (Z.to_nat z) →
+  to_val e = None →
+  (∀ σ', reducible e σ') →
+  L = length suffix_total ->
+  (0 < L)%nat ->
+  (α ↪ (N; prefix) ∗
+   (€ (pos_to_nn ε))
+   ⊢ (∀ (i : nat) (HL : (i <= L)%nat),
+        (((∃ junk, α ↪ (N; prefix ++ junk) ∗ €(εAmp N L ε kwf)) ∨
+         (α ↪ (N; prefix ++ (take i suffix_total)) ∗ € (εR N L i ε (mk_fRwf N L i kwf HL))))
+         -∗ WP e @ E {{ Φ }})
+      -∗ WP e @ E {{ Φ }}))%I.
 Proof.
-  iIntros (Htotal HLpos) "Htape Hcr_initial"; iIntros (i).
+  iIntros (? ? ? ? Htotal HLpos) "(Htape & Hcr_initial)".
+  iIntros (i HL).
   iInduction i as [|i'] "IH" forall (suffix_remaining).
-  - iIntros (HL).
+  - iIntros "Hwp"; iApply "Hwp".
     iRight. iSplitL "Htape".
     + rewrite take_0 -app_nil_end. iFrame.
     + iApply ec_spend_irrel; last iFrame.
       rewrite /εR /fR /pos_to_nn /=; lra.
-  - iIntros "%HL".
+  - iIntros "Hwand".
     assert (HL' : (i' <= L)%nat) by lia.
-    iSpecialize ("IH" $! _ with "Htape Hcr_initial").
-    iSpecialize ("IH" $! HL').
-    iDestruct "IH" as "[[%junk(Htape&Hcr)]|(Htape&Hcr)]".
-    + iLeft; iExists junk; iFrame.
-    +
-      (* we need to do something different dependning on if (S i') is L? No. in that case we still need 1 amp*)
+    iSpecialize ("IH" $! HL' _ with "Htape Hcr_initial").
+    iApply "IH". iIntros "[[%junk(Htape&Hcr)]|(Htape&Hcr)]".
+    + iApply "Hwand".
+      iLeft; iExists junk. iFrame.
+    + (* we need to do something different dependning on if (S i') is L? No. in that case we still need 1 amp*)
       assert (Hi' : (i' < length suffix_total)%nat) by lia.
       destruct (lookup_ex i' suffix_total Hi') as [target Htarget].
       rewrite (take_S_r _ _ target); [|apply Htarget].
-      pose M := (εDistr_mean N L i' ε target (mk_fRwf N L (S i') kwf HL)).
-      iPoseProof (presample_adv_comp N 𝛼
-                   (prefix ++ take i' suffix_total)
-                   (εR N L i' ε (fRwf_dec_i N L i' _)) (εDistr N L i' ε target _) M) as "PS".
-      replace {| k_wf := kwf; i_ub := HL' |} with(fRwf_dec_i N L i' {| k_wf := kwf; i_ub := HL |});
-        last by apply fRwf_ext.
-      iSpecialize ("PS" with "[Htape Hcr]"); first iFrame.
-      iDestruct "PS" as "[%s (Htape&Hcr)]".
+      pose HMean := (εDistr_mean N L i' ε target (mk_fRwf N L (S i') kwf HL)).
+      wp_apply (wp_presample_adv_comp N α
+              (prefix ++ take i' suffix_total)
+              _ _ _ _
+              (εR N L i' ε (fRwf_dec_i N L i' _))
+              (εDistr N L i' ε target _)); eauto.
+      replace {| k_wf := kwf; i_ub := HL' |} with (fRwf_dec_i N L i' {| k_wf := kwf; i_ub := HL |}); [|apply fRwf_ext].
+      iFrame.
+      iIntros (s) "(Htape&Hcr)".
+      iApply "Hwand".
       (* NOW we can destruct and decide if we're left or right *)
       rewrite /εDistr.
       case_bool_decide.
-      * iRight. rewrite H app_assoc. iFrame.
+      * iRight. simplify_eq; rewrite app_assoc; iFrame.
       * iLeft. iExists (take i' suffix_total ++ [s]).
         replace (k_wf N L (S i') {| k_wf := kwf; i_ub := HL |}) with kwf; last by apply kwf_ext.
         rewrite -app_assoc; iFrame.
@@ -987,85 +985,111 @@ Proof.
 Qed.
 
 (* do one step in the amplification sequence *)
-Lemma presample_amplify N L prefix suffix 𝛼 (ε : posreal) (kwf: kwf N L) :
+Lemma wp_presample_amplify N z L e E Φ prefix suffix α (ε : posreal) (kwf: kwf N L) :
+  E = ∅ ->
+  TCEq N (Z.to_nat z) →
+  to_val e = None →
+  (∀ σ', reducible e σ') →
   L = (length suffix) ->
-  € (pos_to_nn ε) -∗
-  (𝛼 ↪ (N; prefix)) -∗
-  (𝛼 ↪ (N; prefix ++ suffix) ∨ (∃ junk, 𝛼 ↪ (N; prefix ++ junk) ∗ €(εAmp N L ε kwf))).
+  € (pos_to_nn ε) ∗
+  (α ↪ (N; prefix)) ∗
+  ((α ↪ (N; prefix ++ suffix) ∨ (∃ junk, α ↪ (N; prefix ++ junk) ∗ €(εAmp N L ε kwf))) -∗ WP e @ E {{ Φ }})
+  ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (Hl) "Hcr Htape".
-
+  iIntros (? ? ? ? Hl) "(Hcr & Htape & Hwp)".
   destruct suffix as [|s0 sr].
-  - iLeft. rewrite -app_nil_end. iFrame.
+  - iApply "Hwp". iLeft. rewrite -app_nil_end. iFrame.
   - remember (s0 :: sr) as suffix.
     assert (Hl_pos : (0 < L)%nat).
     { rewrite Hl Heqsuffix cons_length. lia. }
-    iPoseProof (presample_amplify' N L _ prefix suffix suffix 𝛼 ε $! Hl Hl_pos) as "X".
-    iSpecialize ("X" with "Htape Hcr").
-    iSpecialize ("X" $! L (le_n L)).
-    iDestruct "X" as "[H|(H&_)]".
-    + iRight. iApply "H".
-    + iLeft. rewrite Hl firstn_all. iFrame.
+    iApply (presample_amplify' with "[Htape Hcr]"); eauto; [iFrame|].
+    iIntros "[H|(H&_)]"; iApply "Hwp".
+    + iRight. by iFrame.
+    + iLeft. erewrite firstn_all; iFrame.
+ Unshelve. lia.
 Qed.
 
 
-Lemma seq_amplify N L d prefix suffix 𝛼 (ε : posreal) (kwf: kwf N L) :
+Lemma seq_amplify N z L e E Φ d prefix suffix α (ε : posreal) (kwf: kwf N L) :
+  E = ∅ ->
+  TCEq N (Z.to_nat z) →
+  to_val e = None →
+  (∀ σ', reducible e σ') →
   L = (length suffix) ->
-  € (pos_to_nn ε) -∗
-  (𝛼 ↪ (N; prefix)) -∗
-  (∃ junk,
-      𝛼 ↪ (N; prefix ++ junk ++ suffix) ∨ 𝛼 ↪ (N; prefix ++ junk) ∗ €(pos_to_nn (εAmp_iter N L d ε kwf))).
+  € (pos_to_nn ε) ∗
+  (α ↪ (N; prefix)) ∗
+  ((∃ junk, α ↪ (N; prefix ++ junk ++ suffix) ∨ α ↪ (N; prefix ++ junk) ∗ €(pos_to_nn (εAmp_iter N L d ε kwf)))
+   -∗ WP e @ E {{ Φ }})
+  ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (HL) "Hcr Htape".
+  iIntros (? ? ? ? HL) "(Hcr&Htape&Hwp)".
   iInduction (d) as [|d'] "IH".
-  - iExists []; rewrite app_nil_r. iRight. iFrame.
+  - iApply "Hwp".
+    iExists []; rewrite app_nil_r. iRight. iFrame.
     iApply ec_spend_irrel; last auto.
     by rewrite /εAmp_iter /pos_to_nn /= Rmult_1_r.
-  - iDestruct ("IH" with "Hcr Htape") as "[%junk [Hlucky|(Htape&Hcr)]]".
-    + iExists junk; iLeft; iFrame.
-    + rewrite -εAmp_iter_cmp.
-      iPoseProof (presample_amplify N L (prefix ++ junk) suffix 𝛼 (εAmp_iter N L d' ε kwf)) as "X"; try auto.
-      iDestruct ("X" with "Hcr Htape") as "[Hlucky|[%junk' (Htape&Hcr)]]".
-      * iExists junk; iLeft. rewrite -app_assoc; iFrame.
-      * iExists (junk ++ junk'); iRight.
-        rewrite app_assoc; iFrame.
+  - iApply ("IH" with "Hcr Htape").
+    iIntros "[%junk [Hlucky|(Htape&Hcr)]]".
+    + iApply "Hwp". iExists junk; iLeft; iFrame.
+    + iApply wp_presample_amplify; eauto; iFrame.
+      iIntros "[?|[%junk' (Htape&Hcr)]]"; iApply "Hwp".
+      * iExists _; iLeft.
+        rewrite -app_assoc.
+        iFrame.
+      * iExists _; iRight.
+        rewrite -app_assoc -εAmp_iter_cmp; iFrame.
 Qed.
 
 
-Lemma presample_planner_pos N prefix suffix 𝛼 ε (HN : (0 < N)%nat) (HL : (0 < (length suffix))%nat) (Hε : (0 < ε)%R) :
-  € ε -∗
-  (𝛼 ↪ (N; prefix)) -∗
-  (∃ junk, 𝛼 ↪ (N; prefix ++ junk ++ suffix)).
+Lemma presample_planner_pos N z e E Φ prefix suffix α (ε : nonnegreal) (HN : (0 < N)%nat) (HL : (0 < (length suffix))%nat) (Hε : (0 < ε)%R) :
+  E = ∅ ->
+  TCEq N (Z.to_nat z) →
+  to_val e = None →
+  (∀ σ', reducible e σ') →
+  € ε ∗
+  (α ↪ (N; prefix)) ∗
+  ((∃ junk, α ↪ (N; prefix ++ junk ++ suffix)) -∗ WP e @ E {{ Φ }})
+  ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros "Hcr Htape".
+  iIntros (? ? ? ?) "(Hcr & Htape & Hwp)".
   (* make the interface match the other coupling rules *)
   remember (length suffix) as L.
   assert (kwf : kwf N L). { apply mk_kwf; lia. }
   pose ε' := mkposreal ε.(nonneg) Hε.
   replace ε with (pos_to_nn ε'); last first.
   { rewrite /ε' /pos_to_nn. by apply nnreal_ext. }
-
   destruct (amplification_depth N L ε' kwf) as [d Hdepth].
-  iDestruct ((seq_amplify N L d prefix suffix 𝛼 ε' kwf) with "Hcr Htape") as "[%junk [?|(_&Hcr)]]"; auto.
-  iExFalso; iApply ec_spend_1; last iFrame.
-  Set Printing Coercions.
-  rewrite /pos_to_nn /εAmp_iter /=.
-  replace (nonneg ε) with (pos ε') by auto.
-  done.
+  iApply seq_amplify; eauto; iFrame.
+  iIntros "[%junk [?|(_&Hcr)]]".
+  + iApply "Hwp".
+    iExists _.
+    iFrame.
+  + iExFalso; iApply ec_spend_1; last iFrame.
+    rewrite /pos_to_nn /εAmp_iter /=.
+    replace (nonneg ε) with (pos ε') by auto.
+    done.
 Qed.
 
-Lemma presample_planner N prefix suffix 𝛼 ε (Hε : (0 < ε)%R) :
-  € ε -∗
-  (𝛼 ↪ (S N; prefix)) -∗
-  (∃ junk, 𝛼 ↪ (S N; prefix ++ junk ++ suffix)).
+Lemma presample_planner N z e E Φ prefix suffix α (ε : nonnegreal) (Hε : (0 < ε)%R) :
+  E = ∅ ->
+  TCEq N (Z.to_nat z) →
+  to_val e = None →
+  (∀ σ', reducible e σ') →
+  € ε ∗
+  (α ↪ (S N; prefix)) ∗
+  ((∃ junk, α ↪ (S N; prefix ++ junk ++ suffix)) -∗ WP e @ E {{ Φ }})
+  ⊢ WP e @ E {{ Φ }}.
 Proof.
+  iIntros (? ? ? ?).
   destruct suffix as [|h R].
-  - iIntros "_ Htape". iExists []. do 2 (rewrite -app_nil_end); iFrame.
+  - iIntros "(_ & Htape & Hwp)".
+    iApply "Hwp".
+    iExists [].
+    do 2 (rewrite -app_nil_end); iFrame.
   - remember (h :: R) as suffix.
-    iApply presample_planner_pos; auto; try lia.
-    rewrite Heqsuffix cons_length.
-    lia.
+    iApply presample_planner_pos; eauto; try lia.
+    + rewrite Heqsuffix cons_length; lia.
+    + by erewrite Nat2Z.id.
 Qed.
-*)
 
 End rules.

From acb791588e06efcfcb8878ad1f225095cd5e79dc Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Wed, 3 Jan 2024 18:29:16 -0500
Subject: [PATCH 26/37] prove amplification depth rule

---
 theories/ub_logic/ub_rules.v | 55 +++++++++++++++++++++++++++++++++---
 1 file changed, 51 insertions(+), 4 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 69aaeba1..2e832239 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -902,15 +902,62 @@ Proof.
   replace ε1 with ε2; [iFrame|by apply nnreal_ext].
 Qed.
 
+Lemma wp_ec_spend e E Φ ε :
+  (1 <= ε.(nonneg))%R →
+  (to_val e = None) ->
+  € ε -∗ WP e @ E {{ Φ }}.
+Proof.
+  iIntros (? Hred) "Hε".
+  rewrite ub_wp_unfold /ub_wp_pre /= Hred.
+  iIntros (σ1 ε0) "(_&Hε_supply)".
+  iExFalso.
+  (* we'd need *)
+Abort.
 
-(* FIXME make this a wp rule *)
 Lemma ec_spend_1 ε1 : (1 <= ε1.(nonneg))%R → € ε1 -∗ False.
 Proof. Admitted.
 
-Lemma amplification_depth N L (ε : posreal) (kwf : kwf N L) : exists n : nat, (1 <= ε * (k N L kwf) ^ n)%R.
+
+(* there has to be a better proof, fix this *)
+Lemma amplification_depth N L (ε : posreal) (kwf : kwf N L) :
+  exists n : nat, (1 <= ε * (k N L kwf) ^ n)%R.
 Proof.
-  (* shouldn't be too hard, it's the log *)
-Admitted.
+  destruct kwf.
+  intros.
+  remember (1 + 1 / (S N ^ L - 1))%R as β.
+  assert (H1 : Lim_seq.is_lim_seq (fun n => (β ^ n)%R) Rbar.p_infty).
+  { eapply Lim_seq.is_lim_seq_geom_p.
+    rewrite Heqβ.
+    apply (Rplus_lt_reg_l (-1)%R).
+    rewrite -Rplus_assoc Rplus_opp_l Rplus_0_l.
+    rewrite /Rdiv Rmult_1_l.
+    apply Rinv_0_lt_compat.
+    apply (Rplus_lt_reg_r 1%R).
+    rewrite Rplus_assoc Rplus_opp_l Rplus_0_r Rplus_0_l.
+    apply Rlt_pow_R1; auto.
+    apply lt_1_INR; lia.
+  }
+  rewrite /Lim_seq.is_lim_seq
+          /Hierarchy.filterlim
+          /Hierarchy.filter_le
+          /Hierarchy.eventually
+          /Hierarchy.filtermap
+          /= in H1.
+  specialize H1 with (fun r : R => (/ ε <= r)%R).
+  simpl in H1; destruct H1.
+  { exists (/ε)%R. intros. by apply Rlt_le. }
+  specialize H with x.
+  exists x.
+
+  apply (Rmult_le_reg_l (/ ε)%R).
+  - apply Rinv_0_lt_compat, cond_pos.
+  - rewrite -Rmult_assoc Rinv_l; last first.
+    { pose (cond_pos ε); lra. }
+    rewrite Rmult_1_l Rmult_1_r /k.
+    rewrite -Heqβ.
+    apply H.
+    done.
+Qed.
 
 
 Lemma lookup_ex {A} (n : nat) (L : list A) : (n < length L)%nat -> exists x, (L !! n) = Some x.

From 9e63f12206543905f764fba257face76dfc7f650 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 5 Jan 2024 14:24:30 -0500
Subject: [PATCH 27/37] push reducibility into exec_ub (in ub_weakestpre, 1
 admit)

---
 theories/ub_logic/ub_rules.v      |   1 -
 theories/ub_logic/ub_weakestpre.v | 126 ++++++++++++++++++------------
 2 files changed, 74 insertions(+), 53 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 2e832239..d75a4019 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -911,7 +911,6 @@ Proof.
   rewrite ub_wp_unfold /ub_wp_pre /= Hred.
   iIntros (σ1 ε0) "(_&Hε_supply)".
   iExFalso.
-  (* we'd need *)
 Abort.
 
 Lemma ec_spend_1 ε1 : (1 <= ε1.(nonneg))%R → € ε1 -∗ False.
diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 66408d6c..9c0aa8e2 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -48,17 +48,24 @@ Section exec_ub.
     (λ (x : nonnegreal * cfg Λ),
       let '(ε, (e1, σ1)) := x in
       (* [prim_step] *)
-      (∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
+      (∃ R (ε1 ε2 : nonnegreal),
+          ⌜reducible e1 σ1⌝ ∗
+          ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗
+          ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z ε2 ρ2 ) ∨
       (* [prim_step] with adv composition *)
       (∃ R (ε1 : nonnegreal) (ε2 : cfg Λ -> nonnegreal),
+          ⌜reducible e1 σ1⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
           ⌜ (ε1 + SeriesC (λ ρ, (prim_step e1 σ1 ρ) * ε2(ρ)) <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z (ε2 ρ2) ρ2 ) ∨
       (* [state_step]  *)
       ([∨ list] α ∈ get_active σ1,
       (* We allow an explicit weakening of the grading, but maybe it is not needed *)
-        (∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ ub_lift (state_step σ1 α) R ε1 ⌝ ∗
+        (∃ R (ε1 ε2 : nonnegreal),
+            ⌜reducible e1 σ1⌝ ∗
+            ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗
+            ⌜ ub_lift (state_step σ1 α) R ε1 ⌝ ∗
               ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ Φ (ε2,((e1, σ2))))) ∨
       (* [state_step] with adv composition*)
       ([∨ list] α ∈ get_active σ1,
@@ -93,11 +100,12 @@ Section exec_ub.
       iInduction (get_active σ1) as [| l] "IH" forall "H".
       { rewrite big_orL_nil //. }
       rewrite !big_orL_cons.
-      iDestruct "H" as "[(% & % & % & %Hsum & Hlift & HΦ) | H]".
+      iDestruct "H" as "[(% & % & % & %Hred & %Hsum & %Hlift & HΦ) | H]".
       + iLeft. iExists R2.
         iExists ε1. iExists _.
         iSplit; [try done|].
         iSplit; [try done|].
+        iSplit; [try done|].
         iIntros. iApply "Hwand". by iApply "HΦ".
       + iRight. by iApply "IH".
     - iRight; iRight; iRight.
@@ -119,14 +127,21 @@ Section exec_ub.
 
   Lemma exec_ub_unfold e1 σ1 Z ε :
     exec_ub e1 σ1 Z ε ≡
-      ((∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
+      ((∃ R (ε1 ε2 : nonnegreal),
+           ⌜reducible e1 σ1⌝ ∗
+           ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗
+           ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z ε2 ρ2 ) ∨
       (∃ R (ε1 : nonnegreal) (ε2 : cfg Λ -> nonnegreal),
+          ⌜reducible e1 σ1⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
           ⌜ (ε1 + SeriesC (λ ρ, (prim_step e1 σ1 ρ) * ε2(ρ)) <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z (ε2 ρ2) ρ2 ) ∨
       ([∨ list] α ∈ get_active σ1,
-        (∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ ub_lift (state_step σ1 α) R ε1 ⌝ ∗
+        (∃ R (ε1 ε2 : nonnegreal),
+            ⌜reducible e1 σ1⌝ ∗
+            ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗
+            ⌜ ub_lift (state_step σ1 α) R ε1 ⌝ ∗
               ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z ε2 )) ∨
       ([∨ list] α ∈ get_active σ1,
         (∃ R (ε1 : nonnegreal) (ε2 : cfg Λ -> nonnegreal),
@@ -151,24 +166,26 @@ Section exec_ub.
     iPoseProof (least_fixpoint_ind (exec_ub_pre Z) Φ with "[]") as "H"; last first.
     { iApply ("H" with "H_ub"). }
     iIntros "!#" ([ε'' [? σ']]). rewrite /exec_ub_pre.
-    iIntros "[ (% & % & % & % & H) | [ (% & % & % & % & % & % & H) | [ H | H ]]] %ε3 %Hleq' /="; simpl in Hleq'.
+    iIntros "[ (% & % & % & % & % & % & H) | [ (% & % & % & % & % & % & % & H) | [ H | H ]]] %ε3 %Hleq' /="; simpl in Hleq'.
     - rewrite least_fixpoint_unfold.
       iLeft. iExists _,_,_.
-      iSplit; [|done].
-      iPureIntro; etrans; done.
+      iSplit; [done|].
+      iSplit; [iPureIntro; etrans; done|].
+      iSplit; [done|].
+      done.
     - rewrite least_fixpoint_unfold.
       iRight;iLeft. iExists _,_,_.
-      iSplit; [|iSplit; [| iSplit]].
-      1,3,4:done.
+      iSplit; [|iSplit; [| iSplit; [| iSplit]]]; try done.
       iPureIntro; etrans; done.
     - rewrite least_fixpoint_unfold.
       iRight; iRight; iLeft.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
-      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hleq2 & %Hub & H)) | Ht]".
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hred & %Hleq2 & %Hub & H)) | Ht]".
       + iLeft.
         iExists R2. iExists ε1. iExists ε2.
+        iSplit; [ done |].
         iSplit; [ iPureIntro; lra | ].
         iSplit; [ done | ].
         iIntros.
@@ -209,10 +226,11 @@ Section exec_ub.
     iPoseProof (least_fixpoint_iter (exec_ub_pre Z1) Φ with "[]") as "H"; last first.
     { by iApply ("H" with "H_ub"). }
     iIntros "!#" ([ε'' [? σ']]). rewrite /exec_ub_pre.
-    iIntros "[ (% & % & % & % & % & H) | [ (% & % & % & % & % & % & H) | [H | H]] ] HZ /=".
+    iIntros "[ (% & % & % & % & % & % & H) | [ (% & % & % & % & % & % & % & H) | [H | H]] ] HZ /=".
     - rewrite least_fixpoint_unfold.
       iLeft. iExists _,_,_.
       iSplit; [done|].
+      iSplit; [done|].
       iSplit.
       { iPureIntro.
         by apply ub_lift_pos_R. }
@@ -223,6 +241,7 @@ Section exec_ub.
       iExists _,_,_.
       iSplit; [done|].
       iSplit; [done|].
+      iSplit; [done|].
       iSplit.
       { iPureIntro.
         by apply ub_lift_pos_R. }
@@ -233,8 +252,9 @@ Section exec_ub.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
-      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (% & % & H)) | Ht]".
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (% & % & % & H)) | Ht]".
       + iLeft. iExists R2. iExists ε1. iExists ε2.
+        iSplit; [done | ].
         iSplit; [iPureIntro; lra | ].
         iSplit; [done | ].
         iIntros.
@@ -295,10 +315,11 @@ Section exec_ub.
                  with "[]") as "H"; last first.
     { iIntros (?). iApply ("H" $! (_, (_, _)) with "Hub [//]"). }
     iIntros "!#" ([ε' [? σ']]). rewrite /exec_ub_pre.
-    iIntros "[(% & % & % & % & % & H) | [ (% & % & % & (%r & %Hr) & % & % & H) | [H | H]]] %Hv'".
+    iIntros "[(% & % & % & % & % & % & H) | [ (% & % & % & % & (%r & %Hr) & % & % & H) | [H | H]]] %Hv'".
     - rewrite least_fixpoint_unfold.
       iLeft. simpl.
       iExists (λ '(e2, σ2), ∃ e2', e2 = K e2' ∧ R2 (e2', σ2)),_,_.
+      iSplit; [iPureIntro; by apply reducible_fill|].
       iSplit; [done|].
       rewrite fill_dmap //=.
       iSplit.
@@ -331,6 +352,7 @@ Section exec_ub.
         rewrite /ε3 HKinv3 //.
       }
       iExists (λ '(e2, σ2), ∃ e2', e2 = K e2' ∧ R2 (e2', σ2)),_,ε3.
+      iSplit; [iPureIntro; by apply reducible_fill|].
       iSplit.
       {
         iPureIntro. exists r. intros (e&σ). rewrite /ε3.
@@ -350,7 +372,7 @@ Section exec_ub.
         - auto.
        }
       + iPureIntro.
-        etrans; [ | apply H0].
+        etrans; [ | apply H1].
         apply Rplus_le_compat_l.
         transitivity (SeriesC (λ '(e,σ), (prim_step (K o) σ' (K e, σ) * ε3 (K e, σ))%R)).
         * etrans; [ | eapply (SeriesC_le_inj _ (λ '(e,σ), (Kinv e ≫= (λ e', Some (e',σ)))))].
@@ -412,9 +434,10 @@ Section exec_ub.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
-      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hleq & %Hub & H)) | Ht]".
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hred & %Hleq & %Hub & H)) | Ht]".
       + iLeft.
         iExists _,_,_.
+        iSplit; [iPureIntro; by apply reducible_fill|].
         iSplit; [done|].
         iSplit; [done|].
         iIntros. by iApply ("H" with "[//]").
@@ -477,48 +500,53 @@ Section exec_ub.
 
 
   Lemma exec_ub_prim_step e1 σ1 Z (ε : nonnegreal) :
-    (∃ R (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
+    (∃ R (ε1 ε2 : nonnegreal), ⌜reducible e1 σ1⌝ ∗ ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
           ∀ ρ2 , ⌜R ρ2⌝ ={∅}=∗ Z ε2 ρ2)
     ⊢ exec_ub e1 σ1 Z ε.
   Proof.
-    iIntros "(% & % & % & % & % & H)".
+    iIntros "(% & % & % & % & % & % & H)".
     rewrite {1}exec_ub_unfold.
     iLeft.
     iExists _,_,_.
     iSplit; [done|].
+    iSplit; [done|].
     iSplit; done.
   Qed.
 
 
   Lemma exec_ub_adv_comp e1 σ1 Z (ε : nonnegreal) :
       (∃ R (ε1 : nonnegreal) (ε2 : cfg Λ -> nonnegreal),
+          ⌜reducible e1 σ1⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
           ⌜ (ε1 + SeriesC (λ ρ, (prim_step e1 σ1 ρ) * ε2(ρ)) <= ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R ε1⌝ ∗
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z (ε2 ρ2) ρ2 )
     ⊢ exec_ub e1 σ1 Z ε.
   Proof.
-    iIntros "(% & % & % & % & % & % & H)".
+    iIntros "(% & % & % & % & % & % & % & H)".
     rewrite {1}exec_ub_unfold.
     iRight; iLeft.
     iExists _,_,_.
     iSplit; [done|].
     iSplit; [done|].
+    iSplit; [done|].
     iSplit; done.
   Qed.
 
 
   Lemma exec_ub_adv_comp' e1 σ1 Z (ε : nonnegreal) :
       (∃ R (ε2 : cfg Λ -> nonnegreal),
+          ⌜reducible e1 σ1⌝ ∗
           ⌜ exists r, forall ρ, (ε2 ρ <= r)%R ⌝ ∗
           ⌜ (SeriesC (λ ρ, (prim_step e1 σ1 ρ) * ε2(ρ)) = ε)%R ⌝ ∗ ⌜ub_lift (prim_step e1 σ1) R nnreal_zero⌝ ∗
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z (ε2 ρ2) ρ2 )
     ⊢ exec_ub e1 σ1 Z ε.
   Proof.
-    iIntros "(% & % & % & %Hε & % & H)".
+    iIntros "(% & % & % & % & %Hε & % & H)".
     rewrite {1}exec_ub_unfold.
     iRight; iLeft.
     iExists _,nnreal_zero,_.
     iSplit; [done|].
+    iSplit; [done|].
     iSplit.
     { iPureIntro.
       simpl. rewrite Hε. lra.
@@ -529,12 +557,13 @@ Section exec_ub.
   (* TODO: Maybe allow weakening of the grading *)
   Lemma exec_ub_state_step α e1 σ1 Z (ε ε' : nonnegreal) :
     α ∈ get_active σ1 →
-    (∃ R, ⌜ub_lift (state_step σ1 α) R ε⌝ ∗
+    (∃ R, ⌜reducible e1 σ1⌝ ∗
+          ⌜ub_lift (state_step σ1 α) R ε⌝ ∗
           ∀ σ2 , ⌜R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z ε')
     ⊢ exec_ub e1 σ1 Z (ε + ε').
   Proof.
     iIntros (?) "H".
-    iDestruct "H" as (?) "H".
+    iDestruct "H" as (?) "(% & % & H)".
     rewrite {1}exec_ub_unfold.
     iRight; iRight; iLeft.
     iApply big_orL_elem_of; eauto.
@@ -543,7 +572,7 @@ Section exec_ub.
     iExists ε'.
     iFrame.
     iPureIntro.
-    simpl. lra.
+    by simpl.
   Qed.
 
 
@@ -685,7 +714,6 @@ Definition ub_wp_pre `{!irisGS Λ Σ}
   | Some v => |={E}=> Φ v
   | None => ∀ σ1 ε,
       state_interp σ1 ∗ err_interp ε ={E,∅}=∗
-      ⌜reducible e1 σ1⌝ ∗
       exec_ub e1 σ1 (λ ε2 '(e2, σ2),
         ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ wp E e2 Φ) ε
 end%I.
@@ -693,10 +721,10 @@ end%I.
 Local Instance wp_pre_contractive `{!irisGS Λ Σ} : Contractive (ub_wp_pre).
 Proof.
   rewrite /ub_wp_pre /= => n wp wp' Hwp E e1 Φ /=.
-  do 8 (f_equiv).
+  do 7 (f_equiv).
   apply least_fixpoint_ne_outer; [|done].
   intros Ψ [ε' [e' σ']]. rewrite /exec_ub_pre.
-  do 14 f_equiv.
+  do 15 f_equiv.
   { f_contractive. do 3 f_equiv. apply Hwp. }
   { do 2 f_equiv. f_contractive. do 3 f_equiv. apply Hwp. }
 Qed.
@@ -732,10 +760,10 @@ Global Instance ub_wp_ne s E e n :
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
   rewrite !ub_wp_unfold /ub_wp_pre /=.
-  do 8 f_equiv.
+  do 7 f_equiv.
   apply least_fixpoint_ne_outer; [|done].
   intros ? [? []]. rewrite /exec_ub_pre.
-  do 14 f_equiv.
+  do 15 f_equiv.
   { f_contractive. do 3 f_equiv. rewrite IH; [done|lia|].
     intros ?. eapply dist_S, HΦ. }
   { do 2 f_equiv. f_contractive. rewrite IH; [done|lia|].
@@ -752,10 +780,10 @@ Global Instance ub_wp_contractive s E e n :
   Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
 Proof.
   intros He Φ Ψ HΦ. rewrite !ub_wp_unfold /ub_wp_pre He /=.
-  do 7 f_equiv.
+  do 6 f_equiv.
   apply least_fixpoint_ne_outer; [|done].
   intros ? [? []]. rewrite /exec_ub_pre.
-  do 14 f_equiv.
+  do 15 f_equiv.
   { f_contractive. do 6 f_equiv. }
   { do 2 f_equiv. f_contractive. do 6 f_equiv. }
 Qed.
@@ -773,9 +801,7 @@ Proof.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1 ε) "[Hσ Hε]".
   iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
-  iMod ("H" with "[$]") as "[% H]".
-  iModIntro.
-  iSplit; [done | ].
+  iMod ("H" with "[$]") as "H".
   iApply (exec_ub_mono_pred with "[Hclose HΦ] H").
   iIntros (? [e2 σ2]) "H".
   iModIntro.
@@ -788,7 +814,7 @@ Lemma fupd_ub_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ
 Proof.
   rewrite ub_wp_unfold /ub_wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-  iIntros (σ1 ε) "Hi". iMod "H". by iApply "H".
+   iIntros (σ1 ε) "Hi". iMod "H". by iApply "H".
 Qed.
 Lemma ub_wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
 Proof. iIntros "H". iApply (ub_wp_strong_mono E with "H"); auto. Qed.
@@ -800,7 +826,7 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1 ε) "[Hσ Hε]". iMod "H".
-  iMod ("H" with "[$]") as "[$ H]".
+  iMod ("H" with "[$]") as "H".
   iModIntro.
   iDestruct (exec_ub_strengthen with "H") as "H".
   iApply (exec_ub_mono_pred with "[] H").
@@ -810,15 +836,15 @@ Proof.
   rewrite !ub_wp_unfold /ub_wp_pre.
   destruct (to_val e2) as [v2|] eqn:He2.
   - iDestruct "H" as ">> $". by iFrame.
-  - iMod ("H" with "[$]") as "(%&H)".
+  - iMod ("H" with "[$]") as "H".
     pose proof (atomic σ e2 σ2 Hstep) as H3.
     case_match.
     + rewrite /is_Some in H3.
       destruct H3.
       simplify_eq.
     + apply not_reducible in H3.
-      done.
-Qed.
+      admit.
+Admitted.
 
 
 Lemma ub_wp_step_fupd s E1 E2 e P Φ :
@@ -827,9 +853,8 @@ Lemma ub_wp_step_fupd s E1 E2 e P Φ :
 Proof.
   rewrite !ub_wp_unfold /ub_wp_pre. iIntros (-> ?) "HR H".
   iIntros (σ1 ε) "[Hσ Hε]". iMod "HR".
-  iMod ("H" with "[$Hσ $Hε]") as "[% H]".
+  iMod ("H" with "[$Hσ $Hε]") as "H".
   iModIntro.
-  iSplit; [done | ].
   iApply (exec_ub_mono_pred with "[HR] H").
   iIntros (? [e2 σ2]) "H".
   iModIntro.
@@ -848,19 +873,16 @@ Proof.
   { apply of_to_val in He as <-. by iApply fupd_ub_wp. }
   rewrite ub_wp_unfold /ub_wp_pre fill_not_val /=; [|done].
   iIntros (σ1 ε) "[Hσ Hε]".
-  iMod ("H" with "[$Hσ $Hε]") as "(%Hs & H)".
+  iMod ("H" with "[$Hσ $Hε]") as "H".
   iModIntro.
-  iSplit.
-  - iPureIntro.
-    apply reducible_fill; auto.
-  - iApply exec_ub_bind; [done |].
-    iApply (exec_ub_mono with "[] [] H").
-    + iPureIntro; lra.
-    + iIntros (? [e2 σ2]) "H".
-      iModIntro.
-      iMod "H" as "(Hσ & Hρ & H)".
-      iModIntro.
-      iFrame "Hσ Hρ". by iApply "IH".
+  iApply exec_ub_bind; [done |].
+  iApply (exec_ub_mono with "[] [] H").
+  - iPureIntro; lra.
+  - iIntros (? [e2 σ2]) "H".
+    iModIntro.
+    iMod "H" as "(Hσ & Hρ & H)".
+    iModIntro.
+    iFrame "Hσ Hρ". by iApply "IH".
 Qed.
 
 (* Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ : *)

From 9f1bed881ad77af3856b9fe5f23edb73e6f7f709 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 5 Jan 2024 14:30:21 -0500
Subject: [PATCH 28/37] push reducibility in lifting

---
 theories/ub_logic/lifting.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/ub_logic/lifting.v b/theories/ub_logic/lifting.v
index 4a83f361..e1ecbdcd 100644
--- a/theories/ub_logic/lifting.v
+++ b/theories/ub_logic/lifting.v
@@ -21,7 +21,6 @@ Lemma wp_lift_step_fupd_exec_ub E Φ e1 :
   (∀ σ1 ε,
     state_interp σ1 ∗ err_interp ε
     ={E,∅}=∗
-    ⌜reducible e1 σ1⌝ ∗
     exec_ub e1 σ1 (λ ε2 '(e2, σ2),
       ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ E {{ Φ }}) ε)
   ⊢ WP e1 @ E {{ Φ }}.
@@ -45,12 +44,13 @@ Proof.
   iApply wp_lift_step_fupd_exec_ub; [done|].
   iIntros (σ1 ε) "[Hσ Hε]".
   iMod ("H" with "Hσ") as "[%Hs H]". iModIntro.
-  iSplit; [done|].
   iApply (exec_ub_prim_step e1 σ1).
   iExists _.
   iExists nnreal_zero.
   iExists ε.
   iSplit.
+  { iPureIntro. simpl. done. }
+  iSplit.
   { iPureIntro. simpl. lra. }
   iSplit.
   { iPureIntro.

From 9c9ffadb899a29eafc6b102e4487c85e2e561051 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 5 Jan 2024 14:34:11 -0500
Subject: [PATCH 29/37] changes to adequacy

---
 theories/ub_logic/adequacy.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/ub_logic/adequacy.v b/theories/ub_logic/adequacy.v
index c07c3edc..598e25d7 100644
--- a/theories/ub_logic/adequacy.v
+++ b/theories/ub_logic/adequacy.v
@@ -69,7 +69,7 @@ Section adequacy.
     }
     clear.
     iIntros "!#" ([ε'' [e1 σ1]]). rewrite /Φ/F/exec_ub_pre.
-    iIntros "[ (%R & %ε1 & %ε2 & % & %Hlift & H)| [ (%R & %ε1 & %ε2 & (%r & %Hr) & % & %Hlift & H)| [H|H]]] %Hv".
+    iIntros "[ (%R & %ε1 & %ε2 & %Hred & % & %Hlift & H)| [ (%R & %ε1 & %ε2 & %Hred & (%r & %Hr) & % & %Hlift & H)| [H|H]]] %Hv".
     - iApply step_fupdN_mono.
       { apply pure_mono.
         eapply UB_mon_grading; eauto. }
@@ -94,7 +94,7 @@ Section adequacy.
                      |={∅}▷=>^(S n)
                        ⌜ub_lift (prim_step e1 σ1 ≫= exec n) φ ε''⌝)%I
                   with "H") as "H".
-      { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hleq & %Hlift & H)".
+      { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hleq & %Hlift & %Hred & H)".
         replace (prim_step e1 σ1) with (step (e1, σ1)) => //.
         rewrite -exec_Sn_not_final; [|eauto].
         iApply (step_fupdN_mono _ _ _
@@ -170,7 +170,7 @@ Section adequacy.
         apply (UB_mon_grading _ _ 0); [apply cond_nonneg | ].
         apply ub_lift_dret; auto.
       + rewrite ub_wp_unfold /ub_wp_pre /= Heq.
-        iMod ("Hwp" with "[$]") as "(%Hexec_ub & Hlift)".
+        iMod ("Hwp" with "[$]") as "Hlift".
         iModIntro.
         iPoseProof
           (exec_ub_mono _ (λ ε' '(e2, σ2), |={∅}▷=>^(S n)

From 2daebc9f61100a05ebd4e46744fb72ee00919dec Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 5 Jan 2024 14:41:16 -0500
Subject: [PATCH 30/37] remove reducibility from state steps in both cases

---
 theories/ub_logic/adequacy.v      |  2 +-
 theories/ub_logic/ub_weakestpre.v | 14 ++++----------
 2 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/theories/ub_logic/adequacy.v b/theories/ub_logic/adequacy.v
index 598e25d7..eb46c7eb 100644
--- a/theories/ub_logic/adequacy.v
+++ b/theories/ub_logic/adequacy.v
@@ -94,7 +94,7 @@ Section adequacy.
                      |={∅}▷=>^(S n)
                        ⌜ub_lift (prim_step e1 σ1 ≫= exec n) φ ε''⌝)%I
                   with "H") as "H".
-      { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hleq & %Hlift & %Hred & H)".
+      { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hleq & %Hlift & H)".
         replace (prim_step e1 σ1) with (step (e1, σ1)) => //.
         rewrite -exec_Sn_not_final; [|eauto].
         iApply (step_fupdN_mono _ _ _
diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 9c0aa8e2..3c61562b 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -63,7 +63,6 @@ Section exec_ub.
       ([∨ list] α ∈ get_active σ1,
       (* We allow an explicit weakening of the grading, but maybe it is not needed *)
         (∃ R (ε1 ε2 : nonnegreal),
-            ⌜reducible e1 σ1⌝ ∗
             ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗
             ⌜ ub_lift (state_step σ1 α) R ε1 ⌝ ∗
               ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ Φ (ε2,((e1, σ2))))) ∨
@@ -100,12 +99,11 @@ Section exec_ub.
       iInduction (get_active σ1) as [| l] "IH" forall "H".
       { rewrite big_orL_nil //. }
       rewrite !big_orL_cons.
-      iDestruct "H" as "[(% & % & % & %Hred & %Hsum & %Hlift & HΦ) | H]".
+      iDestruct "H" as "[(% & % & % & %Hsum & %Hlift & HΦ) | H]".
       + iLeft. iExists R2.
         iExists ε1. iExists _.
         iSplit; [try done|].
         iSplit; [try done|].
-        iSplit; [try done|].
         iIntros. iApply "Hwand". by iApply "HΦ".
       + iRight. by iApply "IH".
     - iRight; iRight; iRight.
@@ -139,7 +137,6 @@ Section exec_ub.
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z (ε2 ρ2) ρ2 ) ∨
       ([∨ list] α ∈ get_active σ1,
         (∃ R (ε1 ε2 : nonnegreal),
-            ⌜reducible e1 σ1⌝ ∗
             ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗
             ⌜ ub_lift (state_step σ1 α) R ε1 ⌝ ∗
               ∀ σ2, ⌜ R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z ε2 )) ∨
@@ -182,10 +179,9 @@ Section exec_ub.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
-      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hred & %Hleq2 & %Hub & H)) | Ht]".
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hleq2 & %Hub & H)) | Ht]".
       + iLeft.
         iExists R2. iExists ε1. iExists ε2.
-        iSplit; [ done |].
         iSplit; [ iPureIntro; lra | ].
         iSplit; [ done | ].
         iIntros.
@@ -252,9 +248,8 @@ Section exec_ub.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
-      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (% & % & % & H)) | Ht]".
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (% & % & H)) | Ht]".
       + iLeft. iExists R2. iExists ε1. iExists ε2.
-        iSplit; [done | ].
         iSplit; [iPureIntro; lra | ].
         iSplit; [done | ].
         iIntros.
@@ -434,10 +429,9 @@ Section exec_ub.
       iInduction (get_active σ') as [| l] "IH".
       { rewrite big_orL_nil //. }
       rewrite 2!big_orL_cons.
-      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hred & %Hleq & %Hub & H)) | Ht]".
+      iDestruct "H" as "[(%R2 & %ε1 & %ε2 & (%Hleq & %Hub & H)) | Ht]".
       + iLeft.
         iExists _,_,_.
-        iSplit; [iPureIntro; by apply reducible_fill|].
         iSplit; [done|].
         iSplit; [done|].
         iIntros. by iApply ("H" with "[//]").

From 58f35d4bb381d3b5914870c88bbdda7cea92a30a Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 5 Jan 2024 15:44:45 -0500
Subject: [PATCH 31/37] move reducibility (1 admit)

---
 theories/ub_logic/ub_rules.v      | 89 ++++++++++++-------------------
 theories/ub_logic/ub_weakestpre.v | 12 +++--
 2 files changed, 42 insertions(+), 59 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index d75a4019..5d670466 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -167,7 +167,6 @@ Proof.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
-  solve_red.
   iDestruct (ec_supply_bound with "Hε Herr ") as %Hle.
   set (ε' := nnreal_minus ε (nnreal_inv (nnreal_nat (Z.to_nat z + 1))) Hle ).
   replace ε with (nnreal_plus (nnreal_inv (nnreal_nat (Z.to_nat z + 1))) ε'); last first.
@@ -177,6 +176,8 @@ Proof.
       (λ (ρ : expr * state),
         ∃ (n : fin (S (Z.to_nat z))), n ≠ m /\ ρ = (Val #n, σ1)), _, _.
   iSplit.
+  { iPureIntro. solve_red. }
+  iSplit.
   {
     iPureIntro.
     apply Rle_refl.
@@ -223,7 +224,6 @@ Proof.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
-  solve_red.
   iDestruct (ec_supply_bound with "Hε Herr ") as %Hle.
   set (ε' := nnreal_minus ε (nnreal_inv (nnreal_nat (Z.to_nat z + 1))) Hle ).
   replace ε with (nnreal_plus (nnreal_inv (nnreal_nat (Z.to_nat z + 1))) ε'); last first.
@@ -232,6 +232,7 @@ Proof.
   iExists
       (λ (ρ : expr * state),
         ∃ (n : fin (S (Z.to_nat z))), fin_to_nat n ≠ m /\ ρ = (Val #n, σ1)),_,_.
+  iSplit. { iPureIntro. solve_red. }
   iSplit.
   {
     iPureIntro; apply Rle_refl.
@@ -278,7 +279,6 @@ Proof.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
-  solve_red.
   iDestruct (ec_supply_bound with "Hε Herr ") as %Hle.
   set (ε' := nnreal_minus ε (nnreal_div (nnreal_nat (length ns)) (nnreal_nat (Z.to_nat z + 1))) Hle ).
   replace ε with (nnreal_plus (nnreal_div (nnreal_nat (length ns)) (nnreal_nat (Z.to_nat z + 1))) ε'); last first.
@@ -287,6 +287,7 @@ Proof.
   iExists
       (λ (ρ : expr * state),
         ∃ (n : fin (S (Z.to_nat z))), Forall (λ m, fin_to_nat n ≠ m) ns /\ ρ = (Val #n, σ1)),_,_.
+  iSplit. {iPureIntro. solve_red. }
   iSplit.
   {
     iPureIntro; apply Rle_refl.
@@ -333,7 +334,6 @@ Proof.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
-  solve_red.
   iDestruct (ec_supply_bound with "Hε Herr ") as %Hle.
   set (ε' := nnreal_minus ε (nnreal_div (nnreal_nat (length zs)) (nnreal_nat (Z.to_nat z + 1))) Hle ).
   replace ε with (nnreal_plus (nnreal_div (nnreal_nat (length zs)) (nnreal_nat (Z.to_nat z + 1))) ε'); last first.
@@ -342,6 +342,7 @@ Proof.
   iExists
       (λ (ρ : expr * state),
         ∃ (n : fin (S (Z.to_nat z))), Forall (λ m, Z.of_nat (fin_to_nat n) ≠ m) zs /\ ρ = (Val #n, σ1)),_,_.
+  iSplit. { iPureIntro. solve_red. }
   iSplit.
   {
     iPureIntro; apply Rle_refl.
@@ -425,7 +426,6 @@ Proof.
   iIntros (σ1 ε_now) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
-  solve_red.
   iApply exec_ub_adv_comp; simpl.
   iDestruct (ec_split_supply with "Hε Herr") as (ε3) "%Hε3".
   (* ε3 is the amount of credit supply left outside of ε1 (?) *)
@@ -445,6 +445,7 @@ Proof.
   iExists
       (λ (ρ : expr * state),
         ∃ (n : fin (S (Z.to_nat z))), ρ = (Val #n, σ1)), nnreal_zero, foo.
+  iSplit. { iPureIntro. solve_red. }
   iSplit.
   {
     iPureIntro. exists (ε3 + r)%R.
@@ -610,24 +611,22 @@ Qed.
 (** adapted from wp_couple_tapes in the relational logic *)
 Lemma wp_presample (N : nat) E e 𝛼 ns Φ :
   to_val e = None →
-  (∀ σ', reducible e σ') →
   ▷ 𝛼 ↪ (N; ns) ∗
   (∀ (n : fin (S N)), 𝛼 ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-    iIntros (He Hred) "(>H𝛼&Hwp)".
+    iIntros (He) "(>H𝛼&Hwp)".
     iApply wp_lift_step_fupd_exec_ub; [done|].
     iIntros (𝜎 ε) "((Hheap&Htapes)&Hε)".
     iDestruct (ghost_map_lookup with "Htapes H𝛼") as %Hlookup.
     iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'".
-    iSplitR; [done|].
     (* now we need to prove an exec_ub, we should be able to do this with a state step. *)
     replace ε with (nnreal_zero + ε)%NNR by (apply nnreal_ext; simpl; lra).
     iApply exec_ub_state_step.
     { rewrite /= /get_active.
       by apply elem_of_list_In, elem_of_list_In, elem_of_elements, elem_of_dom. }
     iExists _.
-    iSplit.
+    iSplitR.
     { iPureIntro. apply ub_lift_state, Hlookup. }
     iIntros (𝜎') "[%n %H𝜎']".
     (* now we have to prove the exec_ub about 𝜎', we should be able to do this with the wp *)
@@ -638,7 +637,7 @@ Proof.
     iSpecialize ("Hwp" $! n with "H𝛼").
     rewrite !ub_wp_unfold /ub_wp_pre /= He.
     iSpecialize ("Hwp" $! 𝜎' ε).
-    iMod ("Hwp" with "[Hheap Htapes Hε]") as "(?&Hwp)".
+    iMod ("Hwp" with "[Hheap Htapes Hε]") as "Hwp".
     { replace (nnreal_zero + ε)%NNR with ε by (apply nnreal_ext; simpl; lra).
       rewrite H𝜎'.
       iFrame.
@@ -667,30 +666,6 @@ refine(
 Defined.
 
 
-Lemma compute_ε2_in_state_expr e σ N z ε2 H :
-  to_val e = None ->
-  compute_ε2_in_state (e, σ) N z ε2 H = nnreal_zero.
-Proof.
-  intros; rewrite /compute_ε2_in_state; simpl.
-  case_match; auto.
-  simplify_eq.
-Qed.
-
-
-Check (fun (s : state) => s.(tapes)).
-Check (fun α z ns sample=> (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample]) : tape]> )).
-Check (fun σ σ' α z ns N => (exists s : fin _, σ' = (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s]) : tape]> σ))).
-Check (fun σ σ' α z ns N =>
-            match exists_dec (fun s : fin _ => σ' = (state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s]) : tape]> σ)) with
-                | left H => _ H
-                | right H => nnreal_zero
-              end).
-
-(* I'll admit this for now to see if the rest of the proof works  *)
-
-(* really this should not depend on the expr at all :/*)
-
-
 Definition compute_ε2 (σ : state) (ρ : cfg) α N ns (ε2 : fin (S N) -> nonnegreal) : nonnegreal :=
   match finite.find (fun s => state_upd_tapes <[α:=(N; ns ++ [s]) : tape]> σ = snd ρ) with
     | Some s => ε2 s
@@ -702,21 +677,19 @@ Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 :
   E = ∅ -> (* can this really only be proven when E = ∅ or can we improve this? *)
   TCEq N (Z.to_nat z) →
   to_val e = None →
-  (∀ σ', reducible e σ') →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
   α ↪ (N; ns) ∗
   € ε1 ∗
   (∀ (n : fin (S N)), € (ε2 n) ∗ α ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? -> Hred Hσ_red Hsum) "(Hα & Hε & Hwp)".
+  iIntros (? -> Hσ_red Hsum) "(Hα & Hε & Hwp)".
   iApply wp_lift_step_fupd_exec_ub; [done|].
   iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
   iDestruct (ghost_map_lookup with "Htapes Hα") as %Hlookup.
   iDestruct (ec_supply_bound with "Hε_supply Hε") as %Hε1_ub.
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose".
-  iSplitR; [auto|].
   iApply (exec_ub_state_adv_comp' α); simpl.
   { rewrite /get_active.
     apply elem_of_list_In, elem_of_list_In, elem_of_elements, elem_of_dom.
@@ -850,25 +823,25 @@ Proof.
   iMod (ec_increase_supply _ (ε2 sample) with "Hε_supply") as "[Hε_supply Hε]".
   iMod (ghost_map_update ((Z.to_nat z; ns ++ [sample]) : tape) with "Htapes Hα") as "[Htapes Hα]".
   iSpecialize ("Hwp" $! sample).
-
   (* open the WP and specialize it to get the goal *)
   rewrite ub_wp_unfold /ub_wp_pre.
   iAssert (⌜ (common.language.to_val e) = None ⌝)%I as "%X". { auto. }
   rewrite X; clear X.
   (* then we should be able to specialize using the updated ghost state.. *)
 
-  iAssert (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝ ={∅,E}=∗ emp)%I with "[Hclose]" as "HcloseW".
-  { iIntros; iFrame. }
+  (* iAssert (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝ ={∅,E}=∗ emp)%I with "[Hclose]" as "HcloseW".
+  { iIntros; iFrame. } *)
 
+  (*
   iPoseProof (fupd_trans_frame E ∅ E _ (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝))%I as "HR".
-  iSpecialize ("HR" with "[Hwp Hheap Hε_supply Hε Htapes Hα HcloseW]").
+  iSpecialize ("HR" with "[Hwp Hheap Hε_supply Hε Htapes Hα Hclose]").
   { iFrame.
     iApply ("Hwp" with "[Hε Hα]"). { iFrame. }
     rewrite /state_interp /=.
     rewrite /state_upd_tapes in Hsample.
     inversion Hsample.
     iFrame. }
-
+    *)
   rewrite Hsample /compute_ε2 /=.
   destruct (@find_is_Some _ _ _
                (λ s : fin (S (Z.to_nat z)), state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s])]> σ1 = state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample])]> σ1)
@@ -888,11 +861,22 @@ Proof.
     apply app_inv_head in Heqt.
     by inversion Heqt. }
 
-  iApply fupd_mask_mono; last done.
-
+  (* iSpecialize ("Hwp" with "[Hwp Hheap Hε_supply Hε Htapes Hα HcloseW]"). *)
+  iSpecialize ("Hwp" with "[Hε Hα]"); first iFrame.
+  remember {| heap := heap2; tapes := tapes2 |} as σ2.
+  iSpecialize ("Hwp" $! σ2 _).
+  iSpecialize ("Hwp" with "[Hheap Htapes Hε_supply]").
+  { iSplitL "Hheap Htapes".
+    - rewrite /tapes_auth.
+      rewrite Heqσ2 in Hsample. inversion Hsample.
+      simplify_eq. simpl. iFrame.
+    - iFrame. }
+
+  rewrite -Hsample.
   (* FIXME I can't see where this could be improved in the proof, but I also see no reason why it could't.
       (related to the prophecy counterexample? idk. )*)
-  set_solver.
+  simplify_eq.
+  done.
 Qed.
 
 
@@ -981,7 +965,6 @@ Lemma presample_amplify' N z L e E Φ kwf prefix (suffix_total suffix_remaining
   E = ∅ ->
   TCEq N (Z.to_nat z) →
   to_val e = None →
-  (∀ σ', reducible e σ') →
   L = length suffix_total ->
   (0 < L)%nat ->
   (α ↪ (N; prefix) ∗
@@ -992,7 +975,7 @@ Lemma presample_amplify' N z L e E Φ kwf prefix (suffix_total suffix_remaining
          -∗ WP e @ E {{ Φ }})
       -∗ WP e @ E {{ Φ }}))%I.
 Proof.
-  iIntros (? ? ? ? Htotal HLpos) "(Htape & Hcr_initial)".
+  iIntros (? ? ? Htotal HLpos) "(Htape & Hcr_initial)".
   iIntros (i HL).
   iInduction i as [|i'] "IH" forall (suffix_remaining).
   - iIntros "Hwp"; iApply "Hwp".
@@ -1035,14 +1018,13 @@ Lemma wp_presample_amplify N z L e E Φ prefix suffix α (ε : posreal) (kwf: kw
   E = ∅ ->
   TCEq N (Z.to_nat z) →
   to_val e = None →
-  (∀ σ', reducible e σ') →
   L = (length suffix) ->
   € (pos_to_nn ε) ∗
   (α ↪ (N; prefix)) ∗
   ((α ↪ (N; prefix ++ suffix) ∨ (∃ junk, α ↪ (N; prefix ++ junk) ∗ €(εAmp N L ε kwf))) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? ? ? ? Hl) "(Hcr & Htape & Hwp)".
+  iIntros (? ? ? Hl) "(Hcr & Htape & Hwp)".
   destruct suffix as [|s0 sr].
   - iApply "Hwp". iLeft. rewrite -app_nil_end. iFrame.
   - remember (s0 :: sr) as suffix.
@@ -1060,7 +1042,6 @@ Lemma seq_amplify N z L e E Φ d prefix suffix α (ε : posreal) (kwf: kwf N L)
   E = ∅ ->
   TCEq N (Z.to_nat z) →
   to_val e = None →
-  (∀ σ', reducible e σ') →
   L = (length suffix) ->
   € (pos_to_nn ε) ∗
   (α ↪ (N; prefix)) ∗
@@ -1068,7 +1049,7 @@ Lemma seq_amplify N z L e E Φ d prefix suffix α (ε : posreal) (kwf: kwf N L)
    -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? ? ? ? HL) "(Hcr&Htape&Hwp)".
+  iIntros (? ? ? HL) "(Hcr&Htape&Hwp)".
   iInduction (d) as [|d'] "IH".
   - iApply "Hwp".
     iExists []; rewrite app_nil_r. iRight. iFrame.
@@ -1091,13 +1072,12 @@ Lemma presample_planner_pos N z e E Φ prefix suffix α (ε : nonnegreal) (HN :
   E = ∅ ->
   TCEq N (Z.to_nat z) →
   to_val e = None →
-  (∀ σ', reducible e σ') →
   € ε ∗
   (α ↪ (N; prefix)) ∗
   ((∃ junk, α ↪ (N; prefix ++ junk ++ suffix)) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? ? ? ?) "(Hcr & Htape & Hwp)".
+  iIntros (? ? ?) "(Hcr & Htape & Hwp)".
   (* make the interface match the other coupling rules *)
   remember (length suffix) as L.
   assert (kwf : kwf N L). { apply mk_kwf; lia. }
@@ -1120,13 +1100,12 @@ Lemma presample_planner N z e E Φ prefix suffix α (ε : nonnegreal) (Hε : (0
   E = ∅ ->
   TCEq N (Z.to_nat z) →
   to_val e = None →
-  (∀ σ', reducible e σ') →
   € ε ∗
   (α ↪ (S N; prefix)) ∗
   ((∃ junk, α ↪ (S N; prefix ++ junk ++ suffix)) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? ? ? ?).
+  iIntros (? ? ?).
   destruct suffix as [|h R].
   - iIntros "(_ & Htape & Hwp)".
     iApply "Hwp".
diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 3c61562b..9da63cda 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -551,13 +551,12 @@ Section exec_ub.
   (* TODO: Maybe allow weakening of the grading *)
   Lemma exec_ub_state_step α e1 σ1 Z (ε ε' : nonnegreal) :
     α ∈ get_active σ1 →
-    (∃ R, ⌜reducible e1 σ1⌝ ∗
-          ⌜ub_lift (state_step σ1 α) R ε⌝ ∗
+    (∃ R, ⌜ub_lift (state_step σ1 α) R ε⌝ ∗
           ∀ σ2 , ⌜R σ2 ⌝ ={∅}=∗ exec_ub e1 σ2 Z ε')
     ⊢ exec_ub e1 σ1 Z (ε + ε').
   Proof.
     iIntros (?) "H".
-    iDestruct "H" as (?) "(% & % & H)".
+    iDestruct "H" as (?) "(% & H)".
     rewrite {1}exec_ub_unfold.
     iRight; iRight; iLeft.
     iApply big_orL_elem_of; eauto.
@@ -837,7 +836,12 @@ Proof.
       destruct H3.
       simplify_eq.
     + apply not_reducible in H3.
-      admit.
+      (* so... we could get this back if we did a case match on
+         the exec_ub in H. We would need to exclude the two state step cases somehow. *)
+      rewrite {1}exec_ub_unfold.
+      iDestruct "H" as "[[% [% [% (%Hred&_)]]]|[[% [% [% (%Hred&_)]]]|[H|H]]]".
+      1,2: by destruct H3.
+      (* ??? *)
 Admitted.
 
 

From 313f037d635a4a3f10d5da8aa04c4e0cacef4b7c Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Fri, 5 Jan 2024 16:19:09 -0500
Subject: [PATCH 32/37] small cleanup

---
 theories/ub_logic/ub_rules.v | 46 +-----------------------------------
 1 file changed, 1 insertion(+), 45 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 5d670466..4bf68f7f 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -646,26 +646,6 @@ Proof.
 Qed.
 
 
-
-(* old (broken?) version *)
-Definition compute_ε2_in_state (ρ : expr * state) N z (ε2 : fin (S N) -> nonnegreal) (_ : TCEq N (Z.to_nat z)) : nonnegreal.
-refine(
-  match ρ with
-  | (Val (LitV (LitInt n)), σ) =>
-      if bool_decide (0 <= n)%Z
-      then match (lt_dec (Z.to_nat n) (S (Z.to_nat z))) with
-             | left H => ε2 (@Fin.of_nat_lt (Z.to_nat n) _ _)
-             | _ => nnreal_zero
-            end
-      else nnreal_zero
-  | _ => nnreal_zero
-  end).
-  eapply Nat.le_trans.
-  - apply Nat.le_succ_l, H.
-  - apply Nat.eq_le_incl, eq_S. symmetry. by apply TCEq_eq.
-Defined.
-
-
 Definition compute_ε2 (σ : state) (ρ : cfg) α N ns (ε2 : fin (S N) -> nonnegreal) : nonnegreal :=
   match finite.find (fun s => state_upd_tapes <[α:=(N; ns ++ [s]) : tape]> σ = snd ρ) with
     | Some s => ε2 s
@@ -827,21 +807,6 @@ Proof.
   rewrite ub_wp_unfold /ub_wp_pre.
   iAssert (⌜ (common.language.to_val e) = None ⌝)%I as "%X". { auto. }
   rewrite X; clear X.
-  (* then we should be able to specialize using the updated ghost state.. *)
-
-  (* iAssert (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝ ={∅,E}=∗ emp)%I with "[Hclose]" as "HcloseW".
-  { iIntros; iFrame. } *)
-
-  (*
-  iPoseProof (fupd_trans_frame E ∅ E _ (⌜reducible e {| heap := heap2; tapes := tapes2 |}⌝))%I as "HR".
-  iSpecialize ("HR" with "[Hwp Hheap Hε_supply Hε Htapes Hα Hclose]").
-  { iFrame.
-    iApply ("Hwp" with "[Hε Hα]"). { iFrame. }
-    rewrite /state_interp /=.
-    rewrite /state_upd_tapes in Hsample.
-    inversion Hsample.
-    iFrame. }
-    *)
   rewrite Hsample /compute_ε2 /=.
   destruct (@find_is_Some _ _ _
                (λ s : fin (S (Z.to_nat z)), state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s])]> σ1 = state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample])]> σ1)
@@ -850,7 +815,6 @@ Proof.
   rewrite Hfind.
   replace r with sample; last first.
   { rewrite /state_upd_tapes in Hr.
-    (* again: I want to destruct this equality *)
     inversion Hr as [Heqt].
     apply (insert_inv (tapes σ1) α) in Heqt.
     (* FIXME is there a way around using clasical theorem here?
@@ -860,8 +824,6 @@ Proof.
     apply classic_proof_irrel.PIT.EqdepTheory.inj_pair2 in Heqt.
     apply app_inv_head in Heqt.
     by inversion Heqt. }
-
-  (* iSpecialize ("Hwp" with "[Hwp Hheap Hε_supply Hε Htapes Hα HcloseW]"). *)
   iSpecialize ("Hwp" with "[Hε Hα]"); first iFrame.
   remember {| heap := heap2; tapes := tapes2 |} as σ2.
   iSpecialize ("Hwp" $! σ2 _).
@@ -871,7 +833,6 @@ Proof.
       rewrite Heqσ2 in Hsample. inversion Hsample.
       simplify_eq. simpl. iFrame.
     - iFrame. }
-
   rewrite -Hsample.
   (* FIXME I can't see where this could be improved in the proof, but I also see no reason why it could't.
       (related to the prophecy counterexample? idk. )*)
@@ -959,8 +920,6 @@ Proof.
 Qed.
 
 
-(* whenever i is strictly less than l (ie, (S i) <= l) we can amplify *)
-(* we'll need another rule for spending?, but that should be simple *)
 Lemma presample_amplify' N z L e E Φ kwf prefix (suffix_total suffix_remaining : list (fin (S N))) α (ε : posreal) :
   E = ∅ ->
   TCEq N (Z.to_nat z) →
@@ -989,8 +948,7 @@ Proof.
     iApply "IH". iIntros "[[%junk(Htape&Hcr)]|(Htape&Hcr)]".
     + iApply "Hwand".
       iLeft; iExists junk. iFrame.
-    + (* we need to do something different dependning on if (S i') is L? No. in that case we still need 1 amp*)
-      assert (Hi' : (i' < length suffix_total)%nat) by lia.
+    + assert (Hi' : (i' < length suffix_total)%nat) by lia.
       destruct (lookup_ex i' suffix_total Hi') as [target Htarget].
       rewrite (take_S_r _ _ target); [|apply Htarget].
       pose HMean := (εDistr_mean N L i' ε target (mk_fRwf N L (S i') kwf HL)).
@@ -1003,7 +961,6 @@ Proof.
       iFrame.
       iIntros (s) "(Htape&Hcr)".
       iApply "Hwand".
-      (* NOW we can destruct and decide if we're left or right *)
       rewrite /εDistr.
       case_bool_decide.
       * iRight. simplify_eq; rewrite app_assoc; iFrame.
@@ -1078,7 +1035,6 @@ Lemma presample_planner_pos N z e E Φ prefix suffix α (ε : nonnegreal) (HN :
   ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (? ? ?) "(Hcr & Htape & Hwp)".
-  (* make the interface match the other coupling rules *)
   remember (length suffix) as L.
   assert (kwf : kwf N L). { apply mk_kwf; lia. }
   pose ε' := mkposreal ε.(nonneg) Hε.

From 5a880bcaf0dfcf2a485e2f82d533485f6328c7d1 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 8 Jan 2024 10:19:40 -0500
Subject: [PATCH 33/37] fix ub_wp_atomic

---
 theories/ub_logic/ub_weakestpre.v | 30 +++++++++++++++++++++++++++---
 1 file changed, 27 insertions(+), 3 deletions(-)

diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 9da63cda..5156656f 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -812,6 +812,30 @@ Qed.
 Lemma ub_wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
 Proof. iIntros "H". iApply (ub_wp_strong_mono E with "H"); auto. Qed.
 
+Lemma ub_wp_atomic E1 E2 e Φ `{!Atomic StronglyAtomic e} a :
+  (|={E1,E2}=> WP e @ a; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ a; E1 {{ Φ }}.
+Proof.
+  iIntros "H".
+  rewrite !ub_wp_unfold /ub_wp_pre.
+  destruct (to_val e) as [v|] eqn:He; [by do 2 iMod "H"|].
+  iIntros (σ1 ε1) "(Hσ&Hε)".
+  iSpecialize ("H" $! σ1 ε1).
+  iMod ("H" with "[Hσ Hε]") as "H"; [iFrame|].
+  iMod "H"; iModIntro.
+  iApply (exec_ub_strong_mono with "[] [] H"); [done|].
+  iIntros (e2 σ2 ε2) "([%σ' %Hstep]&H)".
+  iNext.
+  iMod "H" as "(Hσ&Hε&Hwp)".
+  rewrite !ub_wp_unfold /ub_wp_pre.
+  destruct (to_val e2) as [?|] eqn:He2.
+  + iFrame. do 2 (iMod "Hwp"). by do 2 iModIntro.
+  + iMod ("Hwp" $! _ _ with "[Hσ Hε]") as "Hwp"; [iFrame|].
+    specialize (atomic _ _ _ Hstep) as Hatomic. (* key step *)
+    destruct Hatomic.
+    congruence. (* how do we do this "by hand"? Not obvious to me *)
+Qed.
+
+(* Fixable?
 Lemma ub_wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
   (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
 Proof.
@@ -843,7 +867,7 @@ Proof.
       1,2: by destruct H3.
       (* ??? *)
 Admitted.
-
+*)
 
 Lemma ub_wp_step_fupd s E1 E2 e P Φ :
   TCEq (to_val e) None → E2 ⊆ E1 →
@@ -999,7 +1023,7 @@ Section proofmode_classes.
   Qed.
 
   Global Instance elim_modal_fupd_ub_wp_atomic p s E1 E2 e P Φ :
-    ElimModal (Atomic WeaklyAtomic e) p false
+    ElimModal (Atomic StronglyAtomic e) p false
             (|={E1,E2}=> P) P
             (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof.
@@ -1013,7 +1037,7 @@ Section proofmode_classes.
   Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_ub_wp. Qed.
 
   Global Instance elim_acc_ub_wp_atomic {X} E1 E2 α β γ e s Φ :
-    ElimAcc (X:=X) (Atomic WeaklyAtomic e)
+    ElimAcc (X:=X) (Atomic StronglyAtomic e)
             (fupd E1 E2) (fupd E2 E1)
             α β γ (WP e @ s; E1 {{ Φ }})
             (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I | 100.

From d0abf4a876fee56d852c14d428619ad988d4f811 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 8 Jan 2024 10:29:05 -0500
Subject: [PATCH 34/37] cleanup countable_sum

---
 theories/prob/countable_sum.v | 30 ++++++++++--------------------
 1 file changed, 10 insertions(+), 20 deletions(-)

diff --git a/theories/prob/countable_sum.v b/theories/prob/countable_sum.v
index a7554fdb..6d2084fa 100644
--- a/theories/prob/countable_sum.v
+++ b/theories/prob/countable_sum.v
@@ -378,20 +378,6 @@ Section filter.
 
   Implicit Types P Q : A → Prop.
 
-  Lemma is_seriesC_singleton (a : A) v :
-    is_seriesC (λ (n : A), if bool_decide (n = a) then v else 0) v.
-  Proof.
-    rewrite /is_seriesC.
-    eapply is_series_ext; [|apply (is_series_singleton (encode_nat a))].
-    intros n =>/=. rewrite /countable_sum.
-    case_bool_decide as Hneq=>/=; subst.
-    - rewrite encode_inv_encode_nat //= bool_decide_eq_true_2 //.
-    - destruct (encode_inv_nat _) eqn:Heq=>//=.
-      case_bool_decide; [|done]; subst.
-      exfalso. apply Hneq. symmetry. by apply encode_inv_Some_nat.
-  Qed.
-
-  (* same proof as is_seriesC_singleton but stronger *)
   Lemma is_seriesC_singleton_dependent (a : A) v :
     is_seriesC (λ (n : A), if bool_decide (n = a) then v n else 0) (v a).
   Proof.
@@ -405,22 +391,26 @@ Section filter.
       exfalso. apply Hneq. symmetry. by apply encode_inv_Some_nat.
   Qed.
 
-  Lemma ex_seriesC_singleton (a : A) v :
-    ex_seriesC (λ (n : A), if bool_decide (n = a) then v else 0).
-  Proof. eexists. eapply is_seriesC_singleton. Qed.
+  Lemma is_seriesC_singleton (a : A) v :
+    is_seriesC (λ (n : A), if bool_decide (n = a) then v else 0) v.
+  Proof. apply is_seriesC_singleton_dependent. Qed.
 
   Lemma ex_seriesC_singleton_dependent (a : A) v :
     ex_seriesC (λ (n : A), if bool_decide (n = a) then v n else 0).
   Proof. eexists. eapply is_seriesC_singleton_dependent. Qed.
 
-  Lemma SeriesC_singleton (a : A) v :
-    SeriesC (λ n, if bool_decide (n = a) then v else 0) = v.
-  Proof. apply is_series_unique, is_seriesC_singleton. Qed.
+  Lemma ex_seriesC_singleton (a : A) v :
+    ex_seriesC (λ (n : A), if bool_decide (n = a) then v else 0).
+  Proof. eexists. eapply is_seriesC_singleton. Qed.
 
   Lemma SeriesC_singleton_dependent (a : A) v :
     SeriesC (λ n, if bool_decide (n = a) then v n else 0) = v a.
   Proof. apply is_series_unique, is_seriesC_singleton_dependent. Qed.
 
+  Lemma SeriesC_singleton (a : A) v :
+    SeriesC (λ n, if bool_decide (n = a) then v else 0) = v.
+  Proof. apply is_series_unique, is_seriesC_singleton. Qed.
+
   Lemma is_seriesC_singleton_inj (b : B) (f : A → B) v `{Inj A B (=) (=) f} :
     (∃ a, f a = b) →
     is_seriesC (λ (a : A), if bool_decide (f a = b) then v else 0) v.

From 38571ac9bdcd70bd7d1e8cd152e0c5e22a86caaa Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 8 Jan 2024 10:38:21 -0500
Subject: [PATCH 35/37] cleanup adequacy, seq_amplification

---
 theories/ub_logic/adequacy.v          |  1 -
 theories/ub_logic/seq_amplification.v | 34 +++++++++------------------
 2 files changed, 11 insertions(+), 24 deletions(-)

diff --git a/theories/ub_logic/adequacy.v b/theories/ub_logic/adequacy.v
index eb46c7eb..b7bf2bb1 100644
--- a/theories/ub_logic/adequacy.v
+++ b/theories/ub_logic/adequacy.v
@@ -124,7 +124,6 @@ Section adequacy.
         - iIntros (?). iPureIntro.
           rewrite /= /get_active in Hα.
           apply elem_of_elements, elem_of_dom in Hα as [bs Hα].
-
           erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim _ _ _ _ _ Hα)); eauto.
           apply (UB_mon_grading _ _
                    (ε1 + (SeriesC (λ ρ : language.state prob_lang, language.state_step σ1 α ρ * ε2 (e1, ρ))))) => //.
diff --git a/theories/ub_logic/seq_amplification.v b/theories/ub_logic/seq_amplification.v
index 22b769b6..8254c5b1 100644
--- a/theories/ub_logic/seq_amplification.v
+++ b/theories/ub_logic/seq_amplification.v
@@ -29,12 +29,14 @@ Section seq_ampl.
   Qed.
 
 
-
   (* well-formedness for k *)
   (* well-formedness of k doesn't depend on the proof => OK to use proof irrelevence *)
   Record kwf N l : Set := mk_kwf { N_lb : (0 < N)%nat; l_lb: (0 < l)%nat }.
   Lemma kwf_ext N l (x : kwf N l) (y : kwf N l) : x = y.
-  Proof. destruct x; destruct y. Admitted.
+  Proof.
+    destruct x; destruct y.
+    f_equal; apply proof_irrelevance.
+  Qed.
 
   (** amplification factor on our error *)
   Definition k N l (kwf : kwf N l) : R := 1 + 1 / ((S N)^l - 1).
@@ -63,7 +65,7 @@ Section seq_ampl.
   Lemma fRwf_lower N l : kwf N l -> fRwf N l 0.
   Proof. intros. apply mk_fRwf; auto. lia. Qed.
   Lemma fRwf_ext N l i (x : fRwf N l i) (y : fRwf N l i) : x = y.
-  Proof. destruct x; destruct y. Admitted.
+  Proof. destruct x; destruct y. f_equal; [apply kwf_ext | apply proof_irrelevance]. Qed.
 
 
   (** remainder factor on error after step i *)
@@ -80,7 +82,6 @@ Section seq_ampl.
   Proof.
     destruct fRwf as [[Hn Hl] Hi].
     remember {| k_wf := _; i_ub := _|} as fRwf.
-
     induction i as [|i' IH].
     - simpl; lra.
     - Opaque INR.
@@ -201,30 +202,18 @@ Section seq_ampl.
   Proof.
     destruct fRwf as [[Hn Hl] Hi].
     remember {| k_wf := _; i_ub := _ |} as fRwf.
-
     remember (fun n : fin _ => 1 / INR (S N) * nonneg (εDistr N l i ε target fRwf n))%R as body.
     (* we want to exclude the n=target case, and then it's a constant *)
-
     assert (body_pos : ∀ a : fin _, 0 <= body a).
     { intro a.
       rewrite Heqbody.
       apply Rmult_le_pos.
       - apply Rle_mult_inv_pos; [lra|apply lt_0_INR; lia].
       - destruct εDistr. simpl; lra. }
-    rewrite (SeriesC_split_elem body target body_pos); try (apply ex_seriesC_finite).
-    simpl.
-
-    (* FIXME: Revisit that thing about rewriting under the function
-        setoid something?
-        Then we don't need the dependent versions of the function in this case
-
-     *)
-
-    (* this will come up a bunch *)
+    rewrite (SeriesC_split_elem body target body_pos) /=; try (apply ex_seriesC_finite).
     assert (HSN : not (@eq R (INR (S N)) (IZR Z0))).
     { rewrite S_INR. apply Rgt_not_eq. apply Rcomplements.INRp1_pos. }
 
-
     (* Evaluate the first series *)
     replace (SeriesC (λ a : fin _, if bool_decide (a = target) then body a else 0))
        with (1 / INR (S N) * (εR N l (S i) ε fRwf)); last first.
@@ -236,21 +225,20 @@ Section seq_ampl.
     replace (SeriesC (λ a : fin _, if bool_decide (not (a = target)) then body a else 0))
        with (N  * / INR (S N) * (εAmp N l ε (fRwf.(k_wf N l (S i))))); last first.
     { apply (Rplus_eq_reg_l (1 * / INR (S N) * (εAmp N l ε (fRwf.(k_wf N l (S i)))))).
+
       (* simplify the LHS *)
       do 2 rewrite Rmult_assoc.
       rewrite -Rmult_plus_distr_r.
       rewrite Rplus_comm -S_INR -Rmult_assoc Rinv_r; try auto.
       do 2 rewrite Rmult_1_l.
 
-
       (* turn the first term on the RHS into a singleton series, and combine into constant series *)
       rewrite -(SeriesC_singleton target  (/ INR (S N) * _)).
       rewrite -SeriesC_plus; try (apply ex_seriesC_finite).
       rewrite -(SeriesC_ext (fun x : fin (S N) => / INR (S N) * (εAmp N l ε (fRwf.(k_wf N l (S i)))))); last first.
-      { (* series are extensionally equal*)
-        intros n.
+      { intros n.
         case_bool_decide.
-        - rewrite bool_decide_false; auto. lra.
+        - rewrite bool_decide_false; auto; lra.
         - rewrite bool_decide_true; auto.
           rewrite Heqbody /εDistr.
           rewrite bool_decide_false; auto.
@@ -258,7 +246,7 @@ Section seq_ampl.
           apply Rmult_eq_compat_l.
           by simpl nonneg. }
 
-      (* compute the finite series *)
+      (* evaluate the finite series *)
       rewrite SeriesC_finite_mass fin_card.
       rewrite -Rmult_assoc Rinv_r; try auto.
       lra.
@@ -273,7 +261,7 @@ Section seq_ampl.
     rewrite Rinv_r; [| apply not_0_INR;lia].
     rewrite Rmult_1_l.
 
-    (* Turn everything into fR and k by dividing out 𝜀*)
+    (* Divide by 𝜀 *)
     rewrite /εR. Opaque fR. simpl nonneg.
     do 2 rewrite (Rmult_comm (INR _)) Rmult_assoc.
     rewrite -Rmult_plus_distr_l.

From 051d558b3152dd7103721760e3bc716e67122912 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 8 Jan 2024 11:30:22 -0500
Subject: [PATCH 36/37] cleanup ub_rules (fixes E=\emptyset issue)

---
 theories/ub_logic/ub_rules.v | 184 +++++++++++++----------------------
 1 file changed, 66 insertions(+), 118 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 4bf68f7f..ae866ed0 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -398,10 +398,8 @@ Proof.
     rewrite /= Rinv_r; try lra.
     Transparent nnreal_nat.
     rewrite /nnreal_nat.
-    (* simpl does too much here and I can't figure out how to stop it *)
     replace (nonneg {| nonneg := INR (S N); cond_nonneg := _ |}) with (INR (S N)); [| by simpl ].
-    apply not_0_INR.
-    auto.
+    by apply not_0_INR.
   - rewrite -match_nonneg_coercions.
     rewrite -(SeriesC_singleton_dependent _ ε2).
     apply SeriesC_le.
@@ -413,8 +411,6 @@ Proof.
 Qed.
 
 
-
-
 Lemma wp_couple_rand_adv_comp (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
   (exists r, ∀ n, (ε2 n <= r)%R) →
@@ -428,7 +424,6 @@ Proof.
   iIntros "Hclose'".
   iApply exec_ub_adv_comp; simpl.
   iDestruct (ec_split_supply with "Hε Herr") as (ε3) "%Hε3".
-  (* ε3 is the amount of credit supply left outside of ε1 (?) *)
   rewrite Hε3.
   set (foo := (λ (ρ : expr * state),
                 ε3 +
@@ -579,7 +574,6 @@ Admitted.
 
 
 (** * Approximate Lifting *)
-(* FIXME: clean up *)
 Lemma ub_lift_state (N : nat) 𝜎 𝛼 ns :
   𝜎.(tapes) !! 𝛼 = Some (N; ns) →
   ub_lift
@@ -587,8 +581,7 @@ Lemma ub_lift_state (N : nat) 𝜎 𝛼 ns :
     (fun 𝜎' => exists (n : fin (S N)), 𝜎' = state_upd_tapes <[𝛼 := (N; ns ++ [n])]> 𝜎)
     nnreal_zero.
 Proof.
-  rewrite /ub_lift.
-  intros Htapes P Hp.
+  rewrite /ub_lift. intros Htapes P Hp.
   apply Req_le_sym; simpl.
   rewrite /prob SeriesC_0; auto.
   intros 𝜎'.
@@ -602,14 +595,13 @@ Proof.
   apply dmap_unif_zero.
   intros n Hcont.
   apply diff_true_false.
-  specialize Hp with 𝜎'.
-  rewrite -Hp; [| by exists n].
+  rewrite -(Hp 𝜎'); [| by exists n].
   replace false with (negb true) by auto.
   by rewrite HeqK negb_involutive.
 Qed.
 
 (** adapted from wp_couple_tapes in the relational logic *)
-Lemma wp_presample (N : nat) E e 𝛼 ns Φ :
+Lemma wp_presample (N : nat) E e 𝛼 Φ ns :
   to_val e = None →
   ▷ 𝛼 ↪ (N; ns) ∗
   (∀ (n : fin (S N)), 𝛼 ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
@@ -620,7 +612,6 @@ Proof.
     iIntros (𝜎 ε) "((Hheap&Htapes)&Hε)".
     iDestruct (ghost_map_lookup with "Htapes H𝛼") as %Hlookup.
     iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'".
-    (* now we need to prove an exec_ub, we should be able to do this with a state step. *)
     replace ε with (nnreal_zero + ε)%NNR by (apply nnreal_ext; simpl; lra).
     iApply exec_ub_state_step.
     { rewrite /= /get_active.
@@ -629,11 +620,9 @@ Proof.
     iSplitR.
     { iPureIntro. apply ub_lift_state, Hlookup. }
     iIntros (𝜎') "[%n %H𝜎']".
-    (* now we have to prove the exec_ub about 𝜎', we should be able to do this with the wp *)
-    (* first: udpate the resources *)
     iDestruct (ghost_map_lookup with "Htapes H𝛼") as %?%lookup_total_correct.
     iMod (ghost_map_update ((N; ns ++ [n]) : tape) with "Htapes H𝛼") as "[Htapes H𝛼]".
-    iMod "Hclose'" as "_". (* ?? *)
+    iMod "Hclose'" as "_".
     iSpecialize ("Hwp" $! n with "H𝛼").
     rewrite !ub_wp_unfold /ub_wp_pre /= He.
     iSpecialize ("Hwp" $! 𝜎' ε).
@@ -645,16 +634,7 @@ Proof.
     iModIntro. iApply "Hwp".
 Qed.
 
-
-Definition compute_ε2 (σ : state) (ρ : cfg) α N ns (ε2 : fin (S N) -> nonnegreal) : nonnegreal :=
-  match finite.find (fun s => state_upd_tapes <[α:=(N; ns ++ [s]) : tape]> σ = snd ρ) with
-    | Some s => ε2 s
-    | None => nnreal_zero
-  end.
-
-
-Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
-  E = ∅ -> (* can this really only be proven when E = ∅ or can we improve this? *)
+Lemma wp_presample_adv_comp (N : nat) z E e α Φ ns (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
   to_val e = None →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
@@ -663,7 +643,7 @@ Lemma wp_presample_adv_comp (N : nat) α (ns : list (fin (S N))) z e E Φ (ε1 :
   (∀ (n : fin (S N)), € (ε2 n) ∗ α ↪ (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? -> Hσ_red Hsum) "(Hα & Hε & Hwp)".
+  iIntros (-> Hσ_red Hsum) "(Hα & Hε & Hwp)".
   iApply wp_lift_step_fupd_exec_ub; [done|].
   iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
   iDestruct (ghost_map_lookup with "Htapes Hα") as %Hlookup.
@@ -680,9 +660,13 @@ Proof.
   (* R: predicate should hold iff tapes σ' at α is ns ++ [n] *)
   iExists
     (fun σ' : state => exists n : fin _, σ' = (state_upd_tapes <[α:=(_; ns ++ [n]) : tape]> σ1)),
-    (fun ρ => (ε_rem + compute_ε2 σ1 ρ α _ ns ε2)%NNR).
+    (fun ρ => (ε_rem +
+              match finite.find (fun s => state_upd_tapes <[α:=(_; ns ++ [s]) : tape]> σ1 = snd ρ) with
+                | Some s => ε2 s
+                | None => nnreal_zero
+              end))%NNR.
 
-  (* upper bound *)
+  (* upper bound on ε2 *)
   iSplit.
   { iPureIntro.
     destruct (mean_constraint_ub _ _ _ Hsum) as [r [Hr_nonneg Hr_ub]].
@@ -693,62 +677,51 @@ Proof.
     exists (ε_rem + r)%R.
     intros [e' σ'].
     apply Rplus_le_compat_l.
-    rewrite /compute_ε2.
     destruct (finite.find _); auto; apply Hr_ub.
   }
 
+  (* upper bound on total error *)
   iSplit.
   { iPureIntro. simpl.
     rewrite -Hsum.
-
-    (* first: deal with the ε_rem term *)
     setoid_rewrite Rmult_plus_distr_l.
     rewrite SeriesC_plus.
-
+    (* existence *)
     2: { apply ex_seriesC_scal_r, pmf_ex_seriesC. }
     2: { apply pmf_ex_seriesC_mult_fn.
          destruct (mean_constraint_ub _ _ _ Hsum) as [r [Hr_nonneg Hr_ub]].
          exists r; intros; split.
-          - apply cond_nonneg.
-          - rewrite /compute_ε2.
-            destruct (finite.find _).
-            + apply Hr_ub.
-            + simpl; apply Hr_nonneg.
-    }
+         - apply cond_nonneg.
+         - destruct (finite.find _); [apply Hr_ub | simpl; apply Hr_nonneg]. }
 
     rewrite -Rplus_comm; apply Rplus_le_compat; last first.
-    { (* true because state_step is a pmf so is lt 1 *)
+    { (* holds because state_step is a pmf so is lt 1 *)
       rewrite SeriesC_scal_r -{2}(Rmult_1_l (nonneg ε_rem)).
       apply Rmult_le_compat; try auto; [apply cond_nonneg | lra]. }
 
-    (* now we make an injection: we rewrite the lhs series to use a from_option *)
+    (* rewrite to a form for SeriesC_le *)
     pose f := (fun n : fin _ => 1 / S (Z.to_nat z) * ε2 n)%R.
     rewrite (SeriesC_ext
-               (λ x : state, state_step σ1 α x * compute_ε2 σ1 (e, x) α (Z.to_nat z) ns ε2)%R
+               (λ x : state, state_step σ1 α x * _)%R
                (fun x : state => from_option f 0
                                 (finite.find (fun n => state_upd_tapes <[α:=(_; ns ++ [n]) : tape]> σ1 = x ))%R));
       last first.
     { intros n.
-      rewrite /compute_ε2.
-      remember (finite.find _) as F.
-      destruct F as [sf|].
+      destruct (finite.find _) as [sf|] eqn:HeqF.
       - Opaque INR.
-        symmetry in HeqF.
         apply find_Some in HeqF.
         simpl in HeqF; rewrite -HeqF.
         rewrite /from_option /f.
         apply Rmult_eq_compat_r.
         rewrite /state_upd_tapes /=.
-        rewrite /pmf.
-        rewrite /state_step.
+        rewrite /pmf /state_step.
         rewrite bool_decide_true; last first.
-        { rewrite elem_of_dom Hlookup /= /is_Some.
-          by exists (Z.to_nat z; ns). }
+        { rewrite elem_of_dom Hlookup /= /is_Some; by exists (Z.to_nat z; ns). }
         rewrite (lookup_total_correct _ _ (Z.to_nat z; ns)); auto.
         rewrite /dmap /dbind /dbind_pmf /pmf.
         rewrite /= SeriesC_scal_l -{1}(Rmult_1_r (1 / _))%R.
         rewrite /Rdiv Rmult_1_l; apply Rmult_eq_compat_l.
-        (* then show that this series is 0 unless a = sf *)
+        (* this series is 0 unless a = sf *)
         rewrite /dret /dret_pmf.
         rewrite -{2}(SeriesC_singleton sf 1%R).
         apply SeriesC_ext; intros.
@@ -756,16 +729,13 @@ Proof.
         case_bool_decide; simplify_eq.
         + rewrite bool_decide_true; auto.
         + rewrite bool_decide_false; auto.
-          rewrite /not; intros K.
-          rewrite /not in H0; apply H0.
-          rewrite /state_upd_tapes in K.
-
+          rewrite /not; intros Hcont.
+          rewrite /not in H; apply H.
+          rewrite /state_upd_tapes in Hcont.
           assert (R1 : ((Z.to_nat z; ns ++ [sf]) : tape) = (Z.to_nat z; ns ++ [n0])).
-          { apply (insert_inv (tapes σ1) α).
-            by inversion K.
-          }
+          { apply (insert_inv (tapes σ1) α). by inversion Hcont. }
 
-          (* FIXME: same problem as below: is classical logic really necessary here? *)
+          (* FIXME: is classical logic really necessary here? *)
           apply classic_proof_irrel.PIT.EqdepTheory.inj_pair2, app_inv_head in R1.
           by inversion R1.
           Transparent INR.
@@ -803,11 +773,8 @@ Proof.
   iMod (ec_increase_supply _ (ε2 sample) with "Hε_supply") as "[Hε_supply Hε]".
   iMod (ghost_map_update ((Z.to_nat z; ns ++ [sample]) : tape) with "Htapes Hα") as "[Htapes Hα]".
   iSpecialize ("Hwp" $! sample).
-  (* open the WP and specialize it to get the goal *)
   rewrite ub_wp_unfold /ub_wp_pre.
-  iAssert (⌜ (common.language.to_val e) = None ⌝)%I as "%X". { auto. }
-  rewrite X; clear X.
-  rewrite Hsample /compute_ε2 /=.
+  rewrite Hsample /=.
   destruct (@find_is_Some _ _ _
                (λ s : fin (S (Z.to_nat z)), state_upd_tapes <[α:=(Z.to_nat z; ns ++ [s])]> σ1 = state_upd_tapes <[α:=(Z.to_nat z; ns ++ [sample])]> σ1)
                _ sample eq_refl)
@@ -817,15 +784,13 @@ Proof.
   { rewrite /state_upd_tapes in Hr.
     inversion Hr as [Heqt].
     apply (insert_inv (tapes σ1) α) in Heqt.
-    (* FIXME is there a way around using clasical theorem here?
-       Search ((_; ?X) = (_; ?Y)) (?X = ?Y).
-       apply eq_sigT_eq_dep in Heqt.
-       apply eq_dep_non_dep in Heqt. *)
+    (* FIXME is classical necessary here? *)
     apply classic_proof_irrel.PIT.EqdepTheory.inj_pair2 in Heqt.
     apply app_inv_head in Heqt.
     by inversion Heqt. }
-  iSpecialize ("Hwp" with "[Hε Hα]"); first iFrame.
   remember {| heap := heap2; tapes := tapes2 |} as σ2.
+  rewrite Hσ_red.
+  iSpecialize ("Hwp" with "[Hε Hα]"); first iFrame.
   iSpecialize ("Hwp" $! σ2 _).
   iSpecialize ("Hwp" with "[Hheap Htapes Hε_supply]").
   { iSplitL "Hheap Htapes".
@@ -834,9 +799,7 @@ Proof.
       simplify_eq. simpl. iFrame.
     - iFrame. }
   rewrite -Hsample.
-  (* FIXME I can't see where this could be improved in the proof, but I also see no reason why it could't.
-      (related to the prophecy counterexample? idk. )*)
-  simplify_eq.
+  iMod "Hclose"; iMod "Hwp"; iModIntro.
   done.
 Qed.
 
@@ -862,8 +825,7 @@ Lemma ec_spend_1 ε1 : (1 <= ε1.(nonneg))%R → € ε1 -∗ False.
 Proof. Admitted.
 
 
-(* there has to be a better proof, fix this *)
-Lemma amplification_depth N L (ε : posreal) (kwf : kwf N L) :
+Lemma amplification_depth N L (kwf : kwf N L) (ε : posreal) :
   exists n : nat, (1 <= ε * (k N L kwf) ^ n)%R.
 Proof.
   destruct kwf.
@@ -887,26 +849,20 @@ Proof.
           /Hierarchy.eventually
           /Hierarchy.filtermap
           /= in H1.
-  specialize H1 with (fun r : R => (/ ε <= r)%R).
-  simpl in H1; destruct H1.
-  { exists (/ε)%R. intros. by apply Rlt_le. }
-  specialize H with x.
-  exists x.
-
-  apply (Rmult_le_reg_l (/ ε)%R).
-  - apply Rinv_0_lt_compat, cond_pos.
-  - rewrite -Rmult_assoc Rinv_l; last first.
-    { pose (cond_pos ε); lra. }
-    rewrite Rmult_1_l Rmult_1_r /k.
-    rewrite -Heqβ.
-    apply H.
-    done.
+  destruct (H1 (fun r : R => (/ ε <= r)%R)); simpl.
+  - exists (/ε)%R; intros; by apply Rlt_le.
+  - exists x.
+    apply (Rmult_le_reg_l (/ ε)%R).
+    + apply Rinv_0_lt_compat, cond_pos.
+    + rewrite -Rmult_assoc Rinv_l; last first.
+      { pose (cond_pos ε); lra. }
+      rewrite Rmult_1_l Rmult_1_r /k -Heqβ.
+      by apply H.
 Qed.
 
-
+(* FIXME: relocate? *)
 Lemma lookup_ex {A} (n : nat) (L : list A) : (n < length L)%nat -> exists x, (L !! n) = Some x.
 Proof.
-  (* can't figure out how to do this with existing lemmas! *)
   intros HL.
   destruct L as [|h H]; [simpl in HL; lia|].
   generalize dependent H. generalize dependent h.
@@ -920,8 +876,7 @@ Proof.
 Qed.
 
 
-Lemma presample_amplify' N z L e E Φ kwf prefix (suffix_total suffix_remaining : list (fin (S N))) α (ε : posreal) :
-  E = ∅ ->
+Lemma presample_amplify' N z e E α Φ (ε : posreal) L kwf prefix suffix_total (suffix_remaining : list (fin (S N))) :
   TCEq N (Z.to_nat z) →
   to_val e = None →
   L = length suffix_total ->
@@ -934,7 +889,7 @@ Lemma presample_amplify' N z L e E Φ kwf prefix (suffix_total suffix_remaining
          -∗ WP e @ E {{ Φ }})
       -∗ WP e @ E {{ Φ }}))%I.
 Proof.
-  iIntros (? ? ? Htotal HLpos) "(Htape & Hcr_initial)".
+  iIntros (? ? Htotal HLpos) "(Htape & Hcr_initial)".
   iIntros (i HL).
   iInduction i as [|i'] "IH" forall (suffix_remaining).
   - iIntros "Hwp"; iApply "Hwp".
@@ -952,12 +907,9 @@ Proof.
       destruct (lookup_ex i' suffix_total Hi') as [target Htarget].
       rewrite (take_S_r _ _ target); [|apply Htarget].
       pose HMean := (εDistr_mean N L i' ε target (mk_fRwf N L (S i') kwf HL)).
-      wp_apply (wp_presample_adv_comp N α
-              (prefix ++ take i' suffix_total)
-              _ _ _ _
-              (εR N L i' ε (fRwf_dec_i N L i' _))
-              (εDistr N L i' ε target _)); eauto.
-      replace {| k_wf := kwf; i_ub := HL' |} with (fRwf_dec_i N L i' {| k_wf := kwf; i_ub := HL |}); [|apply fRwf_ext].
+      wp_apply wp_presample_adv_comp; [done | apply HMean | ].
+      replace {| k_wf := kwf; i_ub := HL' |} with
+        (fRwf_dec_i N L i' {| k_wf := kwf; i_ub := HL |}); [|apply fRwf_ext].
       iFrame.
       iIntros (s) "(Htape&Hcr)".
       iApply "Hwand".
@@ -971,8 +923,7 @@ Proof.
 Qed.
 
 (* do one step in the amplification sequence *)
-Lemma wp_presample_amplify N z L e E Φ prefix suffix α (ε : posreal) (kwf: kwf N L) :
-  E = ∅ ->
+Lemma wp_presample_amplify N z e E α Φ (ε : posreal) L (kwf: kwf N L) prefix suffix :
   TCEq N (Z.to_nat z) →
   to_val e = None →
   L = (length suffix) ->
@@ -981,7 +932,7 @@ Lemma wp_presample_amplify N z L e E Φ prefix suffix α (ε : posreal) (kwf: kw
   ((α ↪ (N; prefix ++ suffix) ∨ (∃ junk, α ↪ (N; prefix ++ junk) ∗ €(εAmp N L ε kwf))) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? ? ? Hl) "(Hcr & Htape & Hwp)".
+  iIntros (? ? Hl) "(Hcr & Htape & Hwp)".
   destruct suffix as [|s0 sr].
   - iApply "Hwp". iLeft. rewrite -app_nil_end. iFrame.
   - remember (s0 :: sr) as suffix.
@@ -994,9 +945,7 @@ Proof.
  Unshelve. lia.
 Qed.
 
-
-Lemma seq_amplify N z L e E Φ d prefix suffix α (ε : posreal) (kwf: kwf N L) :
-  E = ∅ ->
+Lemma seq_amplify N z e E α Φ (ε : posreal) L (kwf: kwf N L) prefix suffix d :
   TCEq N (Z.to_nat z) →
   to_val e = None →
   L = (length suffix) ->
@@ -1006,7 +955,7 @@ Lemma seq_amplify N z L e E Φ d prefix suffix α (ε : posreal) (kwf: kwf N L)
    -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? ? ? HL) "(Hcr&Htape&Hwp)".
+  iIntros (? ? HL) "(Hcr&Htape&Hwp)".
   iInduction (d) as [|d'] "IH".
   - iApply "Hwp".
     iExists []; rewrite app_nil_r. iRight. iFrame.
@@ -1018,44 +967,43 @@ Proof.
     + iApply wp_presample_amplify; eauto; iFrame.
       iIntros "[?|[%junk' (Htape&Hcr)]]"; iApply "Hwp".
       * iExists _; iLeft.
-        rewrite -app_assoc.
-        iFrame.
+        rewrite -app_assoc; iFrame.
       * iExists _; iRight.
         rewrite -app_assoc -εAmp_iter_cmp; iFrame.
 Qed.
 
 
-Lemma presample_planner_pos N z e E Φ prefix suffix α (ε : nonnegreal) (HN : (0 < N)%nat) (HL : (0 < (length suffix))%nat) (Hε : (0 < ε)%R) :
-  E = ∅ ->
+Lemma presample_planner_pos N z e E α Φ (ε : nonnegreal) prefix suffix :
   TCEq N (Z.to_nat z) →
   to_val e = None →
+  (0 < N)%nat ->
+  (0 < (length suffix))%nat ->
+  (0 < ε)%R ->
   € ε ∗
   (α ↪ (N; prefix)) ∗
   ((∃ junk, α ↪ (N; prefix ++ junk ++ suffix)) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (? ? ?) "(Hcr & Htape & Hwp)".
+  iIntros (? ? ? ? Hε) "(Hcr & Htape & Hwp)".
   remember (length suffix) as L.
   assert (kwf : kwf N L). { apply mk_kwf; lia. }
   pose ε' := mkposreal ε.(nonneg) Hε.
   replace ε with (pos_to_nn ε'); last first.
   { rewrite /ε' /pos_to_nn. by apply nnreal_ext. }
-  destruct (amplification_depth N L ε' kwf) as [d Hdepth].
+  destruct (amplification_depth N L kwf ε') as [d Hdepth].
   iApply seq_amplify; eauto; iFrame.
   iIntros "[%junk [?|(_&Hcr)]]".
-  + iApply "Hwp".
-    iExists _.
-    iFrame.
+  + iApply "Hwp"; iExists _; iFrame.
   + iExFalso; iApply ec_spend_1; last iFrame.
     rewrite /pos_to_nn /εAmp_iter /=.
     replace (nonneg ε) with (pos ε') by auto.
     done.
 Qed.
 
-Lemma presample_planner N z e E Φ prefix suffix α (ε : nonnegreal) (Hε : (0 < ε)%R) :
-  E = ∅ ->
+Lemma presample_planner N z e E α Φ (ε : nonnegreal) prefix suffix :
   TCEq N (Z.to_nat z) →
   to_val e = None →
+  (0 < ε)%R ->
   € ε ∗
   (α ↪ (S N; prefix)) ∗
   ((∃ junk, α ↪ (S N; prefix ++ junk ++ suffix)) -∗ WP e @ E {{ Φ }})
@@ -1068,9 +1016,9 @@ Proof.
     iExists [].
     do 2 (rewrite -app_nil_end); iFrame.
   - remember (h :: R) as suffix.
-    iApply presample_planner_pos; eauto; try lia.
-    + rewrite Heqsuffix cons_length; lia.
+    iApply (presample_planner_pos); eauto; try lia.
     + by erewrite Nat2Z.id.
+    + rewrite Heqsuffix cons_length; lia.
 Qed.
 
 End rules.

From 06ba834f1544d14a22fb8c21b599c26734774ae9 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 8 Jan 2024 11:45:02 -0500
Subject: [PATCH 37/37] remove classical dependency

---
 theories/ub_logic/ub_rules.v | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index ae866ed0..c895d8bc 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -734,9 +734,8 @@ Proof.
           rewrite /state_upd_tapes in Hcont.
           assert (R1 : ((Z.to_nat z; ns ++ [sf]) : tape) = (Z.to_nat z; ns ++ [n0])).
           { apply (insert_inv (tapes σ1) α). by inversion Hcont. }
-
-          (* FIXME: is classical logic really necessary here? *)
-          apply classic_proof_irrel.PIT.EqdepTheory.inj_pair2, app_inv_head in R1.
+          apply Eqdep_dec.inj_pair2_eq_dec in R1; [|apply PeanoNat.Nat.eq_dec].
+          apply app_inv_head in R1.
           by inversion R1.
           Transparent INR.
       - rewrite /from_option /INR /=. lra.
@@ -784,8 +783,7 @@ Proof.
   { rewrite /state_upd_tapes in Hr.
     inversion Hr as [Heqt].
     apply (insert_inv (tapes σ1) α) in Heqt.
-    (* FIXME is classical necessary here? *)
-    apply classic_proof_irrel.PIT.EqdepTheory.inj_pair2 in Heqt.
+    apply Eqdep_dec.inj_pair2_eq_dec in Heqt; [|apply PeanoNat.Nat.eq_dec].
     apply app_inv_head in Heqt.
     by inversion Heqt. }
   remember {| heap := heap2; tapes := tapes2 |} as σ2.