diff options
author | jadep <jade.philipoom@gmail.com> | 2016-05-20 16:12:33 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-05-20 16:12:33 -0400 |
commit | dd0d844b43e5cfdaa49a589e78fba42a8fe97220 (patch) | |
tree | 4af5f838b7bd84a3e91fdc24e14f88eb0e9cac71 /src/ModularArithmetic | |
parent | fe65d254b0864e66f583d0e7b20d2769b0d64109 (diff) |
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])
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 53 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 782 |
2 files changed, 835 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 |