Added canonicalization to ModularBaseSystemOpt.

1 files changed, 110 insertions, 1 deletions

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