blob: c16cc8d388fe996bcb6bb049d85063d30075b917 (
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
40
41
42
43
44
45
46
47
48
49
50
|
Require Import ZArith.
Require Crypto.BaseSystem.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs Crypto.ModularArithmetic.PseudoMersenneBaseParams.
Local Open Scope Z_scope.
Class RepZMod (modulus : Z) := {
T : Type;
encode : F modulus -> T;
decode : T -> F modulus;
rep : T -> F modulus -> Prop;
encode_rep : forall x, rep (encode x) x;
rep_decode : forall u x, rep u x -> decode u = x;
add : T -> T -> T;
add_rep : forall u v x y, rep u x -> rep v y -> rep (add u v) (x+y)%F;
sub : T -> T -> T;
sub_rep : forall u v x y, rep u x -> rep v y -> rep (sub u v) (x-y)%F;
mul : T -> T -> T;
mul_rep : forall u v x y, rep u x -> rep v y -> rep (mul u v) (x*y)%F
}.
Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := {
coeff : BaseSystem.digits;
coeff_length : (length coeff <= length PseudoMersenneBaseParamProofs.base)%nat;
coeff_mod: (BaseSystem.decode PseudoMersenneBaseParamProofs.base coeff) mod m = 0
}.
Instance PseudoMersenneBase m (prm : PseudoMersenneBaseParams m) (sc : SubtractionCoefficient m prm)
: RepZMod m := {
T := list Z;
encode := ModularBaseSystem.encode;
decode := ModularBaseSystem.decode;
rep := ModularBaseSystem.rep;
encode_rep := ModularBaseSystemProofs.encode_rep;
rep_decode := ModularBaseSystemProofs.rep_decode;
add := BaseSystem.add;
add_rep := ModularBaseSystemProofs.add_rep;
sub := ModularBaseSystem.sub coeff coeff_mod;
sub_rep := ModularBaseSystemProofs.sub_rep coeff coeff_mod coeff_length;
mul := ModularBaseSystem.mul;
mul_rep := ModularBaseSystemProofs.mul_rep
}.
|
