[mjthatch]

Stacked on #2 (sparse commitments).

Summary

An addition step used to prove xQ ≠ x with an inverse d from the prover: one F_p2 word pair and one relation per addition. This PR drops d. At an addition, B's line is taken through the two points, which is B's line multiplied by xQ − x. If xQ = x, that line is 0, so the residue check fails on its own.

	#2	this PR
program cost	68.5 M mWU	67.6 M mWU
pruned program	60.3 kB	60.2 kB
witness	29.7 kB	28.5 kB
spend on Elements 23.3.1 regtest	90.8 kWU, 22.7 kvB	89.4 kWU, 22.4 kvB
relations, degree of S, coefficients of Q	150, 211, 200	127, 217, 208

How it works

At an addition T + Q, B's line is yP + c3 xP w + c4 w³ with c3 = −λ and c4 = λx − y. Multiply it by Δ = xQ − x and replace λΔ by yQ − y, which the slope relation guarantees:

l'_B = (xQ - x) yP - (yQ - y) xP w + (x yQ - y xQ) w^3

This is the line through T and Q. It doesn't use the slope.

Soundness. The slope relation λ(xQ − x) = yQ − y has one solution when xQ ≠ x. If xQ = x, the relation forces yQ = y. Then l'_B = 0·yP − 0 + (x·y − y·x) w³ = 0, so f' = 0. Every later Miller value is then 0 too: committed values have to equal the products. The last relation, f·π(c⁻¹)π²(c)π³(c⁻¹) = T_s, fails because T_s ≠ 0. So an accepted slope is still the true slope, and every step is still the group law.

Completeness. The Miller value now carries a factor Δ ∈ F_p2 at each addition. Elements of F_p2* are r-th powers in F_p12* (p² − 1 divides (p¹² − 1)/r), so the factor doesn't change whether f·e(α, β) is an r-th power. That is exactly the condition the residue witness proves. The prover computes c and s for the scaled Miller value (pairing.miller_values).

What it costs. l'_B has degree 27 instead of 21, so each addition's relation grows by 6. The schedule now uses a degree cap of 217: 35 Miller values and a 206-word Q, padded to 208 so the eight-word chunks of QCHUNK still fit. Each addition step also becomes cheaper, since it drops the evaluation of d and one relation.

Net effect: 23 relations fewer, 46 witness words fewer, 8 Q words more. Soundness is the same kind of bound: (127 + 219)/p per hash query.

Changes

• groth/pairing.py:
  • relations: the two-point line at additions; the inverse relation is gone.
  • miller_values: the prover's Miller values with the scaled lines, used for the residue witness.
  • Leaves without d.
  • The addition step evaluates l'_B from xQ − x, yQ − y and x·yQ − y·xQ.
  • DEG_CAP = 217; Q is padded to a multiple of 8.
• Tests:
  • test_pairing.py: the "wrong inverse" case is gone.
  • test_g2_check.py: builds its constant from miller_values.
• Docs, benchmarks, the README cost table and examples/multiplier/ are updated. The example files come from a new regtest spend.

Testing

• All tests pass (fp, poly, curve, pairing, g2_check, binding, groth16, bn254_ref), and the predicted costs equal hand's.
• These re-sealed tampered witnesses are rejected: a wrong slope, a wrong committed Miller value, a wrong s, a wrong challenge.
• Points outside G2 fail only on the two G2 relations.
• Elements 23.3.1 regtest, tools/regtest.sh:
  • proof spend 116e0f79…: 89,403 WU;
  • the redirected proof is rejected (Assertion failed inside jet);
  • second spend 71b20492… (the example files);
  • key path c17731ad….
• The example's program and witness regenerate byte for byte.

🤖 Generated with Claude Code

[mjthatch]

Superseded by #5: no addition of the loop can meet T = Q, so the inverses are not needed at all, and neither is the two-point line.