Added canonicalization to ModularBaseSystemOpt.

3 files changed, 124 insertions, 16 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index c25f89785..7989d641d 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -89,7 +89,7 @@ Section Canonicalization.
     | 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 us - 1)%nat.
+  Definition isFull us := isFull' us true (length base - 1)%nat.
 
   Fixpoint modulus_digits' i :=
     match i with
@@ -108,10 +108,12 @@ Section Canonicalization.
                   | b :: lb' => f a b :: map2 f la' lb'
                   end
     end.
+
+  Definition and_term us := if isFull us then max_ones else 0.
     
   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
+    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).
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 981680b4a..71841d871 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -460,4 +460,113 @@ Section Multiplication.
     change (carry_mul_opt _ _ _) with (carry_sequence_opt_cps c_ is (mul_opt us vs)).
     apply carry_sequence_opt_cps_rep, mul_opt_rep; auto.
   Qed.
-End Multiplication.
\ No newline at end of file
+End Multiplication.
+
+Section Canonicalization.
+  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}
+    (* allows caller to precompute k and c *)
+    (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_)
+    (lt_1_length_base : (1 < length base)%nat)
+    {int_width} (int_width_pos : 0 < int_width) (int_width_compat : forall w, In w limb_widths -> w <= int_width)
+    (c_pos : 0 < c)
+    (c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < max_bound 0 + 1)
+    (c_reduce2 : c <= max_bound 0 - c)
+    (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus).
+
+  Print freeze.
+  Definition max_ones_opt := Eval compute in max_ones.
+  Definition max_bound_opt := Eval compute in max_bound.
+  Definition full_carry_chain_opt := Eval compute in full_carry_chain.
+  Definition length_opt := Eval compute in length.
+  Definition minus_opt := Eval compute in minus.
+
+  Definition isFull'_opt_sig (us : T) full i :
+    { b : bool | b = isFull' us full i }.
+  Proof.
+    eexists.
+    cbv [isFull'].
+    change max_bound with max_bound_opt.
+    reflexivity.
+  Defined.
+
+  Definition isFull'_opt (us : T) full i: bool
+    := Eval cbv [proj1_sig isFull'_opt_sig] in proj1_sig (isFull'_opt_sig us full i).
+
+  Definition isFull'_opt_correct us full i: isFull'_opt us full i = isFull' us full i :=
+    proj2_sig (isFull'_opt_sig us full i).
+
+  Lemma full_carry_chain_bounds : forall i, In i full_carry_chain -> (i < length base)%nat.
+  Proof.
+    unfold full_carry_chain; rewrite <-base_length; intros.
+    apply make_chain_lt; auto.
+  Qed.
+
+  Definition carry_full_opt_sig (us : T) : { b : digits | b = carry_full us }.
+  Proof.
+    eexists.
+    cbv [carry_full].
+    change full_carry_chain with full_carry_chain_opt.
+    rewrite <-(carry_sequence_opt_cps_correct c_) by (auto; apply full_carry_chain_bounds).
+    reflexivity.
+  Defined.
+
+  Definition carry_full_opt (us : T) : digits
+    := Eval cbv [proj1_sig carry_full_opt_sig] in proj1_sig (carry_full_opt_sig us).
+
+  Definition carry_full_opt_correct us : carry_full_opt us = carry_full us :=
+    proj2_sig (carry_full_opt_sig us).
+
+  Definition and_term_opt_sig (us : T) : { b : Z | b = and_term us }.
+  Proof.
+    eexists.
+    cbv [and_term isFull].
+    change length with length_opt.
+    rewrite <-isFull'_opt_correct.
+    change max_ones with max_ones_opt.
+    reflexivity.
+  Defined.
+
+  Definition and_term_opt (us : T) : Z
+    := Eval cbv [proj1_sig and_term_opt_sig] in proj1_sig (and_term_opt_sig us).
+
+  Definition and_term_opt_correct us : and_term_opt us = and_term us :=
+    proj2_sig (and_term_opt_sig us).
+
+  Definition freeze_opt_sig (us : T) :
+    { b : digits | b = freeze us }.
+  Proof.
+    eexists.
+    cbv beta iota delta [freeze map2].
+    repeat rewrite <-carry_full_opt_correct.
+    change (@carry_full modulus prm) with @carry_full_opt.
+    change and_term with and_term_opt.
+    change @map with @map_opt.
+    reflexivity.
+  Defined.
+
+  Definition freeze_opt (us : T) : digits
+    := Eval cbv [proj1_sig freeze_opt_sig] in proj1_sig (freeze_opt_sig us).
+
+  Definition freeze_opt_correct us
+    : freeze_opt us = freeze us
+    := proj2_sig (freeze_opt_sig us).
+
+  Lemma freeze_opt_canonical: forall us vs x,
+    @pre_carry_bounds _ _ int_width us -> (length us = length base) -> rep us x -> 
+    @pre_carry_bounds _ _ int_width vs -> (length vs = length base) -> rep vs x ->
+    freeze_opt us = freeze_opt vs.
+  Proof.
+    intros.
+    rewrite !freeze_opt_correct.
+    eapply freeze_canonical with (B := int_width); eauto.
+  Qed.
+
+  Lemma freeze_opt_preserves_rep : forall us x, (length us = length base) ->
+    rep us x -> rep (freeze_opt us) x.
+  Proof.
+    intros.
+    rewrite freeze_opt_correct.
+    eauto using freeze_preserves_rep.
+  Qed.
+
+End Canonicalization.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 350660323..8ac3a0faa 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -1229,9 +1229,6 @@ Section CanonicalizationProofs.
     right.
     apply IHl; auto using in_cons.
   Qed.
-  (*
-  Local Hint Resolve max_ones_nonneg. *)
-
 
   Lemma land_max_ones_noop : forall x i, 0 <= x < 2 ^ log_cap i -> Z.land max_ones x = x.
   Proof.
@@ -1343,7 +1340,7 @@ Section CanonicalizationProofs.
   Proof.
     destruct ls1; reflexivity.
   Qed.
-  Hint Resolve map2_nil_r map2_nil_l.
+  Local Hint Resolve map2_nil_r map2_nil_l.
 
   Opaque map2.
 
@@ -1651,7 +1648,7 @@ Section CanonicalizationProofs.
   Proof.
     unfold rep; intros.
     intuition; rewrite ?freeze_length; auto.
-    unfold freeze.
+    unfold freeze, and_term.
     break_if.
     + apply decode_mod with (us := carry_full (carry_full (carry_full us))).
       - rewrite carry_full_3_length; auto.
@@ -1679,14 +1676,14 @@ Section CanonicalizationProofs.
 
   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 us - 1)%nat -> nth_default 0 us i = max_bound i)).
