Use named structures for QueryCounts

Replace the anonymous `Nat × Nat × Nat × Nat` quads / `Nat × Nat` pairs
shipped from the executor with `GroupStats { groupIdx, totalWidth,
uniqueRows, totalHits }` and `MemoryCount { uniqueRows, totalHits }`,
bundled into a `QueryCounts { functionStats, memoryCounts }` struct.

The FFI extern keeps the tuple shape (so the Rust side can build it
without matching a Lean structure ctor); `Bytecode.Toplevel.execute`
converts to the structured form at the public API boundary. Callers
(`Kernel.lean`, `Statistics.computeStats`) lose the `.1`/`.2.2.1`
indexing and use named field access.

Author: arthurpaulino

Ix/Aiur/Semantics/BytecodeFfi.lean

@@ -50,52 +50,69 @@ instance : BEq IOBuffer where
 -- via `Std.HashMap.beq_iff_equiv` + `Std.HashMap.Equiv.{refl,symm,trans}`,
 -- bypassing the need for `LawfulBEq` on the outer `IOBuffer`.
 
-/-- Per-circuit query counts for one circuit (one per function circuit, then
-one per memory size). `uniqueRows` is the trace height; `totalHits` is the sum
-of query multiplicities. The difference `totalHits - uniqueRows` is the number
-of cache hits. -/
-structure QueryCount where
+namespace Bytecode.Toplevel
+
+/-- Per-split execution stats for one return-group of one function.
+`groupIdx` keys the corresponding entry in `Function.groupNames`. -/
+structure GroupStats where
+  groupIdx : Nat
+  totalWidth : Nat
   uniqueRows : Nat
   totalHits : Nat
-  deriving Inhabited
+  deriving Inhabited, Repr
 
-namespace Bytecode.Toplevel
+/-- Per-memory-size counts. `uniqueRows` is the trace height; `totalHits`
+is the sum of multiplicities. `totalHits - uniqueRows` is the cache-hit
+count. -/
+structure MemoryCount where
+  uniqueRows : Nat
+  totalHits : Nat
+  deriving Inhabited, Repr
 
-/-- Per-function execution stats. One entry per split (return group), keyed
-by group index. Each quadruple is
-`(groupIdx, totalWidth, uniqueRows, totalHits)`. The display name is looked
-up via `Function.groupNames[groupIdx]`. -/
-abbrev FunctionStats := Array (Array (Nat × Nat × Nat × Nat))
+/-- Per-function execution stats. Outer index is `FunIdx`; inner index is
+the `USize` group index used by `Ctrl.return`. -/
+abbrev FunctionStats := Array (Array GroupStats)
 
-/-- Per-memory-size `(uniqueRows, totalHits)` pairs. -/
-abbrev MemoryCounts := Array (Nat × Nat)
+/-- Per-memory-size counts, parallel to `Toplevel.memorySizes`. -/
+abbrev MemoryCounts := Array MemoryCount
 
-/-- Query counts shipped back from the Rust executor: per-function split stats
-plus per-memory pairs. -/
-abbrev QueryCounts := FunctionStats × MemoryCounts
+/-- Query counts shipped back from the Rust executor. -/
+structure QueryCounts where
+  functionStats : FunctionStats
+  memoryCounts : MemoryCounts
+  deriving Inhabited
 
+/-- Raw FFI tuple shape — kept tuple-flat so the Rust side can build it
+without declaring matching Lean structure ctors. `execute` wraps the
+result in the structured `QueryCounts` immediately. -/
 @[extern "rs_aiur_toplevel_execute"]
 private opaque execute' : @& Bytecode.Toplevel →
   @& Bytecode.FunIdx → @& Array G → (ioData : @& Array G) →
   (ioMap : @& Array (Array G × IOKeyInfo)) →
-    Except String (Array G × (Array G × Array (Array G × IOKeyInfo)) × QueryCounts)
+    Except String (Array G × (Array G × Array (Array G × IOKeyInfo))
+      × (Array (Array (Nat × Nat × Nat × Nat)) × Array (Nat × Nat)))
 
 /-- Executes the bytecode function `funIdx` with the given `args` and `ioBuffer`,
 returning the raw output of the function, the updated `IOBuffer`, and a
