Add opt-in direct quotient lowering for the Solidity verifier

[jtcoolen]

Summary

Adds QuotientLowering::Direct, an opt-in alternative to the quotient bytecode VM. The option lives in RenderOptions.quotient_lowering. The default is still Vm, and Vm renders are byte-identical to main.

In Direct mode the quotient numerator is written as Yul that follows the Rust verifier identity by identity:

• One function per gate identity. Each gate identity becomes q_identity_<j>, in partially_evaluate_identities order. A header gives its index, gate name, polynomial index, bucket and y power. The body transliterates the gate's Expression tree node by node, using named constants for evaluation slots, buckets, y powers and constants.

• Explicit fold. Every identity is folded as bucket += Y_POW[m-1-j] * e_j, which is the weighting compute_linearization_commitment uses. This covers the gates and the permutation, lookup and trash families (the families keep their existing structured emitters). The gap/tail selector machinery is not used.

• Two shapes recognised from the expression trees. No circuit parameters are hard-coded; anything that doesn't match stays plain transliteration.

  • A linear combination over a limb vector becomes a call to sum_exprs.
  • sum c_ij x_i y_j, where the generator checks that c_ij depends only on i+j, becomes pair_wise_prod_by_degree followed by sum_exprs_by_degree.

  These are the shapes produced by sum_exprs / pair_wise_prod in circuits/src/field/foreign/util.rs. The i+j grouping is valid because of double_base_powers in params.rs.

• Constants live in the VK. Scalar constants and coefficient runs go into the VK payload in place of the VM constants and program.

Motivation: the VM spreads the 49 Moonlight identities over six mechanisms. Most of the gate logic exists only as packed bytecode in the VK contract. That is hard to cross-reference with the Rust code, and it costs about 200k gas per proof. The VM was a bytecode-size measure, not a gas measure.

Checks

• IR validation at codegen (fails closed). Every identity's IR, bound to the deployed memory layout and VK table, is evaluated at 4 random points against the original Expression::evaluate.
• Fold check at codegen (fails closed). Every identity 0..m-1 is folded exactly once, with weight Y_POW[m-1-j] and into its manifest bucket. This includes the family loops, which are expanded iteration by iteration. Negative tests cover a duplicated weight, a missing identity, a wrong bucket and family-loop off-by-one errors.
• Probe differential (EVM tier). A test-only probe render returns [expected_eval, selector_acc[..]] after the quotient section.
  • It runs in revm on the honest proof, 8 random evaluation frames and one frame with changed challenges.
  • The reference is midnight-proofs' own partially_evaluate_identities values, folded with the linearization rule. The Vm probe is compared against the same reference.
  • A dropped-limb bug injected in the sum_exprs emitter passes codegen and is caught here, with the failing buckets and identities named.
• Trace test.
  • The existing per-identity trace ids (30000+j) still match in Direct mode.
  • New intermediate ids are added and documented in docs/reference/TRACE_VARIABLES.md: helper results 70000+, product-table entries 75000+, limb-view words 77500+. They are compared against the original sub-expressions evaluated natively.
  • Trace renders (only) now return false instead of reverting on final-check failure, so a rejected proof's trace survives. Production renders are unchanged.
• New fixture. tests/foreign_field_fixture.rs is a secp256k1 foreign-field / EC circuit that exercises the recognisers.

Measurements

solc 0.8.35 via-IR, optimizer runs 200, Cancun; anvil with --hardfork prague and the default code-size limit.

Circuit	Vm verify gas	Direct verify gas
poseidon	636,758	622,400
rsa	593,487	588,056
sha_preimage	829,441	783,365
hybrid_mt	852,454	786,909
foreign_field (new)	871,126	787,866
IVC decider	1,282,342	1,058,582

Moonlight wrap verifier (Nightfall fee_12345, B64; B8 is within a few dozen gas), rendered from the committed production VK and verified with the real fixture proofs:

	Verifier runtime	VK runtime	Verify gas	Quotient section gas
Production (VM)	21,253 B	17,057 B	1,277,218	301,747
Direct	22,578 B	10,081 B	1,065,440	93,481

Correctness on Moonlight:

• Real proofs: both accepted at each block size.
• Mutants: all rejected, in the implementer's run (15 per block size) and in an independent reviewer's own set (14 per block size).
• Equivalence with production: the expected evaluation and the 10 selector accumulators equal production's on 16 inputs, including random evaluation frames and changed challenges.
• Trace diff: 244 shared ids plus 227 intermediates match, with 0 mismatches.

Tests

• cargo test --release --lib: 169 passed.
• HALO2_SOLIDITY_RUN_EVM_TESTS=1 cargo test --release --features evm,rust-verifier-trace --lib: 207 passed.
• Fixtures (poseidon, rsa, sha_preimage, hybrid_mt, foreign_field) with evm,rust-verifier-trace and with evm,truncated-challenges: pass.
• ivc_keccak_solidity with evm,rust-verifier-trace,in-circuit-fewer-point-sets: passes.
• Clippy is clean apart from an existing warning in abi/proof.rs.

Limitations / follow-ups

• Headroom. The Direct verifier is about 1.3 KB larger than the VM verifier on Moonlight, leaving about 2 KB under EIP-170. A compile-and-measure size policy with a split fallback is not included yet.
• Inline only. Direct works only with RenderQuotient::Inline; ExternalPinned is refused.
• Compiler dependence. Helpers stay out of line only because solc does not inline recursive functions (each helper has a never-taken self call). Without that the Moonlight verifier does not fit.
• What the IR validation does not see. It does not execute the emitted Yul. That is what the probe differential and the trace test cover.
• Not run. The whole-workspace --all-features suite and the pbt_ tests.
• Making Direct the default. This needs the default flipped, the VM emitter and codec removed, and the committed dumps and Nightfall contracts regenerated.

This branch is based on 6b3d2096 ("Fix transcript buffer sizing and quotient VM const-table overflow"), which is not yet on main, so it is included here.

🤖 Generated with Claude Code