perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
samuelburnham wants to merge 7 commits into
base:main
Choose a base branch
from
Draft

perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
66fb376
aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro…
arthurpaulino Aug 24, 2026
1639996
aiur: batch weights; budget-gated proves that split in place
samuelburnham Aug 28, 2026
f529e09
aiur: model-driven splitting, exec-only audits, corrected-manifest emit
samuelburnham Aug 27, 2026
7de7a7b
aiur: quality pass, --ram-budget semantics, settled seed sizing
samuelburnham Aug 28, 2026
20f5e62
bench: aiur-sharded-env exercises the split audit
samuelburnham Aug 28, 2026
f43447c
aiur: scale static shard seeds by block profile
samuelburnham Aug 28, 2026
319df80
fmt, clippy
samuelburnham Aug 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
133 changes: 116 additions & 17 deletions Ix/Aiur/Protocol.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -173,54 +173,153 @@ def proveAddrWithEnv (system : @& AiurSystem)
(proveAddrWithEnv' system funIdx envHandle addrBytes useBytecode).map
fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

/-- Result of a per-shard prove: the claim's wire bytes, the proof, the
projected prover RAM peak of the record that produced it
(`AiurSystem::peak_prove_bytes`), and the part count the peak model
projects will fit the budget
(`AiurSystem::suggested_split_parts`).

`proof` is `none` exactly when the peak exceeded the budget — a
RESULT rather than an error, since the caller's answer is to cut
the shard into `suggestedParts` parts and prove those. The count is
computed Rust-side because only there does the executed record
still exist to read per-circuit heights from; it is optimistic
(parts re-execute dependencies shared across the cut), so each part
must still be gated on its own record. `suggestedParts` is 1
whenever the prove ran. The claim bytes are filled either way (the
claim is known before proving starts).

The final IO buffer is not returned — it is the shard's whole
ingested byte scope and no caller reads it. -/
structure ShardProveResult where
claimBytes : ByteArray
proof : Option Proof
peakBytes : Nat
suggestedParts : Nat

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem →
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
Except String ProveEnvResult

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& Nat → Bool →
Except String ShardProveResult

/-- Per-shard prove against a Rust-owned `EnvHandle`: ONE execution,
whose record is proven from directly.

`maxRamBytes` is a per-shard prover-RAM budget checked against that
record's projected peak before the witness phase begins; `0` means
detect (85% of `MemAvailable`, the policy the check batch's RAM gate
uses), and an unreadable `/proc/meminfo` disables the check rather
than guessing. Over budget, the record is dropped and `proof` is
`none` — learning that here costs one execution instead of an OOM
part-way through an FFT. The peak comes back either way, so a prove
run yields the same split/merge signal a check run does.

`execOnly` stops after execution + measurement (`proof` is `none`
either way; `suggestedParts` is 1 exactly when the peak fits): the
split loop runs on executions alone, never starting a STARK. -/
def shardProveWithEnv (system : @& AiurSystem)
(funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
Except String (ByteArray × Proof × IOBuffer) :=
(shardProveWithEnv' system funIdx envHandle ownedBlob).map
fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
(funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
(ownedBlob : ByteArray) (maxRamBytes : Nat := 0)
(execOnly : Bool := false) :
Except String ShardProveResult :=
shardProveWithEnv' system funIdx envHandle ownedBlob maxRamBytes execOnly

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem →
@& Array G → @& Proof → Except String Unit

end AiurSystem

/-- Write a `.ixes` manifest for an EXPLICIT partition — the block lists
a run actually produced (splits included) rather than a planner's
output. `shardsBlob`: per shard, a 4-byte LE block count followed by
that many 32-byte block addresses; every env block must appear in
exactly one shard. `peaksBlob`: one 8-byte LE measured prover peak
per shard in order, recorded on the manifest for schedulers. Own
sizes, foreign blocks, cross-ingress and assumption roots are
recomputed from the env's static profile; prints the manifest
summary to stderr. -/
@[extern "rs_shard_manifest_from_partition"]
opaque shardManifestFromPartition : @& EnvHandle →
@& ByteArray → @& ByteArray → @& String → IO Unit

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. -/
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 →
Except String (Array (String × Nat))
@& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
Except String (Array ShardResult)

/-- Check EVERY shard of a partition in one call: rayon over the shard
list with true work-stealing (no chunk barriers), each shard
through the exact single-shard machinery over its own private
record and witness io. `shardsBlob` encodes, per shard, a 4-byte LE
owned-constant count followed by that many 32-byte addresses.
Returns one `(error, peakBytes)` pair 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).
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).
`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
system RAM), not by thread count — pass `jobs` only to narrow
CPU use. -/
CPU use.

`maxRamBytes > 0` is a per-shard prover-RAM budget: each result's
`suggestedParts` is 1 when its peak fits and the model's projected
part count otherwise, so a caller can cut over-budget shards and
re-batch the parts — the wave loop that audits a partition's split
behavior on executions alone. -/
def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
(funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
(shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
(commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
(friParameters : FriParameters := defaultFriParameters)
: Except String (Array (String × Nat)) :=
(profile : Bool := false) (checkConstIdx : Nat := 0)
(maxRamBytes : Nat := 0)
: Except String (Array ShardResult) :=
shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
jobs commitmentParameters friParameters
jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes

end Bytecode.Toplevel

Expand Down
109 changes: 101 additions & 8 deletions Ix/Aiur/Semantics/BytecodeFfi.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -75,14 +75,61 @@ 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`. -/
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. -/
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.
Expand DownExpand Up@@ -122,6 +169,7 @@ 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`,
Expand All@@ -132,14 +180,24 @@ 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).map
(execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -153,9 +211,19 @@ 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).map
(executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -181,7 +249,8 @@ opaque executeMultiStark (toplevel : @& Bytecode.Toplevel)

@[extern "rs_aiur_toplevel_check_addr_with_env"]
private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
(useBytecode profile : Bool) →
Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -193,7 +262,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).map
(checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

@[extern "rs_aiur_toplevel_check_addrs_with_env"]
Expand All@@ -207,7 +276,8 @@ private opaque checkAddrsWithEnv' : @& Bytecode.Toplevel →
through the exact single-claim machinery over task-private data
(own witness io, own query record), nothing shared between tasks
but the read-only toplevel and env. Returns the FAILURES as
`(addrHex, error)` pairs; empty means all passed. Per-claim
`(batch index as a decimal string, error)` pairs, resolving back to
the caller's label order; empty means all passed. Per-claim
outputs/records are not returned — use `checkAddrWithEnv` for a
single claim's full result. -/
def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
Expand All@@ -216,9 +286,21 @@ 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 → Bool →
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
(useBytecode profile : Bool) →
Except String ExecuteResult

/-- Per-shard check with the witness shape (wrapper-augmented byte
Expand All@@ -228,9 +310,20 @@ 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).map
(shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).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
Expand Down
Loading
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
7
commits into

base:main
Choose a base branch

from

 Draft


perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


7 commits


Select commit
Hold shift + click to select a range
66fb376

aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro…


arthurpaulino Aug 24, 2026
1639996

aiur: batch weights; budget-gated proves that split in place


samuelburnham Aug 28, 2026
f529e09

aiur: model-driven splitting, exec-only audits, corrected-manifest emit


samuelburnham Aug 27, 2026
7de7a7b

aiur: quality pass, --ram-budget semantics, settled seed sizing


samuelburnham Aug 28, 2026
20f5e62

bench: aiur-sharded-env exercises the split audit


samuelburnham Aug 28, 2026
f43447c

aiur: scale static shard seeds by block profile


samuelburnham Aug 28, 2026
319df80

fmt, clippy


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


133 changes: 116 additions & 17 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -173,54 +173,153 @@ def proveAddrWithEnv (system : @& AiurSystem)
 (proveAddrWithEnv' system funIdx envHandle addrBytes useBytecode).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

/-- Result of a per-shard prove: the claim's wire bytes, the proof, the
 projected prover RAM peak of the record that produced it
 (`AiurSystem::peak_prove_bytes`), and the part count the peak model
 projects will fit the budget
 (`AiurSystem::suggested_split_parts`).

 `proof` is `none` exactly when the peak exceeded the budget — a
 RESULT rather than an error, since the caller's answer is to cut
 the shard into `suggestedParts` parts and prove those. The count is
 computed Rust-side because only there does the executed record
 still exist to read per-circuit heights from; it is optimistic
 (parts re-execute dependencies shared across the cut), so each part
 must still be gated on its own record. `suggestedParts` is 1
 whenever the prove ran. The claim bytes are filled either way (the
 claim is known before proving starts).

 The final IO buffer is not returned — it is the shard's whole
 ingested byte scope and no caller reads it. -/
structure ShardProveResult where
 claimBytes : ByteArray
 proof : Option Proof
 peakBytes : Nat
 suggestedParts : Nat

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String ProveEnvResult

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& Nat → Bool →
 Except String ShardProveResult

/-- Per-shard prove against a Rust-owned `EnvHandle`: ONE execution,
 whose record is proven from directly.

 `maxRamBytes` is a per-shard prover-RAM budget checked against that
 record's projected peak before the witness phase begins; `0` means
 detect (85% of `MemAvailable`, the policy the check batch's RAM gate
 uses), and an unreadable `/proc/meminfo` disables the check rather
 than guessing. Over budget, the record is dropped and `proof` is
 `none` — learning that here costs one execution instead of an OOM
 part-way through an FFT. The peak comes back either way, so a prove
 run yields the same split/merge signal a check run does.

 `execOnly` stops after execution + measurement (`proof` is `none`
 either way; `suggestedParts` is 1 exactly when the peak fits): the
 split loop runs on executions alone, never starting a STARK. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (maxRamBytes : Nat := 0)
 (execOnly : Bool := false) :
 Except String ShardProveResult :=
 shardProveWithEnv' system funIdx envHandle ownedBlob maxRamBytes execOnly

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem →
 @& Array G → @& Proof → Except String Unit

end AiurSystem

/-- Write a `.ixes` manifest for an EXPLICIT partition — the block lists
 a run actually produced (splits included) rather than a planner's
 output. `shardsBlob`: per shard, a 4-byte LE block count followed by
 that many 32-byte block addresses; every env block must appear in
 exactly one shard. `peaksBlob`: one 8-byte LE measured prover peak
 per shard in order, recorded on the manifest for schedulers. Own
 sizes, foreign blocks, cross-ingress and assumption roots are
 recomputed from the env's static profile; prints the manifest
 summary to stderr. -/
@[extern "rs_shard_manifest_from_partition"]
opaque shardManifestFromPartition : @& EnvHandle →
 @& ByteArray → @& ByteArray → @& String → IO Unit

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. -/
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 →
 Except String (Array (String × Nat))
 @& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
 Except String (Array ShardResult)

/-- Check EVERY shard of a partition in one call: rayon over the shard
 list with true work-stealing (no chunk barriers), each shard
 through the exact single-shard machinery over its own private
 record and witness io. `shardsBlob` encodes, per shard, a 4-byte LE
 owned-constant count followed by that many 32-byte addresses.
 Returns one `(error, peakBytes)` pair 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).
 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).
 `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
 system RAM), not by thread count — pass `jobs` only to narrow
 CPU use. -/
 CPU use.

 `maxRamBytes > 0` is a per-shard prover-RAM budget: each result's
 `suggestedParts` is 1 when its peak fits and the model's projected
 part count otherwise, so a caller can cut over-budget shards and
 re-batch the parts — the wave loop that audits a partition's split
 behavior on executions alone. -/
def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
 (commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
 (friParameters : FriParameters := defaultFriParameters)
 : Except String (Array (String × Nat)) :=
 (profile : Bool := false) (checkConstIdx : Nat := 0)
 (maxRamBytes : Nat := 0)
 : Except String (Array ShardResult) :=
 shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
 jobs commitmentParameters friParameters
 jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes

end Bytecode.Toplevel

Expand Down

109 changes: 101 additions & 8 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -75,14 +75,61 @@ 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`. -/
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. -/
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.
Expand DownExpand Up@@ -122,6 +169,7 @@ 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`,
Expand All@@ -132,14 +180,24 @@ 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).map
 (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -153,9 +211,19 @@ 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).map
 (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -181,7 +249,8 @@ opaque executeMultiStark (toplevel : @& Bytecode.Toplevel)

@[extern "rs_aiur_toplevel_check_addr_with_env"]
private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -193,7 +262,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).map
 (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

@[extern "rs_aiur_toplevel_check_addrs_with_env"]
Expand All@@ -207,7 +276,8 @@ private opaque checkAddrsWithEnv' : @& Bytecode.Toplevel →
 through the exact single-claim machinery over task-private data
 (own witness io, own query record), nothing shared between tasks
 but the read-only toplevel and env. Returns the FAILURES as
 `(addrHex, error)` pairs; empty means all passed. Per-claim
 `(batch index as a decimal string, error)` pairs, resolving back to
 the caller's label order; empty means all passed. Per-claim
 outputs/records are not returned — use `checkAddrWithEnv` for a
 single claim's full result. -/
def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
Expand All@@ -216,9 +286,21 @@ 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 → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-shard check with the witness shape (wrapper-augmented byte
Expand All@@ -228,9 +310,20 @@ 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).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).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
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
7
commits into

base:main
Choose a base branch

from

 Draft


perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


7 commits


Select commit
Hold shift + click to select a range
66fb376

aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro…


arthurpaulino Aug 24, 2026
1639996

aiur: batch weights; budget-gated proves that split in place


samuelburnham Aug 28, 2026
f529e09

aiur: model-driven splitting, exec-only audits, corrected-manifest emit


samuelburnham Aug 27, 2026
7de7a7b

aiur: quality pass, --ram-budget semantics, settled seed sizing


samuelburnham Aug 28, 2026
20f5e62

bench: aiur-sharded-env exercises the split audit


samuelburnham Aug 28, 2026
f43447c

aiur: scale static shard seeds by block profile


samuelburnham Aug 28, 2026
319df80

fmt, clippy


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


133 changes: 116 additions & 17 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -173,54 +173,153 @@ def proveAddrWithEnv (system : @& AiurSystem)
 (proveAddrWithEnv' system funIdx envHandle addrBytes useBytecode).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

/-- Result of a per-shard prove: the claim's wire bytes, the proof, the
 projected prover RAM peak of the record that produced it
 (`AiurSystem::peak_prove_bytes`), and the part count the peak model
 projects will fit the budget
 (`AiurSystem::suggested_split_parts`).

 `proof` is `none` exactly when the peak exceeded the budget — a
 RESULT rather than an error, since the caller's answer is to cut
 the shard into `suggestedParts` parts and prove those. The count is
 computed Rust-side because only there does the executed record
 still exist to read per-circuit heights from; it is optimistic
 (parts re-execute dependencies shared across the cut), so each part
 must still be gated on its own record. `suggestedParts` is 1
 whenever the prove ran. The claim bytes are filled either way (the
 claim is known before proving starts).

 The final IO buffer is not returned — it is the shard's whole
 ingested byte scope and no caller reads it. -/
structure ShardProveResult where
 claimBytes : ByteArray
 proof : Option Proof
 peakBytes : Nat
 suggestedParts : Nat

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String ProveEnvResult

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& Nat → Bool →
 Except String ShardProveResult

/-- Per-shard prove against a Rust-owned `EnvHandle`: ONE execution,
 whose record is proven from directly.

 `maxRamBytes` is a per-shard prover-RAM budget checked against that
 record's projected peak before the witness phase begins; `0` means
 detect (85% of `MemAvailable`, the policy the check batch's RAM gate
 uses), and an unreadable `/proc/meminfo` disables the check rather
 than guessing. Over budget, the record is dropped and `proof` is
 `none` — learning that here costs one execution instead of an OOM
 part-way through an FFT. The peak comes back either way, so a prove
 run yields the same split/merge signal a check run does.

 `execOnly` stops after execution + measurement (`proof` is `none`
 either way; `suggestedParts` is 1 exactly when the peak fits): the
 split loop runs on executions alone, never starting a STARK. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (maxRamBytes : Nat := 0)
 (execOnly : Bool := false) :
 Except String ShardProveResult :=
 shardProveWithEnv' system funIdx envHandle ownedBlob maxRamBytes execOnly

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem →
 @& Array G → @& Proof → Except String Unit

end AiurSystem

/-- Write a `.ixes` manifest for an EXPLICIT partition — the block lists
 a run actually produced (splits included) rather than a planner's
 output. `shardsBlob`: per shard, a 4-byte LE block count followed by
 that many 32-byte block addresses; every env block must appear in
 exactly one shard. `peaksBlob`: one 8-byte LE measured prover peak
 per shard in order, recorded on the manifest for schedulers. Own
 sizes, foreign blocks, cross-ingress and assumption roots are
 recomputed from the env's static profile; prints the manifest
 summary to stderr. -/
@[extern "rs_shard_manifest_from_partition"]
opaque shardManifestFromPartition : @& EnvHandle →
 @& ByteArray → @& ByteArray → @& String → IO Unit

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. -/
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 →
 Except String (Array (String × Nat))
 @& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
 Except String (Array ShardResult)

/-- Check EVERY shard of a partition in one call: rayon over the shard
 list with true work-stealing (no chunk barriers), each shard
 through the exact single-shard machinery over its own private
 record and witness io. `shardsBlob` encodes, per shard, a 4-byte LE
 owned-constant count followed by that many 32-byte addresses.
 Returns one `(error, peakBytes)` pair 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).
 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).
 `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
 system RAM), not by thread count — pass `jobs` only to narrow
 CPU use. -/
 CPU use.

 `maxRamBytes > 0` is a per-shard prover-RAM budget: each result's
 `suggestedParts` is 1 when its peak fits and the model's projected
 part count otherwise, so a caller can cut over-budget shards and
 re-batch the parts — the wave loop that audits a partition's split
 behavior on executions alone. -/
def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
 (commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
 (friParameters : FriParameters := defaultFriParameters)
 : Except String (Array (String × Nat)) :=
 (profile : Bool := false) (checkConstIdx : Nat := 0)
 (maxRamBytes : Nat := 0)
 : Except String (Array ShardResult) :=
 shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
 jobs commitmentParameters friParameters
 jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes

end Bytecode.Toplevel

Expand Down

109 changes: 101 additions & 8 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -75,14 +75,61 @@ 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`. -/
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. -/
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.
Expand DownExpand Up@@ -122,6 +169,7 @@ 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`,
Expand All@@ -132,14 +180,24 @@ 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).map
 (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -153,9 +211,19 @@ 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).map
 (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -181,7 +249,8 @@ opaque executeMultiStark (toplevel : @& Bytecode.Toplevel)

@[extern "rs_aiur_toplevel_check_addr_with_env"]
private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -193,7 +262,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).map
 (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

@[extern "rs_aiur_toplevel_check_addrs_with_env"]
Expand All@@ -207,7 +276,8 @@ private opaque checkAddrsWithEnv' : @& Bytecode.Toplevel →
 through the exact single-claim machinery over task-private data
 (own witness io, own query record), nothing shared between tasks
 but the read-only toplevel and env. Returns the FAILURES as
 `(addrHex, error)` pairs; empty means all passed. Per-claim
 `(batch index as a decimal string, error)` pairs, resolving back to
 the caller's label order; empty means all passed. Per-claim
 outputs/records are not returned — use `checkAddrWithEnv` for a
 single claim's full result. -/
def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
Expand All@@ -216,9 +286,21 @@ 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 → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-shard check with the witness shape (wrapper-augmented byte
Expand All@@ -228,9 +310,20 @@ 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).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).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
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
7
commits into

base:main
Choose a base branch

from

 Draft


perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


7 commits


Select commit
Hold shift + click to select a range
66fb376

aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro…


arthurpaulino Aug 24, 2026
1639996

aiur: batch weights; budget-gated proves that split in place


samuelburnham Aug 28, 2026
f529e09

aiur: model-driven splitting, exec-only audits, corrected-manifest emit


samuelburnham Aug 27, 2026
7de7a7b

aiur: quality pass, --ram-budget semantics, settled seed sizing


samuelburnham Aug 28, 2026
20f5e62

bench: aiur-sharded-env exercises the split audit


samuelburnham Aug 28, 2026
f43447c

aiur: scale static shard seeds by block profile


samuelburnham Aug 28, 2026
319df80

fmt, clippy


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


133 changes: 116 additions & 17 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -173,54 +173,153 @@ def proveAddrWithEnv (system : @& AiurSystem)
 (proveAddrWithEnv' system funIdx envHandle addrBytes useBytecode).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

/-- Result of a per-shard prove: the claim's wire bytes, the proof, the
 projected prover RAM peak of the record that produced it
 (`AiurSystem::peak_prove_bytes`), and the part count the peak model
 projects will fit the budget
 (`AiurSystem::suggested_split_parts`).

 `proof` is `none` exactly when the peak exceeded the budget — a
 RESULT rather than an error, since the caller's answer is to cut
 the shard into `suggestedParts` parts and prove those. The count is
 computed Rust-side because only there does the executed record
 still exist to read per-circuit heights from; it is optimistic
 (parts re-execute dependencies shared across the cut), so each part
 must still be gated on its own record. `suggestedParts` is 1
 whenever the prove ran. The claim bytes are filled either way (the
 claim is known before proving starts).

 The final IO buffer is not returned — it is the shard's whole
 ingested byte scope and no caller reads it. -/
structure ShardProveResult where
 claimBytes : ByteArray
 proof : Option Proof
 peakBytes : Nat
 suggestedParts : Nat

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String ProveEnvResult

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& Nat → Bool →
 Except String ShardProveResult

/-- Per-shard prove against a Rust-owned `EnvHandle`: ONE execution,
 whose record is proven from directly.

 `maxRamBytes` is a per-shard prover-RAM budget checked against that
 record's projected peak before the witness phase begins; `0` means
 detect (85% of `MemAvailable`, the policy the check batch's RAM gate
 uses), and an unreadable `/proc/meminfo` disables the check rather
 than guessing. Over budget, the record is dropped and `proof` is
 `none` — learning that here costs one execution instead of an OOM
 part-way through an FFT. The peak comes back either way, so a prove
 run yields the same split/merge signal a check run does.

 `execOnly` stops after execution + measurement (`proof` is `none`
 either way; `suggestedParts` is 1 exactly when the peak fits): the
 split loop runs on executions alone, never starting a STARK. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (maxRamBytes : Nat := 0)
 (execOnly : Bool := false) :
 Except String ShardProveResult :=
 shardProveWithEnv' system funIdx envHandle ownedBlob maxRamBytes execOnly

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem →
 @& Array G → @& Proof → Except String Unit

end AiurSystem

/-- Write a `.ixes` manifest for an EXPLICIT partition — the block lists
 a run actually produced (splits included) rather than a planner's
 output. `shardsBlob`: per shard, a 4-byte LE block count followed by
 that many 32-byte block addresses; every env block must appear in
 exactly one shard. `peaksBlob`: one 8-byte LE measured prover peak
 per shard in order, recorded on the manifest for schedulers. Own
 sizes, foreign blocks, cross-ingress and assumption roots are
 recomputed from the env's static profile; prints the manifest
 summary to stderr. -/
@[extern "rs_shard_manifest_from_partition"]
opaque shardManifestFromPartition : @& EnvHandle →
 @& ByteArray → @& ByteArray → @& String → IO Unit

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. -/
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 →
 Except String (Array (String × Nat))
 @& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
 Except String (Array ShardResult)

/-- Check EVERY shard of a partition in one call: rayon over the shard
 list with true work-stealing (no chunk barriers), each shard
 through the exact single-shard machinery over its own private
 record and witness io. `shardsBlob` encodes, per shard, a 4-byte LE
 owned-constant count followed by that many 32-byte addresses.
 Returns one `(error, peakBytes)` pair 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).
 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).
 `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
 system RAM), not by thread count — pass `jobs` only to narrow
 CPU use. -/
 CPU use.

 `maxRamBytes > 0` is a per-shard prover-RAM budget: each result's
 `suggestedParts` is 1 when its peak fits and the model's projected
 part count otherwise, so a caller can cut over-budget shards and
 re-batch the parts — the wave loop that audits a partition's split
 behavior on executions alone. -/
