blob: e539eaa8d6d4a4008337979ae778a853e0d800f7 (
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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
Require Import Crypto.ModularArithmetic.ModularBaseSystem.
Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
Require Import Coq.Lists.List Crypto.Util.ListUtil.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface.
Require Import Crypto.Tactics.VerdiTactics.
Require Import Crypto.BaseSystem.
Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.Notations.
Require Import Crypto.Algebra.
Import ListNotations.
Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
Local Open Scope Z.
Local Infix "<<" := Z.shiftr.
Local Infix "&" := Z.land.
(* BEGIN PseudoMersenneBaseParams instance construction. *)
Definition modulus : Z := 2^130 - 5.
Lemma prime_modulus : prime modulus. Admitted.
Definition int_width := 32%Z.
Instance params1305 : PseudoMersenneBaseParams modulus.
construct_params prime_modulus 5%nat 130.
Defined.
Definition mul2modulus := Eval compute in (construct_mul2modulus params1305).
Instance subCoeff : SubtractionCoefficient modulus params1305.
apply Build_SubtractionCoefficient with (coeff := mul2modulus).
cbv; auto.
cbv [ModularBaseSystem.decode].
apply ZToField_eqmod.
cbv; reflexivity.
Defined.
Definition freezePreconditions1305 : freezePreconditions params1305 int_width.
Proof.
constructor; compute_preconditions.
Defined.
(* END PseudoMersenneBaseParams instance construction. *)
(* Precompute k and c *)
Definition k_ := Eval compute in k.
Definition c_ := Eval compute in c.
Definition k_subst : k = k_ := eq_refl k_.
Definition c_subst : c = c_ := eq_refl c_.
Definition fe1305 : Type := Eval cbv in fe.
Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In phi.
Definition add_formula (f g:fe1305) : { fg | phi fg = @ModularArithmetic.add modulus (phi f) (phi g) }.
Proof.
cbv [fe1305] in *.
repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
eexists.
rewrite <-add_phi.
cbv.
apply f_equal.
reflexivity.
Qed.
Definition add f g := proj1_sig (add_formula f g).
Definition sub_formula (f g:fe1305) : { fg | phi fg = @ModularArithmetic.sub modulus (phi f) (phi g) }.
Proof.
cbv [fe1305] in *.
repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
eexists.
rewrite <-sub_phi.
cbv.
apply f_equal.
reflexivity.
Qed.
Definition sub f g := proj1_sig (sub_formula f g).
Definition mul_formula (f g:fe1305) : { fg | phi fg = @ModularArithmetic.mul modulus (phi f) (phi g) }.
Proof.
cbv [fe1305] in *.
repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
eexists.
rewrite <-(mul_phi (c_ := c_) (k_ := k_)) by auto using k_subst,c_subst.
cbv.
apply f_equal.
autorewrite with zsimplify.
repeat match goal with |- appcontext[?a * 1] => rewrite (Z.mul_1_r a) end.
reflexivity.
Qed.
Definition mul f g := proj1_sig (mul_formula f g).
(*
Local Transparent Let_In.
Eval cbv iota beta delta [proj1_sig mul Let_In] in (fun f0 f1 f2 f3 f4 g0 g1 g2 g3 g4 => proj1_sig (mul (f4,f3,f2,f1,f0) (g4,g3,g2,g1,g0))).
*)
(* TODO: This file should eventually contain the following operations:
toBytes
fromBytes
inv
opp
sub
zero
one
eq
*)
|
