blob: f75f179e8d76d377fd6b98bfaf61cc78dc46b62b (
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
|
Require Import Crypto.BaseSystem.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.ModularArithmetic.ModularBaseSystem.
Require Import Crypto.Algebra.
Require Import Crypto.Util.Relations.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.Tactics.
Require Import Crypto.SpecificGen.GF41417_32.
Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
Definition edwards_extended_add_coordinates td P Q :=
Eval cbv iota beta delta [
Extended.add_coordinates
add sub mul
] in
(@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
Definition edwards_extended_carry_add_coordinates td P Q :=
Eval cbv iota beta delta [
Extended.add_coordinates
carry_add carry_sub mul
] in
(@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
Print edwards_extended_add_coordinates.
Create HintDb edwards_extended_add_coordinates_correct discriminated.
Section noncarry.
Local Existing Instance field41417_32.
Hint Rewrite
(Ring.homomorphism_mul(is_homomorphism:=homomorphism_F41417_32_decode))
(Ring.homomorphism_add(H1 :=homomorphism_F41417_32_decode))
(Ring.homomorphism_sub(H1 :=homomorphism_F41417_32_decode))
: edwards_extended_add_coordinates_correct.
Lemma edwards_extended_add_coordinates_correct td P Q :
Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
= (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
Proof.
change (edwards_extended_add_coordinates td P Q)
with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
destruct_head' prod.
simpl.
rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
reflexivity.
Qed.
End noncarry.
Section carry.
Local Existing Instance carry_field41417_32.
Hint Rewrite
(Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F41417_32_decode))
(Ring.homomorphism_add(H1 :=homomorphism_carry_F41417_32_decode))
(Ring.homomorphism_sub(H1 :=homomorphism_carry_F41417_32_decode))
: edwards_extended_add_coordinates_correct.
Lemma edwards_extended_carry_add_coordinates_correct td P Q :
Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
= (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
Proof.
change (edwards_extended_carry_add_coordinates td P Q)
with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
destruct_head' prod.
simpl.
rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
reflexivity.
Qed.
End carry.
Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
Tuple.fieldwise
(n:=4) eq
(edwards_extended_carry_add_coordinates td P Q)
(edwards_extended_add_coordinates td P Q).
Proof.
pose proof (edwards_extended_carry_add_coordinates_correct td P Q) as H0.
pose proof (edwards_extended_add_coordinates_correct td P Q) as H1.
rewrite <- H0 in H1; clear H0.
assert (Tuple.fieldwise
(fun x y => x = y)
(Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q))
(Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)))
by (rewrite H1; reflexivity).
clear H1.
destruct (edwards_extended_carry_add_coordinates td P Q), (edwards_extended_add_coordinates td P Q).
destruct_head' prod; simpl; unfold eq; trivial.
Qed.
|
