axis-verifier-integration.md

axis (pattern 0) + look (pattern 17): verifier_steps() integration

status: approved 2026-09-07 — part of trident soft3-release M4

context

verifier_steps() is implemented (zheng/src/ccs/verifier_steps.rs, 62 tests pass). The function encodes a Brakedown opening as a flat sequence of m=1 CCS instances with VZ_LEN=3 ([a, b, 1]). All steps are structurally uniform — they fold.

pattern_axis() and pattern_look_inline() both return trivial_ccs() — the proof system currently does not verify Lens/Brakedown openings. This is a soundness gap: a prover can return any value for any axis or look instruction.

the core problem

Main trace CCS steps use Z_LEN=33 (16 registers at t, 16 at t+1, constant 1). Verifier steps use VZ_LEN=3. These cannot be folded into the same accumulator because fold_step() rejects mismatched num_cols as FoldError::InstanceMismatch.

Solution: two-accumulator design.

main_acc:  fold all per-row nox trace CCS steps  (num_cols = 33)
axis_acc:  fold all verifier_steps() sequences    (num_cols = 3)

The decider runs decide() on both, producing two proofs. The verifier checks both.

linkage constraint (what prevents the prover from cheating)

Without linkage, a prover could provide a valid axis_acc for a different opening than what the main trace's axis row used. The inline constraint in pattern_axis() must bind the axis row's commitment/value fields to the axis_acc binding steps.

Specifically, verifier_steps() already emits 4 eq_step binding checks:

eq_step(rc0_limb_k, commitment_limb_k)  for k = 0..3