def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
 (commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
 (friParameters : FriParameters := defaultFriParameters)
 : Except String (Array (String × Nat)) :=
 (profile : Bool := false) (checkConstIdx : Nat := 0)
 (maxRamBytes : Nat := 0)
 : Except String (Array ShardResult) :=
 shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
 jobs commitmentParameters friParameters
 jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes

end Bytecode.Toplevel

Expand Down

109 changes: 101 additions & 8 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -75,14 +75,61 @@ 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`. -/
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. -/
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.
Expand DownExpand Up@@ -122,6 +169,7 @@ 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`,
Expand All@@ -132,14 +180,24 @@ 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).map
 (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -153,9 +211,19 @@ 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).map
 (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -181,7 +249,8 @@ opaque executeMultiStark (toplevel : @& Bytecode.Toplevel)

@[extern "rs_aiur_toplevel_check_addr_with_env"]
private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -193,7 +262,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).map
 (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

@[extern "rs_aiur_toplevel_check_addrs_with_env"]
Expand All@@ -207,7 +276,8 @@ private opaque checkAddrsWithEnv' : @& Bytecode.Toplevel →
 through the exact single-claim machinery over task-private data
 (own witness io, own query record), nothing shared between tasks
 but the read-only toplevel and env. Returns the FAILURES as
 `(addrHex, error)` pairs; empty means all passed. Per-claim
 `(batch index as a decimal string, error)` pairs, resolving back to
 the caller's label order; empty means all passed. Per-claim
 outputs/records are not returned — use `checkAddrWithEnv` for a
 single claim's full result. -/
def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
Expand All@@ -216,9 +286,21 @@ 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 → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-shard check with the witness shape (wrapper-augmented byte
Expand All@@ -228,9 +310,20 @@ 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).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).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
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
7
commits into

