Handle fully symbolic assumptions.

Fixes #13.

2 files changed, 30 insertions, 2 deletions

diff --git a/pyecsca/ec/formula.py b/pyecsca/ec/formula.py
index c785166..ef206ab 100644
--- a/pyecsca/ec/formula.py
+++ b/pyecsca/ec/formula.py
@@ -11,7 +11,7 @@ from sympy import sympify, FF, symbols, Poly, Rational
 
 from .context import ResultAction, getcontext, NullContext
 from .error import UnsatisfiedAssumptionError, raise_unsatisified_assumption
-from .mod import Mod
+from .mod import Mod, SymbolicMod
 from .op import CodeOp, OpType
 from ..misc.cfg import getconfig
 
@@ -139,6 +139,8 @@ class Formula(ABC):
 
     def __validate_assumptions(self, field, params):
         # Validate assumptions and compute formula parameters.
+        # TODO: Should this also validate coordinate assumptions and compute their parameters?
+        is_symbolic = any(isinstance(x, SymbolicMod) for x in params.values())
         for assumption in self.assumptions:
             assumption_string = unparse(assumption)[1:-2]
             lhs, rhs = assumption_string.split(" == ")
@@ -153,6 +155,16 @@ class Formula(ABC):
                         getconfig().ec.unsatisfied_formula_assumption_action,
                         f"Unsatisfied assumption in the formula ({assumption_string}).",
                     )
+            elif lhs in self.parameters and is_symbolic:
+                # Handle a symbolic assignment to a new parameter.
+                k = FF(field)
+                expr = sympify(rhs, evaluate=False)
+                for curve_param, value in params.items():
+                    if isinstance(value, SymbolicMod):
+                        expr = expr.subs(curve_param, value.x)
+                    else:
+                        expr = expr.subs(curve_param, k(value))
+                params[lhs] = SymbolicMod(expr, field)
             else:
                 k = FF(field)
                 expr = sympify(f"{rhs} - {lhs}", evaluate=False)
diff --git a/test/ec/test_regress.py b/test/ec/test_regress.py
index ad3e096..9304c9e 100644
--- a/test/ec/test_regress.py
+++ b/test/ec/test_regress.py
@@ -1,10 +1,11 @@
 from typing import cast
 from unittest import TestCase
+from sympy import symbols
 
 from pyecsca.ec.coordinates import AffineCoordinateModel
 from pyecsca.ec.curve import EllipticCurve
 from pyecsca.ec.formula import AdditionFormula, DoublingFormula, ScalingFormula
-from pyecsca.ec.mod import Mod
+from pyecsca.ec.mod import Mod, SymbolicMod
 from pyecsca.ec.model import MontgomeryModel, EdwardsModel
 from pyecsca.ec.params import get_params
 from pyecsca.ec.mult import LTRMultiplier
@@ -75,3 +76,18 @@ class RegressionTests(TestCase):
         self.assertEqual(neutral, neutral_affine.to_model(coords, curve))
         neutral_sqr = Point(coords_sqr, Y=c ** 2 * r, Z=Mod(1, p))
         self.assertEqual(neutral_sqr, neutral_affine.to_model(coords_sqr, curve))
+
+    def test_issue_13(self):
+        model = EdwardsModel()
+        coords = model.coordinates["yz"]
+        c, r, d = symbols("c r d")
+        p = 53
+        c = SymbolicMod(c, p)
+        r = SymbolicMod(r, p)
+        d = SymbolicMod(d, p)
+        yd, zd, yp, zp, yq, zq = symbols("yd zd yp zp yq zq")
+        PmQ = Point(coords, Y=SymbolicMod(yd, p), Z=SymbolicMod(zd, p))
+        P = Point(coords, Y=SymbolicMod(yp, p), Z=SymbolicMod(zp, p))
+        Q = Point(coords, Y=SymbolicMod(yq, p), Z=SymbolicMod(zq, p))
+        formula = coords.formulas["dadd-2006-g-2"]
+        formula(p, PmQ, P, Q, c=c, r=r, d=d)