Chunk-Freivalds and the Dispute Calculus: Sub-Recompute Verification of Integer Transformer Inference with a 288-Byte Settlement Receipt

Research corpus codename: NOOSPHERE.

Date: 2026-07-10 Provenance: Compiled entirely from three lab artifacts — kt-verification-ladder/README.md (cycle-model square leaf), nel-dispute-ladder/README.md (rectangular chunk leaf + layer dispute calculus), zkvm-port/README.md (real RISC Zero prover) — every number below was re-verified against its source on 2026-07-10; unless a label says otherwise, all values carry that date.

Abstract

Recomputing a disputed T-token decode chunk of an integer transformer layer costs O(TKN) multiply-accumulates per GEMM. We show the chunk can instead be verified: a committed C32/C8 witness passes an exact mod-2^64 Freivalds check in O(KN + TK + TN) cycles, so for fixed weights the per-token dispute cost falls as ~1/T. Measured on a deterministic RV32IM-subset cycle model, the square INT8 leaf verifies at 1.8669 cycles/MAC MEASURED, cycle-model versus 2.7198 cycles/MAC for direct in-VM recompute; the rectangular decode-chunk leaf at (K,N)=(256,256) follows the law 958,090/T + 11,602 cycles/token essentially exactly (residual ≤ 2 cycles/token at the held-out T). Composed across all 9 GEMM leaves plus exact-integer nonlinearity recompute of a Qwen2-0.5B-class decoder layer, full-chunk dispute verification is 12.67× cheaper than direct recompute at T=128 MODELED, instruction-exact, gated cycle-exact against every measured shape. The dispute ladder descends token → layer → op → leaf, and the leaf terminates in a real proof: the same statement ported to RISC Zero (risc0 3.0.5) produces a Groth16 receipt of dispute_settlement_bytes = 288 that settles one challenged span out of S = 8192 committed spans — 0.0352 settlement bytes per span MEASURED, real prover. Per-span soundness is 2^-64 THEORY: 2-adic spacing argument, post-commit beacon required. The dispute ladder is a cycle-model harness, not a production lane; the Groth16 receipt is a real artifact.

Claims

Label discipline (ch08 §5.4): MEASURED = retired cycles or bytes from actual runs; MODELED = closed-form models gated cycle-exact (diff = 0) against every measured run; THEORY = proven or argued, not yet adversarially executed at scale. Denominators travel with numerators. All values dated 2026-07-10.

