8 files changed, 64 insertions, 4 deletions
diff --git a/docs/libraries.rst b/docs/libraries.rst
index b1f7c41..49e1234 100644
--- a/docs/libraries.rst
+++ b/docs/libraries.rst
@@ -154,7 +154,7 @@ Primitives
 
 Supports P-224, P-256, P-384 and P-521.
 Also Curve25519.
-Uses fiat-crypto for the SECP curve field arithmetic.
+Uses fiat-crypto for the SECP curve field arithmetic and x25519.
 
 P-224
 ^^^^^
@@ -235,8 +235,8 @@ KeyGen:
 Derive:
  - Montgomery
  - Ladder via ``X25519 -> x25519_scalar_mult -> x25519_NEON/x25519_scalar_mult_adx/x25519_scalar_mult_generic``
- - Actually seems to use xz.
- - Unknown formula (ladder).
+ - xz.
+ - Unknown formula: `ladd-boringssl-x25519 <https://github.com/J08nY/pyecsca/blob/master/test/data/formulas/ladd-boringssl-x25519.op3>`__ from fiat-crypto.
 
 Ed25519
 ^^^^^^^
@@ -521,7 +521,7 @@ KeyGen:
  - Montgomery
  - `Some Full precomputation <https://github.com/intel/ipp-crypto/blob/ippcp_2021.9.0/sources/ippcp/crypto_mb/src/x25519/ifma_x25519.c#L1596>`__ via ``mbx_x25519_public_key``
  - xz
- - Unknown formulas.
+ - Unknown formulas: `add-ipp-x25519 <https://github.com/J08nY/pyecsca/blob/master/test/data/formulas/add-ipp-x25519.op3>`__, `dbl-ipp-x25519 <https://github.com/J08nY/pyecsca/blob/master/test/data/formulas/dbl-ipp-x25519.op3>`__
 
 Derive:
  - Montgomery
diff --git a/test/data/formulas/add-ipp-x25519 b/test/data/formulas/add-ipp-x25519
new file mode 100644
index 0000000..befda7b
--- /dev/null
+++ b/test/data/formulas/add-ipp-x25519
@@ -0,0 +1,2 @@
+source Intel IPP crypto https://github.com/intel/ipp-crypto/blob/ippcp_2021.9.0/sources/ippcp/crypto_mb/src/x25519/ifma_x25519.c#L1676
+coords xz
diff --git a/test/data/formulas/add-ipp-x25519.op3 b/test/data/formulas/add-ipp-x25519.op3
new file mode 100644
index 0000000..2b2a446
--- /dev/null
+++ b/test/data/formulas/add-ipp-x25519.op3
@@ -0,0 +1,9 @@
+B = X1 - Z1
+A = X1 + Z1
+C = mu * B //???
+B = A - C
+A = A + C
+A = A^2
+B = B^2
+X1 = Z2 * A
+Z1 = X2 * B
diff --git a/test/data/formulas/dbl-ipp-x25519 b/test/data/formulas/dbl-ipp-x25519
new file mode 100644
index 0000000..9010ee9
--- /dev/null
+++ b/test/data/formulas/dbl-ipp-x25519
@@ -0,0 +1,4 @@
+source Intel IPP crypto https://github.com/intel/ipp-crypto/blob/ippcp_2021.9.0/sources/ippcp/crypto_mb/src/x25519/ifma_x25519.c#L1689
+parameter a24
+assume a24 = (a+2)/4
+coords xz
diff --git a/test/data/formulas/dbl-ipp-x25519.op3 b/test/data/formulas/dbl-ipp-x25519.op3
new file mode 100644
index 0000000..baaeb54
--- /dev/null
+++ b/test/data/formulas/dbl-ipp-x25519.op3
@@ -0,0 +1,9 @@
+A = X1 + Z1
+B = X1 - Z1
+A = A^2
+B = B^2
+C = A - B
+D = a24 * C
+D = D + B
+X3 = A * B
+Z3 = C * D
diff --git a/test/data/formulas/ladd-boringssl-x25519 b/test/data/formulas/ladd-boringssl-x25519
new file mode 100644
index 0000000..416b245
--- /dev/null
+++ b/test/data/formulas/ladd-boringssl-x25519
@@ -0,0 +1,4 @@
+source BoringSSL bfa8369 https://github.com/google/boringssl/blob/bfa8369795b7533a222a72b7a1bc928941cd66bf/crypto/curve25519/curve25519.c#L624
+parameter a24
+assume a24 = (a+2)/4
+coords xz
diff --git a/test/data/formulas/ladd-boringssl-x25519.op3 b/test/data/formulas/ladd-boringssl-x25519.op3
new file mode 100644
index 0000000..738d213
--- /dev/null
+++ b/test/data/formulas/ladd-boringssl-x25519.op3
@@ -0,0 +1,18 @@
+tmp0 = X3 - Z3
+tmp1 = X2 - Z2
+X2 = X2 + Z2
+Z2 = X3 + Z3
+Z3 = tmp0 * X2
+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
diff --git a/test/sca/test_structural.py b/test/sca/test_structural.py
index bf93a20..b323f58 100644
--- a/test/sca/test_structural.py
+++ b/test/sca/test_structural.py
@@ -224,6 +224,20 @@ def test_formula_similarity(secp128r1):
             ("secg", "secp256r1"),
             DoublingEFDFormula,
         ],
+        [
+            "ladd-boringssl-x25519",
+            MontgomeryModel,
+            "xz",
+            ("other", "Curve25519"),
+            LadderEFDFormula,
+        ],
+        [
+            "dbl-ipp-x25519",
+            MontgomeryModel,
+            "xz",
+            ("other", "Curve25519"),
+            DoublingEFDFormula,
+        ],
     ],
 )
 def test_formula_correctness(name, model, coords, param_spec, formula_type):