PseudoMersenneBaseRep.mul now carries by default (made possible by strictly base-length digit vectors)

6 files changed, 89 insertions, 77 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index a1258674e..9c6a58f9a 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -61,25 +61,25 @@ 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).
 
+  Definition carry_full := carry_sequence full_carry_chain.
+
+  Definition carry_mul us vs := carry_full (mul us vs).
+
+End CarryBasePow2.
+
+Section Canonicalization.
+  Context `{prm :PseudoMersenneBaseParams}.
+
   (* compute at compile time *)
   Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths).
-  
-  (* compute at compile time? *)
-  Definition carry_full := carry_sequence full_carry_chain.
 
   Definition max_bound i := Z.ones (log_cap i).
 
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index b2c9ee0fa..4fd9748c5 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -28,6 +28,8 @@ Definition nth_default_opt {A} := Eval compute in @nth_default A.
 Definition set_nth_opt {A} := Eval compute in @set_nth A.
 Definition map_opt {A B} := Eval compute in @map A B.
 Definition base_from_limb_widths_opt := Eval compute in base_from_limb_widths.
+Definition full_carry_chain_opt := Eval compute in @full_carry_chain.
+Definition length_opt := Eval compute in length.
 
 Definition Let_In {A P} (x : A) (f : forall y : A, P y)
   := let y := x in f y.
@@ -226,14 +228,35 @@ Section Carries.
   Lemma carry_sequence_opt_cps_rep
        : forall (is : list nat) (us : list Z) (x : F modulus),
          (forall i : nat, In i is -> i < length base)%nat ->
-         length us = length base ->
          rep us x -> rep (carry_sequence_opt_cps is us) x.
   Proof.
     intros.
     rewrite carry_sequence_opt_cps_correct by assumption.
-    apply carry_sequence_rep; assumption.
+    apply carry_sequence_rep; eauto using rep_length.
   Qed.
 
+
+  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 : digits) : { 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 by (auto; apply full_carry_chain_bounds).
+    reflexivity.
+  Defined.
+
+  Definition carry_full_opt (us : digits) : 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).
+
 End Carries.
 
 Section Addition.
@@ -433,33 +456,32 @@ Section Multiplication.
     : mul_opt us vs = mul us vs
     := proj2_sig (mul_opt_sig us vs).
 
-  Lemma mul_opt_rep:
+  Definition carry_mul_opt_sig (us vs : T) : { b : digits | b = carry_mul us vs }.
+  Proof.
+    eexists.
+    cbv [carry_mul].
+    erewrite <-carry_full_opt_correct by eauto.
+    erewrite <-mul_opt_correct.
+    reflexivity.
+  Defined.
+
+  Definition carry_mul_opt (us vs : T) : digits
+    := Eval cbv [proj1_sig carry_mul_opt_sig] in proj1_sig (carry_mul_opt_sig us vs).
+
+  Definition carry_mul_opt_correct us vs
+    : carry_mul_opt us vs = carry_mul us vs
+    := proj2_sig (carry_mul_opt_sig us vs).
+
+  Lemma carry_mul_opt_rep:
     forall (u v : T) (x y : F modulus), PseudoMersenneBaseRep.rep u x -> PseudoMersenneBaseRep.rep v y ->
-    PseudoMersenneBaseRep.rep (mul_opt u v) (x * y)%F.
+    PseudoMersenneBaseRep.rep (carry_mul_opt u v) (x * y)%F.
   Proof.
     intros.
-    rewrite mul_opt_correct.
-    change mul with PseudoMersenneBaseRep.mul.
+    rewrite carry_mul_opt_correct.
+    change carry_mul with PseudoMersenneBaseRep.mul.
     auto using PseudoMersenneBaseRep.mul_rep.
   Qed.
 
-  Definition carry_mul_opt 
-             (is : list nat)
-             (us vs : list Z)
-             : list Z
-    := carry_sequence_opt_cps c_ is (mul_opt us vs).
-
-  Lemma carry_mul_opt_correct
-    : forall (is : list nat) (us vs : list Z) (x  y: F modulus),
-      PseudoMersenneBaseRep.rep us x -> PseudoMersenneBaseRep.rep vs y ->
-      (forall i : nat, In i is -> i < length base)%nat ->
-      length (mul_opt us vs) = length base ->
-      PseudoMersenneBaseRep.rep (carry_mul_opt is us vs) (x*y)%F.
-  Proof.
-    intros is us vs x y; intros.
-    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.
 
 Section Canonicalization.
@@ -475,8 +497,6 @@ Section Canonicalization.
 
   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 :
@@ -494,27 +514,6 @@ Section Canonicalization.
   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.
@@ -536,8 +535,7 @@ Section Canonicalization.
   Proof.
     eexists.
     cbv beta iota delta [freeze map2].
-    repeat rewrite <-carry_full_opt_correct.
-    change (@carry_full modulus prm) with @carry_full_opt.
+    repeat erewrite <-carry_full_opt_correct by eauto.
     change and_term with and_term_opt.
     change @map with @map_opt.
     reflexivity.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 0aa83ae6b..562c7d6d4 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -22,6 +22,11 @@ Section PseudoMersenneProofs.
     autounfold; intuition.
   Qed.
 
+  Lemma rep_length : forall us x, us ~= x -> length us = length base.
+  Proof.
+    autounfold; intuition.
+  Qed.
+
   Lemma encode_rep : forall x : F modulus, encode x ~= x.
   Proof.
     intros. unfold encode, rep.
@@ -385,6 +390,31 @@ Section CarryProofs.
     induction is; boring.
   Qed.
 
+
+  (* TODO : move? *)
+  Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat.
+  Proof.
+    induction x; simpl; intuition.
+  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.
+
+  Lemma carry_mul_rep : forall us vs x y, rep us x -> rep vs y ->
+    rep (carry_mul us vs) (x * y)%F.
+  Proof.
+    unfold carry_mul; intros; apply carry_full_preserves_rep.
+    auto using mul_rep.
+  Qed.
+
 End CarryProofs.
 
 Section CanonicalizationProofs.
@@ -1132,22 +1162,6 @@ Section CanonicalizationProofs.
 
   (* END proofs about third carry loop *)
 
-  (* TODO : move? *)
-  Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat.
-  Proof.
-    induction x; simpl; intuition.
-  Qed.
-
-  Lemma carry_full_preserves_rep : forall us x, (length us = length base)%nat ->
-    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.
-  Qed.
-
-  Opaque carry_full.
-
   Lemma isFull'_false : forall us n, isFull' us false n = false.
   Proof.
     unfold isFull'; induction n; intros; rewrite Bool.andb_false_r; auto.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseRep.v b/src/ModularArithmetic/PseudoMersenneBaseRep.v
index 5f3644cca..6b4d29a35 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseRep.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseRep.v
@@ -45,6 +45,6 @@ Instance PseudoMersenneBase m (prm : PseudoMersenneBaseParams m) (sc : Subtracti
   sub := ModularBaseSystem.sub coeff coeff_mod;
   sub_rep := ModularBaseSystemProofs.sub_rep coeff coeff_mod coeff_length;
 
-  mul := ModularBaseSystem.mul;
-  mul_rep := ModularBaseSystemProofs.mul_rep
+  mul := ModularBaseSystem.carry_mul;
+  mul_rep := ModularBaseSystemProofs.carry_mul_rep
 }.
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index b004a60d1..31dee21f3 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -45,7 +45,7 @@ Lemma GF1305Base26_mul_reduce_formula :
                       -> rep ls (f*g)%F}.
 Proof.
   eexists; intros ? ? Hf Hg.
-  pose proof (carry_mul_opt_correct k_ c_ (eq_refl k) (eq_refl c_) [0;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg.
+  pose proof (carry_mul_opt_rep k_ c_ (eq_refl k) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
 Defined.
 
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 68278ce4c..37e0c08db 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -47,7 +47,7 @@ Lemma GF25519Base25Point5_mul_reduce_formula :
                       -> rep ls (f*g)%F}.
 Proof.
   eexists; intros ? ? Hf Hg.
-  pose proof (carry_mul_opt_correct k_ c_ (eq_refl k_) (eq_refl c_) [0;9;8;7;6;5;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg.
+  pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
 Time Defined.