From acaaa4a8822628b20cb29d855ceb26229fa475cf Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Mon, 29 Jan 2024 21:47:08 -0500
Subject: [PATCH] close some admits in the ub_logic examples

---
 .../approx_higherorder_rejection_sampler.v    |  26 +--
 .../approximate_samplers/approx_random_walk.v |   7 +-
 .../approx_rejection_sampler.v                |   4 +-
 .../approximate_samplers/approx_sampler_lib.v | 112 ++++++-------
 .../approximate_samplers/approx_walkSAT.v     | 152 +++++++++++-------
 theories/ub_logic/seq_amplification.v         |  35 ++++
 theories/ub_logic/ub_examples.v               |   3 +-
 theories/ub_logic/ub_rules.v                  |  14 +-
 8 files changed, 207 insertions(+), 146 deletions(-)

diff --git a/theories/examples/approximate_samplers/approx_higherorder_rejection_sampler.v b/theories/examples/approximate_samplers/approx_higherorder_rejection_sampler.v
index 3f20a0e1..e8972963 100644
--- a/theories/examples/approximate_samplers/approx_higherorder_rejection_sampler.v
+++ b/theories/examples/approximate_samplers/approx_higherorder_rejection_sampler.v
@@ -229,7 +229,7 @@ Section higherorder_rand.
     iStartProof; iSplit.
     - (* sampling rule *)
       iIntros (ε Φ) "!> Hcr HΦ"; wp_pures.
