[mjthatch]

Hardening from the security audit (build/security-audit/). Stacked on the security-fixes PR. Some facts the soundness argument relies on were kept only by construction or by a test, so the generator now checks them. Some tests could pass with the check they were meant to test removed, so they now exercise it. The generated programs are unchanged byte for byte.

Summary

	before	after
no addition meets T = Q; the loop reaches [6x+2]B	a test	the generator refuses otherwise (additions_avoid_q)
the loop state stays within its bounds	the output bounds were recorded but never compared	compared; a stale bounds dict is refused
each witness node is read once	by construction	Groth16.compile counts its occurrences in the tree unfolding
subtree, split	assumed a whole subtree in order, and matching widths	checked
a binding with more than one public input	refused only by the CLI	refused by Groth16
a crash of hand in a test	the remaining cases were silently skipped	the test fails
an intended rejection	any failure at stage exec or finalize, type errors included	must be a failed jet
wrong input and tampered proof in test_groth16	rejected by the challenge first	also sealed again, so the identity must reject them; plus x + 2^254 and x + r, which only the range check rejects
keys with 3 to 5 inputs	numeric model only; the wrong input was not sealed again	also sealed again; the window factors of the normalised step run in hand

Commits

1. Check at generation the invariants the soundness argument rests on.

• pairing.additions_avoid_q(STEPS). This runs in every PairingCheck. No addition can meet T = Q for any point of the twist, and the loop reaches [6x+2]B before its two Frobenius additions. The check uses the eigenvalues of ψ on the cofactor's primes (PSI_EIGEN); tests/test_g2_check.py derives them and compares.
• Loop bounds. After the step functions and QCHUNK are built, every output bound is compared with the input bound it must stay within.
• Witness nodes. Emitter.tree_uses() counts how often each definition occurs in the tree unfolding of main. Groth16.compile requires exactly 90 witness nodes, each occurring once.
• Projections. Sym.subtree requires the leaves to be exactly one subtree, in its order (the numeric backend takes them in the order given), and Sym.split requires matching widths.
• Binding. Groth16(depth > 0) requires one public input.
• Check names. chain names its checks with a counter, so a dropped check can no longer make a later one overwrite an earlier one.
• All of these are ensure, so python -O keeps them.
• Tests. tests/test_invariants.py is new, in make and CI. It checks:
  • each refusal;
  • that all 23 jet_verify nodes of the verifier are reachable from main;
  • that none of them lies under a branch of any of its 8,226 cases, which pruning could drop.

2. Make the tests fail when a check of the program is broken.

• harness.run. It raises if hand exits non-zero or prints fewer results than witnesses. harness.expect_rejected requires Jet failed during execution, and replaces the stage-only asserts in five tests.

• test_groth16.py. Four witnesses are sealed again (r, Q and z recomputed, which anyone can do), so that the challenges pass:

  • the wrong input and the tampered proof: the identity rejects them;
  • the input plus 2^254: the windows read bits 0..253 and the identity holds;
  • the input plus r, when it fits in 254 bits: the same factors.

  Only the range check rejects the last two. The numeric model runs the pairing check before the range checks, so the test also asserts which check rejects each case there: the identity (verify failed) for the first four, range check for the aliases.

• test_inputs.py.

  • The wrong input is also sealed again.
  • For the 3-input key, win_factors at step 87 runs in hand as a program of its own, against the numeric model, on the honest and the extreme run values; a wrong factor must be rejected. Step 87 is where PairingCheck.prod normalises. The whole 3-input program takes 25 minutes to parse; this takes seconds.
  • The test now needs the harness.

• test_pairing.py. It adds a flipped z, and a point word re-encoded as itself plus 4p without sealing again: the challenge must reject both.

• test_fp.py. It adds words the jets must reduce first: 2^256 - 1, p_s + 5 and n_s + 7.

How the new tests were checked

Two controls were removed by hand in a scratch copy, and tests/test_groth16.py was run with its numeric-model precheck turned off, so that hand alone decides:

control removed	the old cases	the new case
the range check x < r (the word still read whole)	still rejected	accepted by the program: input + 2^254, sealed, so the test fails
the identity S(z) = Q(z) M(z)	still rejected (by the challenge)	accepted by the program: wrong input, sealed, so the test fails

On the old tests both mutants pass. Similarly, the 3-to-5-input numeric test passes with the identity removed, and the new sealed case catches it.

Testing

• Byte for byte. Program text and witness hashes were taken for every test program at main and at this branch: fp, curve, pairing, g2_check, binding, groth16, INPUTS=2 groth16. The programs are identical. The witnesses are identical, with the new cases added after them.
• Generated verifiers. Identical text for 1 input at depths 0, 1 and 2, and for 2 and 3 inputs.
• Tests. All pass: fp, poly, curve, pairing, g2_check, binding, groth16, inputs2, inputs, invariants, tools and bn254_ref.
• Lint. make lint is clean.

🤖 Generated with Claude Code