blob: af2c1a679d5cf4ac97e41dabf6bb8029ed280549 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
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.
|
