IxVM: native execution pipeline#463

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

Merged
arthurpaulino merged 10 commits into from
Jul 3, 2026
Merged

IxVM: native execution pipeline #463

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
0cec144
Aiur Bytecode → Rust codegen for the IxVM kernel
arthurpaulino Jun 30, 2026
aedbf85
Move shard witness construction to Rust + parallelise
arthurpaulino Jun 30, 2026
c9ffd70
Codegen: value-returning byte ops, dead-fold the unconstrained
arthurpaulino Jun 30, 2026
c6c86a6
Wire Rust witness fast path through every check/prove entry point
arthurpaulino Jun 30, 2026
e7b37f7
EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls
arthurpaulino Jun 30, 2026
899d212
ix codegen: add --check flag for CI; gate stale generated kernel
arthurpaulino Jun 30, 2026
56a7ab8
ix check: --interp {source|bytecode} to bypass codegen kernel
arthurpaulino Jul 1, 2026
33ad65a
IxVM codegen: regen + rebase-fixups after KLevel port
arthurpaulino Jul 2, 2026
9d17f9f
ix-check + ixvm tests: coverage gate, --interp source fix, codegen pa…
arthurpaulino Jul 3, 2026
033968c
cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception
arthurpaulino Jul 3, 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
2 changes: 2 additions & 0 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -27,6 +27,8 @@ jobs:
# lean-action builds above — fails CI.
- name: Build all targets
run: lake lint -- --wfail -v
- name: Check codegen'd IxVM kernel is up to date
run: lake exe ix codegen --check
- name: Test Ix CLI
run: lake test --wfail -- cli
- name: Aiur tests
Expand Down
4 changes: 3 additions & 1 deletion Benchmarks/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -34,7 +34,9 @@ def main : IO Unit := do