-`QueryCounts` (per-function split stats + per-memory `(uniqueRows, totalHits)`
-pairs). Returns `Except.error msg` when execution fails (e.g. `assert_eq!`
-mismatch from a typechecker rejecting a constant), so callers can recover
-instead of crashing. -/
+`QueryCounts`. Returns `Except.error msg` when execution fails (e.g.
+`assert_eq!` mismatch from a typechecker rejecting a constant), so callers
+can recover instead of crashing. -/
 def execute (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
     Except String (Array G × IOBuffer × QueryCounts) :=
   let ioData := ioBuffer.data
   let ioMap := ioBuffer.map
   match execute' toplevel funIdx args ioData ioMap.toArray with
   | .error e => .error e
-  | .ok (output, (ioData, ioMap), queryCounts) =>
+  | .ok (output, (ioData, ioMap), rawFn, rawMem) =>
     let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
-    .ok (output, ⟨ioData, ioMap⟩, queryCounts)
+    let functionStats : FunctionStats := rawFn.map fun perFn =>
+      perFn.map fun quad =>
+        { groupIdx := quad.1, totalWidth := quad.2.1,
+          uniqueRows := quad.2.2.1, totalHits := quad.2.2.2 }
+    let memoryCounts : MemoryCounts := rawMem.map fun pair =>
+      { uniqueRows := pair.1, totalHits := pair.2 }
+    .ok (output, ⟨ioData, ioMap⟩, { functionStats, memoryCounts })
 
 end Bytecode.Toplevel
 

Ix/Aiur/Statistics.lean

@@ -39,9 +39,8 @@ def fftCost (w h : Nat) : Float :=
     let hf := h.toFloat
     wf * hf * (max hf 2.0).log2
 
-def computeStats (compiled : CompiledToplevel)
-    (functionStats : Array (Array (Nat × Nat × Nat × Nat)))
-    (memoryCounts : Array (Nat × Nat)) : ExecutionStats :=
+def computeStats (compiled : CompiledToplevel) (qc : Bytecode.Toplevel.QueryCounts) :
+    ExecutionStats :=
   let t := compiled.bytecode
   -- Invert nameMap to get FunIdx → String
   let reverseMap := compiled.nameMap.fold (init := (∅ : Std.HashMap Bytecode.FunIdx String))
@@ -53,24 +52,20 @@ def computeStats (compiled : CompiledToplevel)
       if t.functions[i]!.constrained then
         let baseName := reverseMap[i]?.getD s!"<fn {i}>"
         let groupNames := t.functions[i]!.groupNames
-        for quad in functionStats[i]! do
-          let groupIdx := quad.1
-          let w := quad.2.1
-          let h := quad.2.2.1
-          let totalHits := quad.2.2.2
-          let hits := totalHits - h
-          let group := groupNames[groupIdx]?.getD ""
+        for gs in qc.functionStats[i]! do
+          let group := groupNames[gs.groupIdx]?.getD ""
           let name := if group.isEmpty then baseName else s!"{baseName} [{group}]"
-          acc := acc.push { name, width := w, height := h, cacheHits := hits, fftCost := fftCost w h : CircuitStats }
+          let hits := gs.totalHits - gs.uniqueRows
+          acc := acc.push
+            { name, width := gs.totalWidth, height := gs.uniqueRows,
+              cacheHits := hits, fftCost := fftCost gs.totalWidth gs.uniqueRows : CircuitStats }
     acc
   let memoryCircuits := t.memorySizes.mapIdx fun i size =>
     let w := size + 11
-    let pair := memoryCounts[i]!
-    let h := pair.1
-    let totalHits := pair.2
-    let hits := totalHits - h
-    { name := s!"memory[{size}]",
-      width := w, height := h, cacheHits := hits, fftCost := fftCost w h : CircuitStats }
+    let mc := qc.memoryCounts[i]!
+    let hits := mc.totalHits - mc.uniqueRows
+    { name := s!"memory[{size}]", width := w, height := mc.uniqueRows,
+      cacheHits := hits, fftCost := fftCost w mc.uniqueRows : CircuitStats }
   let circuits := (functionCircuits ++ memoryCircuits).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

Kernel.lean

@@ -59,7 +59,7 @@ where
       if ioBuffer != testCase.expectedIOBuffer then
         IO.eprintln s!"{name}: IOBuffer mismatch"
         return 1
-      let stats := Aiur.computeStats compiled queryCounts.1 queryCounts.2
+      let stats := Aiur.computeStats compiled queryCounts
       Aiur.printStats stats
       pure 0
   interpCheck decls name env : IO UInt32 := do