First stage of canonicalization proofs complete; proved 3 carry loops reduce input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1])

3 files changed, 934 insertions, 0 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 324834b76..558b9a5a2 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -62,3 +62,56 @@ Section CarryBasePow2.
   Definition carry_sequence is us := fold_right carry us is.
 
 End CarryBasePow2.
+
+Section Canonicalization.
+  Context `{prm :PseudoMersenneBaseParams}.
+
+  Fixpoint make_chain i :=
+    match i with
+    | O => nil
+    | S i' => i' :: make_chain i'
+    end.
+
+  (* compute at compile time *)
+  Definition full_carry_chain := make_chain (length limb_widths).
+
+  (* compute at compile time *)
+  Definition max_ones := Z.ones
+    ((fix loop current_max lw :=
+      match lw with
+      | nil => current_max
+      | w :: lw' => loop (Z.max w current_max) lw'
+      end
+    ) 0 limb_widths).
+  
+  (* compute at compile time? *)
+  Definition carry_full := carry_sequence full_carry_chain.
+
+  Definition max_bound i := Z.ones (log_cap i).
+
+  Definition isFull us := 
+    (fix loop full i :=
+      match i with
+      | O => full (* don't test 0; the test for 0 is the initial value of [full]. *)
+      | S i' => loop (andb (Z.eqb (max_bound i) (nth_default 0 us i)) full) i'
+      end
+    ) (Z.ltb (max_bound 0 - (c + 1)) (nth_default 0 us 0)) (length us - 1)%nat.
+
+  Fixpoint range' n m :=
+    match m with
+    | O => nil
+    | S m' => (n - m)%nat :: range' n m'
+    end.
+
+  Definition range n := range' n n.
+
+  Definition land_max_bound and_term i := Z.land and_term (max_bound i). 
+    
+  Definition freeze us :=
+    let us' := carry_full (carry_full (carry_full us)) in
+    let and_term := if isFull us' then max_ones else 0 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. *)
+       map (fun x => (snd x) - land_max_bound and_term (fst x)) (combine (range (length us')) us').
+   
+End Canonicalization.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index d9f1bd393..274acff5a 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -1,4 +1,5 @@
 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.
 Require Import VerdiTactics.
@@ -395,3 +396,784 @@ Section CarryProofs.
   Qed.
 
 End CarryProofs.
+
+Section CanonicalizationProofs.
+  Context `{prm : PseudoMersenneBaseParams} (lt_1_length_base : (1 < length base)%nat) (c_pos : 0 < c) {B} (B_pos : 0 < B) (B_compat : forall w, In w limb_widths -> w <= B).
+
+  (* TODO : move *)
+  Lemma set_nth_nth_default : forall {A} (d:A) n x l i, (0 <= i < length l)%nat ->
+    nth_default d (set_nth n x l) i =
+    if (eq_nat_dec i n) then x else nth_default d l i.
+  Proof.
+    induction n; (destruct l; [intros; simpl in *; omega | ]); simpl;
+      destruct i; break_if; try omega; intros; try apply nth_default_cons;
+        rewrite !nth_default_cons_S, ?IHn; try break_if; omega || reflexivity.
+  Qed.
+
+  (* TODO : move *)
+  Lemma add_to_nth_nth_default : forall n x l i, (0 <= i < length l)%nat ->
+    nth_default 0 (add_to_nth n x l) i =
+    if (eq_nat_dec i n) then x + nth_default 0 l i else nth_default 0 l i.
+  Proof.
+    intros.
+    unfold add_to_nth.
+    rewrite set_nth_nth_default by assumption.
+    break_if; subst; reflexivity.
+  Qed.
+
+  (* TODO : move *)
+  Lemma length_add_to_nth : forall n x l, length (add_to_nth n x l) = length l.
+  Proof.
+    unfold add_to_nth; intros; apply length_set_nth.
+  Qed.
+
+  (* TODO : move *)
+  Lemma singleton_list : forall {A} (l : list A), length l = 1%nat -> exists x, l = x :: nil.
+  Proof.
+    intros; destruct l; simpl in *; try congruence.
+    eexists; f_equal.
+    apply length0_nil; omega.
+  Qed.
+
+  (* BEGIN groundwork proofs *)
+
+  Lemma pow_2_log_cap_pos : forall i, 0 < 2 ^ log_cap i.
+  Proof.
+    intros; apply Z.pow_pos_nonneg; auto using log_cap_nonneg; omega.
+  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.
+  Proof.
+    intros.
+    unfold max_bound, Z.ones.
+    rewrite Z.shiftl_1_l.
+    omega.
+  Qed.
+
+  Hint Resolve log_cap_nonneg.
+  Lemma pow2_mod_log_cap_range : forall a i, 0 <= pow2_mod a (log_cap i) <= max_bound i.
+  Proof.
+    intros.
+    unfold pow2_mod.
+    rewrite Z.land_ones by apply log_cap_nonneg.
+    unfold max_bound, Z.ones.
+    rewrite Z.shiftl_1_l, <-Z.lt_le_pred.
+    apply Z_mod_lt.
+    pose proof (pow_2_log_cap_pos i).
+    omega.
+  Qed.
+
+  Lemma pow2_mod_log_cap_bounds_lower : forall a i, 0 <= pow2_mod a (log_cap i).
+  Proof.
+    intros.
+    pose proof (pow2_mod_log_cap_range a  i); omega.
+  Qed.
+
+  Lemma pow2_mod_log_cap_bounds_upper : forall a i, pow2_mod a (log_cap i) <= max_bound 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 ->
+    pow2_mod a (log_cap i) = a.
+  Proof.
+    intros.
+    unfold pow2_mod.
+    rewrite Z.land_ones by apply log_cap_nonneg.
+    apply Z.mod_small.
+    split; try omega.
+    rewrite <- max_bound_log_cap.
+    omega.
+  Qed.
+
+  Lemma max_bound_nonneg : forall i, 0 <= max_bound i.
+  Proof.
+    unfold max_bound; intros; auto using Z_ones_nonneg.
+  Qed.
+  Local Hint Resolve max_bound_nonneg.
+
+  Lemma pow2_mod_spec : forall a b, (0 <= b) -> pow2_mod a b = a mod (2 ^ b).
+  Proof.
+    intros.
+    unfold pow2_mod.
+    rewrite Z.land_ones; auto.
+  Qed.
+
+  Lemma pow2_mod_upper_bound : forall a b, (0 <= a) -> (0 <= b) -> pow2_mod a b <= a.
+  Proof.
+    intros.
+    unfold pow2_mod.
+    rewrite Z.land_ones; auto.
+    apply Z.mod_le; auto.
+    apply Z.pow_pos_nonneg; omega.
+  Qed.
+
+  Lemma shiftr_eq_0_max_bound : forall i a, Z.shiftr a (log_cap i) = 0 ->
+    a <= max_bound i.
+  Proof.
+    intros ? ? shiftr_0.
+    apply Z.shiftr_eq_0_iff in shiftr_0.
+    intuition; subst; try apply max_bound_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)
+    end; auto.
+    omega.
+  Qed.
+
+  Lemma B_compat_log_cap : forall i, 0 <= B - log_cap i.
+  Proof.
+    unfold log_cap; intros.
+    destruct (lt_dec i (length limb_widths)).
+    + apply Z.le_0_sub.
+      apply B_compat.
+      rewrite nth_default_eq.
+      apply nth_In; assumption.
+    + replace (nth_default 0 limb_widths i) with 0; try omega.
+      symmetry; apply nth_default_out_of_bounds.
+      omega.
+  Qed.
+  Local Hint Resolve B_compat_log_cap.
+
+  Lemma max_bound_shiftr_eq_0 : forall i a, 0 <= a -> a <= max_bound i ->
+    Z.shiftr a (log_cap i) = 0.
+  Proof.
+    intros ? ? ? le_max_bound.
+    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.
+    omega.
+  Qed.
+
+  (* END groundwork proofs *)
+  Opaque pow2_mod log_cap max_bound.
+
+  (* automation *)
+  Ltac carry_length_conditions' := unfold carry_full, add_to_nth;
+    rewrite ?length_set_nth, ?carry_length_exact, ?carry_sequence_length_exact, ?carry_sequence_length_exact;
+    try omega; try solve [pose proof base_length; pose proof base_length_nonzero; omega || auto ].
+  Ltac carry_length_conditions := try split; try omega; repeat carry_length_conditions'.
+
+  Ltac add_set_nth := rewrite ?add_to_nth_nth_default; try solve [carry_length_conditions];
+    try break_if; try omega; rewrite ?set_nth_nth_default; try solve [carry_length_conditions];
+    try break_if; try omega.
+
+  (* BEGIN defs *)
+
+  Definition c_carry_constraint : Prop :=
+    (c * (Z.ones (B - log_cap (pred (length base)))) < max_bound 0 + 1)
+    /\ (max_bound 0 + c < 2 ^ (log_cap 0 + 1))
+    /\ (c <= max_bound 0 - c).
+
+  Definition pre_carry_bounds us := forall i, 0 <= nth_default 0 us i <
+    if (eq_nat_dec i 0) then 2 ^ B else 2 ^ B - 2 ^ (B - log_cap (pred i)).
+
+  Lemma pre_carry_bounds_nonzero : forall us, pre_carry_bounds us ->
+    (forall i, 0 <= nth_default 0 us i).
+  Proof.
+    unfold pre_carry_bounds.
+    intros ? PCB i.
+    specialize (PCB i).
+    omega.
+  Qed.
+  Hint Resolve pre_carry_bounds_nonzero.
+
+  Definition carry_done us := forall i, (i < length base)%nat -> Z.shiftr (nth_default 0 us i) (log_cap i) = 0.
+
+  Lemma carry_carry_done_done : forall i us,
+    (length us = length base)%nat ->
+    (i < length base)%nat ->
+    (forall i, 0 <= nth_default 0 us i) ->
+    carry_done us -> carry_done (carry i us).
+  Proof.
+    unfold carry_done; intros until 3. intros Hcarry_done ? ?.
+    unfold carry, carry_simple, carry_and_reduce; break_if; subst.
+    + rewrite Hcarry_done by omega.
+      rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound).
+      destruct i0; add_set_nth; rewrite ?Z.mul_0_r, ?Z.add_0_l; auto.
+      match goal with H : S _ = pred (length base) |- _ => rewrite H; auto end.
+   + rewrite Hcarry_done by omega.
+     rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound).
+     destruct i0; add_set_nth; subst; rewrite ?Z.add_0_l; auto.    
+  Qed.
+
+  (* END defs *)
+
+  (* 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.
+  Proof.
+    unfold carry; intros.
+    break_if.
+    + unfold carry_and_reduce.
+      add_set_nth.
+      apply pow2_mod_log_cap_bounds_upper.
+    + unfold carry_simple.
+      destruct (lt_dec i (length us)).
+      - add_set_nth.
+        apply pow2_mod_log_cap_bounds_upper.
+      - rewrite nth_default_out_of_bounds by carry_length_conditions; auto.
+  Qed.
+
+  Lemma nth_default_carry_bound_lower : forall i us, (length us = length base) ->
+    0 <= nth_default 0 (carry i us) i.
+  Proof.
+    unfold carry; intros.
+    break_if.
+    + unfold carry_and_reduce.
+      add_set_nth.
+      apply pow2_mod_log_cap_bounds_lower.
+    + unfold carry_simple.
+      destruct (lt_dec i (length us)).
+      - add_set_nth.
+        apply pow2_mod_log_cap_bounds_lower.
+      - rewrite nth_default_out_of_bounds by carry_length_conditions; omega.
+  Qed.
+
+  Lemma nth_default_carry_bound_succ_lower : forall i us, (forall i, 0 <= nth_default 0 us i) ->
+    (length us = length base) ->
+    0 <= nth_default 0 (carry i us) (S i).
+  Proof.
+    unfold carry; intros ? ? PCB ? .
+    break_if.
+    + subst. replace (S (pred (length base))) with (length base) by omega.
+      rewrite nth_default_out_of_bounds; carry_length_conditions.
+      unfold carry_and_reduce.
+      add_set_nth.
+    + unfold carry_simple.
+      destruct (lt_dec (S i) (length us)).
+      - add_set_nth.
+        apply Z.add_nonneg_nonneg; [ apply Z.shiftr_nonneg | ]; unfold pre_carry_bounds in PCB.
+        * specialize (PCB i). omega.
+        * specialize (PCB (S i)). omega.
+      - rewrite nth_default_out_of_bounds by carry_length_conditions; omega.
+  Qed.
+
+  Lemma carry_unaffected_low : forall i j us, ((0 < i < j)%nat \/ (i = 0 /\ j <> 0 /\ j <> pred (length base))%nat)->
+    (length us = length base) -> 
+    nth_default 0 (carry j us) i = nth_default 0 us i.
+  Proof.
+    intros.
+    unfold carry.
+    break_if.
+    + unfold carry_and_reduce.
+      add_set_nth.
+    + unfold carry_simple.
+      destruct (lt_dec i (length us)).
+      - add_set_nth.
+      - rewrite !nth_default_out_of_bounds by
+          (omega || rewrite length_add_to_nth; rewrite length_set_nth; pose proof base_length_nonzero; omega).
+        reflexivity.
+  Qed.
+  
+  Lemma carry_unaffected_high : forall i j us, (S j < i)%nat -> (length us = length base) ->
+    nth_default 0 (carry j us) i = nth_default 0 us i.
+  Proof.
+    intros.
+    destruct (lt_dec i (length us));
+      [ | rewrite !nth_default_out_of_bounds by carry_length_conditions; reflexivity].
+    unfold carry, carry_simple.
+    break_if; add_set_nth.
+  Qed.
+
+  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 ->
+    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
+      | subst; apply pow2_mod_log_cap_small; assumption ]).
+  Qed.
+
+  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.
+  Proof.
+    unfold carry_sequence; induction j; [simpl; intros; omega | ].
+    intros.
+    simpl in *.
+    destruct (eq_nat_dec 0 j).
+    + subst. 
+      apply nth_default_carry_bound_upper; fold (carry_sequence (make_chain 0) us); carry_length_conditions.
+    + rewrite carry_unaffected_low; try omega.
+        fold (carry_sequence (make_chain j) us); carry_length_conditions.
+    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.
+  Proof.
+    unfold carry_sequence;
+    induction j; [simpl; intros; omega | ].
+    intros.
+    simpl in *.
+    assert (i = j \/ i < j)%nat as cases by omega.
+    destruct cases as [eq_j_i | lt_i_j]; subst.
+    + apply nth_default_carry_bound_upper; fold (carry_sequence (make_chain j) us); carry_length_conditions.
+    + rewrite carry_unaffected_low; try omega.
+      fold (carry_sequence (make_chain j) us); carry_length_conditions.
+  Qed.
+
+  Lemma carry_sequence_unaffected : forall i us j, (j < i)%nat -> (length us = length base)%nat -> 
+    nth_default 0 (carry_sequence (make_chain j) us) i = nth_default 0 us i.
+  Proof.
+    induction j; [simpl; intros; omega | ].
+    intros.
+    simpl in *.
+    rewrite carry_unaffected_high by carry_length_conditions.
+    apply IHj; omega.
+  Qed.
+
+  Lemma carry_sequence_bounds_lower : forall j i us, (length us = length base) ->
+    (forall i, 0 <= nth_default 0 us i) -> (j <= length base)%nat ->
+    0 <= nth_default 0 (carry_sequence (make_chain j) us) i.
+  Proof.
+    induction j; intros.
+    + simpl. auto.
+    + simpl.
+      destruct (lt_dec (S j) i).
+      - rewrite carry_unaffected_high by carry_length_conditions.
+        apply IHj; auto; omega.
+      - assert ((i = S j) \/ (i = j) \/ (i < j))%nat as cases by omega.
+        destruct cases as [? | [? | ?]].
+        * subst. apply nth_default_carry_bound_succ_lower; carry_length_conditions.
+          intros.
+          eapply IHj; auto; omega.
+        * subst. apply nth_default_carry_bound_lower; carry_length_conditions.
+        * destruct (eq_nat_dec j (pred (length base)));
+            [ | rewrite carry_unaffected_low by carry_length_conditions; apply IHj; auto; omega ].
+          subst.
+          unfold carry, carry_and_reduce; break_if; try omega.
+          add_set_nth; [ | apply IHj; auto; omega ].
+          apply Z.add_nonneg_nonneg; [ | apply IHj; auto; omega ].
+          apply Z.mul_nonneg_nonneg; try omega.
+          apply Z.shiftr_nonneg.
+          apply IHj; auto; omega.
+  Qed.
+
+  Lemma carry_bounds_lower : forall i us j, (0 < i <= j)%nat -> (length us = length base) ->
+    (forall i, 0 <= nth_default 0 us i) -> (j <= length base)%nat ->
+    0 <= nth_default 0 (carry_sequence (make_chain j) us) i.
+  Proof.
+    unfold carry_sequence;
+    induction j; [simpl; intros; omega | ].
+    intros.
+    simpl in *.
+    destruct (eq_nat_dec i (S j)).
+    + subst. apply nth_default_carry_bound_succ_lower; auto;
+        fold (carry_sequence (make_chain j) us); carry_length_conditions.
+      intros.
+      apply carry_sequence_bounds_lower; auto; omega.
+    + assert (i = j \/ i < j)%nat as cases by omega.
+      destruct cases as [eq_j_i | lt_i_j]; subst;
+        [apply nth_default_carry_bound_lower| rewrite carry_unaffected_low]; try omega;
+        fold (carry_sequence (make_chain j) us); carry_length_conditions.
+      apply carry_sequence_bounds_lower; auto; omega.
+  Qed.
+
+  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.
+  Proof.
+    unfold carry_full, full_carry_chain; intros.
+    split; (destruct (lt_dec i (length limb_widths));
+              [ | rewrite nth_default_out_of_bounds by carry_length_conditions; omega || auto ]).
+    + apply carry_bounds_lower; carry_length_conditions.
+    + apply carry_bounds_upper; carry_length_conditions.
+  Qed.
+
+  Lemma carry_simple_no_overflow : forall us i, (i < pred (length base))%nat ->
+    length us = length base ->
+    0 <= nth_default 0 us i < 2 ^ B ->
+    0 <= nth_default 0 us (S i) < 2 ^ B - 2 ^ (B - log_cap i) ->
+    0 <= nth_default 0 (carry i us) (S i) < 2 ^ B.
+  Proof.
+    intros.
+    unfold carry, carry_simple; break_if; try omega.
+    add_set_nth.
+    replace (2 ^ B) with (2 ^ (B - log_cap i) + (2 ^ B - 2 ^ (B - log_cap i))) by omega.
+    split.
+    + apply Z.add_nonneg_nonneg; try omega.
+      apply Z.shiftr_nonneg; try omega.
+    + apply Z.add_lt_mono; try omega.
+      rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
+      apply Z.div_lt_upper_bound; try apply pow_2_log_cap_pos.
+      rewrite <-Z.pow_add_r by (apply log_cap_nonneg || apply B_compat_log_cap).
+      replace (log_cap i + (B - log_cap i)) with B by ring.
+      omega.
+  Qed.
+
+
+  Lemma carry_sequence_no_overflow : forall i us, pre_carry_bounds us ->
+    (length us = length base) ->
+    nth_default 0 (carry_sequence (make_chain i) us) i < 2 ^ B.
+  Proof.
+    unfold pre_carry_bounds.
+    intros ? ? PCB ?.
+    induction i.
+    + simpl. specialize (PCB 0%nat).
+      intuition.
+    + simpl.
+      destruct (lt_eq_lt_dec i (pred (length base))) as [[? | ? ] | ? ].
+      - apply carry_simple_no_overflow; carry_length_conditions.
+        apply carry_sequence_bounds_lower; carry_length_conditions.
+        apply carry_sequence_bounds_lower; carry_length_conditions.
+        rewrite carry_sequence_unaffected; try omega.
+        specialize (PCB (S i)); rewrite Nat.pred_succ in PCB.
+        break_if; intuition.
+      - unfold carry; break_if; try omega.
+        rewrite nth_default_out_of_bounds; [ apply Z.pow_pos_nonneg; omega | ].
+        subst.
+        unfold carry_and_reduce.
+        carry_length_conditions.
+      - rewrite nth_default_out_of_bounds; [ apply Z.pow_pos_nonneg; omega | ].
+        carry_length_conditions.
+  Qed.
+
+  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)))).
+  Proof.
+    unfold carry_full, full_carry_chain; intros.
+    rewrite <- base_length.
+    replace (length base) with (S (pred (length base))) at 1 2 by omega.
+    simpl.
+    unfold carry, carry_and_reduce; break_if; try omega.
+    add_set_nth.
+    split.
+    + apply Z.add_nonneg_nonneg.
+      - apply Z.mul_nonneg_nonneg; try omega.
+        apply Z.shiftr_nonneg.
+        apply carry_sequence_bounds_lower; auto; omega.
+      - apply carry_sequence_bounds_lower; auto; omega.
+    + rewrite Z.add_comm.
+      apply Z.add_le_mono.
+      - apply carry_bounds_0_upper; auto; omega.
+      - apply Z.mul_le_mono_pos_l; auto.
+        apply Z_shiftr_ones; auto;
+          [ | pose proof (B_compat_log_cap (pred (length base))); omega ].
+        split.
+        * apply carry_bounds_lower; auto; try omega.
+        * apply carry_sequence_no_overflow; auto.
+  Qed.
+
+  Lemma carry_full_bounds_lower : forall i us, pre_carry_bounds us ->
+    (length us = length base)%nat ->
+    0 <= nth_default 0 (carry_full us) i.
+  Proof.
+   destruct i; intros.
+   + apply carry_full_bounds_0; auto.
+   + destruct (lt_dec (S i) (length base)).
+     - apply carry_bounds_lower; carry_length_conditions.
+     - rewrite nth_default_out_of_bounds; carry_length_conditions.
+  Qed.
+ 
+  (* END proofs about first carry loop *)
+ 
+  (* BEGIN proofs about second carry loop *)
+
+  Lemma carry_sequence_carry_full_bounds_same : forall us i, pre_carry_bounds us -> c_carry_constraint ->
+    (length us = length base)%nat -> (0 < i < length base)%nat ->
+    0 <= nth_default 0 (carry_sequence (make_chain i) (carry_full us)) i <= 2 ^ log_cap i.
+  Proof.
+    induction i; intros; try omega.
+    simpl.
+    unfold carry, carry_simple; break_if; try omega.
+    add_set_nth.
+    split.
+    + apply Z.add_nonneg_nonneg.
+      - apply Z.shiftr_nonneg.
+        destruct (eq_nat_dec i 0); subst.
+        * simpl.
+          apply carry_full_bounds_0; auto.
+        * 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.
+      apply Z.add_le_mono.
+      - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
+        apply Z_div_floor; auto.
+        destruct i.
+        * 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.
+          apply Z.add_lt_le_mono; try omega.
+          unfold c_carry_constraint in *.
+          intuition.
+        * eapply Z.le_lt_trans; [ apply IHi; auto; omega | ].
+          apply Z.lt_mul_diag_r; auto; omega. 
+      - rewrite carry_sequence_unaffected by carry_length_conditions.
+        apply carry_full_bounds; auto; omega.
+  Qed.
+
+  Lemma carry_full_2_bounds_0 : forall us, pre_carry_bounds us -> c_carry_constraint ->
+    (length us = length base)%nat -> (1 < length base)%nat ->
+    0 <= nth_default 0 (carry_full (carry_full us)) 0 <= max_bound 0 + c.
+  Proof.
+    intros.
+    unfold carry_full at 1 3, full_carry_chain.
+    rewrite <-base_length.
+    replace (length base) with (S (pred (length base))) by (pose proof base_length_nonzero; omega).
+    simpl.
+    unfold carry, carry_and_reduce; break_if; try omega.
+    add_set_nth.
+    split.
+    + apply Z.add_nonneg_nonneg.
+      apply Z.mul_nonneg_nonneg; try omega.
+      apply Z.shiftr_nonneg.
+      apply carry_sequence_carry_full_bounds_same; auto; omega.
+      eapply carry_sequence_bounds_lower; eauto; carry_length_conditions.
+      intros.
+      eapply carry_sequence_bounds_lower; eauto; carry_length_conditions.
+    + rewrite Z.add_comm.
+      apply Z.add_le_mono.
+      - apply carry_bounds_0_upper; carry_length_conditions.
+      - replace c with (c * 1) at 2 by ring.
+        apply Z.mul_le_mono_pos_l; try omega.
+        rewrite Z.shiftr_div_pow2 by auto.
+        apply Z.div_le_upper_bound; auto.
+        ring_simplify.
+        apply carry_sequence_carry_full_bounds_same; auto.
+        omega.
+  Qed.
+
+  Lemma carry_full_2_bounds_succ : forall us i, pre_carry_bounds us -> c_carry_constraint ->
+    (length us = length base)%nat -> (0 < i < pred (length base))%nat ->
+    ((0 < i < length base)%nat ->
+      0 <= nth_default 0
+        (carry_sequence (make_chain i) (carry_full (carry_full us))) i <=
+      2 ^ log_cap i) ->
+      0 <= nth_default 0 (carry_simple i
+        (carry_sequence (make_chain i) (carry_full (carry_full us)))) (S i) <= 2 ^ log_cap (S i).
+  Proof.
+    unfold carry_simple; intros ? ? PCB CCC length_eq ? IH.
+    add_set_nth.
+    split.
+    + apply Z.add_nonneg_nonneg.
+      apply Z.shiftr_nonneg. 
+      destruct i;
+        [ simpl; pose proof (carry_full_2_bounds_0 us PCB CCC length_eq); omega | ].
+      - assert (0 < S i < length base)%nat as IHpre by omega.
+        specialize (IH IHpre).
+        omega.
+      - rewrite carry_sequence_unaffected by carry_length_conditions.
+        apply carry_full_bounds; carry_length_conditions.
+        intros.
+        apply carry_sequence_bounds_lower; eauto; carry_length_conditions.
+    + rewrite <-max_bound_log_cap, <-Z.add_1_l.
+      rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
+      apply Z.add_le_mono.
+      - apply Z.div_le_upper_bound; auto.
+        ring_simplify. apply IH. omega.
+      - rewrite carry_sequence_unaffected by carry_length_conditions.
+        apply carry_full_bounds; carry_length_conditions.
+        intros; apply carry_sequence_bounds_lower; eauto; carry_length_conditions.
+  Qed.
+
+  Lemma carry_full_2_bounds_same : forall us i, pre_carry_bounds us -> c_carry_constraint ->
+    (length us = length base)%nat -> (0 < i < length base)%nat ->
+    0 <= nth_default 0 (carry_sequence (make_chain i) (carry_full (carry_full us))) i <= 2 ^ log_cap i.
+  Proof.
+    intros; induction i; try omega.
+    simpl; unfold carry.
+    break_if; try omega.
+    split; (destruct (eq_nat_dec i 0); subst;
+      [ cbv [make_chain carry_sequence fold_right carry_simple]; add_set_nth
+      | eapply carry_full_2_bounds_succ; eauto; omega]).
+    + apply Z.add_nonneg_nonneg.
+      apply Z.shiftr_nonneg.
+      eapply carry_full_2_bounds_0; eauto.
+      eapply carry_full_bounds; eauto; carry_length_conditions.
+      intros; apply carry_sequence_bounds_lower; eauto; carry_length_conditions.
+    + rewrite <-max_bound_log_cap, <-Z.add_1_l.
+      rewrite Z.shiftr_div_pow2 by apply 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 <-Z.pow_add_r by (omega || auto).
+        unfold c_carry_constraint in *.
+        intuition.
+      - apply carry_full_bounds; carry_length_conditions.
+        intros; apply carry_sequence_bounds_lower; eauto; carry_length_conditions.
+  Qed.
+
+  Lemma carry_full_2_bounds' : forall us i j, pre_carry_bounds us -> c_carry_constraint ->
+    (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.
+  Proof.
+    induction j; intros; try omega.
+    split; (destruct j; [ rewrite Nat.add_1_r; simpl 
+                         | rewrite <-plus_n_Sm; simpl; rewrite carry_unaffected_low by carry_length_conditions; eapply IHj; eauto; omega ]).
+    + apply nth_default_carry_bound_lower; carry_length_conditions.
+    + apply nth_default_carry_bound_upper; carry_length_conditions.
+  Qed.
+
+  Lemma carry_full_2_bounds : forall us i j, pre_carry_bounds us -> c_carry_constraint ->
+    (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.
+  Proof.
+    intros.
+    replace j with (i + (j - i))%nat by omega.
+    eapply carry_full_2_bounds'; eauto; omega.
+  Qed.
+
+  Lemma carry_carry_full_2_bounds_0_lower : forall us i, pre_carry_bounds us -> c_carry_constraint ->
+    (length us = length base)%nat -> (0 < i < length base)%nat ->
+    (0 <= nth_default 0 (carry_sequence (make_chain i) (carry_full (carry_full us))) 0).
+  Proof.
+    induction i; try omega.
+    intros ? ? length_eq ?; simpl.
+    destruct i.
+    + unfold carry.
+      break_if;
+        [ pose proof base_length_nonzero; replace (length base) with 1%nat in *; omega | ].
+      simpl.
+      unfold carry_simple.
+      add_set_nth.
+      apply pow2_mod_log_cap_bounds_lower.
+    + rewrite carry_unaffected_low by carry_length_conditions.
+      assert (0 < S i < length base)%nat by omega. 
+      intuition.
+  Qed.
+
+  Lemma carry_full_2_bounds_lower :forall us i, pre_carry_bounds us -> c_carry_constraint ->
+    (length us = length base)%nat ->
+    0 <= nth_default 0 (carry_full (carry_full us)) i.
+  Proof.
+    intros.
+    destruct i.
+    + apply carry_full_2_bounds_0; auto.
+    + apply carry_full_bounds; try solve [carry_length_conditions].
+      intro j.
+      destruct j.
+      - apply carry_full_bounds_0; auto.
+      - apply carry_full_bounds; carry_length_conditions.
+  Qed.
+
+  Lemma carry_carry_full_2_bounds_0_upper : forall us i, pre_carry_bounds us -> c_carry_constraint ->
+    (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)
+    \/ 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)).
+      - right.
+        unfold carry_done.
+        intros.
+        apply max_bound_shiftr_eq_0; simpl; rewrite carry_nothing; try solve [carry_length_conditions].
+        * apply carry_full_2_bounds_lower; auto.
+        * split; try apply carry_full_2_bounds_lower; auto.
+        * destruct i; auto.
+          apply carry_full_bounds; try solve [carry_length_conditions].
+          auto using carry_full_bounds_lower.
+        * split; auto.
+          apply carry_full_2_bounds_lower; auto.
+      - unfold carry.
+        break_if;
+          [ pose proof base_length_nonzero; replace (length base) with 1%nat in *; omega | ].
+        simpl.
+        unfold carry_simple.
+        add_set_nth. left.
+        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)).
+        * replace x with ((x - 2 ^ log_cap 0) + (1 * 2 ^ log_cap 0)) by ring.
+          rewrite pow2_mod_spec by auto.
+          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.
+          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.sub_le_mono_r; subst x; apply carry_full_2_bounds_0; auto;
+            ring_simplify; unfold c_carry_constraint in *; omega | ].
+          ring_simplify; unfold c_carry_constraint in *; omega.
+        * ring_simplify; unfold c_carry_constraint in *; omega.
+    + rewrite carry_unaffected_low by carry_length_conditions.
+      assert (0 < S i < length base)%nat by omega. 
+      intuition.
+      right.
+      apply carry_carry_done_done; try solve [carry_length_conditions].
+      intro j.
+      destruct j.
+      - apply carry_carry_full_2_bounds_0_lower; auto.
+      - destruct (lt_eq_lt_dec j i) as [[? | ?] | ?].
+        * apply carry_full_2_bounds; auto; omega.
+        * subst. apply carry_full_2_bounds_same; auto; omega.
+        * rewrite carry_sequence_unaffected; try solve [carry_length_conditions].
+          apply carry_full_2_bounds_lower; auto; omega.
+  Qed.
+ 
+  (* END proofs about second carry loop *)
+ 
+  (* BEGIN proofs about third carry loop *)
+
+  Lemma carry_full_3_bounds : forall us i, pre_carry_bounds us -> c_carry_constraint ->
+    (length us = length base)%nat ->(i < length base)%nat ->
+    0 <= nth_default 0 (carry_full (carry_full (carry_full us))) i <= max_bound i.
+  Proof.
+    intros.
+    destruct i; [ | apply carry_full_bounds; carry_length_conditions;
+                    do 2 (intros; apply carry_sequence_bounds_lower; eauto; carry_length_conditions) ].
+    unfold carry_full at 1 4, full_carry_chain.
+    case_eq limb_widths; [intros; pose proof limb_widths_nonnil; congruence | ].
+    simpl.
+    intros ? ? limb_widths_eq.
+    replace (length l) with (pred (length limb_widths)) by (rewrite limb_widths_eq; auto).
+    rewrite <- base_length.
+    unfold carry, carry_and_reduce; break_if; try omega; intros.
+    add_set_nth.
+    split.
+    + apply Z.add_nonneg_nonneg.
+      - apply Z.mul_nonneg_nonneg; auto; try omega.
+        apply Z.shiftr_nonneg.
+        eapply carry_full_2_bounds_same; eauto; omega.
+      - eapply carry_carry_full_2_bounds_0_lower; eauto; omega.
+    + 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.
+        apply Z.add_le_mono; try assumption.
+        replace c with (c * 1) at 2 by ring.
+        apply Z.mul_le_mono_pos_l; try omega.
+        rewrite Z.shiftr_div_pow2 by auto.
+        apply Z.div_le_upper_bound; auto.
+        ring_simplify.
+        apply carry_full_2_bounds_same; auto.
+      - match goal with H : carry_done _ |- _ => unfold carry_done in H; rewrite H by omega end.
+        ring_simplify.
+        apply shiftr_eq_0_max_bound; auto; omega.
+  Qed.
+
+  Lemma nth_error_combine : forall {A B} i (x : A) (x' : B) l l', nth_error l i = Some x ->
+    nth_error l' i = Some x' -> nth_error (combine l l') i = Some (x, x').
+  Admitted.
+
+  Lemma nth_error_range : forall {A} i (l : list A), (i < length l)%nat ->
+    nth_error (range (length l)) i = Some i.
+  Admitted.
+
+  (* END proofs about third carry loop *)
+  Opaque carry_full.
+
+  Lemma freeze_in_bounds : forall us i, (us <> nil)%nat ->
+    0 <= nth_default 0 (freeze us) i < 2 ^ log_cap i.
+  Proof.
+  Admitted.
+
+  Lemma freeze_canonical : forall us vs x, rep us x -> rep vs x ->
+    freeze us = freeze vs.
+  Admitted.
+
+End CanonicalizationProofs.
\ No newline at end of file
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index bc7e9d740..1b7cfafdc 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -297,6 +297,94 @@ Proof.
   apply Z_mod_mult.
 Qed.
 
+  Lemma Z_ones_succ : forall x, (0 <= x) ->
+    Z.ones (Z.succ x) = 2 ^ x + Z.ones x.
+  Proof.
+    unfold Z.ones; intros.
+    rewrite !Z.shiftl_1_l.
+    rewrite Z.add_pred_r.
+    apply Z.succ_inj.
+    rewrite !Z.succ_pred.
+    rewrite Z.pow_succ_r; omega.
+  Qed.
+
+  Lemma Z_div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c.
+  Proof.
+    intros.
+    apply Z.lt_succ_r.
+    apply Z.div_lt_upper_bound; try omega.
+  Qed.
+
+  Lemma Z_shiftr_1_r_le : forall a b, a <= b ->
+    Z.shiftr a 1 <= Z.shiftr b 1.
+  Proof.
+    intros.
+    rewrite !Z.shiftr_div_pow2, Z.pow_1_r by omega.
+    apply Z.div_le_mono; omega.
+  Qed.
+
+  Lemma Z_ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1.
+  Proof.
+    induction i; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega.
+    intros.
+    unfold Z.ones.
+    rewrite !Z.shiftl_1_l, Z.shiftr_div_pow2, <-!Z.sub_1_r, Z.pow_1_r, <-!Z.add_opp_r by omega.
+    replace (2 ^ (Z.pos p)) with (2 ^ (Z.pos p - 1)* 2).
+    rewrite Z.div_add_l by omega.
+    reflexivity.
+    replace 2 with (2 ^ 1) at 2 by auto.
+    rewrite <-Z.pow_add_r by (pose proof (Pos2Z.is_pos p); omega).
+    f_equal. omega.
+  Qed.
+
+  Lemma Z_shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) ->
+    Z.shiftr a i <= Z.ones (n - i) \/ n <= i.
+  Proof.
+    intros until 1.
+    apply natlike_ind.
+    + unfold Z.ones.
+      rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r.
+      omega.
+    + intros. 
+      destruct (Z_lt_le_dec x n); try omega.
+      intuition.
+      left.
+      rewrite shiftr_succ.
+      replace (n - Z.succ x) with (Z.pred (n - x)) by omega.
+      rewrite Z_ones_pred by omega.
+      apply Z_shiftr_1_r_le.
+      assumption.
+  Qed.
+
+  Lemma Z_shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) ->
+    Z.shiftr a i <= Z.ones (n - i) .
+  Proof.
+    intros a n i G G0 G1.
+    destruct (Z_le_lt_eq_dec i n G1). 
+    + destruct (Z_shiftr_ones' a n G i G0); omega.
+    + subst; rewrite Z.sub_diag.
+      destruct (Z_eq_dec a 0).
+      - subst; rewrite Z.shiftr_0_l; reflexivity.
+      - rewrite Z.shiftr_eq_0; try omega; try reflexivity.
+        apply Z.log2_lt_pow2; omega.
+  Qed.
+
+  Lemma Z_shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1.
+  Proof.
+    intros a ? ? [a_nonneg a_upper_bound].
+    apply Z_le_lt_eq_dec in a_upper_bound.
+    destruct a_upper_bound.
+    + destruct (Z_eq_dec 0 a).
+      - subst; rewrite Z.shiftr_0_l; omega.
+      - rewrite Z.shiftr_eq_0; auto; try omega.
+        apply Z.log2_lt_pow2; auto; omega.
+    + subst.
+      rewrite Z.shiftr_div_pow2 by assumption.
+      rewrite Z.div_same; try omega.
+      assert (0 < 2 ^ n) by (apply Z.pow_pos_nonneg; omega).
+      omega.
+  Qed.
+
 (* prove that known nonnegative numbers are nonnegative *)
 Ltac zero_bounds' :=
   repeat match goal with
@@ -317,3 +405,14 @@ Ltac zero_bounds' :=
   end; try omega; try prime_bound; auto.
 
 Ltac zero_bounds := try omega; try prime_bound; zero_bounds'.
+
+  Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i.
+  Proof.
+    apply natlike_ind.
+    + unfold Z.ones. simpl; omega.
+    + intros.
+      rewrite Z_ones_succ by assumption.
+      zero_bounds.
+      apply Z.pow_nonneg; omega.
+  Qed.
+