Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.

2 files changed, 195 insertions, 359 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 23b0c2ef6..dde021b4c 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -1,103 +1,58 @@
 Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
 Require Import Coq.Lists.List.
-Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.BaseSystem.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.BaseSystemProofs.
 Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Util.Notations.
 Require Import Crypto.ModularArithmetic.Pow2Base.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemList.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs.
+Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Tactics.VerdiTactics.
 Local Open Scope Z_scope.
 
-Section PseudoMersenneBase.
-  Context `{prm :PseudoMersenneBaseParams} (modulus_multiple : digits).
-  Local Notation base := (base_from_limb_widths limb_widths).
-
-  Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
-
-  Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x.
-  Local Notation "u ~= x" := (rep u x).
-  Local Hint Unfold rep.
-
-  (* max must be greater than input; this is used to truncate last digit *)
-  Definition encode (x : F modulus) := encodeZ limb_widths x.
-
-  (* Converts from length of extended base to length of base by reduction modulo M.*)
-  Definition reduce (us : digits) : digits :=
-    let high := skipn (length base) us in
-    let low := firstn (length base) us in
-    let wrap := map (Z.mul c) high in
-    BaseSystem.add low wrap.
-
-  Definition mul (us vs : digits) := reduce (BaseSystem.mul ext_base us vs).
-
-  (* In order to subtract without underflowing, we add a multiple of the modulus first. *)
-  Definition sub (us vs : digits) := BaseSystem.sub (add modulus_multiple us) vs.
-
-End PseudoMersenneBase.
-
-Section CarryBasePow2.
+Section ModularBaseSystem.
   Context `{prm :PseudoMersenneBaseParams}.
   Local Notation base := (base_from_limb_widths limb_widths).
-  Local Notation log_cap i := (nth_default 0 limb_widths i).
+  Local Notation digits := (tuple Z (length limb_widths)).
+  Local Arguments to_list {_ _} _.
+  Local Arguments from_list {_ _} _ _.
+  Local Arguments length_to_list {_ _ _}.
+  Local Notation "[[ u ]]" := (to_list u).
 
-  (*
-  Definition carry_and_reduce :=
-    carry_gen limb_widths (fun ci => c * ci).
-   *)
-  Definition carry_and_reduce i := fun us =>
-    let di := nth_default 0 us      i in
-    let us' := set_nth i (Z.pow2_mod di (log_cap i)) us in
-    add_to_nth   0  (c * (Z.shiftr di (log_cap i))) us'.
+  Definition decode (us : digits) : F modulus := decode [[us]].
 
-  Definition carry i : digits -> digits :=
-    if eq_nat_dec i (pred (length base))
-    then carry_and_reduce i
-    else carry_simple limb_widths i.
+  Definition encode (x : F modulus) : digits := from_list (encode x) length_encode.
 
-  Definition carry_sequence is us := fold_right carry us is.
+  Definition add (us vs : digits) : digits := from_list (add [[us]] [[vs]])
+    (add_same_length _ _ _ length_to_list length_to_list).
 
-  Definition carry_full := carry_sequence (full_carry_chain limb_widths).
+  Definition mul (us vs : digits) : digits := from_list (mul [[us]] [[vs]])
+    (length_mul length_to_list length_to_list).
 
-  Definition carry_mul us vs := carry_full (mul us vs).
+  Definition sub (modulus_multiple us vs : digits) : digits :=
+   from_list (sub [[modulus_multiple]] [[us]] [[vs]])
+   (length_sub length_to_list length_to_list length_to_list).
 
-End CarryBasePow2.
+  Definition carry i (us : digits) : digits := from_list (carry i [[us]])
+    (length_carry length_to_list).
 
-Section Canonicalization.
-  Context `{prm :PseudoMersenneBaseParams}.
-  Local Notation base := (base_from_limb_widths limb_widths).
-  Local Notation log_cap i := (nth_default 0 limb_widths i).
-
-  (* compute at compile time *)
-  Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths).
-
-  Definition max_bound i := Z.ones (log_cap i).
-
-  Fixpoint isFull' us full i :=
-    match i with
-    | O => andb (Z.ltb (max_bound 0 - c) (nth_default 0 us 0)) full
-    | S i' => isFull' us (andb (Z.eqb (max_bound i) (nth_default 0 us i)) full) i'
-    end.
-
-  Definition isFull us := isFull' us true (length base - 1)%nat.
+  Definition rep (us : digits) (x : F modulus) := decode us = x.
+  Local Notation "u ~= x" := (rep u x).
+  Local Hint Unfold rep.
 
-  Fixpoint modulus_digits' i :=
-    match i with
-    | O => max_bound i - c + 1 :: nil
-    | S i' => modulus_digits' i' ++ max_bound i :: nil
-    end.
+  Definition carry_sequence is (us : digits) : digits := fold_right carry us is.
 
-  (* compute at compile time *)
-  Definition modulus_digits := modulus_digits' (length base - 1).
+  Definition carry_full : digits -> digits := carry_sequence (full_carry_chain limb_widths).
 
-  Definition and_term us := if isFull us then max_ones else 0.
+  Definition carry_mul (us vs : digits) : digits := carry_full (mul us vs).
 
-  Definition freeze us :=
+  Definition freeze (us : digits) : digits :=
     let us' := carry_full (carry_full (carry_full us)) in
-    let and_term := and_term us' in
-    (* [and_term] is all ones if us' is full, so the subtractions subtract q overall.
-       Otherwise, it's all zeroes, and the subtractions do nothing. *)
-     map2 (fun x y => x - y) us' (map (Z.land and_term) modulus_digits).
+     from_list (conditional_subtract_modulus [[us]] (ge_modulus [[us]]))
+     (length_conditional_subtract_modulus length_to_list).
 
-End Canonicalization.
+End ModularBaseSystem.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index e5ae285de..58f44e8e9 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -1,15 +1,20 @@
 Require Import Zpower ZArith.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import List.
-Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil Crypto.Util.NatUtil.
 Require Import VerdiTactics.
-Require Crypto.BaseSystem.
-Require Import Crypto.ModularArithmetic.ModularBaseSystem Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.BaseSystemProofs Crypto.ModularArithmetic.Pow2Base.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.BaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.ModularArithmetic.Pow2Base.
 Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
-Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemList.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil Crypto.Util.NatUtil.
+Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 Local Open Scope Z_scope.
@@ -18,28 +23,25 @@ Local Open Scope Z_scope.
 Section PseudoMersenneProofs.
   Context `{prm :PseudoMersenneBaseParams}.
 
+  Local Arguments to_list {_ _} _.
+  Local Arguments from_list {_ _} _ _.
+
   Local Hint Unfold decode.
   Local Notation "u ~= x" := (rep u x).