base:main
Choose a base branch

from

 Draft


perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


7 commits


Select commit
Hold shift + click to select a range
66fb376

aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro…


arthurpaulino Aug 24, 2026
1639996

aiur: batch weights; budget-gated proves that split in place


samuelburnham Aug 28, 2026
f529e09

aiur: model-driven splitting, exec-only audits, corrected-manifest emit


samuelburnham Aug 27, 2026
7de7a7b

aiur: quality pass, --ram-budget semantics, settled seed sizing


samuelburnham Aug 28, 2026
20f5e62

bench: aiur-sharded-env exercises the split audit


samuelburnham Aug 28, 2026
f43447c

aiur: scale static shard seeds by block profile


samuelburnham Aug 28, 2026
319df80

fmt, clippy


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


133 changes: 116 additions & 17 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -173,54 +173,153 @@ def proveAddrWithEnv (system : @& AiurSystem)
 (proveAddrWithEnv' system funIdx envHandle addrBytes useBytecode).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

/-- Result of a per-shard prove: the claim's wire bytes, the proof, the
 projected prover RAM peak of the record that produced it
 (`AiurSystem::peak_prove_bytes`), and the part count the peak model
 projects will fit the budget
 (`AiurSystem::suggested_split_parts`).

 `proof` is `none` exactly when the peak exceeded the budget — a
 RESULT rather than an error, since the caller's answer is to cut
 the shard into `suggestedParts` parts and prove those. The count is
 computed Rust-side because only there does the executed record
 still exist to read per-circuit heights from; it is optimistic
 (parts re-execute dependencies shared across the cut), so each part
 must still be gated on its own record. `suggestedParts` is 1
 whenever the prove ran. The claim bytes are filled either way (the
 claim is known before proving starts).

 The final IO buffer is not returned — it is the shard's whole
 ingested byte scope and no caller reads it. -/
structure ShardProveResult where
 claimBytes : ByteArray
 proof : Option Proof
 peakBytes : Nat
 suggestedParts : Nat

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String ProveEnvResult

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& Nat → Bool →
 Except String ShardProveResult

/-- Per-shard prove against a Rust-owned `EnvHandle`: ONE execution,
 whose record is proven from directly.

 `maxRamBytes` is a per-shard prover-RAM budget checked against that
 record's projected peak before the witness phase begins; `0` means
 detect (85% of `MemAvailable`, the policy the check batch's RAM gate
 uses), and an unreadable `/proc/meminfo` disables the check rather
 than guessing. Over budget, the record is dropped and `proof` is
 `none` — learning that here costs one execution instead of an OOM
 part-way through an FFT. The peak comes back either way, so a prove
 run yields the same split/merge signal a check run does.

 `execOnly` stops after execution + measurement (`proof` is `none`
 either way; `suggestedParts` is 1 exactly when the peak fits): the
 split loop runs on executions alone, never starting a STARK. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (maxRamBytes : Nat := 0)
 (execOnly : Bool := false) :
 Except String ShardProveResult :=
 shardProveWithEnv' system funIdx envHandle ownedBlob maxRamBytes execOnly

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem →
 @& Array G → @& Proof → Except String Unit

end AiurSystem

/-- Write a `.ixes` manifest for an EXPLICIT partition — the block lists
 a run actually produced (splits included) rather than a planner's
 output. `shardsBlob`: per shard, a 4-byte LE block count followed by
 that many 32-byte block addresses; every env block must appear in
 exactly one shard. `peaksBlob`: one 8-byte LE measured prover peak
 per shard in order, recorded on the manifest for schedulers. Own
 sizes, foreign blocks, cross-ingress and assumption roots are
 recomputed from the env's static profile; prints the manifest
 summary to stderr. -/
@[extern "rs_shard_manifest_from_partition"]
opaque shardManifestFromPartition : @& EnvHandle →
 @& ByteArray → @& ByteArray → @& String → IO Unit

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. -/
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 →
 Except String (Array (String × Nat))
 @& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
 Except String (Array ShardResult)

/-- Check EVERY shard of a partition in one call: rayon over the shard
 list with true work-stealing (no chunk barriers), each shard
 through the exact single-shard machinery over its own private
 record and witness io. `shardsBlob` encodes, per shard, a 4-byte LE
 owned-constant count followed by that many 32-byte addresses.
 Returns one `(error, peakBytes)` pair 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).
 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).
 `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
 system RAM), not by thread count — pass `jobs` only to narrow
 CPU use. -/
 CPU use.

 `maxRamBytes > 0` is a per-shard prover-RAM budget: each result's
 `suggestedParts` is 1 when its peak fits and the model's projected
 part count otherwise, so a caller can cut over-budget shards and
 re-batch the parts — the wave loop that audits a partition's split
 behavior on executions alone. -/
def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
 (commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
 (friParameters : FriParameters := defaultFriParameters)
 : Except String (Array (String × Nat)) :=
 (profile : Bool := false) (checkConstIdx : Nat := 0)
 (maxRamBytes : Nat := 0)
 : Except String (Array ShardResult) :=
 shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
 jobs commitmentParameters friParameters
 jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes

end Bytecode.Toplevel

Expand Down

109 changes: 101 additions & 8 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -75,14 +75,61 @@ 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`. -/
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. -/
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.
Expand DownExpand Up@@ -122,6 +169,7 @@ 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`,
Expand All@@ -132,14 +180,24 @@ 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).map
 (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -153,9 +211,19 @@ 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).map
 (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -181,7 +249,8 @@ opaque executeMultiStark (toplevel : @& Bytecode.Toplevel)

@[extern "rs_aiur_toplevel_check_addr_with_env"]
private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -193,7 +262,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).map
 (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

@[extern "rs_aiur_toplevel_check_addrs_with_env"]
Expand All@@ -207,7 +276,8 @@ private opaque checkAddrsWithEnv' : @& Bytecode.Toplevel →
 through the exact single-claim machinery over task-private data
 (own witness io, own query record), nothing shared between tasks
 but the read-only toplevel and env. Returns the FAILURES as
 `(addrHex, error)` pairs; empty means all passed. Per-claim
 `(batch index as a decimal string, error)` pairs, resolving back to
 the caller's label order; empty means all passed. Per-claim
 outputs/records are not returned — use `checkAddrWithEnv` for a
 single claim's full result. -/
def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
Expand All@@ -216,9 +286,21 @@ 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 → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-shard check with the witness shape (wrapper-augmented byte
Expand All@@ -228,9 +310,20 @@ 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).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).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
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
7
commits into

base:main
Choose a base branch

from

 Draft


perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


7 commits


Select commit
Hold shift + click to select a range
66fb376

aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro…


arthurpaulino Aug 24, 2026
1639996

aiur: batch weights; budget-gated proves that split in place


samuelburnham Aug 28, 2026
f529e09

aiur: model-driven splitting, exec-only audits, corrected-manifest emit


samuelburnham Aug 27, 2026
7de7a7b

aiur: quality pass, --ram-budget semantics, settled seed sizing


samuelburnham Aug 28, 2026
20f5e62

bench: aiur-sharded-env exercises the split audit


samuelburnham Aug 28, 2026
f43447c

aiur: scale static shard seeds by block profile


samuelburnham Aug 28, 2026
319df80

fmt, clippy


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


133 changes: 116 additions & 17 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -173,54 +173,153 @@ def proveAddrWithEnv (system : @& AiurSystem)
 (proveAddrWithEnv' system funIdx envHandle addrBytes useBytecode).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

/-- Result of a per-shard prove: the claim's wire bytes, the proof, the
 projected prover RAM peak of the record that produced it
 (`AiurSystem::peak_prove_bytes`), and the part count the peak model
 projects will fit the budget
 (`AiurSystem::suggested_split_parts`).

 `proof` is `none` exactly when the peak exceeded the budget — a
 RESULT rather than an error, since the caller's answer is to cut
 the shard into `suggestedParts` parts and prove those. The count is
 computed Rust-side because only there does the executed record
 still exist to read per-circuit heights from; it is optimistic
 (parts re-execute dependencies shared across the cut), so each part
 must still be gated on its own record. `suggestedParts` is 1
 whenever the prove ran. The claim bytes are filled either way (the
 claim is known before proving starts).

 The final IO buffer is not returned — it is the shard's whole
 ingested byte scope and no caller reads it. -/
structure ShardProveResult where
 claimBytes : ByteArray
 proof : Option Proof
 peakBytes : Nat
 suggestedParts : Nat

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String ProveEnvResult

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& Nat → Bool →
 Except String ShardProveResult

/-- Per-shard prove against a Rust-owned `EnvHandle`: ONE execution,
 whose record is proven from directly.

 `maxRamBytes` is a per-shard prover-RAM budget checked against that
 record's projected peak before the witness phase begins; `0` means
 detect (85% of `MemAvailable`, the policy the check batch's RAM gate
 uses), and an unreadable `/proc/meminfo` disables the check rather
 than guessing. Over budget, the record is dropped and `proof` is
 `none` — learning that here costs one execution instead of an OOM
 part-way through an FFT. The peak comes back either way, so a prove
 run yields the same split/merge signal a check run does.

 `execOnly` stops after execution + measurement (`proof` is `none`
 either way; `suggestedParts` is 1 exactly when the peak fits): the
 split loop runs on executions alone, never starting a STARK. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (maxRamBytes : Nat := 0)
 (execOnly : Bool := false) :
 Except String ShardProveResult :=
 shardProveWithEnv' system funIdx envHandle ownedBlob maxRamBytes execOnly

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem →
 @& Array G → @& Proof → Except String Unit

end AiurSystem

/-- Write a `.ixes` manifest for an EXPLICIT partition — the block lists
 a run actually produced (splits included) rather than a planner's
 output. `shardsBlob`: per shard, a 4-byte LE block count followed by
 that many 32-byte block addresses; every env block must appear in
 exactly one shard. `peaksBlob`: one 8-byte LE measured prover peak
 per shard in order, recorded on the manifest for schedulers. Own
 sizes, foreign blocks, cross-ingress and assumption roots are
 recomputed from the env's static profile; prints the manifest
 summary to stderr. -/
@[extern "rs_shard_manifest_from_partition"]
opaque shardManifestFromPartition : @& EnvHandle →
 @& ByteArray → @& ByteArray → @& String → IO Unit

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. -/
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 →
 Except String (Array (String × Nat))
 @& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
 Except String (Array ShardResult)

/-- Check EVERY shard of a partition in one call: rayon over the shard
 list with true work-stealing (no chunk barriers), each shard
 through the exact single-shard machinery over its own private
 record and witness io. `shardsBlob` encodes, per shard, a 4-byte LE
 owned-constant count followed by that many 32-byte addresses.
 Returns one `(error, peakBytes)` pair 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).
 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).
 `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
 system RAM), not by thread count — pass `jobs` only to narrow
 CPU use. -/
 CPU use.

 `maxRamBytes > 0` is a per-shard prover-RAM budget: each result's
 `suggestedParts` is 1 when its peak fits and the model's projected
 part count otherwise, so a caller can cut over-budget shards and
 re-batch the parts — the wave loop that audits a partition's split
 behavior on executions alone. -/
