aiur: retire the virtual-gas meter's API surface

Ix/Aiur/Protocol.lean

@@ -356,45 +356,21 @@ def detectedRamBudgetBytes : IO Nat := do
 
 namespace Bytecode.Toplevel
 
-/-- One shard's result from `shardCheckBatchWithEnv`. `weights` is the
-    shard's per-constant virtual-gas table, packed as 48-byte rows —
-    32-byte address, then `vspan` and `mult` as little-endian `UInt64`s
-    (see `ShardResult.foldWeights`). Empty unless the batch ran with
-    `profile := true`; the record it is read from is reduced to these
-    rows and dropped inside the shard's own task, so a whole partition's
-    weights fit in RAM when its records could not. -/
+/-- One shard's result from `shardCheckBatchWithEnv`. -/
 structure ShardResult where
   error : String
   peakBytes : Nat
-  weights : ByteArray
   /-- 1 when `peakBytes` fits the batch's `maxRamBytes` (or no budget
       was given); otherwise the part count the peak model projects will
       fit (`AiurSystem::suggested_split_parts`, measured on the record
       in-task). -/
   suggestedParts : Nat
   deriving Inhabited
 
-/-- Bytes per packed `weights` row: 32 address + 8 vspan + 8 mult. -/
-def shardWeightRow : Nat := 48
-
-/-- Fold `f` over the packed `(addrBytes, vspan, mult)` rows of `weights`.
-    Trailing bytes that do not complete a row are ignored. -/
-@[inline] def ShardResult.foldWeights {α : Type} (r : ShardResult) (init : α)
-    (f : α → ByteArray → UInt64 → UInt64 → α) : α :=
-  go (r.weights.size / shardWeightRow) 0 init
-where
-  go : Nat → Nat → α → α
-    | 0, _, acc => acc
-    | rows + 1, off, acc =>
-      go rows (off + shardWeightRow) <| f acc
-        (r.weights.extract off (off + 32))
-        (r.weights.extract (off + 32) (off + 40)).toUInt64LE!
-        (r.weights.extract (off + 40) (off + 48)).toUInt64LE!
-
 @[extern "rs_aiur_toplevel_shard_check_batch"]
 private opaque shardCheckBatchWithEnv' : @& Bytecode.Toplevel →
   @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool → @& Nat →
-  @& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
+  @& CommitmentParameters → @& FriParameters → @& Nat →
     Except String (Array ShardResult)
 
 /-- Check EVERY shard of a partition in one call: rayon over the shard
@@ -405,11 +381,7 @@ private opaque shardCheckBatchWithEnv' : @& Bytecode.Toplevel →
     Returns one `ShardResult` per shard in shard order: empty error =
     clean, and `peakBytes` is the analytic prover RAM peak
     ([`AiurSystem::peak_prove_bytes`] Rust-side) of the shard's executed