let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
throughput (.Elements n.toUInt64 "consts")
-- IxVM-native prove: routes execution through the codegen'd Rust
-- kernel (`execute_generated`) instead of the bytecode interpreter.
bench "serde/blake3 Nat.add_comm"
(aiurSystem.prove friParameters funIdx #[.ofNat n])
(aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
ioBuffer
return
47 changes: 35 additions & 12 deletions Benchmarks/Typecheck.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -172,11 +172,6 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
| .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1
| .ok env => pure env
IO.println s!"Loaded {ixePath}: {ixonEnv.namedCount} named, {ixonEnv.constCount} consts"
-- Build the witness for `addr`: subject-only (`verify_const`) trusts deps;
-- otherwise the full-closure check (`verify_claim`, `check addr none`).
let mkWitness (addr : Address) : IO IxVM.ClaimHarness.ClaimWitness :=
if subjectOnly then pure (IxVM.ClaimHarness.buildVerifyConst ixonEnv addr)
else IO.ofExcept (IxVM.ClaimHarness.buildClaimWitness ixonEnv (Ix.Claim.check addr none))
let mut targets : Array (String × Address) := #[]
for arg in nameArgs do
match Ix.Cli.NameResolve.resolveIxeAddr ixonEnv arg with
Expand All@@ -186,16 +181,28 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
IO.eprintln "no requested constants were found in the env"
return 1

-- Build the env once into a Rust-owned `EnvHandle` and share it
-- across both Phase 1 and Phase 2 loops. Per-target FFI calls
-- reuse the parsed env — no per-call mmap / lazy-index rebuild.
let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with
| .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1
| .ok h => pure h

-- Phase 1: execute every constant (cheap, deterministic structural metrics).
-- Carry each target's address through so phase 2 can rebuild its witness.
-- For full-closure check claims, use `checkAddrWithEnv` against the
-- shared `envHandle`. For `--subject-only` (`buildVerifyConst`), the
-- witness is a small subject-only blob — keep Lean witness +
-- `executeIxVM`.
IO.println "── Phase 1: execute (witness generation) ──"
let mut execed : Array (Result × Address) := #[]
for (label, addr) in targets do
try
let witness ← mkWitness addr
let (res, execSec) ← timed fun _ =>
Aiur.Bytecode.Toplevel.execute compiled.bytecode funIdx
witness.input witness.inputIOBuffer
if subjectOnly then
let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer
else
compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash
match res with
| .error e => IO.eprintln s!" execute {label} failed: {e}"
| .ok (_, _, queryCounts) =>
Expand DownExpand Up@@ -226,9 +233,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
for i in [:ordered.size] do
let (r, addr) := ordered[i]!
try
let witness ← mkWitness addr
let (_, proveSec) ← timed fun _ =>
aiurSystem.prove friParameters funIdx witness.input witness.inputIOBuffer
let (proveRes, proveSec) ← timed fun _ =>
if subjectOnly then
let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
let (claim, proof, ioBuf) :=
aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer
(.ok (claim, proof, ioBuf) :
Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
else
match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle addr.hash with
| .error e => .error e
| .ok (_claimBytes, proof, ioBuf) =>
-- The shared envHandle path doesn't return an `Array G`
-- claim — adapt to the existing benchmark return shape
-- by recomputing the claim digest from the witness's
-- input (Phase 2 doesn't read it).
.ok (#[], proof, ioBuf)
match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with
| .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue
| .ok _ => pure ()
spent := spent + proveSec
IO.println s!" {r.name}: prove={proveSec}s (cumulative {spent}s)"
ordered := ordered.set! i ({ r with proveSec := some proveSec }, addr)
Expand Down
61 changes: 59 additions & 2 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions Cargo.toml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -4,6 +4,7 @@ members = [
"crates/common",
"crates/compile",
"crates/ffi",
"crates/ixvm-codegen",
"crates/ixon",
"crates/kernel",
]
Expand All@@ -27,6 +28,7 @@ license = "MIT OR Apache-2.0"
[workspace.dependencies]
# Internal crates
aiur = { path = "crates/aiur" }
ixvm-codegen = { path = "crates/ixvm-codegen" }
ix-common = { path = "crates/common" }
ix-compile = { path = "crates/compile" }
ixon = { path = "crates/ixon" }
Expand Down
60 changes: 60 additions & 0 deletions Ix/Aiur/Protocol.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -73,6 +73,66 @@ def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
(claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_ixvm"]
private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
@& Bytecode.FunIdx → @& Array G →
(ioData : @& Array (G × Array G)) →
(ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
Array G × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)

/-- IxVM-native prove: same shape as `prove`, but routes execution
through the codegen'd Rust kernel (`execute_generated`) instead
of the bytecode interpreter. The resulting `Proof` is
verification-compatible with one from `prove`. Only valid when
`system.toplevel` is the IxVM kernel's bytecode. -/
def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
(funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
Array G × Proof × IOBuffer :=
let ioData := ioBuffer.data.toArray
let ioMap := ioBuffer.map.toArray
let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
ioData ioMap
let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
(claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_addr_with_env"]
private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
Except String (ByteArray × Proof ×
Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-claim prove against a Rust-owned `EnvHandle`. Returns
`(claimBytes, proof, ioBuffer)` — Rust serializes the
reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
deserialize directly without re-running the closure walk. -/
def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
(funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
Except String (ByteArray × Proof × IOBuffer) :=
match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
| .error e => .error e
| .ok (claimBytes, proof, ioData, ioMap) =>
let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
.ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
Except String (ByteArray × Proof ×
Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
(funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
Except String (ByteArray × Proof × IOBuffer) :=
match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
| .error e => .error e
| .ok (claimBytes, proof, ioData, ioMap) =>
let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
.ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem → @& FriParameters →
@& Array G → @& Proof → Except String Unit
Expand Down
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
IxVM: native execution pipeline#463

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

 Merged

arthurpaulino
merged 10 commits into

from

Jul 3, 2026
 Merged


IxVM: native execution pipeline
#463
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
0cec144

Aiur Bytecode → Rust codegen for the IxVM kernel


arthurpaulino Jun 30, 2026
aedbf85

Move shard witness construction to Rust + parallelise


arthurpaulino Jun 30, 2026
c9ffd70

Codegen: value-returning byte ops, dead-fold the unconstrained


arthurpaulino Jun 30, 2026
c6c86a6

Wire Rust witness fast path through every check/prove entry point


arthurpaulino Jun 30, 2026
e7b37f7

EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls


arthurpaulino Jun 30, 2026
899d212

ix codegen: add --check flag for CI; gate stale generated kernel


arthurpaulino Jun 30, 2026
56a7ab8

ix check: --interp {source|bytecode} to bypass codegen kernel


arthurpaulino Jul 1, 2026
33ad65a

IxVM codegen: regen + rebase-fixups after KLevel port


arthurpaulino Jul 2, 2026
9d17f9f

ix-check + ixvm tests: coverage gate, --interp source fix, codegen pa…


arthurpaulino Jul 3, 2026
033968c

cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception


arthurpaulino Jul 3, 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


2 changes: 2 additions & 0 deletions
.github/workflows/ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -27,6 +27,8 @@ jobs:
 # lean-action builds above — fails CI.
 - name: Build all targets
 run: lake lint -- --wfail -v
 - name: Check codegen'd IxVM kernel is up to date
 run: lake exe ix codegen --check
 - name: Test Ix CLI
 run: lake test --wfail -- cli
 - name: Aiur tests
Expand Down

4 changes: 3 additions & 1 deletion
Benchmarks/IxVM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -34,7 +34,9 @@ def main : IO Unit := do

 let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
 throughput (.Elements n.toUInt64 "consts")
 -- IxVM-native prove: routes execution through the codegen'd Rust
 -- kernel (`execute_generated`) instead of the bytecode interpreter.
 bench "serde/blake3 Nat.add_comm"
 (aiurSystem.prove friParameters funIdx #[.ofNat n])
 (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
 ioBuffer
 return

47 changes: 35 additions & 12 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -172,11 +172,6 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 | .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1
 | .ok env => pure env
 IO.println s!"Loaded {ixePath}: {ixonEnv.namedCount} named, {ixonEnv.constCount} consts"
 -- Build the witness for `addr`: subject-only (`verify_const`) trusts deps;
 -- otherwise the full-closure check (`verify_claim`, `check addr none`).
 let mkWitness (addr : Address) : IO IxVM.ClaimHarness.ClaimWitness :=
 if subjectOnly then pure (IxVM.ClaimHarness.buildVerifyConst ixonEnv addr)
 else IO.ofExcept (IxVM.ClaimHarness.buildClaimWitness ixonEnv (Ix.Claim.check addr none))
 let mut targets : Array (String × Address) := #[]
 for arg in nameArgs do
 match Ix.Cli.NameResolve.resolveIxeAddr ixonEnv arg with
Expand All@@ -186,16 +181,28 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 IO.eprintln "no requested constants were found in the env"
 return 1

 -- Build the env once into a Rust-owned `EnvHandle` and share it
 -- across both Phase 1 and Phase 2 loops. Per-target FFI calls
 -- reuse the parsed env — no per-call mmap / lazy-index rebuild.
 let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with
 | .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1
 | .ok h => pure h

 -- Phase 1: execute every constant (cheap, deterministic structural metrics).
 -- Carry each target's address through so phase 2 can rebuild its witness.
 -- For full-closure check claims, use `checkAddrWithEnv` against the
 -- shared `envHandle`. For `--subject-only` (`buildVerifyConst`), the
 -- witness is a small subject-only blob — keep Lean witness +
 -- `executeIxVM`.
 IO.println "── Phase 1: execute (witness generation) ──"
 let mut execed : Array (Result × Address) := #[]
 for (label, addr) in targets do
 try
 let witness ← mkWitness addr
 let (res, execSec) ← timed fun _ =>
 Aiur.Bytecode.Toplevel.execute compiled.bytecode funIdx
 witness.input witness.inputIOBuffer
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer
 else
 compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash
 match res with
 | .error e => IO.eprintln s!" execute {label} failed: {e}"
 | .ok (_, _, queryCounts) =>
Expand DownExpand Up@@ -226,9 +233,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 for i in [:ordered.size] do
 let (r, addr) := ordered[i]!
 try
 let witness ← mkWitness addr
 let (_, proveSec) ← timed fun _ =>
 aiurSystem.prove friParameters funIdx witness.input witness.inputIOBuffer
 let (proveRes, proveSec) ← timed fun _ =>
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 let (claim, proof, ioBuf) :=
 aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer
 (.ok (claim, proof, ioBuf) :
 Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
 else
 match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle addr.hash with
 | .error e => .error e
 | .ok (_claimBytes, proof, ioBuf) =>
 -- The shared envHandle path doesn't return an `Array G`
 -- claim — adapt to the existing benchmark return shape
 -- by recomputing the claim digest from the witness's
 -- input (Phase 2 doesn't read it).
 .ok (#[], proof, ioBuf)
 match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with
 | .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue
 | .ok _ => pure ()
 spent := spent + proveSec
 IO.println s!" {r.name}: prove={proveSec}s (cumulative {spent}s)"
 ordered := ordered.set! i ({ r with proveSec := some proveSec }, addr)
Expand Down

61 changes: 59 additions & 2 deletions
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


2 changes: 2 additions & 0 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -4,6 +4,7 @@ members = [
 "crates/common",
 "crates/compile",
 "crates/ffi",
 "crates/ixvm-codegen",
 "crates/ixon",
 "crates/kernel",
]
Expand All@@ -27,6 +28,7 @@ license = "MIT OR Apache-2.0"
[workspace.dependencies]
# Internal crates
aiur = { path = "crates/aiur" }
ixvm-codegen = { path = "crates/ixvm-codegen" }
ix-common = { path = "crates/common" }
ix-compile = { path = "crates/compile" }
ixon = { path = "crates/ixon" }
Expand Down

60 changes: 60 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -73,6 +73,66 @@ def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_ixvm"]
private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& Array G →
 (ioData : @& Array (G × Array G)) →
 (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
 Array G × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)

/-- IxVM-native prove: same shape as `prove`, but routes execution
 through the codegen'd Rust kernel (`execute_generated`) instead
 of the bytecode interpreter. The resulting `Proof` is
 verification-compatible with one from `prove`. Only valid when
 `system.toplevel` is the IxVM kernel's bytecode. -/
def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
 Array G × Proof × IOBuffer :=
 let ioData := ioBuffer.data.toArray
 let ioMap := ioBuffer.map.toArray
 let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
 ioData ioMap
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_addr_with_env"]
private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-claim prove against a Rust-owned `EnvHandle`. Returns
 `(claimBytes, proof, ioBuffer)` — Rust serializes the
 reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
 deserialize directly without re-running the closure walk. -/
def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem → @& FriParameters →
 @& Array G → @& Proof → Except String Unit
Expand Down
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
IxVM: native execution pipeline#463

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

 Merged

arthurpaulino
merged 10 commits into

from

Jul 3, 2026
 Merged


IxVM: native execution pipeline
#463
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
0cec144

Aiur Bytecode → Rust codegen for the IxVM kernel


arthurpaulino Jun 30, 2026
aedbf85

Move shard witness construction to Rust + parallelise


arthurpaulino Jun 30, 2026
c9ffd70

Codegen: value-returning byte ops, dead-fold the unconstrained


arthurpaulino Jun 30, 2026
c6c86a6

Wire Rust witness fast path through every check/prove entry point


arthurpaulino Jun 30, 2026
e7b37f7

EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls


arthurpaulino Jun 30, 2026
899d212

ix codegen: add --check flag for CI; gate stale generated kernel


arthurpaulino Jun 30, 2026
56a7ab8

ix check: --interp {source|bytecode} to bypass codegen kernel


arthurpaulino Jul 1, 2026
33ad65a

IxVM codegen: regen + rebase-fixups after KLevel port


arthurpaulino Jul 2, 2026
9d17f9f

ix-check + ixvm tests: coverage gate, --interp source fix, codegen pa…


arthurpaulino Jul 3, 2026
033968c

cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception


arthurpaulino Jul 3, 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


2 changes: 2 additions & 0 deletions
.github/workflows/ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -27,6 +27,8 @@ jobs:
 # lean-action builds above — fails CI.
 - name: Build all targets
 run: lake lint -- --wfail -v
 - name: Check codegen'd IxVM kernel is up to date
 run: lake exe ix codegen --check
 - name: Test Ix CLI
 run: lake test --wfail -- cli
 - name: Aiur tests
Expand Down

4 changes: 3 additions & 1 deletion
Benchmarks/IxVM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -34,7 +34,9 @@ def main : IO Unit := do

 let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
 throughput (.Elements n.toUInt64 "consts")
 -- IxVM-native prove: routes execution through the codegen'd Rust
 -- kernel (`execute_generated`) instead of the bytecode interpreter.
 bench "serde/blake3 Nat.add_comm"
 (aiurSystem.prove friParameters funIdx #[.ofNat n])
 (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
 ioBuffer
 return

47 changes: 35 additions & 12 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -172,11 +172,6 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 | .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1
 | .ok env => pure env
 IO.println s!"Loaded {ixePath}: {ixonEnv.namedCount} named, {ixonEnv.constCount} consts"
 -- Build the witness for `addr`: subject-only (`verify_const`) trusts deps;
 -- otherwise the full-closure check (`verify_claim`, `check addr none`).
 let mkWitness (addr : Address) : IO IxVM.ClaimHarness.ClaimWitness :=
 if subjectOnly then pure (IxVM.ClaimHarness.buildVerifyConst ixonEnv addr)
 else IO.ofExcept (IxVM.ClaimHarness.buildClaimWitness ixonEnv (Ix.Claim.check addr none))
 let mut targets : Array (String × Address) := #[]
 for arg in nameArgs do
 match Ix.Cli.NameResolve.resolveIxeAddr ixonEnv arg with
Expand All@@ -186,16 +181,28 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 IO.eprintln "no requested constants were found in the env"
 return 1

 -- Build the env once into a Rust-owned `EnvHandle` and share it
 -- across both Phase 1 and Phase 2 loops. Per-target FFI calls
 -- reuse the parsed env — no per-call mmap / lazy-index rebuild.
 let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with
 | .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1
 | .ok h => pure h

 -- Phase 1: execute every constant (cheap, deterministic structural metrics).
 -- Carry each target's address through so phase 2 can rebuild its witness.
 -- For full-closure check claims, use `checkAddrWithEnv` against the
 -- shared `envHandle`. For `--subject-only` (`buildVerifyConst`), the
 -- witness is a small subject-only blob — keep Lean witness +
 -- `executeIxVM`.
 IO.println "── Phase 1: execute (witness generation) ──"
 let mut execed : Array (Result × Address) := #[]
 for (label, addr) in targets do
 try
 let witness ← mkWitness addr
 let (res, execSec) ← timed fun _ =>
 Aiur.Bytecode.Toplevel.execute compiled.bytecode funIdx
 witness.input witness.inputIOBuffer
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer
 else
 compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash
 match res with
 | .error e => IO.eprintln s!" execute {label} failed: {e}"
 | .ok (_, _, queryCounts) =>
Expand DownExpand Up@@ -226,9 +233,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 for i in [:ordered.size] do
 let (r, addr) := ordered[i]!
 try
 let witness ← mkWitness addr
 let (_, proveSec) ← timed fun _ =>
 aiurSystem.prove friParameters funIdx witness.input witness.inputIOBuffer
 let (proveRes, proveSec) ← timed fun _ =>
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 let (claim, proof, ioBuf) :=
 aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer
 (.ok (claim, proof, ioBuf) :
 Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
 else
 match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle addr.hash with
 | .error e => .error e
 | .ok (_claimBytes, proof, ioBuf) =>
 -- The shared envHandle path doesn't return an `Array G`
 -- claim — adapt to the existing benchmark return shape
 -- by recomputing the claim digest from the witness's
 -- input (Phase 2 doesn't read it).
 .ok (#[], proof, ioBuf)
 match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with
 | .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue
 | .ok _ => pure ()
 spent := spent + proveSec
 IO.println s!" {r.name}: prove={proveSec}s (cumulative {spent}s)"
 ordered := ordered.set! i ({ r with proveSec := some proveSec }, addr)
Expand Down

61 changes: 59 additions & 2 deletions
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


2 changes: 2 additions & 0 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -4,6 +4,7 @@ members = [
 "crates/common",
 "crates/compile",
 "crates/ffi",
 "crates/ixvm-codegen",
 "crates/ixon",
 "crates/kernel",
]
Expand All@@ -27,6 +28,7 @@ license = "MIT OR Apache-2.0"
[workspace.dependencies]
# Internal crates
aiur = { path = "crates/aiur" }
ixvm-codegen = { path = "crates/ixvm-codegen" }
ix-common = { path = "crates/common" }
ix-compile = { path = "crates/compile" }
ixon = { path = "crates/ixon" }
Expand Down

60 changes: 60 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -73,6 +73,66 @@ def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_ixvm"]
private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& Array G →
 (ioData : @& Array (G × Array G)) →
 (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
 Array G × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)

/-- IxVM-native prove: same shape as `prove`, but routes execution
 through the codegen'd Rust kernel (`execute_generated`) instead
 of the bytecode interpreter. The resulting `Proof` is
 verification-compatible with one from `prove`. Only valid when
 `system.toplevel` is the IxVM kernel's bytecode. -/
def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
 Array G × Proof × IOBuffer :=
 let ioData := ioBuffer.data.toArray
 let ioMap := ioBuffer.map.toArray
 let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
 ioData ioMap
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_addr_with_env"]
private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-claim prove against a Rust-owned `EnvHandle`. Returns
 `(claimBytes, proof, ioBuffer)` — Rust serializes the
 reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
 deserialize directly without re-running the closure walk. -/
def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem → @& FriParameters →
 @& Array G → @& Proof → Except String Unit
Expand Down
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
IxVM: native execution pipeline#463

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

 Merged

arthurpaulino
merged 10 commits into

from

Jul 3, 2026
 Merged


IxVM: native execution pipeline
#463
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
0cec144

Aiur Bytecode → Rust codegen for the IxVM kernel


arthurpaulino Jun 30, 2026
aedbf85

Move shard witness construction to Rust + parallelise


arthurpaulino Jun 30, 2026
c9ffd70

Codegen: value-returning byte ops, dead-fold the unconstrained


arthurpaulino Jun 30, 2026
c6c86a6

Wire Rust witness fast path through every check/prove entry point


arthurpaulino Jun 30, 2026
e7b37f7

EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls


arthurpaulino Jun 30, 2026
899d212

ix codegen: add --check flag for CI; gate stale generated kernel


arthurpaulino Jun 30, 2026
56a7ab8

ix check: --interp {source|bytecode} to bypass codegen kernel


arthurpaulino Jul 1, 2026
33ad65a

IxVM codegen: regen + rebase-fixups after KLevel port


arthurpaulino Jul 2, 2026
9d17f9f

ix-check + ixvm tests: coverage gate, --interp source fix, codegen pa…


arthurpaulino Jul 3, 2026
033968c

cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception


arthurpaulino Jul 3, 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


2 changes: 2 additions & 0 deletions
.github/workflows/ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -27,6 +27,8 @@ jobs:
 # lean-action builds above — fails CI.
 - name: Build all targets
 run: lake lint -- --wfail -v
 - name: Check codegen'd IxVM kernel is up to date
 run: lake exe ix codegen --check
 - name: Test Ix CLI
 run: lake test --wfail -- cli
 - name: Aiur tests
Expand Down

4 changes: 3 additions & 1 deletion
Benchmarks/IxVM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -34,7 +34,9 @@ def main : IO Unit := do

 let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
 throughput (.Elements n.toUInt64 "consts")
 -- IxVM-native prove: routes execution through the codegen'd Rust
 -- kernel (`execute_generated`) instead of the bytecode interpreter.
 bench "serde/blake3 Nat.add_comm"
 (aiurSystem.prove friParameters funIdx #[.ofNat n])
 (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
 ioBuffer
 return

47 changes: 35 additions & 12 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -172,11 +172,6 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 | .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1
 | .ok env => pure env
 IO.println s!"Loaded {ixePath}: {ixonEnv.namedCount} named, {ixonEnv.constCount} consts"
 -- Build the witness for `addr`: subject-only (`verify_const`) trusts deps;
 -- otherwise the full-closure check (`verify_claim`, `check addr none`).
 let mkWitness (addr : Address) : IO IxVM.ClaimHarness.ClaimWitness :=
 if subjectOnly then pure (IxVM.ClaimHarness.buildVerifyConst ixonEnv addr)
 else IO.ofExcept (IxVM.ClaimHarness.buildClaimWitness ixonEnv (Ix.Claim.check addr none))
 let mut targets : Array (String × Address) := #[]
 for arg in nameArgs do
 match Ix.Cli.NameResolve.resolveIxeAddr ixonEnv arg with
Expand All@@ -186,16 +181,28 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 IO.eprintln "no requested constants were found in the env"
 return 1

 -- Build the env once into a Rust-owned `EnvHandle` and share it
 -- across both Phase 1 and Phase 2 loops. Per-target FFI calls
 -- reuse the parsed env — no per-call mmap / lazy-index rebuild.
 let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with
 | .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1
 | .ok h => pure h

 -- Phase 1: execute every constant (cheap, deterministic structural metrics).
 -- Carry each target's address through so phase 2 can rebuild its witness.
 -- For full-closure check claims, use `checkAddrWithEnv` against the
 -- shared `envHandle`. For `--subject-only` (`buildVerifyConst`), the
 -- witness is a small subject-only blob — keep Lean witness +
 -- `executeIxVM`.
 IO.println "── Phase 1: execute (witness generation) ──"
 let mut execed : Array (Result × Address) := #[]
 for (label, addr) in targets do
 try
 let witness ← mkWitness addr
 let (res, execSec) ← timed fun _ =>
 Aiur.Bytecode.Toplevel.execute compiled.bytecode funIdx
 witness.input witness.inputIOBuffer
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer
 else
 compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash
 match res with
 | .error e => IO.eprintln s!" execute {label} failed: {e}"
 | .ok (_, _, queryCounts) =>
Expand DownExpand Up@@ -226,9 +233,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 for i in [:ordered.size] do
 let (r, addr) := ordered[i]!
 try
 let witness ← mkWitness addr
 let (_, proveSec) ← timed fun _ =>
 aiurSystem.prove friParameters funIdx witness.input witness.inputIOBuffer
 let (proveRes, proveSec) ← timed fun _ =>
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 let (claim, proof, ioBuf) :=
 aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer
 (.ok (claim, proof, ioBuf) :
 Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
 else
 match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle addr.hash with
 | .error e => .error e
 | .ok (_claimBytes, proof, ioBuf) =>
 -- The shared envHandle path doesn't return an `Array G`
 -- claim — adapt to the existing benchmark return shape
 -- by recomputing the claim digest from the witness's
 -- input (Phase 2 doesn't read it).
 .ok (#[], proof, ioBuf)
 match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with
 | .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue
 | .ok _ => pure ()
 spent := spent + proveSec
 IO.println s!" {r.name}: prove={proveSec}s (cumulative {spent}s)"
 ordered := ordered.set! i ({ r with proveSec := some proveSec }, addr)
Expand Down

61 changes: 59 additions & 2 deletions
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


2 changes: 2 additions & 0 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -4,6 +4,7 @@ members = [
 "crates/common",
 "crates/compile",
 "crates/ffi",
 "crates/ixvm-codegen",
 "crates/ixon",
 "crates/kernel",
]
Expand All@@ -27,6 +28,7 @@ license = "MIT OR Apache-2.0"
[workspace.dependencies]
# Internal crates
aiur = { path = "crates/aiur" }
ixvm-codegen = { path = "crates/ixvm-codegen" }
ix-common = { path = "crates/common" }
ix-compile = { path = "crates/compile" }
ixon = { path = "crates/ixon" }
Expand Down

60 changes: 60 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -73,6 +73,66 @@ def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_ixvm"]
private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& Array G →
 (ioData : @& Array (G × Array G)) →
 (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
 Array G × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)

/-- IxVM-native prove: same shape as `prove`, but routes execution
 through the codegen'd Rust kernel (`execute_generated`) instead
 of the bytecode interpreter. The resulting `Proof` is
 verification-compatible with one from `prove`. Only valid when
 `system.toplevel` is the IxVM kernel's bytecode. -/
def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
 Array G × Proof × IOBuffer :=
 let ioData := ioBuffer.data.toArray
 let ioMap := ioBuffer.map.toArray
 let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
 ioData ioMap
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_addr_with_env"]
private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-claim prove against a Rust-owned `EnvHandle`. Returns
 `(claimBytes, proof, ioBuffer)` — Rust serializes the
 reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
 deserialize directly without re-running the closure walk. -/
def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem → @& FriParameters →
 @& Array G → @& Proof → Except String Unit
Expand Down
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
IxVM: native execution pipeline#463

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

 Merged

arthurpaulino
merged 10 commits into

from

Jul 3, 2026
 Merged


IxVM: native execution pipeline
#463
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
0cec144

Aiur Bytecode → Rust codegen for the IxVM kernel


arthurpaulino Jun 30, 2026
aedbf85

Move shard witness construction to Rust + parallelise


arthurpaulino Jun 30, 2026
c9ffd70

Codegen: value-returning byte ops, dead-fold the unconstrained


arthurpaulino Jun 30, 2026
c6c86a6

Wire Rust witness fast path through every check/prove entry point


arthurpaulino Jun 30, 2026
e7b37f7

EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls


arthurpaulino Jun 30, 2026
899d212

ix codegen: add --check flag for CI; gate stale generated kernel


arthurpaulino Jun 30, 2026
56a7ab8

ix check: --interp {source|bytecode} to bypass codegen kernel


arthurpaulino Jul 1, 2026
33ad65a

IxVM codegen: regen + rebase-fixups after KLevel port


arthurpaulino Jul 2, 2026
9d17f9f

ix-check + ixvm tests: coverage gate, --interp source fix, codegen pa…


arthurpaulino Jul 3, 2026
033968c

cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception


arthurpaulino Jul 3, 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


2 changes: 2 additions & 0 deletions
.github/workflows/ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -27,6 +27,8 @@ jobs:
 # lean-action builds above — fails CI.
 - name: Build all targets
 run: lake lint -- --wfail -v
 - name: Check codegen'd IxVM kernel is up to date
 run: lake exe ix codegen --check
 - name: Test Ix CLI
 run: lake test --wfail -- cli
 - name: Aiur tests
Expand Down

4 changes: 3 additions & 1 deletion
Benchmarks/IxVM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -34,7 +34,9 @@ def main : IO Unit := do

 let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
 throughput (.Elements n.toUInt64 "consts")
 -- IxVM-native prove: routes execution through the codegen'd Rust
 -- kernel (`execute_generated`) instead of the bytecode interpreter.
 bench "serde/blake3 Nat.add_comm"
 (aiurSystem.prove friParameters funIdx #[.ofNat n])
 (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
 ioBuffer
 return

47 changes: 35 additions & 12 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -172,11 +172,6 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 | .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1
 | .ok env => pure env
 IO.println s!"Loaded {ixePath}: {ixonEnv.namedCount} named, {ixonEnv.constCount} consts"
 -- Build the witness for `addr`: subject-only (`verify_const`) trusts deps;
 -- otherwise the full-closure check (`verify_claim`, `check addr none`).
 let mkWitness (addr : Address) : IO IxVM.ClaimHarness.ClaimWitness :=
 if subjectOnly then pure (IxVM.ClaimHarness.buildVerifyConst ixonEnv addr)
 else IO.ofExcept (IxVM.ClaimHarness.buildClaimWitness ixonEnv (Ix.Claim.check addr none))
 let mut targets : Array (String × Address) := #[]
 for arg in nameArgs do
 match Ix.Cli.NameResolve.resolveIxeAddr ixonEnv arg with
Expand All@@ -186,16 +181,28 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 IO.eprintln "no requested constants were found in the env"
 return 1

 -- Build the env once into a Rust-owned `EnvHandle` and share it
 -- across both Phase 1 and Phase 2 loops. Per-target FFI calls
 -- reuse the parsed env — no per-call mmap / lazy-index rebuild.
 let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with
 | .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1
 | .ok h => pure h

 -- Phase 1: execute every constant (cheap, deterministic structural metrics).
 -- Carry each target's address through so phase 2 can rebuild its witness.
 -- For full-closure check claims, use `checkAddrWithEnv` against the
 -- shared `envHandle`. For `--subject-only` (`buildVerifyConst`), the
 -- witness is a small subject-only blob — keep Lean witness +
 -- `executeIxVM`.
 IO.println "── Phase 1: execute (witness generation) ──"
 let mut execed : Array (Result × Address) := #[]
 for (label, addr) in targets do
 try
 let witness ← mkWitness addr
 let (res, execSec) ← timed fun _ =>
 Aiur.Bytecode.Toplevel.execute compiled.bytecode funIdx
 witness.input witness.inputIOBuffer
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer
 else
 compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash
 match res with
 | .error e => IO.eprintln s!" execute {label} failed: {e}"
 | .ok (_, _, queryCounts) =>
Expand DownExpand Up@@ -226,9 +233,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 for i in [:ordered.size] do
 let (r, addr) := ordered[i]!
 try
 let witness ← mkWitness addr
 let (_, proveSec) ← timed fun _ =>
 aiurSystem.prove friParameters funIdx witness.input witness.inputIOBuffer
 let (proveRes, proveSec) ← timed fun _ =>
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 let (claim, proof, ioBuf) :=
 aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer
 (.ok (claim, proof, ioBuf) :
 Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
 else
 match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle addr.hash with
 | .error e => .error e
 | .ok (_claimBytes, proof, ioBuf) =>
 -- The shared envHandle path doesn't return an `Array G`
 -- claim — adapt to the existing benchmark return shape
 -- by recomputing the claim digest from the witness's
 -- input (Phase 2 doesn't read it).
 .ok (#[], proof, ioBuf)
 match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with
 | .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue
 | .ok _ => pure ()
 spent := spent + proveSec
 IO.println s!" {r.name}: prove={proveSec}s (cumulative {spent}s)"
 ordered := ordered.set! i ({ r with proveSec := some proveSec }, addr)
Expand Down

61 changes: 59 additions & 2 deletions
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


2 changes: 2 additions & 0 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -4,6 +4,7 @@ members = [
 "crates/common",
 "crates/compile",
 "crates/ffi",
 "crates/ixvm-codegen",
 "crates/ixon",
 "crates/kernel",
]
Expand All@@ -27,6 +28,7 @@ license = "MIT OR Apache-2.0"
[workspace.dependencies]
# Internal crates
aiur = { path = "crates/aiur" }
ixvm-codegen = { path = "crates/ixvm-codegen" }
ix-common = { path = "crates/common" }
ix-compile = { path = "crates/compile" }
ixon = { path = "crates/ixon" }
Expand Down

60 changes: 60 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -73,6 +73,66 @@ def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_ixvm"]
private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& Array G →
 (ioData : @& Array (G × Array G)) →
 (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
 Array G × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)

/-- IxVM-native prove: same shape as `prove`, but routes execution
 through the codegen'd Rust kernel (`execute_generated`) instead
 of the bytecode interpreter. The resulting `Proof` is
 verification-compatible with one from `prove`. Only valid when
 `system.toplevel` is the IxVM kernel's bytecode. -/
def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
 Array G × Proof × IOBuffer :=
 let ioData := ioBuffer.data.toArray
 let ioMap := ioBuffer.map.toArray
 let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
 ioData ioMap
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_addr_with_env"]
private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-claim prove against a Rust-owned `EnvHandle`. Returns
 `(claimBytes, proof, ioBuffer)` — Rust serializes the
 reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
 deserialize directly without re-running the closure walk. -/
def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem → @& FriParameters →
 @& Array G → @& Proof → Except String Unit
Expand Down
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
IxVM: native execution pipeline#463

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

 Merged

arthurpaulino
merged 10 commits into

from

Jul 3, 2026
 Merged


IxVM: native execution pipeline
#463
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
0cec144

Aiur Bytecode → Rust codegen for the IxVM kernel


arthurpaulino Jun 30, 2026
aedbf85

Move shard witness construction to Rust + parallelise


arthurpaulino Jun 30, 2026
c9ffd70

Codegen: value-returning byte ops, dead-fold the unconstrained


arthurpaulino Jun 30, 2026
c6c86a6

Wire Rust witness fast path through every check/prove entry point


arthurpaulino Jun 30, 2026
e7b37f7

EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls


arthurpaulino Jun 30, 2026
899d212

ix codegen: add --check flag for CI; gate stale generated kernel


arthurpaulino Jun 30, 2026
56a7ab8

ix check: --interp {source|bytecode} to bypass codegen kernel


arthurpaulino Jul 1, 2026
33ad65a

IxVM codegen: regen + rebase-fixups after KLevel port


arthurpaulino Jul 2, 2026
9d17f9f

ix-check + ixvm tests: coverage gate, --interp source fix, codegen pa…


arthurpaulino Jul 3, 2026
033968c

cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception


arthurpaulino Jul 3, 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


2 changes: 2 additions & 0 deletions
.github/workflows/ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -27,6 +27,8 @@ jobs:
 # lean-action builds above — fails CI.
 - name: Build all targets
 run: lake lint -- --wfail -v
 - name: Check codegen'd IxVM kernel is up to date
 run: lake exe ix codegen --check
 - name: Test Ix CLI
 run: lake test --wfail -- cli
 - name: Aiur tests
Expand Down

4 changes: 3 additions & 1 deletion
Benchmarks/IxVM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -34,7 +34,9 @@ def main : IO Unit := do

 let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
 throughput (.Elements n.toUInt64 "consts")
 -- IxVM-native prove: routes execution through the codegen'd Rust
 -- kernel (`execute_generated`) instead of the bytecode interpreter.
 bench "serde/blake3 Nat.add_comm"
 (aiurSystem.prove friParameters funIdx #[.ofNat n])
 (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
 ioBuffer
 return

47 changes: 35 additions & 12 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -172,11 +172,6 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 | .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1
 | .ok env => pure env
 IO.println s!"Loaded {ixePath}: {ixonEnv.namedCount} named, {ixonEnv.constCount} consts"
 -- Build the witness for `addr`: subject-only (`verify_const`) trusts deps;
 -- otherwise the full-closure check (`verify_claim`, `check addr none`).
 let mkWitness (addr : Address) : IO IxVM.ClaimHarness.ClaimWitness :=
 if subjectOnly then pure (IxVM.ClaimHarness.buildVerifyConst ixonEnv addr)
 else IO.ofExcept (IxVM.ClaimHarness.buildClaimWitness ixonEnv (Ix.Claim.check addr none))
 let mut targets : Array (String × Address) := #[]
 for arg in nameArgs do
 match Ix.Cli.NameResolve.resolveIxeAddr ixonEnv arg with
Expand All@@ -186,16 +181,28 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 IO.eprintln "no requested constants were found in the env"
 return 1

 -- Build the env once into a Rust-owned `EnvHandle` and share it
 -- across both Phase 1 and Phase 2 loops. Per-target FFI calls
 -- reuse the parsed env — no per-call mmap / lazy-index rebuild.
 let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with
 | .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1
 | .ok h => pure h

 -- Phase 1: execute every constant (cheap, deterministic structural metrics).
 -- Carry each target's address through so phase 2 can rebuild its witness.
 -- For full-closure check claims, use `checkAddrWithEnv` against the
 -- shared `envHandle`. For `--subject-only` (`buildVerifyConst`), the
 -- witness is a small subject-only blob — keep Lean witness +
 -- `executeIxVM`.
 IO.println "── Phase 1: execute (witness generation) ──"
 let mut execed : Array (Result × Address) := #[]
 for (label, addr) in targets do
 try
 let witness ← mkWitness addr
 let (res, execSec) ← timed fun _ =>
 Aiur.Bytecode.Toplevel.execute compiled.bytecode funIdx
 witness.input witness.inputIOBuffer
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer
 else
 compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash
 match res with
 | .error e => IO.eprintln s!" execute {label} failed: {e}"
 | .ok (_, _, queryCounts) =>
Expand DownExpand Up@@ -226,9 +233,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 for i in [:ordered.size] do
 let (r, addr) := ordered[i]!
 try
 let witness ← mkWitness addr
 let (_, proveSec) ← timed fun _ =>
 aiurSystem.prove friParameters funIdx witness.input witness.inputIOBuffer
 let (proveRes, proveSec) ← timed fun _ =>
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 let (claim, proof, ioBuf) :=
 aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer
 (.ok (claim, proof, ioBuf) :
 Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
 else
 match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle addr.hash with
 | .error e => .error e
 | .ok (_claimBytes, proof, ioBuf) =>
 -- The shared envHandle path doesn't return an `Array G`
 -- claim — adapt to the existing benchmark return shape
 -- by recomputing the claim digest from the witness's
 -- input (Phase 2 doesn't read it).
 .ok (#[], proof, ioBuf)
 match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with
 | .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue
 | .ok _ => pure ()
 spent := spent + proveSec
 IO.println s!" {r.name}: prove={proveSec}s (cumulative {spent}s)"
 ordered := ordered.set! i ({ r with proveSec := some proveSec }, addr)
Expand Down

61 changes: 59 additions & 2 deletions
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


2 changes: 2 additions & 0 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -4,6 +4,7 @@ members = [
 "crates/common",
 "crates/compile",
 "crates/ffi",
 "crates/ixvm-codegen",
 "crates/ixon",
 "crates/kernel",
]
Expand All@@ -27,6 +28,7 @@ license = "MIT OR Apache-2.0"
[workspace.dependencies]
# Internal crates
aiur = { path = "crates/aiur" }
ixvm-codegen = { path = "crates/ixvm-codegen" }
ix-common = { path = "crates/common" }
ix-compile = { path = "crates/compile" }
ixon = { path = "crates/ixon" }
Expand Down

60 changes: 60 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -73,6 +73,66 @@ def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_ixvm"]
private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& Array G →
 (ioData : @& Array (G × Array G)) →
 (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
 Array G × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)

/-- IxVM-native prove: same shape as `prove`, but routes execution
 through the codegen'd Rust kernel (`execute_generated`) instead
 of the bytecode interpreter. The resulting `Proof` is
 verification-compatible with one from `prove`. Only valid when
 `system.toplevel` is the IxVM kernel's bytecode. -/
def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
 Array G × Proof × IOBuffer :=
 let ioData := ioBuffer.data.toArray
 let ioMap := ioBuffer.map.toArray
 let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
 ioData ioMap
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_addr_with_env"]
private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-claim prove against a Rust-owned `EnvHandle`. Returns
 `(claimBytes, proof, ioBuffer)` — Rust serializes the
 reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
 deserialize directly without re-running the closure walk. -/
def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem → @& FriParameters →
 @& Array G → @& Proof → Except String Unit
Expand Down
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
IxVM: native execution pipeline#463

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

 Merged

arthurpaulino
merged 10 commits into

from

Jul 3, 2026
 Merged


IxVM: native execution pipeline
#463
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
0cec144

Aiur Bytecode → Rust codegen for the IxVM kernel


arthurpaulino Jun 30, 2026
aedbf85

Move shard witness construction to Rust + parallelise


arthurpaulino Jun 30, 2026
c9ffd70

Codegen: value-returning byte ops, dead-fold the unconstrained


arthurpaulino Jun 30, 2026
c6c86a6

Wire Rust witness fast path through every check/prove entry point


arthurpaulino Jun 30, 2026
e7b37f7

EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls


arthurpaulino Jun 30, 2026
899d212

ix codegen: add --check flag for CI; gate stale generated kernel


arthurpaulino Jun 30, 2026
56a7ab8

ix check: --interp {source|bytecode} to bypass codegen kernel


arthurpaulino Jul 1, 2026
33ad65a

IxVM codegen: regen + rebase-fixups after KLevel port


arthurpaulino Jul 2, 2026
9d17f9f

ix-check + ixvm tests: coverage gate, --interp source fix, codegen pa…


arthurpaulino Jul 3, 2026
033968c

cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception


arthurpaulino Jul 3, 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


2 changes: 2 additions & 0 deletions
.github/workflows/ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -27,6 +27,8 @@ jobs:
 # lean-action builds above — fails CI.
 - name: Build all targets
 run: lake lint -- --wfail -v
 - name: Check codegen'd IxVM kernel is up to date
 run: lake exe ix codegen --check
 - name: Test Ix CLI
 run: lake test --wfail -- cli
 - name: Aiur tests
Expand Down

4 changes: 3 additions & 1 deletion
Benchmarks/IxVM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -34,7 +34,9 @@ def main : IO Unit := do

 let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
 throughput (.Elements n.toUInt64 "consts")
 -- IxVM-native prove: routes execution through the codegen'd Rust
 -- kernel (`execute_generated`) instead of the bytecode interpreter.
 bench "serde/blake3 Nat.add_comm"
 (aiurSystem.prove friParameters funIdx #[.ofNat n])
 (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
 ioBuffer
 return

47 changes: 35 additions & 12 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -172,11 +172,6 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 | .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1
 | .ok env => pure env
 IO.println s!"Loaded {ixePath}: {ixonEnv.namedCount} named, {ixonEnv.constCount} consts"
 -- Build the witness for `addr`: subject-only (`verify_const`) trusts deps;
 -- otherwise the full-closure check (`verify_claim`, `check addr none`).
 let mkWitness (addr : Address) : IO IxVM.ClaimHarness.ClaimWitness :=
 if subjectOnly then pure (IxVM.ClaimHarness.buildVerifyConst ixonEnv addr)
 else IO.ofExcept (IxVM.ClaimHarness.buildClaimWitness ixonEnv (Ix.Claim.check addr none))
 let mut targets : Array (String × Address) := #[]
 for arg in nameArgs do
 match Ix.Cli.NameResolve.resolveIxeAddr ixonEnv arg with
Expand All@@ -186,16 +181,28 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 IO.eprintln "no requested constants were found in the env"
 return 1

 -- Build the env once into a Rust-owned `EnvHandle` and share it
 -- across both Phase 1 and Phase 2 loops. Per-target FFI calls
 -- reuse the parsed env — no per-call mmap / lazy-index rebuild.
 let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with
 | .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1
 | .ok h => pure h

 -- Phase 1: execute every constant (cheap, deterministic structural metrics).
 -- Carry each target's address through so phase 2 can rebuild its witness.
 -- For full-closure check claims, use `checkAddrWithEnv` against the
 -- shared `envHandle`. For `--subject-only` (`buildVerifyConst`), the
 -- witness is a small subject-only blob — keep Lean witness +
 -- `executeIxVM`.
 IO.println "── Phase 1: execute (witness generation) ──"
 let mut execed : Array (Result × Address) := #[]
 for (label, addr) in targets do
 try
 let witness ← mkWitness addr
 let (res, execSec) ← timed fun _ =>
 Aiur.Bytecode.Toplevel.execute compiled.bytecode funIdx
 witness.input witness.inputIOBuffer
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer
 else
 compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash
 match res with
 | .error e => IO.eprintln s!" execute {label} failed: {e}"
 | .ok (_, _, queryCounts) =>
Expand DownExpand Up@@ -226,9 +233,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 for i in [:ordered.size] do
 let (r, addr) := ordered[i]!
 try
 let witness ← mkWitness addr
 let (_, proveSec) ← timed fun _ =>
 aiurSystem.prove friParameters funIdx witness.input witness.inputIOBuffer
 let (proveRes, proveSec) ← timed fun _ =>
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 let (claim, proof, ioBuf) :=
 aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer
 (.ok (claim, proof, ioBuf) :
 Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
 else
 match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle addr.hash with
 | .error e => .error e
 | .ok (_claimBytes, proof, ioBuf) =>
 -- The shared envHandle path doesn't return an `Array G`
 -- claim — adapt to the existing benchmark return shape
 -- by recomputing the claim digest from the witness's
 -- input (Phase 2 doesn't read it).
 .ok (#[], proof, ioBuf)
 match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with
 | .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue
 | .ok _ => pure ()
 spent := spent + proveSec
 IO.println s!" {r.name}: prove={proveSec}s (cumulative {spent}s)"
 ordered := ordered.set! i ({ r with proveSec := some proveSec }, addr)
Expand Down

61 changes: 59 additions & 2 deletions
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


2 changes: 2 additions & 0 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -4,6 +4,7 @@ members = [
 "crates/common",
 "crates/compile",
 "crates/ffi",
 "crates/ixvm-codegen",
 "crates/ixon",
 "crates/kernel",
]
Expand All@@ -27,6 +28,7 @@ license = "MIT OR Apache-2.0"
[workspace.dependencies]
# Internal crates
aiur = { path = "crates/aiur" }
ixvm-codegen = { path = "crates/ixvm-codegen" }
ix-common = { path = "crates/common" }
ix-compile = { path = "crates/compile" }
ixon = { path = "crates/ixon" }
Expand Down

60 changes: 60 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -73,6 +73,66 @@ def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_ixvm"]
private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& Array G →
 (ioData : @& Array (G × Array G)) →
 (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
 Array G × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)

/-- IxVM-native prove: same shape as `prove`, but routes execution
 through the codegen'd Rust kernel (`execute_generated`) instead
 of the bytecode interpreter. The resulting `Proof` is
 verification-compatible with one from `prove`. Only valid when
 `system.toplevel` is the IxVM kernel's bytecode. -/
def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
 Array G × Proof × IOBuffer :=
 let ioData := ioBuffer.data.toArray
 let ioMap := ioBuffer.map.toArray
 let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
 ioData ioMap
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_addr_with_env"]
private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-claim prove against a Rust-owned `EnvHandle`. Returns
 `(claimBytes, proof, ioBuffer)` — Rust serializes the
 reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
 deserialize directly without re-running the closure walk. -/
def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_verify"]
opaque verify : @& AiurSystem → @& FriParameters →
 @& Array G → @& Proof → Except String Unit
Expand Down
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
IxVM: native execution pipeline#463

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

 Merged

arthurpaulino
merged 10 commits into

from

Jul 3, 2026
 Merged


IxVM: native execution pipeline
#463
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
0cec144

Aiur Bytecode → Rust codegen for the IxVM kernel


arthurpaulino Jun 30, 2026
aedbf85

Move shard witness construction to Rust + parallelise


arthurpaulino Jun 30, 2026
c9ffd70

Codegen: value-returning byte ops, dead-fold the unconstrained


arthurpaulino Jun 30, 2026
c6c86a6

Wire Rust witness fast path through every check/prove entry point


arthurpaulino Jun 30, 2026
e7b37f7

EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls


arthurpaulino Jun 30, 2026
899d212

ix codegen: add --check flag for CI; gate stale generated kernel


arthurpaulino Jun 30, 2026
56a7ab8

ix check: --interp {source|bytecode} to bypass codegen kernel


arthurpaulino Jul 1, 2026
33ad65a

IxVM codegen: regen + rebase-fixups after KLevel port


arthurpaulino Jul 2, 2026
9d17f9f

ix-check + ixvm tests: coverage gate, --interp source fix, codegen pa…


arthurpaulino Jul 3, 2026
033968c

cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception


arthurpaulino Jul 3, 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


2 changes: 2 additions & 0 deletions
.github/workflows/ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -27,6 +27,8 @@ jobs:
 # lean-action builds above — fails CI.
 - name: Build all targets
 run: lake lint -- --wfail -v
 - name: Check codegen'd IxVM kernel is up to date
 run: lake exe ix codegen --check
 - name: Test Ix CLI
 run: lake test --wfail -- cli
 - name: Aiur tests
Expand Down

4 changes: 3 additions & 1 deletion
Benchmarks/IxVM.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -34,7 +34,9 @@ def main : IO Unit := do

 let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
 throughput (.Elements n.toUInt64 "consts")
 -- IxVM-native prove: routes execution through the codegen'd Rust
 -- kernel (`execute_generated`) instead of the bytecode interpreter.
 bench "serde/blake3 Nat.add_comm"
 (aiurSystem.prove friParameters funIdx #[.ofNat n])
 (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
 ioBuffer
 return

47 changes: 35 additions & 12 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -172,11 +172,6 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 | .error e => IO.eprintln s!"deserialize {ixePath} failed: {e}"; return 1
 | .ok env => pure env
 IO.println s!"Loaded {ixePath}: {ixonEnv.namedCount} named, {ixonEnv.constCount} consts"
 -- Build the witness for `addr`: subject-only (`verify_const`) trusts deps;
 -- otherwise the full-closure check (`verify_claim`, `check addr none`).
 let mkWitness (addr : Address) : IO IxVM.ClaimHarness.ClaimWitness :=
 if subjectOnly then pure (IxVM.ClaimHarness.buildVerifyConst ixonEnv addr)
 else IO.ofExcept (IxVM.ClaimHarness.buildClaimWitness ixonEnv (Ix.Claim.check addr none))
 let mut targets : Array (String × Address) := #[]
 for arg in nameArgs do
 match Ix.Cli.NameResolve.resolveIxeAddr ixonEnv arg with
Expand All@@ -186,16 +181,28 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 IO.eprintln "no requested constants were found in the env"
 return 1

 -- Build the env once into a Rust-owned `EnvHandle` and share it
 -- across both Phase 1 and Phase 2 loops. Per-target FFI calls
 -- reuse the parsed env — no per-call mmap / lazy-index rebuild.
 let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with
 | .error e => IO.eprintln s!"EnvHandle.fromIxe {ixePath}: {e}"; return 1
 | .ok h => pure h

 -- Phase 1: execute every constant (cheap, deterministic structural metrics).
 -- Carry each target's address through so phase 2 can rebuild its witness.
 -- For full-closure check claims, use `checkAddrWithEnv` against the
 -- shared `envHandle`. For `--subject-only` (`buildVerifyConst`), the
 -- witness is a small subject-only blob — keep Lean witness +
 -- `executeIxVM`.
 IO.println "── Phase 1: execute (witness generation) ──"
 let mut execed : Array (Result × Address) := #[]
 for (label, addr) in targets do
 try
 let witness ← mkWitness addr
 let (res, execSec) ← timed fun _ =>
 Aiur.Bytecode.Toplevel.execute compiled.bytecode funIdx
 witness.input witness.inputIOBuffer
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 compiled.bytecode.executeIxVM funIdx witness.input witness.inputIOBuffer
 else
 compiled.bytecode.checkAddrWithEnv funIdx envHandle addr.hash
 match res with
 | .error e => IO.eprintln s!" execute {label} failed: {e}"
 | .ok (_, _, queryCounts) =>
Expand DownExpand Up@@ -226,9 +233,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
 for i in [:ordered.size] do
 let (r, addr) := ordered[i]!
 try
 let witness ← mkWitness addr
 let (_, proveSec) ← timed fun _ =>
 aiurSystem.prove friParameters funIdx witness.input witness.inputIOBuffer
 let (proveRes, proveSec) ← timed fun _ =>
 if subjectOnly then
 let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
 let (claim, proof, ioBuf) :=
 aiurSystem.proveIxVM friParameters funIdx witness.input witness.inputIOBuffer
 (.ok (claim, proof, ioBuf) :
 Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
 else
 match aiurSystem.proveAddrWithEnv friParameters funIdx envHandle addr.hash with
 | .error e => .error e
 | .ok (_claimBytes, proof, ioBuf) =>
 -- The shared envHandle path doesn't return an `Array G`
 -- claim — adapt to the existing benchmark return shape
 -- by recomputing the claim digest from the witness's
 -- input (Phase 2 doesn't read it).
 .ok (#[], proof, ioBuf)
 match (proveRes : Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer)) with
 | .error e => IO.eprintln s!" prove {r.name} failed: {e}"; continue
 | .ok _ => pure ()
 spent := spent + proveSec
 IO.println s!" {r.name}: prove={proveSec}s (cumulative {spent}s)"
 ordered := ordered.set! i ({ r with proveSec := some proveSec }, addr)
Expand Down

61 changes: 59 additions & 2 deletions
Cargo.lock

View file


Open in desktop


Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.


2 changes: 2 additions & 0 deletions
Cargo.toml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -4,6 +4,7 @@ members = [
 "crates/common",
 "crates/compile",
 "crates/ffi",
 "crates/ixvm-codegen",
 "crates/ixon",
 "crates/kernel",
]
Expand All@@ -27,6 +28,7 @@ license = "MIT OR Apache-2.0"
[workspace.dependencies]
# Internal crates
aiur = { path = "crates/aiur" }
ixvm-codegen = { path = "crates/ixvm-codegen" }
ix-common = { path = "crates/common" }
ix-compile = { path = "crates/compile" }
ixon = { path = "crates/ixon" }
Expand Down

60 changes: 60 additions & 0 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -73,6 +73,66 @@ def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_ixvm"]
private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& Array G →
 (ioData : @& Array (G × Array G)) →
 (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
 Array G × Proof × Array (G × Array G) × Array ((G × Array G) × IOKeyInfo)

/-- IxVM-native prove: same shape as `prove`, but routes execution
 through the codegen'd Rust kernel (`execute_generated`) instead
 of the bytecode interpreter. The resulting `Proof` is
 verification-compatible with one from `prove`. Only valid when
 `system.toplevel` is the IxVM kernel's bytecode. -/
def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
 Array G × Proof × IOBuffer :=
 let ioData := ioBuffer.data.toArray
 let ioMap := ioBuffer.map.toArray
 let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
 ioData ioMap
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 (claim, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_prove_addr_with_env"]
private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-claim prove against a Rust-owned `EnvHandle`. Returns
 `(claimBytes, proof, ioBuffer)` — Rust serializes the
 reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
 deserialize directly without re-running the closure walk. -/
def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

@[extern "rs_aiur_system_shard_prove_with_env"]
private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
 Except String (ByteArray × Proof ×
 Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))

/-- Per-shard prove against a Rust-owned `EnvHandle`. -/
def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 Except String (ByteArray × Proof × IOBuffer) :=
 match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
 | .error e => .error e
 | .ok (claimBytes, proof, ioData, ioMap) =>
 let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
 let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
 .ok (claimBytes, proof, ⟨ioData, ioMap⟩)

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