Add OpenSSL.

6 files changed, 68 insertions, 0 deletions

diff --git a/test/data/formulas/add-openssl-z256 b/test/data/formulas/add-openssl-z256
new file mode 100644
index 0000000..84efc9d
--- /dev/null
+++ b/test/data/formulas/add-openssl-z256
@@ -0,0 +1,2 @@
+source OpenSSL 3.1.4 https://github.com/openssl/openssl/blob/openssl-3.1.4/crypto/ec/ecp_nistz256.c#L312
+coords jacobian-3
diff --git a/test/data/formulas/add-openssl-z256.op3 b/test/data/formulas/add-openssl-z256.op3
new file mode 100644
index 0000000..bc0ccfc
--- /dev/null
+++ b/test/data/formulas/add-openssl-z256.op3
@@ -0,0 +1,23 @@
+Z2sqr = Z2^2
+Z1sqr = Z1^2
+S1 = Z2sqr * Z2
+S2 = Z1sqr * Z1
+S1 = Y1 * S1
+S2 = Y2 * S2
+R = S2 - S1
+U1 = X1 * Z2sqr
+U2 = X2 * Z1sqr
+H = U2 - U1
+Rsqr = R^2
+Z3 = H * Z1
+Hsqr = H^2
+Z3 = H * Z2
+Hcub = Hsqr * H
+U2 = U1 * Hsqr
+Hsqr = 2 * U2
+X3 = Rsqr - Hsqr
+X3 = X3 - Hcub
+Y3 = U2 - X3
+S2 = S1 * Hcub
+Y3 = R * Y3
+Y3 = Y3 - S2
diff --git a/test/data/formulas/add-openssl-z256a b/test/data/formulas/add-openssl-z256a
new file mode 100644
index 0000000..71de9d0
--- /dev/null
+++ b/test/data/formulas/add-openssl-z256a
@@ -0,0 +1,3 @@
+source OpenSSL 3.1.4 https://github.com/openssl/openssl/blob/openssl-3.1.4/crypto/ec/ecp_nistz256.c#L442
+coords jacobian-3
+assume Z2 = 1
diff --git a/test/data/formulas/add-openssl-z256a.op3 b/test/data/formulas/add-openssl-z256a.op3
new file mode 100644
index 0000000..23f90e6
--- /dev/null
+++ b/test/data/formulas/add-openssl-z256a.op3
@@ -0,0 +1,18 @@
+Z1sqr = Z1^2
+U2 = X2 * Z1sqr
+H = U2 - X1
+S2 = Z1sqr * Z1
+Z3 = H * Z1
+S2 = S2 * Y2
+R = S2 - Y1
+Hsqr = H^2
+Rsqr = R^2
+Hcub = Hsqr * H
+U2 = X1 * Hsqr
+Hsqr = 2 * U2
+X3 = Rsqr - Hsqr
+X3 = X3 - Hcub
+H = U2 - X3
+S2 = Y1 * Hcub
+H = H * R
+Y3 = H - S2
diff --git a/test/data/formulas/ladd-openssl-x25519 b/test/data/formulas/ladd-openssl-x25519
new file mode 100644
index 0000000..a40fdc7
--- /dev/null
+++ b/test/data/formulas/ladd-openssl-x25519
@@ -0,0 +1,4 @@
+source OpenSSL 3.1.4 https://github.com/openssl/openssl/blob/openssl-3.1.4/crypto/ec/curve25519.c#L211
+parameter a24
+assume a24 = (a+2)/4
+coords xz
diff --git a/test/data/formulas/ladd-openssl-x25519.op3 b/test/data/formulas/ladd-openssl-x25519.op3
new file mode 100644
index 0000000..f781529
--- /dev/null
+++ b/test/data/formulas/ladd-openssl-x25519.op3
@@ -0,0 +1,18 @@
+tmp0 = X3 - Z3
+tmp1 = X2 - Z2
+X2 = X2 + Z2
+Z2 = X3 + Z3
+Z3 = X2 * tmp0
+Z2 = Z2 * tmp1
+tmp0 = tmp1^2
+tmp1 = X2^2
+X3 = Z3 + Z2
+Z2 = Z3 - Z2
+X4 = tmp1 * tmp0
+tmp1 = tmp1 - tmp0
+Z2 = Z2^2
+Z3 = tmp1 * a24
+X5 = X3^2
+tmp0 = tmp0 + Z3
+Z5 = X1 * Z2
+Z4 = tmp1 * tmp0