From 0f01e8233c066bcd1307b421723c484b651c7365 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 29 Jun 2026 21:18:30 +0000 Subject: [PATCH 1/4] perf: Switch Aiur from Keccak to Blake3 hashing Pins multi-stark at the blake3 branch rebased onto the Generic config refactor (75fcd1b), and migrates ix accordingly: - AiurSystem::build takes FriParameters alongside CommitmentParameters: the config (GoldilocksBlake3Config) is constructed once at build time and prove/verify no longer take FRI parameters. The FFI externs and every Lean call site shift the parameter from prove/verify to build. - The verifying-key codec writes the five FRI parameters after the commitment parameters, since the config's challenger seed is derived from all seven and the config doesn't expose them back. - The in-circuit verifier mirrors the new Fiat-Shamir transcript: challenger seeded with b"multi-stark/v0" + the 7 protocol parameters, observe_shape (circuit count + 6 metadata words per circuit, captured as raw wire limbs during VK deserialization), intermediate accumulators observed between stage_2 and alpha, and length-prefixed claim observation. - The public FRI-parameter inputs (num_queries, commit_pow_bits) are now also asserted against the digest-bound verifying key's values. --- Benchmarks/Aiur.lean | 6 +- Benchmarks/Blake3.lean | 4 +- Benchmarks/IxVM.lean | 4 +- Benchmarks/RecursiveVerifier.lean | 14 +-- Benchmarks/Sha256.lean | 4 +- Benchmarks/Typecheck.lean | 14 +-- Cargo.lock | 13 ++- Cargo.toml | 2 +- Ix/Aiur/Protocol.lean | 28 ++--- Ix/Cli/ProveCmd.lean | 10 +- Ix/Cli/VerifyCmd.lean | 4 +- Ix/MultiStark.lean | 27 ++--- Ix/MultiStark/Pcs.lean | 160 ++++++++++----------------- Ix/MultiStark/SystemDeserialize.lean | 85 +++++++++----- Ix/MultiStark/Tests.lean | 81 +++++++------- Ix/MultiStark/Verifier.lean | 129 +++++++++++++++------ Tests/Aiur/Common.lean | 8 +- Tests/FFI/Lifecycle.lean | 48 ++++++++ Tests/MultiStark.lean | 24 ++-- crates/aiur/src/synthesis.rs | 36 +++--- crates/aiur/src/vk_codec.rs | 113 +++++++++++++------ crates/ffi/src/aiur/protocol.rs | 36 ++---- 22 files changed, 499 insertions(+), 351 deletions(-) diff --git a/Benchmarks/Aiur.lean b/Benchmarks/Aiur.lean index ef8bd0e39..adda1d460 100644 --- a/Benchmarks/Aiur.lean +++ b/Benchmarks/Aiur.lean @@ -86,9 +86,9 @@ def main : IO Unit := do countInE2E let compiled ← benchStepE "compile" Aiur.Source.Toplevel.compile toplevel let system ← benchStep "build AiurSystem" - (Aiur.AiurSystem.build compiled.bytecode) commitmentParameters + (Aiur.AiurSystem.build compiled.bytecode commitmentParameters) friParameters let funIdx := compiled.getFuncIdx `main |>.get! let (claim, proof, _) ← benchStep "prove fib 10" - (Aiur.AiurSystem.prove system friParameters funIdx #[10]) default (oneShot := true) + (Aiur.AiurSystem.prove system funIdx #[10]) default (oneShot := true) let _ ← benchStepE "verify fib 10" - (Aiur.AiurSystem.verify system friParameters claim) proof + (Aiur.AiurSystem.verify system claim) proof diff --git a/Benchmarks/Blake3.lean b/Benchmarks/Blake3.lean index 74c368926..d8d047724 100644 --- a/Benchmarks/Blake3.lean +++ b/Benchmarks/Blake3.lean @@ -34,7 +34,7 @@ def blake3Bench : IO $ Array BenchReport := do | throw (IO.userError "Compilation failed") let some funIdx := compiled.getFuncIdx `blake3_bench | throw (IO.userError "Aiur function not found") - let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters + let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters bgroup "prove blake3" { oneShot := true, avgThroughput := true, report := true } do for dataSize in dataSizes do for numHashes in numHashesPerProof do @@ -47,7 +47,7 @@ def blake3Bench : IO $ Array BenchReport := do ioBuffer.extend 0 #[.ofNat idx] data throughput (.ElementsAndBytes numHashes.toUInt64 (dataSize * numHashes).toUInt64 "hashes") bench s!"dataSize={dataSize} numHashes={numHashes}" - (aiurSystem.prove friParameters funIdx #[Aiur.G.ofNat numHashes]) ioBuffer + (aiurSystem.prove funIdx #[Aiur.G.ofNat numHashes]) ioBuffer def main : IO Unit := do let _ ← blake3Bench diff --git a/Benchmarks/IxVM.lean b/Benchmarks/IxVM.lean index 57f391876..39593b6fc 100644 --- a/Benchmarks/IxVM.lean +++ b/Benchmarks/IxVM.lean @@ -26,7 +26,7 @@ def main : IO Unit := do | throw (IO.userError "Compilation failed") let some funIdx := compiled.getFuncIdx `ixon_serde_blake3_bench | throw (IO.userError "Aiur function not found") - let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters + let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters let env ← get_env! let ixonEnv ← IxVM.ClaimHarness.loadIxonEnv ``Nat.add_comm env @@ -37,6 +37,6 @@ def main : IO Unit := do -- IxVM-native prove: routes execution through the codegen'd Rust -- kernel (`execute_generated`) instead of the bytecode interpreter. bench "serde/blake3 Nat.add_comm" - (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n]) + (aiurSystem.proveIxVM funIdx #[.ofNat n]) ioBuffer return diff --git a/Benchmarks/RecursiveVerifier.lean b/Benchmarks/RecursiveVerifier.lean index 18868a093..d6403f088 100644 --- a/Benchmarks/RecursiveVerifier.lean +++ b/Benchmarks/RecursiveVerifier.lean @@ -116,15 +116,15 @@ def main (args : List String) : IO UInt32 := do let facCompiled ← match program.compile with | .ok c => pure c | .error e => IO.eprintln s!"inner compile failed: {e}"; return 1 - let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams + let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams innerFri let facIdx := facCompiled.getFuncIdx entry |>.get! IO.println s!"proving inner {entry}(5)…" TracingTexray.resetPeakTreeRss let it0 ← IO.monoNanosNow - let (claim, proof, _) := facSystem.prove innerFri facIdx #[Aiur.G.ofNat 5] default + let (claim, proof, _) := facSystem.prove facIdx #[Aiur.G.ofNat 5] default let proofBytes := proof.toBytes let it1 ← IO.monoNanosNow - let innerOk := facSystem.verify innerFri claim proof matches .ok _ + let innerOk := facSystem.verify claim proof matches .ok _ let it2 ← IO.monoNanosNow let innerPeak ← TracingTexray.peakTreeRssBytes IO.println s!"inner PROVE: {secs it0 it1} s, \ @@ -134,7 +134,7 @@ def main (args : List String) : IO UInt32 := do IO.eprintln "inner proof failed to verify" return 1 -- Proof (advice, channel 0), vk (channel 1), claims (channel 2), plus the - -- Keccak-bound vk/claims digests and FRI params as public input. + -- Blake3-bound vk/claims digests and FRI params as public input. let claimBytes := MultiStark.serializeClaims #[claim] let (pubInput, io) := MultiStark.verifierInput proofBytes facSystem.vkBytes claimBytes recCommitParams innerFri @@ -173,14 +173,14 @@ def main (args : List String) : IO UInt32 := do return 0 -- PROVE the verifier execution (multi-stark): the recursion step itself. IO.println "\n=== PROVING the verifier (multi-stark) ===" - let vSystem := AiurSystem.build vCompiled.bytecode recCommitParams + let vSystem := AiurSystem.build vCompiled.bytecode recCommitParams innerFri TracingTexray.resetPeakTreeRss let t0 ← IO.monoNanosNow - let (vclaim, vproof, _) := vSystem.prove innerFri vIdx pubInput io + let (vclaim, vproof, _) := vSystem.prove vIdx pubInput io let nbytes := vproof.toBytes.size -- force the (lazy, pure) prove to run let t1 ← IO.monoNanosNow let outerPeak ← TracingTexray.peakTreeRssBytes - let outerOk := vSystem.verify innerFri vclaim vproof matches .ok _ + let outerOk := vSystem.verify vclaim vproof matches .ok _ let t2 ← IO.monoNanosNow IO.println s!"verifier PROVE time: {secs t0 t1} s, proof {nbytes} bytes" IO.println s!"verifier proof VERIFY time: \ diff --git a/Benchmarks/Sha256.lean b/Benchmarks/Sha256.lean index beea833ee..96c780d4d 100644 --- a/Benchmarks/Sha256.lean +++ b/Benchmarks/Sha256.lean @@ -34,7 +34,7 @@ def sha256Bench : IO $ Array BenchReport := do | throw (IO.userError "Compilation failed") let some funIdx := compiled.getFuncIdx `sha256_bench | throw (IO.userError "Aiur function not found") - let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters + let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters bgroup "prove sha256" { oneShot := true, avgThroughput := true, report := true } do for dataSize in dataSizes do for numHashes in numHashesPerProof do @@ -47,7 +47,7 @@ def sha256Bench : IO $ Array BenchReport := do ioBuffer.extend 0 #[.ofNat idx] data throughput (.ElementsAndBytes numHashes.toUInt64 (dataSize * numHashes).toUInt64 "hashes") bench s!"dataSize={dataSize} numHashes={numHashes}" - (aiurSystem.prove friParameters funIdx #[Aiur.G.ofNat numHashes]) ioBuffer + (aiurSystem.prove funIdx #[Aiur.G.ofNat numHashes]) ioBuffer def main : IO Unit := do let _ ← sha256Bench diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index a140fce19..45386f3d6 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -325,7 +325,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let (commitParams, friParams) := if recursive then (recursiveCommitmentParameters, recursiveFriParameters) else (commitmentParameters, friParameters) - let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitParams + let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitParams friParams -- The recursive-verifier context, compiled and built ONCE: the verifier -- toplevel is constant-independent, and its prover system (same recursion -- parameters) is reused for every constant's outer prove. @@ -338,7 +338,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let some vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof | throw (IO.userError "verify_multi_stark_proof entrypoint missing") pure (some (vCompiled, vIdx, - Aiur.AiurSystem.build vCompiled.bytecode commitParams)) + Aiur.AiurSystem.build vCompiled.bytecode commitParams friParams)) -- Load the serialized env lazily (the `ix check --ixe` path, #445): byte-window -- constants over the backing buffer, so only the checked closure is ever @@ -452,11 +452,11 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do if skipDeps then let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr let (claim, proof, ioBuf) := - aiurSystem.proveIxVM friParams funIdx witness.input witness.inputIOBuffer + aiurSystem.proveIxVM funIdx witness.input witness.inputIOBuffer (.ok (claim, proof, ioBuf) : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) else - match aiurSystem.proveAddrWithEnv friParams funIdx envHandle addr.hash with + match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => .error e | .ok (claimBytes, proof, ioBuf) => -- The envHandle path returns the SERIALIZED `Ix.Claim`; rebuild @@ -474,7 +474,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let peak ← TracingTexray.peakTreeRssBytes let proofBytes := Aiur.Proof.toBytes proof let (verifyRes, verifySec) ← timed fun _ => - aiurSystem.verify friParams claim proof + aiurSystem.verify claim proof let verifySec? ← match verifyRes with | .ok () => pure (some verifySec) | .error e => @@ -519,11 +519,11 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do (← IO.getStdout).flush TracingTexray.resetPeakTreeRss let ((rvClaim, rvProof, _), rvProveSec) ← timed fun _ => - vSystem.prove friParams vIdx pubInput io + vSystem.prove vIdx pubInput io let rvPeak ← TracingTexray.peakTreeRssBytes let rvProofBytes := Aiur.Proof.toBytes rvProof let (rvVerifyRes, rvVerifySec) ← timed fun _ => - vSystem.verify friParams rvClaim rvProof + vSystem.verify rvClaim rvProof let rvVerifySec? ← match rvVerifyRes with | .ok () => pure (some rvVerifySec) | .error e => diff --git a/Cargo.lock b/Cargo.lock index b3ae9ab9f..78a40ab8a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2075,10 +2075,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=75fcd1b2e9f2cdf19422892598d0f0d69fd82521#75fcd1b2e9f2cdf19422892598d0f0d69fd82521" dependencies = [ "bincode", "p3-air", + "p3-blake3", "p3-challenger", "p3-commit", "p3-dft", @@ -2502,6 +2503,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 719fee16f..840d45d70 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -50,7 +50,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 = "75fcd1b2e9f2cdf19422892598d0f0d69fd82521" } num-bigint = "0.4.6" quickcheck = "1.0.3" quickcheck_macros = "1.0.0" diff --git a/Ix/Aiur/Protocol.lean b/Ix/Aiur/Protocol.lean index b5d6b332d..b59e3c2dd 100644 --- a/Ix/Aiur/Protocol.lean +++ b/Ix/Aiur/Protocol.lean @@ -45,14 +45,14 @@ instance : Nonempty AiurSystem := AiurSystemNonempty.property namespace AiurSystem @[extern "rs_aiur_system_build"] -opaque build : @&Bytecode.Toplevel → @&CommitmentParameters → AiurSystem +opaque build : @&Bytecode.Toplevel → @&CommitmentParameters → @&FriParameters → AiurSystem /-- Serialize the verifying key (`System`) to bytes. -/ @[extern "rs_aiur_system_vk_bytes"] opaque vkBytes : @& AiurSystem → ByteArray @[extern "rs_aiur_system_prove"] -private opaque prove' : @& AiurSystem → @& FriParameters → +private opaque prove' : @& AiurSystem → @& Bytecode.FunIdx → @& Array G → (ioData : @& Array (G × Array G)) → (ioMap : @& Array ((G × Array G) × IOKeyInfo)) → @@ -62,19 +62,19 @@ private opaque prove' : @& AiurSystem → @& FriParameters → then generates a proof of the computation. Returns the claim (`#[functionChannel, funIdx] ++ args ++ output`), the `Proof`, and the updated `IOBuffer`. -/ -def prove (system : @& AiurSystem) (friParameters : @& FriParameters) +def prove (system : @& AiurSystem) (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) : Array G × Proof × IOBuffer := let ioData := ioBuffer.data.toArray let ioMap := ioBuffer.map.toArray - let (claim, proof, ioData, ioMap) := prove' system friParameters funIdx args + let (claim, proof, ioData, ioMap) := prove' system funIdx args ioData ioMap let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅ let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅ (claim, proof, ⟨ioData, ioMap⟩) @[extern "rs_aiur_system_prove_ixvm"] -private opaque proveIxVM' : @& AiurSystem → @& FriParameters → +private opaque proveIxVM' : @& AiurSystem → @& Bytecode.FunIdx → @& Array G → (ioData : @& Array (G × Array G)) → (ioMap : @& Array ((G × Array G) × IOKeyInfo)) → @@ -85,19 +85,19 @@ private opaque proveIxVM' : @& AiurSystem → @& FriParameters → of the bytecode interpreter. The resulting `Proof` is verification-compatible with one from `prove`. Only valid when `system.toplevel` is the IxVM kernel's bytecode. -/ -def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters) +def proveIxVM (system : @& AiurSystem) (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) : Array G × Proof × IOBuffer := let ioData := ioBuffer.data.toArray let ioMap := ioBuffer.map.toArray - let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args + let (claim, proof, ioData, ioMap) := proveIxVM' system funIdx args ioData ioMap let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅ let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅ (claim, proof, ⟨ioData, ioMap⟩) @[extern "rs_aiur_system_prove_addr_with_env"] -private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters → +private opaque proveAddrWithEnv' : @& AiurSystem → @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Except String (ByteArray × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)) @@ -106,10 +106,10 @@ private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters → `(claimBytes, proof, ioBuffer)` — Rust serializes the reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can deserialize directly without re-running the closure walk. -/ -def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters) +def proveAddrWithEnv (system : @& AiurSystem) (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) : Except String (ByteArray × Proof × IOBuffer) := - match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with + match proveAddrWithEnv' system funIdx envHandle addrBytes with | .error e => .error e | .ok (claimBytes, proof, ioData, ioMap) => let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅ @@ -117,16 +117,16 @@ def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters) .ok (claimBytes, proof, ⟨ioData, ioMap⟩) @[extern "rs_aiur_system_shard_prove_with_env"] -private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters → +private opaque shardProveWithEnv' : @& AiurSystem → @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Except String (ByteArray × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)) /-- Per-shard prove against a Rust-owned `EnvHandle`. -/ -def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters) +def shardProveWithEnv (system : @& AiurSystem) (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) : Except String (ByteArray × Proof × IOBuffer) := - match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with + match shardProveWithEnv' system funIdx envHandle ownedBlob with | .error e => .error e | .ok (claimBytes, proof, ioData, ioMap) => let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅ @@ -134,7 +134,7 @@ def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters .ok (claimBytes, proof, ⟨ioData, ioMap⟩) @[extern "rs_aiur_system_verify"] -opaque verify : @& AiurSystem → @& FriParameters → +opaque verify : @& AiurSystem → @& Array G → @& Proof → Except String Unit end AiurSystem diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean index 8f515882a..183b39209 100644 --- a/Ix/Cli/ProveCmd.lean +++ b/Ix/Cli/ProveCmd.lean @@ -79,7 +79,7 @@ def proveOne (aiurSystem : Aiur.AiurSystem) -- via `proveIxVM` (used for non-`check addr none` `--claim hex`). let proof : Aiur.Proof ← match target, envHandle? with | .addr a, some envHandle => - match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle a.hash with + match aiurSystem.proveAddrWithEnv funIdx envHandle a.hash with | .error e => IO.eprintln s!"{label}: proveAddrWithEnv error: {e}" return 1 @@ -87,14 +87,14 @@ def proveOne (aiurSystem : Aiur.AiurSystem) | .shard owned, some envHandle => let mut blob := ByteArray.empty for x in owned do blob := blob ++ x.hash - match aiurSystem.shardProveWithEnv friParameters funIdx envHandle blob with + match aiurSystem.shardProveWithEnv funIdx envHandle blob with | .error e => IO.eprintln s!"{label}: shardProveWithEnv error: {e}" return 1 | .ok (_claimBytes, proof, _outIO) => pure proof | .leanW witness, _ => let (_aiurClaim, proof, _outIO) := - aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer + aiurSystem.proveIxVM funIdx witness.input witness.inputIOBuffer pure proof | _, none => IO.eprintln s!"{label}: internal: addr/shard target with no envHandle" @@ -123,7 +123,7 @@ def runShardProveNative (manifestPath : String) (envHandle : Aiur.EnvHandle) IO.println s!"Proving {label}" (← IO.getStdout).flush let funIdx := compiled.getFuncIdx `verify_claim |>.get! - match aiurSystem.shardProveWithEnv friParameters funIdx envHandle blob with + match aiurSystem.shardProveWithEnv funIdx envHandle blob with | .error e => IO.eprintln s!"{label}: shardProveWithEnv error: {e}" return 1 @@ -155,7 +155,7 @@ def runProveCmd (p : Cli.Parsed) : IO UInt32 := do let compiled ← match toplevel.compile with | .error e => IO.eprintln s!"compilation failed: {e}"; return 1 | .ok c => pure c - let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters + let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters let runOne := proveOne aiurSystem compiled match ixePath, (p.flag? "ixes").map (·.as! String), (p.flag? "shard").map (·.as! Nat) with | some ixe, some manifest, some k => diff --git a/Ix/Cli/VerifyCmd.lean b/Ix/Cli/VerifyCmd.lean index e66b55488..634028410 100644 --- a/Ix/Cli/VerifyCmd.lean +++ b/Ix/Cli/VerifyCmd.lean @@ -63,7 +63,7 @@ def verifyOneProof (aiurSystem : Aiur.AiurSystem) (compiled : Aiur.CompiledTople return 1 let input : Array Aiur.G := claimDigest.hash.data.map .ofUInt8 let aiurClaim := Aiur.buildClaim funIdx input #[] - match aiurSystem.verify friParameters aiurClaim proof with + match aiurSystem.verify aiurClaim proof with | .ok () => IO.println s!"ok: proof {proofAddr} verifies claim {claimDigest}" return 0 @@ -79,7 +79,7 @@ def buildBackend : IO (Except String (Aiur.AiurSystem × Aiur.CompiledToplevel)) | .ok toplevel => match toplevel.compile with | .error e => return .error s!"compilation failed: {e}" | .ok compiled => - return .ok (Aiur.AiurSystem.build compiled.bytecode commitmentParameters, compiled) + return .ok (Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters, compiled) /-- Shard-aware verification (parity with `check`/`prove`): - `--shard K`, no proof: print shard K's reconstructed `CheckEnv` claim diff --git a/Ix/MultiStark.lean b/Ix/MultiStark.lean index ebe829cb1..93254d717 100644 --- a/Ix/MultiStark.lean +++ b/Ix/MultiStark.lean @@ -1,9 +1,10 @@ module +public import Blake3.Rust public import Ix.Aiur.Meta public import Ix.Aiur.Protocol -public import Ix.Keccak 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 @@ -17,12 +18,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*. @@ -37,8 +38,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. @@ -49,19 +50,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. @@ -75,12 +76,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 @@ -89,7 +90,7 @@ def multiStark : Except Aiur.Global Aiur.Source.Toplevel := do /-! ## Lean-side input assembly Callers of `verify_multi_stark_proof` (tests, benchmarks) must reproduce the -verifier's wire formats byte-for-byte — the vk and claims are keccak-256 +verifier's wire formats byte-for-byte — the vk and claims are Blake3 digest-bound. These helpers are that recipe's single home. -/ /-- The 8 little-endian bytes of `n` as a `u64`. -/ @@ -115,7 +116,7 @@ def verifierInput (proofBytes vkBytes claimBytes : ByteArray) (commitParams : Aiur.CommitmentParameters) (friParams : Aiur.FriParameters) : Array Aiur.G × Aiur.IOBuffer := let gs := fun (b : ByteArray) => b.data.map Aiur.G.ofUInt8 - let digestGs := fun (b : ByteArray) => gs (Keccak.hash b) + let digestGs := fun (b : ByteArray) => gs (Blake3.Rust.hash b).val let pubInput := digestGs vkBytes ++ digestGs claimBytes ++ #[.ofNat friParams.numQueries, .ofNat friParams.commitProofOfWorkBits, .ofNat commitParams.logBlowup] diff --git a/Ix/MultiStark/Pcs.lean b/Ix/MultiStark/Pcs.lean index 024adb87d..85dc2227d 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/SystemDeserialize.lean b/Ix/MultiStark/SystemDeserialize.lean index fbbbc046c..1d76594aa 100644 --- a/Ix/MultiStark/SystemDeserialize.lean +++ b/Ix/MultiStark/SystemDeserialize.lean @@ -76,14 +76,22 @@ def systemDeserialize := ⟦ -- preprocessed_width, stage_1_width, stage_2_width. enum SysCircuit { Mk(SysLookupAir, G, G, G, G, G, G) } - enum SysParams { Mk(G, G) } -- log_blowup, cap_height + -- log_blowup, cap_height, log_final_poly_len, max_log_arity, num_queries, + -- commit_proof_of_work_bits, query_proof_of_work_bits — the commitment + FRI + -- parameters the config (and its challenger seed) was built from. + enum SysParams { Mk(G, G, G, G, G, G, G) } -- `Option`s as dedicated non-generic enums (unambiguous constructors). enum OptCommit { NoCommit, SomeCommit(MerkleCap) } enum OptIdx { NoIdx, SomeIdx(G) } - -- commitment_parameters, circuits, preprocessed_commit, preprocessed_indices. - enum Sys { Mk(SysParams, List‹SysCircuit›, OptCommit, List‹OptIdx›) } + -- parameters, transcript limbs, circuits, preprocessed_commit, + -- preprocessed_indices. The transcript limbs are the raw u64 wire words the + -- challenger observes before any commitment — the 7 parameters (bound via + -- the challenger seed) followed by the system shape (`observe_shape`: the + -- circuit count, then 6 metadata words per circuit) — kept as limbs because + -- the Fiat-Shamir replay needs their little-endian bytes. + enum Sys { Mk(SysParams, List‹U64›, List‹SysCircuit›, OptCommit, List‹OptIdx›) } -- ========================================================================== -- Byte primitives specific to the VK format. @@ -212,27 +220,39 @@ def systemDeserialize := ⟦ (SysLookupAir.Mk(inner, lookups), s1) } - fn read_sys_circuit(stream: ByteStream) -> (SysCircuit, ByteStream) { + -- Besides the parsed circuit, also returns its 6 metadata words as raw u64 + -- limbs — `observe_shape` feeds exactly these bytes into the challenger. + fn read_sys_circuit(stream: ByteStream) -> (SysCircuit, [U64; 6], ByteStream) { let (air, s) = read_sys_lookupair(stream); - let (cc, s1) = read_count(s); - let (md, s2) = read_count(s1); - let (ph, s3) = read_count(s2); - let (pw, s4) = read_count(s3); - let (w1, s5) = read_count(s4); - let (w2, s6) = read_count(s5); - (SysCircuit.Mk(air, cc, md, ph, pw, w1, w2), s6) + let (cc, s1) = read_u64(s); + let (md, s2) = read_u64(s1); + let (ph, s3) = read_u64(s2); + let (pw, s4) = read_u64(s3); + let (w1, s5) = read_u64(s4); + let (w2, s6) = read_u64(s5); + (SysCircuit.Mk(air, flatten_u64(cc), flatten_u64(md), flatten_u64(ph), + flatten_u64(pw), flatten_u64(w1), flatten_u64(w2)), + [cc, md, ph, pw, w1, w2], s6) } - fn read_sys_circuits(stream: ByteStream) -> (List‹SysCircuit›, ByteStream) { - let (n, s) = read_count(stream); - read_sys_circuits_n(s, n) + fn cons_shape6(l: [U64; 6], tail: List‹U64›) -> List‹U64› { + store(ListNode.Cons(l[0], store(ListNode.Cons(l[1], store(ListNode.Cons(l[2], + store(ListNode.Cons(l[3], store(ListNode.Cons(l[4], store(ListNode.Cons(l[5], + tail)))))))))))) + } + -- Returns the circuits plus their shape limbs (`observe_shape` order: the + -- raw circuit-count word, then each circuit's 6 metadata words). + fn read_sys_circuits(stream: ByteStream) -> (List‹SysCircuit›, List‹U64›, ByteStream) { + let (nl, s) = read_u64(stream); + let (cs, limbs, s1) = read_sys_circuits_n(s, flatten_u64(nl)); + (cs, store(ListNode.Cons(nl, limbs)), s1) } - fn read_sys_circuits_n(stream: ByteStream, n: G) -> (List‹SysCircuit›, ByteStream) { + fn read_sys_circuits_n(stream: ByteStream, n: G) -> (List‹SysCircuit›, List‹U64›, ByteStream) { match n { - 0 => (store(ListNode.Nil), stream), + 0 => (store(ListNode.Nil), store(ListNode.Nil), stream), _ => - let (x, s) = read_sys_circuit(stream); - let (rest, s2) = read_sys_circuits_n(s, n - 1); - (store(ListNode.Cons(x, rest)), s2), + let (x, xl, s) = read_sys_circuit(stream); + let (rest, lrest, s2) = read_sys_circuits_n(s, n - 1); + (store(ListNode.Cons(x, rest)), cons_shape6(xl, lrest), s2), } } @@ -265,19 +285,32 @@ def systemDeserialize := ⟦ } } - fn read_sys_params(stream: ByteStream) -> (SysParams, ByteStream) { - let (log_blowup, s) = read_count(stream); - let (cap_height, s1) = read_count(s); - (SysParams.Mk(log_blowup, cap_height), s1) + -- The 7 protocol parameters, both as field counts (for the verifier logic) + -- and as raw u64 limbs (their LE bytes seed the challenger). + fn read_sys_params(stream: ByteStream) -> (SysParams, List‹U64›, ByteStream) { + let (l0, s0) = read_u64(stream); + let (l1, s1) = read_u64(s0); + let (l2, s2) = read_u64(s1); + let (l3, s3) = read_u64(s2); + let (l4, s4) = read_u64(s3); + let (l5, s5) = read_u64(s4); + let (l6, s6) = read_u64(s5); + (SysParams.Mk(flatten_u64(l0), flatten_u64(l1), flatten_u64(l2), + flatten_u64(l3), flatten_u64(l4), flatten_u64(l5), + flatten_u64(l6)), + store(ListNode.Cons(l0, store(ListNode.Cons(l1, store(ListNode.Cons(l2, + store(ListNode.Cons(l3, store(ListNode.Cons(l4, store(ListNode.Cons(l5, + store(ListNode.Cons(l6, store(ListNode.Nil))))))))))))))), + s6) } -- Full `System`. fn read_system(stream: ByteStream) -> (Sys, ByteStream) { - let (params, s) = read_sys_params(stream); - let (circuits, s1) = read_sys_circuits(s); + let (params, plimbs, s) = read_sys_params(stream); + let (circuits, climbs, s1) = read_sys_circuits(s); let (commit, s2) = read_opt_commit(s1); let (indices, s3) = read_opt_idx_list(s2); - (Sys.Mk(params, circuits, commit, indices), s3) + (Sys.Mk(params, list_concat(plimbs, climbs), circuits, commit, indices), s3) } ⟧ diff --git a/Ix/MultiStark/Tests.lean b/Ix/MultiStark/Tests.lean index 801481234..6d26ed434 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 eed9c09a8..0892cde14 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 @@ -32,11 +32,13 @@ The Rust verifier runs these steps: * Step 2: accumulator balance — the last `intermediate_accumulator` is the zero extension element. * Step 3: the Fiat-Shamir challenger replay (`fiat_shamir`). Prover-faithful: - observes the verifying key's preprocessed commitment, the stage_1 commitment, - the trace heights, and the public claims (in that order), then samples and - re-observes the lookup/fingerprint challenges, observes stage_2, samples α, - observes the quotient commitment, and samples ζ — matching - `verify_multiple_claims` byte-for-byte. + starts from the parameter-seeded challenger (`b"multi-stark/v0"` + the 7 + protocol parameters), observes the system shape, the verifying key's + preprocessed commitment, the stage_1 commitment, the trace heights, and the + length-prefixed public claims (in that order), then samples and re-observes + the lookup/fingerprint challenges, observes stage_2 and the intermediate + accumulators, samples α, observes the quotient commitment, and samples ζ — + matching `verify_multiple_claims` byte-for-byte. * Step 5: the out-of-domain composition/quotient check (`ood_verify`). For each circuit it recomputes `composition(ζ)` by replaying the AIR constraint folder (`VerifierConstraintFolder` + `LookupAir::eval`) over the deserialized @@ -47,13 +49,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 +86,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 +139,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 +188,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 +226,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))) @@ -222,6 +235,15 @@ def verifier := ⟦ fn snoc_cap(input: ByteStream, cap: MerkleCap) -> ByteStream { list_concat(input, cap_onto(cap, store(ListNode.Nil))) } + -- Append (observe) the intermediate accumulators, in order — each an + -- `observe_algebra_element`: two canonical 8-LE-byte limbs. (`read_ext` + -- reduced the limbs mod p, matching `as_canonical_u64` serialization.) + fn snoc_accs(input: ByteStream, accs: List‹Ext›) -> ByteStream { + match load(accs) { + ListNode.Nil => input, + ListNode.Cons(e, rest) => snoc_accs(snoc_b8(snoc_b8(input, e[0]), e[1]), rest), + } + } -- ========================================================================== -- PCS challenger continuation (Phase 4): the post-ζ transcript that @@ -256,11 +278,37 @@ def verifier := ⟦ ListNode.Cons(v, rest) => b8_onto(v, claim_vals_onto(rest, tail)), } } - -- Append every claim's values (`challenger.observe_slice(claim)` per claim). - fn claims_onto(claims: List‹List‹U64››, tail: ByteStream) -> ByteStream { + -- Each claim, length-prefixed: `observe(Val::from_usize(claim.len()))` then + -- `observe_slice(claim)`. + fn claims_each_onto(claims: List‹List‹U64››, tail: ByteStream) -> ByteStream { match load(claims) { ListNode.Nil => tail, - ListNode.Cons(c, rest) => claim_vals_onto(c, claims_onto(rest, tail)), + ListNode.Cons(c, rest) => + b8_onto(list_length_u64(c), claim_vals_onto(c, claims_each_onto(rest, tail))), + } + } + -- Append every claim: the claim count, then each claim length-prefixed + -- (`verify_multiple_claims`' claim observation, byte-for-byte). + fn claims_onto(claims: List‹List‹U64››, tail: ByteStream) -> ByteStream { + b8_onto(list_length_u64(claims), claims_each_onto(claims, tail)) + } + + -- `b"multi-stark/v0"` — the domain-separation tag the challenger seed + -- starts with (`GoldilocksBlake3Config::new`). + fn seed_tag_onto(tail: ByteStream) -> ByteStream { + store(ListNode.Cons(109u8, store(ListNode.Cons(117u8, store(ListNode.Cons(108u8, + store(ListNode.Cons(116u8, store(ListNode.Cons(105u8, store(ListNode.Cons(45u8, + store(ListNode.Cons(115u8, store(ListNode.Cons(116u8, store(ListNode.Cons(97u8, + store(ListNode.Cons(114u8, store(ListNode.Cons(107u8, store(ListNode.Cons(47u8, + store(ListNode.Cons(118u8, store(ListNode.Cons(48u8, + tail)))))))))))))))))))))))))))) + } + -- Raw u64 wire words (protocol parameters + system shape), each as its 8 LE + -- bytes, in order. + fn limbs_onto(ls: List‹U64›, tail: ByteStream) -> ByteStream { + match load(ls) { + ListNode.Nil => tail, + ListNode.Cons(l, rest) => b8_onto(l, limbs_onto(rest, tail)), } } @@ -276,9 +324,12 @@ def verifier := ⟦ -- Replay the verifier transcript and derive the four challenges -- `(lookup, fingerprint, alpha, zeta)`. Mirrors `verify_multiple_claims`'s -- challenger sequence exactly: - -- observe preprocessed_commit (if any) → stage_1 → log_degrees → claims; + -- seed = tag + protocol parameters; observe_shape (circuit count + 6 + -- metadata words per circuit) → preprocessed_commit (if any) → stage_1 → + -- log_degrees → length-prefixed claims; -- sample lookup, observe it; sample fingerprint, observe it; - -- observe stage_2; sample α; observe quotient; sample ζ. + -- observe stage_2; observe the intermediate accumulators; sample α; + -- observe quotient; sample ζ. -- `observe` clears the challenger's output buffer, and every sample here is -- preceded by an observe, so each `ch_sample_ext` re-flushes from an empty -- output (hence the `store(ListNode.Nil)` output argument each time). @@ -289,15 +340,19 @@ def verifier := ⟦ -- (Phase 4+) continues observing into. The leftover `output` after the ζ -- sample is discarded — the next challenger op is an observe (of the opened -- values), which clears `output` anyway. - fn fiat_shamir(prep: MerkleCap, s1: MerkleCap, s2: MerkleCap, q: MerkleCap, - lds: List‹U8›, claims: List‹List‹U64››) -> (Ext, Ext, Ext, Ext, ByteStream) { - -- Initial transcript, front-to-back: prep, stage_1, log_degrees, claims. + fn fiat_shamir(tlimbs: List‹U64›, prep: MerkleCap, s1: MerkleCap, s2: MerkleCap, + q: MerkleCap, lds: List‹U8›, claims: List‹List‹U64››, accs: List‹Ext›) + -> (Ext, Ext, Ext, Ext, ByteStream) { + -- Initial transcript, front-to-back: seed tag, parameter + shape words + -- (`tlimbs`, from the verifying key), prep, stage_1, log_degrees, claims. -- Built inner-to-outer with the prepend helpers so the result is in -- forward (observation) order. let input = claims_onto(claims, store(ListNode.Nil)); let input = log_degrees_onto(lds, input); let input = cap_onto(s1, input); let input = cap_onto(prep, input); + let input = limbs_onto(tlimbs, input); + let input = seed_tag_onto(input); -- sample lookup challenge, then observe it back (append) let (l0, l1, input, _ol) = ch_sample_ext(input, store(ListNode.Nil)); let input = snoc_b8(snoc_b8(input, l0), l1); @@ -306,6 +361,9 @@ def verifier := ⟦ let input = snoc_b8(snoc_b8(input, f0), f1); -- observe stage_2 commitment let input = snoc_cap(input, s2); + -- observe the intermediate accumulators (public values entering the + -- constraints; α and ζ must depend on them directly) + let input = snoc_accs(input, accs); -- sample constraint challenge α (not observed) let (a0, a1, input, _oa) = ch_sample_ext(input, store(ListNode.Nil)); -- observe quotient commitment @@ -434,9 +492,8 @@ def verifier := ⟦ -- composition(ζ) · inv_vanishing(ζ) == quotient(ζ). -- -- The challenges (lookup, fingerprint, α, ζ) come from `fiat_shamir` above. - -- As with `fiat_shamir`, claims are not observed; this assumes the no-claims - -- case, so the running lookup accumulator starts at the zero extension - -- element (`acc` in Rust = ExtVal::ZERO). + -- The running lookup accumulator starts from the public claims + -- (`claims_acc`; ExtVal::ZERO when there are none). -- ========================================================================== -- One Horner fold step of the constraint folder: `acc := acc·α + x` @@ -767,23 +824,25 @@ def verifier := ⟦ fn ood_verify(sys: Sys, proof: Proof, claims: List‹List‹U64››, num_queries: G, commit_pow_bits: G, log_blowup_pub: G) -> G { -- The FRI parameters (`num_queries`, `commit_pow_bits`, `log_blowup`) are - -- public inputs. `log_blowup` also lives in the (digest-bound) verifying - -- key's CommitmentParameters — assert the two agree. - let Sys.Mk(params, circuits, commit, prep_indices) = sys; - let SysParams.Mk(log_blowup, _cap_height) = params; + -- public inputs. All parameters also live in the (digest-bound) verifying + -- key — assert the public ones agree with it. + let Sys.Mk(params, tlimbs, circuits, commit, prep_indices) = sys; + let SysParams.Mk(log_blowup, _cap_height, _log_final_poly_len, + _max_log_arity, vk_num_queries, vk_commit_pow_bits, + _query_pow_bits) = params; assert_eq!(eq_zero(log_blowup - log_blowup_pub), 1); + assert_eq!(eq_zero(vk_num_queries - num_queries), 1); + assert_eq!(eq_zero(vk_commit_pow_bits - commit_pow_bits), 1); match proof { Proof.Mk(commitments, accs, log_degrees, opening, q_opened, prep_opt, stage1, stage2) => let Commitments.Mk(s1c, s2c, qc) = commitments; let prep_cap = opt_commit_cap(commit); - let (lch, fch, alpha, zeta, post_zeta_input) = fiat_shamir(prep_cap, s1c, s2c, qc, log_degrees, claims); + let (lch, fch, alpha, zeta, post_zeta_input) = fiat_shamir(tlimbs, prep_cap, s1c, s2c, qc, log_degrees, claims, accs); let acc0 = claims_acc([gl_zero(), gl_zero()], claims, lch, fch); -- 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/Aiur/Common.lean b/Tests/Aiur/Common.lean index 57a0cd561..8f17b28fb 100644 --- a/Tests/Aiur/Common.lean +++ b/Tests/Aiur/Common.lean @@ -58,7 +58,7 @@ def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Source.Toplevel) : let toplevel ← toplevelFn.mapError toString let compiled ← toplevel.compile let decls ← toplevel.mkDecls.mapError toString - let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters + let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters return ⟨compiled, decls, aiurSystem⟩ def AiurTestEnv.interpTest (env : AiurTestEnv) (testCase : AiurTestCase) @@ -105,14 +105,14 @@ def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : Test if testCase.executionOnly then execTest ++ interpTest else let (claim, proof, ioBuffer) := env.aiurSystem.prove - friParameters funIdx testCase.input testCase.inputIOBuffer + funIdx testCase.input testCase.inputIOBuffer let claimTest := test s!"Claim matches for {label}" (claim == Aiur.buildClaim funIdx testCase.input testCase.expectedOutput) let ioTest := test s!"IOBuffer matches for {label}" (ioBuffer == testCase.expectedIOBuffer) let proof := .ofBytes proof.toBytes let pvTest := withExceptOk s!"Prove/verify works for {label}" - (env.aiurSystem.verify friParameters claim proof) fun _ => .done + (env.aiurSystem.verify claim proof) fun _ => .done execTest ++ interpTest ++ claimTest ++ ioTest ++ pvTest def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Source.Toplevel) @@ -120,7 +120,7 @@ def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Source.Toplevel) withExceptOk "Toplevel merging succeeds" toplevelFn fun toplevel => withExceptOk "Compilation succeeds" toplevel.compile fun compiled => withExceptOk "mkDecls succeeds" (toplevel.mkDecls.mapError toString) fun decls => - let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters + let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters let env : AiurTestEnv := ⟨compiled, decls, aiurSystem⟩ cases.foldl (init := .done) fun tSeq testCase => tSeq ++ env.runTestCase testCase diff --git a/Tests/FFI/Lifecycle.lean b/Tests/FFI/Lifecycle.lean index d30554b78..01270cd13 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 fb852fb98..a22a214af 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"), @@ -132,24 +132,24 @@ def endToEndSuite : IO UInt32 := do let facCompiled ← match factorialProgram.compile with | .error e => IO.eprintln s!"factorial compilation failed: {e}"; return 1 | .ok c => pure c - let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams + let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams innerFri let facIdx ← match facCompiled.getFuncIdx `factorial with | some i => pure i | none => IO.eprintln "factorial entrypoint not found"; return 1 -- ── prove factorial(5) = 120 (`G` is a reserved DSL token, spell it qualified) let input := #[Aiur.G.ofNat 5] - let (claim, proof, _) := facSystem.prove innerFri facIdx input default + let (claim, proof, _) := facSystem.prove facIdx input default 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,11 +182,11 @@ 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)…" - let innerVerify := facSystem.verify innerFri claim (.ofBytes proofBytes) + let innerVerify := facSystem.verify claim (.ofBytes proofBytes) let honest := vCompiled.bytecode.execute vIdx pubInput (mkIO proofGs claimGs) let tamperedProof := vCompiled.bytecode.execute vIdx pubInput (mkIO badProofGs claimGs) let tamperedClaim := diff --git a/crates/aiur/src/synthesis.rs b/crates/aiur/src/synthesis.rs index e4422dfa5..2e59a775a 100644 --- a/crates/aiur/src/synthesis.rs +++ b/crates/aiur/src/synthesis.rs @@ -5,7 +5,7 @@ use multi_stark::{ p3_matrix::dense::RowMajorMatrix, prover::Proof, system::{ProverKey, System, SystemWitness}, - types::{CommitmentParameters, FriParameters, PcsError}, + types::{CommitmentParameters, FriParameters, GoldilocksBlake3Config, PcsError}, verifier::VerificationError, }; use rayon::iter::{ @@ -22,11 +22,20 @@ use crate::{ memory::Memory, }; +/// The concrete STARK configuration Aiur instantiates multi-stark with. +pub type AiurConfig = GoldilocksBlake3Config; +/// A proof under [`AiurConfig`]. +pub type AiurProof = Proof; + pub struct AiurSystem { toplevel: Toplevel, // perhaps remove the key from the system in verifier only mode? - key: ProverKey, - pub(crate) system: System, + key: ProverKey, + /// The parameters the system's config was built from, kept for the + /// verifying-key codec (the config itself doesn't expose them back). + pub(crate) commitment_parameters: CommitmentParameters, + pub(crate) fri_parameters: FriParameters, + pub(crate) system: System, } pub(crate) enum AiurCircuit { @@ -81,6 +90,7 @@ impl AiurSystem { pub fn build( toplevel: Toplevel, commitment_parameters: CommitmentParameters, + fri_parameters: FriParameters, ) -> Self { let function_circuits = (0..toplevel.functions.len()).filter_map(|i| { if !toplevel.functions[i].constrained { @@ -102,21 +112,21 @@ impl AiurSystem { ] .into_iter(); + let config = AiurConfig::new(commitment_parameters, fri_parameters); let (system, key) = System::new( - commitment_parameters, + config, function_circuits.chain(memory_circuits).chain(gadget_circuits), ); - AiurSystem { system, key, toplevel } + AiurSystem { system, key, toplevel, commitment_parameters, fri_parameters } } #[tracing::instrument(level = "info", skip_all, name = "aiur/prove")] pub fn prove( &self, - fri_parameters: FriParameters, fun_idx: FunIdx, input: &[G], io_buffer: &mut IOBuffer, - ) -> (Vec, Proof) { + ) -> (Vec, AiurProof) { tracing_texray::examine_current(); // Execute the Aiur bytecode. @@ -170,7 +180,7 @@ impl AiurSystem { claim.extend(output); // Finally prove. - let proof = self.system.prove(fri_parameters, &self.key, &claim, witness); + let proof = self.system.prove(&self.key, &claim, witness); (claim, proof) } @@ -187,12 +197,11 @@ impl AiurSystem { #[tracing::instrument(level = "info", skip_all, name = "aiur/prove_ixvm")] pub fn prove_ixvm( &self, - fri_parameters: FriParameters, fun_idx: FunIdx, input: &[G], io_buffer: &mut IOBuffer, executor: F, - ) -> (Vec, Proof) + ) -> (Vec, AiurProof) where F: FnOnce( &Toplevel, @@ -246,17 +255,16 @@ impl AiurSystem { claim.extend(input); claim.extend(output); - let proof = self.system.prove(fri_parameters, &self.key, &claim, witness); + let proof = self.system.prove(&self.key, &claim, witness); (claim, proof) } #[inline] pub fn verify( &self, - fri_parameters: FriParameters, claim: &[G], - proof: &Proof, + proof: &AiurProof, ) -> Result<(), VerificationError> { - self.system.verify(fri_parameters, claim, proof) + self.system.verify(claim, proof) } } diff --git a/crates/aiur/src/vk_codec.rs b/crates/aiur/src/vk_codec.rs index f48273fbb..f83e43c97 100644 --- a/crates/aiur/src/vk_codec.rs +++ b/crates/aiur/src/vk_codec.rs @@ -2,17 +2,18 @@ //! //! The verifier needs the system's per-circuit AIR (symbolic constraints + //! lookups + widths), the shared preprocessed commitment, the preprocessed -//! index map, and the commitment parameters — i.e. everything in -//! [`System`] except the prover-only preprocessed traces (the -//! large gadget tables in each `LookupAir.preprocessed`), which are -//! reconstructed/committed separately and so are *not* serialized. +//! index map, and the commitment + FRI parameters (which seed the config's +//! challenger) — i.e. everything in [`System`] except the +//! prover-only preprocessed traces (the large gadget tables in each +//! `LookupAir.preprocessed`), which are reconstructed/committed separately +//! and so are *not* serialized. //! //! This is a **hand-written, serde-free** codec. `multi-stark` does not derive //! `serde` on its types, and we do not want to fork it just to add the derives, //! so the encoder and decoder are written by hand against the public fields of //! `System`, `Circuit`, `LookupAir`, `Lookup`, `SymbolicExpression`, -//! `SymbolicVariable`, `Entry`, `CommitmentParameters` and the Ix -//! `AiurCircuit`/`Constraints`/`Memory`. The wire format mirrors the +//! `SymbolicVariable`, `Entry`, `CommitmentParameters`, `FriParameters` and +//! the Ix `AiurCircuit`/`Constraints`/`Memory`. The wire format mirrors the //! `bincode standard().little_endian().fixed_int` layout the proof uses, so the //! Aiur port (`Ix/MultiStark/SystemDeserialize.lean`) can read it the same way. //! @@ -39,13 +40,13 @@ use multi_stark::{ lookup::{Lookup, LookupAir}, p3_field::{PrimeCharacteristicRing, PrimeField64}, system::{Circuit, System}, - types::{Commitment, CommitmentParameters, Val}, + types::{Commitment, CommitmentParameters, FriParameters, Val}, }; use crate::{ constraints::Constraints, memory::Memory, - synthesis::{AiurCircuit, AiurSystem}, + synthesis::{AiurCircuit, AiurConfig, AiurSystem}, }; type Expr = SymbolicExpression; @@ -160,7 +161,7 @@ impl W { AiurCircuit::Bytes2 => self.u32(3), } } - fn circuit(&mut self, c: &Circuit) { + fn circuit(&mut self, c: &Circuit) { // LookupAir: inner_air, lookups (preprocessed is not serialized). self.aircircuit(&c.air.inner_air); self.vec(&c.air.lookups, Self::lookup); @@ -172,10 +173,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); } }); } @@ -191,11 +192,22 @@ impl W { } /// Serialize the verifying key `System` (preprocessed traces are -/// skipped — see the module docs). -pub(crate) fn to_bytes(system: &System) -> Vec { +/// skipped — see the module docs). The config's construction parameters are +/// passed alongside because [`AiurConfig`] doesn't expose them back; they are +/// written first so the decoder can rebuild the config. +pub(crate) fn to_bytes( + system: &System, + commitment_parameters: CommitmentParameters, + fri_parameters: FriParameters, +) -> Vec { let mut w = W { buf: Vec::new() }; - w.usize(system.commitment_parameters.log_blowup); - w.usize(system.commitment_parameters.cap_height); + w.usize(commitment_parameters.log_blowup); + w.usize(commitment_parameters.cap_height); + w.usize(fri_parameters.log_final_poly_len); + w.usize(fri_parameters.max_log_arity); + w.usize(fri_parameters.num_queries); + w.usize(fri_parameters.commit_proof_of_work_bits); + w.usize(fri_parameters.query_proof_of_work_bits); w.vec(&system.circuits, W::circuit); w.option(&system.preprocessed_commit, W::commitment); w.vec(&system.preprocessed_indices, |w, idx| { @@ -206,7 +218,7 @@ pub(crate) fn to_bytes(system: &System) -> Vec { /// Convenience: serialize the verifying key of a built [`AiurSystem`]. pub fn aiur_system_to_bytes(sys: &AiurSystem) -> Result, String> { - Ok(to_bytes(&sys.system)) + Ok(to_bytes(&sys.system, sys.commitment_parameters, sys.fri_parameters)) } // ════════════════════════════════════════════════════════════════════════════ @@ -317,7 +329,7 @@ impl<'a> R<'a> { t => return Err(format!("bad AiurCircuit tag {t}")), }) } - fn circuit(&mut self) -> Result, String> { + fn circuit(&mut self) -> Result, String> { // LookupAir: inner_air, lookups (preprocessed is prover-only -> None). let air = LookupAir { inner_air: self.aircircuit()?, @@ -335,7 +347,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( @@ -351,11 +369,24 @@ impl<'a> R<'a> { } /// Deserialize a `System` from [`to_bytes`] output, requiring that -/// every byte is consumed. -pub(crate) fn from_bytes(bytes: &[u8]) -> Result, String> { +/// every byte is consumed. Also returns the config's construction parameters, +/// which the `System` itself doesn't expose. +pub(crate) fn from_bytes( + bytes: &[u8], +) -> Result< + (System, CommitmentParameters, FriParameters), + String, +> { let mut r = R { buf: bytes, pos: 0 }; let commitment_parameters = CommitmentParameters { log_blowup: r.usize()?, cap_height: r.usize()? }; + let fri_parameters = FriParameters { + log_final_poly_len: r.usize()?, + max_log_arity: r.usize()?, + num_queries: r.usize()?, + commit_proof_of_work_bits: r.usize()?, + query_proof_of_work_bits: r.usize()?, + }; let circuits = r.vec(R::circuit)?; let preprocessed_commit = r.option(R::commitment)?; let preprocessed_indices = r.vec(|r| r.option(R::usize))?; @@ -366,12 +397,13 @@ pub(crate) fn from_bytes(bytes: &[u8]) -> Result, String> { bytes.len() )); } - Ok(System { - commitment_parameters, + let system = System { + config: AiurConfig::new(commitment_parameters, fri_parameters), circuits, preprocessed_commit, preprocessed_indices, - }) + }; + Ok((system, commitment_parameters, fri_parameters)) } #[cfg(test)] @@ -380,31 +412,44 @@ mod tests { use crate::gadgets::{AiurGadget, bytes1::Bytes1, bytes2::Bytes2}; use multi_stark::{lookup::LookupAir, types::CommitmentParameters}; + fn test_parameters() -> (CommitmentParameters, FriParameters) { + let cp = CommitmentParameters { log_blowup: 1, cap_height: 0 }; + let fp = FriParameters { + log_final_poly_len: 0, + max_log_arity: 1, + num_queries: 64, + commit_proof_of_work_bits: 0, + query_proof_of_work_bits: 0, + }; + (cp, fp) + } + /// Build a small real `System` from the two byte gadgets and /// check the verifying-key codec round-trips: decode(encode(x)) re-encodes to /// the same bytes (a serialization fixpoint). #[test] fn system_vk_round_trips() { - let cp = CommitmentParameters { log_blowup: 1, cap_height: 0 }; + let (cp, fp) = test_parameters(); let (system, _key) = System::new( - cp, + AiurConfig::new(cp, fp), [ LookupAir::new(AiurCircuit::Bytes1, Bytes1.lookups()), LookupAir::new(AiurCircuit::Bytes2, Bytes2.lookups()), ], ); - let bytes = to_bytes(&system); - let back = from_bytes(&bytes).expect("decode"); - let reencoded = to_bytes(&back); + let bytes = to_bytes(&system, cp, fp); + let (back, back_cp, back_fp) = from_bytes(&bytes).expect("decode"); + let reencoded = to_bytes(&back, back_cp, back_fp); assert_eq!(bytes, reencoded, "verifying-key codec round-trip mismatch"); } #[test] fn rejects_trailing_bytes() { - let cp = CommitmentParameters { log_blowup: 1, cap_height: 0 }; - let (system, _key) = - System::new(cp, [LookupAir::new(AiurCircuit::Bytes1, Bytes1.lookups())]); - let mut bytes = to_bytes(&system); + let (cp, fp) = test_parameters(); + let (system, _key) = System::new(AiurConfig::new(cp, fp), [ + LookupAir::new(AiurCircuit::Bytes1, Bytes1.lookups()), + ]); + let mut bytes = to_bytes(&system, cp, fp); bytes.push(0); assert!(from_bytes(&bytes).is_err(), "should reject trailing data"); } diff --git a/crates/ffi/src/aiur/protocol.rs b/crates/ffi/src/aiur/protocol.rs index 5a9b5e147..e155fe049 100644 --- a/crates/ffi/src/aiur/protocol.rs +++ b/crates/ffi/src/aiur/protocol.rs @@ -1,6 +1,5 @@ use multi_stark::{ p3_field::PrimeField64, - prover::Proof, types::{CommitmentParameters, FriParameters}, }; use rustc_hash::{FxBuildHasher, FxHashMap}; @@ -20,7 +19,7 @@ use crate::{ use aiur::{ G, execute::{IOBuffer, IOKeyInfo, QueryRecord}, - synthesis::AiurSystem, + synthesis::{AiurProof, AiurSystem}, }; // ============================================================================= @@ -28,7 +27,7 @@ use aiur::{ // ============================================================================= static AIUR_PROOF_CLASS: LazyLock = - LazyLock::new(ExternalClass::register_with_drop::); + LazyLock::new(ExternalClass::register_with_drop::); static AIUR_SYSTEM_CLASS: LazyLock = LazyLock::new(ExternalClass::register_with_drop::); static IX_ENV_HANDLE_CLASS: LazyLock = LazyLock::new( @@ -42,7 +41,7 @@ static IX_ENV_HANDLE_CLASS: LazyLock = LazyLock::new( /// `Aiur.Proof.toBytes : @& Proof → ByteArray` #[unsafe(no_mangle)] extern "C" fn rs_aiur_proof_to_bytes( - proof_obj: LeanExternal>, + proof_obj: LeanExternal>, ) -> LeanByteArray { let bytes = proof_obj.get().to_bytes().expect("Serialization error"); LeanByteArray::from_bytes(&bytes) @@ -52,9 +51,9 @@ extern "C" fn rs_aiur_proof_to_bytes( #[unsafe(no_mangle)] extern "C" fn rs_aiur_proof_of_bytes( byte_array: LeanByteArray>, -) -> LeanExternal { +) -> LeanExternal { let proof = - Proof::from_bytes(byte_array.as_bytes()).expect("Deserialization error"); + AiurProof::from_bytes(byte_array.as_bytes()).expect("Deserialization error"); LeanExternal::alloc(&AIUR_PROOF_CLASS, proof) } @@ -71,30 +70,30 @@ extern "C" fn rs_aiur_system_vk_bytes( LeanByteArray::from_bytes(&bytes) } -/// `AiurSystem.build : @&Bytecode.Toplevel → @&CommitmentParameters → AiurSystem` +/// `AiurSystem.build : @&Bytecode.Toplevel → @&CommitmentParameters → @&FriParameters → AiurSystem` #[unsafe(no_mangle)] extern "C" fn rs_aiur_system_build( toplevel: LeanAiurToplevel>, commitment_parameters: LeanAiurCommitmentParameters>, + fri_parameters: LeanAiurFriParameters>, ) -> LeanExternal { let system = AiurSystem::build( decode_toplevel(&toplevel), decode_commitment_parameters(&commitment_parameters), + decode_fri_parameters(&fri_parameters), ); LeanExternal::alloc(&AIUR_SYSTEM_CLASS, system) } -/// `AiurSystem.verify : @& AiurSystem → @& FriParameters → @& Array G → @& Proof → Except String Unit` +/// `AiurSystem.verify : @& AiurSystem → @& Array G → @& Proof → Except String Unit` #[unsafe(no_mangle)] extern "C" fn rs_aiur_system_verify( aiur_system_obj: LeanExternal>, - fri_parameters: LeanAiurFriParameters>, claim: LeanArray>, - proof_obj: LeanExternal>, + proof_obj: LeanExternal>, ) -> LeanExcept { - let fri_parameters = decode_fri_parameters(&fri_parameters); let claim = claim.map(|x| lean_unbox_g(&x)); - match aiur_system_obj.get().verify(fri_parameters, &claim, proof_obj.get()) { + match aiur_system_obj.get().verify(&claim, proof_obj.get()) { Ok(()) => LeanExcept::ok(LeanOwned::box_usize(0)), Err(err) => LeanExcept::error_string(&format!("{err:?}")), } @@ -248,19 +247,17 @@ extern "C" fn rs_aiur_toplevel_execute_ixvm( #[unsafe(no_mangle)] extern "C" fn rs_aiur_system_prove( aiur_system_obj: LeanExternal>, - fri_parameters: LeanAiurFriParameters>, fun_idx: LeanNat>, args: LeanArray>, io_data_arr: LeanArray>, io_map_arr: LeanArray>, ) -> LeanOwned { - let fri_parameters = decode_fri_parameters(&fri_parameters); let fun_idx = lean_unbox_nat_as_usize(fun_idx.inner()); let args = args.map(|x| lean_unbox_g(&x)); let mut io_buffer = decode_io_buffer(&io_data_arr, &io_map_arr); let (claim, proof) = - aiur_system_obj.get().prove(fri_parameters, fun_idx, &args, &mut io_buffer); + aiur_system_obj.get().prove(fun_idx, &args, &mut io_buffer); let lean_proof: LeanOwned = LeanExternal::alloc(&AIUR_PROOF_CLASS, proof).into(); @@ -531,7 +528,6 @@ extern "C" fn rs_aiur_toplevel_shard_check_with_env( #[unsafe(no_mangle)] extern "C" fn rs_aiur_system_prove_addr_with_env( aiur_system_obj: LeanExternal>, - fri_parameters: LeanAiurFriParameters>, fun_idx: LeanNat>, env_handle: LeanExternal< ixvm_codegen::env_handle::EnvHandle, @@ -539,7 +535,6 @@ extern "C" fn rs_aiur_system_prove_addr_with_env( >, addr_bytes: LeanByteArray>, ) -> LeanExcept { - let fri_parameters = decode_fri_parameters(&fri_parameters); let fun_idx = lean_unbox_nat_as_usize(fun_idx.inner()); let addr = match decode_addr(&addr_bytes) { Ok(a) => a, @@ -557,7 +552,6 @@ extern "C" fn rs_aiur_system_prove_addr_with_env( }; let (_aiur_claim_arr, proof) = aiur_system_obj.get().prove_ixvm( - fri_parameters, fun_idx, &input, &mut io_buffer, @@ -581,7 +575,6 @@ extern "C" fn rs_aiur_system_prove_addr_with_env( #[unsafe(no_mangle)] extern "C" fn rs_aiur_system_shard_prove_with_env( aiur_system_obj: LeanExternal>, - fri_parameters: LeanAiurFriParameters>, fun_idx: LeanNat>, env_handle: LeanExternal< ixvm_codegen::env_handle::EnvHandle, @@ -589,7 +582,6 @@ extern "C" fn rs_aiur_system_shard_prove_with_env( >, owned_blob: LeanByteArray>, ) -> LeanExcept { - let fri_parameters = decode_fri_parameters(&fri_parameters); let fun_idx = lean_unbox_nat_as_usize(fun_idx.inner()); let owned = match decode_owned_blob(&owned_blob) { Ok(v) => v, @@ -608,7 +600,6 @@ extern "C" fn rs_aiur_system_shard_prove_with_env( }; let (_aiur_claim_arr, proof) = aiur_system_obj.get().prove_ixvm( - fri_parameters, fun_idx, &input, &mut io_buffer, @@ -634,19 +625,16 @@ extern "C" fn rs_aiur_system_shard_prove_with_env( #[unsafe(no_mangle)] extern "C" fn rs_aiur_system_prove_ixvm( aiur_system_obj: LeanExternal>, - fri_parameters: LeanAiurFriParameters>, fun_idx: LeanNat>, args: LeanArray>, io_data_arr: LeanArray>, io_map_arr: LeanArray>, ) -> LeanOwned { - let fri_parameters = decode_fri_parameters(&fri_parameters); let fun_idx = lean_unbox_nat_as_usize(fun_idx.inner()); let args = args.map(|x| lean_unbox_g(&x)); let mut io_buffer = decode_io_buffer(&io_data_arr, &io_map_arr); let (claim, proof) = aiur_system_obj.get().prove_ixvm( - fri_parameters, fun_idx, &args, &mut io_buffer, From 1aac679ff72326917a5f7edeadc695c597a54b5f Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 10 Jul 2026 23:34:19 -0400 Subject: [PATCH 2/4] Formatting --- crates/aiur/src/synthesis.rs | 4 +++- crates/aiur/src/vk_codec.rs | 7 ++++--- crates/ffi/src/aiur/protocol.rs | 4 ++-- 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/crates/aiur/src/synthesis.rs b/crates/aiur/src/synthesis.rs index 2e59a775a..09bf0a0c7 100644 --- a/crates/aiur/src/synthesis.rs +++ b/crates/aiur/src/synthesis.rs @@ -5,7 +5,9 @@ use multi_stark::{ p3_matrix::dense::RowMajorMatrix, prover::Proof, system::{ProverKey, System, SystemWitness}, - types::{CommitmentParameters, FriParameters, GoldilocksBlake3Config, PcsError}, + types::{ + CommitmentParameters, FriParameters, GoldilocksBlake3Config, PcsError, + }, verifier::VerificationError, }; use rayon::iter::{ diff --git a/crates/aiur/src/vk_codec.rs b/crates/aiur/src/vk_codec.rs index f83e43c97..8effdb271 100644 --- a/crates/aiur/src/vk_codec.rs +++ b/crates/aiur/src/vk_codec.rs @@ -446,9 +446,10 @@ mod tests { #[test] fn rejects_trailing_bytes() { let (cp, fp) = test_parameters(); - let (system, _key) = System::new(AiurConfig::new(cp, fp), [ - LookupAir::new(AiurCircuit::Bytes1, Bytes1.lookups()), - ]); + let (system, _key) = System::new( + AiurConfig::new(cp, fp), + [LookupAir::new(AiurCircuit::Bytes1, Bytes1.lookups())], + ); let mut bytes = to_bytes(&system, cp, fp); bytes.push(0); assert!(from_bytes(&bytes).is_err(), "should reject trailing data"); diff --git a/crates/ffi/src/aiur/protocol.rs b/crates/ffi/src/aiur/protocol.rs index e155fe049..63163d547 100644 --- a/crates/ffi/src/aiur/protocol.rs +++ b/crates/ffi/src/aiur/protocol.rs @@ -52,8 +52,8 @@ extern "C" fn rs_aiur_proof_to_bytes( extern "C" fn rs_aiur_proof_of_bytes( byte_array: LeanByteArray>, ) -> LeanExternal { - let proof = - AiurProof::from_bytes(byte_array.as_bytes()).expect("Deserialization error"); + let proof = AiurProof::from_bytes(byte_array.as_bytes()) + .expect("Deserialization error"); LeanExternal::alloc(&AIUR_PROOF_CLASS, proof) } From 03e039b32affdbcc2ce21b04f1d5254360f76f1b Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Sat, 11 Jul 2026 00:29:58 -0400 Subject: [PATCH 3/4] chore: Pin multi-stark at main (blake3 merged as #61) The multi-stark Blake3 migration merged to its main as 2c01922 (perf: Switch from Keccak to Blake3 hashing #61), so pin there instead of the pre-merge blake3 branch tip. --- Cargo.lock | 2 +- Cargo.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 78a40ab8a..53739e47e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2075,7 +2075,7 @@ dependencies = [ [[package]] name = "multi-stark" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/multi-stark.git?rev=75fcd1b2e9f2cdf19422892598d0f0d69fd82521#75fcd1b2e9f2cdf19422892598d0f0d69fd82521" +source = "git+https://github.com/argumentcomputer/multi-stark.git?rev=2c019220cb43ce946efec6b9caf507f5a6bccd1c#2c019220cb43ce946efec6b9caf507f5a6bccd1c" dependencies = [ "bincode", "p3-air", diff --git a/Cargo.toml b/Cargo.toml index 840d45d70..73fe0ea7b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -50,7 +50,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 = "75fcd1b2e9f2cdf19422892598d0f0d69fd82521" } +multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "2c019220cb43ce946efec6b9caf507f5a6bccd1c" } num-bigint = "0.4.6" quickcheck = "1.0.3" quickcheck_macros = "1.0.0" From 6bf143098ac50a9e1d2c07268fb3e5e84c3ac830 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 14 Jul 2026 18:28:42 -0400 Subject: [PATCH 4/4] bench: Benchmark recursion at the q=100 soundness level MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The recursion path measured q=3 / q=1 — tractable but cryptographically toy configs. A real recursive proof needs ~100 FRI queries for soundness, so the query count is now 100 everywhere in the recursion path: - aiur-recursive configs: square-q100-b1 and factorial-q100-b2 - aiur --recursive mode: recursiveFriParameters numQueries=100 - bench-recursive-verifier default: --queries 100 (pass a small value for a cheap local run) At q=100 the verifier's query loop (~96% of its cost) grows ~33x, so the verifier trace is ~15x larger (measured: 1.19e9 -> 1.83e10 fft on the factorial toy) and the outer prove needs ~100 GB — marginal on a 128 GB host. An OOM row there is the honest signal that secure recursion does not yet fit; the standing feasibility gap is the point of the metric. --- Benchmarks/RecursiveVerifier.lean | 8 +++++--- Benchmarks/Typecheck.lean | 14 ++++++++------ Ix/Cli/BenchCmd.lean | 17 ++++++++++------- docs/benchmarking.md | 2 +- 4 files changed, 24 insertions(+), 17 deletions(-) diff --git a/Benchmarks/RecursiveVerifier.lean b/Benchmarks/RecursiveVerifier.lean index d6403f088..afc51aa02 100644 --- a/Benchmarks/RecursiveVerifier.lean +++ b/Benchmarks/RecursiveVerifier.lean @@ -18,11 +18,13 @@ of `Tests/MultiStark.lean::endToEndSuite`, but measures cost instead of asserting accept/reject. ``` -lake exe bench-recursive-verifier # factorial(5), q=3, blowup 2 +lake exe bench-recursive-verifier # factorial(5), q=100 (soundness level — heavy) +lake exe bench-recursive-verifier --queries 3 # cheap local run (toy soundness) lake exe bench-recursive-verifier --execute-only # skip the outer prove (FFT/exec only) --trivial square(5) instead of factorial(5) — the per-statement floor - --queries N FRI query count (default 3) + --queries N FRI query count (default 100 = soundness level; pass a + small value for a cheap local run) --blowup N log2 blowup (default 2) --pow N commit PoW bits (default 20) --json write a benchmark results row (Ix.Benchmark.Results); the @@ -82,7 +84,7 @@ def recCommitParams (args : List String) : Aiur.CommitmentParameters := { logBlowup := argNat args "--blowup" 2, capHeight := 0 } def innerFri (args : List String) : Aiur.FriParameters := { logFinalPolyLen := argNat args "--final-poly" 0, maxLogArity := 1, - numQueries := argNat args "--queries" 3, + numQueries := argNat args "--queries" 100, commitProofOfWorkBits := argNat args "--pow" 20, queryProofOfWorkBits := 0 } def secs (t0 t1 : Nat) : Float := (Float.ofNat (t1 - t0)) / 1e9 diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 45386f3d6..3c5b9f183 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -125,15 +125,17 @@ def recursiveCommitmentParameters : Aiur.CommitmentParameters := { capHeight := 0 } -/-- Recursion-tuned FRI parameters: the in-circuit verifier's cost scales with - the inner proof's query count, so the recursion configuration trades - queries (3, not 100) for blowup and commit proof-of-work. `--recursive` - runs the WHOLE system — the inner prove included — under these, so its - rows are not comparable to the standard `prove` cell's. -/ +/-- Recursion FRI parameters for `--recursive`. The query count IS the + soundness level, so a real (secure) recursive proof needs the full query + count, not a toy handful. The in-circuit verifier's cost scales with that + count, so at IxVM scale the cell is expected to exceed even a 128 GB host — + an OOM row here documents the gap between secure recursion and what fits + today. `--recursive` runs the WHOLE system, inner prove included, under + these, so its rows are not comparable to the standard `prove` cell's. -/ def recursiveFriParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 - numQueries := 3 + numQueries := 100 commitProofOfWorkBits := 20 queryProofOfWorkBits := 0 } diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index f6b7a0d26..2aa8c13c4 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -199,14 +199,17 @@ def backendSpecs : List BackendSpec := [ def findBackend (name : String) : Option BackendSpec := backendSpecs.find? (·.name == name) -/-- The `recursive` backend's rows: (row name, bench-recursive-verifier - config args). Fixed configs rather than `Vectors.csv` constants — the - toy proves the same tiny statements everywhere: `square-q1-b1` is the - floor config (completes at ~80 GB under Keccak; ~2.6 GB under Blake3) - and `factorial-q3-b2` the recursion-tuned default. -/ +/-- The `aiur-recursive` backend's rows: (row name, bench-recursive-verifier + config args). Fixed configs, not `Vectors.csv` constants. The FRI query + count IS the soundness level, so a benchmark of *secure* recursion uses the + real security requirement (~100 queries) throughout; the two rows vary the + inner statement and blowup (`square`, trivial + blowup 1, is the lighter + end; `factorial`, recursive + blowup 2, the heavier). At this query count + both outer proves strain a 128 GB host, so an OOM row is the honest signal + that secure recursion does not yet fit. -/ def recursiveConfigs : List (String × Array String) := [ - ("square-q1-b1", #["--trivial", "--queries", "1", "--blowup", "1"]), - ("factorial-q3-b2", #[]) + ("square-q100-b1", #["--trivial", "--queries", "100", "--blowup", "1"]), + ("factorial-q100-b2", #["--queries", "100"]) ] def BackendSpec.testbedFor (b : BackendSpec) (mode : String) : Option String := diff --git a/docs/benchmarking.md b/docs/benchmarking.md index 515f4cd34..f16d6ecb6 100644 --- a/docs/benchmarking.md +++ b/docs/benchmarking.md @@ -97,7 +97,7 @@ a PR tree and compare them — exactly what the PR workflow does. | backend | what it measures | tool | |---|---|---| | `aiur` | Aiur STARK check, one bench-main cell per mode on its own testbed: prove — the real-workload simulation (prove-time, proof-size, verify-time, peak-rss, plus fft-cost / execute-time from its own Phase 1) — and execute, the fast Phase-1-only signal (fft-cost, execute-time, throughput, peak-rss). `!benchmark aiur [execute]` picks the mode. A third mode, recursive (`bench-typecheck --recursive`), additionally executes AND proves the in-circuit multi-stark verifier over each fresh proof — the whole system runs under recursion-tuned FRI parameters, so its rows land on their own testbed (`aiur-check-recursive`) and are not comparable to the prove cell's. Local-only (`ix bench run --backend aiur --mode recursive`): an IxVM-scale verifier execute needs >108 GB, beyond the CI ceiling, so no CI job or comment token schedules it | `bench-typecheck` | -| `aiur-recursive` | the aiur-recursive toy: prove a fixed tiny statement per config (`square-q1-b1`, the per-statement floor; `factorial-q3-b2`, the recursion-tuned default), run the in-circuit multi-stark verifier over the proof (recursive-execute-time, recursive-fft-cost — the recursion-cost proxy), then prove that execution end-to-end (recursive-prove-time, recursive-peak-rss, recursive-proof-size, recursive-verify-time). Env-independent: fixed configs instead of `Vectors.csv` constants, no `.ixe`, always exactly one cell regardless of `BENCH_ENVS` | `bench-recursive-verifier` | +| `aiur-recursive` | the aiur-recursive toy: prove a fixed tiny statement per config, both at the ~100-query soundness level (`square-q100-b1`, the lighter trivial-statement end; `factorial-q100-b2`, the heavier recursive one), run the in-circuit multi-stark verifier over the proof (recursive-execute-time, recursive-fft-cost — the recursion-cost proxy), then prove that execution end-to-end (recursive-prove-time, recursive-peak-rss, recursive-proof-size, recursive-verify-time). Env-independent: fixed configs instead of `Vectors.csv` constants, no `.ixe`, always exactly one cell regardless of `BENCH_ENVS` | `bench-recursive-verifier` | | `zisk` | ZisK VM execute: cycles, execute-time, throughput, peak-rss, constants (pre-shard closure count, same universe as aiur's), shards (1 when unsharded) | `zisk-host` | | `sp1` | SP1 VM execute (currently disabled in the registry) | `sp1-host` | | `ooc` | out-of-circuit Rust kernel: whole-env row + one full-closure row per primary (`check-time` wraps only the check — the env loads once, outside every row's timed window) | `ix check-rs --json` |