feat(primitives): formally verified BMT inclusion proof + CI - #89
Closed
mfw78 wants to merge 4 commits into
Closed
Conversation
…l test
Add the first slice of the formal-verification effort for the BMT hash, the
Swarm content-address kernel that every chunk hashes through.
- verification/bmt/Bmt.fst: F* model of the BMT inclusion proof, mirroring
nectar-primitives::bmt and the Book of Swarm (§2.2.2). Proves completeness
(honest proofs verify) and soundness (a forged segment that verifies implies a
keccak collision) with no admits; the only assumptions are abstract keccak and
its collision-resistance.
- crates/primitives/src/bmt/spec_equivalence.rs: differential test pinning the
optimised Hasher (zero-tree rollup, all-zeros fast path, rayon) to a naive
brute-force reference across random inputs, boundary sizes, the all-zeros path,
and proof round-trips with tamper-detection.
- verification/bmt/{README.md,Makefile}: methodology, spec-to-code mapping, and
`make verify` to re-run the proof via nix.
F* proves the reference is sound; the Rust test proves the production code equals
the reference; the Book of Swarm validates the reference matches the spec.
Add a verification workflow with two gates: an F* job that proves verification/bmt/Bmt.fst (F* from the nix binary cache), and a Rust job that runs the bmt::spec_equivalence differential tests. Path-filtered to bmt/verification changes on PRs; always run on main and in merge queues.
#90) Stacks on #89 — base branch is `verification/bmt-fstar`, because this change uses the `bmt::spec_equivalence` differential test added there as its correctness gate. Re-target to `main` after #89 merges. ## What Performance optimization of the BMT hasher and inclusion-proof generation. **Output hashes are byte-identical** — every change is gated by the spec-equivalence differential test (optimised `Hasher` vs the F\*-proven-sound brute-force reference: 512 random inputs, all boundary sizes, the all-zeros path, all 128 proof indices + tamper detection). 26/26 bmt tests pass on both branches. This is the synthesis of three parallel optimization explorations (sequential / parallel / unsafe lenses); only changes that measured as a real win were kept. ### `hasher.rs` - `Keccak256::finalize()` already returns a `B256` — drop the redundant `B256::from_slice(finalize().as_slice())` copy at every one of the ~127 nodes. - Allocation-free iterative bottom-up sweep over a fixed `[B256; 64]` stack array, collapsing levels in place with zero-subtree short-circuiting (replaces the recursive sequential hash). - Full-body (4096) path recurses with rayon only down to 512-byte subtrees, then hands each off to the iterative sweep — ~8-way leaf parallelism instead of a deep per-node `rayon::join`. - Word-wide `is_all_zeros` (usize lanes via `align_to`). ### `proof.rs` - `generate_proof` builds the 128 leaves into one `[B256; 128]` stack array and collapses in place — **8 heap allocations per proof → 0**. Fully safe: an `unsafe`/`get_unchecked` variant measured no faster (proof time is keccak-dominated). Discarded a flat `par_chunks` leaf strategy — it regressed the large sizes versus divide-and-conquer `rayon::join`. ## Benchmarks AMD Ryzen 9 7940HS (16 cores), `performance` governor, `cargo bench -p nectar-primitives --bench bmt_bench`, 8 interleaved rounds with alternating run-order. **Best-case (full-boost) medians** shown: on this laptop AMD Core Performance Boost swings single-thread clocks ~1.7× with thermal headroom, so the per-round minimum is the reproducible figure. | Benchmark | Baseline | Optimised | Speedup | |---|---|---|---| | `bmt_hash/64` | 2.39 µs | 2.34 µs | 1.02× | | `bmt_hash/128` | 2.75 µs | 2.68 µs | 1.03× | | `bmt_hash/256` | 3.54 µs | 3.49 µs | 1.01× | | `bmt_hash/512` | 5.61 µs | 5.53 µs | 1.01× | | `bmt_hash/1024` | 9.89 µs | 9.70 µs | 1.02× | | `bmt_hash/2048` | 19.07 µs | 18.57 µs | 1.03× | | **`bmt_hash/4096`** (full chunk) | **45.15 µs** | **31.16 µs** | **1.45×** | | **`bmt_proof/generate`** | **118.3 µs** | **36.36 µs** | **3.25×** | | `bmt_proof/verify` | 2.65 µs | 2.27 µs | 1.17× | **Headlines:** - **4096-byte hashing — every full chunk — is ~1.45× faster** (stable on the median too, ~1.40×, since the all-core path saturates boost). Swarm splits all data into 4096-byte chunks, so this is the dominant path. - **Proof generation is ~3.25× faster** (zero heap allocations). - Single-threaded partial-chunk sizes (64–2048) are at parity (1.01–1.03×) — same keccak work, no regression at any size. ## Correctness Output is byte-identical; the `bmt::spec_equivalence` differential test (added in #89) is the gate — the optimised hasher is checked against the brute-force reference that #89's F\* proof establishes is sound. `cargo test -p nectar-primitives --lib bmt`: **26 passed, 0 failed**. clippy + rustfmt clean.
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 subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
First slice of the formal-verification effort, targeting the BMT hash — the Swarm content-address kernel that every chunk hashes through. A divergence here is catastrophic (wrong addresses, failed proof-of-custody, self-fork off the network), and the logic is pure and finite, so it's the ideal first target.
What's in here
1. Machine-checked F* proof —
verification/bmt/Bmt.fstnectar-primitives::bmtimplements it and as the Book of Swarm specifies it (§2.2.2).admits, including the elementary index-arithmetic helpers. The only assumptions are the two intended cryptographic axioms: keccak is abstract and collision-resistant.2. Differential test —
crates/primitives/src/bmt/spec_equivalence.rsHasher(zero-tree rollup, all-zeros fast path, rayon) to a deliberately naive brute-force reference: 512 random(data, span)cases, every boundary size, the all-zeros path, and proof round-trips for all 128 segment indices with tamper-detection.3. CI —
.github/workflows/verification.ymlfstar-proof: provesBmt.fst(F* from the public nix binary cache, pinning the same version as local dev).bmt-differential: runs thebmt::spec_equivalencetests.mainand in merge queues.How the guarantees compose
unsafe, new parallelism) as long as the test stays green.keccak(span_le ‖ bmt_root)address wrap.Verifying locally
Next increments (see
verification/bmt/README.md)