blob: 4fd881e1e6477ae55f309d1920126c4c480c6fed (
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.BaseSystem.
Require Import Crypto.BaseSystemProofs.
Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
Require Import Crypto.ModularArithmetic.Pow2Base.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
Require Import Crypto.ModularArithmetic.ModularBaseSystemList.
Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs.
Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Notations.
Require Import Crypto.Tactics.VerdiTactics.
Local Open Scope Z_scope.
Section ModularBaseSystem.
Context `{prm :PseudoMersenneBaseParams}.
Local Notation base := (base_from_limb_widths limb_widths).
Local Notation digits := (tuple Z (length limb_widths)).
Local Arguments to_list {_ _} _.
Local Arguments from_list {_ _} _ _.
Local Arguments length_to_list {_ _ _}.
Local Notation "[[ u ]]" := (to_list u).
Definition decode (us : digits) : F modulus := decode [[us]].
Definition encode (x : F modulus) : digits := from_list (encode x) length_encode.
Definition add (us vs : digits) : digits := from_list (add [[us]] [[vs]])
(add_same_length _ _ _ length_to_list length_to_list).
Definition mul (us vs : digits) : digits := from_list (mul [[us]] [[vs]])
(length_mul length_to_list length_to_list).
Definition sub (modulus_multiple us vs : digits) : digits :=
from_list (sub [[modulus_multiple]] [[us]] [[vs]])
(length_sub length_to_list length_to_list length_to_list).
Definition zero : digits := encode (ZToField 0).
Definition one : digits := encode (ZToField 1).
(* Placeholder *)
Definition opp (x : digits) : digits := encode (ModularArithmetic.opp (decode x)).
(* Placeholder *)
Definition inv (x : digits) : digits := encode (ModularArithmetic.inv (decode x)).
(* Placeholder *)
Definition div (x y : digits) : digits := encode (ModularArithmetic.div (decode x) (decode y)).
Definition rep (us : digits) (x : F modulus) := decode us = x.
Local Notation "u ~= x" := (rep u x).
Local Hint Unfold rep.
Definition carry_full (us : digits) : digits := from_list (carry_full [[us]])
(length_carry_full length_to_list).
Definition carry_mul (us vs : digits) : digits := carry_full (mul us vs).
Definition freeze (us : digits) : digits :=
let us' := carry_full (carry_full (carry_full us)) in
from_list (conditional_subtract_modulus [[us']] (ge_modulus [[us']]))
(length_conditional_subtract_modulus length_to_list).
Definition eq (x y : digits) : Prop := decode x = decode y.
Import Morphisms.
Global Instance eq_Equivalence : Equivalence eq.
Proof.
split; cbv [eq]; repeat intro; congruence.
Qed.
End ModularBaseSystem.
|
