blob: 359b4313ba8d08f8a43c60eaced524826cd42d05 (
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
35
36
37
38
39
|
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.Notations.
Require Export Crypto.Util.FixCoqMistakes.
Import Nat.
Local Open Scope Z.
Class BaseVector (base : list Z):= {
base_positive : forall b, In b base -> b > 0; (* nonzero would probably work too... *)
b0_1 : forall x, nth_default x base 0 = 1; (** TODO(jadep,jgross): change to [nth_error base 0 = Some 1], then use [nth_error_value_eq_nth_default] to prove a [forall x, nth_default x base 0 = 1] as a lemma *)
base_good :
forall i j, (i+j < length base)%nat ->
let b := nth_default 0 base in
let r := (b i * b j) / b (i+j)%nat in
b i * b j = r * b (i+j)%nat
}.
Section BaseSystem.
Context (base : list Z).
(** [BaseSystem] implements an constrained positional number system.
A wide variety of bases are supported: the base coefficients are not
required to be powers of 2, and it is NOT necessarily the case that
$b_{i+j} = b_i b_j$. Implementations of addition and multiplication are
provided, with focus on near-optimal multiplication performance on
non-trivial but small operands: maybe 10 32-bit integers or so. This
module does not handle carries automatically: if no restrictions are put
on the use of a [BaseSystem], each digit is unbounded. This has nothing
to do with modular arithmetic either.
*)
Definition digits : Type := list Z.
Definition accumulate p acc := fst p * snd p + acc.
Definition decode' bs u := fold_right accumulate 0 (combine u bs).
Definition decode := decode' base.
Definition mul_each u := map (Z.mul u).
End BaseSystem.
|
