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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
Require Import Crypto.BaseSystem.
Require Import Crypto.ModularArithmetic.ModularBaseSystem.
Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
Require Import Crypto.BaseSystemProofs.
Require Import Crypto.Util.Tuple Crypto.Util.CaseUtil.
Require Import ZArith.
Require Import Crypto.Algebra.
Import Group.
Import PseudoMersenneBaseParams PseudoMersenneBaseParamProofs.
Generalizable All Variables.
Section s.
Context `{prm:PseudoMersenneBaseParams m} {sc : SubtractionCoefficient m prm}.
Context {k_ c_} (pfk : k = k_) (pfc:c = c_).
Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
Definition fe := tuple Z (length base).
Definition mul (x y:fe) : fe :=
carry_mul_opt_cps k_ c_ (from_list_default 0%Z (length base))
(to_list _ x) (to_list _ y).
Definition add : fe -> fe -> fe.
refine (on_tuple2 add_opt _).
abstract (intros; rewrite add_opt_correct, add_length_exact; case_max; omega).
Defined.
Definition sub : fe -> fe -> fe.
refine (on_tuple2 sub_opt _).
abstract (intros; rewrite sub_opt_correct; apply length_sub; rewrite ?coeff_length; auto).
Defined.
Arguments to_list {_ _} _.
Definition phi (a : fe) : ModularArithmetic.F m := decode (to_list a).
Definition phi_inv (a : ModularArithmetic.F m) : fe :=
from_list_default 0%Z _ (encode a).
Lemma phi_inv_spec : forall a, phi (phi_inv a) = a.
Proof.
intros; cbv [phi_inv phi].
erewrite from_list_default_eq.
rewrite to_list_from_list.
apply ModularBaseSystemProofs.encode_rep.
Grab Existential Variables.
apply ModularBaseSystemProofs.encode_rep.
Qed.
Definition eq (x y : fe) : Prop := phi x = phi y.
Import Morphisms.
Global Instance eq_Equivalence : Equivalence eq.
Proof.
split; cbv [eq]; repeat intro; congruence.
Qed.
Lemma phi_inv_spec_reverse : forall a, eq (phi_inv (phi a)) a.
Proof.
intros. unfold eq. rewrite phi_inv_spec; reflexivity.
Qed.
Definition zero : fe := phi_inv (ModularArithmetic.ZToField 0).
Definition opp (x : fe) : fe := phi_inv (ModularArithmetic.opp (phi x)).
Definition one : fe := phi_inv (ModularArithmetic.ZToField 1).
Definition inv (x : fe) : fe := phi_inv (ModularArithmetic.inv (phi x)).
Definition div (x y : fe) : fe := phi_inv (ModularArithmetic.div (phi x) (phi y)).
Lemma add_correct : forall a b,
to_list (add a b) = BaseSystem.add (to_list a) (to_list b).
Proof.
intros; cbv [add on_tuple2].
rewrite to_list_from_list.
apply add_opt_correct.
Qed.
Lemma add_phi : forall a b : fe,
phi (add a b) = ModularArithmetic.add (phi a) (phi b).
Proof.
intros; cbv [phi].
rewrite add_correct.
apply ModularBaseSystemProofs.add_rep; auto using decode_rep, length_to_list.
Qed.
Lemma sub_correct : forall a b,
to_list (sub a b) = ModularBaseSystem.sub coeff (to_list a) (to_list b).
Proof.
intros; cbv [sub on_tuple2].
rewrite to_list_from_list.
apply sub_opt_correct.
Qed.
Lemma sub_phi : forall a b : fe,
phi (sub a b) = ModularArithmetic.sub (phi a) (phi b).
Proof.
intros; cbv [phi].
rewrite sub_correct.
apply ModularBaseSystemProofs.sub_rep; auto using decode_rep, length_to_list,
coeff_length, coeff_mod.
Qed.
Lemma mul_correct : forall a b,
to_list (mul a b) = carry_mul (to_list a) (to_list b).
Proof.
intros; cbv [mul].
rewrite carry_mul_opt_cps_correct by assumption.
erewrite from_list_default_eq.
apply to_list_from_list.
Grab Existential Variables.
apply carry_mul_length; apply length_to_list.
Qed.
Lemma mul_phi : forall a b : fe,
phi (mul a b) = ModularArithmetic.mul (phi a) (phi b).
Proof.
intros; cbv beta delta [phi].
rewrite mul_correct.
apply carry_mul_rep; auto using decode_rep, length_to_list.
Qed.
Lemma modular_base_system_field : @field fe eq zero one opp add sub mul inv div.
Proof.
eapply (Field.isomorphism_to_subfield_field (phi := phi) (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))).
Grab Existential Variables.
+ intros; apply phi_inv_spec.
+ intros; apply phi_inv_spec.
+ intros; apply phi_inv_spec.
+ intros; apply phi_inv_spec.
+ intros; apply mul_phi.
+ intros; apply sub_phi.
+ intros; apply add_phi.
+ intros; apply phi_inv_spec.
+ cbv [eq zero one]. rewrite !phi_inv_spec. intro A.
eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). congruence.
+ trivial.
+ repeat intro. cbv [div]. congruence.
+ repeat intro. cbv [inv]. congruence.
+ repeat intro. cbv [eq]. rewrite !mul_phi. congruence.
+ repeat intro. cbv [eq]. rewrite !sub_phi. congruence.
+ repeat intro. cbv [eq]. rewrite !add_phi. congruence.
+ repeat intro. cbv [opp]. congruence.
+ cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
Qed.
End s.
|
