-
Notifications
You must be signed in to change notification settings - Fork 0
/
short_sum_verification.magma
72 lines (64 loc) · 2.96 KB
/
short_sum_verification.magma
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
// Usage: magma -s "short_sum_verification.magma"
R<X1,Y1,Z1, X2,Y2,Z2, a1,a2,a3,a4,a6> := PolynomialRing(Integers(), 11);
xx := X1*X2;
yy := Y1*Y2;
zz := Z1*Z2;
xyp := X1*Y2 + X2*Y1;
xym := X1*Y2 - X2*Y1;
xzp := X1*Z2 + X2*Z1;
xzm := X1*Z2 - X2*Z1;
yzp := Y1*Z2 + Y2*Z1;
yzm := Y1*Z2 - Y2*Z1;
// Second addition law [Bosma - Lenstra, 1995]
X3 := yy*xyp + a1*(2*X1*Y2 + X2*Y1)*(X2*Y1) + a1^2*(X1*X2^2*Y1)
- a2*xx*xyp - a1*a2*xx^2 + a3*(X2*Y1)*(Y1*Z2 + 2*Y2*Z1)
+ a1*a3*xx*yzm - a1*a3*xyp*xzm
- a4*xx*yzp - a4*xyp*xzp
- a1^2*a3*(X1^2*X2*Z2) - a1*a4*xx*(2*X1*Z2 + X2*Z1)
- a2*a3*X1*X2^2*Z1 - a3^2*X1*Z2*(2*Y2*Z1 + Y1*Z2)
- 3*a6*xyp*zz
- 3*a6*xzp*yzp - a1*a3^2*X1*Z2*(X1*Z2 + 2*X2*Z1)
- 3*a1*a6*X1*Z2*(X1*Z2 + 2*X2*Z1) + a3*a4*(-2*X1*Z2 - X2*Z1)*(X2*Z1)
- (a1^2*a6 - a1*a3*a4 + a2*a3^2 + 4*a2*a6 - a4^2)*yzp*zz
- (a1^3*a6 - a1^2*a3*a4 + a1*a2*a3^2 + 4*a1*a2*a6 - a1*a4^2)*(X1*Z1*Z2^2)
- a3^3*xzp*zz - 3*a3*a6*(xzp + X2*Z1)*zz
- (a1^2*a3*a6 - a1*a3^2*a4 + a2*a3^3 + 4*a2*a3*a6 - a3*a4^2)*zz^2;
Y3 := yy^2 + a1*X2*Y1^2*Y2 + (a1*a2 - 3*a3)*(X1*X2^2*Y1)
+ a3*(Y1^2*Y2*Z2) - (a2^2 - 3*a4)*xx^2
+ (a1*a4 - a2*a3)*(xzp + X1*Z2)*(X2*Y1)
+ (a1^2*a4 - 2*a1*a2*a3 + 3*a3^2)*(X1^2*X2*Z2)
- (a2*a4 - 9*a6)*xx*xzp
+ (3*a1*a6 - a3*a4)*(xzp + X2*Z1)*(Y1*Z2)
+ (3*a1^2*a6 - 2*a1*a3*a4 + a2*a3^2 + 3*a2*a6 - a4^2)*(X1*Z2)*(xzp + X2*Z1)
- (3*a2*a6 - a4^2)*(-2*X1*Z2 - X2*Z1)*X2*Z1
+ (a1^3*a6 - a1^2*a3*a4 + a1*a2*a3^2 - a1*a4^2 + 4*a1*a2*a6 - a3^3 - 3*a3*a6)*(Y1*Z1*Z2^2)
+ (a1^4*a6 - a1^3*a3*a4 + 5*a1^2*a2*a6 + a1^2*a2*a3^2 - a1*a2*a3*a4 - a1*a3^3 - 3*a1*a3*a6
- a1^2*a4^2 + a2^2*a3^2 - a2*a4^2 + 4*a2^2*a6 - a3^2*a4 - 3*a4*a6)*(X1*Z1*Z2^2)
+ (a1^2*a2*a6 - a1*a2*a3*a4 + 3*a1*a3*a6 + a2^2*a3^2 - a2*a4^2
+ 4*a2^2*a6 - 2*a3^2*a4 - 3*a4*a6)*(X2*Z1^2*Z2)
+ (a1^3*a3*a6 - a1^2*a3^2*a4 + a1^2*a4*a6 + a1*a2*a3^3
+ 4*a1*a2*a3*a6 - 2*a1*a3*a4^2 + a2*a3^2*a4
+ 4*a2*a4*a6 - a3^4 - 6*a3^2*a6 - a4^3 - 9*a6^2)*zz^2;
Z3 := 3*xx*xyp + yy*yzp + 3*a1*xx^2
+ a1*(xyp + X1*Y2)*Y1*Z2 + a1^2*X1*Z2*(xyp + X2*Y1)
+ a2*xx*yzp
+ a2*xyp*xzp
+ a1^3*X1^2*X2*Z2 + a1*a2*xx*(2*X1*Z2 + X2*Z1)
+ 3*a3*X1*X2^2*Z1 + a3*Y1*Z2*(yzp + Y2*Z1)
+ 2*a1*a3*X1*Z2*yzp
+ 2*a1*a3*(X2*Y1*zz) + a4*xyp*zz
+ a4*xzp*yzp
+ (a1^2*a3 + a1*a4)*X1*Z2*(xzp + X2*Z1) + a2*a3*X2*Z1*(xzp + X1*Z2)
+ a3^2*Y1*Z1*Z2^2 + (a3^2 + 3*a6)*yzp*zz
+ a1*a3^2*(xzp + X1*Z2)*zz + 3*a1*a6*X1*Z1*Z2^2
+ a3*a4*(X1*Z2 + 2*X2*Z1)*zz + (a3^3 + 3*a3*a6)*zz^2;
// Our short form
g1 := X1*X2*a1 + X2*Z1*a3 + X2*Y1 + X1*Y2;
g2 := X1*Z2*a1 + Z1*Z2*a3 + Y2*Z1 + Y1*Z2;
Q1 := -X1*Z2*a1*a3 - Z1*Z2*a3^2 + X2*Y1*a1 - X1*X2*a2 - X2*Z1*a4 - X1*Z2*a4 - 3*Z1*Z2*a6 + Y1*Y2;
Q2 := -Z1*Z2*a2*a3^2 + Z1*Z2*a1*a3*a4 - Z1*Z2*a1^2*a6 - X1*Z2*a3^2 + Z1*Z2*a4^2 - 4*Z1*Z2*a2*a6 + X2*Y1*a3 - X1*X2*a4 - 3*X2*Z1*a6 - 3*X1*Z2*a6;
Q3 := X1*Z2*a1^2 + Z1*Z2*a1*a3 + Y1*Z2*a1 + X2*Z1*a2 + X1*Z2*a2 + Z1*Z2*a4 + 3*X1*X2;
Q4 := X1*Z2*a1*a3 + Z1*Z2*a3^2 + X1*X2*a2 + Y1*Z2*a3 + X2*Z1*a4 + X1*Z2*a4 + 3*Z1*Z2*a6 + Y1*Y2;
assert X3 eq g1*Q1 + g2*Q2;
assert Z3 eq g1*Q3 + g2*Q4;
assert Y3 eq Q1*Q4 - Q2*Q3;