12 files changed, 138 insertions, 0 deletions

diff --git a/test/data/formulas/add-sunec-v21 b/test/data/formulas/add-sunec-v21
new file mode 100644
index 0000000..2d6f395
--- /dev/null
+++ b/test/data/formulas/add-sunec-v21
@@ -0,0 +1,3 @@
+source Java JDK 21 https://github.com/openjdk/jdk/blob/jdk-21-ga/src/jdk.crypto.ec/share/classes/sun/security/ec/ECOperations.java#L287
+coords projective-3
+assume Z2 = 1
diff --git a/test/data/formulas/add-sunec-v21-ed25519 b/test/data/formulas/add-sunec-v21-ed25519
new file mode 100644
index 0000000..078aa39
--- /dev/null
+++ b/test/data/formulas/add-sunec-v21-ed25519
@@ -0,0 +1,2 @@
+source Java JDK 21 https://github.com/openjdk/jdk/blob/jdk-21-ga/src/jdk.crypto.ec/share/classes/sun/security/ec/ed/Ed25519Operations.java#L147
+coords extended
diff --git a/test/data/formulas/add-sunec-v21-ed25519.op3 b/test/data/formulas/add-sunec-v21-ed25519.op3
new file mode 100644
index 0000000..2498a1f
--- /dev/null
+++ b/test/data/formulas/add-sunec-v21-ed25519.op3
@@ -0,0 +1,19 @@
+t1 = Y2 - X2
+t2 = Y1 - X1
+t2 = t2 * t1
+t1 = Y2 + X2
+t3 = Y1 + X1
+t3 = t3 * t1
+X = t3 - t2
+t3 = t3 + t2
+t2 = d + d
+t2 = t2 * T1
+t2 = t2 * T2
+t1 = Z1 * Z2
+t1 = t1 * 2
+Y = t1 + t2
+Z = t1 - t2
+T3 = X1 * t3
+X3 = X * Z
+Z3 = Z * Y
+Y3 = Y * t3
diff --git a/test/data/formulas/add-sunec-v21.op3 b/test/data/formulas/add-sunec-v21.op3
new file mode 100644
index 0000000..d682b16
--- /dev/null
+++ b/test/data/formulas/add-sunec-v21.op3
@@ -0,0 +1,32 @@
+t0 = X1 * X2
+t1 = Y1 * Y2
+t3 = X2 + Y2
+t4 = X1 + Y1
+t3 = t3 * t4
+t4 = t0 + t1
+t3 = t3 - t4
+t4 = Y2 * Z1
+t4 = t4 + Y1
+Y = X2 * Z1
+Y = Y + X1
+Z = Z1 * b
+X = Y - Z
+X = X * 3
+Z = t1 - X
+X = X + t1
+Y = Y * b
+t2 = Z1 * 3
+Y = Y - t2
+Y = Y - t0
+Y = Y * 3
+t0 = t0 * 3
+t0 = t0 - t2
+t1 = t4 * Y
+t2 = t0 * Y
+Y = X * Z
+Y3 = Y + t2
+X = X * t3
+X3 = X - t1
+Z = Z * t4
+t3 = t3 * t0
+Z3 = Z + t3
diff --git a/test/data/formulas/dbl-hacl-x25519 b/test/data/formulas/dbl-hacl-x25519
new file mode 100644
index 0000000..b2a1d00
--- /dev/null
+++ b/test/data/formulas/dbl-hacl-x25519
@@ -0,0 +1,4 @@
+source HACL* https://github.com/hacl-star/hacl-star/blob/v0.3.0/specs/Spec.Curve25519.fst#L80C9-L80C9
+parameter am24
+assume am24 = (a-2)/4
+coords xz
diff --git a/test/data/formulas/dbl-hacl-x25519.op3 b/test/data/formulas/dbl-hacl-x25519.op3
new file mode 100644
index 0000000..8b315db
--- /dev/null
+++ b/test/data/formulas/dbl-hacl-x25519.op3
@@ -0,0 +1,9 @@
+a = X1 + Z1
+b = X1 - Z1
+aa = a^2
+bb = b^2
+e = aa - bb
+e121665 = e * am24
+aa_e121665 = e121665 + aa
+X3 = aa * bb
+Z3 = e * aa_e121665
diff --git a/test/data/formulas/dbl-sunec-v21 b/test/data/formulas/dbl-sunec-v21
new file mode 100644
index 0000000..663793a
--- /dev/null
+++ b/test/data/formulas/dbl-sunec-v21
@@ -0,0 +1,2 @@
+source Java JDK 21 https://github.com/openjdk/jdk/blob/jdk-21-ga/src/jdk.crypto.ec/share/classes/sun/security/ec/ECOperations.java#L220
+coords projective-3
diff --git a/test/data/formulas/dbl-sunec-v21-ed25519 b/test/data/formulas/dbl-sunec-v21-ed25519
new file mode 100644
index 0000000..6814542
--- /dev/null
+++ b/test/data/formulas/dbl-sunec-v21-ed25519
@@ -0,0 +1,2 @@
+source Java JDK 21 https://github.com/openjdk/jdk/blob/jdk-21-ga/src/jdk.crypto.ec/share/classes/sun/security/ec/ed/Ed25519Operations.java#L184
+coords extended
diff --git a/test/data/formulas/dbl-sunec-v21-ed25519.op3 b/test/data/formulas/dbl-sunec-v21-ed25519.op3
new file mode 100644
index 0000000..9f25c7e
--- /dev/null
+++ b/test/data/formulas/dbl-sunec-v21-ed25519.op3
@@ -0,0 +1,14 @@
+t1 = X1 + Y1
+t1 = t1^2
+X = X1^2
+Y = Y1^2
+t2 = X + Y
+Z = Z1^2
+Z = Z * 2
+T = t2 - t1
+t1 = X - Y
+Z = Z + t1
+X3 = T * Z
+Y3 = t1 * t2
+T3 = T * t2
+Z3 = Z * t1
diff --git a/test/data/formulas/dbl-sunec-v21.op3 b/test/data/formulas/dbl-sunec-v21.op3
new file mode 100644
index 0000000..7480ec6
--- /dev/null
+++ b/test/data/formulas/dbl-sunec-v21.op3
@@ -0,0 +1,29 @@
+t0 = X1^2
+t1 = Y1^2
+t2 = Z1^2
+t3 = X1 * Y1
+t4 = Y1 * Z1
+t3 = t3 + t3
+Z = Z1 * X1
+Z = Z * 2
+Y = t2 * b
+Y = Y - Z
+Y = 3 * Y
+X = t1 - Y
+Y = Y + t1
+Y = Y * X
+X = X * t3
+t2 = t2 * 3
+Z = Z * b
+Z = Z - t2
+Z = Z - t0
+Z = Z * 3
+t0 = t0 * 3
+t0 = t0 - t2
+t0 = t0 * Z
+Y3 = Y + t0
+t4 = t4 + t4
+Z = Z * t4
+X3 = X - Z
+Z = t4 * t1
+Z3 = Z * 4
diff --git a/test/data/formulas/ladd-rfc7748 b/test/data/formulas/ladd-rfc7748
new file mode 100644
index 0000000..70c69e3
--- /dev/null
+++ b/test/data/formulas/ladd-rfc7748
@@ -0,0 +1,4 @@
+source RFC 7748
+parameter am24
+assume am24 = (a-2)/4
+coords xz
diff --git a/test/data/formulas/ladd-rfc7748.op3 b/test/data/formulas/ladd-rfc7748.op3
new file mode 100644
index 0000000..8ea3d94
--- /dev/null
+++ b/test/data/formulas/ladd-rfc7748.op3
@@ -0,0 +1,18 @@
+A = X2 + Z2
+AA = A^2
+B = X2 - Z2
+BB = B^2
+E = AA - BB
+C = X3 + Z3
+D = X3 - Z3
+DA = D * A
+CB = C * B
+DApCB = DA + CB
+X5 = DApCB^2
+DAmCB = DA - CB
+DAmCB2 = DAmCB^2
+Z5 = X1 * DAmCB2
+X4 = AA * BB
+E24 = E * am24
+AAE = AA + E24
+Z4 = E * AAE