From e16ae7fa0a4945413ed1bb04aa7ac1fcf9ec46b6 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Wed, 5 Aug 2026 13:15:35 -0700 Subject: [PATCH] aiur: ground the FFT cost model in the prover's actual transforms MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The per-circuit FFT cost statistic (`Ix/Aiur/Statistics.lean`) was `(stage1 + stage2 width) * h * log2(h)` over function and memory circuits only. Compared against the pinned prover (multi-stark `be1755e`, Plonky3 `e9d7561`), that misses: - the quotient chunk columns: `q*D` committed base columns per circuit, `q = next_pow2(max(d, 2) - 1)` — constraint-degree changes were invisible to the statistic; - the commit transform structure: `Radix2DitParallel::coset_lde_batch` runs one size-h inverse DFT plus B size-h coset DFTs per column, not one size-`B*h` DFT; - the two quotient-rebasing transforms: the iDFT of the `(q*h) x D` flattened quotient and the size-h DFT of the `q*D` coefficient slices; - the `Bytes1`/`Bytes2` gadget circuits, whose witness builders always emit full tables (256 / 65536 rows with zero multiplicities on unqueried rows), so they are active in every proof as a fixed cost. The new per-circuit cost, with `F(0) = 0`, `F(x) = x*log2(max(x, 2))`, and the raw (unpadded) height `h` so one-row changes stay visible while structural powers of two (`B`, `q`) stay exact: (B+1)*(m + s2 + q*D)*F(h) + D*F(q*h) + q*D*F(h) summed over constrained functions, memories, `Bytes1`, and `Bytes2`. Circuit shapes (main/stage-2 width, quotient degree, preprocessed dimensions) are read off the compiled Rust `System` through a new `AiurSystem::circuit_shapes` API and FFI — never re-derived in Lean, since `max_constraint_degree` requires the compiled constraint graph. `ix check` statistics use a one-shot build-extract-drop variant (that flow never builds a system otherwise, and pays the build only when stats are requested). The prove/verify/stats parameter triple is deduplicated into `Aiur.defaultCommitmentParameters` / `defaultFriParameters`. The report now prints per-circuit costs in scientific notation (two-decimal mantissa); the total stays in full digits with the scientific form in parentheses. A new `aiur-cost` primary suite covers the pure formula: exact values at power-of-two heights, one-row monotonicity across power-of-two boundaries (where the padded prover plateaus), per-input monotonicity in width, lookups, quotient degree, and blowup, and the scientific formatter (including the mantissa-carry edge). A Rust test pins `circuit_shapes` against `System.circuits` field-for-field, including canonical order and the fixed gadget table dimensions. FFT pins regenerated from one `lake test -- --ignored ixvm` run (only the FFT pin assertions moved; all execution/parity tests passed). Small constants now sit on a ~174M fixed floor that is almost entirely the always-active `Bytes2` commit: `5 * 32 * F(65536) ≈ 168M`. --- Benchmarks/RecursionDebug.lean | 4 +- Benchmarks/RecursiveVerifier.lean | 6 +- Benchmarks/Typecheck.lean | 9 +- Ix/Aiur/Protocol.lean | 41 ++++++++++ Ix/Aiur/Statistics.lean | 130 +++++++++++++++++++++-------- Ix/Cli/CheckCmd.lean | 10 ++- Ix/Cli/ProveCmd.lean | 21 ++--- Ix/Cli/VerifyCmd.lean | 20 ++--- Tests/Aiur.lean | 1 + Tests/Aiur/Common.lean | 7 +- Tests/Aiur/Cost.lean | 79 ++++++++++++++++++ Tests/Ix/IxVM.lean | 132 +++++++++++++++--------------- Tests/Main.lean | 7 +- crates/aiur/src/synthesis.rs | 69 ++++++++++++++++ crates/ffi/src/aiur/protocol.rs | 50 ++++++++++- crates/ffi/src/lean.rs | 3 + 16 files changed, 450 insertions(+), 139 deletions(-) create mode 100644 Tests/Aiur/Cost.lean diff --git a/Benchmarks/RecursionDebug.lean b/Benchmarks/RecursionDebug.lean index f0e7bb062..8bc203020 100644 --- a/Benchmarks/RecursionDebug.lean +++ b/Benchmarks/RecursionDebug.lean @@ -204,7 +204,9 @@ def main (args : List String) : IO UInt32 := do return 1 | .ok (out, qc) => let t1 ← IO.monoNanosNow - let stats := Aiur.computeStats vCompiled qc + let vShapes := Aiur.circuitShapes vCompiled.bytecode commitParams fri + let stats := Aiur.computeStats vCompiled qc vShapes + (logBlowup := commitParams.logBlowup) IO.println s!"ACCEPTED in {secs t0 t1} s, output {out}, \ fft-cost {stats.totalFftCost}" return 0 diff --git a/Benchmarks/RecursiveVerifier.lean b/Benchmarks/RecursiveVerifier.lean index d3c312a4c..30c761c52 100644 --- a/Benchmarks/RecursiveVerifier.lean +++ b/Benchmarks/RecursiveVerifier.lean @@ -163,7 +163,11 @@ def main (args : List String) : IO UInt32 := do | .error e => IO.eprintln s!"verifier execution REJECTED: {e}"; return 1 | .ok (_, qc) => let e1 ← IO.monoNanosNow - let stats := Aiur.computeStats vCompiled qc + -- One-shot shapes: `vSystem` (below) exists only when `--prove` is set, + -- and `--log-blowup` is configurable here — thread it into the model. + let vShapes := Aiur.circuitShapes vCompiled.bytecode recCommitParams innerFri + let stats := Aiur.computeStats vCompiled qc vShapes + (logBlowup := recCommitParams.logBlowup) IO.println s!"verifier accepted, execute {secs e0 e1} s" IO.println s!"\n=== recursive verifier in-circuit cost ===" IO.println s!"totalFftCost = {stats.totalFftCost}" diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 983772aae..179e8c22a 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -382,6 +382,9 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do -- witness is a small subject-only blob — keep Lean witness + -- `executeIxVM`. IO.println "── Phase 1: execute (witness generation) ──" + -- Shapes off the already-built system (cheap: reads the compiled + -- circuits), hoisted out of the per-constant loop. + let shapes := aiurSystem.circuitShapes let mut execed : Array (Result × Address) := #[] let mut execIdx := 0 for (label, addr) in targets do @@ -408,7 +411,8 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do ({ name := label, constants := 0, fftCost := 0, executeSec := 0, failed := true }, addr) | .ok (_, _, queryCounts) => - let stats := Aiur.computeStats compiled queryCounts + let stats := Aiur.computeStats compiled queryCounts shapes + (logBlowup := commitParams.logBlowup) -- Constants CHECKED, not shipped: `check_const` is memoized per -- (ci, addr), so its unique query count is exactly the number of -- constants the kernel typechecked. The shipped byte scope @@ -543,7 +547,8 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do | .error e => IO.eprintln s!" ❌ recursive verifier REJECTED {r.name}'s proof: {e}" | .ok (_, qc) => - let rvStats := Aiur.computeStats vCompiled qc + let rvStats := Aiur.computeStats vCompiled qc vSystem.circuitShapes + (logBlowup := commitParams.logBlowup) IO.println s!" {r.name}: recursive={rvSec}s \ recursive-fft-cost={rvStats.totalFftCost}" -- The per-circuit breakdown names where the verifier's cost diff --git a/Ix/Aiur/Protocol.lean b/Ix/Aiur/Protocol.lean index b43f9d827..705f2565f 100644 --- a/Ix/Aiur/Protocol.lean +++ b/Ix/Aiur/Protocol.lean @@ -38,6 +38,34 @@ structure FriParameters where commitProofOfWorkBits : Nat queryProofOfWorkBits : Nat +/-- Canonical Aiur parameters, shared by `ix prove`, `ix verify`, and the +`ix check` statistics. Until these become flags / commit to the proof +header, every flow MUST use the same values or proofs won't verify. -/ +def defaultCommitmentParameters : CommitmentParameters := + { logBlowup := 2, capHeight := 0 } + +def defaultFriParameters : FriParameters := { + logFinalPolyLen := 0 + maxLogArity := 1 + numQueries := 100 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 +} + +/-- Shape of one compiled circuit, built directly by Rust +(`LeanAiurCircuitShape` in `crates/ffi/src/lean.rs`; field order must +match). Heights of function and memory circuits are execution-dependent +and are not part of the shape; `preprocessedHeight` doubles as the fixed +trace height of the byte-gadget circuits (256 and 65536), whose witness +builders always emit the full table. -/ +structure CircuitShape where + mainWidth : Nat + stage2Width : Nat + quotientDegree : Nat + preprocessedWidth : Nat + preprocessedHeight : Nat + deriving Inhabited + private opaque AiurSystemNonempty : NonemptyType def AiurSystem : Type := AiurSystemNonempty.type instance : Nonempty AiurSystem := AiurSystemNonempty.property @@ -71,6 +99,11 @@ opaque build : @&Bytecode.Toplevel → @&CommitmentParameters → @&FriParameter @[extern "rs_aiur_system_vk_bytes"] opaque vkBytes : @& AiurSystem → ByteArray +/-- Per-circuit shapes in canonical system order: constrained functions +(ascending index), memories, `Bytes1`, `Bytes2`. -/ +@[extern "rs_aiur_system_circuit_shapes"] +opaque circuitShapes : @& AiurSystem → Array CircuitShape + @[extern "rs_aiur_system_prove"] private opaque prove' : @& AiurSystem → @& Bytecode.FunIdx → @& Array G → @@ -154,6 +187,14 @@ opaque verify : @& AiurSystem → end AiurSystem +/-- One-shot variant of `AiurSystem.circuitShapes` for flows that never +build an `AiurSystem` (the `ix check` statistics): Rust builds the system, +extracts the shapes, and drops it. -/ +@[extern "rs_aiur_circuit_shapes"] +opaque circuitShapes : + @& Bytecode.Toplevel → @& CommitmentParameters → @& FriParameters → + Array CircuitShape + abbrev functionChannel : G := .ofNat 0 def buildClaim (funIdx : Bytecode.FunIdx) (input output : Array G) := diff --git a/Ix/Aiur/Statistics.lean b/Ix/Aiur/Statistics.lean index d50d40496..de4e26c41 100644 --- a/Ix/Aiur/Statistics.lean +++ b/Ix/Aiur/Statistics.lean @@ -1,17 +1,33 @@ module public import Ix.Aiur.Compiler public import Ix.Aiur.Semantics.BytecodeFfi +public import Ix.Aiur.Protocol /-! Circuit statistics for Aiur executions. -Given a `CompiledToplevel` and the per-circuit `QueryCount`s -returned by `execute`, computes per-circuit width, height (the unique-row -count), cache hits (sum of multiplicities), and the FFT cost -(width × height × log2(height)) for every constrained function and memory -circuit. The FFT cost is a Float to capture small changes continuously. -Results are sorted by FFT cost in decreasing order and printed with cumulative -FFT cost percentages. +Given a `CompiledToplevel`, the per-circuit `QueryCount`s returned by +`execute`, and the per-circuit `CircuitShape`s read off the compiled Rust +`System`, computes per-circuit committed width, height (the unique-row +count), cache hits (sum of multiplicities), and the FFT cost for every +system circuit — constrained functions, memories, and the fixed-height +`Bytes1`/`Bytes2` byte gadgets. + +The FFT cost counts the transforms the pinned prover actually runs, per +committed column, using the raw (unpadded) height `h` so the statistic +stays sensitive to one-row changes (the real prover pads `h` to a power of +two; structural powers of two like the blowup `B` and the quotient degree +`q` stay exact): + +- each PCS commit (stage 1 width `m`, stage 2 width `s2`, quotient chunks + `q·D`) is one size-`h` inverse DFT plus `B` size-`h` coset DFTs per + column (`Radix2DitParallel::coset_lde_batch`), i.e. `(B+1)·F(h)`; +- the quotient rebase adds an iDFT of the `(q·h) × D` flattened quotient + and a size-`h` DFT of the `q·D` coefficient slices, + +where `F(0) = 0` and `F(x) = x·log2(max(x, 2))`. Costs are `Float`s to +capture small changes continuously. Results are sorted by FFT cost in +decreasing order and printed with cumulative FFT cost percentages. -/ public section @@ -24,53 +40,88 @@ structure CircuitStats where height : Nat cacheHits : Nat fftCost : Float + /-- FFT cost at the uncached height `height + cacheHits` (fixed-height + gadget circuits keep their normal cost). Feeds `totalUncachedFftCost`. -/ + uncachedFftCost : Float structure ExecutionStats where circuits : Array CircuitStats totalFftCost : Float totalUncachedFftCost : Float totalCacheHits : Nat + deriving Inhabited --- Clamp to at least 2 so that log2 is at least 1, avoiding zero cost for h = 1 -def fftCost (w h : Nat) : Float := - if h == 0 then 0.0 +/-- Continuous transform-size surrogate: `0` at `0` (an empty circuit is +deactivated by the prover), else `x·log2(max(x, 2))` — the clamp keeps a +height-1 transform nonzero. -/ +def transformCost (x : Nat) : Float := + if x == 0 then 0.0 else - let wf := w.toFloat - let hf := h.toFloat - wf * hf * (max hf 2.0).log2 + let xf := x.toFloat + xf * (max xf 2.0).log2 + +/-- FFT work of one circuit at height `h`: `(B+1)` size-`h` transforms per +committed column (three PCS commits), plus the two quotient-rebasing +transforms. See the module docstring. -/ +def fftCost (shape : CircuitShape) (h : Nat) (logBlowup : Nat) : Float := + let qD := shape.quotientDegree * G.extensionDegree + let commitWidth := shape.mainWidth + shape.stage2Width + qD + ((2 ^ logBlowup) + 1).toFloat * commitWidth.toFloat * transformCost h + + G.extensionDegree.toFloat * transformCost (shape.quotientDegree * h) + + qD.toFloat * transformCost h + +/-- Committed width of a circuit: stage 1 + stage 2 + quotient chunks. -/ +def CircuitShape.committedWidth (shape : CircuitShape) : Nat := + shape.mainWidth + shape.stage2Width + shape.quotientDegree * G.extensionDegree -def computeStats (compiled : CompiledToplevel) (queryCounts : Array QueryCount) : +def computeStats (compiled : CompiledToplevel) (queryCounts : Array QueryCount) + (shapes : Array CircuitShape) + (logBlowup : Nat := defaultCommitmentParameters.logBlowup) : ExecutionStats := let t := compiled.bytecode -- Invert nameMap to get FunIdx → String let reverseMap := compiled.nameMap.fold (init := (∅ : Std.HashMap Bytecode.FunIdx String)) fun acc global idx => if !acc.contains idx then acc.insert idx (toString global) else acc let nAllFuns := t.functions.size + let nConstrained := t.functions.foldl (fun n f => if f.constrained then n + 1 else n) 0 + -- Shapes arrive in canonical system order: constrained functions + -- (ascending index), memories, `Bytes1`, `Bytes2`. A mismatch means the + -- shapes were built from a different toplevel; misindexing would silently + -- attribute costs to the wrong circuits. + if shapes.size != nConstrained + t.memorySizes.size + 2 then + panic! s!"computeStats: {shapes.size} circuit shapes for \ + {nConstrained} constrained functions + {t.memorySizes.size} memories + 2 gadgets" + else + let mkStats (name : String) (shape : CircuitShape) (h hits : Nat) : CircuitStats := + { name, width := shape.committedWidth, height := h, cacheHits := hits, + fftCost := fftCost shape h logBlowup, + uncachedFftCost := fftCost shape (h + hits) logBlowup } let functionCircuits := Id.run do let mut acc := #[] + let mut shapeIdx := 0 for i in [:nAllFuns] do if t.functions[i]!.constrained then - let w := t.functions[i]!.layout.totalWidth + let shape := shapes[shapeIdx]! + shapeIdx := shapeIdx + 1 let qc := queryCounts[i]! - let h := qc.uniqueRows - let hits := qc.totalHits - qc.uniqueRows let name := reverseMap[i]?.getD s!"" - acc := acc.push { name, width := w, height := h, cacheHits := hits, fftCost := fftCost w h : CircuitStats } + acc := acc.push + (mkStats name shape qc.uniqueRows (qc.totalHits - qc.uniqueRows)) acc let memoryCircuits := t.memorySizes.mapIdx fun i size => - -- Mirrors `crates/aiur/src/memory.rs` (`Memory::width`): multiplicity + - -- selector + pointer + `size` value columns; the single lookup adds - -- `G.extensionDegree * max(1, 1)` stage-2 columns (one chained - -- accumulator, no message inverse), as in `FunctionLayout.totalWidth`. - let w := 3 + size + G.extensionDegree + let shape := shapes[nConstrained + i]! let qc := queryCounts[nAllFuns + i]! - let h := qc.uniqueRows - let hits := qc.totalHits - qc.uniqueRows - { name := s!"memory[{size}]", - width := w, height := h, cacheHits := hits, fftCost := fftCost w h : CircuitStats } - let circuits := (functionCircuits ++ memoryCircuits).qsort (·.fftCost > ·.fftCost) + mkStats s!"memory[{size}]" shape qc.uniqueRows (qc.totalHits - qc.uniqueRows) + -- The byte gadgets commit full-table traces in every proof: their height + -- is the (fixed) preprocessed height, independent of the query set, so + -- they carry no cache-hit counterfactual. + let gadgetCircuits := #["Bytes1", "Bytes2"].mapIdx fun i name => + let shape := shapes[nConstrained + t.memorySizes.size + i]! + mkStats name shape shape.preprocessedHeight 0 + let circuits := (functionCircuits ++ memoryCircuits ++ gadgetCircuits).qsort + (·.fftCost > ·.fftCost) let totalFftCost := circuits.foldl (· + ·.fftCost) 0.0 - let totalUncachedFftCost := circuits.foldl (fun acc cs => acc + fftCost cs.width (cs.height + cs.cacheHits)) 0.0 + let totalUncachedFftCost := circuits.foldl (· + ·.uncachedFftCost) 0.0 let totalCacheHits := circuits.foldl (· + ·.cacheHits) 0 { circuits, totalFftCost, totalUncachedFftCost, totalCacheHits } @@ -92,6 +143,21 @@ private def formatPercent (fftCost totalFftCost : Float) : String := let fracStr := if frac < 10 then s!"0{frac}" else toString frac s!"{whole}.{fracStr}%" +/-- Scientific notation with a two-decimal mantissa (`1.74e8`). Only used +for nonnegative costs; any nonzero circuit cost is ≥ 1, so the exponent +is never negative. -/ +def formatSci (f : Float) : String := + if f == 0.0 then "0" + else + let e := f.log10.floor + let cents := (f / (10.0 ^ e) * 100.0).round + -- Rounding can push the mantissa to 10.00; carry into the exponent. + let (cents, e) := if cents >= 1000.0 then (100.0, e + 1.0) else (cents, e) + let cents := cents.toUInt64.toNat + let frac := cents % 100 + let fracStr := if frac < 10 then s!"0{frac}" else toString frac + s!"{cents / 100}.{fracStr}e{e.toUInt64.toNat}" + def printStats (stats : ExecutionStats) : IO Unit := do let wName := stats.circuits.foldl (fun m cs => Nat.max m cs.name.length) 4 let wWidth := stats.circuits.foldl (fun m cs => Nat.max m (toString cs.width).length) 5 @@ -100,7 +166,7 @@ def printStats (stats : ExecutionStats) : IO Unit := do let formatCost (f : Float) : String := let n := f.round.toUInt64.toNat toString n - let wFftCost := stats.circuits.foldl (fun m cs => Nat.max m (formatCost cs.fftCost).length) 7 + let wFftCost := stats.circuits.foldl (fun m cs => Nat.max m (formatSci cs.fftCost).length) 8 let wPct := 7 let wCum := 7 let totalW := wName + 1 + wWidth + 1 + wHeight + 1 + wHits + 1 + wFftCost + 1 + wPct + 1 + wCum @@ -112,7 +178,7 @@ def printStats (stats : ExecutionStats) : IO Unit := do IO.println "=== Circuit Statistics ===" IO.println s!"Circuits: {stats.circuits.size}" IO.println s!"Total width: {totalWidth}" - IO.println s!"Total FFT cost: {formatCost stats.totalFftCost}" + IO.println s!"Total FFT cost: {formatCost stats.totalFftCost} ({formatSci stats.totalFftCost})" IO.println s!"Total cache hits: {stats.totalCacheHits}" IO.println s!"Total saved cost: {savedPct}" IO.println sep @@ -123,7 +189,7 @@ def printStats (stats : ExecutionStats) : IO Unit := do cumFftCost := cumFftCost + cs.fftCost let pct := formatPercent cs.fftCost stats.totalFftCost let cum := formatPercent cumFftCost stats.totalFftCost - IO.println s!"{padRight cs.name wName} {padLeft (toString cs.width) wWidth} {padLeft (toString cs.height) wHeight} {padLeft (toString cs.cacheHits) wHits} {padLeft (formatCost cs.fftCost) wFftCost} {padLeft pct wPct} {padLeft cum wCum}" + IO.println s!"{padRight cs.name wName} {padLeft (toString cs.width) wWidth} {padLeft (toString cs.height) wHeight} {padLeft (toString cs.cacheHits) wHits} {padLeft (formatSci cs.fftCost) wFftCost} {padLeft pct wPct} {padLeft cum wCum}" end Aiur diff --git a/Ix/Cli/CheckCmd.lean b/Ix/Cli/CheckCmd.lean index 8756255ab..565538782 100644 --- a/Ix/Cli/CheckCmd.lean +++ b/Ix/Cli/CheckCmd.lean @@ -88,11 +88,17 @@ def mkWitness (addr : Address) (ixonEnv : Ixon.Env) : /-- Compute + emit per-circuit stats. With `statsOut = none` prints to stdout; with `some path` redirects stdout to the file for the - duration of `printStats` so the terminal stays clean. -/ + duration of `printStats` so the terminal stays clean. + + Circuit shapes come from the one-shot FFI (`Aiur.circuitShapes`), + which builds and drops an `AiurSystem` — the check flow never builds + one otherwise. That cost is paid only when stats are requested. -/ def emitStats (compiled : Aiur.CompiledToplevel) (queryCounts : Array Aiur.QueryCount) (statsOut : Option String) : IO Unit := do - let stats := Aiur.computeStats compiled queryCounts + let shapes := Aiur.circuitShapes compiled.bytecode + Aiur.defaultCommitmentParameters Aiur.defaultFriParameters + let stats := Aiur.computeStats compiled queryCounts shapes match statsOut with | none => Aiur.printStats stats | some path => do diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean index 2342a172b..a35609d9a 100644 --- a/Ix/Cli/ProveCmd.lean +++ b/Ix/Cli/ProveCmd.lean @@ -43,20 +43,15 @@ open IxVM.ClaimHarness namespace Ix.Cli.ProveCmd -/-- Canonical aiur params shared between prove and verify. Matches - `Tests.Aiur.Common`. Until these become flags / commit to the - proof header, they MUST stay in sync between `prove` and - `verify`. -/ +/-- Canonical aiur params shared between prove and verify (the shared + defaults in `Ix.Aiur.Protocol`). Matches `Tests.Aiur.Common`. Until + these become flags / commit to the proof header, they MUST stay in + sync between `prove` and `verify`. -/ private def commitmentParameters : Aiur.CommitmentParameters := - { logBlowup := 2, capHeight := 0 } - -private def friParameters : Aiur.FriParameters := { - logFinalPolyLen := 0 - maxLogArity := 1 - numQueries := 100 - commitProofOfWorkBits := 0 - queryProofOfWorkBits := 20 -} + Aiur.defaultCommitmentParameters + +private def friParameters : Aiur.FriParameters := + Aiur.defaultFriParameters def proveOne (aiurSystem : Aiur.AiurSystem) (compiled : Aiur.CompiledToplevel) diff --git a/Ix/Cli/VerifyCmd.lean b/Ix/Cli/VerifyCmd.lean index 3c1943f9d..381352579 100644 --- a/Ix/Cli/VerifyCmd.lean +++ b/Ix/Cli/VerifyCmd.lean @@ -34,19 +34,15 @@ private def addrOfHex! (label : String) (s : String) : IO Address := do throw <| IO.userError s!"error: {label}: expected 64-char hex (32-byte address), got {s.length}-char {s}" -/-- Same parameters as `ix prove`. Mismatch makes verification fail - silently with no useful diagnostic, so these MUST match the - proving side until they migrate into the proof header. -/ +/-- Same parameters as `ix prove` (the shared canonical defaults). + Mismatch makes verification fail silently with no useful diagnostic, + so these MUST match the proving side until they migrate into the + proof header. -/ private def commitmentParameters : Aiur.CommitmentParameters := - { logBlowup := 2, capHeight := 0 } - -private def friParameters : Aiur.FriParameters := { - logFinalPolyLen := 0 - maxLogArity := 1 - numQueries := 100 - commitProofOfWorkBits := 0 - queryProofOfWorkBits := 20 -} + Aiur.defaultCommitmentParameters + +private def friParameters : Aiur.FriParameters := + Aiur.defaultFriParameters /-- Verify one persisted `Ixon.Proof` wrapper (by store address) against its bundled claim, using an already-built Aiur backend. -/ diff --git a/Tests/Aiur.lean b/Tests/Aiur.lean index b1af44f71..dcdafc545 100644 --- a/Tests/Aiur.lean +++ b/Tests/Aiur.lean @@ -2,6 +2,7 @@ module public import Tests.Aiur.Common public import Tests.Aiur.Aiur +public import Tests.Aiur.Cost public import Tests.Aiur.Hashes public import Tests.Aiur.RBTreeMap public import Tests.Aiur.Cross diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean index 182af0231..f90e64f66 100644 --- a/Tests/Aiur/Common.lean +++ b/Tests/Aiur/Common.lean @@ -70,6 +70,7 @@ structure AiurTestEnv where compiled : Aiur.CompiledToplevel decls : Aiur.Source.Decls aiurSystem : Aiur.AiurSystem + shapes : Array Aiur.CircuitShape def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Source.Toplevel) : Except String AiurTestEnv := do @@ -77,7 +78,7 @@ def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Source.Toplevel) : let compiled ← toplevel.compile let decls ← toplevel.mkDecls.mapError toString let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters - return ⟨compiled, decls, aiurSystem⟩ + return ⟨compiled, decls, aiurSystem, aiurSystem.circuitShapes⟩ def AiurTestEnv.interpTest (env : AiurTestEnv) (testCase : AiurTestCase) (execOutput : Array Aiur.G) (execIOBuffer : Aiur.IOBuffer) : TestSeq := @@ -112,7 +113,7 @@ def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : Test let fftTest := match testCase.expectedFftCost with | none => .done | some expected => - let stats := Aiur.computeStats env.compiled queryCounts + let stats := Aiur.computeStats env.compiled queryCounts env.shapes let actual := stats.totalFftCost.round.toUInt64.toNat test s!"FFT cost matches for {label}: expected {expected}, got {actual}" (actual == expected) @@ -139,7 +140,7 @@ def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Source.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 friParameters - let env : AiurTestEnv := ⟨compiled, decls, aiurSystem⟩ + let env : AiurTestEnv := ⟨compiled, decls, aiurSystem, aiurSystem.circuitShapes⟩ cases.foldl (init := .done) fun tSeq testCase => tSeq ++ env.runTestCase testCase diff --git a/Tests/Aiur/Cost.lean b/Tests/Aiur/Cost.lean new file mode 100644 index 000000000..f23e1c700 --- /dev/null +++ b/Tests/Aiur/Cost.lean @@ -0,0 +1,79 @@ +module + +public import LSpec +public import Ix.Aiur + +/-! +Unit tests for the pure FFT cost model in `Ix/Aiur/Statistics.lean`. + +Everything here is `Float` arithmetic over integer inputs — fully +deterministic, no execution, no FFI. Exact equalities stick to inputs +whose logs are integral (powers of two); everything else is checked via +strict monotonicity, including across power-of-two boundaries where the +real (padded) prover would plateau. +-/ + +public section + +open LSpec Aiur + +namespace AiurTests.Cost + +/-- A small function-like circuit: main width 4, one lookup +(stage 2 width `D = 2`), quotient degree 2 (today's uniform value). -/ +def fnShape : CircuitShape := + { mainWidth := 4, stage2Width := 2, quotientDegree := 2, + preprocessedWidth := 0, preprocessedHeight := 0 } + +/-- `logBlowup = 2` (production `B = 4`): committed width +`4 + 2 + q·D = 10`; at `h = 8`: +`(B+1)·10·F(8) + D·F(16) + q·D·F(8) = 50·24 + 2·64 + 4·24 = 1424`. -/ +def handComputed : Float := 1424.0 + +def transformCostTests : TestSeq := + test "F(0) = 0 (empty circuit is deactivated)" (transformCost 0 == 0.0) ++ + test "F(1) = 1 (clamp keeps height-1 transforms nonzero)" + (transformCost 1 == 1.0) ++ + test "F(2) = 2" (transformCost 2 == 2.0) ++ + test "F(4) = 8" (transformCost 4 == 8.0) ++ + test "F(1024) = 10240" (transformCost 1024 == 10240.0) ++ + test "F strictly increases across a power-of-two boundary" + (transformCost 1023 < transformCost 1024 && + transformCost 1024 < transformCost 1025) + +def fftCostTests : TestSeq := + test "cost is zero at h = 0" (fftCost fnShape 0 2 == 0.0) ++ + test "hand-computed value at h = 8, logBlowup = 2" + (fftCost fnShape 8 2 == handComputed) ++ + test "one-row sensitivity at small heights" + (fftCost fnShape 1 2 < fftCost fnShape 2 2 && + fftCost fnShape 2 2 < fftCost fnShape 3 2) ++ + test "one-row sensitivity across a power-of-two boundary" + (fftCost fnShape 1023 2 < fftCost fnShape 1024 2 && + fftCost fnShape 1024 2 < fftCost fnShape 1025 2) ++ + test "wider main trace costs more" + (fftCost fnShape 8 2 < + fftCost { fnShape with mainWidth := fnShape.mainWidth + 1 } 8 2) ++ + test "extra lookup (wider stage 2) costs more" + (fftCost fnShape 8 2 < + fftCost { fnShape with stage2Width := fnShape.stage2Width + 2 } 8 2) ++ + test "higher quotient degree costs more" + (fftCost fnShape 8 2 < + fftCost { fnShape with quotientDegree := 4 } 8 2) ++ + test "larger blowup costs more" + (fftCost fnShape 8 1 < fftCost fnShape 8 2) ++ + test "committedWidth = main + stage2 + q·D" + (fnShape.committedWidth == 4 + 2 + 2 * G.extensionDegree) + +def formatSciTests : TestSeq := + test "formatSci 0 = 0" (formatSci 0.0 == "0") ++ + test "formatSci 1 = 1.00e0" (formatSci 1.0 == "1.00e0") ++ + test "formatSci 1424 = 1.42e3" (formatSci 1424.0 == "1.42e3") ++ + test "formatSci 174253453 = 1.74e8" (formatSci 174253453.0 == "1.74e8") ++ + test "mantissa carry: formatSci 999.9 = 1.00e3" (formatSci 999.9 == "1.00e3") + +def tests : TestSeq := transformCostTests ++ fftCostTests ++ formatSciTests + +end AiurTests.Cost + +end diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 6022954f2..5b4604bba 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -188,72 +188,72 @@ private def nameOfString (str : String) : Lean.Name := listed constant fails the suite, so a regression cannot land quietly and an improvement has to be acknowledged by re-pinning. -/ private def kernelCheckEntries : List (String × Nat) := [ - ("HEq", 396_267), - ("HEq.rec", 1_311_905), - ("Eq.rec", 1_239_724), - ("Nat", 398_336), - ("Nat.add", 9_696_843), - ("Nat.add_comm", 42_375_707), - ("Nat.decEq", 52_744_704), - ("Nat.decLe", 147_487_341), - ("Nat.sub_le_of_le_add", 401_101_967), - ("Nat.shiftRight_succ", 291_387_591), - ("Trans.mk", 1_635_822), - ("Array.append_assoc", 1_861_614_190), - ("Vector.append", 1_914_990_215), - ("IxVMPrim.nat_add_lit", 21_173_813), - ("IxVMPrim.nat_sub_lit", 25_877_844), - ("IxVMPrim.nat_mul_lit", 19_003_829), - ("IxVMPrim.nat_mul_big", 18_520_173), - ("IxVMPrim.nat_div_lit", 284_318_446), - ("IxVMPrim.nat_mod_lit", 290_903_252), - ("IxVMPrim.nat_succ_lit", 4_811_530), - ("IxVMPrim.nat_pred_lit", 10_858_515), - ("IxVMPrim.nat_gcd_lit", 471_798_408), - ("IxVMPrim.nat_land_lit", 799_156_568), - ("IxVMPrim.nat_lor_lit", 799_831_190), - ("IxVMPrim.nat_xor_lit", 805_615_928), - ("IxVMPrim.nat_shl_lit", 26_839_257), - ("IxVMPrim.nat_shr_lit", 288_362_941), - ("IxVMPrim.nat_pow_big", 57_840_233), - ("IxVMPrim.nat_beq_lit", 18_232_986), - ("IxVMPrim.nat_ble_lit", 16_851_217), - ("IxVMPrim.nat_cases_big", 10_575_443), - ("IxVMPrim.nat_dec_le", 152_401_268), - ("IxVMPrim.nat_dec_lt", 155_516_288), - ("IxVMPrim.nat_dec_eq", 63_259_938), - ("IxVMPrim.str_size_lit", 555_223_250), - ("IxVMPrim.bv_to_nat_lit", 448_080_398), - ("IxVMInd.Even", 19_814_542), - ("IxVMInd.Odd", 19_814_843), - ("IxVMInd.Even.rec", 24_361_340), - ("IxVMInd.Odd.rec", 24_362_006), - ("IxVMInd.Tree", 797_589), - ("IxVMInd.Tree.rec", 3_326_674), - ("IxVMInd.DedupM", 1_892_596), - ("IxVMInd.DedupM.rec", 5_207_701), - ("IxVMInd.DepthM", 1_348_131), - ("IxVMInd.DepthM.rec", 4_102_359), - ("String.Internal.append", 547_750_479), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 825_829_669), - ("Lean.Syntax.rec", 562_535_048), - ("IxVMInd.AuxTie", 53_023_517), - ("IxVMInd.AuxTie.rec", 63_340_386), - ("String.Slice.Pattern.Model.NoPrefixForwardPatternModel.rec", 765_565_858), - ("Lean.Widget.TaggedText.rec", 553_150_145), - ("Lean.Doc.Part.rec", 563_987_815), - ("Lean.Doc.Block.rec", 601_541_004), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 1_290_722), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 2_157_749), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 1_706_482), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 1_706_482), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 1_706_482), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 1_326_429), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 4_188_001), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 4_187_901), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 1_706_482), - ("strOfListFoldSize", 630_069_070), - ("strOfListFoldSizeAscii", 630_357_426), + ("HEq", 174_253_453), + ("HEq.rec", 179_369_968), + ("Eq.rec", 178_930_907), + ("Nat", 174_251_146), + ("Nat.add", 225_775_784), + ("Nat.add_comm", 407_548_669), + ("Nat.decEq", 468_535_350), + ("Nat.decLe", 996_808_469), + ("Nat.sub_le_of_le_add", 2_420_761_499), + ("Nat.shiftRight_succ", 1_804_091_690), + ("Trans.mk", 181_197_569), + ("Array.append_assoc", 10_738_511_002), + ("Vector.append", 11_035_924_603), + ("IxVMPrim.nat_add_lit", 288_623_864), + ("IxVMPrim.nat_sub_lit", 314_399_330), + ("IxVMPrim.nat_mul_lit", 276_684_084), + ("IxVMPrim.nat_mul_big", 274_058_123), + ("IxVMPrim.nat_div_lit", 1_763_986_073), + ("IxVMPrim.nat_mod_lit", 1_800_333_279), + ("IxVMPrim.nat_succ_lit", 198_297_622), + ("IxVMPrim.nat_pred_lit", 231_370_407), + ("IxVMPrim.nat_gcd_lit", 2_814_985_577), + ("IxVMPrim.nat_land_lit", 4_641_488_018), + ("IxVMPrim.nat_lor_lit", 4_645_134_614), + ("IxVMPrim.nat_xor_lit", 4_676_489_108), + ("IxVMPrim.nat_shl_lit", 319_654_333), + ("IxVMPrim.nat_shr_lit", 1_786_050_303), + ("IxVMPrim.nat_pow_big", 512_968_596), + ("IxVMPrim.nat_beq_lit", 272_411_595), + ("IxVMPrim.nat_ble_lit", 264_866_250), + ("IxVMPrim.nat_cases_big", 229_921_312), + ("IxVMPrim.nat_dec_le", 1_023_823_024), + ("IxVMPrim.nat_dec_lt", 1_040_897_495), + ("IxVMPrim.nat_dec_eq", 526_350_470), + ("IxVMPrim.str_size_lit", 3_268_640_491), + ("IxVMPrim.bv_to_nat_lit", 2_678_798_227), + ("IxVMInd.Even", 280_975_929), + ("IxVMInd.Odd", 280_978_002), + ("IxVMInd.Even.rec", 306_197_358), + ("IxVMInd.Odd.rec", 306_202_523), + ("IxVMInd.Tree", 176_446_075), + ("IxVMInd.Tree.rec", 190_363_971), + ("IxVMInd.DedupM", 182_347_784), + ("IxVMInd.DedupM.rec", 200_631_175), + ("IxVMInd.DepthM", 179_415_730), + ("IxVMInd.DepthM.rec", 194_647_830), + ("String.Internal.append", 3_227_514_931), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 4_778_782_780), + ("Lean.Syntax.rec", 3_308_305_946), + ("IxVMInd.AuxTie", 462_091_745), + ("IxVMInd.AuxTie.rec", 518_787_326), + ("String.Slice.Pattern.Model.NoPrefixForwardPatternModel.rec", 4_460_118_540), + ("Lean.Widget.TaggedText.rec", 3_257_809_387), + ("Lean.Doc.Part.rec", 3_317_631_822), + ("Lean.Doc.Block.rec", 3_526_952_467), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 179_103_548), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 183_862_937), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 181_494_202), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 181_494_202), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 181_494_202), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 179_304_623), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 195_052_162), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 195_051_307), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 181_494_202), + ("strOfListFoldSize", 3_681_557_577), + ("strOfListFoldSizeAscii", 3_683_080_324), ] /-- Variant of `kernelChecks`, pinned to the baseline diff --git a/Tests/Main.lean b/Tests/Main.lean index f89d12afa..98f273cc0 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -81,6 +81,7 @@ def primarySuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ ("aux-gen-unit", Tests.AuxGen.ExprUtils.suite ++ Tests.AuxGen.Levels.suite ++ Tests.AuxGen.Recursor.suite ++ Tests.AuxGen.Surgery.suite), ("ground-unit", Tests.Ground.suite), ("aiur-cross", [AiurTests.Cross.tests]), + ("aiur-cost", [AiurTests.Cost.tests]), ("prim-addrs", Tests.Ix.Kernel.PrimAddrs.suite), ("tc-unit", Tests.Tc.Unit.suite ++ Tests.Tc.Substrate.suite ++ Tests.Tc.Fixtures.suite ++ Tests.Tc.WhnfTests.suite @@ -219,10 +220,10 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [ -- (`.round.toUInt64.toNat`): any cost shift must be an -- explicit, reviewed bump. let actual := - (Aiur.computeStats v2Env.compiled qc).totalFftCost.round.toUInt64.toNat + (Aiur.computeStats v2Env.compiled qc v2Env.shapes).totalFftCost.round.toUInt64.toNat pure (LSpec.test - s!"Shard pipeline FFT matches: expected 1929255084, got {actual}" - (actual = 1_929_255_084)) + s!"Shard pipeline FFT matches: expected 10817625733, got {actual}" + (actual = 10_817_625_733)) LSpec.lspecIO (.ofList [("ixvm", [fullSeq, aiurSeq, arenaSeq, exploitSeq, paritySeq, shardSeq])]) []), diff --git a/crates/aiur/src/synthesis.rs b/crates/aiur/src/synthesis.rs index 9f886f3f2..cf5083b07 100644 --- a/crates/aiur/src/synthesis.rs +++ b/crates/aiur/src/synthesis.rs @@ -50,6 +50,19 @@ enum CircuitType { Bytes2, } +/// Shape of one compiled circuit, as needed by the Lean-side FFT cost model +/// (`Ix/Aiur/Statistics.lean`). Heights of function and memory circuits are +/// execution-dependent and are NOT part of the shape; `preprocessed_height` +/// doubles as the fixed trace height of the byte-gadget circuits (256 and +/// 65536), whose witness builders always emit the full table. +pub struct CircuitShape { + pub main_width: usize, + pub stage2_width: usize, + pub quotient_degree: usize, + pub preprocessed_width: usize, + pub preprocessed_height: usize, +} + impl AiurSystem { pub fn build( toplevel: Toplevel, @@ -139,6 +152,24 @@ impl AiurSystem { self.slot_widths[circuit_idx].clone() } + /// Per-circuit shape data for the FFT cost model, read straight off the + /// compiled [`System`] circuits (same order as [`Self::circuit_types`]: + /// constrained functions ascending, memories, `Bytes1`, `Bytes2`). + pub fn circuit_shapes(&self) -> Vec { + self + .system + .circuits + .iter() + .map(|circuit| CircuitShape { + main_width: circuit.main_width, + stage2_width: circuit.stage_2_width, + quotient_degree: circuit.quotient_degree(), + preprocessed_width: circuit.preprocessed_width, + preprocessed_height: circuit.preprocessed_height, + }) + .collect() + } + #[tracing::instrument(level = "info", skip_all, name = "aiur/prove")] pub fn prove( &self, @@ -492,4 +523,42 @@ mod tests { "verification must reject a tampered claim" ); } + + #[test] + fn circuit_shapes_match_system() { + let (cp, fp) = test_parameters(); + let system = AiurSystem::build(call_and_memory_toplevel(), cp, fp); + let shapes = system.circuit_shapes(); + + // Canonical order and count: 2 constrained functions, 1 memory, Bytes1, + // Bytes2. + assert_eq!(shapes.len(), 5); + assert_eq!(shapes.len(), system.system.circuits.len()); + + for (shape, circuit) in shapes.iter().zip(&system.system.circuits) { + assert_eq!(shape.main_width, circuit.main_width); + assert_eq!(shape.stage2_width, circuit.stage_2_width); + assert_eq!(shape.quotient_degree, circuit.quotient_degree()); + assert_eq!(shape.preprocessed_width, circuit.preprocessed_width); + assert_eq!(shape.preprocessed_height, circuit.preprocessed_height); + } + + // Function circuits: main width = inputs + selectors + auxiliaries, no + // preprocessed matrix. + assert_eq!(shapes[0].main_width, 2 + 1 + 5); + assert_eq!(shapes[1].main_width, 1 + 1 + 1); + // Memory of size 1: multiplicity + selector + pointer + 1 value. + assert_eq!(shapes[2].main_width, 3 + 1); + for shape in &shapes[..3] { + assert_eq!(shape.preprocessed_width, 0); + assert_eq!(shape.preprocessed_height, 0); + } + + // Byte gadgets: always-active fixed-height tables whose preprocessed + // height doubles as the committed trace height. + assert_eq!(shapes[3].preprocessed_width, 11); + assert_eq!(shapes[3].preprocessed_height, 256); + assert_eq!(shapes[4].preprocessed_width, 16); + assert_eq!(shapes[4].preprocessed_height, 65536); + } } diff --git a/crates/ffi/src/aiur/protocol.rs b/crates/ffi/src/aiur/protocol.rs index 8d2fcea1b..5e5417545 100644 --- a/crates/ffi/src/aiur/protocol.rs +++ b/crates/ffi/src/aiur/protocol.rs @@ -13,15 +13,15 @@ use lean_ffi::object::{ use crate::{ aiur::{lean_unbox_g, lean_unbox_nat_as_usize, toplevel::decode_toplevel}, lean::{ - LeanAiurCommitmentParameters, LeanAiurExecuteResult, LeanAiurFriParameters, - LeanAiurIOKeyInfo, LeanAiurProveEnvResult, LeanAiurProveResult, - LeanAiurQueryCount, LeanAiurToplevel, + LeanAiurCircuitShape, LeanAiurCommitmentParameters, LeanAiurExecuteResult, + LeanAiurFriParameters, LeanAiurIOKeyInfo, LeanAiurProveEnvResult, + LeanAiurProveResult, LeanAiurQueryCount, LeanAiurToplevel, }, }; use aiur::{ G, execute::{IOBuffer, IOKeyInfo, QueryRecord}, - synthesis::{AiurProof, AiurSystem}, + synthesis::{AiurProof, AiurSystem, CircuitShape}, }; // ============================================================================= @@ -87,6 +87,48 @@ extern "C" fn rs_aiur_system_build( LeanExternal::alloc(&AIUR_SYSTEM_CLASS, system) } +/// Helper: encode `CircuitShape`s as a Lean `Array CircuitShape`. Field +/// order must match `Aiur.CircuitShape` in `Ix/Aiur/Protocol.lean`. +fn build_circuit_shapes_array(shapes: &[CircuitShape]) -> LeanArray { + let arr = LeanArray::alloc(shapes.len()); + for (i, shape) in shapes.iter().enumerate() { + let s = LeanAiurCircuitShape::alloc(0); + s.set_obj(0, LeanOwned::box_usize(shape.main_width)); + s.set_obj(1, LeanOwned::box_usize(shape.stage2_width)); + s.set_obj(2, LeanOwned::box_usize(shape.quotient_degree)); + s.set_obj(3, LeanOwned::box_usize(shape.preprocessed_width)); + s.set_obj(4, LeanOwned::box_usize(shape.preprocessed_height)); + arr.set(i, s); + } + arr +} + +/// `AiurSystem.circuitShapes : @& AiurSystem → Array CircuitShape` +#[unsafe(no_mangle)] +extern "C" fn rs_aiur_system_circuit_shapes( + system: LeanExternal>, +) -> LeanArray { + build_circuit_shapes_array(&system.get().circuit_shapes()) +} + +/// `Aiur.circuitShapes : @&Bytecode.Toplevel → @&CommitmentParameters → @&FriParameters → Array CircuitShape` +/// +/// One-shot variant for flows that never build an `AiurSystem` (`ix check` +/// statistics): builds the system, extracts the shapes, and drops it. +#[unsafe(no_mangle)] +extern "C" fn rs_aiur_circuit_shapes( + toplevel: LeanAiurToplevel>, + commitment_parameters: LeanAiurCommitmentParameters>, + fri_parameters: LeanAiurFriParameters>, +) -> LeanArray { + let system = AiurSystem::build( + decode_toplevel(&toplevel), + decode_commitment_parameters(&commitment_parameters), + decode_fri_parameters(&fri_parameters), + ); + build_circuit_shapes_array(&system.circuit_shapes()) +} + /// `AiurSystem.verify : @& AiurSystem → @& Array G → @& Proof → Except String Unit` #[unsafe(no_mangle)] extern "C" fn rs_aiur_system_verify( diff --git a/crates/ffi/src/lean.rs b/crates/ffi/src/lean.rs index 8e958f790..83ecc71bf 100644 --- a/crates/ffi/src/lean.rs +++ b/crates/ffi/src/lean.rs @@ -277,6 +277,9 @@ lean_ffi::lean_inductive! { LeanAiurIOKeyInfo [ { num_obj: 2 } ]; // uniqueRows, totalHits LeanAiurQueryCount [ { num_obj: 2 } ]; + // mainWidth, stage2Width, quotientDegree, preprocessedWidth, + // preprocessedHeight + LeanAiurCircuitShape [ { num_obj: 5 } ]; // output, ioData, ioMap, queryCounts LeanAiurExecuteResult [ { num_obj: 4 } ]; // claim, proof, ioData, ioMap