+    /\ (forall i, (0 < i <= length base - 1)%nat -> nth_default 0 us i = max_bound i)).
   Proof.
     unfold isFull; intros; auto using isFull'_true_iff.
   Qed.
-
+  
   Definition minimal_rep us := BaseSystem.decode base us = (BaseSystem.decode base us) mod modulus.
 
-   Fixpoint compare' us vs i :=
+  Fixpoint compare' us vs i :=
     match i with
     | O => Eq
     | S i' => if Z_eq_dec (nth_default 0 us i') (nth_default 0 vs i')
@@ -1695,7 +1692,7 @@ Section CanonicalizationProofs.
     end.
 
   (* Lexicographically compare two vectors of equal length, starting from the END of the list
-     (in our context, this is the most significant end). *)
+     (in our context, this is the most significant end). NOT constant time. *)
   Definition compare us vs := compare' us vs (length us).
 
   Lemma compare'_Eq : forall us vs i, (length us = length vs) ->
@@ -2012,7 +2009,7 @@ Section CanonicalizationProofs.
     pre_carry_bounds us -> (length us = length base) ->
     carry_done (freeze us).
   Proof.
-    unfold freeze; intros ? PCB lengths_eq.
+    unfold freeze, and_term; intros ? PCB lengths_eq.
     rewrite carry_done_bounds by simpl_lengths; intro i.
     rewrite nth_default_map2 with (d1 := 0) (d2 := 0).
     simpl_lengths.
@@ -2030,7 +2027,7 @@ Section CanonicalizationProofs.
         rewrite carry_done_bounds in cf3_done by simpl_lengths.
         specialize (cf3_done 0%nat).
         omega.
-      - assert ((0 < i <= length (carry_full (carry_full (carry_full us))) - 1)%nat) as i_range by
+      - assert ((0 < i <= length base - 1)%nat) as i_range by
           (simpl_lengths; apply lt_min_l in l; omega).
         specialize (high_digits i i_range).
         clear first_digit i_range.
@@ -2054,7 +2051,7 @@ Section CanonicalizationProofs.
   Lemma freeze_minimal_rep : forall us, pre_carry_bounds us -> (length us = length base) ->
     minimal_rep (freeze us).
   Proof.
-    unfold minimal_rep, freeze.
+    unfold minimal_rep, freeze, and_term.
     intros.
     symmetry. apply Z.mod_small.
     split; break_if; rewrite decode_map2_sub; simpl_lengths.
@@ -2106,4 +2103,4 @@ Section CanonicalizationProofs.
     intros; eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption.
   Qed.
 
-End CanonicalizationProofs.
+End CanonicalizationProofs.
\ No newline at end of file