S6, option A: constrain the degenerate cases in the Montgomery templates

[OBrezhniev]

Stacked on #149 (fix/circomlib_buses_review); this PR shows only its own commits. Independent of the other stacked PRs unless stated. Full suite passes on the branch.

One of two mutually exclusive alternatives for S6. This option closes the underconstrained cases (Edwards2Montgomery at (0,−1), Montgomery2Edwards at (0,0), MontgomeryAdd at pin1 == pin2) with one constraint each. Cost: +11–17% on the scalar multipliers, all from MontgomeryAdd in their inner loops (eddsapedersen_test 17671 → 19652). Fuzzed: 4140 cases, the guard never fired on a legitimate input. The alternative, #151, keeps the two cheap conversion guards and replaces the adder's constraint with a tag.

Constrain the degenerate cases in the Montgomery templates

Three templates left a signal free instead of rejecting an input they
cannot handle, so a prover could choose that signal at will:

• Edwards2Montgomery at pin == (0, -1): pout.y * pin.x === pout.x forces
  pout.x to 0 and never mentions pout.y again.
• Montgomery2Edwards at pin == (0, 0): pout.x * pin.y === pin.x forces
  pin.x to 0 and never mentions pout.x again.
• MontgomeryAdd for pin1 == pin2: lamda * (pin2.x - pin1.x) === pin2.y -
  pin1.y becomes 0 === 0, and the whole output follows from lamda.

Each is closed by requiring the divisor to be invertible, which is one
constraint and is satisfiable exactly when the divisor is non-zero. The
remaining degenerate inputs, pin.y == 1 in Edwards2Montgomery, pin.x ==
-1 in Montgomery2Edwards, same x with different y in MontgomeryAdd, and
pin.y == 0 in MontgomeryDouble, were already unsatisfiable and are left
alone.

Two of the three were reachable by the ordinary witness generator, which
is what makes them worth constraining rather than documenting:
MontgomeryAdd(P, P) and Montgomery2Edwards at (0, 0) both produced a
witness before and produce none now. The Edwards2Montgomery case only
ever failed on a division by zero in the generator, while the
constraints still left pout.y free.

Cost, non-linear constraints, all from MontgomeryAdd, which the scalar
multipliers and the Pedersen hash instantiate in their inner loops:

eddsapedersen_test 17671 -> 19652 (+1981, +11%)
escalarmulfix_test 3939 -> 4625 (+686, +17%)
escalarmulany_test 2557 -> 2813 (+256, +10%)
babypbk_test 4690 -> 5376 (+686, +15%)

The two conversion guards alone account for 14, 6, 5 and 6 of those.
Every existing test still passes, so no legitimate input relied on the
unconstrained behaviour.

Say which adder to use when MontgomeryAdd cannot be

8e03929 made MontgomeryAdd reject pin1 == pin2 rather than leave lamda
free, which is right but leaves a caller who cannot rule that out with
nothing to call. The answer is BabyAdd, whose law is complete on
Baby-Jubjub (see 2e29520).

MontgomeryAdd now states its precondition in its spec and says what to
reach for: MontgomeryDouble when the points are known equal, itself when
they are known to differ in x and the cheaper law is wanted, BabyAdd when
neither is known.

Comments only.

🤖 Generated with Claude Code

https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD