blob: f5bedd6443872c1f8037800ebc22564ee594da9c (
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
|
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
Require Import Crypto.ModularArithmetic.ModularBaseSystem.
Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Algebra. Import Field.
Require Import Crypto.Util.Tuple Crypto.Util.Notations.
Local Open Scope Z_scope.
Section ModularBaseSystemField.
Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}
(k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_).
Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
Local Notation digits := (tuple Z (length limb_widths)).
Lemma add_decode : forall a b : digits,
decode (add_opt a b) = (decode a + decode b)%F.
Proof.
intros; rewrite add_opt_correct by assumption.
apply add_rep; apply decode_rep.
Qed.
Lemma sub_decode : forall a b : digits,
decode (sub_opt a b) = (decode a - decode b)%F.
Proof.
intros; rewrite sub_opt_correct by assumption.
apply sub_rep; auto using coeff_mod, decode_rep.
Qed.
Lemma mul_decode : forall a b : digits,
decode (carry_mul_opt k_ c_ a b) = (decode a * decode b)%F.
Proof.
intros; rewrite carry_mul_opt_correct by assumption.
apply carry_mul_rep; apply decode_rep.
Qed.
Lemma zero_neq_one : eq zero one -> False.
Proof.
cbv [eq zero one]. erewrite !encode_rep. intro A.
eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)).
congruence.
Qed.
Lemma modular_base_system_field :
@field digits eq zero one opp add_opt sub_opt (carry_mul_opt k_ c_) inv div.
Proof.
eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))).
Grab Existential Variables.
+ intros; eapply encode_rep.
+ intros; eapply encode_rep.
+ intros; eapply encode_rep.
+ intros; eapply encode_rep.
+ intros; eapply mul_decode.
+ intros; eapply sub_decode.
+ intros; eapply add_decode.
+ intros; eapply encode_rep.
+ cbv [eq zero one]. erewrite !encode_rep. 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]. erewrite !mul_decode. congruence.
+ repeat intro. cbv [eq]. erewrite !sub_decode. congruence.
+ repeat intro. cbv [eq]. erewrite !add_decode. congruence.
+ repeat intro. cbv [opp]. congruence.
+ cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
Qed.
End ModularBaseSystemField.
|