where rc0 is the round_commitments[0] in the opening (the "outer Brakedown commitment" that the verifier checks matches the prover's committed polynomial).

For axis (pattern 0), r4 = noun polynomial commitment. The linkage is:

axis_row.r4 == axis_acc.binding_commitment

This cross-accumulator reference is the architectural crux. Options:

option A: hash-of-commitment linkage (recommended)

The main proof absorbs axis_acc.witness_commitment into the Fiat-Shamir transcript. The verifier independently computes the same commitment from the axis opening it verifies. No additional inline constraint in pattern_axis() — the shared transcript enforces linkage.

Advantages: no new pattern_axis() constraint, no nox trace change, works now. Limitation: implicit linkage via Fiat-Shamir; not an explicit circuit constraint.

option B: inline commitment constraint

Add r7..r10 to the axis trace row to carry the Brakedown commitment bytes (4×8 bytes = 32 bytes = 4 Goldilocks elements). Then pattern_axis() can verify:

r7 = commitment_limb_0
r8 = commitment_limb_1   (wait: r8 = budget_in, CONFLICT)

But r8 = budget_in, r9 = budget_out. Reserved slots r10-r13 are free for axis (4 regs = 32 bytes = exactly one Brakedown commitment).

So with nox emitting commitment in r10-r13:

fn pattern_axis() -> CCSInstance {
    // axis_commitment_limb_k = r10+k_t (k = 0..3)
    // eq_step links these to axis_acc's binding steps
    // 4 eq constraints between r10..r13 and the axis_acc binding commitment
}

This requires a nox trace update (emit commitment in r10-r13 for pattern 0). Advantage: explicit verifiable circuit constraint.

current nox trace layout for axis (from nox/specs/trace.md)

r4  = noun polynomial commitment  — Lens commitment to the object noun polynomial
r5  = axis index
r6  = evaluation point
r7  = result value
r10-r15 = 0 (reserved, unused)

The commitment (r4) is already in the trace. The opening proof itself is NOT in the trace (unlike look/17 which embeds proof elements in r7/r10/r11).

For axis, since r4 = commitment already, option A (Fiat-Shamir linkage via r4) is sufficient without any nox trace change.

implementation plan

phase 1: two-accumulator infrastructure (no nox change needed)

src/types.rs: Add AxisAccumulator or reuse Accumulator with a flag. Actually: Accumulator already works for VZ_LEN=3 steps; just use a second instance. No new type needed.
src/ccs/mod.rs: Add build_axis_steps_from_trace(trace, openings). Signature:
```
pub fn build_axis_steps_from_trace(
    trace: &[TraceRow],
    openings: &[(Commitment, Vec<Goldilocks>, Goldilocks, Opening)],
) -> Vec<(CCSInstance, CCSWitness)>
```
Scans for rows with r0 == 0 (axis), calls verifier_steps() for each, flattens into one sequence. The openings slice is prover-provided and parallel to the axis rows in order.
src/lib.rs: The commit() entry point needs to:
- Execute nox → trace
- For each axis row, perform the Brakedown opening and collect (commitment, point, value, opening)
- Build main_steps via build_ccs_from_trace()
- Build axis_steps via build_axis_steps_from_trace()
- Fold main_steps → main_acc, fold axis_steps → axis_acc
- Return both accumulators
src/folding/decide.rs: Extend decide() or add decide_pair() that takes (main_acc, axis_acc) and returns (main_proof, axis_proof).
src/spartan/verifier.rs: Extend verify() or add verify_pair().

phase 2: inline pattern_axis() linkage constraint (option A)

pattern_axis() encodes the budget constraint only (inline linear):

r9_t = r8_t - 1  →  r9_t - r8_t + 1 = 0

Using existing select_matrix on reg_t(9), reg_t(8), CONST_IDX:

fn pattern_axis() -> CCSInstance {
    let m_r9 = select_matrix(reg_t(9));
    let m_r8 = select_matrix(reg_t(8));
    let m_c  = select_matrix(CONST_IDX);
    build_ccs(vec![m_r9, m_r8, m_c], vec![
        (vec![0], Goldilocks::ONE),  // +r9
        (vec![1], neg_one()),        // -r8
        (vec![2], Goldilocks::ONE),  // +1 (= +const)
    ])
}

The Brakedown opening correctness is guaranteed by the axis_acc; the Fiat-Shamir transcript of the main proof absorbs both commitments, providing implicit linkage.

phase 3: option B inline commitment constraint (requires nox update)

Deferred. Requires nox to emit commitment bytes in r10-r13 for pattern 0. If nox adds this, pattern_axis() can be upgraded to 4 explicit eq constraints that bind the axis row's commitment to the axis_acc binding steps.

what blocks each phase

phase	blocker
1 (two-acc infra)	none — can implement now
2 (budget constraint)	none — can implement now
3 (option B commitment constraint)	nox trace update for axis r10-r13
look (pattern 17)	BBG_root in Statement (blocked on bbg)

implemented (2026-09-07, branch feat/axis-openings)

The repo had grown past this plan's draft state before implementation began: build_axis_steps_from_trace(), the pattern_axis() budget constraint, per-CCS-structure accumulator groups in commit() (a generalization of the two-accumulator design — one group per distinct instance, so main/hash/axis/ look each land in their own accumulators), and the full look (17) binding suite were already in place. What this milestone added:

1. axis trace bindings (`rs/src/ccs/mod.rs`)

For every prover-active axis row (r11-r14 non-zero, i.e. the executor's CallProvider::axis_commitment() was live), build_axis_steps_from_trace() now emits eq steps binding the opening to the trace:

commitment limbs ↔ r11-r14
evaluation point ↔ axis_eval_point(r5) (binary path of the axis address)
opened value ↔ r7 (result particle)

A strictness gate rejects at commit time (CommitError::AxisBinding). This settles the axis opening derivation: point = binary path of r5, value = r7, commitment = r11-r14. Interpreter mode (NullCalls, registers zero) keeps opening-only behavior per specs/trace.md.

2. option A linkage (`rs/src/lib.rs`, `rs/src/folding/decide.rs`, `rs/src/transcript.rs`)

linkage_digest = hemera hash over group count + every group's witness commitment in order. commit() folds all groups first, computes the digest, then decides each group with the digest absorbed (domain \x08linkage) right after the statement. verify() recomputes the digest from the proof's own groups and absorbs identically. Demonstrated: without the digest, an axis group spliced from another valid proof verifies (test observed accepting before the change); with it, splicing breaks every group's Fiat-Shamir chain (verify_rejects_spliced_axis_group).

3. zero-error rule for degree-1 groups (`rs/src/lib.rs::verify`)

Error is linear in the witness for degree-1 CCS, so satisfied steps fold to exactly zero error. verify() now rejects (VerifyError::LinearErrorNonzero) any all-linear group carrying a non-zero error term — closing the relaxed- fold loophole where a malicious prover folds an unsatisfied binding step and reports its honest error. Negative tests fold a wrong-commitment binding and a forged-result binding directly (bypassing the commit gate) and are rejected at verify time.

surfaced by the zero-error rule: pattern_quote fix

The quote constraint was stale (r5_{t+1} = r4_t, cross-row) and no real trace satisfied it — the relaxed fold masked the violation. Fixed to the spec's r7 = r4 (same row). Any linear pattern that real traces violate would now surface the same way; compose (2) and cons (3) still use the old cross-row wiring (r5_{t+1} = r3_t) and are untested against real traces — flagged for the same treatment when their e2e coverage lands.

known limitation (accepted by option A)

The eq-step witnesses binding opening ↔ trace registers are prover-supplied; no cross-accumulator constraint forces them to equal the main accumulator's committed register values. A fully malicious prover who omits or rewrites binding steps is not caught by the verifier — the linkage digest binds groups to each other, not step content to the main trace witness. Closing this requires option B (commitment limbs constrained inside pattern_axis(), nox already emits r11-r14) plus recursion over the step count, or a permutation argument across accumulators. Tracked as the residual gap for the recursion milestone.

hash (pattern 15) — implemented 2026-09-07, branch feat/hash-openings

finding: hash carries no opening

Evidence: nox specs/trace.md pattern 15 register map holds Poseidon2 sponge state (r4-r7, r10-r13), round index (r14), digest and result — no commitment or opening registers; nox/rs/patterns/hash.rs writes exactly that. Verification is in-circuit (particle::partial_round_ccs, 16-row degree-2 CCS per partial round) driven by HashAux — the "hash opening derivation" of this plan's title is a misnomer. The prover-supplied surface is the HashAux rate, and it was unbound: full-round pairs use trivial_hash_ccs (no constraints) and the capacity/y witness columns are injected from a replay of whatever rate the prover claims.

what landed

spartan relaxed-path fix (prerequisite): two challenge/row-bit pairing bugs made prover and verifier disagree on any m>1 group whose error vector or matrix activity extends past row 0 — e_claim used MSB-paired evaluate_multilinear against the prover's LSB-paired eq_evals weighting, and w_combined row weights used unreversed challenge order against MSB-first-folded matrix_evals. Satisfied witnesses collapse all row activity to row 0 (bit-reversal symmetric), which hid both. A tampered rate was "rejected" only by these bugs. Fixed both sides; regression tests pin the fold convention and the relaxed round-trip.
hash trace bindings (rs/src/ccs/hash_binding.rs): degree-1 eq steps bind every block row to the replay of the claimed rate — state limbs and round index per round row, output digest and 24-sentinel on the squeeze row. Strictness gate CommitError::HashBinding. The steps fold into the shared eq-step group and inherit option-A linkage and the zero-error rule — verified by tests (tampered rate, swapped rate, forged digest folded past the gate, spliced hash binding group).
compose (2) and cons (3) fixed — same bug class as pattern_quote: constraints wired to registers no real trace sets (r5_{t+1} = r3_t; nox leaves compose r3 = 0). Under the zero-error rule every honest compose/cons program committed and failed verification. Both are trivial_ccs until cross-row / particle-identity wiring lands; e2e round-trips for real compose and cons programs now guard the class.

joy wiring follow-up (2026-09-07, branch feat/proof-serde)

Wiring the prover into joy surfaced that the WHOLE arithmetic pattern family (add 5, sub 6, mul 7, eq 9, branch 4) still encoded the stale register map (operands r3/r4, result in the next row's r5). Real trident programs failed verify on the degree-1 patterns (zero-error rule) while mul/eq/branch violations were accepted SILENTLY as relaxed degree-2 claims. All five re-encoded against specs/trace.md + real traces; real_traces_satisfy_pattern_family (real nox programs, both eq outcomes, both branch arms) now guards the class. It also caught nox zeroing r10 on success rows (branch selector clobbered — nox 713d04e) and nox's std feature silently switching to the arena-forking par_binary executor (now opt-in behind 'parallel' — nox e8cad47). Axis openings are now owed only by prover-active rows — interpreter rows (every trident variable reference) carry no commitment and owe no opening.

spec-code drift found (nox specs/trace.md)

pattern 15 squeeze: spec claims r9 = r8 - 25; nox records r8 before the body sub-formula (observed r9 = r8 - 26 for [15 [1 s]])
pattern 2: spec claims r3 = result particle and r9 = r8 - 1; nox leaves r3 = 0 and records post-continuation budget (observed r9 = r8 - 4)
pattern 3: budget drift likewise (observed r9 = r8 - 3)
patterns 5-7: budget claim r9 = r8 - 1 does not hold either — r8/r9 bracket the bound-partitioned sub-evaluation (observed r8=3, r9=0 on a real add row); axis rows DO satisfy r9 = r8 - 1

Per the spec-first rule these need resolution in nox specs (or code) — out of zheng's scope, flagged for the nox milestone.

hash residual (same class as axis option A)

The rate ↔ input-particle link stays prover-claimed: r15 holds the particle id, its structural digest is not in the trace. Closing requires recursion over the digest computation or a nox trace change emitting the digest limbs — the exact analog of the axis r11-r14 option-B upgrade.

remaining

phase 3 / option B: explicit r11-r14 constraint in pattern_axis() (nox already emits the limbs; needs per-row constant matrices at fold time)
hash: full-round in-circuit CCS (transitions k∈{0..2,19..23} still trivial — the replay bindings pin them to the claimed rate, the circuit itself does not); rate ↔ input digest binding (see residual above)
compose/cons: cross-row result wiring (blocked on wiring infrastructure)
look (17): DONE 2026-09-07 — Statement.bbg_root public input, root eq-binding + LookBinding gate, full-pipeline e2e (see look-bbg-root.md). The option-A residual (prover-supplied eq witnesses) applies to look as to axis and hash.

option-B rationale (axis-options-comparison.md, deleted for the .claude budget): A and B tied on soundness and speed; A won on zero nox coordination. B's path stays: pattern_axis gains 4 eq constraints on r11-r14.

wall we did not see: proof size — universal step CCS (zheng#8)

what the spec says (specs/constraints.md §"the combined constraint"): one step relation C(t) = Σ_p selector_p(r0_t) · C_p(t) over the 18 patterns — ONE CCS structure for every trace row, therefore ONE HyperNova accumulator, ONE decider, ~2 KiB per proof regardless of program.

what commit() does: builds a distinct CCS instance per pattern (and per Poseidon2 round constant set, per binding run) and folds sequential runs — a new group every time the instance changes along the trace. Groups = number of structure switches, not even number of structures. Measured: add 3 groups, hp 12, one hash 23, a depth-32 Merkle path 1343 groups → 2.67 MB. Per group ~1.7 KiB holds; the count is the bug.

two steps, in order:

Group by structure, not by run (small, pure commit() change). Partition instances by exact CCSInstance equality across the whole trace (BTreeMap keyed on the instance), fold each key once. fold_step already requires acc.committed_instance == instance, so soundness is unchanged; the linkage digest covers every group as before (verify recomputes it from the proof). Expected: Merkle-32 from 1343 groups to ~30 (18 patterns × hash-round variants + binding shapes) → ~50 KB. This alone lifts hash-heavy programs from MB to tens of KB.
The universal step CCS (the spec). One instance for all Layer-1 rows: pattern constraints multiplied by a selector on r0. NOT Lagrange over 18 values (degree +17): add 18 one-hot selector columns s_0..s_17 to z (Z_LEN 33 → 51, with Σ s_p = 1, s_p·(r0−p) = 0), so s_p · C_p raises degree by one. Poseidon2 rounds: the round constant becomes a witness column selected by the round index (r14) instead of baking constants into the matrices — one instance for all 25 rows of a hash block. Binding eq-steps (VZ_LEN=3) stay a second, single accumulator (the original two-accumulator design) — or are widened into the universal row with their own selector. Result: 2 groups (main + bindings), ~4 KB per proof, constant in program size. Decider cost per the spec's ~825 constraints. This also makes the option-B residual (binding steps ↔ main witness) expressible: the binding can reference the universal row's committed registers directly.

effort: step 1 — one session, mechanical, no spec change. step 2 — 3–5 sessions (selector columns, per-pattern CCS rewrite into a shared matrix set, round-constant witnessing for hash, new negative tests that a wrong selector fails). specs/constraints.md gains the one-hot form.

acceptance: Merkle-32 proves into ≤ 8 KB; group count is independent of trace length; every existing negative test still rejects.

step 1 landed (2026-09-09, branch fix/group-by-structure, 0.2.2): commit() keys accumulators on exact instance equality, first-occurrence order, own fold transcript per group. Measured with joy: hello 3→2 groups (3623 B), two-divine 12→5 (8525 B), one hash 23→22 (50204 B), Merkle-32 1343→22 (56886 B). The 22 = 17 Poseidon2 shapes (16 partial-round constant sets + the trivial full-round shape) + main patterns + the one eq-step group; group_count_independent_of_trace_length pins it.

step 2 landed (2026-09-09, branch feat/universal-step-ccs, 0.3.0): ccs/universal.rs — one instance, m = 64, 15 slot matrices, 6 fixed product shapes, degree ≤ 4; selectors as designed plus 25 round selectors with Σ u_k = s_15 (one linear row gives both "one round on hash rows" and "no round elsewhere", so π/κ are exclusive gates and the Poseidon2 terms cannot leak into other patterns' rows); rc as a witness column bound by rc = Σ RC_j·u_j. Transcript replays and root chains are universal rows (r0 = 15 layout). TraceProof { universal, binding }, instances verifier-derived, never on the wire. Measured: hello 2388 B, two-divine 2440 B, hashone 4496 B, Merkle-32 4503 B (proof bytes; joy's artifact adds statement + meta, 11176 B for Merkle-32 because meta.assembly carries the 6.5 KB formula text). No wall was hit.

Zero-error rule under the universal instance. No verifier-side equivalent exists: every universal row is a gated product, so an honest fold carries non-zero cross-term error and e cannot distinguish a violated row. The relaxed fold as implemented never had verifier-side soundness for degree ≥ 2 (the mul/eq/branch "silently accepted" finding above); 0.3.0 makes this explicit — commit() gates every row (StepUnsatisfied), the binding group keeps the zero-error rule, and specs/decider.md §soundness records the residual. Closing it is the recursion milestone: a verifier-checked fold.

Residuals carried forward. Full Poseidon2 rounds still unconstrained in-circuit (bindings pin them to the replay); capacity columns are not chained between consecutive rows; compose/cons/look carry no in-row constraint; bit patterns lack block decomposition sums; inv checks only the final-row inverse; the option-A residual (prover-supplied binding witnesses) is unchanged. cybergraph, mudra and inf pin older zheng versions by path (0.2, 0.1.2, 0.1.2) and will need bumps when they next build with the prove features.