Reuse batched rational denominators

[ValarDragon]

Summary

• explicitly mark the projective lambda_2 / z batch as sharing the preceding
  lambda_1 / z denominators
• mark the following accumulator x / z^2 batch as using their squares
• retain 3,565 of 7,007 rational denominators per prepared Orchard circuit and
  derive the other 3,442 inverses from those retained values
• use per-cell source and target markers so the normal assignment path does not
  scan previously recorded relationship descriptors
• expand related denominators only on the existing advice-cell reassignment
  fallback

This PR applies directly to main and does not depend on #400.

Halo2 already performs one batch inversion per circuit witness. This PR keeps
that inversion count and shortens its serial multiplication walk. It reuses
1/z directly for lambda_2, and squares 1/z for x/z^2; it does not
recompute z, z^2, or add an earlier inversion.

The relationships are explicit, untrusted assignment hints. Debug builds check
the supplied denominators against the retained z values. A bad hint can only
produce an invalid witness; the circuit still constrains every assigned value.
If a recorded source or target cell is reassigned, the prover reconstructs the
ordinary per-cell denominators before applying the assignment.

The optimization is enabled for multi-circuit proof batches. Single-circuit
synthesis retains the original collection and evaluation path.

V12 follow-up

V12's review found five edge cases in the generic
relation API. The amended commit fixes all five and adds a focused regression
for each:

• shorter equality-related batches now become the complete remembered batch
• denominator removal materializes relationships before swap_remove
• expansion during an overwrite cannot be recorded as the new batch
• pre-existing rational target cells use ordinary batch-assignment fallback
• related batches validate and collect all numerators before mutating targets

These paths do not occur in the in-tree Sinsemilla assignment sequence, but
they are supported by the public assignment API and now retain ordinary batch
assignment semantics.

Performance

I temporarily instrumented real Orchard proof creation around
FloorPlanner::synthesize_batch and AdviceWitness::evaluate. Merkle witness
preparation was completed before the timed synthesis call, separating
assignment from concurrent preparation scheduling. Results are medians of 50
interleaved control/candidate pairs per arm with Rust 1.97.1:

Host	Circuits	Phase	Control	This change	Change
Apple M4, 10 workers	2	synthesis	0.991 ms	0.976 ms	-1.4%
Apple M4, 10 workers	2	rational evaluation	0.237 ms	0.170 ms	-28.2%
Apple M4, 10 workers	2	combined	1.226 ms	1.147 ms	-6.5%
Apple M4, 10 workers	6	synthesis	2.090 ms	2.071 ms	-0.9%
Apple M4, 10 workers	6	rational evaluation	0.458 ms	0.350 ms	-23.5%
Apple M4, 10 workers	6	combined	2.550 ms	2.414 ms	-5.3%
x86_64 Linux, 8 workers	2	synthesis	1.996 ms	2.063 ms	+3.4%
x86_64 Linux, 8 workers	2	rational evaluation	0.734 ms	0.496 ms	-32.4%
x86_64 Linux, 8 workers	2	combined	2.766 ms	2.563 ms	-7.3%
x86_64 Linux, 8 workers	6	synthesis	4.927 ms	4.884 ms	-0.9%
x86_64 Linux, 8 workers	6	rational evaluation	0.859 ms	0.588 ms	-31.6%
x86_64 Linux, 8 workers	6	combined	5.794 ms	5.487 ms	-5.3%

These measurements predate the rebase and used #400 as the control revision.
That does not include #400's Merkle-preparation work in the timed interval, so
the table isolates this change, but it is not a fresh comparison against the
current main revision.

I also benchmarked the old PR head against the V12-fixed head using 50 fresh
interleaved pairs per arm. The paired median change in combined synthesis and
rational evaluation was +0.0035 ms (2 circuits) and +0.0009 ms (6 circuits) on
Apple M4, and +0.0329 ms (2 circuits) and -0.1399 ms (6 circuits) on x86_64
Linux. The reusable validation scratch and defensive fallbacks therefore do
not materially change the optimized six-circuit path.

The earlier benchmark_witness_assignment numbers were not valid for this PR:
that benchmark intentionally leaves Assigned::Rational values unevaluated.

Testing

