Add more formulas to lib db.

10 files changed, 118 insertions, 0 deletions

diff --git a/test/data/formulas/add-bearssl-v06 b/test/data/formulas/add-bearssl-v06
new file mode 100644
index 0000000..b7ac8cd
--- /dev/null
+++ b/test/data/formulas/add-bearssl-v06
@@ -0,0 +1,2 @@
+source BearSSL v0.6 https://bearssl.org/gitweb/?p=BearSSL;a=blob;f=src/ec/ec_prime_i15.c;h=f86dbe6ff0dbc036af470e369048c4ae02d33337;hb=HEAD#l320
+coords jacobian
diff --git a/test/data/formulas/add-bearssl-v06.op3 b/test/data/formulas/add-bearssl-v06.op3
new file mode 100644
index 0000000..9b3d3a9
--- /dev/null
+++ b/test/data/formulas/add-bearssl-v06.op3
@@ -0,0 +1,23 @@
+t3 = Z2^2
+t1 = X1 * t3
+t4 = Z2 * t3
+t3 = Y1 * t4
+t4 = Z1^2
+t2 = X2 * t4
+t5 = Z1 * t4
+t4 = Y2 * t5
+t2 = t2 - t1
+t4 = t4 - t3
+t7 = t2^2
+t6 = t1 * t7
+t5 = t7 * t2
+X = t4^2
+X = X - t5
+X = X - t6
+X3 = X - t6
+t6 = t6 - X3
+Y = t4 * t6
+t1 = t5 * t3
+Y3 = Y - t1
+t1 = Z1 * Z2
+Z3 = t1 * t2
diff --git a/test/data/formulas/add-libgcrypt-v1102 b/test/data/formulas/add-libgcrypt-v1102
new file mode 100644
index 0000000..3d542ed
--- /dev/null
+++ b/test/data/formulas/add-libgcrypt-v1102
@@ -0,0 +1,4 @@
+source libgcrypt v1.10.2 https://git.gnupg.org/cgi-bin/gitweb.cgi?p=libgcrypt.git;a=blob;f=mpi/ec.c;h=c24921eea8bea8363a503d6d6071b116c176d8e5;hb=1c5cbacf3d88dded5063e959ee68678ff7d0fa56#l1406
+parameter half
+assume half = 1/2
+coords jacobian
diff --git a/test/data/formulas/add-libgcrypt-v1102.op3 b/test/data/formulas/add-libgcrypt-v1102.op3
new file mode 100644
index 0000000..d41d7b8
--- /dev/null
+++ b/test/data/formulas/add-libgcrypt-v1102.op3
@@ -0,0 +1,25 @@
+l1 = Z2^2
+l1 = l1 * X1
+l2 = Z1^2
+l2 = l2 * X2
+l3 = l1 - l2
+l4 = Z2^3
+l4 = l4 * Y1
+l5 = Z1^3
+l5 = l5 * Y2
+l6 = l4 - l5
+l7 = l1 + l2
+l8 = l4 + l5
+Z3 = Z1 * Z2
+Z3 = Z3 * l3
+t1 = l6^2
+t2 = l3^2
+t2 = t2 * l7
+X3 = t1 - t2
+t1 = X3 * 2
+l9 = t2 - t1
+l9 = l9 * l6
+t1 = l3^3
+t1 = t1 * l8
+Y3 = l9 - t1
+Y3 = Y3 * half
diff --git a/test/data/formulas/dbl-bearssl-v06 b/test/data/formulas/dbl-bearssl-v06
new file mode 100644
index 0000000..9479888
--- /dev/null
+++ b/test/data/formulas/dbl-bearssl-v06
@@ -0,0 +1,2 @@
+source BearSSL v0.6 https://bearssl.org/gitweb/?p=BearSSL;a=blob;f=src/ec/ec_prime_i15.c;h=f86dbe6ff0dbc036af470e369048c4ae02d33337;hb=HEAD#l214
+coords jacobian
diff --git a/test/data/formulas/dbl-bearssl-v06.op3 b/test/data/formulas/dbl-bearssl-v06.op3
new file mode 100644
index 0000000..c89c340
--- /dev/null
+++ b/test/data/formulas/dbl-bearssl-v06.op3
@@ -0,0 +1,20 @@
+t1 = Z1^2
+t2 = X1 - t1
+t1 = t1 + X1
+t3 = t1 * t2
+t1 = t3 + t3
+t1 = t1 + t3
+t3 = Y1^2
+t3 = t3 + t3
+t2 = X1 * t3
+t2 = t2 + t2
+X = t1^2
+X = X - t2
+X3 = X - t2
+t4 = Y1 * Z1
+Z3 = t4 + t4
+t2 = t2 - X3
+Y = t1 * t2
+t4 = t3^2
+Y = Y - t4
+Y3 = Y - t4
diff --git a/test/data/formulas/dbl-libgcrypt-v1102 b/test/data/formulas/dbl-libgcrypt-v1102
new file mode 100644
index 0000000..fdb3878
--- /dev/null
+++ b/test/data/formulas/dbl-libgcrypt-v1102
@@ -0,0 +1,2 @@
+source libgcrypt v1.10.2 https://git.gnupg.org/cgi-bin/gitweb.cgi?p=libgcrypt.git;a=blob;f=mpi/ec.c;h=c24921eea8bea8363a503d6d6071b116c176d8e5;hb=1c5cbacf3d88dded5063e959ee68678ff7d0fa56#l1219
+coords jacobian
diff --git a/test/data/formulas/dbl-libgcrypt-v1102.op3 b/test/data/formulas/dbl-libgcrypt-v1102.op3
new file mode 100644
index 0000000..3ae81dd
--- /dev/null
+++ b/test/data/formulas/dbl-libgcrypt-v1102.op3
@@ -0,0 +1,18 @@
+l1 = X1^2
+l1 = l1 * 3
+t1 = Z1^4
+t1 = t1 * a
+l1 = l1 + t1
+Z3 = Y1 * Z1
+Z3 = Z3 * 2
+t2 = Y1^2
+l2 = t2 * X1
+l2 = l2 * 4
+X3 = l1^2
+t1 = l2 * 2
+X3 = X3 - t1
+t2 = t2^2
+l3 = t2 * 8
+Y3 = l2 - X3
+Y3 = Y3 * l1
+Y3 = Y3 - l3
diff --git a/test/data/formulas/ladd-go-1214 b/test/data/formulas/ladd-go-1214
new file mode 100644
index 0000000..6756685
--- /dev/null
+++ b/test/data/formulas/ladd-go-1214
@@ -0,0 +1,4 @@
+source go crypto/ecdh/x25519 https://github.com/golang/go/blob/go1.21.4/src/crypto/ecdh/x25519.go#L86
+parameter a24
+assume a24 = (a+2)/4
+coords xz
diff --git a/test/data/formulas/ladd-go-1214.op3 b/test/data/formulas/ladd-go-1214.op3
new file mode 100644
index 0000000..3bf8e7d
--- /dev/null
+++ b/test/data/formulas/ladd-go-1214.op3
@@ -0,0 +1,18 @@
+t0 = X3-Z3
+t1 = X2-Z2
+X2 = X2+Z2
+Z2 = X3+Z3
+Z3 = t0*X2
+Z2 = Z2*t1
+t0 = t1^2
+t1 = X2^2
+X3 = Z3+Z2
+Z2 = Z3-Z2
+X4 = t1*t0
+t1 = t1-t0
+Z2 = Z2^2
+Z3 = t1 * a24
+X5 = X3^2
+t0 = t0+Z3
+Z5 = X1*Z2
+Z4 = t1*t0