Add NSS.

3 files changed, 29 insertions, 0 deletions

diff --git a/test/data/formulas/ladd-hacl-x25519 b/test/data/formulas/ladd-hacl-x25519
new file mode 100644
index 0000000..1dbe8cc
--- /dev/null
+++ b/test/data/formulas/ladd-hacl-x25519
@@ -0,0 +1,4 @@
+source HACL* https://github.com/hacl-star/hacl-star/blob/v0.3.0/specs/Spec.Curve25519.fst#L56
+parameter am24
+assume am24 = (a-2)/4
+coords xz
diff --git a/test/data/formulas/ladd-hacl-x25519.op3 b/test/data/formulas/ladd-hacl-x25519.op3
new file mode 100644
index 0000000..7893eb9
--- /dev/null
+++ b/test/data/formulas/ladd-hacl-x25519.op3
@@ -0,0 +1,18 @@
+a = X2 + Z2
+b = X2 - Z2
+c = X3 + Z3
+d = X3 - Z3
+da = d * a
+cb = c * b
+X3 = da + cb
+Z3 = da - cb
+aa = a^2
+bb = b^2
+X5 = X3^2
+Z3 = Z3^2
+e = aa - bb
+e121665 = e * am24
+aa_e121665 = aa + e121665
+X4 = aa * bb
+Z4 = e * aa_e121665
+Z5 = Z3 * X1
diff --git a/test/sca/test_structural.py b/test/sca/test_structural.py
index 0645972..099e348 100644
--- a/test/sca/test_structural.py
+++ b/test/sca/test_structural.py
@@ -185,6 +185,13 @@ def test_efd_formula_match():
             ("other", "Curve25519"),
             LadderEFDFormula,
         ],
+        [
+            "ladd-hacl-x25519",
+            MontgomeryModel,
+            "xz",
+            ("other", "Curve25519"),
+            LadderEFDFormula,
+        ],
     ],
 )
 def test_formula_correctness(name, model, coords, param_spec, formula_type):