• cargo fmt --all -- --check
• git diff --check
• ./scripts/changelog.py check
• cargo check -p zakura-orchard --no-default-features
• cargo check -p zakura-orchard --all-features
• cargo test -p zakura-halo2-proofs --lib
• cargo test --release -p zakura-halo2-proofs advice_witness_ --lib
• cargo test -p zakura-halo2-proofs parallel_advice_evaluation_preserves_proof_bytes --lib
• cargo test -p zakura-halo2-gadgets sinsemilla::merkle::tests --lib
• cargo test -p zakura-orchard --lib
• cargo test -p zakura-orchard --test builder

[v12-auditor]

Note

Complete: Audit complete. V12 found five issues worth reviewing.

Open the full results here.

Finding	Severity	Details
F-268859	🔵 Low	Short hints retain stale predecessor length The public Region relation APIs define each hint against the immediately preceding batch, but the optimized prover does not update the remembered length after a shorter equality-related batch. Given a base batch of length N, an equality-related batch of length M < N, and a later relation of length L where M < L <= N, the later call passes because last_denominator_batch still contains the original length N. Debug builds compare the later denominators against the older base batch, while release builds discard the supplied denominators and evaluate the advice using inverses from that older batch. The optimization is reachable through the public API whenever more than one circuit is proved. The in-tree Sinsemilla sequence uses equal base/equality lengths followed by a shorter square batch, so it does not trigger this defect.
F-268860	🟡 Medium	Denominator removal invalidates relation indices A supported public assignment sequence leaves related-denominator source indices stale: assign an earlier rational cell, assign an all-rational source batch, assign an equal-length related batch, and then overwrite the earlier unrelated cell with Zero or Trivial. Because the overwritten cell is not itself a marked source or target, assign_valid skips expansion and remove_denominator uses swap_remove. The source batch's last denominator is moved into the removed slot, but its source marker is lost and the recorded RelatedDenominatorBatch.source range is not repaired. For a full-length relation, evaluate subsequently indexes one past the shortened denominator vector and panics. This path is enabled in normal multi-circuit create_proof and the panic is not converted into Error; no invalid proof is emitted.
F-268861	🟡 Medium	Expansion suffix impersonates overwritten batch In multi-circuit proving, an ordinary batch that overwrites a related batch's source cells can cause materialized expansion denominators to be recorded as the newly assigned batch. assign_batch snapshots the denominator-vector length before calling assign_valid, but the first marked source overwrite invokes expand_related_denominator_batches, which appends the old related targets' denominators at that snapshot position. The rational source overwrites then update their existing slots instead of appending the new denominators. If the appended expansion count equals the overwrite batch length, record_denominator_batch accepts the expansion suffix as the immediately preceding batch. A following correct equality or square hint therefore derives from stale denominators; debug builds panic on the assertion, while release builds commit advice divided by the old denominators.
F-268862	🟡 Medium	Batched reuse rejects valid target overwrites A future related-target cell may already contain a rational assignment that the circuit intentionally overwrites. Ordinary advice assignment supports this, and the public relation API states that a correct hint is equivalent to ordinary batch assignment. In single-circuit proving the relation method falls back to ordinary assignment and succeeds, but multi-circuit proving enables optimization and requires each target slot to be exactly NO_DENOMINATOR. An existing rational denominator therefore causes Error::Synthesis before the valid overwrite is applied. The same circuit and witness consequently behave differently solely because they are included in a proof batch.
F-268863	🟡 Medium	Failed relation leaves orphan target sentinel The optimized relation loop mutates target cells one at a time before all targets and closure results have been validated. Each successful prefix target is replaced by its raw numerator and the RELATED_DENOMINATOR sentinel, but source markers and the relation descriptor are installed only after the entire loop succeeds. If a later cell is already assigned, a later closure errors, or a later value is non-rational, the method returns Err with an orphan sentinel that no descriptor can expand or evaluate. Because the public API returns a recoverable Result, a circuit that handles the error and continues can either leave the numerator unevaluated or trigger an out-of-bounds panic when reassigning the orphan cell. This state corruption is specific to the multi-circuit optimized path.

Analyzed seven files, diff 1626bde...db4beb0.

[ValarDragon]

Addressed all five findings in 5e0942e, with one focused regression test per
finding:

• F-268859: remember the actual shortened predecessor length
• F-268860: expand relationships before denominator removal
• F-268861: do not record an expansion suffix as a new denominator batch
• F-268862: fall back to ordinary assignment for rational target overwrites
• F-268863: validate and collect a related batch before mutating target cells

The full halo2-proofs library test suite and Orchard/gadget integration tests
pass. A fresh 50-pair M4/Linux comparison found no material regression in the
normal six-circuit Sinsemilla path.