feat(prover,executor): BLAKE3 6-round compression accelerator - #903
Draft
MauroToscano wants to merge 15 commits into
Draft
feat(prover,executor): BLAKE3 6-round compression accelerator#903MauroToscano wants to merge 15 commits into
MauroToscano wants to merge 15 commits into
Conversation
…anscripts The 2026-07-23 BLAKE3 work — an independent reference implementation, a three-anchor oracle harness, a chip design and a z3 soundness gate — was written to a session scratchpad under /private/tmp, never committed, and the scratchpad was gone by the time anyone went looking. Nothing named blake exists anywhere in this repo's history. Recovered by replaying the Write and Edit tool calls out of the subagent transcripts (5 Writes + 11 Edits, every Edit applied cleanly). Committing it so this cannot happen a third time: the keccak spike's artifacts went the same way, and the EC campaign's audits spent two days in the same state before being pushed. Evidence the recovery is faithful rather than plausible-looking: the gate runs and its structural negative controls all fire, 5/5 — rot_wrong_amount / swap_g_operand / wrong_iv / drop_ff_xor / wrong_msg_index each SAT as designed. Two fixtures are absent because they were downloaded or generated rather than written by a tool call, so the transcript never held them: the upstream official_test_vectors.json, and canonical_6round_vectors.json (regenerated by running test_oracle.py). The gate's positive controls and oracle anchors 1-2 therefore have NOT been re-run. Anchor 3 needs nothing external — Plonky3 is vendored at others/Plonky3/blake3-air. README.md says exactly how to restore full validation. Status is unchanged from when it stopped: design gate-proved, no Rust written, blocked on a protocol decision — sign-off on a named "6-round collision resistance" assumption. The gate proves the chip matches the reference, not that 6 rounds are secure. One correction this recovery makes possible: the EC lincomb2 design study justified its NUMS assumption with "like blake3's 6-round assumption". No such assumption was ever recorded in the spec, because this work never shipped — it was cited as precedent for something that had not happened.
…h run green
The recovery left two fixtures absent because they had been downloaded or
generated rather than written by a tool call, so no transcript held them. Both
are now restored, and every claim in DESIGN.md §9 reproduces end to end:
oracle [1] official vector set PASS 35/35 x 3 modes
[2] blake3 PyPI package SKIP (not installed)
[3] Plonky3 blake3-air PASS 20,000 compressions
gate G-function UNSAT, init+feed-forward UNSAT, 5/5 negative controls SAT,
4/4 positive controls SAT (6-round seeds 0-2 and 7-round),
width audit both bounds necessary. OVERALL: PASS
The positive controls were the gap that mattered: they are the only check that
would catch a per-instance wiring bug across the 48 unrolled G-functions, and
they were unrunnable until now.
PROVENANCE, because the label matters: official_test_vectors.json was
REGENERATED from the official blake3 Rust crate v1.8.5 (generator kept in
ground-truth/), not downloaded from upstream. It carries the official
parameters — the Elvish key, the 2019-12-27 context string, the same 35 input
lengths — and case 0 matches the independently known published digest. That is
a genuine, non-circular anchor: the crate is the authors' reference
implementation and is independent of blake3_ref.py. It is NOT the published
artifact, and test_oracle.py still calls it "Official test_vectors.json". Read
it as "checked against the official reference implementation using the official
vector parameters". Keeping the generator in-tree means this is reproducible
rather than another thing that evaporates.
Two independent reviews (different models, no coordination) found no
discrepancy in the primitive. One wrote a from-scratch BLAKE3 structured
deliberately differently and differentially tested 100k random compressions,
all 128 flag values x {6,7} rounds, a rounds sweep 0..8, and whole-hash over
227 lengths x 4 modes, with zero mismatches; it confirmed r < rounds-1, so the
classic 6-permutes-for-7-rounds off-by-one is absent. Independently,
blake3_ref.py reproduces the published known-answer vectors for "" and "abc"
exactly, which pins IV, G, all four rotations, the permutation and its count,
the feed-forward, the flag bits and LE packing in one shot.
README records what review found and did not fix:
- the harness prints "VALIDATION STATUS: VALIDATED ... anchored on official
test vectors + official PyPI package + Plonky3" even when anchor 2 SKIPs;
the status dict is written and never consulted. Observed firing.
- test_internal_consistency documents a feed-forward recomputation it does not
implement.
- DESIGN's internal Blake3 bus omits the input-to-output timestamp binding that
keccak — its own cited precedent — carries in both halves of its tuple.
Without it two compressions can swap outputs with every bus still balancing.
The gate models arithmetic only and cannot see it.
Two reviews, different models, no coordination between them. Both reached the same verdict independently: NO discrepancy in the primitive. Recording what each pinned, and — more usefully — what neither covered. Settled that no anchor covers: - Counter split order at t >= 2^32: t_lo -> v[12], t_hi -> v[13], verified BEHAVIOURALLY against the official crate via two independent counter paths (OutputReader::set_position, hazmat::HasherExt::set_input_offset) over counters 0..2^47, 44/44. Negative control breaks 5 of 6 chunk cases; the sixth is counter=0, correctly invariant under the swap. Closes ORACLE.md's O5. - Message schedule count AND direction: iterating permute from the identity reproduces all seven rows of the crate's MSG_SCHEDULE. Three mutants caught; a fourth (permute after the last round) is provably a no-op, so the guard cannot hide an off-by-one in either direction. - compress does not mutate its arguments; incremental update() == one-shot. Four more harness defects beyond the two already recorded: - the missing-file FileNotFoundError CASCADES — it kills anchors 2 and 3 and the canonical-vector emitter, which is why the gate's positive controls were blocked on an unrelated download. That single coupling is what made this recovery look worse than it was. - test_6round_derivation's first assertion is a tautology: compress_6round's body IS compress(rounds=6). ORACLE.md §2.6 calls it the "Code-diff anchor"; it establishes nothing. - compress() defaults to rounds=7, so a 6-round caller that omits the kwarg silently gets 7. Trace generators must use compress_6round — this should be enforced, not conventional. - ORACLE.md §5's ratio is internally inconsistent (~1/6 by its own numbers, not the "1/4-1/3" its prose claims); superseded by DESIGN.md §6's derived ~1/15. And the honest gap, recorded as the next reviewer's target: both passes established that the ORACLE defines the right function, so the gate's UNSATs are about the right function. NOBODY has audited the gate's transcription of that oracle into constraints — only its constants block was spot-checked. The EC campaign's equivalent audit found three premises the gate asserted and never read, one hiding a working forgery, so this is not hypothetical. The dangerous direction is a model STRONGER than what it models: it yields UNSAT where the real object is forgeable, and no positive anchor can catch it, because honest inputs satisfy a correct model and an over-strong one equally well.
…e banner Three findings from the review were recorded as "open" instead of being fixed. Fixing them; they were small. DESIGN — the input/output binding on the internal Blake3 bus is now MANDATORY. §1.1 defined a receive of (h, m, t, block_len, flags) and a separate send of out[0..16], both at multiplicity mu, and §3 listed TIMESTAMP_0/1 as "bus binding (internal variant may omit)". Omitting it is a real hole: with two compressions in a trace, row A can receive inputs_A and send out_B while row B does the reverse — every tuple appears exactly once on each side, so the bus BALANCES, and both callers read a result that is not the compression of their own input. keccak.rs, the chip this design copies its I/O idiom from, carries the timestamp in both halves of its internal bus precisely for this reason. §1.1 now states the requirement with the attack and the precedent, §3's "may omit" is gone, and it is item 10 of §7's soundness-critical list — together with the fact that the gate CANNOT catch a violation, because it models arithmetic and has no bus layer at all. Added item 11 for the same reason: MAIN 0 proves one G under free inputs, so a wrong column index in one of the 48 emitted instances is invisible to it; the concrete positive controls are what cover that. The third finding (the 3-op carry admits (1,0) and (0,1) for carry 1) is left alone on purpose — it does not admit a wrong sum, so it is a note, not a defect, and the README says so to stop someone "fixing" it into a bug. test_oracle.py — the banner no longer lies, and a missing fixture no longer cascades. It printed "VALIDATION STATUS: VALIDATED ... anchored on official test vectors + official PyPI package + Plonky3" unconditionally, including on runs where an anchor SKIPped: the status dict was written and never read. It now reports what actually ran (VALIDATED / PARTIALLY VALIDATED / NOT VALIDATED) and names the anchors it is NOT anchored on. Separately, one FileNotFoundError used to abort anchors 2 and 3 AND the canonical-vector emitter, which is what silently blocked the z3 gate's positive controls on an unrelated download; anchors are now independent and a missing fixture skips only itself. Anchor 1 is relabelled "Official-parameter vectors" and prints its provenance, because the shipped file is regenerated from the blake3 crate rather than downloaded — a genuine non-circular anchor, but not the published artifact. Both fixes verified to bite: with official_test_vectors.json removed, anchor 3 still runs, the canonical vectors are still emitted, and the banner degrades to PARTIALLY VALIDATED naming what it lost. Gate re-run after the changes: OVERALL PASS, positive controls included.
Two independent transcription audits of z3_blake_verify.py — one authored elsewhere (TRANSCRIPTION-AUDIT.md), one an executable 74-check suite (audit_gate_transcription.py + GATE-TRANSCRIPTION-AUDIT.md). Both ask the only dangerous question: is the gate's model STRONGER than the thing it models? A weaker model yields spurious SAT, which is safe; a stronger one yields UNSAT on a forgeable object, and no positive anchor can see that, because an honest witness satisfies a correct model and an over-strong one equally well. Headline: every equation in the gate matches the design it encodes, and the gate's bref_* reference is element-wise identical to the externally-anchored oracle (IV, MSG_PERMUTATION, G_CALLS, counter split across 2^32, and permute applications = max(rounds-1,0)). So the "gate proves the wrong function" risk is closed. The mutation sweep fires on 7/7 bug classes that ship no negative control, including a wrong column in G instance #7 — the per-instance wiring gap recorded as §7.11. One audit also ran anchor 2 live (PyPI, 92/92), so the historical counts now reproduce as recorded rather than on trust. THE FINDING, agreed by both and now written into DESIGN §7.4/§7.5: the "free range check" invariant is DECLARED, not derived. build_g returns each add output as fresh_word() = 4x BitVec(...,8), so byte range holds by construction in the model, and the gate proves the identical UNSAT for a chip that has the downstream XOR and for one that does not. Dropped, the sum is forgeable — a = b = 0x80000000, honest s = 0, forged s = 2^32 with carry = 0, satisfying every modelled constraint. Same blind spot for the message columns: m is declared as bytes, so the 32 explicit AreBytes sends §4.7 requires are unverifiable here, and without them a word has many F_p cell representations of one value. These invariants rest on the implementer; a green board is not evidence for them. Corrections forced into DESIGN.md: - §4.2/§7.3: the load-bearing bound set is AT LEAST ONE of {SLL_lo, SLL_hi} — the two SLLC bounds are not load-bearing at all, so only half the AreBytes sends per rotation carry soundness weight. The composed forgery with both SLL bounds dropped exists for exactly ONE input, X = 0xFFFFFFFF (forged Y = 0), exhaustive for r = 4 and r = 9 — the isolated control made it look reachable for arbitrary inputs. And the rotation OUTPUT needs no range check of its own; the recombine identities pin it. - §4.8: the recombine identity's body is linear, so 1 -> 2 after x mu, not the 2 -> 3 claimed. Overstated in the safe direction; "no constraint exceeds 3" is unaffected. - ground-truth/Cargo.toml needed an empty [workspace] table or cargo absorbs it into the parent workspace and the documented regeneration flow fails out of the box. That was a real bug in what I committed. Both audits independently verified the previous commit's fixes are real: the TIMESTAMP binding (with the keccak precedent confirmed at keccak.rs:264-319), the banner honesty fix, and the cascade fix — the last two exercised live by renaming the fixture away. Also committing the t >= 2^32 counter probe (ground-truth/src/bin/), and a .gitignore for target/, Cargo.lock, __pycache__ and the 114 MB venv. Re-verified after all edits: suite 74/74, gate OVERALL PASS.
DESIGN.md defers twice to `../keccak-verify/` — the cost model (tier2_cost_model.md) and the shift-identity bound-necessity proof (hwsl_inline_test.py Part 2). That directory died in the same 2026-07-23 session scratchpad this design was recovered from and was never committed: it exists on no branch, and `git log --all --diff-filter=A` finds it zero times. A reader following either citation chases nothing. Nothing rests on them. The cost arithmetic was recomputed from scratch (per-G 62 cells x 48 = 2,976; columns 3,155; sends 1,250; aux 1,875; total ~5,030, and ~1/15 of keccak-f) and checks out. The shift-identity result was re-derived symbolically over all 2^32 inputs by the 2026-07-29 transcription audits, which is stronger than the single-point check the lost file made — one audit flagged the missing file precisely because it had re-derived the result rather than trusting the citation. Fourth dead-citation instance this week. The others: lincomb2's "blake3 6-round assumption" precedent, which never existed because this very work never shipped; the EC gate's C5 pointing at a document containing no soundness argument; and the EC board's C4 invoked well outside its own text. Marking rather than deleting, so the provenance stays legible. Gate re-run after the edit: OVERALL PASS.
The Rust realization of the gate-proved design in thoughts/blake3/ (recovered spike, merged into this branch): syscall u64::MAX-2, executor implementation ported from the validated oracle, and a one-row-per-compression chip. ⚠ 6-round INTERNAL variant, not standard 7-round BLAKE3. Merkle/Fiat-Shamir replacement candidate; rests on the named A6R assumption recorded in thoughts/blake3/blake3-chip/IMPLEMENTATION.md, to be ratified in the spec before production use. ABI: x10 -> 8-aligned 176-byte region, h[32] | m[64] | t[8] | len,flags[8] | out[64]; the syscall writes the 64-byte output back. One compression digests a 64-byte message block — exactly one 2-to-1 Merkle merge of two 32-byte CVs. Chip (prover/src/tables/blake3.rs): fully unrolled Layout B — 3,219 main columns, 1,397 sends, 813 mu-gated constraints, max degree 3, ~5,316 cell-equiv per compression ~= 1/13.7 of a post-#889 keccak-f. The compression dataflow is written once (run_flow) and interpreted twice — columns (constraints + bus senders) and u32 values (trace fill + BITWISE multiplicities) — so sender/witness wiring cannot diverge by construction. Design decisions and deltas from DESIGN.md are in IMPLEMENTATION.md: two summed carry bits per 3-op add (ternary carry is degree 4 after gating), expression carries for 2-op adds, free rotr16/rotr8 byte relabels, inline mu-gated shift identities for rotr12/rotr7, explicit AreBytes for the never-XORed message/OLD_OUT/addr bytes; I/O is keccak.rs's Ecall + x10 register read + per-dword Memw idiom verbatim. Gates: 10/10 canonical 6-round oracle vectors through the syscall (full-width t — the counter-split order is load-bearing); ValueFlow == executor differential; wire audit (every mixing cell written exactly once); e2e test_prove_elfs_blake3 proves+verifies two CHAINED compressions — full bus balance across Ecall/Memw/ByteAlu/AreBytes/IsHalfword on the first run; keccak/ecsm suites unaffected; clippy clean. Known cost: FIXED_TABLE_COUNT 10 -> 11 — every proof now carries a >=4-row BLAKE3 AIR even when unused. This is the PR #871 regression shape at reduced scale; a real-block ABBA is required before merge, and the fallback is gating the table on use. Proof wire format changes (one more sub-proof). count_table_lengths does not yet count blake3 Memw ops (disk-spill sizing only; documented). scripts/gen_blake3_bench.sh generates the dependent-chain bench guest (1 row/compression -> padding-flush at N = 2^k).
|
Benchmark Results for modified programs 🚀
|
Chaining cost an 8-dword copy loop = ~82 of ~87 guest cycles per compression (measured on the box), and those copy cycles become CPU/MEMW rows that dilute the very table being measured. The prover's cost per ecall is identical either way — the executor runs every call and nothing dedupes rows (timestamps differ) — so the loop body drops to ~5 cycles and the trace is >90% blake3-saturated, matching gen_keccak_bench.sh's shape. The e2e correctness test keeps its chained two-call form.
…librated to Plonky3 exact and zisk 1% Multi-agent mining of the vendored references plus a synthesis under this repo's cost model (deg <=3 incl. mu-gating, LogUp aux 1.5 cells/send, the shipped syscall I/O idiom). Headline: ~651 table-only per 2-to-1 merge (in-place ABI variant), 8.2x under BLAKE3-6r table-only, ~5-9x end-to-end; the mu-gated degree cap alone doubles the permutation core vs ungated designs. Verdict: defensible number, but BLAKE3-6r already captures ~91% of the addressable per-merge saving vs keccak, and poseidon2 uniquely requires the verifier-hash switch, a GPU Merkle kernel, and a native-prover hashing slowdown. The gating measurement nobody has taken: hashing's share of a real recursion-verifier trace AFTER the blake3 switch.
The bus argument already pins mu to {0,1} indirectly (the Ecall receive
anchors mu>0 rows to a CPU ecall whose ECALL flag is IS_BIT; MEMW's width
flags are boolean), but that is a three-table argument written down nowhere.
One ungated degree-2 constraint makes it local, matching ecsm/commit. Also
corrects the constraint-layout doc: emission is grouped by op type across the
row, not per G.
Contributor
Author
Measured on the CPU bench box (32c/124GB, build e7b55fd, blowup 2, single-epoch continuations)
Matched resources — equal wall (96 vs 97.5 s) and equal peak heap (84 vs 82 GB): 524,288 blake3 2-to-1 merges vs 43,690 keccak permutations = 12.2× more merges per second, end-to-end. Per byte absorbed: 350 KB/s vs 61 KB/s (5.7×). Cell-model validation: measured marginal cost is 7,194 cell-equiv/compression (5,316 table + ~1,880 ecall/MEMW/CPU plumbing, from differencing count-elements at 2^18→2^19); at the measured 40.1 M cells/s the model predicts 5,574 merges/s vs 5,473 measured — within 2%. Throughput plateaus from 2^17 rows up; no memory cliff through 84 GB. Guest: Numbers are clean idle-box runs; a back-to-back sweep inflates the mid points ~1.5-2× through memory-reclaim contention — worth knowing when reproducing. |
Adds the BLAKE3_6R accelerator to the spec book. spec/src/blake3.toml machine-formalizes the chip's I/O-and-range surface: the ECALL binding, the x10 register read, all 22 MEMW dword operations, the pointer arithmetic and every explicit ARE_BYTES/IS_HALF/IS_BIT check — exactly the surface the z3 gate does not model (DESIGN.md §1.1, §7 items 4/5/10). The spec machinery derives 565 interactions from it. That number cross-checks the implementation: 565 + the 832 BYTE_ALU[XOR] lookups of the unrolled mixing core = 1,397 = the chip's exact interaction count, and the toml's column tally matches NUM_COLUMNS = 3,219. The mixing core is deliberately not re-formalized here; its normative sources are the single-source Rust dataflow (run_flow in prover/src/tables/blake3.rs, interpreted once as columns and once as witness) and the z3 gate that proves that dataflow equal to the reference function. spec/blake3.typ states that scope split explicitly rather than implying whole-chip coverage. The page also records A6R as a named assumption: 6-round BLAKE3 is collision-resistant and PRF-suitable in the same sense the 7-round function is believed to be (K12 precedent). The gate proves the chip computes 6-round BLAKE3 correctly; it neither proves nor addresses whether 6 rounds are secure, and any Merkle/Fiat-Shamir use invokes the assumption. The assumption-free alternative is priced next to it: the design is round-parameterised, and a 7-round instantiation — bit-compatible with official BLAKE3 parent merges — costs roughly 10-12% more per merge and needs no novel assumption. Registers the two missing ecall numbers in about_ecalls.typ: -3 (BLAKE3_6R, u64::MAX-2) and -11 (ECSM, u64::MAX-10). thoughts/blake3/README.md gets a truth pass — it claimed no Rust chip existed and that the transcription audit was still owed; both are stale as of PR #903.
Relayed by the project owner: external symmetric-cryptography experts judged removing one round (7->6) comfortable and removing two (7->5) explicitly not. The spec's A6R section now records this, fixes 6 rounds as the endorsed floor (sub-6 variants MUST NOT be instantiated), and reframes 7R as the interop/zero-assumption fallback rather than the preferred default.
Wording fix per the project owner: variants below 6 rounds are not formally ruled out — they are unavailable on the project's own authority and would require dedicated external cryptanalytic review of the reduced margin, rather than being an engineering or configuration decision.
Contributor
Author
Spec package added
Machine-checked I/O surface. The toml formalizes the chip's I/O-and-range surface — ECALL binding, the The spec machinery derives 565 interactions from the toml, which cross-checks the implementation: The 832 decomposes as 6 rounds x 8 G x 4 XORs x 4 bytes = 768, plus 64 for the two feed-forward XOR layers. The toml's column tally also matches The mixing core is intentionally not re-formalized in the toml; its normative sources are the single-source Rust dataflow ( A6R is now a named assumption in the spec, not folded into prose: 6-round BLAKE3 is collision-resistant and PRF-suitable in the same sense the 7-round function is believed to be (K12 precedent). The page is explicit that the gate proves the chip computes 6-round BLAKE3 correctly and says nothing about whether 6 rounds are secure, and that any Merkle/Fiat-Shamir use invokes the assumption. The external symmetric-crypto review is recorded alongside it: removing one round (7 -> 6) was judged comfortable, removing two (7 -> 5) explicitly was not, which makes 6 rounds the endorsed floor. Sub-6 variants are not formally ruled out, but they are expert-gated — adopting one needs a dedicated cryptanalytic review of the reduced-round margin, not an engineering or configuration decision. The assumption-free alternative is priced next to it: the design is round-parameterised, and a 7-round instantiation — bit-compatible with official BLAKE3 parent merges — costs roughly 10-12% more per merge and needs no assumption beyond standard BLAKE3. Also registers the two previously-missing ecall numbers in Book build is green ( z3
|
Ran z3_blake_verify.py --full on 2026-08-06. It took ~145 min and exited 1 with OVERALL: FAIL, but the failure is a resource limit, not a finding: all four monolithic queries (round, rounds=2, rounds=6, rounds=7) returned `unknown`, not `sat`. `unknown` is z3's timeout return — the checks set a solver timeout and return check() directly (z3_blake_verify.py:320-321, :340-341) while the verdict tests == unsat (line 553), so a timeout scores False and pulls OVERALL down. The four budgets sum to 140 min against ~145 min wall, so every check burned its whole allowance. Nothing was disproven and nothing was proven monolithically. The fast board is unchanged and green: G-function UNSAT, init+feed-forward UNSAT, 5/5 negative controls SAT, 4/4 positive controls SAT including the concrete full 6- and 7-round pipelines against the oracle vectors. Records this in IMPLEMENTATION.md "Gates run" and TRANSCRIPTION-AUDIT.md §6 (which said PENDING) as ATTEMPTED-INCONCLUSIVE — explicitly NOT a pass. DESIGN.md §7 item 11's "run --full's monolithic UNSAT before shipping Rust" precondition is attempted but not satisfied. Also corrects TRANSCRIPTION-AUDIT.md §5 Finding 2, which cited those monolithic UNSATs as backing the per-instance G-coverage argument. They do not back it, so that argument now rests on the concrete positive controls and the per-instance index mutant alone. Remediation either way: rerun with a much larger timeout budget on a server (the run is single-threaded and CPU-bound), and/or restructure the monolithic query as round-by-round induction rather than one flat bit-vector problem.
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.
What
A BLAKE3 6-round compression accelerator: syscall (
u64::MAX - 2), executor implementation, and a gate-proved single-row chip — the Rust realization of the design that was taken to a z3-proved model inthoughts/blake3/(recovered spike, in-branch).⚠ This is the 6-round internal variant, not standard 7-round BLAKE3. It is a Merkle / Fiat–Shamir replacement candidate; its security rests on the named assumption A6R recorded in
thoughts/blake3/blake3-chip/IMPLEMENTATION.md, which must be ratified in the spec before production use.Why
Post-#889, a keccak-f permutation costs ~72,672 committed cell-equivalents; this chip costs ~5,316 per compression ≈ 1/13.7 of a keccak at the 2-to-1 Merkle use case (measured cell law pending a prove run on the bench box; the DESIGN-derived internal-variant figure is 5,030, +5.7% syscall I/O overhead).
How
blake3_compress_6roundported from the validated oracle (thoughts/blake3/blake3-oracle/blake3_ref.py); 176-byte state region ABI (h|m|t|len,flags|out), 8-aligned, alignment + overflow rejected. Differentially pinned by the 10 canonical 6-round vectors (full-widtht— the counter-split order is load-bearing and was behaviourally verified against the official crate).prover/src/tables/blake3.rs): one row per compression, fully unrolled (Layout B). 3,219 main columns, 1,397 sends, 813 μ-gated constraints, max degree 3. The compression dataflow is written once (run_flow) and interpreted twice — columns (constraints + senders) and u32 values (trace + BITWISE multiplicities) — so sender/witness wiring cannot diverge by construction.IMPLEMENTATION.md):emit_add_pair-style expression carry, no committed cell (DESIGN §4.3; the §3 column table double-counts these).Soundness gates
z3_blake_verify.py, in-branch): G-function UNSAT, init+feed-forward UNSAT, 5 negative controls SAT, field-level bound-necessity controls SAT.ValueFlow↔ executor differential; wire audit (every mixing cell written exactly once).test_prove_elfs_blake3: two chained compressions (second consumes the first's output, overwrites non-zero out region) → prove + verify = full bus balance across Ecall/Memw/ByteAlu/AreBytes/IsHalfword.The gate cannot see bus wiring or lookup coverage (its own documentation, DESIGN §7 items 4/5/11) — that is what the vector + e2e + single-dataflow structure covers.
Costs / caveats
FIXED_TABLE_COUNT10 → 11: every proof carries a ≥4-row BLAKE3 AIR even when unused. This is the PR perf(ec): pair EC byte range checks, and replace ecrecover's four scalar muls with one joint chain (−61.9% EC cells, z3-gated, unconditional) #871 regression shape at 1/3 scale — a real-block ABBA is required before merge; if it shows, the fix is gating the table on use (proof-format change) rather than deleting the chip.count_table_lengths(disk-spill sizing) doesn't count blake3 Memw ops yet — noted in IMPLEMENTATION.md, not exercised by benches.Bench plan
scripts/gen_blake3_bench.sh(dependent-chain guest, 1 row/compression → padding-flush at N = 2^k). Absolute throughput + vs-keccak ratio on the CPU box, same methodology as the keccak numbers (single-epoch continuations, N flush against a power of two).