-  Local Notation "u .+ x" := (add u x).
-  Local Notation "u .* x" := (ModularBaseSystem.mul u x).
-  Local Hint Unfold rep.
+  Local Notation digits := (tuple Z (length limb_widths)).
   Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg.
   Local Hint Resolve log_cap_nonneg.
   Local Notation base := (base_from_limb_widths limb_widths).
   Local Notation log_cap i := (nth_default 0 limb_widths i).
 
-  Lemma rep_decode : forall us x, us ~= x -> decode us = x.
-  Proof.
-    autounfold; intuition.
-  Qed.
+  Local Hint Unfold rep decode ModularBaseSystemList.decode.
 
-  Lemma rep_length : forall us x, us ~= x -> length us = length base.
+  Lemma rep_decode : forall us x, us ~= x -> decode us = x.
   Proof.
     autounfold; intuition.
   Qed.
 
-  Lemma decode_rep : forall us, length us = length base ->
-    rep us (decode us).
+  Lemma decode_rep : forall us, rep us (decode us).
   Proof.
     cbv [rep]; auto.
   Qed.
@@ -55,75 +57,32 @@ Section PseudoMersenneProofs.
     pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega.
   Qed. Hint Resolve modulus_pos.
 
-  Lemma encode'_eq : forall (x : F modulus) i, (i <= length limb_widths)%nat ->
-    encode' limb_widths x i = BaseSystem.encode' base x (2 ^ k) i.
+  Lemma encode_eq : forall x : F modulus,
+    ModularBaseSystemList.encode x = BaseSystem.encode base x (2 ^ k).
   Proof.
-    rewrite <-base_length; induction i; intros.
-    + rewrite encode'_zero. reflexivity.
-    + rewrite encode'_succ, <-IHi by omega.
-      simpl; do 2 f_equal.
-      rewrite Z.land_ones, Z.shiftr_div_pow2 by eauto.
-      match goal with H : (S _ <= length base)%nat |- _ =>
-        apply le_lt_or_eq in H; destruct H end.
-      - repeat f_equal; rewrite nth_default_base  by (eauto || omega); reflexivity.
-      - repeat f_equal; try solve [rewrite nth_default_base  by (eauto || omega); reflexivity].
-        rewrite nth_default_out_of_bounds by omega.
-        unfold k.
-        rewrite <-base_length; congruence.
+    cbv [ModularBaseSystemList.encode BaseSystem.encode encodeZ]; intros.
+    rewrite base_length.
+    apply encode'_spec; auto using Nat.eq_le_incl, base_length.
   Qed.
 
-  Lemma encode_eq : forall x : F modulus,
-    encode x = BaseSystem.encode base x (2 ^ k).
+  Lemma encode_rep : forall x : F modulus, encode x ~= x.
   Proof.
-    unfold encode, BaseSystem.encode; intros.
-    rewrite base_length; apply encode'_eq; omega.
+    autounfold; cbv [encode]; intros.
+    rewrite to_list_from_list; autounfold.
+    rewrite encode_eq, encode_rep.
+    + apply ZToField_FieldToZ.
+    + apply bv.
+    + split; [ | etransitivity]; try (apply FieldToZ_range; auto using modulus_pos); auto.
+    + eauto using base_upper_bound_compatible, limb_widths_nonneg.
   Qed.
 
-  Lemma encode_rep : forall x : F modulus, encode x ~= x.
+  Lemma add_rep : forall u v x y, u ~= x -> v ~= y ->
+    add u v ~= (x+y)%F.
   Proof.