-      iApply (wp_couple_rand_adv_comp  m' _ _ _ ε (rand_ε2 n' m' ε) _ with "Hcr").
+      iApply (wp_couple_rand_adv_comp  m' _ _ ε (rand_ε2 n' m' ε) _ with "Hcr").
       { (* uniform bound *)
         eexists (nnreal_div ε (err_factor (S n') (S m'))); intros s.
         rewrite /rand_ε2.
@@ -290,7 +290,6 @@ Section higherorder_rand.
         specialize (fin_to_nat_lt s'); by lia.
 
     Unshelve.
-    { apply Φ. }
     { rewrite Nat2Z.id; apply TCEq_refl. }
   Qed.
 
@@ -327,7 +326,7 @@ Section higherorder_flip2.
     {{{ v, RET #v; ⌜(v = 0%nat) \/ (v = 1%nat) ⌝ ∗ € (scale_flip ε1 εh εt #v) }}}.
   Proof.
     iIntros (Φ) "Hcr HΦ".
-    iApply (wp_couple_rand_adv_comp 1%nat  _ _ _ ε1 (ε2_flip1 ε1 εh εt) _ with "Hcr").
+    iApply (wp_couple_rand_adv_comp 1%nat  _ _ ε1 (ε2_flip1 ε1 εh εt) _ with "Hcr").
     - (* uniform bound *)
       exists (εh + εt)%NNR; intros n.
       rewrite /ε2_flip1.
@@ -338,20 +337,17 @@ Section higherorder_flip2.
       lra.
     - (* continutation *)
       iNext. iIntros (n) "Hcr".
-      iApply ("HΦ" $! (fin_to_nat n)); iSplitR.
-      + iPureIntro; apply fin2_enum.
+      iApply ("HΦ" $! _); iSplitR.
+      + iPureIntro. apply fin2_enum.
       + iApply (ec_spend_irrel with "Hcr"). rewrite /ε2_flip2.
         destruct (fin2_enum n) as [H|H].
         * rewrite /ε2_flip1 H /=.
-          rewrite -fin2_nat_bool.
-          replace (n =? 1)%nat with false; [done|].
-          symmetry; apply Nat.eqb_neq; lia.
+          rewrite -fin_to_nat_to_bool_inv H /=.
+          f_equal.
         * rewrite /ε2_flip1 H /=.
-          rewrite -fin2_nat_bool.
-          replace (n =? 1)%nat with true; [done|].
-          symmetry; apply Nat.eqb_eq; lia.
+          rewrite -fin_to_nat_to_bool_inv H /=.
+          f_equal.
       Unshelve.
-      { apply Φ. }
       { apply TCEq_refl. }
   Qed.
 
@@ -430,6 +426,10 @@ Section higherorder_flip2.
         wp_pures; iModIntro; iApply "HΦ".
         wp_pures; case_bool_decide; wp_pures; auto.
         (* we have a contradiction in Hv' and H *)
-        exfalso. apply fin2_not_0  in Hv'. apply H. rewrite Hv' /=. f_equal.
+        exfalso.
+        rewrite /not in Hv', H.
+        destruct (fin2_enum v').
+        { apply Hv', fin_to_nat_inj. rewrite H0 /=. done.  }
+        { apply H. do 2 f_equal. rewrite H0 /=. auto. }
   Qed.
 End higherorder_flip2.
diff --git a/theories/examples/approximate_samplers/approx_random_walk.v b/theories/examples/approximate_samplers/approx_random_walk.v
index b0b0895e..30b4f9e0 100644
--- a/theories/examples/approximate_samplers/approx_random_walk.v
+++ b/theories/examples/approximate_samplers/approx_random_walk.v
@@ -131,7 +131,7 @@ Section integer_walk.
       excluded by virtue of the (S p) in the amp spec.
 
      *)
-    wp_apply (wp_couple_rand_adv_comp1 _ _ _ _
+    wp_apply (wp_couple_rand_adv_comp1 _ _ _
                 ((IC εᵢ (S p)) + (AC εᵢ εₐ (L εᵢ - S p) (I_obligation_1 εᵢ (S p)) kwf))%NNR
                 (integer_walk_distr εᵢ εₐ (S p) kwf) with "[HcrAC HcrIC]").
     { (* Series mean *)
@@ -211,7 +211,7 @@ Section integer_walk.
     - eauto.
   Qed.
 
-  Lemma integer_walk_sampling_scheme (l : loc) εᵢ εₐ kwf E :
+  Lemma integer_walk_sampling_scheme (l : loc) εᵢ εₐ kwf E B:
     ⊢ (* ⌜(0 < nonneg ε0)%R ⌝ -∗ *)
       incr_sampling_scheme_spec
         (λ: "_", int_walk_sampler #l)
@@ -219,6 +219,7 @@ Section integer_walk.
         (I εᵢ εₐ l kwf)
         (AX εᵢ εₐ kwf)
         (L εᵢ)
+        B
         E.
   Proof.
     iSplit.
@@ -243,7 +244,7 @@ Section integer_walk.
           iModIntro. iPureIntro. f_equal. f_equal.
           apply bool_decide_eq_true_2. lia.
     - iModIntro.
-      iIntros (i p) "(%Hpwf&HcrAX&HI)".
+      iIntros (i p) "(%Hpwf&%Hb&HcrAX&HI)".
       wp_pure.
       wp_apply (ub_wp_wand with "[HcrAX HI]"); first iApply (wp_sampler_amp with "[$]").
       iIntros (s) "[(HI&HAX)|(HI&HAX)]".
diff --git a/theories/examples/approximate_samplers/approx_rejection_sampler.v b/theories/examples/approximate_samplers/approx_rejection_sampler.v
index 808ed621..88ce18c2 100644
--- a/theories/examples/approximate_samplers/approx_rejection_sampler.v
+++ b/theories/examples/approximate_samplers/approx_rejection_sampler.v
@@ -73,7 +73,7 @@ Section basic.
     - wp_pures.
       replace (bool_decide _) with false; last (symmetry; apply bool_decide_eq_false; lia).
       wp_pures.
-      wp_apply (wp_couple_rand_adv_comp _ _ _ Φ _ (bdd_cf_sampling_error (S n') _ _) with "Hcr").
+      wp_apply (wp_couple_rand_adv_comp _ _ _ _ (bdd_cf_sampling_error (S n') _ _) with "Hcr").
       { exists 1. intros s. apply sample_err_wf; try lia. }
       { by apply sample_err_mean. }
       iIntros (sample') "Hcr".
@@ -120,7 +120,7 @@ Section basic.
           replace (S n' + (S m'-S n'))%nat with (S m') by lia.
           specialize (fin_to_nat_lt sample''); by lia.
     - wp_pures.
-      wp_apply (wp_couple_rand_adv_comp _ _ _ Φ _ (bdd_cf_sampling_error (S n') _ _) with "Hcr").
+      wp_apply (wp_couple_rand_adv_comp _ _ _ _ (bdd_cf_sampling_error (S n') _ _) with "Hcr").
       { eexists _. intros s. apply sample_err_wf; try lia. }
       { pose P := (sample_err_mean n' m' Hnm' (bdd_cf_error (S n') (S m') _ Hnm)). by eapply P. }
       iIntros (sample') "Hcr".
diff --git a/theories/examples/approximate_samplers/approx_sampler_lib.v b/theories/examples/approximate_samplers/approx_sampler_lib.v
index 85cf6de0..4d39523b 100644
--- a/theories/examples/approximate_samplers/approx_sampler_lib.v
+++ b/theories/examples/approximate_samplers/approx_sampler_lib.v
@@ -79,46 +79,21 @@ Section finite.
   Qed.
 
 
-
+  (* I feel like there has to be a better way to do this *)
+  (* The best way would be to delete it, I don't think they do this in the actual flip library *)
   Lemma fin2_enum (x : fin 2) : (fin_to_nat x = 0%nat) \/ (fin_to_nat x = 1%nat).
-  Proof. Admitted.
-
-
-  (* surely there has to be a better way *)
-  Lemma fin2_not_0 (x : fin 2) : not (x = 0%fin) -> (x = 1%fin).
-  Proof.
-    intros Hx.
-    destruct (fin2_enum x) as [H|H].
-    - replace 0%nat with (@fin_to_nat 2 (0%fin)) in H by auto.
-      apply fin_to_nat_inj in H.
-      exfalso; apply Hx; apply H.
-    - replace 1%nat with (@fin_to_nat 2 (1%fin)) in H by auto.
-      apply fin_to_nat_inj in H.
-      done.
-  Qed.
-
-
-  Lemma fin2_not_1 (x : fin 2) : not (x = 1%fin) -> (x = 0%fin).
-  Proof.
-    intros Hx.
-    destruct (fin2_enum x) as [H|H]; last first.
-    - replace 1%nat with (@fin_to_nat 2 (1%fin)) in H by auto.
-      apply fin_to_nat_inj in H.
-      exfalso; apply Hx; apply H.
-    - replace 0%nat with (@fin_to_nat 2 (0%fin)) in H by auto.
-      apply fin_to_nat_inj in H.
-      done.
-  Qed.
-
-  Lemma fin2_nat_bool (x : fin 2) : (fin_to_nat x =? 1)%nat = (fin_to_bool x).
   Proof.
-    destruct (fin2_enum x) as [H|H]; rewrite H; simpl.
-    - replace 0%nat with (@fin_to_nat 2 (0%fin)) in H by auto.
-      apply fin_to_nat_inj in H.
-      by rewrite H /=.
-    - replace 1%nat with (@fin_to_nat 2 (1%fin)) in H by auto.
-      apply fin_to_nat_inj in H.
-      by rewrite H /=.
+    destruct (fin_to_bool x) as [|] eqn:H.
+    - right.
+      replace 1%nat with (fin_to_nat (1 : fin 2)%fin); [|simpl; done].
+      replace true with (fin_to_bool (bool_to_fin true)) in H; [|simpl; done].
+      rewrite (@inj _ _ eq eq _ fin_to_bool_inj x (bool_to_fin true) H).
+      simpl. done.
+    - left.
+      replace 0%nat with (fin_to_nat (0 : fin 2)%fin); [|simpl; done].
+      replace false with (fin_to_bool (bool_to_fin false)) in H; [|simpl; done].
+      rewrite (@inj _ _ eq eq _ fin_to_bool_inj x (bool_to_fin false) H).
+      simpl. done.
   Qed.
 End finite.
 
@@ -147,24 +122,36 @@ Section finSeries.
   Proof.
     Opaque firstn.
     simpl.
-    induction v as [|N' v' IH].
-    - simpl; intros. admit. (* wait now this isn't true too *)
-    - simpl.
+    induction n as [|n' IH].
+    - intros H. rewrite take_0 in H. by apply elem_of_nil in H.
+    - (* We can finish cases that are too large immediately  *)
+      destruct (PeanoNat.Nat.le_gt_cases (S n') N) as [Hn'|?]; last first.
+      { intros _. eapply Nat.lt_trans; [apply fin_to_nat_lt | apply H ]. }
+      (* Rewrite ∈ ... fin_enum to a useful form *)
       intros H.
-      destruct n; simpl.
-      { exfalso. rewrite take_0 in H. by eapply (elem_of_nil _). }
-      rewrite firstn_cons in H.
-      apply elem_of_cons in H; destruct H; first simplify_eq.
-      rewrite -fmap_take in H.
-      (* really, we should be able to get the v ∈ take n (fin_enum N') now from H *)
-      assert (HIH: v' ∈ take n (fin_enum N')).
-      { admit. }
-
-      (* anad this should be provable *)
-      assert (Hs: forall A x i (l : list A), (x ∈ take i l) -> (x ∈ take (S i) l) (* and it's not the last element *)).
-      { admit. }
-
-      apply Hs, IH in HIH.
+      assert (Hn'_alt : (n' < length (fin_enum N))%nat).
+      { rewrite fin_enum_length. lia. }
+      edestruct (lookup_ex n' (fin_enum N) Hn'_alt) as [r Hr].
+      erewrite take_S_r in H; last apply Hr.
+      apply elem_of_app in H; destruct H as [H|H].
+      { eapply Nat.lt_le_trans; [apply (IH H)|lia]. }
+      apply elem_of_list_singleton in H; simplify_eq.
+      (* Now we just have to prove it for the last element *)
+      apply Nat.lt_succ_r, Nat.eq_le_incl.
+      Set Printing Coercions.
+      clear IH Hn' Hn'_alt.
+      generalize dependent N.
+      induction n' as [|n'' IHn''].
+      { destruct N.
+        -- intros. simpl in Hr. discriminate.
+        -- intros. simpl in Hr. inversion Hr. auto.
+      }
+      induction N as [|N' IHN'].
+      { intros. rewrite /fin_enum /= in Hr. discriminate. }
+      intros.
+      simpl in Hr.
+      apply (nth_lookup_Some _ _ 0%fin _) in Hr.
+      (* brutal *)
   Admitted.
 
 
@@ -177,6 +164,7 @@ Section finSeries.
   Lemma reindex_fin_series M z K (Hnm : ((S z) < M)%nat):
     SeriesC (fun x : fin M => nonneg (if bool_decide (x < (S z))%nat then nnreal_zero else K)) = (M-(S z)) * nonneg K.
   Proof.
+    Set Printing Coercions.
     rewrite countable_sum.SeriesC_finite_foldr.
     rewrite -(take_drop (S z) (enum (fin M))).
     rewrite foldr_app.
@@ -377,12 +365,12 @@ Section incremental_spec.
      ξ : error
      L : progress bound
    *)
-  Definition incr_sampling_scheme_spec (sampler checker : val) (Ψ : nat -> iProp Σ) (ξ : nat -> nonnegreal) L E : iProp Σ :=
+  Definition incr_sampling_scheme_spec (sampler checker : val) (Ψ : nat -> iProp Σ) (ξ : nat -> nonnegreal) L iL E : iProp Σ :=
     ( (* Either 0 credit or 0 progress => we will sample a value which the checker accepts
          Allowed to consume (or invalidate Ψ) in this process *)
       ((€ (ξ 0%nat) ∨ Ψ 0%nat) -∗ WP sampler #() @ E {{ fun s => WP checker (Val s) @ E {{fun v => ⌜v = #true⌝}}}}) ∗
       (* Given any amount of credit and progress, we can get a sample such that... *)
-     □ (∀ i p, (⌜((S p) <= L)%nat ⌝ ∗ € (ξ (S i)) ∗ Ψ (S p)) -∗
+     □ (∀ i p, (⌜((S p) <= L)%nat ⌝ ∗ ⌜((S i) < iL)%nat ⌝ ∗ € (ξ (S i)) ∗ Ψ (S p)) -∗
             WP sampler #() @ E {{ fun s =>
                    (*...we're done by chance alone, or... *)
                   (WP checker (Val s) @ E {{fun v => ⌜v = #true⌝}}) ∨
@@ -392,15 +380,16 @@ Section incremental_spec.
                   (∃ p', ⌜(p' <= L)%nat ⌝ ∗ € (ξ i) ∗ Ψ p' ∗ (Ψ p' -∗ WP checker (Val s) @ E {{fun v => Ψ p' ∗ ∃ b: bool, ⌜v = #b⌝}}))}}))%I.
 
 
-  Lemma ho_incremental_ubdd_approx_safe (sampler checker : val) Ψ ξ L E i p :
+  Lemma ho_incremental_ubdd_approx_safe (sampler checker : val) Ψ ξ L E i iL p :
     ⊢ ⌜(p <= L)%nat ⌝ ∗
-    incr_sampling_scheme_spec sampler checker Ψ ξ L E ∗
+      ⌜(i < iL)%nat ⌝ ∗
+    incr_sampling_scheme_spec sampler checker Ψ ξ L iL E ∗
     € (ξ i) ∗
     Ψ p -∗
     WP (gen_rejection_sampler sampler checker) @ E {{ fun v => ∃ v', ⌜ v = SOMEV v' ⌝}}.
   Proof.
     rewrite /incr_sampling_scheme_spec.
-    iIntros "(%Hl&(Hfinal&#Hamp)&Hcr&HΨ)".
+    iIntros "(%Hl&%Hil&(Hfinal&#Hamp)&Hcr&HΨ)".
     rewrite /gen_rejection_sampler.
     do 7 wp_pure.
     iRevert (Hl).
@@ -457,7 +446,8 @@ Section incremental_spec.
           -- (* lucky: checker accepts *)
              wp_pures. eauto.
           -- (* not lucky: checker rejects *)
-             wp_pure. iApply ("IHerror" with "Hfinal Hcr HΨ"). eauto.
+             assert (HiL' : (i' < iL)%nat) by lia.
+             wp_pure. iApply ("IHerror" $! HiL' with "Hfinal Hcr HΨ"). eauto.
     Qed.
 
 
diff --git a/theories/examples/approximate_samplers/approx_walkSAT.v b/theories/examples/approximate_samplers/approx_walkSAT.v
index 094094b2..85b00e01 100644
--- a/theories/examples/approximate_samplers/approx_walkSAT.v
+++ b/theories/examples/approximate_samplers/approx_walkSAT.v
@@ -160,10 +160,13 @@ Section higherorder_walkSAT.
         iIntros (v) "%Hv".
         wp_pures.
         iModIntro; iPureIntro.
-        replace (n')%nat with (S (n' - 1))%nat; last admit. (* provable *)
+        replace (n')%nat with (S (n' - 1))%nat; last first.
+        { destruct n'; last by lia.
+          exfalso; rewrite /not in H; apply H.
+          f_equal. }
         simpl.
         by constructor.
-  Admitted.
+  Qed.
 
   (** 3SAT formulas *)
 
@@ -331,6 +334,8 @@ Section higherorder_walkSAT.
       (m !!! (fVar_index v) = negb (solution !!! (fVar_index v))) ->
       (progress_measure f (<[fVar_index v := negb (m !!! (fVar_index v))]> m ) solution < progress_measure f m solution)%nat.
   Proof.
+    (* We want to split the list into before- and after (fVar_index v). The IH will only be
+       true on suffixes of the list containing (fVar_index v) *)
     intros Hdiff.
     (* Induct over the lists, = when not equal to fVar_index v, < when equal *)
     (* need to show we hit fVar_index... induction should keep track of location? *)
@@ -459,36 +464,6 @@ Section higherorder_walkSAT.
     rewrite /not; intros Hk; inversion Hk; lia.
   Qed.
 
-
-  (** General credit accounting (FIXME: move to seq_amplification) *)
-
-  (* Every time we amplify, we have to restore εInv p for some value of p. The seq_amplification sampling scheme
-     ensures that we have enough credit for this, plus some excess credit. Δε is a lower bound on that excess credit. *)
-  Program Definition Δε (ε : posreal) N1 L kwf : posreal := mkposreal (εAmp N1 L ε kwf - ε) _.
-  Next Obligation. intros. pose (εAmp_amplification N1 L ε kwf). lra. Qed.
-
-  Lemma fR_lt_1 N1 L i fRwf : (fR N1 L i fRwf <= 1)%R.
-  Proof.
-    rewrite fR_closed_2.
-    (* True *)
-  Admitted.
-
-  Lemma εAmp_excess (ε : posreal) N1 L kwf :
-    forall i fRwf, ((εR N1 L i ε fRwf) + (Δε ε N1 L kwf) <= εAmp N1 L ε kwf)%R.
-  Proof.
-    intros.
-    rewrite -(Rplus_0_r (εAmp _ _ _ _)).
-    rewrite /Δε /=.
-    rewrite Rplus_comm Rplus_assoc; apply Rplus_le_compat_l.
-    apply (Rplus_le_reg_l ε).
-    rewrite -Rplus_assoc Rplus_opp_r Rplus_0_l Rplus_0_r.
-    rewrite -{2}(Rmult_1_r ε).
-    apply Rmult_le_compat_l; [apply Rlt_le, cond_pos|].
-    apply fR_lt_1.
-  Qed.
-
-
-
   (** Accounting specific to this example *)
 
   (* We need to keep some amount of credit inside the progress invariant so we always have something to amplify against *)
@@ -518,8 +493,37 @@ Section higherorder_walkSAT.
 
   (* We can start out with some amount of progress for free *)
   (* This value is up (1/εExcess...)*)
-  Lemma initial_progress : ⊢ ∀ ε0, ∃ i, € (εProgress ε0 i).
-  Proof. Admitted.
+  (* Doing this in a super annoying way because I can't find a good way to round numbers
+     that works well with the INR/IZR coercions *)
+  Lemma initial_progress : ⊢ ∀ ε0, ∃ i, |==> € (εProgress ε0 i).
+  Proof.
+    iIntros (ε0).
+    iExists (Z.to_nat (up _)).
+    replace (εProgress _ _) with nnreal_zero; first iApply ec_zero.
+    apply nnreal_ext.
+    rewrite /εProgress /=.
+    rewrite Rmax_left; eauto.
+    apply Rle_minus.
+    rewrite INR_IZR_INZ Z2Nat.id.
+    - erewrite Rinv_l_sym.
+      + eapply Rmult_le_compat_r.
+        * rewrite -{2}(Rmult_1_r (pos _)) -Rmult_minus_distr_l.
+          apply Rmult_le_pos; [apply Rlt_le, cond_pos|].
+          apply Rle_0_le_minus, Rlt_le, lt_1_k.
+        * eapply Rlt_le, Rgt_lt, archimed.
+      + rewrite -{2}(Rmult_1_r (pos _)) -Rmult_minus_distr_l.
+        apply Rgt_not_eq, Rlt_gt, Rmult_lt_0_compat; [apply cond_pos|].
+        apply Rlt_Rminus, lt_1_k.
+    - apply le_IZR.
+      apply Rge_le, Rgt_ge.
+      eapply Rgt_trans.
+      + eapply archimed.
+      + apply Rlt_gt, Rinv_0_lt_compat.
+        rewrite -{2}(Rmult_1_r (pos _)) -Rmult_minus_distr_l.
+        apply Rmult_lt_0_compat; [apply cond_pos|].
+        apply Rlt_Rminus, lt_1_k.
+  Qed.
+
 
   Lemma final_progress ε0 : (1 <= εProgress ε0 0%nat)%R.
   Proof. rewrite /= Rmult_0_l Rminus_0_r. apply Rmax_r. Qed.
@@ -530,6 +534,8 @@ Section higherorder_walkSAT.
     := (fun v: fin 3 => εDistr 2 N i ε0 v _).
   Next Obligation. intros. do 2 (constructor; try lia). Qed.
 
+
+
   Lemma resample_amplify (c : clause) (target : fin 3) (m : list bool) (l: loc) ε0 p (Hp : ((S p) <= length m)%nat) (asn : val) E :
     inv_asn m asn ->
     ⊢ (l ↦ asn -∗
@@ -553,13 +559,16 @@ Section higherorder_walkSAT.
     iIntros "Hl".
     wp_pures.
     wp_bind (rand _)%E.
-    wp_apply (wp_couple_rand_adv_comp1 _ _ _ _ _ (εDistr_resampler _ _ _ target) with "Hε").
-    { rewrite εDistr_mean.
+    replace (length m) with N in Hp; [|by destruct Hinv].
+    wp_apply (wp_couple_rand_adv_comp1 _ _ _ _ (εDistr_resampler _ _ _ target) with "Hε").
+    {
+      rewrite εDistr_mean.
       rewrite /εInv.
       replace (fRwf_dec_i _ _ _ _) with (εInv_obligation_1 (S p)) by apply fRwf_ext.
       eauto. }
     iIntros  (i) "Hcr".
     destruct (Fin.eqb i target) eqn:Hi.
+
     - (* sampler chooses the target index and flips it *)
       wp_bind (clause_to_index c _)%E.
       wp_apply (ub_wp_wand); first iApply (wp_clause_to_index c i).
@@ -583,6 +592,7 @@ Section higherorder_walkSAT.
           simpl; lia. }
       iIntros (v) "%Hinv'".
       wp_pures.
+
       wp_store.
       iModIntro.
       iExists _, _.
@@ -597,9 +607,14 @@ Section higherorder_walkSAT.
         rewrite -Hi.
         rewrite /εDistr_resampler /εDistr /εInv.
         rewrite bool_decide_true; eauto.
+        erewrite εR_ext.
         iApply (ec_spend_irrel with "Hcr").
-        (* provable but the rewrite is annoying *)
-        admit.
+        f_equal.
+        (* weird unification thing I guess *)
+        assert (Her : forall a b c d e f g , (a = b) -> εR c d a e f = εR c d b e g).
+        { intros. simplify_eq. apply εR_ext. }
+        eapply Her.
+        lia.
       }
       iPureIntro.
       apply Fin.eqb_eq in Hi.
@@ -607,6 +622,7 @@ Section higherorder_walkSAT.
       apply list_lookup_total_insert.
       destruct (proj_clause_value c target) as [? ? ?].
       simpl; destruct Hinv; lia.
+
     - (* sampler chooses the wrong index, step through and conclude by the amplification  *)
       wp_bind (clause_to_index c _)%E.
       wp_apply (ub_wp_wand); first iApply (wp_clause_to_index c i).
@@ -632,7 +648,12 @@ Section higherorder_walkSAT.
       wp_pures; wp_store.
       iModIntro.
       iExists _, _; iFrame.
-      { assert (i ≠ target)%fin by admit. (* fin nonsense *)
+      { assert (i ≠ target)%fin.
+        { rewrite /not.
+          intros.
+          simplify_eq.
+          replace (Fin.eqb target target) with true in Hi; [discriminate|].
+          symmetry. by apply Fin.eqb_eq. }
         rewrite /εDistr_resampler /εDistr.
         rewrite bool_decide_false; eauto.
         iSplitR.
@@ -640,10 +661,12 @@ Section higherorder_walkSAT.
         iRight.
         iApply (ec_spend_irrel with "Hcr").
         rewrite /εAmplified.
-        (* provable but the rewrite is annoying, like above *)
-        admit.
+        f_equal.
       }
-  Admitted.
+    Unshelve.
+    { lia. }
+    { constructor; last lia. constructor; lia. }
+  Qed.
 
 
   (* running the checker *)
@@ -732,7 +755,8 @@ Section higherorder_walkSAT.
       destruct (find_progress _ _ Hm) as [f1 [f2 [c (-> & Hf1 & Hc)]]].
       (* induct over the SAT clauses doing nothing *)
       iInduction f1 as [| c' f1'] "IH"; last first.
-      { assert (Hc': clause_SAT m c' = true) by admit. (* uses Hf1*)
+      { assert (Hc': clause_SAT m c' = true).
+        { by apply Forall_inv in Hf1. }
         rewrite /sampler.
         wp_pures.
         wp_load.
@@ -746,13 +770,17 @@ Section higherorder_walkSAT.
         replace (f1' ++ [c] ++ f2) with (f1' ++ c :: f2) by auto.
         wp_apply (ub_wp_wand with "[Hl Hε]").
         { iApply ("IH" with "[] [] [] Hl Hε").
-          - admit. (* by Hm and Hc'*)
-          - admit. (* by Hsol*)
-          - admit.  (* by Hf1*)
+          - iPureIntro. rewrite -Hm /formula_SAT /= /fmap. f_equal. auto.
+          - iPureIntro. rewrite -Hsol /formula_SAT /= /fmap. f_equal.
+            replace ((c' :: f1') ++ [c] ++ f2) with (c' :: (f1' ++ c :: f2)) in Hsol; [|by simpl].
+            rewrite /formula_SAT in Hsol.
+            rewrite (fold_symmetric _ andb_assoc) in Hsol; [|intros; apply andb_comm].
+            rewrite /= in Hsol.
+            apply andb_prop in Hsol.
+            by destruct Hsol.
+          - iPureIntro. by apply Forall_inv_tail in Hf1.
         }
-        (* Provable *)
-        admit.
-
+        iIntros (v) "H". iFrame.
       }
       simpl app.
 
@@ -800,8 +828,9 @@ Section higherorder_walkSAT.
 
 
 
-  Lemma walksat_sampling_scheme f solution ε (l : loc) E :
-    (⊢ ⌜formula_SAT solution f = true ⌝ -∗
+  Lemma walksat_sampling_scheme f solution ε (l : loc) HiL E :
+    (⊢ ⌜forall w : nat, (w < HiL)%nat -> (0 <= 1 - w * εExcess ε)%R ⌝ -∗ (* FIXME: Define HiL in terms of ε*)
+       ⌜formula_SAT solution f = true ⌝ -∗
        ⌜length solution = N ⌝ -∗
        ⌜(length f > 0)%nat ⌝ -∗
         incr_sampling_scheme_spec
@@ -810,9 +839,10 @@ Section higherorder_walkSAT.
           (iProgress ε l solution f)
           (εProgress ε)
           N
+          HiL
           E)%I.
   Proof.
-    iIntros "%Hsolution %Hsl %Hnontrivial".
+    iIntros "%HHil %Hsolution %Hsl %Hnontrivial".
     rewrite /incr_sampling_scheme_spec.
     iSplit.
     - iIntros "[Hcr | [%asn [%m (Hl & Hcr & %Hinv & %Hp)]]]".
@@ -835,7 +865,7 @@ Section higherorder_walkSAT.
           iPureIntro; apply Hinv. }
         iIntros (r) "(Hl&->)"; iPureIntro; do 2 f_equal.
         simplify_eq; done.
-    - iIntros (i p) "!> (%Hp_bound & Hε & [%asn [%m (Hl & Hcr & %Hinv & %Hp)]])".
+    - iIntros (i p) "!> (%Hp_bound & %Hi_bound & Hε & [%asn [%m (Hl & Hcr & %Hinv & %Hp)]])".
       wp_pures.
       (* step the sampler differently depending on if it is SAT or not *)
       destruct (formula_SAT m f) as [|] eqn:Hsat.
@@ -887,16 +917,24 @@ Section higherorder_walkSAT.
             iApply ec_spend_irrel; [|iFrame].
             Opaque INR.
             rewrite /εProgress /=.
-            (* doable *)
-            admit.
+            rewrite /εExcess /= in HHil.
+            do 2 (rewrite Rmax_right; [|apply HHil; lia]).
+            rewrite S_INR. lra.
           }
 
           iFrame.
           iSplitL.
           -- iExists _, _; iFrame; iSplit; iPureIntro; eauto.
              rewrite /progress_measure.
-             (* doable by induction *)
-             admit.
+
+              (*
+             assert (LzipLen: forall T : Type, forall A B : list T, (length A = length B) -> (length (zip A B) = length A)).
+              *)
+             replace N with (length (zip m' solution)) by admit.
+             induction (zip m' solution) as [|H T IH].
+             ++ simpl; lia.
+             ++ simpl.
+                destruct H as [m0 s0]; destruct (eqb m0 s0); try lia.
           -- iIntros "[%asn'' [%m'' (Hl & ? & % & %)]]".
              wp_pures.
              wp_apply (ub_wp_wand with "[Hl]").
diff --git a/theories/ub_logic/seq_amplification.v b/theories/ub_logic/seq_amplification.v
index 8254c5b1..e8af5f3d 100644
--- a/theories/ub_logic/seq_amplification.v
+++ b/theories/ub_logic/seq_amplification.v
@@ -131,6 +131,21 @@ Section seq_ampl.
       lia.
   Qed.
 
+  Lemma fR_lt_1 N1 L i fRwf : (fR N1 L i fRwf <= 1)%R.
+  Proof.
+    destruct fRwf as [kwf ?]; destruct kwf.
+    rewrite fR_closed_2.
+    apply Rcomplements.Rle_minus_l.
+    rewrite -{1}(Rplus_0_r 1%R); apply Rplus_le_compat_l.
+    apply Rcomplements.Rdiv_le_0_compat; [apply -> Rcomplements.Rminus_le_0 | apply Rlt_Rminus ].
+    - apply pow_R1_Rle.
+      pose (pos_INR N1).
+      rewrite S_INR.
+      lra.
+    - apply Rlt_pow_R1; try lia.
+      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 .
@@ -272,4 +287,24 @@ Section seq_ampl.
     rewrite (fR_mean N); try lia.
     lra.
   Qed.
+
+
+  Program Definition Δε (ε : posreal) N L kwf : posreal := mkposreal (εAmp N L ε kwf - ε) _.
+  Next Obligation. intros. pose (εAmp_amplification N L ε kwf0). lra. Qed.
+
+  Lemma εAmp_excess (ε : posreal) N1 L kwf :
+    forall i fRwf, ((εR N1 L i ε fRwf) + (Δε ε N1 L kwf) <= εAmp N1 L ε kwf)%R.
+  Proof.
+    intros.
+    rewrite -(Rplus_0_r (εAmp _ _ _ _)).
+    rewrite /Δε /=.
+    rewrite Rplus_comm Rplus_assoc; apply Rplus_le_compat_l.
+    apply (Rplus_le_reg_l ε).
+    rewrite -Rplus_assoc Rplus_opp_r Rplus_0_l Rplus_0_r.
+    rewrite -{2}(Rmult_1_r ε).
+    apply Rmult_le_compat_l; [apply Rlt_le, cond_pos|].
+    apply fR_lt_1.
+  Qed.
+
+
 End seq_ampl.
diff --git a/theories/ub_logic/ub_examples.v b/theories/ub_logic/ub_examples.v
index 1d03b1e3..ca5fd36a 100644
--- a/theories/ub_logic/ub_examples.v
+++ b/theories/ub_logic/ub_examples.v
@@ -74,8 +74,7 @@ Proof.
                 then nnreal_zero
                 else if bool_decide (n = 1%fin) then nnreal_one
                                             else nnreal_inv((nnreal_nat 2))).
-  unshelve wp_apply (wp_couple_rand_adv_comp _ _ _ _ _ f with "Herr").
-  { intro. exact ⌜ true ⌝%I. }
+  unshelve wp_apply (wp_couple_rand_adv_comp _ _ _ _ f with "Herr").
   {
     exists 1; intro n.
     rewrite /f.
diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index 04a1fe31..df6009ba 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -451,7 +451,7 @@ Proof.
 Qed.
 
 
-Lemma twp_couple_rand_adv_comp (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
+Lemma twp_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) →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
@@ -669,7 +669,7 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma wp_couple_rand_adv_comp (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
+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) →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
@@ -682,13 +682,13 @@ Proof.
   iApply ("H2" with "[$]").
 Qed.
 
-Lemma twp_couple_rand_adv_comp1 (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
+Lemma twp_couple_rand_adv_comp1 (N : nat) z E (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
   [[{ € ε1 }]] rand #z @ E [[{ n, RET #n; € (ε2 n) }]].
 Proof.
   iIntros (H1 H2).
-  eapply (twp_couple_rand_adv_comp _ _ _ Φ ε1 ε2).
+  eapply (twp_couple_rand_adv_comp _ _ _ ε1 ε2).
   - apply H1.
   - edestruct mean_constraint_ub as [H3 H4].
     + apply H2.
@@ -696,13 +696,13 @@ Proof.
   - apply H2.
 Qed.
 
-Lemma wp_couple_rand_adv_comp1 (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
+Lemma wp_couple_rand_adv_comp1 (N : nat) z E (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) :
   TCEq N (Z.to_nat z) →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
   {{{ € ε1 }}} rand #z @ E {{{ n, RET #n; € (ε2 n) }}}.
 Proof.
   iIntros (H1 H2).
-  eapply (wp_couple_rand_adv_comp _ _ _ Φ ε1 ε2).
+  eapply (wp_couple_rand_adv_comp _ _ _ ε1 ε2).
   - apply H1.
   - edestruct mean_constraint_ub as [H3 H4].
     + apply H2.
@@ -1655,7 +1655,6 @@ Proof.
         apply Nat.add_le_mono_r, block_pad_ub.
         rewrite HS /=. lia.
     + rewrite HS.
-      (* iFrame is very slow here *)
       iFrame.
 Qed.
 
@@ -1680,7 +1679,6 @@ Proof.
         apply Nat.add_le_mono_r, block_pad_ub.
         rewrite HS /=. lia.
     + rewrite HS.
-      (* iFrame is very slow here *)
       iFrame.
 Qed.