diff --git a/Benchmarks/RecursiveVerifier.lean b/Benchmarks/RecursiveVerifier.lean new file mode 100644 index 00000000..20626d85 --- /dev/null +++ b/Benchmarks/RecursiveVerifier.lean @@ -0,0 +1,118 @@ +import Ix.Aiur.Meta +import Ix.Aiur.Protocol +import Ix.Aiur.Compiler +import Ix.Aiur.Statistics +import Ix.MultiStark +import Blake3.Rust +import Ix.TracingTexray + +open Aiur + +/-! +# Recursive-verifier cost benchmark + +Proves `factorial(5)` with the multi-stark backend, then runs the in-circuit +recursive verifier (`verify_multi_stark_proof`) over that proof and reports its +cost. Mirrors the setup of `Tests/MultiStark.lean::endToEndSuite`, but measures +cost instead of asserting accept/reject. + +``` +lake exe bench-recursive-verifier # execute + FFT + PROVE (texray) — ~5 s / ~7 GB +lake exe bench-recursive-verifier --execute-only # skip the prove (FFT/exec only) +``` + +What it reports: +* **In-circuit FFT cost** (`Σ width·height·log₂(height)`) — the prover-work / RAM + driver for proving the verifier. This is the headline recursion-cost metric. +* By default, the **end-to-end STARK prove** of the verifier, with `tracing-texray` + emitting the per-stage timeline (`stage1_commit` / `quotient` / `fri_open`) and + RAM Δ/peak (~5 s, ~7 GB peak). Pass `--execute-only` to skip the prove on a + memory-constrained box. + +Determinism note: the multi-stark prover is **non-deterministic under `parallel`** +(the same statement yields byte-different valid proofs run-to-run), so the +verifier authenticates slightly different Merkle paths and its FFT drifts ~±15%. +Aiur *execution* FFT is deterministic; pin the inner proof with +`RAYON_NUM_THREADS=1` for exactly reproducible numbers. +-/ + +def factorialProgram : Source.Toplevel := ⟦ + pub fn factorial(n: G) -> G { + match n { + 0 => 1, + _ => n * factorial(n - 1), + } + } +⟧ + +def recCommitParams : Aiur.CommitmentParameters := { logBlowup := 2, capHeight := 0 } +def innerFri : Aiur.FriParameters := + { logFinalPolyLen := 0, maxLogArity := 1, numQueries := 3, + commitProofOfWorkBits := 20, queryProofOfWorkBits := 0 } + +def u64le (n : Nat) : Array UInt8 := + (Array.range 8).map (fun i => UInt8.ofNat ((n >>> (8 * i)) % 256)) + +/-- Serialize the public claims for the verifier's IO channel (matches the +in-circuit `read_claims` wire format). -/ +def serializeClaims (claims : Array (Array Aiur.G)) : ByteArray := Id.run do + let mut out : Array UInt8 := u64le claims.size + for c in claims do + out := out ++ u64le c.size + for g in c do + out := out ++ u64le g.val.toNat + return ⟨out⟩ + +def main (args : List String) : IO Unit := do + let doProve := !args.contains "--execute-only" + -- Inner proof: factorial(5) under the multi-stark backend. + let facCompiled ← match factorialProgram.compile with + | .ok c => pure c | .error e => IO.eprintln s!"factorial compile failed: {e}"; return + let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams + let facIdx := facCompiled.getFuncIdx `factorial |>.get! + IO.println "proving inner factorial(5)…" + let (claim, proof, _) := facSystem.prove innerFri facIdx #[Aiur.G.ofNat 5] default + let proofBytes := proof.toBytes + -- Serialize proof (advice, channel 0), vk (channel 1), claims (channel 2), plus + -- the Blake3-bound vk/claims digests and FRI params as public input. + let proofGs : Array Aiur.G := proofBytes.data.map .ofUInt8 + let vkBytes := facSystem.vkBytes + let sysDigestInput : Array Aiur.G := (Blake3.Rust.hash vkBytes).val.data.map .ofUInt8 + let vkGs : Array Aiur.G := vkBytes.data.map .ofUInt8 + let claimBytes := serializeClaims #[claim] + let claimsDigestInput : Array Aiur.G := (Blake3.Rust.hash claimBytes).val.data.map .ofUInt8 + let claimGs : Array Aiur.G := claimBytes.data.map .ofUInt8 + let friParamInput : Array Aiur.G := + #[Aiur.G.ofNat innerFri.numQueries, Aiur.G.ofNat innerFri.commitProofOfWorkBits, + Aiur.G.ofNat recCommitParams.logBlowup] + let pubInput : Array Aiur.G := sysDigestInput ++ claimsDigestInput ++ friParamInput + let io := (((default : IOBuffer).extend 0 #[Aiur.G.ofNat 0] proofGs).extend + 1 #[Aiur.G.ofNat 0] vkGs).extend 2 #[Aiur.G.ofNat 0] claimGs + IO.println s!"inner proof: {proofBytes.size} bytes" + -- Compile the verifier toplevel and run it over the proof. + let vTop ← match MultiStark.multiStark with + | .ok t => pure t | .error e => IO.eprintln s!"verifier merge failed: {e}"; return + let vCompiled ← match vTop.compile with + | .ok c => pure c | .error e => IO.eprintln s!"verifier compile failed: {e}"; return + let vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof |>.get! + IO.println "executing verify_multi_stark_proof…" + match vCompiled.bytecode.execute vIdx pubInput io with + | .error e => IO.eprintln s!"verifier execution failed: {e}" + | .ok (out, _, qc) => + let stats := Aiur.computeStats vCompiled qc + IO.println s!"verifier output (1=accept): {out}" + IO.println s!"\n=== recursive verifier in-circuit cost ===" + IO.println s!"totalFftCost = {stats.totalFftCost}" + IO.println "\n=== per-circuit breakdown (top FFT contributors) ===" + Aiur.printStats stats + if doProve then + -- PROVE the verifier execution (multi-stark) with texray: per-stage timeline + -- + RAM Δ/peak (~7 GB). + IO.println "\n=== PROVING the verifier (multi-stark + texray) ===" + TracingTexray.init {} + let vSystem := AiurSystem.build vCompiled.bytecode recCommitParams + let t0 ← IO.monoNanosNow + let (_, vproof, _) := vSystem.prove innerFri vIdx pubInput io + let nbytes := vproof.toBytes.size -- force the (lazy, pure) prove to run + let t1 ← IO.monoNanosNow + IO.println s!"verifier PROVE time: {(Float.ofNat (t1 - t0)) / 1e9} s, proof {nbytes} bytes" diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 1906378b..6e4d53d6 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -37,6 +37,7 @@ lake exe bench-typecheck --ixe [names…] [flags] --texray force the tracing-texray timeline + RAM breakdown on. --no-texray force it off. Default: on iff `--json` was NOT given, so a plain local run gets the breakdown while a JSON run stays quiet. + --execute-only stop after Phase 1 (FFT/exec metrics); skip the proving phase. ``` For each constant the harness STARK-checks `Ix.Claim.check addr none` (the full @@ -149,6 +150,8 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do -- subject-only: check just the target (`verify_const`, trusting its deps) -- instead of re-checking the whole transitive closure (`verify_claim`). let subjectOnly := p.hasFlag "subject-only" + -- --execute-only: stop after Phase 1 (FFT/exec metrics), skip proving. + let executeOnly := p.hasFlag "execute-only" -- Default: trace iff we're not in JSON/bencher mode. let useTexray := if p.hasFlag "texray" then true @@ -216,6 +219,11 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do IO.FS.writeFile path (Json.mkObj (results.map Result.toJsonEntry).toList).pretty | none => pure () + if executeOnly then + writeJson (execed.map (·.1)) + IO.println s!"── execute-only: skipped proving ({execed.size} constants) ──" + return 0 + -- Phase 2: prove cheap→expensive. Refine each entry with its prove-time as it -- lands. Install texray first so the prove spans (timeline + RAM Δ/peak) render. if useTexray then TracingTexray.init {} @@ -252,6 +260,7 @@ def typecheckCmd : Cli.Cmd := `[Cli| "subject-only"; "Check only each target itself (verify_const, trusting its deps) instead of re-checking its whole transitive closure (verify_claim)." texray; "Force the tracing-texray timeline + RAM breakdown on (per-prove spans on stderr)." "no-texray"; "Force the breakdown off. Default: on iff --json was not given." + "execute-only"; "Stop after Phase 1 (FFT/exec metrics); skip proving." ARGS: ...names : String; "Fully-qualified constant name(s) to benchmark (e.g. `Nat.add_comm String.append`). Optional if `--manifest` is given." diff --git a/Cargo.lock b/Cargo.lock index 13f6bf3b..9ce74b0f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2039,10 +2039,11 @@ dependencies = [ [[package]] name = "multi-stark" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/multi-stark.git?rev=9ecab51d553445c0cc7b571af00a76b8a83a6f8c#9ecab51d553445c0cc7b571af00a76b8a83a6f8c" +source = "git+https://github.com/argumentcomputer/multi-stark.git?rev=0b260d7b23f239c196a7d03bb8fef3a548669b73#0b260d7b23f239c196a7d03bb8fef3a548669b73" dependencies = [ "bincode", "p3-air", + "p3-blake3", "p3-challenger", "p3-commit", "p3-dft", @@ -2457,6 +2458,16 @@ dependencies = [ "tracing", ] +[[package]] +name = "p3-blake3" +version = "0.5.1" +source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +dependencies = [ + "blake3", + "p3-symmetric", + "p3-util", +] + [[package]] name = "p3-challenger" version = "0.5.1" diff --git a/Cargo.toml b/Cargo.toml index e3a2ae7f..40b8a6c4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -46,7 +46,7 @@ itertools = "0.14.0" log = "0.4" memmap2 = "0.9" mimalloc = { version = "0.1", default-features = false } -multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "9ecab51d553445c0cc7b571af00a76b8a83a6f8c" } +multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "0b260d7b23f239c196a7d03bb8fef3a548669b73" } num-bigint = "0.4.6" quickcheck = "1.0.3" quickcheck_macros = "1.0.0" diff --git a/Ix/MultiStark.lean b/Ix/MultiStark.lean index f30912ef..2241a1bc 100644 --- a/Ix/MultiStark.lean +++ b/Ix/MultiStark.lean @@ -2,6 +2,7 @@ module public import Ix.Aiur.Meta public import Ix.IxVM.Core public import Ix.IxVM.ByteStream +public import Ix.IxVM.Blake3 public import Ix.MultiStark.Goldilocks public import Ix.MultiStark.Deserialize public import Ix.MultiStark.Keccak @@ -15,12 +16,12 @@ public import Ix.MultiStark.Tests The recursive verifier. Its public statement is purely existential: *"there exists a valid multi-stark proof, under the FRI parameters given as public -input, for the constraint system with this keccak-256 digest and these public +input, for the constraint system with this Blake3 digest and these public claims."* The proof itself is **non-deterministic advice** (fed on IO channel 0, never hashed or otherwise bound as a public input): the Fiat-Shamir transcript replay plus the Merkle/OOD/FRI checks are exactly what make any accepted advice a valid proof — a hash binding of the proof bytes would add nothing to the -statement, while costing one keccak-f per 136 bytes in-circuit. +statement, while costing an extra in-circuit hash over those bytes. The verifying key and claims, by contrast, ARE digest-bound (`system_digest`, `claims_digest`): they determine *what was proven*. @@ -35,8 +36,8 @@ public section namespace MultiStark def entrypoints := ⟦ - -- Public inputs: the keccak-256 digests of the verifying key and the claims - -- (4 little-endian u64 lanes each) plus the variable FRI parameters. The + -- Public inputs: the Blake3 digests of the verifying key and the claims + -- (32 bytes = 4 little-endian u64 lanes each) plus the variable FRI parameters. The -- proof is pure non-deterministic advice on IO channel 0 — see the module -- docstring. One stream per channel (0 = proof, 1 = vk, 2 = claims), each -- registered under key `[0]` on its channel. @@ -47,19 +48,19 @@ def entrypoints := ⟦ let (proof, rest) = read_proof(bytes); assert_eq!(load(rest), ListNode.Nil); -- Verifying key (`System`) from IO channel 1: bind the bytes - -- to the public keccak-256 `system_digest`, then reconstruct the system. + -- to the public Blake3 `system_digest`, then reconstruct the system. let (sidx, slen) = io_get_info(1, [0]); let sbytes = #read_byte_stream(1, sidx, slen); - assert_eq!(keccak256(sbytes), system_digest); + assert_eq!(b3_to_digest(blake3(sbytes)), system_digest); let (sys, srest) = read_system(sbytes); assert_eq!(load(srest), ListNode.Nil); -- Public claims (`&[&[Val]]`) from IO channel 2: bind the bytes to the - -- public keccak-256 `claims_digest`, then deserialize. Binding them as a + -- public Blake3 `claims_digest`, then deserialize. Binding them as a -- public input is what makes the lookup argument sound (a prover cannot -- choose claims adaptively). let (cidx, clen) = io_get_info(2, [0]); let cbytes = #read_byte_stream(2, cidx, clen); - assert_eq!(keccak256(cbytes), claims_digest); + assert_eq!(b3_to_digest(blake3(cbytes)), claims_digest); let (claims, crest) = read_claims(cbytes); assert_eq!(load(crest), ListNode.Nil); -- Structural + accumulator + PCS checks. @@ -73,12 +74,12 @@ def entrypoints := ⟦ /-- The standalone Multi-STARK verifier toplevel: `core` (lists/options) + `byteStream` (`U64`, `flatten_u64`, `read_byte_stream`, …) + the deserializer, -the keccak-256 implementation, and the entrypoint. -/ +the Blake3 hash, and the entrypoint. -/ def multiStark : Except Aiur.Global Aiur.Source.Toplevel := do let t ← IxVM.core.merge IxVM.byteStream let t ← t.merge MultiStark.goldilocks let t ← t.merge deserialize - let t ← t.merge keccak + let t ← t.merge IxVM.blake3 let t ← t.merge systemDeserialize let t ← t.merge pcs let t ← t.merge verifier diff --git a/Ix/MultiStark/Pcs.lean b/Ix/MultiStark/Pcs.lean index 024adb87..85dc2227 100644 --- a/Ix/MultiStark/Pcs.lean +++ b/Ix/MultiStark/Pcs.lean @@ -6,37 +6,23 @@ public import Ix.MultiStark.Keccak /-! # PCS (FRI) verification -`multi-stark/src/verifier.rs` calls `pcs.verify(coms_to_verify, opening_proof, -&mut challenger)` — a `TwoAdicFriPcs` FRI verification: query openings, Merkle -authentication paths, FRI folding consistency. This is the heaviest part of the -verifier and is being ported here in stages. +Ports `multi-stark/src/verifier.rs`'s `pcs.verify(...)` — a `TwoAdicFriPcs` FRI +verification: Merkle `verify_batch` (binary tree, multi-height injection), the +challenger continuation, the FRI fold chain (`open_input` / `verify_query`), and +the final-polynomial check. -## Stage 1 — Merkle (MMCS) hash primitives (this file, done + validated) +## Merkle (MMCS) hash primitives -The input/commit-phase commitments are `MerkleTreeMmcs` over the keccak hasher -configured in `multi-stark/src/types.rs`: +The input/commit-phase commitments are a `MerkleTreeMmcs` over Blake3 +(`multi-stark/src/types.rs`): -* leaf hash : `SerializingHasher>` - — serialize each `Goldilocks` element to its canonical `u64`, then run a - padding-free **overwrite-mode** sponge (rate 17 lanes, capacity 8, output 4) - built on the keccak-f[1600] permutation (reused from `Keccak.lean`). -* compression: `CompressionFunctionFromHasher, 2, 4>` - — hash the 8 lanes of two concatenated digests into a 4-lane digest. +* leaf hash : `SerializingHasher` — serialize each `Goldilocks` element + to its canonical 8 LE bytes, then `blake3` the row. +* compression: `CompressionFunctionFromHasher` — `blake3(a || b)` + of two 32-byte child digests. -`PaddingFreeSponge` differs from keccak-256 (`Keccak.lean`): no `10*1` padding, -rate 17 *lanes* (not 136 bytes), and each input block **overwrites** the rate -region (keccak-256 XORs). A full block triggers a permute; a final partial block -permutes once iff it absorbed ≥1 element; an empty trailing block does not -permute. - -Validated against `multi-stark`'s own hasher (see `pcs_hash_test`, reference -values from the `pcs_ref_values` test in `multi-stark/src/types.rs`). - -## Stage 2+ — TODO - -Merkle `verify_batch` (binary tree, multi-height injection), challenger -threading, the FRI fold chain (`open_input` / `verify_query`), and the final -polynomial check. Until those land, `pcs_verify` remains an accept-stub. +`Digest` is `[U64; 4]` = the 32 Blake3 output bytes (8-byte LE groups), so the +deserialized caps round-trip unchanged. The Blake3 gadget is `Ix/IxVM/Blake3.lean`. -/ public section @@ -45,90 +31,59 @@ namespace MultiStark def pcs := ⟦ -- ========================================================================== - -- PaddingFreeSponge in overwrite mode. + -- Blake3 MMCS hash primitives. -- - -- Lanes are the keccak `Lane` type (`&[U8; 8]`, LE). A `U64` opened value is - -- (for an honest, canonical proof) exactly the 8 LE bytes of a lane, so a lane - -- is just `store(u64)`. The 25-lane keccak `State` and `keccak_f_fold` are - -- reused from `Keccak.lean`. + -- The input/commit-phase commitments are a `MerkleTreeMmcs` over Blake3: + -- leaf = `blake3(serialized row bytes)` (`SerializingHasher`) + -- 2-to-1 = `blake3(a || b)` (`CompressionFunctionFromHasher`) + -- A row's `Val`s are serialized as 8 LE bytes each (canonical `u64`). `Digest` + -- is `[U64; 4]` = the 32 blake3 output bytes (8-byte LE groups), so the + -- deserialized caps round-trip with zero change to the deserializer. -- ========================================================================== - -- Take one input element as the next rate lane, or keep the existing state - -- lane `dflt` when the input is exhausted. The flag is 1 iff an input element - -- was consumed (input is consumed front-to-back, so the per-block flags are a - -- run of 1s followed by 0s). - fn u64_pick(vals: List‹U64›, dflt: Lane) -> (Lane, List‹U64›, G) { - match load(vals) { - ListNode.Nil => (dflt, vals, 0), - ListNode.Cons(x, rest) => (store(x), rest, 1), - } - } - - -- Absorb the input lanes into the state, 17 (= RATE) at a time, overwriting - -- the rate region. After a FULL block of 17, permute and continue. A final - -- partial block (1..16 elements) permutes once; an exactly-empty trailing - -- block does not permute (matches `PaddingFreeSponge::hash_iter`). - fn pf_absorb(sp: State, vals: List‹U64›) -> State { - let old = load(sp); - let (l0, v1, f0) = u64_pick(vals, old[0]); - let (l1, v2, _f1) = u64_pick(v1, old[1]); - let (l2, v3, _f2) = u64_pick(v2, old[2]); - let (l3, v4, _f3) = u64_pick(v3, old[3]); - let (l4, v5, _f4) = u64_pick(v4, old[4]); - let (l5, v6, _f5) = u64_pick(v5, old[5]); - let (l6, v7, _f6) = u64_pick(v6, old[6]); - let (l7, v8, _f7) = u64_pick(v7, old[7]); - let (l8, v9, _f8) = u64_pick(v8, old[8]); - let (l9, v10, _f9) = u64_pick(v9, old[9]); - let (l10, v11, _fa) = u64_pick(v10, old[10]); - let (l11, v12, _fb) = u64_pick(v11, old[11]); - let (l12, v13, _fc) = u64_pick(v12, old[12]); - let (l13, v14, _fd) = u64_pick(v13, old[13]); - let (l14, v15, _fe) = u64_pick(v14, old[14]); - let (l15, v16, _ff) = u64_pick(v15, old[15]); - let (l16, v17, f16) = u64_pick(v16, old[16]); - let sp2 = store([l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, - l14, l15, l16, old[17], old[18], old[19], old[20], old[21], - old[22], old[23], old[24]]); - match f16 { - 1 => pf_absorb(keccak_f_fold(sp2, 24), v17), - _ => match f0 { - 0 => sp2, - _ => keccak_f_fold(sp2, 24), - }, + -- 8 LE bytes of a `U64` lane (`SerializingHasher`: a `Val` is 8 LE bytes). + fn b3_u64_onto(v: U64, tail: ByteStream) -> ByteStream { + store(ListNode.Cons(v[0], store(ListNode.Cons(v[1], store(ListNode.Cons(v[2], + store(ListNode.Cons(v[3], store(ListNode.Cons(v[4], store(ListNode.Cons(v[5], + store(ListNode.Cons(v[6], store(ListNode.Cons(v[7], tail)))))))))))))))) + } + -- All lanes of a row, in order. + fn b3_row_onto(row: List‹U64›, tail: ByteStream) -> ByteStream { + match load(row) { + ListNode.Nil => tail, + ListNode.Cons(v, rest) => b3_u64_onto(v, b3_row_onto(rest, tail)), } } - - -- Hash a list of `u64` lanes (a serialized field-element row, or two - -- concatenated digests) into a 4-lane `Digest`. - fn pf_sponge_u64(vals: List‹U64›) -> Digest { - let z = store([0u8; 8]); - let init = store([z, z, z, z, z, z, z, z, z, z, z, z, z, z, z, z, z, z, z, z, - z, z, z, z, z]); - let sp = pf_absorb(init, vals); - let s = load(sp); - [load(s[0]), load(s[1]), load(s[2]), load(s[3])] + -- A 4-byte blake3 output word. + fn b3_w4_onto(w: [U8; 4], tail: ByteStream) -> ByteStream { + store(ListNode.Cons(w[0], store(ListNode.Cons(w[1], store(ListNode.Cons(w[2], + store(ListNode.Cons(w[3], tail)))))))) + } + -- The 32 bytes of a blake3 digest (`[[U8;4];8]`, word order = output order). + fn b3_flatten_onto(h: [[U8; 4]; 8], tail: ByteStream) -> ByteStream { + b3_w4_onto(h[0], b3_w4_onto(h[1], b3_w4_onto(h[2], b3_w4_onto(h[3], + b3_w4_onto(h[4], b3_w4_onto(h[5], b3_w4_onto(h[6], b3_w4_onto(h[7], tail)))))))) + } + -- blake3 output `[[U8;4];8]` -> `Digest` `[U64;4]` (two words per LE lane). + fn b3_to_digest(h: [[U8; 4]; 8]) -> Digest { + [[h[0][0], h[0][1], h[0][2], h[0][3], h[1][0], h[1][1], h[1][2], h[1][3]], + [h[2][0], h[2][1], h[2][2], h[2][3], h[3][0], h[3][1], h[3][2], h[3][3]], + [h[4][0], h[4][1], h[4][2], h[4][3], h[5][0], h[5][1], h[5][2], h[5][3]], + [h[6][0], h[6][1], h[6][2], h[6][3], h[7][0], h[7][1], h[7][2], h[7][3]]] + } + -- The 32 bytes of a `Digest`. + fn b3_digest_bytes_onto(d: Digest, tail: ByteStream) -> ByteStream { + b3_u64_onto(d[0], b3_u64_onto(d[1], b3_u64_onto(d[2], b3_u64_onto(d[3], tail)))) } - -- The MMCS leaf hash of a single matrix row (`SerializingHasher` over the row - -- of canonical `u64`s). For a leaf joining several same-height matrices, the - -- rows are concatenated first (see `verify_batch`, future work). + -- The MMCS leaf hash of a row (`SerializingHasher`). fn mmcs_hash_row(row: List‹U64›) -> Digest { - pf_sponge_u64(row) + b3_to_digest(blake3(b3_row_onto(row, store(ListNode.Nil)))) } - - -- The MMCS 2-to-1 compression: hash the 8 lanes of two concatenated digests. + -- The MMCS 2-to-1 compression (`CompressionFunctionFromHasher`). fn mmcs_compress(a: Digest, b: Digest) -> Digest { - let t0 = store(ListNode.Nil); - let t1 = store(ListNode.Cons(b[3], t0)); - let t2 = store(ListNode.Cons(b[2], t1)); - let t3 = store(ListNode.Cons(b[1], t2)); - let t4 = store(ListNode.Cons(b[0], t3)); - let t5 = store(ListNode.Cons(a[3], t4)); - let t6 = store(ListNode.Cons(a[2], t5)); - let t7 = store(ListNode.Cons(a[1], t6)); - let t8 = store(ListNode.Cons(a[0], t7)); - pf_sponge_u64(t8) + b3_to_digest(blake3(b3_digest_bytes_onto(a, + b3_digest_bytes_onto(b, store(ListNode.Nil))))) } -- ========================================================================== @@ -208,7 +163,8 @@ def pcs := ⟦ } -- The joint leaf hash of all matrices at log-height `target`. fn leaf_hash_at(rows: List‹List‹U64››, lhs: List‹G›, target: G) -> Digest { - pf_sponge_u64(canon_lanes(concat_at(rows, lhs, target))) + -- The joint Blake3 leaf hash of all matrices at log-height `target`. + mmcs_hash_row(canon_lanes(concat_at(rows, lhs, target))) } -- Inject the leaf hash of any matrices at log-height `lh` (if present) via a diff --git a/Ix/MultiStark/Tests.lean b/Ix/MultiStark/Tests.lean index 80148123..6d26ed43 100644 --- a/Ix/MultiStark/Tests.lean +++ b/Ix/MultiStark/Tests.lean @@ -105,7 +105,7 @@ def tests := ⟦ store(ListNode.Cons(5u8, store(ListNode.Cons(4u8, store(ListNode.Cons(3u8, store(ListNode.Cons(2u8, store(ListNode.Cons(1u8, store(ListNode.Nil))))))))))))))))); let (bits, _i, _o) = ch_sample_bits(input, store(ListNode.Nil), 20); - assert_eq!(bits_to_num(bits), 799146); + assert_eq!(bits_to_num(bits), 1019203); 1 } @@ -121,23 +121,23 @@ def tests := ⟦ -- α_pcs (output empty ⇒ flush), then α_fri (CONSECUTIVE ⇒ thread output). let (apcs, input, o1) = pcs_sample_ext(input, store(ListNode.Nil)); let (afri, input, o2) = pcs_sample_ext(input, o1); - assert_eq!(limb_to_field(apcs[0]), 2882912772410685996); - assert_eq!(limb_to_field(apcs[1]), 910933442133595775); - assert_eq!(limb_to_field(afri[0]), 14440140149289897216); - assert_eq!(limb_to_field(afri[1]), 8092267645441512944); + assert_eq!(limb_to_field(apcs[0]), 17795849114622667264); + assert_eq!(limb_to_field(apcs[1]), 4116843485681689527); + assert_eq!(limb_to_field(afri[0]), 11768399386651893439); + assert_eq!(limb_to_field(afri[1]), 10948618071942561750); -- observe commit (clears output), sample β. let v2 = [239u8, 190u8, 173u8, 222u8, 0u8, 0u8, 0u8, 0u8]; -- 0x00000000deadbeef let (input, _oc) = ch_observe_val(input, v2); let (beta, input, _ob) = pcs_sample_ext(input, store(ListNode.Nil)); - assert_eq!(limb_to_field(beta[0]), 10456048119516576995); - assert_eq!(limb_to_field(beta[1]), 3173538015651228593); + assert_eq!(limb_to_field(beta[0]), 12096272534537655203); + assert_eq!(limb_to_field(beta[1]), 11431251745744402868); -- observe final_poly coeff + log_arity (each a Val), then sample the index. let v3 = [4u8, 3u8, 2u8, 1u8, 13u8, 12u8, 11u8, 10u8]; -- 0x0a0b0c0d01020304 let v4 = [2u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]; -- 0x0000000000000002 let (input, _o3) = ch_observe_val(input, v3); let (input, _o4) = ch_observe_val(input, v4); let (bits, _bi, _bo) = ch_sample_bits(input, store(ListNode.Nil), 20); - assert_eq!(bits_to_num(bits), 336138); + assert_eq!(bits_to_num(bits), 458922); 1 } @@ -215,27 +215,26 @@ def tests := ⟦ 1 } pub fn pcs_hash_test() -> G { - -- LEAF3: hash([1,2,3]) + -- Leaf hashes: `blake3` over the row's canonical 8-LE-byte serialization + -- (`SerializingHasher`). Reference digests from the `gen_pcs_refs` + -- generator in `multi-stark`, cross-checked with `b3sum`. let d3 = mmcs_hash_row(build_range(0, 3)); - assert_eq!(assert_digest(d3, 0xc55a6a1beaea9fec, 0xc8f0dbc4c59ec440, - 0xacb1295de9bfe032, 0x445d569d3dfc9543), 1); - -- LEAF17: exactly one full block, no extra permute. + assert_eq!(assert_digest(d3, 4163513704854067712, 9384471110237386207, + 13671380075168847140, 1533933974187331481), 1); let d17 = mmcs_hash_row(build_range(0, 17)); - assert_eq!(assert_digest(d17, 0x388da73622e8fdd5, 0xec687be9c50d2218, - 0x528d145dfe6571af, 0xd2eb808dfba4703c), 1); - -- LEAF22: full block + 5-element partial (two permutes), >20 lanes. + assert_eq!(assert_digest(d17, 8431665677194841246, 4495111673672851816, + 7709594803249897978, 12683511314940902790), 1); let d22 = mmcs_hash_row(build_range(0, 22)); - assert_eq!(assert_digest(d22, 520358013996801752, 12301199992631688477, - 8732686820159480415, 10883226686987971725), 1); - -- LEAF20: full block + 3-element partial (two permutes). + assert_eq!(assert_digest(d22, 14017803411919507972, 9236340131056405306, + 11356520758956579629, 2008168271701183309), 1); let d20 = mmcs_hash_row(build_range(0, 20)); - assert_eq!(assert_digest(d20, 0xec696847be88d358, 0x202861c67ff4cec8, - 0x88e006a48aaa0661, 0xabaddb9d32ecd024), 1); - -- COMPRESS([1,2,3,4],[5,6,7,8]) + assert_eq!(assert_digest(d20, 8822819174011220231, 9835070768970864367, + 9646176123001837413, 1210344881395534089), 1); + -- Compression: `blake3(a_bytes || b_bytes)` of two 32-byte child digests. let c = mmcs_compress([u64_of(1u8), u64_of(2u8), u64_of(3u8), u64_of(4u8)], [u64_of(5u8), u64_of(6u8), u64_of(7u8), u64_of(8u8)]); - assert_eq!(assert_digest(c, 0xda1ef0642722b22e, 0x4851efdbdb2a2fd8, - 0x37e8ff900ea95d47, 0xa153eee7805376fb), 1); + assert_eq!(assert_digest(c, 16432952784711837466, 12565756115161032165, + 6915939387221618258, 11123773279136987111), 1); 1 } @@ -256,32 +255,32 @@ def tests := ⟦ let lhs = store(ListNode.Cons(3, store(ListNode.Cons(2, store(ListNode.Cons(1, store(ListNode.Nil))))))); let ibits = store(ListNode.Cons(1, store(ListNode.Cons(0, store(ListNode.Cons(1, store(ListNode.Nil))))))); -- authentication path SIB0, SIB1, SIB2 (each a Digest = [U64; 4]). - let sib0 = [[9u8, 36u8, 179u8, 127u8, 205u8, 83u8, 105u8, 203u8], - [95u8, 229u8, 105u8, 223u8, 113u8, 55u8, 97u8, 122u8], - [135u8, 8u8, 65u8, 248u8, 163u8, 163u8, 68u8, 81u8], - [9u8, 11u8, 20u8, 209u8, 10u8, 168u8, 151u8, 125u8]]; - let sib1 = [[227u8, 58u8, 255u8, 213u8, 77u8, 152u8, 42u8, 77u8], - [113u8, 86u8, 2u8, 151u8, 97u8, 63u8, 58u8, 45u8], - [228u8, 139u8, 228u8, 194u8, 182u8, 115u8, 107u8, 221u8], - [248u8, 16u8, 30u8, 93u8, 176u8, 36u8, 205u8, 88u8]]; - let sib2 = [[236u8, 144u8, 115u8, 218u8, 140u8, 5u8, 86u8, 229u8], - [95u8, 186u8, 252u8, 175u8, 21u8, 247u8, 153u8, 25u8], - [113u8, 78u8, 92u8, 200u8, 212u8, 175u8, 247u8, 47u8], - [78u8, 145u8, 206u8, 54u8, 175u8, 155u8, 165u8, 206u8]]; + let sib0 = [[229u8, 114u8, 223u8, 248u8, 35u8, 4u8, 112u8, 11u8], + [133u8, 106u8, 85u8, 90u8, 195u8, 164u8, 85u8, 141u8], + [13u8, 243u8, 100u8, 106u8, 55u8, 39u8, 129u8, 101u8], + [0u8, 39u8, 10u8, 147u8, 198u8, 106u8, 172u8, 30u8]]; + let sib1 = [[234u8, 150u8, 163u8, 93u8, 30u8, 78u8, 129u8, 226u8], + [24u8, 27u8, 220u8, 33u8, 92u8, 142u8, 194u8, 191u8], + [193u8, 63u8, 223u8, 131u8, 67u8, 230u8, 55u8, 63u8], + [169u8, 209u8, 214u8, 101u8, 245u8, 28u8, 141u8, 193u8]]; + let sib2 = [[167u8, 176u8, 170u8, 74u8, 66u8, 157u8, 36u8, 153u8], + [220u8, 192u8, 39u8, 69u8, 198u8, 24u8, 123u8, 147u8], + [63u8, 5u8, 74u8, 98u8, 77u8, 73u8, 181u8, 252u8], + [134u8, 86u8, 33u8, 32u8, 240u8, 13u8, 134u8, 153u8]]; let proof = store(ListNode.Cons(sib0, store(ListNode.Cons(sib1, store(ListNode.Cons(sib2, store(ListNode.Nil))))))); let (root, capidx) = mmcs_root(rows, lhs, ibits, proof, 3); assert_eq!(capidx, 0); - assert_eq!(assert_digest(root, 0x6211b9a1a116a006, 0x435ee98e1504880f, - 0x900c7274b9a215f, 0xf6e3aaac5dcd90bd), 1); + assert_eq!(assert_digest(root, 4722047561722553901, 2839201037098837684, + 4926058068911485563, 1219861215742277604), 1); -- tamper: perturb m0's first opened value → root must change. let bad0 = store(ListNode.Cons(u64_of(99u8), store(ListNode.Cons(u64_of(12u8), store(ListNode.Nil))))); let bad_rows = store(ListNode.Cons(bad0, store(ListNode.Cons(row1, store(ListNode.Cons(row2, store(ListNode.Nil))))))); - let cap = store(ListNode.Cons([[6u8, 160u8, 22u8, 161u8, 161u8, 185u8, 17u8, 98u8], - [15u8, 136u8, 4u8, 21u8, 142u8, 233u8, 94u8, 67u8], - [95u8, 33u8, 154u8, 75u8, 39u8, 199u8, 0u8, 9u8], - [189u8, 144u8, 205u8, 93u8, 172u8, 170u8, 227u8, 246u8]], + let cap = store(ListNode.Cons([[45u8, 230u8, 248u8, 40u8, 61u8, 21u8, 136u8, 65u8], + [180u8, 102u8, 50u8, 238u8, 76u8, 222u8, 102u8, 39u8], + [123u8, 114u8, 106u8, 220u8, 182u8, 223u8, 92u8, 68u8], + [228u8, 55u8, 152u8, 7u8, 80u8, 209u8, 237u8, 16u8]], store(ListNode.Nil))); assert_eq!(mmcs_verify(cap, rows, lhs, ibits, proof, 3), 1); assert_eq!(mmcs_verify(cap, bad_rows, lhs, ibits, proof, 3), 0); diff --git a/Ix/MultiStark/Verifier.lean b/Ix/MultiStark/Verifier.lean index eed9c09a..62d3a338 100644 --- a/Ix/MultiStark/Verifier.lean +++ b/Ix/MultiStark/Verifier.lean @@ -19,7 +19,7 @@ The Rust verifier runs these steps: column widths. 2. **Accumulator balance** — the last intermediate accumulator is zero (all lookup pushes/pulls cancel). -3. **Fiat-Shamir replay** — reconstruct the Keccak challenger: observe +3. **Fiat-Shamir replay** — reconstruct the challenger: observe commitments / trace heights / claims, sample (lookup, fingerprint, α, ζ). 4. **PCS verification** — FRI opening proofs (see `Ix/MultiStark/Pcs.lean`). 5. **OOD evaluation** — recompute the composition polynomial at ζ and check @@ -47,13 +47,14 @@ The Rust verifier runs these steps: test runner, `Tests/MultiStark.lean`): the verifier accepts the honest proof and rejects a tampered claim. -### Stubbed / TODO +* Step 4: the PCS/FRI opening proof (`pcs_fri_verify`, `Ix/MultiStark/Pcs.lean`) + — Merkle `verify_batch`, the challenger continuation, the FRI fold chain, and + the final-polynomial check. + +### Notes * Base-field samples are rejection-sampled (`ch_sample_field`): a raw 8-byte limb in the band `[p, 2⁶⁴)` (probability ≈ 2⁻³²) is discarded and redrawn, consuming challenger bytes exactly as `SerializingChallenger64::sample` does. -* The PCS opening proof (`pcs_verify`) is still an accept-stub. With the PCS - stubbed, this verifier checks every algebraic relation except FRI proximity, - so it is not yet fully sound. -/ public section @@ -83,8 +84,8 @@ def verifier := ⟦ -- ========================================================================== -- Fiat-Shamir challenger: `SerializingChallenger64>`. The inner byte challenger keeps an `input` buffer; a - -- `sample` with empty `output` flushes (`input := output := keccak256(input)`) + -- Blake3, 32>>`. The inner byte challenger keeps an `input` buffer; a + -- `sample` with empty `output` flushes (`input := output := blake3(input)`) -- and pops bytes from the END of the hash output. The outer layer serializes -- field elements as 8 little-endian bytes and samples field elements as -- 8-byte little-endian u64s. @@ -136,8 +137,11 @@ def verifier := ⟦ match load(output) { ListNode.Cons(b, rest) => (b, input, rest), ListNode.Nil => - let h = keccak256(input); - let fwd = digest_onto(h, store(ListNode.Nil)); + -- `HashChallenger` flush: hash the `input` buffer with + -- blake3; `b3_flatten_onto` (Pcs.lean) gives the 32 output bytes, popped + -- from the END (rev), with the `input := output := hash` update. + let h = blake3(input); + let fwd = b3_flatten_onto(h, store(ListNode.Nil)); let rev = rev_onto(fwd, store(ListNode.Nil)); let &ListNode.Cons(b, rest) = rev; (b, fwd, rest), @@ -182,11 +186,18 @@ def verifier := ⟦ (c0, c1, i1, o1) } + -- Prepend the 8 elements of `d` onto `tail` (generic list helper). + fn cons8(d: [G; 8], tail: List‹G›) -> List‹G› { + store(ListNode.Cons(d[0], store(ListNode.Cons(d[1], store(ListNode.Cons(d[2], + store(ListNode.Cons(d[3], store(ListNode.Cons(d[4], store(ListNode.Cons(d[5], + store(ListNode.Cons(d[6], store(ListNode.Cons(d[7], tail)))))))))))))))) + } + -- `sample_bits(n)` (FRI query index). `SerializingChallenger64::sample_bits` -- reads one 8-byte sample as a little-endian u64 and masks the low `n` bits. -- We return the low `n` bits as a list (LSB first = the leaf→root Merkle/FRI - -- path), built from the 8 sampled bytes' bit decompositions (reusing keccak's - -- `cons8`), truncated to `n`. + -- path), built from the 8 sampled bytes' bit decompositions (via `cons8`), + -- truncated to `n`. fn sample8_bits(bytes: [U8; 8]) -> List‹G› { cons8(u8_bit_decomposition(bytes[0]), cons8(u8_bit_decomposition(bytes[1]), @@ -213,7 +224,7 @@ def verifier := ⟦ -- Append (observe) 8 little-endian bytes of `b` at the END of the challenger -- input buffer. The transcript is held front-to-back (front = first observed = - -- first hashed, matching `keccak256`'s absorption order), so an observation + -- first hashed, matching `blake3`'s absorption order), so an observation -- appends — `b8_onto` PREPENDS, hence the `list_concat`. fn snoc_b8(input: ByteStream, b: [U8; 8]) -> ByteStream { list_concat(input, b8_onto(b, store(ListNode.Nil))) @@ -782,8 +793,6 @@ def verifier := ⟦ -- Step 5: OOD composition/quotient identity for every circuit. let _ood = ood_loop(circuits, prep_indices, log_degrees, accs, stage1, stage2, prep_opt, q_opened, 0, acc0, 0, lch, fch, alpha, zeta); - -- Step 4: FRI PCS proximity + opening consistency, continuing the same - -- Fiat-Shamir transcript past ζ (observe opened values → α, βs, query). pcs_fri_verify(post_zeta_input, stage1, stage2, q_opened, prep_opt, opening, s1c, s2c, qc, prep_cap, circuits, prep_indices, log_degrees, zeta, list_length(circuits), log_blowup, num_queries, commit_pow_bits), diff --git a/Tests/FFI/Lifecycle.lean b/Tests/FFI/Lifecycle.lean index 79099038..0ca615a9 100644 --- a/Tests/FFI/Lifecycle.lean +++ b/Tests/FFI/Lifecycle.lean @@ -6,6 +6,7 @@ module public import LSpec public import Ix.Keccak +public import Blake3.Rust public import Tests.Sha256 public import Ix.Ixon public import Tests.Gen.Ixon @@ -69,6 +70,50 @@ def keccakLargeInputTests : TestSeq := let result2 := Keccak.hash large test "Keccak large input deterministic" (result == result2) +/-! ## Blake3 external object lifecycle tests -/ + +/-- Basic hash lifecycle against the official BLAKE3 empty-input test vector. -/ +def blake3BasicTests : TestSeq := + -- Official BLAKE3 vector: blake3("") = af1349b9f5f9a1a6…cae41f3262. + let expected : ByteArray := ⟨#[ + 175, 19, 73, 185, 245, 249, 161, 166, 160, 64, 77, 234, 54, 220, 201, 73, + 155, 203, 37, 201, 173, 193, 18, 183, 204, 154, 147, 202, 228, 31, 50, 98 + ]⟩ + let emptyResult := (Blake3.Rust.hash ByteArray.empty).val + test "Blake3 empty matches official vector" (emptyResult == expected) ++ + test "Blake3 empty produces 32 bytes" (emptyResult.size == 32) ++ + -- Determinism: same input twice. + let input : ByteArray := ⟨#[1, 2, 3]⟩ + test "Blake3 deterministic" ((Blake3.Rust.hash input).val == (Blake3.Rust.hash input).val) + +/-- Multi-update lifecycle: init → update × N → finalize. Creates N+1 external + `Hasher` objects (exercising the destructor path); must equal the one-shot hash. -/ +def blake3MultiUpdateTests : TestSeq := + let combined : ByteArray := ⟨#[1, 2, 3, 4, 5, 6, 7, 8, 9]⟩ + let singleHash := (Blake3.Rust.hash combined).val + let multiHash := Id.run do + let mut h := Blake3.Rust.Hasher.init () + h := h.update ⟨#[1, 2, 3]⟩ + h := h.update ⟨#[4, 5, 6]⟩ + h := h.update ⟨#[7, 8, 9]⟩ + return (h.finalizeWithLength 32).val + test "Blake3 multi-update == single" (singleHash == multiHash) ++ + -- Many updates to stress the external object destructor. + let manyHash := Id.run do + let mut h := Blake3.Rust.Hasher.init () + for i in [:20] do + h := h.update ⟨#[i.toUInt8]⟩ + return (h.finalizeWithLength 32).val + let manyExpected := (Blake3.Rust.hash ⟨Array.range 20 |>.map Nat.toUInt8⟩).val + test "Blake3 many-update == single" (manyHash == manyExpected) + +/-- Large-input determinism, mirroring the Keccak large-input test. -/ +def blake3LargeInputTests : TestSeq := + let large : ByteArray := ⟨Array.range 4096 |>.map Nat.toUInt8⟩ + let result := (Blake3.Rust.hash large).val + test "Blake3 large input (4096 bytes)" (result.size == 32) ++ + test "Blake3 large input deterministic" (result == (Blake3.Rust.hash large).val) + /-! ## SHA256 hashing tests -/ def sha256Tests : TestSeq := @@ -275,6 +320,9 @@ public def suite : List TestSeq := [ keccakBasicTests, keccakMultiUpdateTests, keccakLargeInputTests, + blake3BasicTests, + blake3MultiUpdateTests, + blake3LargeInputTests, sha256Tests, serdeTests, serdePropertyTest, diff --git a/Tests/MultiStark.lean b/Tests/MultiStark.lean index fb852fb9..15b2b5b2 100644 --- a/Tests/MultiStark.lean +++ b/Tests/MultiStark.lean @@ -5,7 +5,7 @@ public import Ix.Aiur.Meta public import Ix.Aiur.Protocol public import Ix.Aiur.Compiler public import Ix.MultiStark -public import Ix.Keccak +public import Blake3.Rust /-! # Tests for the Multi-STARK recursive verifier @@ -16,14 +16,14 @@ runners (registered in `Tests/Main.lean`, both wired into `ci.yml`): * **`multi-stark`** — `selfTestSuite`. Executes the verifier's primitive `*_test` entrypoints (`Ix/MultiStark/Tests.lean`), each of which validates one - primitive (keccak MMCS sponge/compress, Merkle `verify_batch`, the challenger, + primitive (Blake3 MMCS leaf/compress, Merkle `verify_batch`, the challenger, FRI fold + reduced openings, non-native Goldilocks/ExtGoldilocks arithmetic) - against the Rust reference values in `multi-stark/src/types.rs`. Cheap: just + against the Rust reference values from `multi-stark` (`gen_pcs_refs`). Cheap: just bytecode execution, no proving. The in-circuit `assert_eq!`s do the checking; every entrypoint returns `1` on success. * **`recursive-verifier`** — `endToEndSuite`. The full pipeline (~1.5 min, - dominated by proving + the keccak-heavy verifier executions): + dominated by proving + the verifier executions): 1. prove `factorial(5) = 120` with the Multi-STARK backend, 2. feed that proof as non-deterministic advice (IO channel 0; vk on 1, claims on 2) and run `verify_multi_stark_proof` over it — it must accept, @@ -60,7 +60,7 @@ def expectErr (descr : String) (e : Except ε α) : TestSeq := /-- The verifier's primitive self-test entrypoints (`Ix/MultiStark/Tests.lean`) and a one-line description of what each validates against the Rust reference. -/ def selfTests : List (Lean.Name × String) := [ - (`pcs_hash_test, "keccak MMCS sponge/compress match reference"), + (`pcs_hash_test, "Blake3 MMCS leaf/compress match reference"), (`pcs_merkle_test, "Merkle verify_batch matches reference (root + tamper)"), (`sample_bits_test, "challenger sample_bits matches reference"), (`pcs_challenger4_test, "PCS challenger continuation (α_pcs/α_fri/β/index) matches reference"), @@ -143,13 +143,13 @@ def endToEndSuite : IO UInt32 := do let expectedClaim := buildClaim facIdx input #[Aiur.G.ofNat 120] let proofBytes := proof.toBytes - -- ── serialize proof (advice) + vk + claims, with public keccak-256 digests ── + -- ── serialize proof (advice) + vk + claims, with public Blake3 digests ── let proofGs : Array Aiur.G := proofBytes.data.map .ofUInt8 let vkBytes := facSystem.vkBytes - let sysDigestInput : Array Aiur.G := (Keccak.hash vkBytes).data.map .ofUInt8 + let sysDigestInput : Array Aiur.G := (Blake3.Rust.hash vkBytes).val.data.map .ofUInt8 let vkGs : Array Aiur.G := vkBytes.data.map .ofUInt8 let claimBytes := serializeClaims #[claim] - let claimsDigestInput : Array Aiur.G := (Keccak.hash claimBytes).data.map .ofUInt8 + let claimsDigestInput : Array Aiur.G := (Blake3.Rust.hash claimBytes).val.data.map .ofUInt8 let claimGs : Array Aiur.G := claimBytes.data.map .ofUInt8 -- Public input = vk digest ++ claims digest ++ (num_queries, commit_pow, log_blowup). let friParamInput : Array Aiur.G := @@ -182,7 +182,7 @@ def endToEndSuite : IO UInt32 := do let badClaim : Array Aiur.G := claim.set! (claim.size - 1) (Aiur.G.ofNat 121) let badClaimBytes := serializeClaims #[badClaim] let badClaimInput : Array Aiur.G := - sysDigestInput ++ ((Keccak.hash badClaimBytes).data.map .ofUInt8) ++ friParamInput + sysDigestInput ++ ((Blake3.Rust.hash badClaimBytes).val.data.map .ofUInt8) ++ friParamInput -- ── run the (expensive) checks, then assert ───────────────────────────────── IO.println "recursive-verifier (proving + recursive verification, ~1.5 min)…" diff --git a/crates/aiur/src/vk_codec.rs b/crates/aiur/src/vk_codec.rs index f48273fb..d15e59e1 100644 --- a/crates/aiur/src/vk_codec.rs +++ b/crates/aiur/src/vk_codec.rs @@ -172,10 +172,10 @@ impl W { self.usize(c.stage_2_width); } fn commitment(&mut self, c: &Commitment) { - // MerkleCap: Vec<[u64; 4]> digests (raw words, no field reduction). - self.vec(c.roots(), |w, digest: &[u64; 4]| { - for &word in digest { - w.u64(word); + // MerkleCap: Vec<[u8; 32]> Blake3 digests (raw bytes). + self.vec(c.roots(), |w, digest: &[u8; 32]| { + for &byte in digest { + w.u8(byte); } }); } @@ -335,7 +335,13 @@ impl<'a> R<'a> { }) } fn commitment(&mut self) -> Result { - let caps = self.vec(|r| Ok([r.u64()?, r.u64()?, r.u64()?, r.u64()?]))?; + let caps = self.vec(|r| { + let mut d = [0u8; 32]; + for b in d.iter_mut() { + *b = r.u8()?; + } + Ok(d) + })?; Ok(Commitment::from(caps)) } fn option( diff --git a/lakefile.lean b/lakefile.lean index 2b99b20c..e8380219 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -122,6 +122,10 @@ lean_exe «bench-typecheck» where root := `Benchmarks.Typecheck supportInterpreter := true +lean_exe «bench-recursive-verifier» where + root := `Benchmarks.RecursiveVerifier + supportInterpreter := true + end Benchmarks section IxApplications