diff options
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/ModularArithmetic/ExtPow2BaseMulProofs.v | 34 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 8 |
3 files changed, 35 insertions, 8 deletions
diff --git a/_CoqProject b/_CoqProject index 3936cf40b..3b197c40c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -34,6 +34,7 @@ src/Experiments/EdDSARefinement.v src/Experiments/GenericFieldPow.v src/Experiments/SpecEd25519.v src/Experiments/SpecificCurve25519.v +src/ModularArithmetic/ExtPow2BaseMulProofs.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v diff --git a/src/ModularArithmetic/ExtPow2BaseMulProofs.v b/src/ModularArithmetic/ExtPow2BaseMulProofs.v new file mode 100644 index 000000000..af2c1a679 --- /dev/null +++ b/src/ModularArithmetic/ExtPow2BaseMulProofs.v @@ -0,0 +1,34 @@ +Require Import Coq.ZArith.ZArith Coq.Lists.List. +Require Import Crypto.BaseSystem. +Require Import Crypto.BaseSystemProofs. +Require Import Crypto.ModularArithmetic.Pow2Base. +Require Import Crypto.ModularArithmetic.Pow2BaseProofs. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.Util.ListUtil. + +Local Open Scope Z_scope. + +Section ext_mul. + Context (limb_widths : list Z) + (limb_widths_nonnegative : forall x, In x limb_widths -> 0 <= x). + Local Notation k := (sum_firstn limb_widths (length limb_widths)). + Local Notation base := (base_from_limb_widths limb_widths). + Context (bv : BaseVector base) + (limb_widths_match_modulus : forall i j, + (i < length limb_widths)%nat -> + (j < length limb_widths)%nat -> + (i + j >= length limb_widths)%nat -> + let w_sum := sum_firstn limb_widths in + k + w_sum (i + j - length limb_widths)%nat <= w_sum i + w_sum j). + + Local Hint Resolve firstn_us_base_ext_base ExtBaseVector bv. + + Lemma mul_rep_extended : forall (us vs : BaseSystem.digits), + (length us <= length base)%nat -> + (length vs <= length base)%nat -> + (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode (ext_base limb_widths) (BaseSystem.mul (ext_base limb_widths) us vs). + Proof. + intros; apply mul_rep_two_base; auto; + distr_length. + Qed. +End ext_mul. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 76a7399e3..e6351dc17 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -106,14 +106,6 @@ Section PseudoMersenneProofs. Local Hint Resolve firstn_us_base_ext_base bv ExtBaseVector limb_widths_match_modulus. Local Hint Extern 1 => apply limb_widths_match_modulus. - Lemma mul_rep_extended : forall (us vs : BaseSystem.digits), - (length us <= length base)%nat -> - (length vs <= length base)%nat -> - (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode (ext_base limb_widths) (BaseSystem.mul (ext_base limb_widths) us vs). - Proof. - intros; apply mul_rep_two_base; auto with arith distr_length. - Qed. - Lemma modulus_nonzero : modulus <> 0. pose proof (Znumtheory.prime_ge_2 _ prime_modulus); omega. Qed. |