-    intros.
-    rewrite encode_eq.
-    unfold encode, rep.
-    split. {
-      unfold BaseSystem.encode.
-      auto using encode'_length.
-    } {
-      unfold decode.
-      rewrite encode_rep.
-      + apply ZToField_FieldToZ.
-      + apply bv.
-      + split; [ | etransitivity]; try (apply FieldToZ_range; auto using modulus_pos); auto.
-      + unfold base_max_succ_divide; intros.
-        match goal with H : (_ <= length base)%nat |- _ =>
-          apply le_lt_or_eq in H; destruct H end.
-        - apply Z.mod_divide.
-          * apply nth_default_base_nonzero; auto using bv, two_k_nonzero.
-          * rewrite !nth_default_eq.
-            do 2 (erewrite nth_indep with (d := 2 ^ k) (d' := 0) by omega).
-            rewrite <-!nth_default_eq.
-            apply base_succ; eauto; omega.
-        - rewrite nth_default_out_of_bounds with (n := S i) by omega.
-          rewrite nth_default_base by (omega || eauto).
-          unfold k.
-          match goal with H : S _ = length base |- _ =>
-            rewrite base_length in H; rewrite <-H end.
-          erewrite sum_firstn_succ by (apply nth_error_Some_nth_default with (x0 := 0); omega).
-          rewrite Z.pow_add_r by (eauto using sum_firstn_limb_widths_nonneg;
-            apply limb_widths_nonneg; rewrite nth_default_eq; apply nth_In; omega).
-          apply Z.divide_factor_r.
-    }
-  Qed.
-
-  Lemma add_rep : forall u v x y, u ~= x -> v ~= y -> BaseSystem.add u v ~= (x+y)%F.
-  Proof.
-    autounfold; intuition. {
-      unfold add.
-      auto using add_same_length.
-    }
-    unfold decode in *; unfold decode in *.
-    rewrite add_rep.
-    rewrite ZToField_add.
-    subst; auto.
+    autounfold; cbv [add]; intros.
+    rewrite to_list_from_list; autounfold.
+    rewrite add_rep, ZToField_add.
+    f_equal; assumption.
   Qed.
 
   Lemma decode_short : forall (us : BaseSystem.digits),
@@ -158,13 +117,11 @@ Section PseudoMersenneProofs.
   Proof.
     intros.
     replace (2^k) with ((2^k - c) + c) by ring.
-    rewrite Z.mul_add_distr_r.
-    rewrite Zplus_mod.
+    rewrite Z.mul_add_distr_r, Zplus_mod.
     unfold c.
     rewrite Z.sub_sub_distr, Z.sub_diag.
     simpl.
-    rewrite Z.mul_comm.
-    rewrite Z.mod_add_l; auto using modulus_nonzero.
+    rewrite Z.mul_comm, Z.mod_add_l; auto using modulus_nonzero.
     rewrite <- Zplus_mod; auto.
   Qed.
 
@@ -190,52 +147,24 @@ Section PseudoMersenneProofs.
     BaseSystem.decode base (reduce us) mod modulus =
     BaseSystem.decode ext_base us mod modulus.
   Proof.
-    intros.
-    rewrite extended_shiftadd.
-    rewrite pseudomersenne_add.
-    unfold reduce.
-    remember (firstn (length base) us) as low.
-    remember (skipn (length base) us) as high.
-    unfold BaseSystem.decode.
-    rewrite BaseSystemProofs.add_rep.
-    replace (map (Z.mul c) high) with (BaseSystem.mul_each c high) by auto.
+    cbv [reduce]; intros.
+    rewrite extended_shiftadd, base_length, pseudomersenne_add, BaseSystemProofs.add_rep.
+    change (map (Z.mul c)) with (BaseSystem.mul_each c).
     rewrite mul_each_rep; auto.
   Qed.
 
-  Lemma reduce_length : forall us,
-      (length base <= length us <= length ext_base)%nat ->
-      (length (reduce us) = length base)%nat.
-  Proof.
-    rewrite extended_base_length.
-    unfold reduce; intros.
-    rewrite add_length_exact.
-    rewrite map_length, firstn_length, skipn_length.
-    rewrite Min.min_l by omega.
-    apply Max.max_l; omega.
-  Qed.
-
-  Lemma length_mul : forall u v,
-      length u = length base
-      -> length v = length base
-      -> length (u .* v) = length base.
-  Proof.
-      autounfold in *; unfold ModularBaseSystem.mul in *; intuition eauto.
-      apply reduce_length.
-      rewrite mul_length_exact, extended_base_length; try omega.
-      destruct u; try congruence.
-      rewrite @nil_length0 in *.
-      pose proof base_length_nonzero; omega.
-  Qed.
-
-  Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> u .* v ~= (x*y)%F.
+  Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> mul u v ~= (x*y)%F.
   Proof.
-    split; autounfold in *; unfold ModularBaseSystem.mul in *.
-    { apply length_mul; intuition auto. }
-    { intuition idtac; subst.
-      rewrite ZToField_mod, reduce_rep, <-ZToField_mod.
-      rewrite mul_rep by (apply ExtBaseVector || rewrite extended_base_length; omega).
-      rewrite 2decode_short by omega.
-      apply ZToField_mul. }
+    autounfold; cbv [mul]; intros.
+    rewrite to_list_from_list; autounfold.
+    cbv [ModularBaseSystemList.mul].
+    rewrite ZToField_mod, reduce_rep.
+    rewrite mul_rep, <-ZToField_mod, ZToField_mul.
+    rewrite <-!decode_short; rewrite ?base_length;
+      auto using Nat.eq_le_incl, length_to_list.
+    + f_equal; assumption.
+    + apply ExtBaseVector.
+    + rewrite extended_base_length, base_length, !length_to_list. omega.
   Qed.
 
   Lemma nth_default_base_positive : forall i, (i < length base)%nat ->
@@ -259,11 +188,11 @@ Section PseudoMersenneProofs.
     apply base_succ; eauto.
   Qed.
 
-  Lemma Fdecode_decode_mod : forall us x, (length us = length base) ->
-    decode us = x -> BaseSystem.decode base us mod modulus = x.
+  Lemma Fdecode_decode_mod : forall us x,
+    decode us = x -> BaseSystem.decode base (to_list us) mod modulus = x.
   Proof.
-    unfold decode; intros ? ? ? decode_us.
-    rewrite <-decode_us.
+    autounfold; intros.
+    rewrite <-H.
     apply FieldToZ_ZToField.
   Qed.
 
@@ -292,31 +221,23 @@ Section PseudoMersenneProofs.
       apply Z.log2_lt_pow2; auto.
   Qed.
 
-  Context mm (mm_length : length mm = length base) (mm_spec : decode mm = 0%F).
-
-  Lemma length_sub :  forall u v,
-      length u = length base
-      -> length v = length base
-      -> length (ModularBaseSystem.sub mm u v) = length base.
-  Proof.
-    autounfold; unfold ModularBaseSystem.sub; intuition idtac.
-    rewrite sub_length, add_length_exact.
-    case_max; try rewrite Max.max_r; omega.
-  Qed.
+  Context (mm : digits) (mm_spec : decode mm = 0%F).
 
   Lemma sub_rep : forall u v x y, u ~= x -> v ~= y ->
     ModularBaseSystem.sub mm u v ~= (x-y)%F.
   Proof.
-    split; autounfold in *.
-    { apply length_sub; intuition (auto; omega). }
-    { unfold decode, ModularBaseSystem.sub, BaseSystem.decode in *; intuition idtac.
-      rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep.
-      rewrite ZToField_sub, ZToField_add.
-      match goal with H : _ = 0%F |- _ => rewrite H end.
-      rewrite F_add_0_l. congruence. }
+    autounfold; cbv [sub]; intros.
+    rewrite to_list_from_list; autounfold.
+    cbv [ModularBaseSystemList.sub].
+    rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep.
+    rewrite ZToField_sub, ZToField_add, ZToField_mod.
+    apply Fdecode_decode_mod in mm_spec; cbv [BaseSystem.decode] in *.
+    rewrite mm_spec, F_add_0_l.
+    f_equal; assumption.
   Qed.
 
 End PseudoMersenneProofs.
+Opaque encode add mul sub.
 
 Section CarryProofs.
   Context `{prm : PseudoMersenneBaseParams}.
@@ -332,101 +253,69 @@ Section CarryProofs.
   Hint Resolve base_length_lt_pred.
 
   Lemma carry_decode_eq_reduce : forall us,
-    (length us = length base) ->
+    (length us = length limb_widths) ->
     BaseSystem.decode base (carry_and_reduce (pred (length base)) us) mod modulus
     = BaseSystem.decode base us mod modulus.
   Proof.
     unfold carry_and_reduce; intros ? length_eq.
     pose proof base_length_nonzero.
-    rewrite add_to_nth_sum by (rewrite length_set_nth; omega).
-    rewrite set_nth_sum by omega.
+    rewrite add_to_nth_sum by (rewrite length_set_nth, base_length; omega).
+    rewrite set_nth_sum by (rewrite base_length; omega).
     rewrite Zplus_comm, <- Z.mul_assoc, <- pseudomersenne_add, BaseSystem.b0_1.
     rewrite (Z.mul_comm (2 ^ k)), <- Zred_factor0.
     f_equal.
     rewrite <- (Z.add_comm (BaseSystem.decode base us)), <- Z.add_assoc, <- Z.add_0_r.
     f_equal.
     destruct (NPeano.Nat.eq_dec (length base) 0) as [length_zero | length_nonzero].
-    + apply length0_nil in length_zero.
-      pose proof (base_length) as limbs_length.
-      rewrite length_zero in length_eq, limbs_length.
-      apply length0_nil in length_eq.
-      symmetry in limbs_length.
-      apply length0_nil in limbs_length.
-      subst; rewrite length_zero, limbs_length, nth_default_nil.
-      reflexivity.
+    + pose proof (base_length) as limbs_length.
+      destruct us; rewrite ?(@nil_length0 Z), ?(@length_cons Z) in *;
+        pose proof base_length_nonzero; omega.
     + rewrite nth_default_base by (omega || eauto).
       rewrite <- Z.add_opp_l, <- Z.opp_sub_distr.
       unfold Z.pow2_mod.
       rewrite Z.land_ones by eauto using log_cap_nonneg.
       rewrite <- Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || eauto using log_cap_nonneg).
       rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg.
-      rewrite Zopp_mult_distr_r.
-      rewrite Z.mul_comm.
-      rewrite Z.mul_assoc.
-      rewrite <- Z.pow_add_r by eauto using log_cap_nonneg.
       unfold k.
       replace (length limb_widths) with (S (pred (length base))) by
         (subst; rewrite <- base_length; apply NPeano.Nat.succ_pred; omega).
       rewrite sum_firstn_succ with (x:= log_cap (pred (length base))) by
         (apply nth_error_Some_nth_default; rewrite <- base_length; omega).
-      rewrite <- Zopp_mult_distr_r.
-      rewrite Z.mul_comm.
-      rewrite (Z.add_comm (log_cap (pred (length base)))).
+      rewrite Z.pow_add_r by eauto using log_cap_nonneg.
       ring.
   Qed.
 
-  Lemma length_carry_and_reduce : forall i us, length (carry_and_reduce i us) = length us.
-  Proof. intros; unfold carry_and_reduce; autorewrite with distr_length; reflexivity. Qed.
-  Hint Rewrite @length_carry_and_reduce : distr_length.
-
-  Lemma length_carry : forall i us, length (carry i us) = length us.
-  Proof. intros; unfold carry; break_if; autorewrite with distr_length; reflexivity. Qed.
-  Hint Rewrite @length_carry : distr_length.
-
-  Local Hint Extern 1 (length _ = _) => progress autorewrite with distr_length.
-
   Lemma carry_rep : forall i us x,
-    (length us = length base) ->
     (i < length base)%nat ->
     us ~= x -> carry i us ~= x.
   Proof.
-    pose proof length_carry. pose proof carry_decode_eq_reduce. pose proof (@carry_simple_decode_eq limb_widths).
+    cbv [carry rep decode]; intros.
+    rewrite to_list_from_list.
+    pose proof carry_decode_eq_reduce. pose proof (@carry_simple_decode_eq limb_widths).
+
     specialize_by eauto.
-    intros; split; auto.
-    unfold rep, decode, carry in *.
-    intuition; break_if; subst; eauto; apply F_eq; simpl; intuition.
+    cbv [ModularBaseSystemList.carry].
+    break_if; subst; eauto.
+    apply F_eq; apply carry_decode_eq_reduce; apply length_to_list.
+    cbv [ModularBaseSystemList.decode].
+    f_equal.
+    apply carry_simple_decode_eq; try omega; rewrite ?base_length; auto using length_to_list.
   Qed.
   Hint Resolve carry_rep.
 
-  Lemma carry_sequence_length: forall is us,
-    (length us = length base)%nat ->
-    (length (carry_sequence is us) = length base)%nat.
-  Proof.
-    induction is; boring.
-  Qed.
-  Hint Resolve carry_sequence_length.
-
   Lemma carry_sequence_rep : forall is us x,
     (forall i, In i is -> (i < length base)%nat) ->
-    (length us = length base) ->
     us ~= x -> carry_sequence is us ~= x.
   Proof.
     induction is; boring.
   Qed.
 
-  Lemma carry_full_length : forall us, (length us = length base)%nat ->
-    length (carry_full us) = length base.
-  Proof.
-    intros; cbv [carry_full]; auto using carry_sequence_length.
-  Qed.
-
   Lemma carry_full_preserves_rep : forall us x,
     rep us x -> rep (carry_full us) x.
   Proof.
     unfold carry_full; intros.
     apply carry_sequence_rep; auto.
     unfold full_carry_chain; rewrite base_length; apply make_chain_lt.
-    eauto using rep_length.
   Qed.
 
   Opaque carry_full.
@@ -438,14 +327,6 @@ Section CarryProofs.
     auto using mul_rep.
   Qed.
 
-  Lemma carry_mul_length : forall us vs,
-    length us = length base -> length vs = length base ->
-    length (carry_mul us vs) = length base.
-  Proof.
-    intros; cbv [carry_mul].
-    auto using carry_full_length, length_mul.
-  Qed.
-
 End CarryProofs.
 
 Hint Rewrite @length_carry_and_reduce @length_carry : distr_length.
@@ -457,13 +338,13 @@ Section CanonicalizationProofs.
   Context (lt_1_length_base : (1 < length base)%nat)
    {B} (B_pos : 0 < B) (B_compat : forall w, In w limb_widths -> w <= B)
    (* on the first reduce step, we add at most one bit of width to the first digit *)
-   (c_reduce1 : c * (Z.ones (B - log_cap (pred (length base)))) < max_bound 0 + 1)
+   (c_reduce1 : c * (Z.ones (B - log_cap (pred (length base)))) < 2 ^ log_cap 0)
    (* on the second reduce step, we add at most one bit of width to the first digit,
       and leave room to carry c one more time after the highest bit is carried *)
-   (c_reduce2 : c <= max_bound 0 - c)
+   (c_reduce2 : c <= nth_default 0 modulus_digits 0)
    (* this condition is probably implied by c_reduce2, but is more straighforward to compute than to prove *)
    (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus).
-
+(*
   (* BEGIN groundwork proofs *)
   Local Hint Resolve (@log_cap_nonneg limb_widths) limb_widths_nonneg.
 
@@ -473,20 +354,20 @@ Section CanonicalizationProofs.
   Qed.
   Local Hint Resolve pow_2_log_cap_pos.
 
-  Lemma max_bound_log_cap : forall i, Z.succ (max_bound i) = 2 ^ log_cap i.
+  Lemma max_value_log_cap : forall i, Z.succ (max_value i) = 2 ^ log_cap i.
   Proof.
     intros.
-    unfold max_bound, Z.ones.
+    unfold max_value, Z.ones.
     rewrite Z.shiftl_1_l.
     omega.
   Qed.
 
-  Lemma pow2_mod_log_cap_range : forall a i, 0 <= Z.pow2_mod a (log_cap i) <= max_bound i.
+  Lemma pow2_mod_log_cap_range : forall a i, 0 <= Z.pow2_mod a (log_cap i) <= max_value i.
   Proof.
     intros.
     unfold Z.pow2_mod.
     rewrite Z.land_ones by eauto using log_cap_nonneg.
-    unfold max_bound, Z.ones.
+    unfold max_value, Z.ones.
     rewrite Z.shiftl_1_l, <-Z.lt_le_pred.
     apply Z_mod_lt.
     pose proof (pow_2_log_cap_pos i).
@@ -499,13 +380,13 @@ Section CanonicalizationProofs.
     pose proof (pow2_mod_log_cap_range a  i); omega.
   Qed.
 
-  Lemma pow2_mod_log_cap_bounds_upper : forall a i, Z.pow2_mod a (log_cap i) <= max_bound i.
+  Lemma pow2_mod_log_cap_bounds_upper : forall a i, Z.pow2_mod a (log_cap i) <= max_value i.
   Proof.
     intros.
     pose proof (pow2_mod_log_cap_range a  i); omega.
   Qed.
 
-  Lemma pow2_mod_log_cap_small : forall a i, 0 <= a <= max_bound i ->
+  Lemma pow2_mod_log_cap_small : forall a i, 0 <= a <= max_value i ->
     Z.pow2_mod a (log_cap i) = a.
   Proof.
     intros.
@@ -513,35 +394,35 @@ Section CanonicalizationProofs.
     rewrite Z.land_ones by eauto using log_cap_nonneg.
     apply Z.mod_small.
     split; try omega.
-    rewrite <- max_bound_log_cap.
+    rewrite <- max_value_log_cap.
     omega.
   Qed.
 
-  Lemma max_bound_pos : forall i, (i < length base)%nat -> 0 < max_bound i.
+  Lemma max_value_pos : forall i, (i < length base)%nat -> 0 < max_value i.
   Proof.
-    unfold max_bound; intros; apply Z.ones_pos_pos.
+    unfold max_value; intros; apply Z.ones_pos_pos.
     apply limb_widths_pos.
     rewrite nth_default_eq.
     apply nth_In.
     rewrite <-base_length; assumption.
   Qed.
-  Local Hint Resolve max_bound_pos.
+  Local Hint Resolve max_value_pos.
 
-  Lemma max_bound_nonneg : forall i, 0 <= max_bound i.
+  Lemma max_value_nonneg : forall i, 0 <= max_value i.
   Proof.
-    unfold max_bound; intros; eauto using Z.ones_nonneg.
+    unfold max_value; intros; eauto using Z.ones_nonneg.
   Qed.
-  Local Hint Resolve max_bound_nonneg.
+  Local Hint Resolve max_value_nonneg.
 
-  Lemma shiftr_eq_0_max_bound : forall i a, Z.shiftr a (log_cap i) = 0 ->
-    a <= max_bound i.
+  Lemma shiftr_eq_0_max_value : forall i a, Z.shiftr a (log_cap i) = 0 ->
+    a <= max_value i.
   Proof.
     intros ? ? shiftr_0.
     apply Z.shiftr_eq_0_iff in shiftr_0.
-    intuition; subst; try apply max_bound_nonneg.
+    intuition; subst; try apply max_value_nonneg.
     match goal with H : Z.log2 _ < log_cap _ |- _ => apply Z.log2_lt_pow2 in H;
-      replace (2 ^ log_cap i) with (Z.succ (max_bound i)) in H by
-        (unfold max_bound, Z.ones; rewrite Z.shiftl_1_l; omega)
+      replace (2 ^ log_cap i) with (Z.succ (max_value i)) in H by
+        (unfold max_value, Z.ones; rewrite Z.shiftl_1_l; omega)
     end; auto.
     omega.
   Qed.
@@ -560,16 +441,16 @@ Section CanonicalizationProofs.
   Qed.
   Local Hint Resolve B_compat_log_cap.
 
-  Lemma max_bound_shiftr_eq_0 : forall i a, 0 <= a -> a <= max_bound i ->
+  Lemma max_value_shiftr_eq_0 : forall i a, 0 <= a -> a <= max_value i ->
     Z.shiftr a (log_cap i) = 0.
   Proof.
-    intros ? ? ? le_max_bound.
+    intros ? ? ? le_max_value.
     apply Z.shiftr_eq_0_iff.
     destruct (Z_eq_dec a 0); auto.
     right.
     split; try omega.
     apply Z.log2_lt_pow2; try omega.
-    rewrite <-max_bound_log_cap.
+    rewrite <-max_value_log_cap.
     omega.
   Qed.
 
@@ -579,7 +460,7 @@ Section CanonicalizationProofs.
   Qed.
 
   (* END groundwork proofs *)
-  Opaque Z.pow2_mod max_bound.
+  Opaque Z.pow2_mod max_value.
 
   (* automation *)
   Ltac carry_length_conditions' := unfold carry_full, add_to_nth;
@@ -611,7 +492,7 @@ Section CanonicalizationProofs.
   (* BEGIN proofs about first carry loop *)
 
   Lemma nth_default_carry_bound_upper : forall i us, (length us = length base) ->
-    nth_default 0 (carry i us) i <= max_bound i.
+    nth_default 0 (carry i us) i <= max_value i.
   Proof.
     unfold carry; intros.
     break_if.
@@ -687,12 +568,12 @@ Section CanonicalizationProofs.
 
   Lemma carry_nothing : forall i j us, (i < length base)%nat ->
     (length us = length base)%nat ->
-    0 <= nth_default 0 us j <= max_bound j ->
+    0 <= nth_default 0 us j <= max_value j ->
     nth_default 0 (carry j us) i = nth_default 0 us i.
   Proof.
     unfold carry, carry_simple, carry_and_reduce; intros.
     break_if; (add_set_nth;
-      [ rewrite max_bound_shiftr_eq_0 by omega; ring
+      [ rewrite max_value_shiftr_eq_0 by omega; ring
       | subst; apply pow2_mod_log_cap_small; assumption ]).
   Qed.
 
@@ -707,16 +588,16 @@ Section CanonicalizationProofs.
     split.
     + rewrite carry_nothing; auto.
       split; [ apply Hcarry_done; auto | ].
-      apply shiftr_eq_0_max_bound.
+      apply shiftr_eq_0_max_value.
       apply Hcarry_done; auto.
     + unfold carry, carry_simple, carry_and_reduce; break_if; subst.
       - add_set_nth; subst.
         * rewrite shiftr_0_i, Z.mul_0_r, Z.add_0_l.
           assumption.
-        * rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound).
+        * rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_value).
           assumption.
       - rewrite shiftr_0_i by omega.
-        rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound).
+        rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_value).
         add_set_nth; subst; rewrite ?Z.add_0_l; auto.
   Qed.
 
@@ -728,7 +609,7 @@ Section CanonicalizationProofs.
 
   Lemma carry_bounds_0_upper : forall us j, (length us = length base) ->
     (0 < j < length base)%nat ->
-    nth_default 0 (carry_sequence (make_chain j) us) 0 <= max_bound 0.
+    nth_default 0 (carry_sequence (make_chain j) us) 0 <= max_value 0.
   Proof.
     induction j as [ | [ | j ] IHj ]; [simpl; intros; omega | | ]; intros.
     + subst; simpl; auto.
@@ -736,7 +617,7 @@ Section CanonicalizationProofs.
     Qed.
 
   Lemma carry_bounds_upper : forall i us j, (0 < i < j)%nat -> (length us = length base) ->
-    nth_default 0 (carry_sequence (make_chain j) us) i <= max_bound i.
+    nth_default 0 (carry_sequence (make_chain j) us) i <= max_value i.
   Proof.
     unfold carry_sequence;
     induction j; [simpl; intros; omega | ].
@@ -815,7 +696,7 @@ Section CanonicalizationProofs.
 
   Lemma carry_full_bounds : forall us i, (i <> 0)%nat -> (forall i, 0 <= nth_default 0 us i) ->
     (length us = length base)%nat ->
-    0 <= nth_default 0 (carry_full us) i <= max_bound i.
+    0 <= nth_default 0 (carry_full us) i <= max_value i.
   Proof.
     unfold carry_full, full_carry_chain; intros.
     split; (destruct (lt_dec i (length limb_widths));
@@ -868,7 +749,7 @@ Section CanonicalizationProofs.
 
   Lemma carry_full_bounds_0 : forall us, pre_carry_bounds us ->
     (length us = length base)%nat ->
-    0 <= nth_default 0 (carry_full us) 0 <= max_bound 0 + c * (Z.ones (B - log_cap (pred (length base)))).
+    0 <= nth_default 0 (carry_full us) 0 <= max_value 0 + c * (Z.ones (B - log_cap (pred (length base)))).
   Proof.
     unfold carry_full, full_carry_chain; intros.
     rewrite <- base_length.
@@ -917,7 +798,7 @@ Section CanonicalizationProofs.
       - apply IHi; auto; omega.
       - rewrite carry_sequence_unaffected by carry_length_conditions.
         apply carry_full_bounds; auto; omega.
-    + rewrite <-max_bound_log_cap, <-Z.add_1_l.
+    + rewrite <-max_value_log_cap, <-Z.add_1_l.
       apply Z.add_le_mono.
       - rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg.
         apply Z.div_floor; auto.
@@ -925,7 +806,7 @@ Section CanonicalizationProofs.
         * simpl.
           eapply Z.le_lt_trans; [ apply carry_full_bounds_0; auto | ].
           replace (2 ^ log_cap 0 * 2) with (2 ^ log_cap 0 + 2 ^ log_cap 0) by ring.
-          rewrite <-max_bound_log_cap, <-Z.add_1_l.
+          rewrite <-max_value_log_cap, <-Z.add_1_l.
           apply Z.add_lt_le_mono; omega.
         * eapply Z.le_lt_trans; [ apply IHi; auto; omega | ].
           apply Z.lt_mul_diag_r; auto; omega.
@@ -935,7 +816,7 @@ Section CanonicalizationProofs.
 
   Lemma carry_full_2_bounds_0 : forall us, pre_carry_bounds us ->
     (length us = length base)%nat -> (1 < length base)%nat ->
-    0 <= nth_default 0 (carry_full (carry_full us)) 0 <= max_bound 0 + c.
+    0 <= nth_default 0 (carry_full (carry_full us)) 0 <= max_value 0 + c.
   Proof.
     intros.
     unfold carry_full at 1 3, full_carry_chain.
@@ -976,7 +857,7 @@ Section CanonicalizationProofs.
       rewrite carry_sequence_unaffected by carry_length_conditions.
       apply carry_full_bounds; carry_length_conditions.
       carry_seq_lower_bound.
-    + rewrite <-max_bound_log_cap, <-Z.add_1_l.
+    + rewrite <-max_value_log_cap, <-Z.add_1_l.
       rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg.
       apply Z.add_le_mono.
       - apply Z.div_le_upper_bound; auto.
@@ -1000,20 +881,20 @@ Section CanonicalizationProofs.
       - eapply carry_full_2_bounds_0; eauto.
       - eapply carry_full_bounds; eauto; carry_length_conditions.
         carry_seq_lower_bound.
-    + rewrite <-max_bound_log_cap, <-Z.add_1_l.
+    + rewrite <-max_value_log_cap, <-Z.add_1_l.
       rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg.
       apply Z.add_le_mono.
       - apply Z.div_floor; auto.
         eapply Z.le_lt_trans; [ eapply carry_full_2_bounds_0; eauto | ].
         replace (Z.succ 1) with (2 ^ 1) by ring.
-        rewrite <-max_bound_log_cap.
+        rewrite <-max_value_log_cap.
         ring_simplify. pose proof c_pos; omega.
       - apply carry_full_bounds; carry_length_conditions; carry_seq_lower_bound.
   Qed.
 
   Lemma carry_full_2_bounds' : forall us i j, pre_carry_bounds us ->
     (length us = length base)%nat -> (0 < i < length base)%nat -> (i + j < length base)%nat -> (j <> 0)%nat ->
-    0 <= nth_default 0 (carry_sequence (make_chain (i + j)) (carry_full (carry_full us))) i <= max_bound i.
+    0 <= nth_default 0 (carry_sequence (make_chain (i + j)) (carry_full (carry_full us))) i <= max_value i.
   Proof.
     induction j; intros; try omega.
     split; (destruct j; [ rewrite Nat.add_1_r; simpl
@@ -1024,7 +905,7 @@ Section CanonicalizationProofs.
 
   Lemma carry_full_2_bounds : forall us i j, pre_carry_bounds us ->
     (length us = length base)%nat -> (0 < i < length base)%nat -> (i < j < length base)%nat ->
-    0 <= nth_default 0 (carry_sequence (make_chain j) (carry_full (carry_full us))) i <= max_bound i.
+    0 <= nth_default 0 (carry_sequence (make_chain j) (carry_full (carry_full us))) i <= max_value i.
   Proof.
     intros.
     replace j with (i + (j - i))%nat by omega.
@@ -1066,36 +947,36 @@ Section CanonicalizationProofs.
 
   Lemma carry_carry_full_2_bounds_0_upper : forall us i, pre_carry_bounds us ->
     (length us = length base)%nat -> (0 < i < length base)%nat ->
-    (nth_default 0 (carry_sequence (make_chain i) (carry_full (carry_full us))) 0 <= max_bound 0 - c)
+    (nth_default 0 (carry_sequence (make_chain i) (carry_full (carry_full us))) 0 <= max_value 0 - c)
     \/ carry_done (carry_sequence (make_chain i) (carry_full (carry_full us))).
   Proof.
     induction i; try omega.
     intros ? length_eq ?; simpl.
     destruct i.
-    + destruct (Z_le_dec (nth_default 0 (carry_full (carry_full us)) 0) (max_bound 0)).
+    + destruct (Z_le_dec (nth_default 0 (carry_full (carry_full us)) 0) (max_value 0)).
       - right.
         apply carry_carry_done_done; try solve [carry_length_conditions].
         apply carry_done_bounds; try solve [carry_length_conditions].
         intros.
         simpl.
         split; [ auto using carry_full_2_bounds_lower | ].
-        destruct i; rewrite <-max_bound_log_cap, Z.lt_succ_r; auto.
+        destruct i; rewrite <-max_value_log_cap, Z.lt_succ_r; auto.
         apply carry_full_bounds; auto using carry_full_bounds_lower.
       - left; unfold carry, carry_simple.
         break_if;
           [ pose proof base_length_nonzero; replace (length base) with 1%nat in *; omega | ].
         add_set_nth. simpl.
         remember ((nth_default 0 (carry_full (carry_full us)) 0)) as x.
-        apply Z.le_trans with (m := (max_bound 0 + c) - (1 + max_bound 0)); try omega.
+        apply Z.le_trans with (m := (max_value 0 + c) - (1 + max_value 0)); try omega.
         replace x with ((x - 2 ^ log_cap 0) + (1 * 2 ^ log_cap 0)) by ring.
         rewrite Z.pow2_mod_spec by eauto.
         cbv [make_chain carry_sequence fold_right].
         rewrite Z.mod_add by (pose proof (pow_2_log_cap_pos 0); omega).
-        rewrite <-max_bound_log_cap, <-Z.add_1_l, Z.mod_small;
+        rewrite <-max_value_log_cap, <-Z.add_1_l, Z.mod_small;
           [ apply Z.sub_le_mono_r; subst; apply carry_full_2_bounds_0; auto | ].
         split; try omega.
         pose proof carry_full_2_bounds_0.
-        apply Z.le_lt_trans with (m := (max_bound 0 + c) - (1 + max_bound 0));
+        apply Z.le_lt_trans with (m := (max_value 0 + c) - (1 + max_value 0));
           [ apply Z.sub_le_mono_r; subst x; apply carry_full_2_bounds_0; auto;
           ring_simplify | ]; pose proof c_pos; omega.
     + rewrite carry_unaffected_low by carry_length_conditions.
@@ -1112,7 +993,7 @@ Section CanonicalizationProofs.
 
   Lemma carry_full_3_bounds : forall us i, pre_carry_bounds us ->
     (length us = length base)%nat ->(i < length base)%nat ->
-    0 <= nth_default 0 (carry_full (carry_full (carry_full us))) i <= max_bound i.
+    0 <= nth_default 0 (carry_full (carry_full (carry_full us))) i <= max_value i.
   Proof.
     intros.
     destruct i; [ | apply carry_full_bounds; carry_length_conditions;
@@ -1132,7 +1013,7 @@ Section CanonicalizationProofs.
     + pose proof (carry_carry_full_2_bounds_0_upper us (pred (length base))).
       assert (0 < pred (length base) < length base)%nat by omega.
       intuition.
-      - replace (max_bound 0) with (c + (max_bound 0 - c)) by ring.
+      - replace (max_value 0) with (c + (max_value 0 - c)) by ring.
         apply Z.add_le_mono; try assumption.
         etransitivity; [ | replace c with (c * 1) by ring; reflexivity ].
         apply Z.mul_le_mono_pos_l; try omega.
@@ -1144,7 +1025,7 @@ Section CanonicalizationProofs.
                         H : carry_done _ |- _ =>
           destruct (H (pred (length base)) H0) as [Hcd1 Hcd2]; rewrite Hcd2 by omega end.
         ring_simplify.
-        apply shiftr_eq_0_max_bound; auto.
+        apply shiftr_eq_0_max_value; auto.
         assert (0 < length base)%nat as zero_lt_length by omega.
         match goal with H : carry_done _ |- _ =>
           destruct (H 0%nat zero_lt_length) end.
@@ -1158,7 +1039,7 @@ Section CanonicalizationProofs.
     intros.
     apply carry_done_bounds; [ carry_length_conditions | intros ].
     destruct (lt_dec i (length base)).
-    + rewrite <-max_bound_log_cap, Z.lt_succ_r.
+    + rewrite <-max_value_log_cap, Z.lt_succ_r.
       auto using carry_full_3_bounds.
     + rewrite nth_default_out_of_bounds; carry_length_conditions.
   Qed.
@@ -1171,7 +1052,7 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma isFull'_last : forall us b j, (j <> 0)%nat -> isFull' us b j = true ->
-    max_bound j = nth_default 0 us j.
+    max_value j = nth_default 0 us j.
   Proof.
     induction j; simpl; intros; try omega.
     match goal with
@@ -1182,7 +1063,7 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma isFull'_lower_bound_0 : forall j us b, isFull' us b j = true ->
-    max_bound 0 - c < nth_default 0 us 0.
+    max_value 0 - c < nth_default 0 us 0.
   Proof.
     induction j; intros.
     + match goal with H : isFull' _ _ 0 = _ |- _ => cbv [isFull'] in H;
@@ -1192,7 +1073,7 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma isFull'_true_full : forall us i j b, (i <> 0)%nat -> (i <= j)%nat -> isFull' us b j = true ->
-    max_bound i = nth_default 0 us i.
+    max_value i = nth_default 0 us i.
   Proof.
     induction j; intros; try omega.
     assert (i = S j \/ i <= j)%nat as cases by omega.
@@ -1235,8 +1116,8 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma full_isFull'_true : forall j us, (length us = length base) ->
-    ( max_bound 0 - c < nth_default 0 us 0
-    /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_bound i)) ->
+    ( max_value 0 - c < nth_default 0 us 0
+    /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_value i)) ->
     isFull' us true j = true.
   Proof.
     induction j; intros.
@@ -1250,8 +1131,8 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma isFull'_true_iff : forall j us, (length us = length base) -> (isFull' us true j = true <->
-    max_bound 0 - c < nth_default 0 us 0
-    /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_bound i)).
+    max_value 0 - c < nth_default 0 us 0
+    /\ (forall i, (0 < i <= j)%nat -> nth_default 0 us i = max_value i)).
   Proof.
     intros; split; intros; auto using full_isFull'_true.
     split; eauto using isFull'_lower_bound_0.
@@ -1264,7 +1145,7 @@ Section CanonicalizationProofs.
     isFull' us true j = true.
   Proof.
     simpl; intros ? ? succ_true.
-    destruct (max_bound (S j) =? nth_default 0 us (S j)); auto.
+    destruct (max_value (S j) =? nth_default 0 us (S j)); auto.
     rewrite isFull'_false in succ_true.
     congruence.
   Qed.
@@ -1399,7 +1280,7 @@ Section CanonicalizationProofs.
   Lemma nth_default_modulus_digits' : forall d j i,
     nth_default d (modulus_digits' j) i =
       if lt_dec i (S j)
-      then (if (eq_nat_dec i 0) then max_bound i - c + 1 else max_bound i)
+      then (if (eq_nat_dec i 0) then max_value i - c + 1 else max_value i)
       else d.
   Proof.
     induction j; intros; (break_if; [| apply nth_default_out_of_bounds; rewrite modulus_digits'_length; omega]).
@@ -1417,7 +1298,7 @@ Section CanonicalizationProofs.
   Lemma nth_default_modulus_digits : forall d i,
     nth_default d modulus_digits i =
       if lt_dec i (length base)
-      then (if (eq_nat_dec i 0) then max_bound i - c + 1 else max_bound i)
+      then (if (eq_nat_dec i 0) then max_value i - c + 1 else max_value i)
       else d.
   Proof.
     unfold modulus_digits; intros.
@@ -1432,7 +1313,7 @@ Section CanonicalizationProofs.
     intros.
     rewrite nth_default_modulus_digits.
     break_if; [ | split; auto; omega].
-    break_if; subst; split; auto; try rewrite <- max_bound_log_cap; pose proof c_pos; omega.
+    break_if; subst; split; auto; try rewrite <- max_value_log_cap; pose proof c_pos; omega.
   Qed.
   Local Hint Resolve carry_done_modulus_digits.
 
@@ -1476,8 +1357,8 @@ Section CanonicalizationProofs.
       rewrite decode'_cons, decode_nil, Z.add_0_r.
       replace z with (nth_default 0 base 0) by (rewrite base_eq; auto).
       rewrite nth_default_base by (omega || eauto).
-      replace (max_bound 0 - c + 1) with (Z.succ (max_bound 0) - c) by ring.
-      rewrite max_bound_log_cap.
+      replace (max_value 0 - c + 1) with (Z.succ (max_value 0) - c) by ring.
+      rewrite max_value_log_cap.
       rewrite sum_firstn_succ with (x := log_cap 0) by (
         apply nth_error_Some_nth_default; rewrite <-base_length; omega).
       rewrite Z.pow_add_r by eauto.
@@ -1488,7 +1369,7 @@ Section CanonicalizationProofs.
       - rewrite sum_firstn_succ with (x := log_cap (S i)) by
           (apply nth_error_Some_nth_default;
           rewrite <-base_length; omega).
-        rewrite Z.pow_add_r, <-max_bound_log_cap, set_higher by eauto.
+        rewrite Z.pow_add_r, <-max_value_log_cap, set_higher by eauto.
         rewrite IHi, modulus_digits'_length by omega.
         rewrite nth_default_base by (omega || eauto).
         ring.
@@ -1515,14 +1396,14 @@ Section CanonicalizationProofs.
     + cbv [modulus_digits' map].
       f_equal.
       apply land_max_ones_noop with (i := 0%nat).
-      rewrite <-max_bound_log_cap.
+      rewrite <-max_value_log_cap.
       pose proof c_pos; omega.
     + unfold modulus_digits'; fold modulus_digits'.
       rewrite map_app.
       f_equal; [ apply IHi; omega | ].
       cbv [map]; f_equal.
       apply land_max_ones_noop with (i := S i).
-      rewrite <-max_bound_log_cap.
+      rewrite <-max_value_log_cap.
       split; auto; omega.
   Qed.
 
@@ -1577,8 +1458,8 @@ Section CanonicalizationProofs.
   Hint Resolve freeze_preserves_rep.
 
   Lemma isFull_true_iff : forall us, (length us = length base) -> (isFull us = true <->
-    max_bound 0 - c < nth_default 0 us 0
-    /\ (forall i, (0 < i <= length base - 1)%nat -> nth_default 0 us i = max_bound i)).
+    max_value 0 - c < nth_default 0 us 0
+    /\ (forall i, (0 < i <= length base - 1)%nat -> nth_default 0 us i = max_value i)).
   Proof.
     unfold isFull; intros; auto using isFull'_true_iff.
   Qed.
@@ -1851,8 +1732,8 @@ Section CanonicalizationProofs.
           apply Z.compare_ge_iff.
           omega.
         * match goal with H : isFull' _ _ _ = true |- _ =>
-            apply isFull'_true_iff in H; try assumption; destruct H as [? eq_max_bound] end.
-          specialize (eq_max_bound j).
+            apply isFull'_true_iff in H; try assumption; destruct H as [? eq_max_value] end.
+          specialize (eq_max_value j).
           omega.
     + apply isFull'_true_iff; try assumption.
       match goal with H : compare' _ _ _ <> Lt |- _ => apply compare'_not_Lt in H; [ destruct H as [Hdigit0 Hnonzero] | | ] end.
@@ -1864,8 +1745,8 @@ Section CanonicalizationProofs.
       - intros.
         rewrite nth_default_modulus_digits.
         repeat (break_if; try omega).
-        rewrite <-Z.lt_succ_r with (m := max_bound i).
-        rewrite max_bound_log_cap; apply carry_done_bounds; assumption.
+        rewrite <-Z.lt_succ_r with (m := max_value i).
+        rewrite max_value_log_cap; apply carry_done_bounds; assumption.
   Qed.
 
   Lemma isFull_compare : forall us, (length us = length base) -> carry_done us ->
@@ -1935,7 +1816,7 @@ Section CanonicalizationProofs.
         specialize (high_digits i i_range).
         clear first_digit i_range.
         rewrite high_digits.
-        rewrite <-max_bound_log_cap.
+        rewrite <-max_value_log_cap.
         rewrite nth_default_modulus_digits.
         repeat (break_if; try omega).
         * rewrite Z.sub_diag.
@@ -2008,5 +1889,5 @@ Section CanonicalizationProofs.
     assert (length vs = length base) by (unfold rep in *; intuition).
     eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption.
   Qed.
-
+*)
 End CanonicalizationProofs.