[OBrezhniev]

Stacked on #150 (option A) so that the diff is exactly the design difference: the adder's constraint replaced by an xdistinct tag, granted by DistinctXCheck (one constraint) or AssumeDistinctX (none; the caller's algorithm is the proof, written beside each of the 18 sites). Untagged callers fail to compile. Restores the pre-guard constraint counts (eddsapedersen_test 17685, i.e. +14 for the two conversion guards only). Mutually exclusive with #150; the fuzz of #150 is the evidence that the assumed property holds on the assume paths.

Guard MontgomeryAdd with a tag instead of a constraint

Alternative to 8e03929 for the incomplete-addition precondition of
MontgomeryAdd, for review against it. 8e03929 closes the pin1 == pin2
hole with one constraint per instantiation, which costs 11–17% on the
scalar multipliers because the adder sits in their inner loops.

This branch removes that constraint and instead requires the tag
xdistinct on pin2. Two templates grant it:

DistinctXCheck()(pin1, pin2) one constraint, holds for any inputs
AssumeDistinctX()(pin2) no constraint; the caller's algorithm
is the proof, written beside the call

A caller that does neither fails to compile:
error[T3001]: missing tags required by input signal.

What this buys: forgetting the precondition is a compile error, and
every place it is assumed rather than checked is a named, greppable
call. What it does not buy: the compiler cannot tell whether an assume
is true. That is the same bargain every other tag in the library makes.

18 AssumeDistinctX sites, each with its argument:
WindowMulFix, Window4 base + (k-1)base, k <= 8: coincide only if
(k-2)base or kbase is the identity,
impossible for a base of prime order r
SegmentMulFix cadders multipliers (8^i-1)/7 and 8^i, distinct,
sum below r for <= 83 windows
SegmentMulFix adders accumulator >= 28^nWB, window <= 8^nWB
Pedersen Segment |acc| < 32^i <= |window_i|, <= 50 windows
BitElementMulAny odd vs even multiple of P below 2^149;
rests on P having prime order, the S5
precondition EscalarMulAny already states
1 DistinctXCheck site: test/circuits/montgomeryadd.circom, whose inputs
are arbitrary.

Edwards2Montgomery and Montgomery2Edwards keep their plain guards from
8e03929; those cost 14 constraints in total across the EdDSA circuit.

Verified: every scalar-multiplication circuit returns to its
conversion-guards-only count (eddsapedersen_test 17685, escalarmulfix
3945, escalarmulany 2562, babypbk 4696; pedersen2_test 3817 -> 3371).
DistinctXCheck accepts G + 2G and rejects G + G and G + (-G). Full
suite 118 passing. Correctness fuzz 1257 cases against circomlibjs,
0 wrong. The evidence that the assumed property holds on the assume
paths is the 4140-case fuzz of 8e03929, where the constraint never
fired; with the constraint gone, this branch's fuzz can check
correctness only.

🤖 Generated with Claude Code

https://claude.ai/code/session_01D1w729xzwemQigkf3PCisD