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

1 files changed, 30 insertions, 16 deletions

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.