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
|
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.ModularArithmetic.ModularBaseSystem.
Require Import Crypto.SpecificGen.GF25519_32Bounded.
Require Import Crypto.SpecificGen.GF25519_32ExtendedAddCoordinates.
Require Import Crypto.SpecificGen.GF25519_32BoundedAddCoordinates.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Tactics.
Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23
: Tuple.fieldwise
(n:=4) GF25519_32BoundedCommon.eq
(@GF25519_32BoundedAddCoordinates.add_coordinates
twice_d P10 P11 P12 P13 P20 P21 P22 P23)
(@ExtendedCoordinates.Extended.add_coordinates
GF25519_32BoundedCommon.fe25519_32
GF25519_32Bounded.add GF25519_32Bounded.sub GF25519_32Bounded.mul twice_d
(P10, P11, P12, P13) (P20, P21, P22, P23)).
Proof.
unfold GF25519_32BoundedCommon.eq.
apply -> (fieldwise_map_iff (n:=4) eq GF25519_32BoundedCommon.proj1_fe25519_32 GF25519_32BoundedCommon.proj1_fe25519_32).
rewrite add_coordinates_correct.
cbv [AddCoordinates.add_coordinates].
setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry.
unfold edwards_extended_carry_add_coordinates.
match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end.
apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF25519_32BoundedCommon.proj1_fe25519_32).
apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero;
intros;
repeat match goal with
| [ |- context[add _ _] ]
=> rewrite add_correct
| [ |- context[sub _ _] ]
=> rewrite sub_correct
| [ |- context[mul _ _] ]
=> rewrite mul_correct
| _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in *
| [ |- and _ _ ] => split
| [ |- ?x = ?x ] => reflexivity
| _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct
| _ => congruence
end.
Qed.
Definition add_coordinates' twice_d P1 P2
:= let '(P10, P11, P12, P13) := P1 in
let '(P20, P21, P22, P23) := P2 in
@GF25519_32BoundedAddCoordinates.add_coordinates
twice_d P10 P11 P12 P13 P20 P21 P22 P23.
Definition add_coordinates twice_d P1 P2
:= Eval cbv beta iota delta [GF25519_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in
let '(P10, P11, P12, P13) := P1 in
let '(P20, P21, P22, P23) := P2 in
@GF25519_32BoundedAddCoordinates.add_coordinates
twice_d P10 P11 P12 P13 P20 P21 P22 P23.
Lemma add_coordinates_correct_full twice_d P1 P2
: Tuple.fieldwise
GF25519_32BoundedCommon.eq
(add_coordinates twice_d P1 P2)
(@ExtendedCoordinates.Extended.add_coordinates
GF25519_32BoundedCommon.fe25519_32
GF25519_32Bounded.add GF25519_32Bounded.sub GF25519_32Bounded.mul twice_d P1 P2).
Proof.
destruct_head' prod.
rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity.
Qed.
|