def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
 (commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
 (friParameters : FriParameters := defaultFriParameters)
 : Except String (Array (String × Nat)) :=
 (profile : Bool := false) (checkConstIdx : Nat := 0)
 (maxRamBytes : Nat := 0)
 : Except String (Array ShardResult) :=
 shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
 jobs commitmentParameters friParameters
 jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes

end Bytecode.Toplevel

Expand Down

109 changes: 101 additions & 8 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -75,14 +75,61 @@ 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`. -/
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. -/
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.
Expand DownExpand Up@@ -122,6 +169,7 @@ 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`,
Expand All@@ -132,14 +180,24 @@ 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).map
 (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -153,9 +211,19 @@ 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).map
 (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -181,7 +249,8 @@ opaque executeMultiStark (toplevel : @& Bytecode.Toplevel)

@[extern "rs_aiur_toplevel_check_addr_with_env"]
private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -193,7 +262,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).map
 (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

@[extern "rs_aiur_toplevel_check_addrs_with_env"]
Expand All@@ -207,7 +276,8 @@ private opaque checkAddrsWithEnv' : @& Bytecode.Toplevel →
 through the exact single-claim machinery over task-private data
 (own witness io, own query record), nothing shared between tasks
 but the read-only toplevel and env. Returns the FAILURES as
 `(addrHex, error)` pairs; empty means all passed. Per-claim
 `(batch index as a decimal string, error)` pairs, resolving back to
 the caller's label order; empty means all passed. Per-claim
 outputs/records are not returned — use `checkAddrWithEnv` for a
 single claim's full result. -/
def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
Expand All@@ -216,9 +286,21 @@ 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 → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-shard check with the witness shape (wrapper-augmented byte
Expand All@@ -228,9 +310,20 @@ 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).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).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
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
7
commits into

