Multi-table proving: one proof for heterogeneous hash batches - #21
Closed
rothblum wants to merge 154 commits into
Closed
Multi-table proving: one proof for heterogeneous hash batches#21rothblum wants to merge 154 commits into
rothblum wants to merge 154 commits into
Conversation
Adds prove_assist/verify_assist: a 2(m+1)-round degree-2 sumcheck proving
β = f̂_t(z_row, z_col, i*) = Σ_{(c,d)} W(c,d)·ĝ(z_row, i*, c, d) directly as
one eq(z_col,·)-weighted claim over only the cumulative-height variables,
with (z_row, i*) pinned inside the branching program. No per-column values,
no batching randomness (the statement is a fixed scalar); columns sharing a
(t_{y-1}, t_y) pair — zero heights — are collapsed up front. Variables bind
in layer-interleaved order (c_0, d_0, c_1, …) so the naive per-round DP
prover can later be swapped for Lemma 4.6 prefix/suffix streaming without
changing the transcript. Matches SP1 Hypercube's slop/jagged design, minus
its {0, ½, 1} round interpolation (no 2⁻¹ in char 2) — we reuse the
codebase's (G(1), G(∞)) encoding.
g_hat_eval generalizes to field-valued height coordinates (g_hat_eval_cd),
which is both the verifier's final one-shot ĝ(ρ) evaluation and the naive
prover's per-round evaluator. prove/verify gain *_with_assist companions.
runtime_assist_m25 (m=25, 2^12 uniform columns, M4 Max): direct f̂_t 10.6ms
vs assist verifier 0.79ms (13.4×, and no height-dependent branching);
naive assist prover 126ms; proof 1680 B.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Replaces the naive per-round DP in prove_assist with the paper's Lemma 4.6
"assist with storage" streaming: per-layer BP transition matrices with
(z_row, i*) pinned (shared across columns; entries are eq4 sums, no extra
mults), per-column suffix vectors S_y[l] from one O(m) backward pass (whose
[0][INITIAL] entries give beta for free), and a shared prefix row vector
b_l = e_I·M_0(rho)···M_{l-1}(rho) advanced once per layer. Each round message
is then two 4-element dot products per column: O(m·2^k) total vs the naive
O(m²·2^k). The layer-interleaved variable order chosen earlier makes this a
drop-in: the transcript is bit-identical, enforced by the new
assist_streamed_matches_naive test (naive prover retained as reference).
runtime_assist_m25 (m=25, 2^12 columns, M4 Max): streamed prover 5.3ms vs
naive 145ms (27x) — now below the 10.8ms direct f̂_t evaluation it delegates;
assist verifier 0.76ms (14.2x vs direct); proof unchanged at 1680 B.
SP1 Hypercube leaves this optimization as a TODO (their block variable order
would not support it transcript-compatibly).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Four transcript-invariant optimizations to the streamed assist prover (assist_streamed_matches_naive still enforces bit-identical transcripts): - One column pass per layer instead of four: the pass folds the previous layer's challenges into the running weights and accumulates four bucketed sums B[cbit + 2*dbit] = sum we*S; the c-round message is dots of the shared u[cd] row vectors against the buckets, and the d-round needs no second pass at all - M_l(rc, x) is a linear combination of the boolean matrices, so folding rc into the u's and B's yields it. 26 parallel sections instead of 104, ~6 mults/column/layer instead of ~20. - Sparse transition rows: the addition check forces the index bit once a is chosen, so each row of a layer matrix has exactly two (eq4 index, next state) entries, layer-independent. Suffix step drops 16 -> 8 mults; the dense LayerMats materialization disappears entirely. - Flat layer-major suffix storage: one allocation, each round streams one contiguous 256KB row instead of gathering from 2^k per-column Vecs; built with one parallel streaming pass per layer. - Explicit par_chunks(256) granularity, matching the module's kernel style. runtime_assist_m25 (m=25, 2^12 columns, M4 Max): streamed prover 2.5ms (was 5.3ms; naive 132ms, 54x). Verifier and proof unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
End-to-end jagged reduction at m=23 (2^30 bits / 128 = 2^23 F128), n=11, k=12, best-of-3: sumcheck prover 9.2ms; assist prover +2.0ms; verifier 9.8ms direct f̂_t vs 0.60ms assisted (16.3x); proof 752 B + 1552 B assist. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… pass Breakdown at m=23 (bits30_breakdown) showed 3.1ms of the 9.2ms prover was avoidable traffic: a q.to_vec() (1.9ms, memcpy-bound, existed only so round 1 could read an owned buffer) and a separate round_msg_par pass re-reading q + B (1.2ms). Two transcript-invariant fixes: - generate_f_and_claim now emits round 1's message alongside B and the claim: the pass already streams q and B pair-by-pair, so fusing (G(1), G(inf)) in costs 2 extra mults per pair and zero extra traffic (chunks are even, pairs never straddle). m=0 special-cased (single element, no pairs). - prove_main folds round 1 straight out of the borrowed q and owned B into the scratch buffers; rounds 2+ ping-pong len/2 and len/4 buffers (the write always fits the smaller pair). q is never copied; peak owned memory drops 384 -> 320 MB at m=23. runtime_bits30: sumcheck prover 9.2ms -> 5.8ms (with assist 7.7ms). Every remaining pass is compulsory: the fold cascade runs at ~200-235 GB/s (scaling_diag ceiling) and gen is write-allocate-bound. round_msg_par retained for the runtime benchmarks; bits30_breakdown updated to mirror the new pipeline. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Design for one proof covering a heterogeneous batch of hash invocations (table per hash type; rows = invocations), with per-proof dynamic counts: static capacity-sized address space, union block-diagonal R1CS whose single zerocheck is implicitly the batched per-table zerocheck, multi-size lincheck via eq-embedding, BatchMajor layout with the univariate skip over row bits, and the jagged stacked-columns commitment as the claim-transport layer. No per-invocation IO in the core; dataflow deferred to a future lookup/bus layer. Build with pdflatex (PDFs untracked). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…it skip Code reconnaissance showed WitnessLayout::BatchMajor is chunk-column-major (addr = [7 in-word | rows | chunk]), so the univariate skip stays over in-word column bits and the existing kernels run byte-identically -- the row-bit-skip construction and both kernel spikes are unnecessary. Rewrite the layout convention, skip section, and lincheck coordinates (restriction notation over interleaved partitions); Phase 1 re-scoped to the jagged composition adapters (multi-claim RLC + univariate-coordinate point format). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Ring-switching already eliminates the seven in-word packing coordinates -- univariate skip coordinate included -- so the jagged transport operates on packed data at ordinary multilinear points. This kills the point-format adapter open question; the remaining Phase 1 composition work is multi-claim RLC batching into one transport sumcheck. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…hing rationale Per discussion: (1) claim batching is a cost matter, not soundness -- a mixed proof emits ~2T claims at distinct points and unbatched transport pays the dense sumcheck + assist per claim; per-claim v0 is a valid stepping stone. (2) The ring-switch prover folds run over the sparse trace and must skip dummy rows: the fused s_hat_v capture inherits the zerocheck run-lists (explicit checkpoint), per-slot lincheck-claim folds are slot-local. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…aim transport Per discussion with Ron: (1) adopt uniform row capacity as the registry convention -- it makes the packed union polynomial literally the jagged grid polynomial, so the zerocheck C-claim transports directly with no per-slot decomposition; (2) the lincheck's inner sumcheck runs over the union column domain (the same addressing trick as the zerocheck), replacing the late-join/eq-embedding machinery and emitting a single witness claim; (3) the proof's core claim inventory drops to two claims sharing their row point, reducing transport batching to a two-term weight table. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Brings the paper-§5 assist (streaming Lemma-4.6 prover), the fused jagged prover pass, and the runtime benches onto the multitable branch as the commitment-layer building block for Phase 1. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…tical) Phase 0 of the multi-table design (docs/multi-table-design.tex §5.2): the padding descriptor becomes an ordered list of (k_log, useful_bits_per_block, n_blocks) runs laid out back-to-back, with an implicit all-zero gap after the last run — the shape a count-derived slot schedule needs to describe dummy rows and useless columns per slot. All current callers build single-run specs (dense, the new uniform constructor, BlockR1cs::padding_spec), and the hot kernels detect that case via as_single_run() and take exactly the pre-run-list code paths: proofs, transcripts, and the s_hat_v_c capture are byte-identical. Multi-run specs go through new general paths with no production callers yet — a full-length window-count table in the round-1 URM, a portable per-pair-skip fold in round 2, and a sound no-skip fallback in the ring-switch chunk classifier (generalizing those folds to run-lists is Phase 2 work). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Phase 0 scaffolding for the multi-table design (docs/multi-table-design.tex §3-4): TableType carries what BlockR1cs stores per base block; Registry fixes the ordered type list plus ONE uniform row capacity 2^nu and derives the static slot layout (descending-area sort, offsets, per-slot prefixes, union variable count M, alignment invariant asserted); Instance adds the per-proof declared counts n_t and derives the count-derived run-list PaddingSpec over the union BatchMajor buffer (blocks are chunk-columns, so dummy rows are per-block useful prefixes; useless columns are explicit zero runs; the region past the last slot is the run-list's implicit gap). Pure data types with unit tests — nothing is wired into the prover or verifier yet; a single-type registry at full utilization reproduces today's BlockR1cs padding semantics, and a schedule-derived multi-run spec drives the zerocheck prover to the same proof as the dense path. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
From the Phase 0 implementation: run-list blocks are chunk-columns (k_log = 7+nu), dummy rows are each chunk-column's dead suffix, and useless chunks need explicit mid-list zero runs so later slots keep their offsets. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Registry::digest() binds the multi-table statement into the transcript (Phase 0 of docs/multi-table-design.tex, "Statement, transcript, wire format"): BLAKE3 over the b"flock-registry-v1" domain label, a format- version byte, nu, the type count, and each type in slot order (k_log, useful_bits, const_pin, base matrices). Matrices are absorbed by the same length-prefixed routine as BlockR1cs::statement_digest, now pub(crate); the label domain-separates the two digests. Cached in a OnceLock like BlockR1cs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Per discussion: sparse bit polynomial (arithmetization) -> ring-switch -> sparse packed polynomial -> jagged -> dense packed polynomial (committed). The two reductions use different claim types: ring-switch necessarily outputs an inner product against a transparent non-factoring weight (the r''-randomized binding of s_hat_v), while jagged consumes point evaluations; a new virtual-opening sumcheck is the standard type converter, and since it runs after the gamma-batching, the jagged reduction always carries exactly one claim. Also: honest Phase 1 gate (no area saving at single-table -- 121/128 and 246/256 chunk utilization rounds back to the padded power of two; savings move to Phase 2's gate), and the claim-batching open item becomes wiring constraints. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Phase 1 of the multi-table design's commitment layer: an additive
alternative to the mixed Ligerito open that routes the batched claim
through the jagged transport. `open_batch_jagged_ligerito` reuses the
existing claim assembly verbatim (ring-switch batched prove +
γ-combination, transcript-identical to the mixed path), then
1. runs the NEW virtual-opening sumcheck (`flock-virtual-open-v0`):
a product sumcheck over the m−7 packed-word variables proving
Σ_x f(x)·b_combined(x) = target_combined, with the char-2-safe
(G(1), G(∞)) round encoding; round 0's message falls out of the
already-computed round-0 prime. Output: ρ and f_eval = f̂(ρ);
2. transports the single evaluation claim through the jagged
sumcheck + assist (q = the packed witness — at Phase 1 single
table the dense stack IS the padded buffer);
3. opens the dense stack with Ligerito against the eq(i*, ·) basis,
reusing the commit-time codeword/Merkle tree as L0.
`verify_opening_batch_jagged_ligerito` mirrors it: per-claim succinct
ring-switch verify + target reconstruction as the mixed path, replay
of the virtual-opening rounds with the final check against
b̂_combined(ρ)·f_eval (evaluated via eval_rs_eq / eq_eval at ρ), the
jagged verify-with-assist, and the succinct Ligerito verifier with a
plain eq residual basis.
jagged.rs changes are visibility/derive only: prove_main,
fold_round_claim, and the fused fold kernels open to the crate (the
virtual-opening sumcheck shares the round structure), and the proof
structs gain serde + Eq derives for the wire format. The existing
mixed open/verify entry points are untouched.
The new pcs test covers an end-to-end roundtrip on a synthetic
single-table instance with dead chunk-columns plus tamper rejection
of every new proof component (f_eval, virtual-open rounds, jagged
rounds, α, assist β/rounds, ring-switch, Ligerito, wrong heights).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Prover side: `prove_fast_ligerito_jagged_from_witness` — the exact
commit → zerocheck → lincheck core of the direct fast path (so the
PIOP transcript prefix is byte-identical on the same statement and
witness), with the opening routed through
`pcs::open_batch_jagged_ligerito`. Requires the BatchMajor layout;
the jagged grid geometry comes from the new
`BlockR1cs::jagged_heights` (ceil(useful_bits/128) full-height
chunk-columns, zero elsewhere), the shared single source of truth for
both sides. New proof type `R1csProofJaggedLigerito`.
Verifier side: `verifier::verify_ligerito_jagged` /
`verify_claims_jagged_ligerito` — shared `verify_core` PIOP replay,
then the jagged batched-opening verify on the single-thread verifier
pool, with heights derived from the statement (never the proof).
Tests (`tests/jagged_roundtrip.rs`, batch-major BLAKE3 m=22 and
SHA-256 m=22):
- jagged prove → verify roundtrips;
- differential against the direct path: same commitment root,
byte-identical zerocheck/lincheck sub-proofs and ring-switch
messages, same accepted claims;
- tamper rejection of every jagged-specific component (f_eval,
virtual-open round, jagged round, α, assist β/round, ring-switch,
Ligerito, wrong heights via a mis-declared useful_bits, and PIOP
tampering through the shared core);
- proof-size report: +1864 B (BLAKE3) / +2536 B (SHA-256) over the
direct path (~0.7–0.9%), the virtual-opening + jagged transport
scalars.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Phase 1 gate measurement (run with --ignored --nocapture): BLAKE3 at m=30, timing witness gen, both prove paths, both verifiers, and proof sizes. First numbers on Apple silicon: jagged prove +10.9% over direct (118 ms vs 107 ms; 485k vs 530k hashes/s e2e), verify at parity, proof +2.2 KB -- the expected pure-overhead regime at single-table full utilization, before any Phase 2 area savings. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…umcheck, un-fused Ron's framing: ring-switch = message + weight + sumcheck (prover sparse, verifier oblivious), leaving one evaluation claim on the sparse packed polynomial; the direct path had fused that sumcheck into Ligerito's inner-product argument. Also records the prover-sparsity status: Phase 1 folds dense buffers (= the support at full utilization); support- proportional folds are Phase 2 work. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Replace the jagged main sumcheck + eq(i*, .)-basis opening with the
corrected fusion: Ligerito discharges the inner product <q, W_rho> =
f_eval directly, with the jagged weight table W_rho = f_hat_t(rho_row,
rho_col, .) as its basis (claim assembly and the flock-virtual-open-v0
sumcheck are byte-identical to before). The basis evaluations Ligerito's
final check needs at ris||bits(y) are prover-supplied (b_tilde) and
bound to the true W_rho MLE by a send-and-spot-check reduction: b_tilde
is observed after Ligerito's messages, yr_log_n fresh challenges r_extra
are squeezed, and the existing, unmodified jagged assist proves
W_rho_hat(ris||r_extra), which the verifier requires to equal
MLE_{b_tilde}(r_extra) (Schwartz-Zippel binding).
- BatchOpeningProofJaggedLigerito: drop jagged_sumcheck, add b_tilde.
- ligerito: the with-basis prover impl also returns its fold challenges;
a new pub(crate) fused entry forwards them and mirrors the succinct
verifier's trailing (alpha_last, beta_last) samples so the transcript
can continue past the opening. Legacy entries are behavior-identical.
- jagged: pub(crate) weight_table_claim_and_round0 exposes the fused
weight-table + claim + round-0-prime pass; prove/verify and the assist
are untouched.
- tests: replace the jagged-main-sumcheck tamper cases with a single
b_tilde flip (caught by Ligerito's final check, which consumes
b_tilde) and a yr-consistent b_tilde pair (crafted to keep Ligerito's
final check satisfied; caught by the spot-check/assist comparison).
BLAKE3 m=30 throughput: jagged prove overhead vs direct drops from
+16.2% to +6.7% (the jagged main sumcheck, the eq(i*, .) build, and the
separate round-0 pass are gone); proof size +2584 B vs direct.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The jagged transport is fused into Ligerito (basis = W_rho); the basis evaluations at the recursion's 2^yr_log_n final points are supplied as a prover vector b_tilde and bound by evaluating its MLE at a fresh random point against one unmodified assist (Schwartz-Zippel). Matches the implementation in 7059f44. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… accounting Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…hput test Matches the canonical benches' warm best-of-N conditions; the old generate-and-drop warm-up freed the buffers instead of pooling them, charging cold allocation to the first timed iteration. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
UnionInstance wraps a Registry + counts and derives everything the union prove/verify paths need from the union address space, replacing what BlockR1cs provides for a single table: the count-derived run-list padding (delegating to Instance::padding_spec), the union jagged-grid heights (slot t contributes ceil(u_t/128) used chunk-columns of height n_t at its aligned column offset o_t >> (7+nu)), the BatchMajor claim-point helpers (the BlockR1cs formulas with (m, n_log) = (M, nu) — slot-independent under uniform capacity, hence multi-slot-ready as-is), and union witness assembly (per-slot (z, a, b) placed at o_t >> 7; single slot = zero-copy passthrough). verify_ligerito_jagged_union replays the PIOP over the union address space and checks the jagged opening against the union heights; the M1 statement binding stays the slot's single-table BlockR1cs digest (bind_statement_single_type), byte-identical to today's transcript — the registry-digest + counts binding lands in a later milestone. Tests: single-slot heights/claim-points/padding-classification equivalence against BlockR1cs, hand-computed multi-slot heights and witness placement, passthrough pointer stability, and the M1 single-type guard. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
prove_fast_ligerito_jagged_union assembles the per-slot witness bundles (UnionSlotProverInput wraps the existing drivers' (z, a, b, stripe) tuples plus the slot's lincheck circuit) into the union buffers and drives the EXISTING jagged path with the UnionInstance-derived quantities: count-derived run-list padding (the zerocheck kernels' general multi-run paths — value-identical to the single-run spec on honestly-zero padding), union jagged heights, n_log = nu, union claim points, and the M1 single-table statement binding. Single-type only; the lincheck is the slot's own, invoked exactly as today. tests/union_roundtrip.rs is the milestone's hard equivalence oracle: BLAKE3 and SHA-256 at full utilization proved via the existing prove_fast_ligerito_jagged_from_witness and via the union entry, the ENTIRE proof bundles asserted bincode-byte-identical and both accepted by their verifiers; plus a prove -> verify roundtrip through the union entry pair alone, with a wrong-declared-count verifier rejected through the heights binding. Ignored per convention; run with `cargo test -p flock-prover --test union_roundtrip -- --ignored`. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
One product sumcheck over the union column domain generalizes the
single-table lincheck to T aligned slot subcubes (design doc, "Lincheck
over the union"): per-type quirky combs scaled by the slots' prefix-eq
weights and per-slot row folds against the one shared eq table of r|_R,
placed at the aligned column offsets, drive the existing sumcheck core --
extracted verbatim as column_sumcheck_prove -- so a single-slot registry
computes byte-for-byte today's lincheck. The verifier replays the rounds
and evaluates the Comb-hat skip-block collapse by the closed form
(union_comb_partial): per-type comb MLEs times r-side prefix weights and
bound-point subcube eq factors, nothing union-sized materialized.
Const-wire pins generalize per type with the count-derived expected value
beta * sum_{row<n} eq(r|_R, row) (dummy rows carry the pin at 0),
reducing exactly to today's target += beta at full utilization.
Oracles: a T = 1 differential (byte-identical proof, claims, captured
fold, and transcript state vs prove_padded_capture_z_vec) and a T = 2
zerocheck-then-lincheck integration test against brute-force MLEs of the
dense union buffers -- initial claim, final witness claim, and the
dense-Comb collapse at the bound point -- plus tamper rejection (round
message, z_partial, comb-affecting declared count).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The milestone: a single proof attesting a mixed batch of boolean rows (BLAKE3 compressions) and element rows (F128 gates), over ONE union commitment. Transport threading: open_claims_with_precomputed_jagged_ligerito and verify_claims_jagged_ligerito grow a packed_direct parameter (both pcs-level entries already took one; only these wrappers hardcoded &[]). The element class's two claims ride it with a Sparse eq tensor — their region-prefix coordinates are a fixed Boolean pattern, so build_eq_sparse pins those index bits instead of doubling the tensor — and no ring-switching, since an element already IS a packed word. New entries prove_fast_ligerito_jagged_union_mixed_class / verify_ligerito_jagged_union_mixed_class over a new R1csProofMixedClassLigerito with one Option sub-proof per class. A NEW proof type on purpose: R1csProofJaggedLigerito's serialized bytes are pinned by union_m6_fixtures, and boolean-only proofs keep going out through it byte-identically. Both share one pipeline (prove_union_with_binding / verify_union_piops), so the classes cannot drift apart. FS order: commit -> bind_statement -> boolean tau -> boolean ZC -> boolean LC -> element tau' -> element ZC -> element alpha' -> element LC -> gamma-batched opening. Either class may be absent; a proof whose class sub-proofs disagree with the registry is rejected (ClassMismatch), not a panic. UnionElementSlotInput is the element witness input: a closure writing the slot's committed element words in place, from which fill_slot derives pa/pb by sparse gather into the union a/b buffers. The element region's a/b copies are taken before the boolean zerocheck recycles those buffers. Tests (tests/union_element.rs, 8 cases): element-only roundtrips at one and two slots, non-power-of-two, single-row and zero counts, with dense_words asserted count-proportional; the mixed BLAKE3+element roundtrip plus the full tamper matrix (element word, boolean word, wrong count each way, swapped registry digest, every claim value and round message, missing/extra class sub-proof, truncation, bit flips, wrong transcript); one class at count zero both directions; the dummy-row closure (a SATISFYING non-zero dummy row — the standalone milestone's known gap — is now rejected, and the same witness with it zeroed verifies); the differential against the standalone element proof on seven honest/broken instances; an opening-binding probe on the element-only proof, whose opening has no ring-switched claims at all; and pinned byte-identity fixtures for the mixed-class payload (7 shapes, verified stable at 1/3/8 rayon threads). Pre-existing and not mine: pcs::tests::pcs_ligerito_backend_roundtrip (#[ignore]d) panics on a too-thin config at HEAD too. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
boolean_packed_len/boolean_col_log computed `M_bool - 7` unconditionally, which underflows on an ELEMENT-ONLY registry (M_bool = 0). Release masks the shift and hides it — a debug run of element_only_union_roundtrip panics. Both now return 0 for an empty boolean region, which is also the honest answer (no boolean PIOP runs), pinned by element_only_boolean_accessors_do_not_underflow. The two union_element cases that hand the prover a non-zero DROPPED word tripped compact_witness's honest-witness debug assertion in debug builds. That assertion IS half of the dummy-row closure, so each half is now checked where it is observable: debug asserts compact_witness panics (catch_unwind), release asserts the resulting proof is rejected. All 8 cases pass in both profiles (debug needs --test-threads=1 — the parallel debug harness overflows a worker stack in the Ligerito recursion, the repo's known pre-existing hazard, same as union_mixed). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The box is noisy, so the arms alternate inside one process and every figure is a median over min-max. Nothing asserts on the clock; each rep still verifies both proofs. Two regimes separate the two candidate mechanisms (full utilization, where stream_b is off in both arms anyway, vs 1/16 utilization, where the boolean-only arm has it and the mixed arm loses it), and a nu sweep attributes the delta by SCALING rather than by argument. A final arm prices the layout on the realistic BLAKE3+SHA-256 registry, where the boolean prefix subcube has a 2^25 hole the element region is not allowed to use. Findings (M4 Max, release): - Mixed vs boolean-only prove: +13/20/27% at nu=10/12/14 on a single-hash registry (1.0/3.0/9.9 ms on 7.7/15.2/36.5), and +9% (1.5 ms on 17.0) on BLAKE3+SHA-256 at nu=10. - The element PIOP itself is 0.3/0.6/1.6 ms — 15-30% of the delta, and it scales with its own region, not with M. - The accepted stream_b regression is NOT measurable: the ABSOLUTE delta is the same at full and at 1/16 utilization (1.0 vs 0.9, 3.0 vs 2.3, 9.9 vs 8.6 ms), so the larger low-utilization percentage is just a cheaper baseline. - PCS_TRACE attributes the rest: on the two-hash arms the opening goes 6.89 -> 7.7 ms, of which combine rs_eq_ind is 0.77 -> 1.45 ms (L doubles, 524288 -> 1048576 words), the virtual-opening sumcheck +0.07 ms (one extra round), and the fused Ligerito open is unchanged at ~3.95 ms because dense_m is equal. So the cost is the padded domain DOUBLING that element_base = 2^M_bool forces, not the element class's own work. The trace also confirms the Sparse eq tensor is load-bearing for speed and not just memory: it keeps the element claims out of pd_dense, so the boolean claims stay on the fused use_fast fold (combine merely doubles with L instead of collapsing to the per-element path). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ness
The γ-combined opening basis is an eq tensor, so the witness's zeros do not
make it zero and the use_fast build wrote all 2^(M-7) entries. That is why
adding an element slot cost ~25% of prove: the prefix-subcube layout pushes
M up by one, and the basis pass is O(2^M) regardless of counts.
But the two classes' claims are supported on DISJOINT regions, and the loop
already hoists the fact per block. A claim point with frozen high
coordinates has eq_hi[hi] == F128::ZERO on every block outside its own
support — the boolean claims carry M - M_bool frozen zeros, so their basis
vanishes on the whole element region AND the inter-class gap. When every
claim's factor vanishes on a block, so does b_combined there, because
fold_one_slot(0, table) = sum_k table[k*256 + 0] and
build_fold_byte_table fills value = 0 with the empty sum: exactly zero. So
store zeros and skip 16 table lookups + 15 XORs + a GF multiply per word.
Bit-identical, not merely value-identical.
The zeros still have to be STORED: the virtual-opening sumcheck's round-0
fold reads b_combined densely when the support is not sparse.
Measured (M4 Max, interleaved arms, median of 5-9 reps). The combine's
domain-doubling term is essentially eliminated —
nu=14 full utilization, combine rs_eq_ind:
before bool 2.46 ms (L=2^21) mixed 5.54 ms (L=2^22) delta 3.08
after bool 2.38 ms mixed 2.62 ms delta 0.24
— and total mixed-vs-boolean prove overhead falls:
nu=10 +15% -> +14% nu=12 +20% -> +13% nu=14 +27% -> +18%
BLAKE3+SHA-256 nu=10 +9% -> +7% (1.5 -> 1.2 ms on 17.0)
low utilization nu=14 +74% -> +51% (8.6 -> 5.7 ms)
Boolean-only proofs are untouched: with M_bool = M there are no frozen
coordinates, so no block is dead (pd=0 combine 2.46 -> 2.38 ms, noise).
union_m6_fixtures, the union_roundtrip differentials and the mixed-class
fixtures all still match byte for byte.
The win generalizes past this milestone — any claim set with frozen high
coordinates benefits, which is the shape every region-restricted PIOP
produces.
Two residuals, NOT addressed here:
- Low utilization still loses stream_b (combine 2.38 vs 0.29 ms for the
streaming boolean arm): the mixed arm materializes the boolean region's
basis where streaming would evaluate it only at live indices. Fixing that
needs the JIT fold to add sparse packed-direct claims pointwise, which is
O(1) for subcube supports like the element claims'.
- The residual full-utilization delta (6.0 ms at nu=14, of which the
element PIOP is 1.4 and the combine 0.24) is unattributed. Leading
suspect from arithmetic, not measurement: take_witness_buffers' threshold
`dense_words * 2 <= len` flips the mixed arm to FreshZeroed, so it
allocates and first-touches 3 x 2^22 fresh zero pages (192 MB) instead of
reusing 3 x 2^21 pooled words, and give_back = false keeps them out of
the pool.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e probe
Two measurement fixes, then the attribution they produced.
1. prove_union_with_binding gains PCS_TRACE phase timings (witgen with its
WitnessBufMode, compact, commit, the element a/b copies, the boolean
PIOP pair, the element region PIOP, open), mirroring the merged path's
convention, plus a self-delimiting `=== done (element: bool) ===` line so
a trace reader never has to guess which prove a phase belonged to. That
guessing had produced a mis-tagged table on the previous pass.
2. The cost probe drove its boolean slot through UnionSlotProverInput::new
in both arms. That is not a fair comparison: with `new`, a single-slot
boolean registry takes assemble_witness's ZERO-COPY passthrough (witgen
0.00 ms), which ANY second slot loses — element or boolean — so it
charged the element class for a multi-slot cost it does not own. Both
arms now use the in-place driver, which is what the real prover uses.
Mixed-vs-boolean overhead drops accordingly:
nu=10 +14% -> +14% nu=12 +13% -> +9% nu=14 +18% -> +14%
BLAKE3+SHA-256 nu=10 +7% -> +6%
low utilization nu=14 +51% -> +38%
Attribution at nu=14 (ms, mixed minus boolean-only):
full util low util
element region PIOP +1.56 +1.48
combine rs_eq_ind +0.41 +2.07
virtual-opening sumcheck +0.83 -0.73
witgen +0.71 +0.58
compact q +0.33 +0.06
boolean zerocheck+lincheck +0.07 +0.08
The boolean PIOP pays nothing for the element class, which is the point of
the disjoint-domain formulation.
Two things this corrects in what I reported earlier:
- The remaining stream_b loss is ~1.3 ms, not 2.1: the combine's +2.07 is
partly offset by the sumcheck's -0.73, because the streaming arm does its
b-side JIT fold INSIDE round 0 rather than up front (combine+sumcheck:
0.30+2.38 streaming vs 2.38+1.64 materializing).
- I claimed the boolean region's unused hole could host the element region
and remove the M doubling. That is WRONG and I retract it: the hole lies
inside [0, 2^M_bool), which IS the boolean zerocheck's domain, so element
data there would re-enter the c = z trap. Given two disjoint domains and
a power-of-two boolean prefix, element_base >= 2^M_bool is forced and so
is M >= M_bool + 1. The doubling is structural, not an accident.
The element PIOP is now the largest term in BOTH regimes, and it costs the
same at 1/16 utilization as at full (1.48 vs 1.56 ms) — it is
count-INDEPENDENT. That is exactly the "count-proportional element prover"
item both handoffs deferred, and it is the highest-value remaining target.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…se ones
The element zerocheck cost the same at 1/16 utilization as at full (1.48 vs
1.56 ms) — the deferred "count-proportional element prover" item, and after
the combine fix the largest remaining term in a mixed proof. It is now
support-proportional, and BIT-identical, so no pinned proof moves.
Why it can be bit-identical. Rows are the LOW nu address bits, so a
column's live rows are a PREFIX and folding maps prefix to prefix. Dead
rows are not zero in pa/pb — z = 0 there leaves the affine constant
a_const[y] — but that constant is uniform down the column and folding
preserves it, so a fully-dead entry equals a_dead[c] at EVERY round. Two
consequences:
- a fully-dead pair contributes nothing to either round message: G(1)'s
summand is a_const*b_const + 0 = 0 by the type's validity rule, and
G(inf)'s factor wa[i0] + wa[i1] vanishes in characteristic 2 because both
halves hold the same constant;
- the one boundary pair a column has when its live count is odd reads its
dead half from a_dead/b_dead analytically.
So the walk covers only the per-column live prefixes and every skipped term
was provably zero. RowSupport carries live[]/a_dead[]/b_dead[] per region
column, derived from the same counts the jagged heights use.
Three things the first cut got wrong, all caught by measurement:
- an eq multiply PER PAIR instead of hoisting eq_hi per block made it
SLOWER than the dense kernel it replaced (1.48 -> 1.7 ms at 1/16). It is
now block-major like the dense kernel.
- the fold parallelized over columns; element blocks are narrow and tall, so
that collapses to 2^kappa threads. Now flat output chunks.
- both the message's and the fold's parallel gates used the DENSE size, and
the witness working copy was a full z.to_vec(). Those three left it O(2^E)
and flat at 1.3-1.5x regardless of utilization. Gating on LIVE work and
copying only the live prefixes is what actually put it on the count axis.
Measured (nu=14, region 2^17 words, arms interleaved, median of 5;
support_proportional_rounds_are_bit_identical asserts equality every rep):
rows dense support speedup
100% 1.44 0.74 2.0x
50% 1.30 0.48 2.7x
25% 1.23 0.35 3.5x
6.25% 1.26 0.15 8.2x
1.56% 1.25 0.08 15.0x
End to end, mixed-vs-boolean prove overhead at nu=14 low utilization:
+38% -> +31% (4.1 -> 3.2 ms); the element PIOP within it 1.48 -> 0.5 ms.
Full utilization holds at +13%.
TRUST BOUNDARY (new, and the one real cost). Like the boolean run-list
skipping, the sparse path is bit-identical only for HONEST zeros: it never
reads a word the declared support calls dead, so the PIOP alone no longer
catches a dirty dead word. Under the union the enforcer is the transport — a
dead word is not committed, so a non-zero one breaks <q, W_rho> = f_hat(rho)
and the opening rejects. Pinned from both sides:
padding_column_boundary_dense_catches_sparse_delegates picks the utilization
that decides which path runs and asserts the dense zerocheck catches a dirty
padding column while the support-proportional one delegates;
union_element's dummy-row-closure and standalone-differential tests cover
the end-to-end rejection. The STANDALONE element proof passes support =
None, so it keeps the dense behaviour.
Also fixed on the way: a count-0 column's final value is its dead constant,
not zero — zeroing it lost a_hat_const(r) from ea and the lincheck then
failed to reconcile it. That is exactly a count-0 element slot, which
mixed_with_one_class_at_zero_count covers.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…sion The design document for the circuit layer over the multi-table core, re-cut after the 2026-07-29 design sessions: recursion-completeness as the driving goal; class-tagged tables (boolean + large-field) on disjoint PIOP regions over one union commitment; the Spartan-style element PIOP (C = I, affine constants, collapsed lincheck) — now implemented; copy-constraint wiring via the reviewed product_gkr with the gather-factorization lemma (no gather sumcheck, no new committed columns); settled decisions recorded in place (BLAKE3 throughout, v1 verifier-known sigma, replacement sampling, full Merkle paths, capacity tax accepted); the "jagged remainder" named and postponed; roadmap and implementation status through the union integration. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The doc asserted "f = g = w is the copy-constraint statement" in one line; the actual argument was nowhere. New subsection: no-dataflow reframing (a wire is an equivalence class of cells; fan-out k = a class of size k+1), the tag-rigidity lemma with the cycle-chasing proof and a worked fan-out example, the pair-multiset-to-product step with its Schwartz-Zippel accounting, and the direction/unread-output/validation corollaries. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The term collided with the codebase's meaning of constraint: state up front that copy constraints are the wiring equalities, enforced entirely by the product identity outside the constraint system — no gate, row, or matrix entry implements them. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…race Clarify the deferred refinement against the natural misreading: the masked leaves live in the prover's uncommitted product-tree input, built per proof from committed values and challenges; dummy trace rows stay all-zero as the zerocheck/jagged conventions require, and the masked input-layer reconstruction relies on exactly that. Name the correction terms (live-indicator MLEs as count-derived aligned-interval eq sums). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
New remark in the layout discussion: class separation costs one address bit regardless of element-class size (neither region can nest in the other's subcube without the c = z trap); the audit shows commitment, both PIOPs, wiring, and the verifier pay nothing for dead addresses, while the unmerged transport's padded-domain auxiliaries and the materialized padded witness buffer do. Plan: accept; merged intake retires the first payer (dense-domain computation); the shelved dense-born witness refactor retires the second and gains value with this inflation; multi-subcube boolean packing rejected. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Concrete registry (sha2 + mult + public, nu = 10, c = 4): the cell enumeration, the bit-concatenation map from a cell to its committed word, that w/sigma/tags all speak cell indices rather than union addresses, and why the second index space exists at all (a factor per schema word instead of per trace word, immune to internal columns and the dead inter-class space). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The worked example's 8-word sha2 schema read as forced by the trace; note it is the chaining-gate choice (h wireable, needed for FS chains and multi-compression Merkle leaves; IV instances wire h to the public IV cell), that a 6-word IV-pinned variant exists, and the rule that a word left out of the schema must be pinned by the relation. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Four kinds of emptiness across the two index spaces (non-IO trace columns, dead addresses, dummy rows, cell-space padding), each with its handling and its enforcement mechanism, unified by the invariant that everything unnamed is zero and zero is both satisfying and inert. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A transcript tamper matrix over the σ-aware verifier — every scalar of a batched proof flipped one at a time must be rejected, and the one exception (s_sigma_eval, which that verifier recomputes) is pinned as inert rather than left ambiguous. The μ ≤ 64 check becomes a hard assert: past that bound the s_id-as-index tag silently stops being s_id, so a release build would prove the wrong statement instead of failing. Unreachable in practice, which is exactly why it must not be the check that is compiled out. Nothing else in the module changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The merged (Frobenius) path is the shipped one and the capacity-free one, but element and circuit proofs cannot use it: their claims are packed-direct, and open_batch_merged had no parameter for them. So those proof shapes sit on the unmerged jagged path by necessity — paying its padded-domain auxiliaries, which is one of the two payers the dead-address audit identified for class-separation address inflation. The mechanism turned out to need no new machinery. The merged weight is built per claim by fold_one_slot(eq_row·eq_col, tab), where fold_one_slot applies the ARBITRARY F2-linear map whose weight on bit i of its input is tab's i-th coefficient. Multiplication by gamma is F2-linear, so a packed-direct claim — whose weight is the plain gamma·eq_row (x) eq_col — is just the table built from weights[i] = gamma·basis_i. It enters the existing per-claim loop in exactly a ring-switched claim's form, and the weight builder cannot tell them apart. ring_switch::identity_fold_weights gives those weights; identity_fold_is_scalar_multiplication pins that fold_one_slot with them IS multiplication by gamma, over random gammas and inputs plus the degenerate ones. That identity is the whole justification for the routing. The one place the two claim kinds genuinely differ is the point split: a ring-switched point is [skip | rows | cols], a packed-direct one has no univariate-skip coordinate, so it splits at n_log with no leading 1. Gammas for packed-direct claims are drawn after the ring-switched ones, in the same order on both sides, with the point and value observed first. NOT YET EXERCISED END TO END. Every caller passes an empty list today, which the m6 fixtures confirm is transcript-identical, so the new branch is correct-by-inspection but unrun. Driving it needs mixed-class-over-merged prove/verify entries — R1csProofMergedLigerito has no element sub-proof — which is the next increment, and the point of this one. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Finishes what the packed-direct intake started: element claims can now ride the shipped, capacity-free path instead of being confined to the unmerged jagged one and its padded-domain auxiliaries — one of the two payers the dead-address audit identified for class-separation address inflation. The transport is now a parameter of the union prove rather than a fork in the code. prove_union_with_binding already ran BOTH class PIOPs and only its final open was jagged-specific, so the whole change is one match at the open site: same claims either way, the boolean pair ring-switched and the element pair packed-direct. No PIOP logic is duplicated, and the existing merged entry is untouched. R1csProofMixedClassMerged mirrors R1csProofMixedClassLigerito with the opening type swapped; the prove/verify entries are thin. mixed_proofs_verify_over_the_merged_transport is the end-to-end exercise the previous commit could not do. It pins the property that matters — the two transports carry the SAME claim set, so they must agree on the claims while their openings differ — plus a tamper matrix (opening, element claim, boolean claim) confirming the merged path still rejects, which is what says the packed-direct claims are not just riding along unchecked. Two things found on the way, both left as they are: - The merged path asserts at least one ring-switched claim (prove_batched_padded_with_precomputed), so an ELEMENT-ONLY proof cannot use it yet. Mixed and boolean-only can. Relaxing that is separate. - My first attempt at the verify entry was written against the deferred verify_union_piops from folding_verifier, which does not exist on this branch. The point layout is subtle enough (x_inner_rest ‖ x_outer, skip carried separately) that I copied the boolean-only merged verifier's construction verbatim rather than re-deriving it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The element class's two packed-direct claims eagerly built a 2^(m_elem-7)-entry Sparse eq tensor each, before the transport dispatch. The shipped (merged, wire v6) transport never reads eq_ind — it derives its weights from point/value alone — so on the production path both tensors were built and dropped. The claims now ride as deferred DirectEqInd::EqPoint; only the jagged arm (the differential/regression oracle) materializes them to Sparse, under a new PCS_TRACE label. A forgotten materialization trips the combine's "EqPoint claims are only supported alone" assert rather than dropping a contribution. The jagged materialization also size-gates build_eq_sparse's inner build: parallel at >= 20 live coords (the element claims' all-random region address bits), sequential below (the tuned ~19-coord chain/merkle case). Byte-identical either way; all pins pass un-re-pinned. Also corrects the stale dummy-row-rejection mechanism comments in union_element (the enforcer is the transport, not the zerocheck summing the row — superseded by the count-proportional row rounds). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…path Two bugs the jagged transport was masking, fixed ahead of its removal: - open_batch_merged called the batched ring-switch prover unconditionally, and that prover asserts a non-empty batch — so an element-only registry (zero ring-switched claims) could not produce a merged proof at all. Guarded with the mixed open's `n_rs > 0` pattern; the empty branch absorbs nothing and DEFINES the element-only merged transcript. `verify_batch_merged` needs no mirror (its rs loop is already count-driven and transcript-symmetric with the empty batch). - The merged arm of prove_union_with_binding `expect`ed the dense stack, panicking on identity compaction (single-slot registries at full utilization, where dense_q is None because q IS the padded buffer). Now clones, mirroring the shipped standalone body. Coverage minted with the fixes: an element-only merged roundtrip with a cross-transport claims/root equality check against the jagged prove (the one differential check this path gets while jagged still exists), and an identity-compaction roundtrip through the merged enum path. No existing transcript moves: all jagged pins and the merged A/B hold. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The merged transport ships (wire v6) but until now had ZERO absolute byte anchors — every pin in the repo was jagged. Minted ahead of the jagged transport's removal: - m6_merged_union_proof_bytes_pinned: the 4-count ladder digested at the proof_io WIRE encoding (MixedProofBundleLigerito::to_bytes — magic, version, flavor, registry id, counts, commitment, merged proof), same witness streams as the jagged fixture so both pin the same statements. - m6_single_slot_merged_anchor_proof_bytes_pinned: BLAKE3/SHA-256 single-slot unions at full utilization — identity compaction, the pow2-lane commit, and the full-utilization batch-major drivers, which the integer-lane mixed config never exercises. Replaces the single-table direct-jagged anchors when that path is removed. - mixed_class_merged_proof_bytes_pinned: the same seven statements as the jagged mixed-class fixture through the merged transport, including the element-only half (pinned at its birth). - merged_transport_roundtrip_and_tamper extended to a field-complete MergedOpenProof walk (ring_switches, round tamper + truncation, q_eval, frobenius v/round, inner open root) plus the counts-vector and registry-digest statement tampers ported from the jagged matrix. Exit-gate record (the last merged-vs-jagged numbers on this branch; min of 2, prove incl. witgen, counts [16384, 16384]): nu=14 (M=30): jagged 110.8 ms merged 113.2 ms nu=15 (M=31): jagged 148.5 ms merged 113.4 ms nu=16 (M=32): jagged 156.7 ms merged 114.9 ms The capacity-free design claim measured against its comparator one final time: merged flat, jagged growing with 2^(M-7). All suites green; zero existing pins moved. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Every surviving union test now drives the merged transport (the shipped protocol), while the jagged entries still compile — the next commit is pure deletion. Highlights: - union_element: all mixed-class tests -> ..._mixed_class_merged. The opening-binding test walks the merged fields (q_eval, every merged and frobenius round, the inner open root) instead of f_eval/virtual rounds/ b_tilde. The standalone differential now asserts the SPLIT verdict on dropped-word tampers: the union accepts (structurally invisible on merged) where the standalone dense proof rejects — in-support tampers still must agree. - satisfying_dummy_row_is_rejected_under_the_union is re-framed and renamed dummy_row_is_structurally_invisible_under_the_union: the release half now asserts proof(dirty) == proof(clean) BYTE-IDENTICAL (stronger than the jagged fail-closed rejection: nothing the prover computes depends on the dropped word). The debug compact_witness half stays. - boolean_only_mixed_class_matches_the_plain_entry compares the two MERGED bodies (hand-written shipped vs prove_union_with_binding) — byte-equal already; this is the unification commit's drift detector. - union_mixed: roundtrip/tamper/sweeps/smokes -> merged; the capacity sweeps time prove/verify at test level (the jagged _timed phase columns died; PCS_TRACE + merged_capacity_attribution are the successor); the m30 probe drops its jagged arm and asserts an ABSOLUTE flatness bound quoting the final A/B record; single-type baselines become single-slot merged unions at the same m; two_blake3_phase_breakdown (jagged-phase attribution) and the control's jagged row are deleted. The jagged pin fixtures (union_m6_fixtures, mixed_class_proof_bytes_pinned, union_roundtrip) are untouched and still green; they die with the entries. All merged pins hold unchanged; full suite green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The merged transport (wire v6) is now the only transport. Removed: - Prover entries: prove_fast_ligerito_jagged_union / _mixed_class / _harness / _timed, the single-table prove_fast_ligerito_jagged_from_witness, open_claims_with_precomputed_jagged_ligerito, materialize_deferred_eq, the Transport and UnionOpen enums (prove_union_with_binding is merged-only, straight-line), UnionProveOutput::into_boolean_only, and the SingleTypeHarness binding (UnionProveBinding/UnionVerifyBinding stay as one-variant enums to minimize forward-merge conflicts with recursion_circuit's Circuit variant). - Verifier entries: verify_ligerito_jagged, verify_ligerito_jagged_union / _timed / _harness / _mixed_class, verify_union_with_binding, verify_claims_jagged_ligerito. - PCS: open_batch_jagged_ligerito, verify_opening_batch_jagged_ligerito, BatchOpeningProofJaggedLigerito (b_tilde + send-and-spot-check), the combine's live_pairs/stream_b streaming mode (its only activator was the jagged open's M6 f-side skip; the dead-block skip survives), the jagged.rs JIT weight machinery (JaggedWeight, claim_and_round0_jit, weight_table_claim_and_round0[_blocked], f_hat_t_batch_y[_split], fold_and_round_sparse[_bjit]) and their equivalence tests, and ligerito's recursive_prover_with_basis_precomputed_round0_fused. KEPT: prove_assist/verify_assist (called by the spec-level prove/verify_with_assist), JaggedParams, the Frobenius assist, and all merged dependencies. VerifyErrorJagged stays (merged raises every variant; renamed in a later pass). - Proof types: R1csProofJaggedLigerito, R1csProofMixedClassLigerito. Nothing jagged was ever on the wire; no VERSION bump. - union.rs: expect_single_type_slot, bind_statement_single_type. - Tests: jagged_roundtrip.rs, jagged_throughput.rs, union_roundtrip.rs (its count-rejection property lives in the merged tamper walk), the jagged pin fixtures (their merged successors were minted at fa84ab0 and hold), and the union_element jagged pin. assist_blocked keeps its single-statement arm (the functions remain as the Lemma 4.6 reference). - Doc sweep: every open_batch_jagged_ligerito/entry reference now points at the merged path; the boolean-only asserts name the mixed-class merged entries. Full suite + all ignored union suites green; every merged pin holds unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
prove_fast_ligerito_jagged_union_merged is now a thin wrapper over prove_union_with_binding, and verify_ligerito_jagged_union_merged over verify_ligerito_jagged_union_mixed_class_merged (repackaging boolean-only proofs as the wire's R1csProofMergedLigerito) — the "kept in lockstep" two-body split existed for the jagged/merged coexistence and died with it. The two-body byte-equality test (boolean_only_mixed_class_matches_the_ plain_entry) proved the merge before it happened and keeps guarding the repackaging. Ported into the shared body from the standalone one: - padding_unread pooling, gated OFF for element registries (the element PIOP's dirty-padding behavior is unaudited — follow-up) and OFF under identity compaction: there q IS the padded buffer, so dirty pooling would commit garbage. The latter is a latent hazard the standalone body always had but never exercised; the unification exposed it through the cost probe's full-utilization arm (PcsJagged(Ligerito) reject), and the gate fixes it. - The PooledDirty compact_witness_unchecked arm and the identity-clone q (the merged open owns the dense stack). All byte pins hold unchanged — the unification is transcript-clean. Full suite + all ignored suites green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Behavior-free rename, proven by the pins (all byte fixtures hold —
bincode is structural and the digests hash proof bytes, not names):
prove_fast_ligerito_jagged_union_merged -> prove_fast_ligerito_union
verify_ligerito_jagged_union_merged -> verify_ligerito_union
prove_fast_ligerito_jagged_union_mixed_class_merged
-> prove_fast_ligerito_union_mixed_class
verify_ligerito_jagged_union_mixed_class_merged
-> verify_ligerito_union_mixed_class
pcs::VerifyErrorJagged -> pcs::VerifyErrorOpen
pcs::VerifyErrorJagged::Jagged -> VerifyErrorOpen::Assist
verifier::VerifyError::PcsJagged -> VerifyError::PcsOpen
"jagged" is dead as a transport; "merged" is redundant as a suffix now
that it is the only transport ("merged" survives as the open protocol's
own name: open_batch_merged, MergedOpenProof, R1csProofMergedLigerito).
The jagged MODULE (JaggedParams, jagged_heights, the Frobenius assist)
keeps its name — it describes the matrix geometry, not the dead
transport. No wire change (bincode field-order only, VERSION stays 6).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The merged open's two claim-count-linear terms both collapse for packed-direct claims, which are γ-SCALAR maps (x -> γ·x): - W build (build_merged_weight_and_prime): claims sharing a row point join one MergedWeightClaim::Scalar group with a precombined (γ-summed) column table — Σγᵢ·eq_row·eq_colᵢ = eq_row·(Σγᵢ·eq_colᵢ) — ONE multiply-sweep instead of a fold-table sweep per claim. - Frobenius assist (frobenius_statements, shared by prove AND verify): statements are linear in their per-column weights, and eq4s/suffix rows depend only on (z_row, ρ) — so specs with identical z_row merge into one statement with γ-summed column weights. A ring-switched claim's 128 Frobenius twists have distinct squared rows and stay singletons. - Both sides also build the γ-scalar linearized coefficients directly ([γ, 0×127]) instead of the byte-table detour (debug-asserted equal). All exact — field sums and products reassociate — hence BIT-IDENTICAL W, assist V, and round messages: every byte pin holds unchanged, which is the proof. The payoff is on the circuit path, whose ~2^c gather claims share ρ_row: the Φ-pass and the assist drop from ~2^c sweeps to one (measured on recursion_circuit after the merge). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The gather claims' column parts are Boolean bit patterns, whose eq table is a one-hot indicator — so the Scalar-group combine scatters gamma at the hot index (instead of building a 2^k_cols table per claim: ~2^20 per claim at MVP-5's composite registry, the untraced ~78 ms inside its open) and assist_columns_at emits the per-run indicator directly. Random column points (the element claims, RS twists) keep the dense builds. Value-identical by construction; all pins hold. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Collaborator
Author
|
Closing as superseded by #26: this branch writes proof-IO v6 and can no longer ship independently (head is at v21), and recursion_circuit carries the successor of the whole multi-table scope — the single-slot union with dense stack + integer lanes, mixed registry + counts binding, and the merged transport. The design doc (docs/multi-table-design.tex) remains the reference. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds multi-table proving: a single Flock proof attesting to a heterogeneous batch of hash invocations — e.g. some BLAKE3 and some SHA-256 compressions in one proof, with one commitment and one opening, and the per-hash counts chosen at prove time. Before this, a proof covered invocations of exactly one hash type.
The statement is modeled as a table per hash type (rows = invocations, columns = one invocation's trace), composed into one block-diagonal R1CS over a static, capacity-sized address space. The central identity is that running Flock's existing single-instance zerocheck over the composed instance is mathematically identical to a batched per-table zerocheck with
eq-derived coefficients — so batching comes for free, with plain single-instance soundness. The genuinely new protocol work is a single union-column lincheck. The commitment uses the jagged (stacked-columns) scheme so only the actual data is committed; padded/dummy rows cost the prover essentially nothing.Full design and soundness write-up:
docs/multi-table-design.tex(v0.4).What's in it
schedule.rs,union.rs): a type registry + per-proof counts, aligned power-of-two capacity slots, and the block-diagonal union R1CS. Single-table proofs are the one-slot special case (byte-identical to today).zerocheck.rs): run-listPaddingSpecso the prover pays only for declared work; the sumcheck kernel is unchanged (the union zerocheck is the implicit batched zerocheck).lincheck/union.rs): one sumcheck over the union column domain, per-type comb + prefix weights, single output claim. Counts are additionally bound inside the PIOP via a count-derived const-pin target (defense in depth).pcs.rs,pcs/jagged.rs,pcs/ligerito.rs): the three-polynomial reduction — sparse bit polynomial → ring-switch → sparse packed polynomial → jagged transport → dense packed polynomial. The jagged transport is fused into the Ligerito opening (basis =W_ρ), with the recursion's final-layer basis values supplied by a send-and-spot-check reduction (b_tilde+ one assist). Height-n_tstacking makes the committed size count-proportional; support-proportional folds make padded rows free in the prover passes too.pcs/commit.rs): the dense stack is rounded up to a power of two, and that padding used to be RS-encoded and Merkle-hashed like real data — 28% of the stack for a full-utilization SHA-256 + BLAKE3 mix. Labelling the interleaving lane as the high index bits makes the zero tail whole zero lanes, so only thetreal ones are committed. Crucially the relabelling is a rotation of the index variables, which every multilinear downstream survives by rotating its evaluation point — the jagged branching program and the assist are untouched, and L0 binds the lane variable by folding at block granularity rather than materializing the rotation. Opt-in per proof viaPcsParams.num_lanes;Noneis byte-identical to the power-of-two commit.proof_ioVERSION 5 with aMixedflavor (registry/tier id + counts vector), andflock_chain prove --mix blake3=N,sha2=M/verify. Existing R1cs/Chain flavors and the single-hash flags are unchanged.Measured performance (m = 30, Apple silicon, best-of-3 on a quiet machine)
Mixed BLAKE3 + SHA-256, 16,384 of each: ~110–115 ms prove, ~290k combined invocations/s, ~11.4 ms verify, 336 KB proof. Against proving the two types separately, the mixed proof costs ~1.10× the singles-sum — i.e. batching two hash types into one proof is close to free.
Multitable machinery overhead — control: the same 65,536 BLAKE3 invocations proved three ways.
Where the remaining prove overhead lives, from per-phase tracing: for one slot it is almost entirely the jagged transport in the open (the virtual-opening sumcheck ~3.8 ms, which provably cannot fuse, plus the second basis table ~2.2 ms — the union builds both
b_combinedandW_ρwhere the direct path builds one). The fused Ligerito open itself runs +0.3 ms over direct, so the fusion is doing its job. For the second slot the added cost is a per-slot tax rather than a per-invocation one — the compaction gather and the per-slot lincheck comb — so it amortizes as more invocations go into each slot.The ~2× verify at two slots is the per-slot lincheck comb replay,
O(nnz)in the circuit rather than the counts. It is why a mixed SHA-256 + BLAKE3 proof verifies in ~11.4 ms while two BLAKE3 slots take ~19 ms (SHA-256's comb is far cheaper). Comb delegation is the planned follow-on.CLI end-to-end:
flock_chain prove --mix blake3=100,sha2=37produces a 198 KB bundle that verifies in ~0.32 s.Single-hash direct path is untouched and byte-stable throughout.
Testing / oracle discipline
Every layer is gated by a hard oracle: single-slot full-utilization proofs are byte-identical to the pre-existing direct path (regression anchors in
union_roundtrip.rs,union_m6_fixtures.rs), and the union-column lincheck is cross-checked against brute-force dense MLEs (union_lincheck.rs). Plus end-to-end mixed roundtrips + tamper matrices (union_mixed.rs,jagged_roundtrip.rs) at non-power-of-two and partial-utilization counts. Fullflock-core/flock-proversuites, clippy-D warnings, and fmt are green.The same discipline covers the optimizations: in-place witness generation is pinned byte-identical against the copying path at full / partial / zero counts, and the integer-lane opening's block-granularity fold is pinned byte-identical against the explicit rotation it replaced.
Scope / follow-ons (intentionally out of this PR)
t = 61is a wash;t = 46is a clear win). Left always-on because the proof-size win is monotone int.u8scratch pool.ntt_layout_probe,jagged_throughput, and the throughput/control tests inunion_mixed.rs) are#[ignore]d.pcs_ligerito_backend_roundtriptest fails on a stale hand-rolled config (also fails onmain), left untouched.Update since the first review pass
Reviewer-visible change: the mixed proof-byte fixtures in
union_m6_fixtures.rswere deliberately re-pinned, because the integer-lane commit changes the committed arrangement for union/mixed proofs. Single-type anchors and the direct path are byte-identical and unchanged.The
num_lanesinteger-lane path, previously landed but dormant, is now wired into the union/mixed path. It was reached by a different route than the notes at the time anticipated: the scoped "reindex the jagged DP" approach turns out to be structurally blocked — with an integer lane count the lane indexe mod tis not a bit field, soW_ρ's extension,b_tildeand the assist would all needdiv/mod tinside jagged's read-once branching program, taking it from width 4 to ~2t states. High-bit lanes sidestep that entirely by making the relabelling a variable rotation.Other work in this range, all byte-identity-gated:
vec![F128::ZERO; …], which was paying a full memset plus a soft page fault per page. Union witness assembly 22.9 → 8.3 ms.🤖 Generated with Claude Code