1 files changed, 0 insertions, 691 deletions

diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v
deleted file mode 100644
index d08fe7a8b..000000000
--- a/src/Arithmetic/Saturated/MontgomeryAPI.v
+++ /dev/null
@@ -1,691 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Arithmetic.Saturated.Core.
-Require Import Crypto.Arithmetic.Saturated.UniformWeight.
-Require Import Crypto.Arithmetic.Saturated.Wrappers.
-Require Import Crypto.Arithmetic.Saturated.AddSub.
-Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil.
-Require Import Crypto.Util.Tuple Crypto.Util.LetIn.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.ListUtil.
-Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.ZUtil.Modulo.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.CPS.
-Require Import Crypto.Util.ZUtil.Zselect.
-Require Import Crypto.Util.ZUtil.AddGetCarry.
-Require Import Crypto.Util.ZUtil.MulSplit.
-Require Import Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Opp.
-Require Import Crypto.Util.Tactics.UniquePose.
-Local Notation "A ^ n" := (tuple A n) : type_scope.
-
-Section API.
-  Context (bound : Z) {bound_pos : bound > 0}.
-  Definition T : nat -> Type := tuple Z.
-
-  (* lowest limb is less than its bound; this is required for [divmod]
-  to simply separate the lowest limb from the rest and be equivalent
-  to normal div/mod with [bound]. *)
-  Local Notation small := (@small bound).
-
-  Definition zero {n:nat} : T n := B.Positional.zeros n.
-
-  (** Returns 0 iff all limbs are 0 *)
-  Definition nonzero_cps {n} (p : T n) {cpsT} (f : Z -> cpsT) : cpsT
-    := CPSUtil.to_list_cps _ p (fun p => CPSUtil.fold_right_cps runtime_lor 0%Z p f).
-  Definition nonzero {n} (p : T n) : Z
-    := nonzero_cps p id.
-
-  Definition join0_cps {n:nat} (p : T n) {R} (f:T (S n) -> R)
-    := Tuple.left_append_cps 0 p f.
-  Definition join0 {n} p : T (S n) := @join0_cps n p _ id.
-
-  Definition divmod_cps {n} (p : T (S n)) {R} (f:T n * Z->R) : R
-    := Tuple.tl_cps p (fun d => Tuple.hd_cps p (fun m =>  f (d, m))).
-  Definition divmod {n} p : T n * Z := @divmod_cps n p _ id.
-
-  Definition drop_high_cps {n : nat} (p : T (S n)) {R} (f:T n->R)
-    := Tuple.left_tl_cps p f.
-  Definition drop_high {n} p : T n := @drop_high_cps n p _ id.
-
-  Definition scmul_cps {n} (c : Z) (p : T n) {R} (f:T (S n)->R) :=
-    Columns.mul_cps (n1:=1) (n3:=S n) (uweight bound) bound c p
-      (* The carry that comes out of Columns.mul_cps will be 0, since
-      (S n) limbs is enough to hold the result of the
-      multiplication, so we can safely discard it. *)
-      (fun carry_result =>f (snd carry_result)).
-  Definition scmul {n} c p : T (S n) := @scmul_cps n c p _ id.
-
-  Definition add_cps {n} (p q: T n) {R} (f:T (S n)->R) :=
-    B.Positional.sat_add_cps (s:=bound) p q _
-      (* join the last carry *)
-      (fun carry_result => Tuple.left_append_cps (fst carry_result) (snd carry_result) f).
-  Definition add {n} p q : T (S n) := @add_cps n p q _ id.
-
-  (* Wrappers for additions with slightly uneven limb counts *)
-  Definition add_S1_cps {n} (p: T (S n)) (q: T n) {R} (f:T (S (S n))->R) :=
-    join0_cps q (fun Q => add_cps p Q f).
-  Definition add_S1 {n} p q := @add_S1_cps n p q _ id.
-  Definition add_S2_cps {n} (p: T n) (q: T (S n)) {R} (f:T (S (S n))->R) :=
-    join0_cps p (fun P => add_cps P q f).
-  Definition add_S2 {n} p q := @add_S2_cps n p q _ id.
-
-  Definition sub_then_maybe_add_cps {n} mask (p q r : T n)
-             {R} (f:T n -> R) :=
-    B.Positional.sat_sub_cps (s:=bound) p q _
-      (* the carry will be 0 unless we underflow--we do the addition only
-         in the underflow case *)
-      (fun carry_result =>
-         B.Positional.select_cps mask (fst carry_result) r
-      (fun selected => join0_cps selected
-      (fun selected' =>
-         B.Positional.sat_add_cps (s:=bound) (left_append (- (fst carry_result))%RT (snd carry_result)) selected' _
-      (* We can now safely discard the carry and the highest digit.
-         This relies on the precondition that p - q + r < bound^n. *)
-      (fun carry_result' => drop_high_cps (snd carry_result') f)))).
-  Definition sub_then_maybe_add {n} mask (p q r : T n) :=
-    sub_then_maybe_add_cps mask p q r id.
-
-   (* Subtract q if and only if p >= q. We rely on the preconditions
-    that 0 <= p < 2*q and q < bound^n (this ensures the output is less
-    than bound^n). *)
-  Definition conditional_sub_cps {n} (p:Z^S n) (q:Z^n) R (f:Z^n->R) :=
-    join0_cps q
-    (fun qq => B.Positional.sat_sub_cps (s:=bound) p qq _
-      (* if carry is zero, we select the result of the subtraction,
-      otherwise the first input *)
-      (fun carry_result =>
-        Tuple.map2_cps (Z.zselect (fst carry_result)) (snd carry_result) p
-      (* in either case, since our result must be < q and therefore <
-      bound^n, we can drop the high digit *)
-      (fun r => drop_high_cps r f))).
-  Definition conditional_sub {n} p q := @conditional_sub_cps n p q _ id.
-
-  Hint Opaque join0 divmod drop_high scmul add sub_then_maybe_add conditional_sub : uncps.
-
-  Section CPSProofs.
-
-    Local Ltac prove_id :=
-      repeat autounfold;
-      repeat (intros; autorewrite with uncps push_id);
-      reflexivity.
-
-    Lemma nonzero_id n p {cpsT} f : @nonzero_cps n p cpsT f = f (@nonzero n p).
-    Proof. cbv [nonzero nonzero_cps]. prove_id. Qed.
-
-    Lemma join0_id n p R f :
-      @join0_cps n p R f = f (join0 p).
-    Proof. cbv [join0_cps join0]. prove_id. Qed.
-
-    Lemma divmod_id n p R f :
-      @divmod_cps n p R f = f (divmod p).
-    Proof. cbv [divmod_cps divmod]; prove_id. Qed.
-
-    Lemma drop_high_id n p R f :
-      @drop_high_cps n p R f = f (drop_high p).
-    Proof. cbv [drop_high_cps drop_high]; prove_id. Qed.
-    Hint Rewrite drop_high_id : uncps.
-
-    Lemma scmul_id n c p R f :
-      @scmul_cps n c p R f = f (scmul c p).
-    Proof. cbv [scmul_cps scmul]. prove_id. Qed.
-
-    Lemma add_id n p q R f :
-      @add_cps n p q R f = f (add p q).
-    Proof. cbv [add_cps add Let_In]. prove_id. Qed.
-    Hint Rewrite add_id : uncps.
-
-    Lemma add_S1_id n p q R f :
-      @add_S1_cps n p q R f = f (add_S1 p q).
-    Proof. cbv [add_S1_cps add_S1 join0_cps]. prove_id. Qed.
-
-    Lemma add_S2_id n p q R f :
-      @add_S2_cps n p q R f = f (add_S2 p q).
-    Proof. cbv [add_S2_cps add_S2 join0_cps]. prove_id. Qed.
-
-    Lemma sub_then_maybe_add_id n mask p q r R f :
-      @sub_then_maybe_add_cps n mask p q r R f = f (sub_then_maybe_add mask p q r).
-    Proof. cbv [sub_then_maybe_add_cps sub_then_maybe_add join0_cps Let_In]. prove_id. Qed.
-
-    Lemma conditional_sub_id n p q R f :
-      @conditional_sub_cps n p q R f = f (conditional_sub p q).
-    Proof. cbv [conditional_sub_cps conditional_sub join0_cps Let_In]. prove_id. Qed.
-
-  End CPSProofs.
-  Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id sub_then_maybe_add_id conditional_sub_id : uncps.
-
-  Section Proofs.
-
-    Definition eval {n} (p : T n) : Z :=
-      B.Positional.eval (uweight bound) p.
-
-    Definition encode n (z : Z) : T n :=
-      B.Positional.encode (uweight bound) (modulo_cps:=@modulo_cps) (div_cps:=@div_cps) z.
-
-    Lemma eval_small n (p : T n) (Hsmall : small p) :
-      0 <= eval p < uweight bound n.
-    Proof.
-      cbv [small eval] in *; intros.
-      induction n; cbv [T uweight] in *; [destruct p|rewrite (subst_left_append p)];
-      repeat match goal with
-             | _ => progress autorewrite with push_basesystem_eval
-             | _ => rewrite Z.pow_0_r
-             | _ => specialize (IHn (left_tl p))
-             | _ =>
-               let H := fresh "H" in
-               match type of IHn with
-                 ?P -> _ => assert P as H by auto using Tuple.In_to_list_left_tl;
-                              specialize (IHn H)
-               end
-             | |- context [?b ^ Z.of_nat (S ?n)] =>
-               replace (b ^ Z.of_nat (S n)) with (b ^ Z.of_nat n * b) by
-                   (rewrite Nat2Z.inj_succ, <-Z.add_1_r, Z.pow_add_r,
-                    Z.pow_1_r by (omega || auto using Nat2Z.is_nonneg);
-                    reflexivity)
-             | _ => omega
-             end.
-
-        specialize (Hsmall _ (Tuple.In_left_hd _ p)).
-        split; [Z.zero_bounds; omega |].
-        apply Z.lt_le_trans with (m:=bound^Z.of_nat n * (left_hd p+1)).
-        { rewrite Z.mul_add_distr_l.
-          apply Z.add_le_lt_mono; omega. }
-        { apply Z.mul_le_mono_nonneg; omega. }
-    Qed.
-
-    Lemma small_encode n (v : Z) (Hsmall : 0 <= v < uweight bound n)
-      : small (encode n v).
-    Proof.
-    Admitted. (* TODO(jadep): prove me *)
-
-    Lemma eval_encode n (v : Z) (Hsmall : 0 <= v < uweight bound n)
-      : eval (encode n v) = v.
-    Proof.
-      destruct n as [|n].
-      { cbv -[Z.le Z.lt Z.gt] in *; omega. }
-      { cbv [eval encode].
-        pose proof (@uweight_divides _ bound_pos) as Hdiv.
-        apply B.Positional.eval_encode; try reflexivity;
-          eauto using modulo_id, div_id, div_mod, uweight_nonzero.
-        { intros i ?; specialize (Hdiv i); omega. } }
-    Qed.
-
-    Lemma eval_zero n : eval (@zero n) = 0.
-    Proof.
-      cbv [eval zero].
-      autorewrite with push_basesystem_eval.
-      reflexivity.
-    Qed.
-
-    Lemma small_zero n : small (@zero n).
-    Proof.
-      cbv [zero small B.Positional.zeros]. destruct n; [simpl;tauto|].
-      rewrite to_list_repeat.
-      intros x H; apply repeat_spec in H; subst x; omega.
-    Qed.
-
-    Lemma small_hd n p : @small (S n) p -> 0 <= hd p < bound.
-    Proof.
-      cbv [small]. let H := fresh "H" in intro H; apply H.
-      rewrite (subst_append p). rewrite to_list_append, hd_append.
-      apply in_eq.
-    Qed.
-
-    Lemma In_to_list_tl {A n} (p : A^(S n)) x :
-      In x (to_list n (tl p)) -> In x (to_list (S n) p).
-    Proof.
-      intros. rewrite (subst_append p).
-      rewrite to_list_append. simpl In. tauto.
-    Qed.
-
-    Lemma small_tl n p : @small (S n) p -> small (tl p).
-    Proof.
-      cbv [small]. let H := fresh "H" in intros H ? ?; apply H.
-      auto using In_to_list_tl.
-    Qed.
-
-    Lemma add_nonneg_zero_iff a b c : 0 <= a -> 0 <= b -> 0 < c ->
-                               a = 0 /\ b = 0 <-> a + c * b = 0.
-    Proof. nia. Qed.
-
-    Lemma eval_pair n (p : T (S (S n))) : small p ->
-      (snd p = 0 /\ eval (n:=S n) (fst p) = 0) <-> eval p = 0.
-    Proof.
-      intro Hsmall. cbv [eval].
-      rewrite uweight_eval_step with (p:=p).
-      change (fst p) with (tl p). change (snd p) with (hd p).
-      apply add_nonneg_zero_iff; try omega.
-      { apply small_hd in Hsmall. omega. }
-      { apply small_tl, eval_small in Hsmall.
-        cbv [eval] in Hsmall; omega. }
-    Qed.
-
-    Lemma eval_nonzero n p : small p -> @nonzero n p = 0 <-> eval p = 0.
-    Proof.
-      destruct n as [|n].
-      { compute; split; trivial. }
-      induction n as [|n IHn].
-      { simpl; rewrite Z.lor_0_r; unfold eval, id.
-        cbv -[Z.add iff].
-        rewrite Z.add_0_r.
-        destruct p; omega. }
-      { destruct p as [ps p]; specialize (IHn ps).
-        unfold nonzero, nonzero_cps in *.
-        autorewrite with uncps in *.
-        unfold id in *.
-        setoid_rewrite to_list_S.
-        set (k := S n) in *; simpl in *.
-        intro Hsmall.
-        rewrite Z.lor_eq_0_iff, IHn
-          by (hnf in Hsmall |- *; simpl in *; eauto);
-          clear IHn.
-        exact (eval_pair n (ps, p) Hsmall). }
-    Qed.
-
-    Lemma eval_join0 n p
-      : eval (@join0 n p) = eval p.
-    Proof.
-      cbv [join0 join0_cps eval]. autorewrite with uncps push_id.
-      rewrite B.Positional.eval_left_append. ring.
-    Qed.
-
-    Local Ltac pose_uweight bound :=
-      match goal with H : bound > 0 |- _ =>
-                      pose proof (uweight_0 bound);
-                      pose proof (@uweight_positive bound H);
-                      pose proof (@uweight_nonzero bound H);
-                      pose proof (@uweight_multiples bound);
-                      pose proof (@uweight_divides bound H)
-      end.
-
-    Local Ltac pose_all :=
-      pose_uweight bound;
-      pose proof Z.add_get_carry_full_div;
-      pose proof Z.add_get_carry_full_mod;
-      pose proof Z.mul_split_div; pose proof Z.mul_split_mod;
-      pose proof div_correct; pose proof modulo_correct;
-      pose proof @div_id; pose proof @modulo_id;
-      pose proof @Z.add_get_carry_full_cps_correct;
-      pose proof @Z.mul_split_cps_correct;
-      pose proof @Z.mul_split_cps'_correct.
-
-    Lemma eval_add n p q :
-      eval (@add n p q) = eval p + eval q.
-    Proof.
-      intros. pose_all. cbv [add_cps add eval Let_In].
-      autorewrite with uncps push_id cancel_pair push_basesystem_eval.
-      symmetry; auto using Z.div_mod.
-    Qed.
-
-    Lemma eval_add_same n p q
-      :  eval (@add n p q) = eval p + eval q.
-    Proof. apply eval_add; omega. Qed.
-    Lemma eval_add_S1 n p q
-      :  eval (@add_S1 n p q) = eval p + eval q.
-    Proof.
-      cbv [add_S1 add_S1_cps]. autorewrite with uncps push_id.
-      rewrite eval_add; rewrite eval_join0; reflexivity.
-    Qed.
-    Lemma eval_add_S2 n p q
-      :  eval (@add_S2 n p q) = eval p + eval q.
-    Proof.
-      cbv [add_S2 add_S2_cps]. autorewrite with uncps push_id.
-      rewrite eval_add; rewrite eval_join0; reflexivity.
-    Qed.
-    Hint Rewrite eval_add_same eval_add_S1 eval_add_S2 using (omega || assumption): push_basesystem_eval.
-
-    Local Definition compact {n} := Columns.compact (n:=n) (add_get_carry_cps:=@Z.add_get_carry_full_cps) (div_cps:=@div_cps) (modulo_cps:=@modulo_cps) (uweight bound).
-    Local Definition compact_digit := Columns.compact_digit (add_get_carry_cps:=@Z.add_get_carry_full_cps) (div_cps:=@div_cps) (modulo_cps:=@modulo_cps) (uweight bound).
-    Lemma small_compact {n} (p:(list Z)^n) : small (snd (compact p)).
-    Proof.
-      pose_all.
-      match goal with
-        |- ?G => assert (G /\ fst (compact p) = fst (compact p)); [|tauto]
-      end. (* assert a dummy second statement so that fst (compact x) is in context *)
-      cbv [compact Columns.compact Columns.compact_cps small
-                   Columns.compact_step Columns.compact_step_cps];
-        autorewrite with uncps push_id.
-      change (fun i s a => Columns.compact_digit_cps (uweight bound) i (s :: a) id)
-      with (fun i s a => compact_digit i (s :: a)).
-      remember (fun i s a => compact_digit i (s :: a)) as f.
-
-      apply @mapi_with'_linvariant with (n:=n) (f:=f) (inp:=p);
-        intros; [|simpl; tauto]. split; [|reflexivity].
-      let P := fresh "H" in
-      match goal with H : _ /\ _ |- _ => destruct H end.
-      destruct n0; subst f.
-      { cbv [compact_digit uweight to_list to_list' In].
-        rewrite Columns.compact_digit_mod
-            by (assumption || (intros; autorewrite with uncps push_id; auto)).
-        rewrite Z.pow_0_r, Z.pow_1_r, Z.div_1_r. intros x ?.
-        match goal with
-          H : _ \/ False |- _ => destruct H; [|exfalso; assumption] end.
-        subst x. apply Z.mod_pos_bound, Z.gt_lt, bound_pos. }
-      { rewrite Tuple.to_list_left_append.
-        let H := fresh "H" in
-        intros x H; apply in_app_or in H; destruct H;
-          [solve[auto]| cbv [In] in H; destruct H;
-                        [|exfalso; assumption] ].
-        subst x. cbv [compact_digit].
-        rewrite Columns.compact_digit_mod
-            by (assumption || (intros; autorewrite with uncps push_id; auto)).
-        rewrite !uweight_succ, Z.div_mul by
-            (apply Z.neq_mul_0; split; auto; omega).
-        apply Z.mod_pos_bound, Z.gt_lt, bound_pos. }
-    Qed.
-
-    Lemma small_left_append {n} b x :
-      0 <= x < bound -> small b -> small (@left_append _ n x b).
-    Proof.
-      intros.
-      cbv [small].
-      setoid_rewrite Tuple.to_list_left_append.
-      setoid_rewrite in_app_iff.
-      intros y HIn; destruct HIn as [HIn|[]]; (contradiction||omega||eauto).
-    Qed.
-
-    Lemma small_add n a b :
-      (2 <= bound) ->
-      small a -> small b -> small (@add n a b).
-    Proof.
-      intros.
-      cbv [add add_cps]; autorewrite with uncps push_id in *.
-      pose proof @B.Positional.small_sat_add bound ltac:(omega) _ a b.
-      eapply small_left_append; eauto.
-      rewrite @B.Positional.sat_add_div by omega.
-      repeat match goal with H:_|-_=> unique pose proof (eval_small _ _ H) end.
-      cbv [eval] in *; Z.div_mod_to_quot_rem_in_goal; nia.
-    Qed.
-
-    Lemma small_join0 {n} b : small b -> small (@join0 n b).
-    Proof.
-      cbv [join0 join0_cps]; autorewrite with uncps push_id in *.
-      eapply small_left_append; omega.
-    Qed.
-
-    Lemma small_add_S1 n a b :
-      (2 <= bound) ->
-      small a -> small b -> small (@add_S1 n a b).
-    Proof.
-      intros.
-      cbv [add_S1 add_S1_cps Let_In]; autorewrite with uncps push_id in *.
-      eauto using small_add, small_join0.
-    Qed.
-
-    Lemma small_left_tl n (v:T (S n)) : small v -> small (left_tl v).
-    Proof. cbv [small]. auto using Tuple.In_to_list_left_tl. Qed.
-
-    Lemma eval_drop_high n v :
-      small v -> eval (@drop_high n v) = eval v mod (uweight bound n).
-    Proof.
-      cbv [drop_high drop_high_cps eval].
-      rewrite Tuple.left_tl_cps_correct, push_id. (* TODO : for some reason autorewrite with uncps doesn't work here *)
-      intro H. apply small_left_tl in H.
-      rewrite (subst_left_append v) at 2.
-      autorewrite with push_basesystem_eval.
-      apply eval_small in H.
-      rewrite Z.mod_add_l' by (pose_uweight bound; auto).
-      rewrite Z.mod_small; auto.
-    Qed.
-
-    Lemma small_drop_high n v : small v -> small (@drop_high n v).
-    Proof.
-      cbv [drop_high drop_high_cps].
-      rewrite Tuple.left_tl_cps_correct, push_id.
-      apply small_left_tl.
-    Qed.
-
-    Lemma div_nonzero_neg_iff x y : x < y -> 0 < y ->
-                                    - (x / y) = 0 <-> x <? 0 = false.
-    Proof.
-      repeat match goal with
-             | _ => progress intros
-             | _ => rewrite Z.ltb_ge
-             | _ => rewrite Z.opp_eq_0_iff
-             | _ => rewrite Z.div_small_iff by omega
-             | _ => split
-             | _ => omega
-             end.
-   Qed.
-
-    Lemma eval_sub_then_maybe_add n mask p q r:
-      small p -> small q -> small r ->
-      (map (Z.land mask) r = r) ->
-      (0 <= eval p < eval r) -> (0 <= eval q < eval r) ->
-      eval (@sub_then_maybe_add n mask p q r) = eval p - eval q + (if eval p - eval q <? 0 then eval r else 0).
-    Proof.
-      pose_all.
-      pose proof (@uweight_le_mono _ bound_pos n (S n) (Nat.le_succ_diag_r _)).
-      intros.
-      repeat match goal with
-             | _ => progress (intros; cbv [eval runtime_opp sub_then_maybe_add sub_then_maybe_add_cps] in * )
-             | _ => progress autorewrite with uncps push_id push_basesystem_eval
-             | _ => rewrite eval_drop_high by (apply @B.Positional.small_sat_add; omega)
-             | _ => rewrite B.Positional.sat_sub_mod by omega
-             | _ => rewrite B.Positional.sat_sub_div by omega
-             | _ => rewrite B.Positional.sat_add_mod by omega
-             | _ => rewrite B.Positional.eval_left_append
-             | _ => rewrite eval_join0
-             | H : small _ |- _ => apply eval_small in H
-             end.
-      let H := fresh "H" in
-      match goal with |- context [- (?X / ?Y) = 0] =>
-                      assert ((- (X / Y) = 0) <-> X <? 0 = false) as H
-                             by (apply div_nonzero_neg_iff; omega)
-      end; destruct H.
-      break_match;  try match goal with
-                          H : ?x = ?x -> _ |- _
-                          => specialize (H (eq_refl x)) end;
-      try congruence;
-      match goal with
-      | H : _ |- _ => rewrite Z.ltb_ge in H
-      | H : _ |- _ => rewrite Z.ltb_lt in H
-      end.
-      { repeat (rewrite Z.mod_small; try omega). }
-      { rewrite !Z.mul_opp_r, Z.opp_involutive.
-        rewrite Z.mul_div_eq_full by (subst; auto).
-        match goal with |- context [?a - ?b + ?b] =>
-                        replace (a - b + b) with a by ring end.
-        repeat (rewrite Z.mod_small; try omega). }
-    Qed.
-
-   Lemma small_sub_then_maybe_add n mask (p q r : T n) :
-      small (sub_then_maybe_add mask p q r).
-   Proof.
-     cbv [sub_then_maybe_add_cps sub_then_maybe_add]; intros.
-     repeat progress autounfold. autorewrite with uncps push_id.
-     apply small_drop_high,  @B.Positional.small_sat_add; omega.
-   Qed.
-
-    Lemma map2_zselect n cond x y :
-      Tuple.map2 (n:=n) (Z.zselect cond) x y = if dec (cond = 0) then x else y.
-    Proof.
-      unfold Z.zselect.
-      break_innermost_match; Z.ltb_to_lt; subst; try omega;
-        [ rewrite Tuple.map2_fst, Tuple.map_id
-        | rewrite Tuple.map2_snd, Tuple.map_id ];
-        reflexivity.
-    Qed.
-
-    Lemma eval_conditional_sub_nz n (p:T (S n)) (q:T n)
-          (n_nonzero: (n <> 0)%nat) (psmall : small p) (qsmall : small q):
-      0 <= eval p < eval q + uweight bound n ->
-      eval (conditional_sub p q) = eval p + (if eval q <=? eval p then - eval q else 0).
-    Proof.
-      pose_all.
-      pose proof (@uweight_le_mono _ bound_pos n (S n) (Nat.le_succ_diag_r _)).
-      intros.
-      repeat match goal with
-             | _ => progress (intros; cbv [eval conditional_sub conditional_sub_cps] in * )
-             | _ => progress autorewrite with uncps push_id push_basesystem_eval
-             | _ => rewrite eval_drop_high
-                 by (break_match; try assumption; apply @B.Positional.small_sat_sub; omega)
-             | _ => rewrite map2_zselect
-             | _ => rewrite B.Positional.sat_sub_mod by omega
-             | _ => rewrite B.Positional.sat_sub_div by omega
-             | _ => rewrite B.Positional.sat_add_mod by omega
-             | _ => rewrite B.Positional.eval_left_append
-             | _ => rewrite eval_join0
-             | H : small _ |- _ => apply eval_small in H
-             end.
-      let H := fresh "H" in
-      match goal with |- context [- (?X / ?Y) = 0] =>
-                      assert ((- (X / Y) = 0) <-> X <? 0 = false) as H
-                             by (apply div_nonzero_neg_iff; omega)
-      end; destruct H.
-      break_match;  try match goal with
-                          H : ?x = ?x -> _ |- _
-                          => specialize (H (eq_refl x)) end;
-      repeat match goal with
-      | H : _ |- _ => rewrite Z.leb_gt in H
-      | H : _ |- _ => rewrite Z.leb_le in H
-      | H : _ |- _ => rewrite Z.ltb_lt in H
-      | H : _ |- _ => rewrite Z.ltb_ge in H
-      end; try omega.
-      { rewrite @B.Positional.sat_sub_mod by omega.
-        rewrite eval_join0; cbv [eval].
-        repeat (rewrite Z.mod_small; try omega). }
-      { repeat (rewrite Z.mod_small; try omega). }
-    Qed.
-
-    Lemma eval_conditional_sub n (p:T (S n)) (q:T n)
-           (psmall : small p) (qsmall : small q) :
-      0 <= eval p < eval q + uweight bound n ->
-      eval (conditional_sub p q) = eval p + (if eval q <=? eval p then - eval q else 0).
-    Proof.
-      destruct n; [|solve[auto using eval_conditional_sub_nz]].
-      repeat match goal with
-             | _ => progress (intros; cbv [T tuple tuple'] in p, q)
-             | q : unit |- _ => destruct q
-             | _ => progress (cbv [conditional_sub conditional_sub_cps eval] in * )
-             | _ => progress autounfold
-             | _ => progress (autorewrite with uncps push_id push_basesystem_eval in * )
-             | _ => (rewrite uweight_0 in * )
-             | _ => assert (p = 0) by omega; subst p; break_match; ring
-             end.
-    Qed.
-
-    Lemma small_conditional_sub n (p:T (S n)) (q:T n)
-           (psmall : small p) (qsmall : small q) :
-      0 <= eval p < eval q + uweight bound n ->
-      small (conditional_sub p q).
-    Proof.
-      intros.
-      cbv [conditional_sub conditional_sub_cps]; autorewrite with uncps push_id.
-      eapply small_drop_high.
-      rewrite map2_zselect; break_match; [|assumption].
-      eauto using @B.Positional.small_sat_sub with omega.
-    Qed.
-
-    Lemma eval_scmul n a v : small v -> 0 <= a < bound ->
-      eval (@scmul n a v) = a * eval v.
-    Proof.
-      intro Hsmall. pose_all. apply eval_small in Hsmall.
-      intros. cbv [scmul scmul_cps eval] in *. repeat autounfold.
-      autorewrite with uncps.
-      autorewrite with push_basesystem_eval.
-      autorewrite with uncps push_id push_basesystem_eval.
-      rewrite uweight_0, Z.mul_1_l. apply Z.mod_small.
-      split; [solve[Z.zero_bounds]|]. cbv [uweight] in *.
-      rewrite !Nat2Z.inj_succ, Z.pow_succ_r by auto using Nat2Z.is_nonneg.
-      apply Z.mul_lt_mono_nonneg; omega.
-    Qed.
-
-    Lemma small_scmul n a v : small (@scmul n a v).
-    Proof.
-      cbv [scmul scmul_cps eval] in *. repeat autounfold.
-      autorewrite with uncps push_id push_basesystem_eval.
-      apply small_compact.
-    Qed.
-
-    (* TODO : move to tuple *)
-    Lemma from_list_tl {A n} (ls : list A) H H':
-      from_list n (List.tl ls) H = tl (from_list (S n) ls H').
-    Proof.
-      induction ls; distr_length. simpl List.tl.
-      rewrite from_list_cons, tl_append, <-!(from_list_default_eq a ls).
-      reflexivity.
-    Qed.
-
-    Lemma eval_div n p : small p -> eval (fst (@divmod n p)) = eval p / bound.
-    Proof.
-      cbv [divmod divmod_cps eval]. intros.
-      autorewrite with uncps push_id cancel_pair.
-      rewrite (subst_append p) at 2.
-      rewrite uweight_eval_step. rewrite hd_append, tl_append.
-      rewrite Z.div_add' by omega. rewrite Z.div_small by auto using small_hd.
-      ring.
-    Qed.
-
-    Lemma eval_mod n p : small p -> snd (@divmod n p) = eval p mod bound.
-    Proof.
-      cbv [divmod divmod_cps eval]. intros.
-      autorewrite with uncps push_id cancel_pair.
-      rewrite (subst_append p) at 2.
-      rewrite uweight_eval_step, Z.mod_add'_full, hd_append.
-      rewrite Z.mod_small by auto using small_hd. reflexivity.
-    Qed.
-
-    Lemma small_div n v : small v -> small (fst (@divmod n v)).
-    Proof.
-      cbv [divmod divmod_cps]. intros.
-      autorewrite with uncps push_id cancel_pair.
-      auto using small_tl.
-    Qed.
-  End Proofs.
-End API.
-Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id add_S1_id add_S2_id sub_then_maybe_add_id conditional_sub_id : uncps.
-
-Hint Unfold
-     nonzero_cps
-     nonzero
-     scmul_cps
-     scmul
-     add_cps
-     add
-     add_S1_cps
-     add_S1
-     add_S2_cps
-     add_S2
-     sub_then_maybe_add_cps
-     sub_then_maybe_add
-     conditional_sub_cps
-     conditional_sub
-     eval
-     encode
-  : basesystem_partial_evaluation_unfolder.
-
-Ltac basesystem_partial_evaluation_unfolder t :=
-  let t := (eval cbv delta [
-                   nonzero_cps
-                     nonzero
-                     scmul_cps
-                     scmul
-                     add_cps
-                     add
-                     add_S1_cps
-                     add_S1
-                     add_S2_cps
-                     add_S2
-                     sub_then_maybe_add_cps
-                     sub_then_maybe_add
-                     conditional_sub_cps
-                     conditional_sub
-                     eval
-                     encode
-                 ] in t) in
-  let t := Saturated.AddSub.basesystem_partial_evaluation_unfolder t in
-  let t := Saturated.Wrappers.basesystem_partial_evaluation_unfolder t in
-  let t := Saturated.Core.basesystem_partial_evaluation_unfolder t in
-  let t := Arithmetic.Core.basesystem_partial_evaluation_unfolder t in
-  t.
-
-Ltac Arithmetic.Core.basesystem_partial_evaluation_default_unfolder t ::=
-  basesystem_partial_evaluation_unfolder t.