base:main
Choose a base branch

from

 Draft


perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


7 commits


Select commit
Hold shift + click to select a range
66fb376

aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro…


arthurpaulino Aug 24, 2026
1639996

aiur: batch weights; budget-gated proves that split in place


samuelburnham Aug 28, 2026
f529e09

aiur: model-driven splitting, exec-only audits, corrected-manifest emit


samuelburnham Aug 27, 2026
7de7a7b

aiur: quality pass, --ram-budget semantics, settled seed sizing


samuelburnham Aug 28, 2026
20f5e62

bench: aiur-sharded-env exercises the split audit


samuelburnham Aug 28, 2026
f43447c

aiur: scale static shard seeds by block profile


samuelburnham Aug 28, 2026
319df80

fmt, clippy


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


133 changes: 116 additions & 17 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -173,54 +173,153 @@ def proveAddrWithEnv (system : @& AiurSystem)
 (proveAddrWithEnv' system funIdx envHandle addrBytes useBytecode).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

/-- Result of a per-shard prove: the claim's wire bytes, the proof, the
 projected prover RAM peak of the record that produced it
 (`AiurSystem::peak_prove_bytes`), and the part count the peak model
 projects will fit the budget
 (`AiurSystem::suggested_split_parts`).

 `proof` is `none` exactly when the peak exceeded the budget — a
 RESULT rather than an error, since the caller's answer is to cut
 the shard into `suggestedParts` parts and prove those. The count is
 computed Rust-side because only there does the executed record
 still exist to read per-circuit heights from; it is optimistic
 (parts re-execute dependencies shared across the cut), so each part
 must still be gated on its own record. `suggestedParts` is 1
 whenever the prove ran. The claim bytes are filled either way (the
 claim is known before proving starts).

 The final IO buffer is not returned — it is the shard's whole
 ingested byte scope and no caller reads it. -/
structure ShardProveResult where
 claimBytes : ByteArray
 proof : Option Proof
 peakBytes : Nat
 suggestedParts : Nat

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String ProveEnvResult

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& Nat → Bool →
 Except String ShardProveResult

/-- Per-shard prove against a Rust-owned `EnvHandle`: ONE execution,
 whose record is proven from directly.

 `maxRamBytes` is a per-shard prover-RAM budget checked against that
 record's projected peak before the witness phase begins; `0` means
 detect (85% of `MemAvailable`, the policy the check batch's RAM gate
 uses), and an unreadable `/proc/meminfo` disables the check rather
 than guessing. Over budget, the record is dropped and `proof` is
 `none` — learning that here costs one execution instead of an OOM
 part-way through an FFT. The peak comes back either way, so a prove
 run yields the same split/merge signal a check run does.

 `execOnly` stops after execution + measurement (`proof` is `none`
 either way; `suggestedParts` is 1 exactly when the peak fits): the
 split loop runs on executions alone, never starting a STARK. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (maxRamBytes : Nat := 0)
 (execOnly : Bool := false) :
 Except String ShardProveResult :=
 shardProveWithEnv' system funIdx envHandle ownedBlob maxRamBytes execOnly

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem →
 @& Array G → @& Proof → Except String Unit

end AiurSystem

/-- Write a `.ixes` manifest for an EXPLICIT partition — the block lists
 a run actually produced (splits included) rather than a planner's
 output. `shardsBlob`: per shard, a 4-byte LE block count followed by
 that many 32-byte block addresses; every env block must appear in
 exactly one shard. `peaksBlob`: one 8-byte LE measured prover peak
 per shard in order, recorded on the manifest for schedulers. Own
 sizes, foreign blocks, cross-ingress and assumption roots are
 recomputed from the env's static profile; prints the manifest
 summary to stderr. -/
@[extern "rs_shard_manifest_from_partition"]
opaque shardManifestFromPartition : @& EnvHandle →
 @& ByteArray → @& ByteArray → @& String → IO Unit

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. -/
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 →
 Except String (Array (String × Nat))
 @& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
 Except String (Array ShardResult)

/-- Check EVERY shard of a partition in one call: rayon over the shard
 list with true work-stealing (no chunk barriers), each shard
 through the exact single-shard machinery over its own private
 record and witness io. `shardsBlob` encodes, per shard, a 4-byte LE
 owned-constant count followed by that many 32-byte addresses.
 Returns one `(error, peakBytes)` pair 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).
 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).
 `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
 system RAM), not by thread count — pass `jobs` only to narrow
 CPU use. -/
 CPU use.

 `maxRamBytes > 0` is a per-shard prover-RAM budget: each result's
 `suggestedParts` is 1 when its peak fits and the model's projected
 part count otherwise, so a caller can cut over-budget shards and
 re-batch the parts — the wave loop that audits a partition's split
 behavior on executions alone. -/
def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
 (commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
 (friParameters : FriParameters := defaultFriParameters)
 : Except String (Array (String × Nat)) :=
 (profile : Bool := false) (checkConstIdx : Nat := 0)
 (maxRamBytes : Nat := 0)
 : Except String (Array ShardResult) :=
 shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
 jobs commitmentParameters friParameters
 jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes

end Bytecode.Toplevel

Expand Down

109 changes: 101 additions & 8 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -75,14 +75,61 @@ 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`. -/
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. -/
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.
Expand DownExpand Up@@ -122,6 +169,7 @@ 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`,
Expand All@@ -132,14 +180,24 @@ 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).map
 (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -153,9 +211,19 @@ 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).map
 (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -181,7 +249,8 @@ opaque executeMultiStark (toplevel : @& Bytecode.Toplevel)

@[extern "rs_aiur_toplevel_check_addr_with_env"]
private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -193,7 +262,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).map
 (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

@[extern "rs_aiur_toplevel_check_addrs_with_env"]
Expand All@@ -207,7 +276,8 @@ private opaque checkAddrsWithEnv' : @& Bytecode.Toplevel →
 through the exact single-claim machinery over task-private data
 (own witness io, own query record), nothing shared between tasks
 but the read-only toplevel and env. Returns the FAILURES as
 `(addrHex, error)` pairs; empty means all passed. Per-claim
 `(batch index as a decimal string, error)` pairs, resolving back to
 the caller's label order; empty means all passed. Per-claim
 outputs/records are not returned — use `checkAddrWithEnv` for a
 single claim's full result. -/
def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
Expand All@@ -216,9 +286,21 @@ 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 → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-shard check with the witness shape (wrapper-augmented byte
Expand All@@ -228,9 +310,20 @@ 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).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).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
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
7
commits into

base:main
Choose a base branch

from

 Draft


perf: Tune ix shard counts and recalibrate for proving via --ram-budget#601
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


7 commits


Select commit
Hold shift + click to select a range
66fb376

aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro…


arthurpaulino Aug 24, 2026
1639996

aiur: batch weights; budget-gated proves that split in place


samuelburnham Aug 28, 2026
f529e09

aiur: model-driven splitting, exec-only audits, corrected-manifest emit


samuelburnham Aug 27, 2026
7de7a7b

aiur: quality pass, --ram-budget semantics, settled seed sizing


samuelburnham Aug 28, 2026
20f5e62

bench: aiur-sharded-env exercises the split audit


samuelburnham Aug 28, 2026
f43447c

aiur: scale static shard seeds by block profile


samuelburnham Aug 28, 2026
319df80

fmt, clippy


samuelburnham Aug 28, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


133 changes: 116 additions & 17 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -173,54 +173,153 @@ def proveAddrWithEnv (system : @& AiurSystem)
 (proveAddrWithEnv' system funIdx envHandle addrBytes useBytecode).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

/-- Result of a per-shard prove: the claim's wire bytes, the proof, the
 projected prover RAM peak of the record that produced it
 (`AiurSystem::peak_prove_bytes`), and the part count the peak model
 projects will fit the budget
 (`AiurSystem::suggested_split_parts`).

 `proof` is `none` exactly when the peak exceeded the budget — a
 RESULT rather than an error, since the caller's answer is to cut
 the shard into `suggestedParts` parts and prove those. The count is
 computed Rust-side because only there does the executed record
 still exist to read per-circuit heights from; it is optimistic
 (parts re-execute dependencies shared across the cut), so each part
 must still be gated on its own record. `suggestedParts` is 1
 whenever the prove ran. The claim bytes are filled either way (the
 claim is known before proving starts).

 The final IO buffer is not returned — it is the shard's whole
 ingested byte scope and no caller reads it. -/
structure ShardProveResult where
 claimBytes : ByteArray
 proof : Option Proof
 peakBytes : Nat
 suggestedParts : Nat

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String ProveEnvResult

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& Nat → Bool →
 Except String ShardProveResult

/-- Per-shard prove against a Rust-owned `EnvHandle`: ONE execution,
 whose record is proven from directly.

 `maxRamBytes` is a per-shard prover-RAM budget checked against that
 record's projected peak before the witness phase begins; `0` means
 detect (85% of `MemAvailable`, the policy the check batch's RAM gate
 uses), and an unreadable `/proc/meminfo` disables the check rather
 than guessing. Over budget, the record is dropped and `proof` is
 `none` — learning that here costs one execution instead of an OOM
 part-way through an FFT. The peak comes back either way, so a prove
 run yields the same split/merge signal a check run does.

 `execOnly` stops after execution + measurement (`proof` is `none`
 either way; `suggestedParts` is 1 exactly when the peak fits): the
 split loop runs on executions alone, never starting a STARK. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (maxRamBytes : Nat := 0)
 (execOnly : Bool := false) :
 Except String ShardProveResult :=
 shardProveWithEnv' system funIdx envHandle ownedBlob maxRamBytes execOnly

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem →
 @& Array G → @& Proof → Except String Unit

end AiurSystem

/-- Write a `.ixes` manifest for an EXPLICIT partition — the block lists
 a run actually produced (splits included) rather than a planner's
 output. `shardsBlob`: per shard, a 4-byte LE block count followed by
 that many 32-byte block addresses; every env block must appear in
 exactly one shard. `peaksBlob`: one 8-byte LE measured prover peak
 per shard in order, recorded on the manifest for schedulers. Own
 sizes, foreign blocks, cross-ingress and assumption roots are
 recomputed from the env's static profile; prints the manifest
 summary to stderr. -/
@[extern "rs_shard_manifest_from_partition"]
opaque shardManifestFromPartition : @& EnvHandle →
 @& ByteArray → @& ByteArray → @& String → IO Unit

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. -/
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 →
 Except String (Array (String × Nat))
 @& CommitmentParameters → @& FriParameters → Bool → @& Nat → @& Nat →
 Except String (Array ShardResult)

/-- Check EVERY shard of a partition in one call: rayon over the shard
 list with true work-stealing (no chunk barriers), each shard
 through the exact single-shard machinery over its own private
 record and witness io. `shardsBlob` encodes, per shard, a 4-byte LE
 owned-constant count followed by that many 32-byte addresses.
 Returns one `(error, peakBytes)` pair 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).
 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).
 `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
 system RAM), not by thread count — pass `jobs` only to narrow
 CPU use. -/
 CPU use.

 `maxRamBytes > 0` is a per-shard prover-RAM budget: each result's
 `suggestedParts` is 1 when its peak fits and the model's projected
 part count otherwise, so a caller can cut over-budget shards and
 re-batch the parts — the wave loop that audits a partition's split
 behavior on executions alone. -/
def shardCheckBatchWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (shardsBlob : ByteArray) (useBytecode : Bool := false) (jobs : Nat := 0)
 (commitmentParameters : CommitmentParameters := defaultCommitmentParameters)
 (friParameters : FriParameters := defaultFriParameters)
 : Except String (Array (String × Nat)) :=
 (profile : Bool := false) (checkConstIdx : Nat := 0)
 (maxRamBytes : Nat := 0)
 : Except String (Array ShardResult) :=
 shardCheckBatchWithEnv' toplevel funIdx envHandle shardsBlob useBytecode
 jobs commitmentParameters friParameters
 jobs commitmentParameters friParameters profile checkConstIdx maxRamBytes

end Bytecode.Toplevel

Expand Down

109 changes: 101 additions & 8 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -75,14 +75,61 @@ 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`. -/
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. -/
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.
Expand DownExpand Up@@ -122,6 +169,7 @@ 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`,
Expand All@@ -132,14 +180,24 @@ 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).map
 (execute' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -153,9 +211,19 @@ 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).map
 (executeIxVM' toplevel funIdx args ioBuffer.data.toArray ioBuffer.map.toArray false).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
Expand All@@ -181,7 +249,8 @@ opaque executeMultiStark (toplevel : @& Bytecode.Toplevel)

@[extern "rs_aiur_toplevel_check_addr_with_env"]
private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -193,7 +262,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).map
 (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode false).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

@[extern "rs_aiur_toplevel_check_addrs_with_env"]
Expand All@@ -207,7 +276,8 @@ private opaque checkAddrsWithEnv' : @& Bytecode.Toplevel →
 through the exact single-claim machinery over task-private data
 (own witness io, own query record), nothing shared between tasks
 but the read-only toplevel and env. Returns the FAILURES as
 `(addrHex, error)` pairs; empty means all passed. Per-claim
 `(batch index as a decimal string, error)` pairs, resolving back to
 the caller's label order; empty means all passed. Per-claim
 outputs/records are not returned — use `checkAddrWithEnv` for a
 single claim's full result. -/
def checkAddrsWithEnv (toplevel : @& Bytecode.Toplevel)
Expand All@@ -216,9 +286,21 @@ 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 → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 (useBytecode profile : Bool) →
 Except String ExecuteResult

/-- Per-shard check with the witness shape (wrapper-augmented byte
Expand All@@ -228,9 +310,20 @@ 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).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode false).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
Expand Down
Loading
Loading