• C1 MEASURED, cycle-model. A stock RV32IM-style ZKVM guest verifies a committed 32³ INT8 matmul + requant witness in 61,175 cycles = 1.8669 cycles/MAC (61,175 / 32,768 MACs), versus 2.7198 cycles/MAC for direct in-VM recompute — a 1.457× verifier advantage at the smallest measured dimension, scaling as n^1.997 (verifier) versus n^2.958 (recompute) on the 32³→64³ two-point probe. Source: kt-verification-ladder/README.md (final valid line: autoresearch run #27).
• C2 MEASURED, cycle-model. The rectangular decode-chunk leaf Y[T,N] = X[T,K]·W[K,N] verifies in O(KN + TK + TN) cycles. Per-token verifier cycles at (K,N)=(256,256) fit 958,090/T + 11,602 — measured 131,363 / 71,481 / 41,542 cycles/token at T = 8/16/32 (T8/T32 ratio 3.16×). At (K,N)=(128,128): 240,471/T + 5,799, measured 35,858 / 20,827 / 13,313. A is the weight-dependent fixed cost per chunk; B is the per-token marginal. Source: nel-dispute-ladder/README.md §1.
• C3 MODELED, instruction-exact + spec-derived. Composing Freivalds verification of all 9 GEMM leaves of one canonical integer decoder layer (hidden 896, GQA 14/2, head_dim 64, MLP 4864, context 1024) with direct recompute of every nonlinearity, full-chunk dispute costs 440,897,006 cycles at T=128 versus 5,586,651,389 for monolithic recompute — 12.67×. Per-token dispute cost falls from 29,362,503 cycles (T=8) to 3,444,507 (T=128): the measured 1/T law survives composition. GEMM cycle models are gated to diff = 0 against every measured VM run; nonlinearity referee constants are hand-derived instruction counts MODELED, spec-derived, 2–18% of the total. Source: nel-dispute-ladder/README.md §3.
• C4 MEASURED, real prover. The leaf statement ported to RISC Zero (risc0 3.0.5, WSL2, CPU prover, run #192) proves in one segment (zkvm_real_total_cycles = 131,072 at SEGMENT_PO2=18; 96,991 user + 22,668 paging cycles) and settles with a Groth16 receipt of dispute_settlement_bytes = 288 (256 B seal + 32 B journal claim). A mixed-radix Merkle dispute wrapper commits S = 8192 real boundary spans and proves only the challenged one (dispute_zk_leaf_proofs = 1, implied proof-count reduction 8192×), giving dispute_effective_settlement_bytes_per_span = 0.0352 (288 / 8192) and 16.0000 effective total cycles per committed span. Conservative full verifier interface: 354 B (0.0432 B/span). Source: zkvm-port/README.md.
• C5 THEORY. Per-span soundness is 2^-64: two independent 32-bit challenge vectors over Z/2^64, where the 2-adic spacing argument (d_J ≠ 0 int32 ⇒ solution classes spaced ≥ 2^33 apart, at most one sampled r_J in [0, 2^32) can satisfy the congruence) gives 2^-32 per vector. Requires a post-commit beacon; offline-grindable challenge derivations are broken and were flagged (kt-ladder runs #7–#12). Per layer-chunk: ~2^-60 by union bound (7 leaves at 2^-64, 2 int16-operand P·V leaves at 2^-62).

Non-claims. No production lane: the dispute ladder is a deterministic RV32IM-subset cycle-model harness (1 cycle/retired instruction, SHA-256 precompile at 68 cycles per 64-byte block), not a proving service. No wall-clock prover claims at production dimensions (the dim-4096 figure of 0.014559 cycles/MAC is a trace-cycle extrapolation, not a proof-time claim). No GPU kernels. Cross-leaf glue, embeddings, lm_head, tokenizer, sampler, DA economics, and proof recursion are out of scope. The zkvm-port Groth16 wall-clock (~315 s MEASURED, noisy) is a 32-thread CPU figure for one 32³ leaf.

Construction

Rung 0 — exact witness (KT-1). The consensus object is a canonical INT8 span: C32[i,j] = Σ_k int32(A[i,k])·int32(B[k,j]), then C8 = sat8((int64(C32)·mult + 2^(shift-1)) >> shift). Integer accumulation is associative and commutative over the exact accumulator, so every honest schedule produces bit-identical C32 — measured 0 mismatches across adversarial schedules including split-K randomized atomic commit order, while FP16 (3/3 at K=32) and biased FP32 (3/3 at K=8192) negative controls diverge MEASURED. At layer scale, 4/4 adversarial schedules produce the identical layer_digest = b4d26b032763d91a, and an fp32 shadow with dequantized operands diverges 4/4 MEASURED. Exactness is what makes a dispute decidable by hash equality.

Rung 1 — the chunk-Freivalds leaf. The guest proves the check, not the compute. Flat transcript root = SHA-256(A || B || C32 || params) with beacon + miner payout key in params (commit-then-challenge on C32; 16-bit dimension packing, injective for all dims < 2^16); challenge block 0 is the root itself; two full-word challenge vectors expanded via SHA-256(root || counter32le). Verifier computes s = W·r once per chunk (O(KN), ~13.5 cycles per K·N element plus SHA over the weight bytes — the A term of the 1/T law), then checks X·s − C32·r ≡ 0 mod 2^64 row-wise with exact RV32 carry chains and every C8 element against the exact scaled-multiplier rounded quotient (6 cycles/element). No prime-field emulation; no range-check pass — the 2-adic spacing argument accounts for wraparound.

Rung 2 — the dispute calculus. A challenged decode chunk bisects token → layer → op → leaf. Every GEMM in the layer is a rectangular leaf (QKV fused as one [T,896]×[896,1152] leaf; attention leaves batch 7 query heads per KV group so the shared K/V cache amortizes as the B operand; score leaves are C32-only since integer softmax consumes int32 scores directly). Every non-GEMM op (RMSNorm with pinned integer sqrt — 1,806/1,806 exact vs floor(sqrt(.)); RoPE with committed Q1.15 LUT; integer softmax with committed exp2 LUT and load-bearing P ≤ 32767 bound; SiLU LUT; saturating residual) has an exact integer spec cheap enough to direct-recompute in the referee (2–18% of dispute cycles). In a real bisection the referee proves one leaf, not all nine: the worst-case single-leaf obligation is the up/gate leaf at 64.7M (T=8) to 82.1M (T=128) cycles MODELED.

Rung 3 — the real receipt. The identical leaf statement (same instance bytes, seed 20260706) runs as a RISC Zero guest: one SHA-256 accelerator pass binds the transcript, REPS=2 Freivalds in wrapping u64, exact requant, and a 32-byte journal claim SHA-256(domain || span_commitment || params_context || accept). Proof mode reconstructs an in-guest mixed-radix Merkle boundary (six 4-ary SHA levels + one binary root) over 8192 distinct generated canonical spans and journals settlement_claim = SHA-256(domain || challenged_span_id_le16 || public_boundary_root). The Merkle path is a private receipt witness, not calldata: public settlement is the 256 B Groth16 seal plus the 32 B claim, total 288 B, regardless of S.

flowchart TD
    A["TokenClaim divergence"] --> B["bisect: token"]
    B --> C["bisect: layer"]
    C --> D["bisect: op"]
    D --> E["one challenged leaf"]
    E --> F{"leaf kind"}
    F -->|"non-GEMM op"| G["exact integer recompute, hash equality"]
    F -->|"GEMM leaf"| H["chunk-Freivalds check mod 2^64, soundness 2^-64 per span"]
    G --> I["referee verdict on the single leaf"]
    H --> I
    I --> J["288 B Groth16 settlement: 256 B seal + 32 B journal claim"]

Figure 1 — The dispute descent: a challenged decode chunk bisects token → layer → op → leaf; the referee proves only the single challenged leaf — exact integer recompute for non-GEMM ops, chunk-Freivalds for GEMM leaves — and settles with the 288 B Groth16 receipt. MODELED — calculus; MEASURED, real prover — receipt 2026-07-10.

Results

Table 1 — square leaf, 32³ INT8 span MEASURED, cycle-model, 2026-07-10 (source: kt-verification-ladder/README.md, run #27):

Table 2 — rectangular decode-chunk leaf grid MEASURED, cycle-model, 2026-07-10 (source: nel-dispute-ladder/README.md §1; gates at every shape: honest accept, C32+1 tamper reject, C8 bit-flip reject, predictor diff = 0):

1/T fits (residual ≤ 2 cycles/token at the held-out T): (256,256): 958,090/T + 11,602; (128,128): 240,471/T + 5,799. The per-MAC number is shape-dependent by construction — kt-ladder's square 1.8669 c/MAC and this grid's 0.634–2.189 c/MAC are one phase law at different (KN + TK + TN)/TKN mixes.

xychart-beta
    title "Per-token dispute verifier cost at (K,N)=(256,256) - fit 958090/T + 11602 cycles/token"
    x-axis "chunk size T (tokens)" ["8", "16", "32"]
    y-axis "verifier cycles per token" 0 --> 140000
    line [131363, 71481, 41542]

Figure 2 — The 1/T law at (K,N)=(256,256): measured per-token verifier cycles 131,363 / 71,481 / 41,542 at T = 8/16/32, fit 958,090/T + 11,602 (residual ≤ 2 cycles/token at the held-out T). MEASURED, cycle-model 2026-07-10.

Table 3 — full-layer dispute composition, Qwen2-0.5B-class decoder layer, context 1024 MODELED, instruction-exact + spec-derived, 2026-07-10 (source: nel-dispute-ladder/README.md §3):

Whole model (24 layers, embeddings/lm_head out of scope): ~207M dispute cycles/token at T=32 MODELED. Per-chunk soundness ~2^-60 union bound THEORY.

xychart-beta
    title "Full-layer dispute vs monolithic recompute speedup by chunk size T"
    x-axis "chunk size T (tokens)" ["8", "16", "32", "128"]
    y-axis "direct recompute cycles / dispute cycles" 0 --> 14
    bar [1.55, 2.87, 5.10, 12.67]

Figure 3 — Composed full-layer dispute advantage grows with chunk size: direct/dispute cycle ratio 1.55× / 2.87× / 5.10× / 12.67× at T = 8/16/32/128 (Table 3); the measured 1/T law survives composition. MODELED, instruction-exact + spec-derived 2026-07-10.

Table 4 — real-prover leaf and settlement, RISC Zero risc0 3.0.5, run #192 MEASURED, real prover, 2026-07-10 (source: zkvm-port/README.md):

The 288 B receipt is a real RISC Zero artifact produced and verified by the harness gates (honest accept, C32/C8 tamper rejects, boundary-root/span-id match, ~30 wrapper rejection gates). The context it settles — which leaf of which layer of which chunk — is the cycle-model calculus of Tables 2–3; wiring both into one live lane is the open build item, recorded in the competitive audit.

Falsifiers & kill thresholds

A kill is a deliverable. These are the standing tripwires, verbatim from the artifacts:

1. Predictor drift = instant kill of C3. The bench fails if either closed-form GEMM model is off by even 1 cycle at any measured shape; a future VM run at a larger shape (e.g. (8,512,256), ~4M cycles) missing predict_cycles falsifies the target-dim composition table.
2. One schedule-dependent bit = kill of the exactness premise. A single adversarial-schedule digest mismatch at span or layer scale breaks KT-1 and with it hash-equality dispute decidability.
3. Nonlinearity constants are spec-derived. If a real measured referee guest costs 2× the hand-derived counts, the T=32 total moves ~7% and T=128 ~18%; the 12.67× headline degrades visibly in the split columns. Writing that guest is the next rung.
4. Soundness THEORY tripwires: a C32/C8 lie accepted above the claimed Freivalds probability; a post-commit replay/grinding route producing reusable challenges; the statistical witness multiplicity (2^-64) breaking an amortization argument that assumes exact uniqueness. Beacon must be real post-commit randomness — the harness constant 0x0BEAC0DE only models it.
5. Real-backend erasure. A named ZKVM backend showing the trace-cycle proxy misleading enough to erase the dispute-leaf advantage. Partially retired: the RISC Zero port measures 96,991 user cycles against the model's 61,175 hand-tuned floor (1.59× compiler overhead) — the advantage survives, and the receipt is 288 B.
6. Decomposition failure. Real model layers that cannot be decomposed into canonical fixed-point leaves without unacceptable accuracy or DA cost kill the calculus above the leaf.

Reproduction

All harnesses are stdlib-only Python ≥ 3.10, fixed seeds, exit 0 iff every gate passes; each prints its numbers as METRIC name=value lines.

# Square leaf + PoUW tables — cwd: kt-verification-ladder
bash autoresearch.sh                 # gates + METRIC lines; primary: METRIC zk_cycles_per_mac=1.8669
python harness/pouw_analysis.py      # mining-model tables (phase sums gated to reproduce the verifier bit-exactly)

# Rectangular leaf + layer spec + dispute calculus — cwd: nel-dispute-ladder
bash autoresearch.sh                 # or: python harness/bench.py   (~70 s CPython 3.10)

# Real RISC Zero prover + Groth16 settlement — cwd: . (repo root)  (needs WSL Ubuntu + rzup, risc0 3.0.5)
bash zkvm-port/autoresearch.sh       # gates + one real proof; METRIC dispute_settlement_bytes=288

Expected anchors: METRIC zk_cycles_per_mac=1.8669, METRIC zk_total_cycles=61175, METRIC zk_soundness_bits=64 (kt-ladder); the Table 2/3 values (nel-dispute-ladder); zkvm_real_total_cycles=131072, dispute_settlement_bytes=288, dispute_effective_settlement_bytes_per_span=0.0352 (zkvm-port).

Related work

What is not new: Freivalds' check is classical; Fiat–Shamir hash-to-challenge is standard; integer determinism is not a new algorithm. The contribution is the composition — an exact-witness spec that makes a cheap ZKVM Freivalds leaf meaningful inside an optimistic dispute ladder — plus reproducible harnesses and a real receipt.

• SafetyNets (Ghodsi et al., 2017, arXiv:1706.10268) — verifiable DNN inference via interactive proofs; outsourced-verification target, not an L1 dispute leaf.
• Agatha (Zheng et al., 2021, arXiv:2105.04919) — closest prior art: optimistic smart-contract DNN computation with graph pinpointing; this work narrows the disputed object to an exact matmul leaf terminating in a ZK receipt.
• Gensyn Verde/RepOps — bitwise-reproducibility motivation; this work avoids pinning FP operation order by making the witness an integer span.
• ORA opML (github.com/ora-io/opml) — optimistic ML with VM fault-proof bisection; here the matmul leaf terminates directly in a subcubic ZK arithmetic receipt.
• Kailua (github.com/risc0/kailua) — same optimistic-by-default, ZK-on-dispute pattern, specialized here to inference spans rather than OP Stack traces.
• Proof of Necessary Work (Kattis–Bonneau, ePrint 2020/190) and Ofelimos (Fitzi–Kiayias–Panagiotakos–Russell, ePrint 2021/1379) — PoUW with usefulness structurally ≤ 1; the verification-based puzzle here has Θ(n) leverage (conjecture status, see kt-ladder README).
• Nock zkVM framework (Kattis–Klatt–Quirk–Allen, ePrint 2025/1110) — the circuit-compilation framework behind Nockchain-style zkPoW; contains no inference-puzzle economics. Dossiers: nockchain-octra-ai-research-handoff/L1-plans/NOCKCHAIN/NOCKCHAIN-claims-vs-reality.md, .../NOCKCHAIN-architecture.md.
• Pearl cuPOW — GPU matmul PoW without a verification asymmetry story: research/08-pearl-matmul-pow.md, digest noosphere/research/02-pearl-cupow-kernel-digest.md.
• Octra HFHE — verification via homomorphic encryption rather than optimistic dispute; different trust model, more running privacy code: noosphere/research/01-octra-hfhe-consensus-digest.md.