-    record — the split/merge input (0 on failure). `profile` turns on the
-    virtual-gas meter and fills each result's `weights` with the shard's
-    per-constant cost rows, read off the record inside the shard's own
-    task; `checkConstIdx` names the `check_const` function whose queries
-    those rows come from (ignored when not profiling).
+    record — the split/merge input (0 on failure).
     `jobs = 0` uses rayon's default pool width (all cores): peak RSS
     is bounded by the Rust-side RAM gate (a byte-weighted admission
     semaphore over estimated per-shard execution RSS vs available
@@ -426,11 +398,10 @@ def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
   (shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
   (commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
   (friParameters : FriParameters := defaultFriParameters)
-  (profile : Bool := false) (checkConstIdx : Nat := 0)
   (maxRamBytes : Nat := 0)
   : Except String (Array ShardResult) :=
   shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
-    jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes
+    jobs commitmentParameters friParameters maxRamBytes
 
 end Bytecode.Toplevel
 

Ix/Aiur/Semantics/BytecodeFfi.lean

@@ -75,61 +75,14 @@ structure QueryCount where
   totalHits : Nat
   deriving Inhabited
 
--- ===========================================================================
--- QueryRecordHandle: the execution's Rust-owned `QueryRecord` exposed to
--- Lean as an opaque handle inside every `ExecuteResult`. Lean inspects
--- queries with its higher-level knowledge (fn names via `nameMap`,
--- layouts, addr→name maps) through the accessors below; the record —
--- the dominant RAM consumer of an execution — frees when Lean drops it.
--- ===========================================================================
-
-private opaque QueryRecordHandleNonempty : NonemptyType
-def QueryRecordHandle : Type := QueryRecordHandleNonempty.type
-instance : Nonempty QueryRecordHandle := QueryRecordHandleNonempty.property
-
-namespace QueryRecordHandle
-
-/-- Number of query entries registered for function `funIdx`. -/
-@[extern "rs_aiur_qr_fn_len"]
-opaque fnLen : @& QueryRecordHandle → (funIdx : @& Nat) → Nat
-
-/-- Input tuple of entry `i` of function `funIdx` (empty when out of
-    range). Entries are in insertion order; iterate within `fnLen`. -/
-@[extern "rs_aiur_qr_fn_key"]
-opaque fnKey : @& QueryRecordHandle → (funIdx i : @& Nat) → Array G
-
-/-- Multiplicity of entry `i` of function `funIdx`. `0` marks an
-    unconstrained hint row (or an out-of-range index). -/
-@[extern "rs_aiur_qr_fn_mult"]
-opaque fnMult : @& QueryRecordHandle → (funIdx i : @& Nat) → Nat
-
-/-- Recorded virtual-gas span of entry `i` of function `funIdx` — the
-    entry's standalone cost, with memo hits replaying the callee's
-    recorded span. `0` unless the execution ran with `profile := true`
-    (the `Full` execution wrappers' trailing flag). -/
-@[extern "rs_aiur_qr_fn_vspan"]
-opaque fnVspan : @& QueryRecordHandle → (funIdx i : @& Nat) → Nat
-
-/-- Stored values of entry `ptr` in the `memory[size]` map — the deref
-    of an Aiur `&[T; size]` pointer (empty when unbound). E.g. an
-    `Addr = &[U8; 32]` argument derefs to its 32 blake3 bytes via
-    `memKey 32 ptr`. -/
-@[extern "rs_aiur_qr_mem_key"]
-opaque memKey : @& QueryRecordHandle → (size ptr : @& Nat) → Array G
-
-end QueryRecordHandle
-
 /-- Result of an execution FFI call, built directly by Rust
 (`LeanAiurExecuteResult` in `crates/ffi/src/lean.rs`). `ioData`/`ioMap`
-are the flattened `IOBuffer`; see `IOBuffer.ofArrays`. `record` owns the
-execution's `QueryRecord` — drop the `ExecuteResult` (or project the
-other fields out) before the next heavy execution to release its RAM. -/
+are the flattened `IOBuffer`; see `IOBuffer.ofArrays`. -/
 structure ExecuteResult where
   output : Array G
   ioData : Array (G × Array G)
   ioMap : Array ((G × Array G) × IOKeyInfo)
   queryCounts : Array QueryCount
-  record : QueryRecordHandle
 
 -- ===========================================================================
 -- EnvHandle: Rust-owned `ixon::Env` exposed to Lean as an opaque handle.
@@ -169,7 +122,6 @@ private opaque execute' : @& Bytecode.Toplevel →
   @& Bytecode.FunIdx → @& Array G →
   (ioData : @& Array (G × Array G)) →
   (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
-  (profile : Bool) →
     Except String ExecuteResult
 
 /-- Executes the bytecode function `funIdx` with the given `args` and `ioBuffer`,
@@ -180,24 +132,14 @@ callers can recover instead of crashing. -/
 def execute (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
     Except String (Array G × IOBuffer × Array QueryCount) :=
-  (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).map
+  (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray).map
     fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)
 
-/-- `execute` variant returning the full `ExecuteResult`, including the
-    `QueryRecordHandle` for post-run query inspection. `profile` enables
-    per-entry virtual-span recording (`QueryRecordHandle.fnVspan`). -/
-def executeFull (toplevel : @& Bytecode.Toplevel)
-  (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer)
-  (profile : Bool := false) :
-    Except String ExecuteResult :=
-  execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray profile
-
 @[extern "rs_aiur_toplevel_execute_ixvm"]
 private opaque executeIxVM' : @& Bytecode.Toplevel →
   @& Bytecode.FunIdx → @& Array G →
   (ioData : @& Array (G × Array G)) →
   (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
-  (profile : Bool) →
     Except String ExecuteResult
 
 /-- IxVM-native execution: same shape as `execute`, but routes the
@@ -211,19 +153,9 @@ private opaque executeIxVM' : @& Bytecode.Toplevel →
 def executeIxVM (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
     Except String (Array G × IOBuffer × Array QueryCount) :=
-  (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).map
+  (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray).map
     fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)
 
-/-- `executeIxVM` variant returning the full `ExecuteResult`, including
-    the `QueryRecordHandle` for post-run query inspection. `profile`
-    enables per-entry virtual-span recording
-    (`QueryRecordHandle.fnVspan`). -/
-def executeIxVMFull (toplevel : @& Bytecode.Toplevel)
-  (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer)
-  (profile : Bool := false) :
-    Except String ExecuteResult :=
-  executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray profile
-
 /-- MultiStark-native execution of `verify_multi_stark_proof`: the IO
     advice buffer (channel 0 = proof, 1 = vk, 2 = claims, key `[0]`
     each) is built natively in Rust from the raw byte blobs — no
@@ -288,8 +220,7 @@ opaque executeIxAggr (toplevel : @& Bytecode.Toplevel)
 
 @[extern "rs_aiur_toplevel_check_addr_with_env"]
 private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
-  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
-  (useBytecode profile : Bool) →
+  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
     Except String ExecuteResult
 
 /-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
@@ -301,7 +232,7 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
   (addrBytes : ByteArray) (useBytecode : Bool := false)
   : Except String (Array G × IOBuffer × Array QueryCount) :=
-  (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
+  (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode).map
     fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)
 
 @[extern "rs_aiur_toplevel_check_addrs_with_env"]
@@ -325,21 +256,9 @@ def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
   : Except String (Array (String × String)) :=
   checkAddrsWithEnv' toplevel funIdx envHandle addrsBlob useBytecode jobs
 
-/-- `checkAddrWithEnv` variant returning the full `ExecuteResult`,
-    including the `QueryRecordHandle` for post-run query inspection.
-    `profile` enables per-entry virtual-span recording
-    (`QueryRecordHandle.fnVspan`). -/
-def checkAddrWithEnvFull (toplevel : @& Bytecode.Toplevel)
-  (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
-  (addrBytes : ByteArray) (useBytecode : Bool := false)
-  (profile : Bool := false)
-  : Except String ExecuteResult :=
-  checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode profile
-
 @[extern "rs_aiur_toplevel_shard_check_with_env"]
 private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
-  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
-  (useBytecode profile : Bool) →
+  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
     Except String ExecuteResult
 
 /-- Per-shard check with the witness shape (wrapper-augmented byte
@@ -349,20 +268,9 @@ def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
   (ownedBlob : ByteArray) (useBytecode : Bool := false)
   : Except String (Array G × IOBuffer × Array QueryCount) :=
-  (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).map
+  (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
     fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)
 
-/-- `shardCheckWithEnv` variant returning the full `ExecuteResult`,
-    including the `QueryRecordHandle` for post-run query inspection.
-    `profile` enables per-entry virtual-span recording
-    (`QueryRecordHandle.fnVspan`). -/
-def shardCheckWithEnvFull (toplevel : @& Bytecode.Toplevel)
-  (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
-  (ownedBlob : ByteArray) (useBytecode : Bool := false)
-  (profile : Bool := false)
-  : Except String ExecuteResult :=
-  shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode profile
-
 end Bytecode.Toplevel
 
 end Aiur

Ix/Aiur/Stages/Codegen.lean

@@ -384,13 +384,11 @@ private def emitCall (out : Nat) (callee : FunIdx) (args : Array ValIdx)
   -- always skipped; when opUn = false both expressions collapse to
   -- just `unconstrained`.
   let cuExpr : String := if opUn then "true" else "unconstrained"
-  -- On a constrained hit, `replay_at` bumps the multiplicity and returns
-  -- the entry's virtual-gas replay cost (its recorded standalone span
-  -- when profiling, else the map weight) to add to `record.virt`.
+  -- On a constrained hit, bump the entry's multiplicity.
   let bumpStmt : String :=
     if opUn then ""
     else
-      s!" if !unconstrained \{ let __r = record.function_queries[{callee}].replay_at(__i); record.virt += __r; }"
+      s!" if !unconstrained \{ record.function_queries[{callee}].bump_multiplicity(__i); }"
   -- Skip `try_into().unwrap()` on the cache hit: we statically know
   -- the cached output has exactly `OUT_{callee}` elements (only we
   -- ever insert into this slot via the matching aiur_fn_{callee}
@@ -428,12 +426,12 @@ private def emitStore (out : Nat) (values : Array ValIdx) : Array RustStmt :=
     s!"\{ let __values: [G; {size}] = {valsStr};" ++
     s!" let __mq = record.memory_queries.get_mut(&{size}).ok_or(ExecError::InvalidMemorySize({size}))?;" ++
     s!" if let Some(__i) = __mq.get_index_of(&__values[..]) \{" ++
-    s!" if !unconstrained \{ let __r = __mq.replay_at(__i); record.virt += __r; }" ++
+    s!" if !unconstrained \{ __mq.bump_multiplicity(__i); }" ++
     s!" __mq.output_at(__i)[0]" ++
     s!" } else \{" ++
     s!" let __ptr = G::from_usize(__mq.len());" ++
     s!" __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained));" ++
-    s!" if !unconstrained \{ record.virt += __mq.weight(); } __ptr } }"
+    s!" __ptr } }"
   #[.letStmt false s!"__v_{out}" (some "G") (.lit blockExpr)]
 
 /-- `Op::Load`: mirror execute.rs lines 328-345. Look up by pointer
@@ -444,7 +442,7 @@ private def emitLoad (out : Nat) (size : Nat) (ptr : ValIdx) : Array RustStmt :=
     s!" let __ptr_u64 = __v_{ptr}.as_canonical_u64();" ++
     s!" let __ptr_usize = usize::try_from(__ptr_u64).ok().ok_or(ExecError::PointerTooLarge(__ptr_u64))?;" ++
     s!" if __ptr_usize >= __mq.len() \{ return Err(ExecError::UnboundPointer \{ ptr: __ptr_u64, size: {size} }); }" ++
-    s!" if !unconstrained \{ let __r = __mq.replay_at(__ptr_usize); record.virt += __r; }" ++
+    s!" if !unconstrained \{ __mq.bump_multiplicity(__ptr_usize); }" ++
     s!" let (__args, _) = __mq.get_index(__ptr_usize).expect(\"bounds checked above\");" ++
     s!" let __arr: [G; {size}] = __args[..{size}].try_into().unwrap(); __arr }"
   let mut stmts : Array RustStmt := #[
@@ -829,12 +827,8 @@ partial def emitCtrl (funIdx : FunIdx) (mcLabel? : Option String)
     let outArr : RustStmt :=
       .letStmt false "__ret" (some s!"[G; OUT_{funIdx}]")
         (.arrayLit (outs.map valVar))
-    -- `finish` inserts / promotes the row, and (when profiling)
-    -- records the frame's virtual span measured against the `__vsnap`
-    -- taken at fn entry. Own-row touch priced before the span is read.
     let insertCall : RustStmt := .exprStmt (.lit <|
-      s!"if !unconstrained \{ record.virt += record.function_queries[{funIdx}].weight(); }" ++
-      s!" record.function_queries[{funIdx}].finish(&inp[..], &__ret[..], !unconstrained, record.virt - __vsnap)")
+      s!"record.function_queries[{funIdx}].finish(&inp[..], &__ret[..], !unconstrained)")
     -- Wrap in Ok(...) since fn now returns Result<[G; OUT_N], ExecError>.
     return #[outArr, insertCall,
       .returnStmt (.call (.var "Ok") #[.var "__ret"])]
@@ -949,9 +943,6 @@ def emitFunction (funIdx : FunIdx) (f : Function) : Array RustItem := Id.run do
     s!"  unconstrained: bool,\n" ++
     s!") -> Result<[G; OUT_{funIdx}], ExecError> {lbrace}\n" ++
     s!"  stacker::maybe_grow(64 * 1024, 4 * 1024 * 1024, || {lbrace}\n" ++
-    -- Virtual-gas snapshot at frame entry; `Ctrl::Return` records the
-    -- frame's span (`record.virt - __vsnap`) on the registered query.
-    s!"  let __vsnap = record.virt;\n" ++
     bodyText ++
     s!"  {rbrace})\n" ++
     s!"{rbrace}\n\n"