aiur: ground the FFT cost model in the prover's actual transforms

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

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}"

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

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) :=

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!"<fn {i}>"
-        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
 

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

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)

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. -/