1"""Stage 3 — symbolic verification (SymPy, exact) of the algebraic identities used in the paper.23Checks (each returns True or raises):4 S1 The affine addition and doubling formulas map curve points to curve points (identity modulo the curve equations).5 S2 φ(x, y) = (βx, y) with β³ = 1 is a group endomorphism: φ(P + Q) = φ(P) + φ(Q) and φ(2P) = 2φ(P) (a = 0).6 S3 The x-only differential addition formula for y² = x³ + b (Brier–Joye 2002 specialised to a = 0):7 x(P+Q) · x(P−Q) · (x_P − x_Q)² = (x_P x_Q − a)² − 4b(x_P + x_Q) [a = 0 here]8 S4 Semaev's third summation polynomial S3 for y² = x³ + ax + b, derived from the group law, vanishes on x-coordinates9 of P, Q, P+Q and P, Q, P−Q (symmetric form), and its total degree is 2 in each variable.10 S5 ECDSA malleability: with s' = −s mod n the verification point is −X, whose x-coordinate equals that of X.11 S6 Schnorr correctness: s = k + e·d ⇒ sG = R + eP (as scalar identities).12Writes results/theory/symbolic_checks.json.13"""14import json, sys, time, pathlib15import sympy as sp16ROOT = pathlib.Path(__file__).resolve().parents[2]17sys.path.insert(0, str(ROOT / "src"))18from wp34.provenance import record1920x1, y1, x2, y2, a, b, beta = sp.symbols("x1 y1 x2 y2 a b beta")212223def reduce_mod_curve(expr, pts):24 """Reduce a rational expression modulo y_i² = x_i³ + a x_i + b for the given points, return canonical numerator."""25 num, den = sp.fraction(sp.together(expr))26 G = [yi**2 - (xi**3 + a * xi + b) for xi, yi in pts]27 gens = [yi for _, yi in pts] + [xi for xi, _ in pts] + [a, b]28 _, r = sp.reduced(sp.expand(num), G, *gens)29 return sp.simplify(r)303132def add_formula(P, Q):33 (xa, ya), (xb, yb) = P, Q34 lam = (yb - ya) / (xb - xa)35 x3 = lam**2 - xa - xb36 y3 = lam * (xa - x3) - ya37 return x3, y3383940def dbl_formula(P):41 xa, ya = P42 lam = (3 * xa**2 + a) / (2 * ya)43 x3 = lam**2 - 2 * xa44 y3 = lam * (xa - x3) - ya45 return x3, y3464748def S1():49 x3, y3 = add_formula((x1, y1), (x2, y2))50 on = y3**2 - (x3**3 + a * x3 + b)51 r_add = reduce_mod_curve(on, [(x1, y1), (x2, y2)])52 x3d, y3d = dbl_formula((x1, y1))53 r_dbl = reduce_mod_curve(y3d**2 - (x3d**3 + a * x3d + b), [(x1, y1)])54 return r_add == 0 and r_dbl == 0555657def S2():58 # a = 0 and beta^3 = 159 x3, y3 = add_formula((x1, y1), (x2, y2))60 phi_sum = (beta * x3, y3)61 x3p, y3p = add_formula((beta * x1, y1), (beta * x2, y2))62 d1 = sp.together(phi_sum[0] - x3p); d2 = sp.together(phi_sum[1] - y3p)63 # reduce beta^3 → 1 : substitute beta^3 = 1 via polynomial remainder64 ok = True65 for d in (d1, d2):66 num, _ = sp.fraction(d)67 _, r = sp.reduced(sp.expand(num), [beta**3 - 1], beta, x1, y1, x2, y2)68 ok &= sp.simplify(r) == 069 xd, yd = dbl_formula((x1, y1))70 xd = xd.subs(a, 0); yd = yd.subs(a, 0)71 xdp, ydp = dbl_formula((beta * x1, y1)); xdp = xdp.subs(a, 0); ydp = ydp.subs(a, 0)72 for d in (beta * xd - xdp, yd - ydp):73 num, _ = sp.fraction(sp.together(d))74 _, r = sp.reduced(sp.expand(num), [beta**3 - 1], beta, x1, y1)75 ok &= sp.simplify(r) == 076 return bool(ok)777879def S3():80 xs, _ = add_formula((x1, y1), (x2, y2))81 xd, _ = add_formula((x1, y1), (x2, -y2))82 lhs = xs * xd * (x1 - x2)**283 rhs = (x1 * x2 - a)**2 - 4 * b * (x1 + x2)84 r = reduce_mod_curve(lhs - rhs, [(x1, y1), (x2, y2)])85 return r == 0868788def S4():89 x3 = sp.symbols("x3")90 # Semaev (2004): S3(x1,x2,x3) = (x1−x2)²x3² − 2((x1+x2)(x1x2+a) + 2b)x3 + (x1x2−a)² − 4b(x1+x2)91 S3p = (x1 - x2)**2 * x3**2 - 2 * ((x1 + x2) * (x1 * x2 + a) + 2 * b) * x3 + (x1 * x2 - a)**2 - 4 * b * (x1 + x2)92 xs, _ = add_formula((x1, y1), (x2, y2))93 xd, _ = add_formula((x1, y1), (x2, -y2))94 ok = reduce_mod_curve(S3p.subs(x3, xs), [(x1, y1), (x2, y2)]) == 095 ok &= reduce_mod_curve(S3p.subs(x3, xd), [(x1, y1), (x2, y2)]) == 096 degs = [sp.Poly(S3p, v).degree() for v in (x1, x2, x3)]97 sym = sp.expand(S3p - S3p.subs({x1: x2, x2: x3, x3: x1}, simultaneous=True)) == 098 return bool(ok and degs == [2, 2, 2] and sym)99100101def S5():102 n, z, r, s, d = sp.symbols("n z r s d")103 # verification point X = u1 G + u2 Q = (z/s) G + (r/s) Q. With s' = -s: X' = -(z/s) G - (r/s) Q = -X.104 w = 1 / s105 u1, u2 = z * w, r * w106 wp = 1 / (-s)107 u1p, u2p = z * wp, r * wp108 return sp.simplify(u1p + u1) == 0 and sp.simplify(u2p + u2) == 0 # scalars negate ⇒ point negates ⇒ same x109110111def S6():112 k, e, d = sp.symbols("k e d")113 s = k + e * d114 return sp.simplify(s - (k + e * d)) == 0 # sG = kG + e(dG) = R + eP by the Z-module structure115116117def main():118 t0 = time.time()119 res = {"S1_formulas_preserve_curve": S1(), "S2_phi_is_endomorphism": S2(), "S3_xonly_differential_addition": S3(),120 "S4_semaev_S3_polynomial": S4(), "S5_ecdsa_malleability_scalars": S5(), "S6_schnorr_correctness_scalars": S6()}121 record("symbolic_checks_sympy", {"sympy": sp.__version__}, res, out=str(ROOT / "results/theory/symbolic_checks.json"), started=t0)122 print(json.dumps(res, indent=1)); print("ALL:", all(res.values()))123124125if __name__ == "__main__":126 main()127