feat(aiur): Measured-ingress sharding#524

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

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

feat(aiur): Measured-ingress sharding #524

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
9b83f72
profile: per-metric block leaderboards (--top N, default 10)
samuelburnham Jul 22, 2026
41deee0
profile: record memo-unique substitutions (.ixprof v2)
samuelburnham Jul 24, 2026
ae4aab9
shard: calibrated Aiur cost model, profile/shard --backend aiur
samuelburnham Jul 24, 2026
645707b
profile: env-wide closure cost sweep (ix profile sweep)
samuelburnham Jul 24, 2026
f475ee0
shard: closure-union byte accounting for Aiur packing
samuelburnham Jul 28, 2026
5244868
shard: price Aiur ingress as frontier-trusted, not full-closure
samuelburnham Jul 28, 2026
bcfa8bc
tests: pin the const/blob classification of a non-ingressed ref
samuelburnham Jul 28, 2026
d2bf0fd
IxVM kernel: classify refs from the discriminator, poison the unresolved
samuelburnham Jul 28, 2026
0b47e09
IxVM kernel: ingress frontier constants as type-only axioms
samuelburnham Jul 28, 2026
688f2c8
claim: separate "not checked here" from "ingressed as a type-only stub"
samuelburnham Jul 28, 2026
176930a
diagnostics: name the missing IO key, count constants touched per check
samuelburnham Jul 28, 2026
9b26d2a
docs: Step 1 must be atomic — dual-field migration breaks node identity
samuelburnham Jul 28, 2026
83450a4
IxVM kernel: synthesize mutual-block member addresses
samuelburnham Jul 28, 2026
0bae7db
profile: record the measured touch graph, seed it FULL in Aiur packing
samuelburnham Jul 29, 2026
2f599ec
shard witnesses: measured ingress sets, wired end to end
samuelburnham Jul 29, 2026
be5cf4b
shard: per-shard stub-promotion rounds, price the emitted sets
samuelburnham Jul 29, 2026
cfa47a6
aiur: assert forensics in the interpreter, witness-set diagnosis probe
samuelburnham Jul 29, 2026
e16c108
repair driver: escalate divergent shards to a green partition
samuelburnham Jul 29, 2026
c86c344
kernel: report every wanted stub, making escalation fully targeted
samuelburnham Jul 29, 2026
b1e6bce
prove: batched, resumable all-shards mode with composed verdict
samuelburnham Jul 29, 2026
826f179
witness: ghost stubs — position-only entries, no bytes, no hashing
samuelburnham Jul 29, 2026
0bc3414
shard: persist whnf/def_eq/nat_arith per shard
samuelburnham Jul 30, 2026
3631500
merge prep: ghost-classification cache, shard-pipeline E2E test, pins
samuelburnham Jul 30, 2026
c029f54
caches: digest-keyed ~/.ix/cache replaces CSV sidecars; ghost -> addr…
samuelburnham Jul 30, 2026
ca25fa5
fmt: rustfmt ix-ffi
samuelburnham Jul 30, 2026
e1feae1
rebase reconcile: regen codegen against main's kernel, refresh FFT pins
samuelburnham Jul 30, 2026
f3c3583
bench: aiur-shard backend — planner metrics + heavy-shard execution
samuelburnham Jul 30, 2026
08ef90c
bench: register Init as a benchmark env
samuelburnham Jul 30, 2026
60b9457
fmt: rustfmt aiur execute + kernel shard
samuelburnham Jul 30, 2026
cf0c47e
remove diag_duplicate_wrappers forensics probe
samuelburnham Jul 30, 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
8 changes: 4 additions & 4 deletions .github/workflows/bencher-thresholds-reset.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
# GitHub requires literal choice options, so this list stays static:
# keep it (and the jobs' valid= lists below) in sync with the
# backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
sha:
description: "Commit to anchor to (default: HEAD)"
required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
# (backendSpecs) minus the runner-arch suffix. Static because this
# job runs on a cheap runner with no built `ix`; keep in sync when
# adding a backend.
valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
if [ "$EVENT" = workflow_dispatch ]; then
# Reset the chosen workload(s) at the given commit; no PR scan.
sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
# which the merge job expands into every workload). Same static
# list as the reset job; keep both in sync with backendSpecs in
# Ix/Cli/BenchCmd.lean.
valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
accepted="$valid all"
# Parse the workload token(s) after the command, lowercased.
workloads=$(printf '%s' "$BODY" \
Expand Down
20 changes: 14 additions & 6 deletions Ix/Aiur/Protocol.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)

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

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

/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
blocks ingressed as type-only axioms; only the partition knows which those
are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
disabled) is the keyed stub-consultation cache directory (normally
`~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
classification execute. -/
def shardProveWithEnv (system : @& AiurSystem)
(funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
(funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
(ownedBlob foreignBlob stubbedBlob : ByteArray)
(consultCacheDir : String := "") :
Except String (ByteArray × Proof × IOBuffer) :=
(shardProveWithEnv' system funIdx envHandle ownedBlob).map
(shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
stubbedBlob consultCacheDir).map
fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

@[extern "rs_aiur_system_verify"]
Expand Down
8 changes: 5 additions & 3 deletions Ix/Aiur/Semantics/BytecodeFfi.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →

@[extern "rs_aiur_toplevel_shard_check_with_env"]
private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
@& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
@& ByteArray → Bool →
Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
`checkAddrWithEnv` for `useBytecode` semantics. -/
def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
(funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
(ownedBlob : ByteArray) (useBytecode : Bool := false)
(ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
: Except String (Array G × IOBuffer × Array QueryCount) :=
(shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
(shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
stubbedBlob useBytecode).map
fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

end Bytecode.Toplevel
Expand Down
32 changes: 26 additions & 6 deletions Ix/Claim.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -137,11 +137,27 @@ Five variants in three families:
the merkle tree rooted at `tree`. Used by aggregation to discharge
leaves from a conditional claim's assumption set. Carries no
assumptions.

`checkEnv` carries a second root, `stubbed`, naming the subset of
`assumptions` the claim ingressed as type-only axioms: their bodies were
withheld, so the claim holds given only their TYPES, and no reduction
passed through them.

The two roots are genuinely different sets, which is why one cannot serve
for both. A shard skips checking everything it does not own, but it must
still ingress in FULL anything it reduces through — a definition it
unfolds, or an inductive whose recursor rules it applies — even though
another shard is responsible for checking that constant. Those blocks are
in `assumptions` but NOT in `stubbed`. Folding them into the owned set
instead is not possible: owned sets partition the environment so each
constant is checked exactly once, and two shards may reduce through the
same constant.
-/
inductive Claim where
| eval (input output : Address) (assumptions : Option Address)
| check (const : Address) (assumptions : Option Address)
| checkEnv (root : Address) (assumptions : Option Address)
(stubbed : Option Address)
| reveal (comm : Address) (info : RevealConstantInfo)
| contains (tree : Address) (const : Address)
deriving BEq, Repr, Inhabited
Expand DownExpand Up@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
Serialize.put const
putOptAddr assumptions
| .checkEnv root assumptions => do
| .checkEnv root assumptions stubbed => do
putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
Serialize.put root
putOptAddr assumptions
putOptAddr stubbed
| .reveal comm info => do
putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
Serialize.put comm
Expand All@@ -523,7 +540,8 @@ def get : GetM Claim := do
else if tag.size == VARIANT_CHECK_ENV_CLAIM then
let root ← Serialize.get
let asm ← getOptAddr
return .checkEnv root asm
let stubbed ← getOptAddr
return .checkEnv root asm stubbed
else if tag.size == VARIANT_REVEAL_CLAIM then
return .reveal (← Serialize.get) (← RevealConstantInfo.get)
else if tag.size == VARIANT_CONTAINS_CLAIM then
Expand All@@ -538,7 +556,7 @@ instance : ToString Claim where
toString c := match c with
| .eval i o asm => s!"Eval({i}, {o}, {asm})"
| .check v asm => s!"Check({v}, {asm})"
| .checkEnv r asm => s!"CheckEnv({r}, {asm})"
| .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
| .reveal comm info => s!"Reveal({comm}, {repr info})"
| .contains t c => s!"Contains({t}, {c})"

Expand DownExpand Up@@ -566,7 +584,7 @@ namespace Proof
def variantOf : Ix.Claim → UInt64
| .eval _ _ _ => Ix.Claim.VARIANT_EVAL_PROOF
| .check _ _ => Ix.Claim.VARIANT_CHECK_PROOF
| .checkEnv _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
| .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
| .reveal _ _ => Ix.Claim.VARIANT_REVEAL_PROOF
| .contains _ _ => Ix.Claim.VARIANT_CONTAINS_PROOF

Expand All@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
| .check addr asm => do
Serialize.put addr
Ix.Claim.putOptAddr asm
| .checkEnv root asm => do
| .checkEnv root asm stubbed => do
Serialize.put root
Ix.Claim.putOptAddr asm
Ix.Claim.putOptAddr stubbed
| .reveal comm info => do
Serialize.put comm
Ix.RevealConstantInfo.put info
Expand All@@ -609,7 +628,8 @@ def get : GetM Proof := do
else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
let root ← Serialize.get
let asm ← Ix.Claim.getOptAddr
pure (.checkEnv root asm)
let stubbed ← Ix.Claim.getOptAddr
pure (.checkEnv root asm stubbed)
else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
let comm ← Serialize.get
let info ← Ix.RevealConstantInfo.get
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
feat(aiur): Measured-ingress sharding#524

New issue

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

 Sign up for GitHub

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

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
30
commits into

base:main
Choose a base branch

from

 Draft


feat(aiur): Measured-ingress sharding
#524
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


30 commits


Select commit
Hold shift + click to select a range
9b83f72

profile: per-metric block leaderboards (--top N, default 10)


samuelburnham Jul 22, 2026
41deee0

profile: record memo-unique substitutions (.ixprof v2)


samuelburnham Jul 24, 2026
ae4aab9

shard: calibrated Aiur cost model, profile/shard --backend aiur


samuelburnham Jul 24, 2026
645707b

profile: env-wide closure cost sweep (ix profile sweep)


samuelburnham Jul 24, 2026
f475ee0

shard: closure-union byte accounting for Aiur packing


samuelburnham Jul 28, 2026
5244868

shard: price Aiur ingress as frontier-trusted, not full-closure


samuelburnham Jul 28, 2026
bcfa8bc

tests: pin the const/blob classification of a non-ingressed ref


samuelburnham Jul 28, 2026
d2bf0fd

IxVM kernel: classify refs from the discriminator, poison the unresolved


samuelburnham Jul 28, 2026
0b47e09

IxVM kernel: ingress frontier constants as type-only axioms


samuelburnham Jul 28, 2026
688f2c8

claim: separate "not checked here" from "ingressed as a type-only stub"


samuelburnham Jul 28, 2026
176930a

diagnostics: name the missing IO key, count constants touched per check


samuelburnham Jul 28, 2026
9b26d2a

docs: Step 1 must be atomic — dual-field migration breaks node identity


samuelburnham Jul 28, 2026
83450a4

IxVM kernel: synthesize mutual-block member addresses


samuelburnham Jul 28, 2026
0bae7db

profile: record the measured touch graph, seed it FULL in Aiur packing


samuelburnham Jul 29, 2026
2f599ec

shard witnesses: measured ingress sets, wired end to end


samuelburnham Jul 29, 2026
be5cf4b

shard: per-shard stub-promotion rounds, price the emitted sets


samuelburnham Jul 29, 2026
cfa47a6

aiur: assert forensics in the interpreter, witness-set diagnosis probe


samuelburnham Jul 29, 2026
e16c108

repair driver: escalate divergent shards to a green partition


samuelburnham Jul 29, 2026
c86c344

kernel: report every wanted stub, making escalation fully targeted


samuelburnham Jul 29, 2026
b1e6bce

prove: batched, resumable all-shards mode with composed verdict


samuelburnham Jul 29, 2026
826f179

witness: ghost stubs — position-only entries, no bytes, no hashing


samuelburnham Jul 29, 2026
0bc3414

shard: persist whnf/def_eq/nat_arith per shard


samuelburnham Jul 30, 2026
3631500

merge prep: ghost-classification cache, shard-pipeline E2E test, pins


samuelburnham Jul 30, 2026
c029f54

caches: digest-keyed ~/.ix/cache replaces CSV sidecars; ghost -> addr…


samuelburnham Jul 30, 2026
ca25fa5

fmt: rustfmt ix-ffi


samuelburnham Jul 30, 2026
e1feae1

rebase reconcile: regen codegen against main's kernel, refresh FFT pins


samuelburnham Jul 30, 2026
f3c3583

bench: aiur-shard backend — planner metrics + heavy-shard execution


samuelburnham Jul 30, 2026
08ef90c

bench: register Init as a benchmark env


samuelburnham Jul 30, 2026
60b9457

fmt: rustfmt aiur execute + kernel shard


samuelburnham Jul 30, 2026
cf0c47e

remove diag_duplicate_wrappers forensics probe


samuelburnham Jul 30, 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


8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

20 changes: 14 additions & 6 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)

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

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

/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
 blocks ingressed as type-only axioms; only the partition knows which those
 are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
 disabled) is the keyed stub-consultation cache directory (normally
 `~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
 classification execute. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob foreignBlob stubbedBlob : ByteArray)
 (consultCacheDir : String := "") :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 (shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
 stubbedBlob consultCacheDir).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

@[extern "rs_aiur_system_verify"]
Expand Down

8 changes: 5 additions & 3 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →

@[extern "rs_aiur_toplevel_shard_check_with_env"]
private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
 @& ByteArray → Bool →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
 `checkAddrWithEnv` for `useBytecode` semantics. -/
def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (useBytecode : Bool := false)
 (ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
 : Except String (Array G × IOBuffer × Array QueryCount) :=
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
 stubbedBlob useBytecode).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

end Bytecode.Toplevel
Expand Down

32 changes: 26 additions & 6 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -137,11 +137,27 @@ Five variants in three families:
 the merkle tree rooted at `tree`. Used by aggregation to discharge
 leaves from a conditional claim's assumption set. Carries no
 assumptions.

`checkEnv` carries a second root, `stubbed`, naming the subset of
`assumptions` the claim ingressed as type-only axioms: their bodies were
withheld, so the claim holds given only their TYPES, and no reduction
passed through them.

The two roots are genuinely different sets, which is why one cannot serve
for both. A shard skips checking everything it does not own, but it must
still ingress in FULL anything it reduces through — a definition it
unfolds, or an inductive whose recursor rules it applies — even though
another shard is responsible for checking that constant. Those blocks are
in `assumptions` but NOT in `stubbed`. Folding them into the owned set
instead is not possible: owned sets partition the environment so each
constant is checked exactly once, and two shards may reduce through the
same constant.
-/
inductive Claim where
 | eval (input output : Address) (assumptions : Option Address)
 | check (const : Address) (assumptions : Option Address)
 | checkEnv (root : Address) (assumptions : Option Address)
 (stubbed : Option Address)
 | reveal (comm : Address) (info : RevealConstantInfo)
 | contains (tree : Address) (const : Address)
 deriving BEq, Repr, Inhabited
Expand DownExpand Up@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
 Serialize.put const
 putOptAddr assumptions
 | .checkEnv root assumptions => do
 | .checkEnv root assumptions stubbed => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
 Serialize.put root
 putOptAddr assumptions
 putOptAddr stubbed
 | .reveal comm info => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
 Serialize.put comm
Expand All@@ -523,7 +540,8 @@ def get : GetM Claim := do
 else if tag.size == VARIANT_CHECK_ENV_CLAIM then
 let root ← Serialize.get
 let asm ← getOptAddr
 return .checkEnv root asm
 let stubbed ← getOptAddr
 return .checkEnv root asm stubbed
 else if tag.size == VARIANT_REVEAL_CLAIM then
 return .reveal (← Serialize.get) (← RevealConstantInfo.get)
 else if tag.size == VARIANT_CONTAINS_CLAIM then
Expand All@@ -538,7 +556,7 @@ instance : ToString Claim where
 toString c := match c with
 | .eval i o asm => s!"Eval({i}, {o}, {asm})"
 | .check v asm => s!"Check({v}, {asm})"
 | .checkEnv r asm => s!"CheckEnv({r}, {asm})"
 | .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
 | .reveal comm info => s!"Reveal({comm}, {repr info})"
 | .contains t c => s!"Contains({t}, {c})"

Expand DownExpand Up@@ -566,7 +584,7 @@ namespace Proof
def variantOf : Ix.Claim → UInt64
 | .eval _ _ _ => Ix.Claim.VARIANT_EVAL_PROOF
 | .check _ _ => Ix.Claim.VARIANT_CHECK_PROOF
 | .checkEnv _ _  => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .reveal _ _ => Ix.Claim.VARIANT_REVEAL_PROOF
 | .contains _ _ => Ix.Claim.VARIANT_CONTAINS_PROOF

Expand All@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
 | .check addr asm => do
 Serialize.put addr
 Ix.Claim.putOptAddr asm
 | .checkEnv root asm => do
 | .checkEnv root asm stubbed => do
 Serialize.put root
 Ix.Claim.putOptAddr asm
 Ix.Claim.putOptAddr stubbed
 | .reveal comm info => do
 Serialize.put comm
 Ix.RevealConstantInfo.put info
Expand All@@ -609,7 +628,8 @@ def get : GetM Proof := do
 else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
 let root ← Serialize.get
 let asm ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm)
 let stubbed ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm stubbed)
 else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
 let comm ← Serialize.get
 let info ← Ix.RevealConstantInfo.get
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
feat(aiur): Measured-ingress sharding#524

New issue

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

 Sign up for GitHub

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

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
30
commits into

base:main
Choose a base branch

from

 Draft


feat(aiur): Measured-ingress sharding
#524
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


30 commits


Select commit
Hold shift + click to select a range
9b83f72

profile: per-metric block leaderboards (--top N, default 10)


samuelburnham Jul 22, 2026
41deee0

profile: record memo-unique substitutions (.ixprof v2)


samuelburnham Jul 24, 2026
ae4aab9

shard: calibrated Aiur cost model, profile/shard --backend aiur


samuelburnham Jul 24, 2026
645707b

profile: env-wide closure cost sweep (ix profile sweep)


samuelburnham Jul 24, 2026
f475ee0

shard: closure-union byte accounting for Aiur packing


samuelburnham Jul 28, 2026
5244868

shard: price Aiur ingress as frontier-trusted, not full-closure


samuelburnham Jul 28, 2026
bcfa8bc

tests: pin the const/blob classification of a non-ingressed ref


samuelburnham Jul 28, 2026
d2bf0fd

IxVM kernel: classify refs from the discriminator, poison the unresolved


samuelburnham Jul 28, 2026
0b47e09

IxVM kernel: ingress frontier constants as type-only axioms


samuelburnham Jul 28, 2026
688f2c8

claim: separate "not checked here" from "ingressed as a type-only stub"


samuelburnham Jul 28, 2026
176930a

diagnostics: name the missing IO key, count constants touched per check


samuelburnham Jul 28, 2026
9b26d2a

docs: Step 1 must be atomic — dual-field migration breaks node identity


samuelburnham Jul 28, 2026
83450a4

IxVM kernel: synthesize mutual-block member addresses


samuelburnham Jul 28, 2026
0bae7db

profile: record the measured touch graph, seed it FULL in Aiur packing


samuelburnham Jul 29, 2026
2f599ec

shard witnesses: measured ingress sets, wired end to end


samuelburnham Jul 29, 2026
be5cf4b

shard: per-shard stub-promotion rounds, price the emitted sets


samuelburnham Jul 29, 2026
cfa47a6

aiur: assert forensics in the interpreter, witness-set diagnosis probe


samuelburnham Jul 29, 2026
e16c108

repair driver: escalate divergent shards to a green partition


samuelburnham Jul 29, 2026
c86c344

kernel: report every wanted stub, making escalation fully targeted


samuelburnham Jul 29, 2026
b1e6bce

prove: batched, resumable all-shards mode with composed verdict


samuelburnham Jul 29, 2026
826f179

witness: ghost stubs — position-only entries, no bytes, no hashing


samuelburnham Jul 29, 2026
0bc3414

shard: persist whnf/def_eq/nat_arith per shard


samuelburnham Jul 30, 2026
3631500

merge prep: ghost-classification cache, shard-pipeline E2E test, pins


samuelburnham Jul 30, 2026
c029f54

caches: digest-keyed ~/.ix/cache replaces CSV sidecars; ghost -> addr…


samuelburnham Jul 30, 2026
ca25fa5

fmt: rustfmt ix-ffi


samuelburnham Jul 30, 2026
e1feae1

rebase reconcile: regen codegen against main's kernel, refresh FFT pins


samuelburnham Jul 30, 2026
f3c3583

bench: aiur-shard backend — planner metrics + heavy-shard execution


samuelburnham Jul 30, 2026
08ef90c

bench: register Init as a benchmark env


samuelburnham Jul 30, 2026
60b9457

fmt: rustfmt aiur execute + kernel shard


samuelburnham Jul 30, 2026
cf0c47e

remove diag_duplicate_wrappers forensics probe


samuelburnham Jul 30, 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


8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

20 changes: 14 additions & 6 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)

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

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

/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
 blocks ingressed as type-only axioms; only the partition knows which those
 are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
 disabled) is the keyed stub-consultation cache directory (normally
 `~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
 classification execute. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob foreignBlob stubbedBlob : ByteArray)
 (consultCacheDir : String := "") :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 (shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
 stubbedBlob consultCacheDir).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

@[extern "rs_aiur_system_verify"]
Expand Down

8 changes: 5 additions & 3 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →

@[extern "rs_aiur_toplevel_shard_check_with_env"]
private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
 @& ByteArray → Bool →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
 `checkAddrWithEnv` for `useBytecode` semantics. -/
def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (useBytecode : Bool := false)
 (ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
 : Except String (Array G × IOBuffer × Array QueryCount) :=
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
 stubbedBlob useBytecode).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

end Bytecode.Toplevel
Expand Down

32 changes: 26 additions & 6 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -137,11 +137,27 @@ Five variants in three families:
 the merkle tree rooted at `tree`. Used by aggregation to discharge
 leaves from a conditional claim's assumption set. Carries no
 assumptions.

`checkEnv` carries a second root, `stubbed`, naming the subset of
`assumptions` the claim ingressed as type-only axioms: their bodies were
withheld, so the claim holds given only their TYPES, and no reduction
passed through them.

The two roots are genuinely different sets, which is why one cannot serve
for both. A shard skips checking everything it does not own, but it must
still ingress in FULL anything it reduces through — a definition it
unfolds, or an inductive whose recursor rules it applies — even though
another shard is responsible for checking that constant. Those blocks are
in `assumptions` but NOT in `stubbed`. Folding them into the owned set
instead is not possible: owned sets partition the environment so each
constant is checked exactly once, and two shards may reduce through the
same constant.
-/
inductive Claim where
 | eval (input output : Address) (assumptions : Option Address)
 | check (const : Address) (assumptions : Option Address)
 | checkEnv (root : Address) (assumptions : Option Address)
 (stubbed : Option Address)
 | reveal (comm : Address) (info : RevealConstantInfo)
 | contains (tree : Address) (const : Address)
 deriving BEq, Repr, Inhabited
Expand DownExpand Up@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
 Serialize.put const
 putOptAddr assumptions
 | .checkEnv root assumptions => do
 | .checkEnv root assumptions stubbed => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
 Serialize.put root
 putOptAddr assumptions
 putOptAddr stubbed
 | .reveal comm info => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
 Serialize.put comm
Expand All@@ -523,7 +540,8 @@ def get : GetM Claim := do
 else if tag.size == VARIANT_CHECK_ENV_CLAIM then
 let root ← Serialize.get
 let asm ← getOptAddr
 return .checkEnv root asm
 let stubbed ← getOptAddr
 return .checkEnv root asm stubbed
 else if tag.size == VARIANT_REVEAL_CLAIM then
 return .reveal (← Serialize.get) (← RevealConstantInfo.get)
 else if tag.size == VARIANT_CONTAINS_CLAIM then
Expand All@@ -538,7 +556,7 @@ instance : ToString Claim where
 toString c := match c with
 | .eval i o asm => s!"Eval({i}, {o}, {asm})"
 | .check v asm => s!"Check({v}, {asm})"
 | .checkEnv r asm => s!"CheckEnv({r}, {asm})"
 | .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
 | .reveal comm info => s!"Reveal({comm}, {repr info})"
 | .contains t c => s!"Contains({t}, {c})"

Expand DownExpand Up@@ -566,7 +584,7 @@ namespace Proof
def variantOf : Ix.Claim → UInt64
 | .eval _ _ _ => Ix.Claim.VARIANT_EVAL_PROOF
 | .check _ _ => Ix.Claim.VARIANT_CHECK_PROOF
 | .checkEnv _ _  => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .reveal _ _ => Ix.Claim.VARIANT_REVEAL_PROOF
 | .contains _ _ => Ix.Claim.VARIANT_CONTAINS_PROOF

Expand All@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
 | .check addr asm => do
 Serialize.put addr
 Ix.Claim.putOptAddr asm
 | .checkEnv root asm => do
 | .checkEnv root asm stubbed => do
 Serialize.put root
 Ix.Claim.putOptAddr asm
 Ix.Claim.putOptAddr stubbed
 | .reveal comm info => do
 Serialize.put comm
 Ix.RevealConstantInfo.put info
Expand All@@ -609,7 +628,8 @@ def get : GetM Proof := do
 else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
 let root ← Serialize.get
 let asm ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm)
 let stubbed ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm stubbed)
 else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
 let comm ← Serialize.get
 let info ← Ix.RevealConstantInfo.get
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
feat(aiur): Measured-ingress sharding#524

New issue

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

 Sign up for GitHub

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

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
30
commits into

base:main
Choose a base branch

from

 Draft


feat(aiur): Measured-ingress sharding
#524
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


30 commits


Select commit
Hold shift + click to select a range
9b83f72

profile: per-metric block leaderboards (--top N, default 10)


samuelburnham Jul 22, 2026
41deee0

profile: record memo-unique substitutions (.ixprof v2)


samuelburnham Jul 24, 2026
ae4aab9

shard: calibrated Aiur cost model, profile/shard --backend aiur


samuelburnham Jul 24, 2026
645707b

profile: env-wide closure cost sweep (ix profile sweep)


samuelburnham Jul 24, 2026
f475ee0

shard: closure-union byte accounting for Aiur packing


samuelburnham Jul 28, 2026
5244868

shard: price Aiur ingress as frontier-trusted, not full-closure


samuelburnham Jul 28, 2026
bcfa8bc

tests: pin the const/blob classification of a non-ingressed ref


samuelburnham Jul 28, 2026
d2bf0fd

IxVM kernel: classify refs from the discriminator, poison the unresolved


samuelburnham Jul 28, 2026
0b47e09

IxVM kernel: ingress frontier constants as type-only axioms


samuelburnham Jul 28, 2026
688f2c8

claim: separate "not checked here" from "ingressed as a type-only stub"


samuelburnham Jul 28, 2026
176930a

diagnostics: name the missing IO key, count constants touched per check


samuelburnham Jul 28, 2026
9b26d2a

docs: Step 1 must be atomic — dual-field migration breaks node identity


samuelburnham Jul 28, 2026
83450a4

IxVM kernel: synthesize mutual-block member addresses


samuelburnham Jul 28, 2026
0bae7db

profile: record the measured touch graph, seed it FULL in Aiur packing


samuelburnham Jul 29, 2026
2f599ec

shard witnesses: measured ingress sets, wired end to end


samuelburnham Jul 29, 2026
be5cf4b

shard: per-shard stub-promotion rounds, price the emitted sets


samuelburnham Jul 29, 2026
cfa47a6

aiur: assert forensics in the interpreter, witness-set diagnosis probe


samuelburnham Jul 29, 2026
e16c108

repair driver: escalate divergent shards to a green partition


samuelburnham Jul 29, 2026
c86c344

kernel: report every wanted stub, making escalation fully targeted


samuelburnham Jul 29, 2026
b1e6bce

prove: batched, resumable all-shards mode with composed verdict


samuelburnham Jul 29, 2026
826f179

witness: ghost stubs — position-only entries, no bytes, no hashing


samuelburnham Jul 29, 2026
0bc3414

shard: persist whnf/def_eq/nat_arith per shard


samuelburnham Jul 30, 2026
3631500

merge prep: ghost-classification cache, shard-pipeline E2E test, pins


samuelburnham Jul 30, 2026
c029f54

caches: digest-keyed ~/.ix/cache replaces CSV sidecars; ghost -> addr…


samuelburnham Jul 30, 2026
ca25fa5

fmt: rustfmt ix-ffi


samuelburnham Jul 30, 2026
e1feae1

rebase reconcile: regen codegen against main's kernel, refresh FFT pins


samuelburnham Jul 30, 2026
f3c3583

bench: aiur-shard backend — planner metrics + heavy-shard execution


samuelburnham Jul 30, 2026
08ef90c

bench: register Init as a benchmark env


samuelburnham Jul 30, 2026
60b9457

fmt: rustfmt aiur execute + kernel shard


samuelburnham Jul 30, 2026
cf0c47e

remove diag_duplicate_wrappers forensics probe


samuelburnham Jul 30, 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


8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

20 changes: 14 additions & 6 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)

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

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

/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
 blocks ingressed as type-only axioms; only the partition knows which those
 are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
 disabled) is the keyed stub-consultation cache directory (normally
 `~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
 classification execute. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob foreignBlob stubbedBlob : ByteArray)
 (consultCacheDir : String := "") :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 (shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
 stubbedBlob consultCacheDir).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

@[extern "rs_aiur_system_verify"]
Expand Down

8 changes: 5 additions & 3 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →

@[extern "rs_aiur_toplevel_shard_check_with_env"]
private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
 @& ByteArray → Bool →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
 `checkAddrWithEnv` for `useBytecode` semantics. -/
def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (useBytecode : Bool := false)
 (ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
 : Except String (Array G × IOBuffer × Array QueryCount) :=
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
 stubbedBlob useBytecode).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

end Bytecode.Toplevel
Expand Down

32 changes: 26 additions & 6 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -137,11 +137,27 @@ Five variants in three families:
 the merkle tree rooted at `tree`. Used by aggregation to discharge
 leaves from a conditional claim's assumption set. Carries no
 assumptions.

`checkEnv` carries a second root, `stubbed`, naming the subset of
`assumptions` the claim ingressed as type-only axioms: their bodies were
withheld, so the claim holds given only their TYPES, and no reduction
passed through them.

The two roots are genuinely different sets, which is why one cannot serve
for both. A shard skips checking everything it does not own, but it must
still ingress in FULL anything it reduces through — a definition it
unfolds, or an inductive whose recursor rules it applies — even though
another shard is responsible for checking that constant. Those blocks are
in `assumptions` but NOT in `stubbed`. Folding them into the owned set
instead is not possible: owned sets partition the environment so each
constant is checked exactly once, and two shards may reduce through the
same constant.
-/
inductive Claim where
 | eval (input output : Address) (assumptions : Option Address)
 | check (const : Address) (assumptions : Option Address)
 | checkEnv (root : Address) (assumptions : Option Address)
 (stubbed : Option Address)
 | reveal (comm : Address) (info : RevealConstantInfo)
 | contains (tree : Address) (const : Address)
 deriving BEq, Repr, Inhabited
Expand DownExpand Up@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
 Serialize.put const
 putOptAddr assumptions
 | .checkEnv root assumptions => do
 | .checkEnv root assumptions stubbed => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
 Serialize.put root
 putOptAddr assumptions
 putOptAddr stubbed
 | .reveal comm info => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
 Serialize.put comm
Expand All@@ -523,7 +540,8 @@ def get : GetM Claim := do
 else if tag.size == VARIANT_CHECK_ENV_CLAIM then
 let root ← Serialize.get
 let asm ← getOptAddr
 return .checkEnv root asm
 let stubbed ← getOptAddr
 return .checkEnv root asm stubbed
 else if tag.size == VARIANT_REVEAL_CLAIM then
 return .reveal (← Serialize.get) (← RevealConstantInfo.get)
 else if tag.size == VARIANT_CONTAINS_CLAIM then
Expand All@@ -538,7 +556,7 @@ instance : ToString Claim where
 toString c := match c with
 | .eval i o asm => s!"Eval({i}, {o}, {asm})"
 | .check v asm => s!"Check({v}, {asm})"
 | .checkEnv r asm => s!"CheckEnv({r}, {asm})"
 | .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
 | .reveal comm info => s!"Reveal({comm}, {repr info})"
 | .contains t c => s!"Contains({t}, {c})"

Expand DownExpand Up@@ -566,7 +584,7 @@ namespace Proof
def variantOf : Ix.Claim → UInt64
 | .eval _ _ _ => Ix.Claim.VARIANT_EVAL_PROOF
 | .check _ _ => Ix.Claim.VARIANT_CHECK_PROOF
 | .checkEnv _ _  => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .reveal _ _ => Ix.Claim.VARIANT_REVEAL_PROOF
 | .contains _ _ => Ix.Claim.VARIANT_CONTAINS_PROOF

Expand All@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
 | .check addr asm => do
 Serialize.put addr
 Ix.Claim.putOptAddr asm
 | .checkEnv root asm => do
 | .checkEnv root asm stubbed => do
 Serialize.put root
 Ix.Claim.putOptAddr asm
 Ix.Claim.putOptAddr stubbed
 | .reveal comm info => do
 Serialize.put comm
 Ix.RevealConstantInfo.put info
Expand All@@ -609,7 +628,8 @@ def get : GetM Proof := do
 else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
 let root ← Serialize.get
 let asm ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm)
 let stubbed ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm stubbed)
 else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
 let comm ← Serialize.get
 let info ← Ix.RevealConstantInfo.get
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
feat(aiur): Measured-ingress sharding#524

New issue

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

 Sign up for GitHub

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

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
30
commits into

base:main
Choose a base branch

from

 Draft


feat(aiur): Measured-ingress sharding
#524
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


30 commits


Select commit
Hold shift + click to select a range
9b83f72

profile: per-metric block leaderboards (--top N, default 10)


samuelburnham Jul 22, 2026
41deee0

profile: record memo-unique substitutions (.ixprof v2)


samuelburnham Jul 24, 2026
ae4aab9

shard: calibrated Aiur cost model, profile/shard --backend aiur


samuelburnham Jul 24, 2026
645707b

profile: env-wide closure cost sweep (ix profile sweep)


samuelburnham Jul 24, 2026
f475ee0

shard: closure-union byte accounting for Aiur packing


samuelburnham Jul 28, 2026
5244868

shard: price Aiur ingress as frontier-trusted, not full-closure


samuelburnham Jul 28, 2026
bcfa8bc

tests: pin the const/blob classification of a non-ingressed ref


samuelburnham Jul 28, 2026
d2bf0fd

IxVM kernel: classify refs from the discriminator, poison the unresolved


samuelburnham Jul 28, 2026
0b47e09

IxVM kernel: ingress frontier constants as type-only axioms


samuelburnham Jul 28, 2026
688f2c8

claim: separate "not checked here" from "ingressed as a type-only stub"


samuelburnham Jul 28, 2026
176930a

diagnostics: name the missing IO key, count constants touched per check


samuelburnham Jul 28, 2026
9b26d2a

docs: Step 1 must be atomic — dual-field migration breaks node identity


samuelburnham Jul 28, 2026
83450a4

IxVM kernel: synthesize mutual-block member addresses


samuelburnham Jul 28, 2026
0bae7db

profile: record the measured touch graph, seed it FULL in Aiur packing


samuelburnham Jul 29, 2026
2f599ec

shard witnesses: measured ingress sets, wired end to end


samuelburnham Jul 29, 2026
be5cf4b

shard: per-shard stub-promotion rounds, price the emitted sets


samuelburnham Jul 29, 2026
cfa47a6

aiur: assert forensics in the interpreter, witness-set diagnosis probe


samuelburnham Jul 29, 2026
e16c108

repair driver: escalate divergent shards to a green partition


samuelburnham Jul 29, 2026
c86c344

kernel: report every wanted stub, making escalation fully targeted


samuelburnham Jul 29, 2026
b1e6bce

prove: batched, resumable all-shards mode with composed verdict


samuelburnham Jul 29, 2026
826f179

witness: ghost stubs — position-only entries, no bytes, no hashing


samuelburnham Jul 29, 2026
0bc3414

shard: persist whnf/def_eq/nat_arith per shard


samuelburnham Jul 30, 2026
3631500

merge prep: ghost-classification cache, shard-pipeline E2E test, pins


samuelburnham Jul 30, 2026
c029f54

caches: digest-keyed ~/.ix/cache replaces CSV sidecars; ghost -> addr…


samuelburnham Jul 30, 2026
ca25fa5

fmt: rustfmt ix-ffi


samuelburnham Jul 30, 2026
e1feae1

rebase reconcile: regen codegen against main's kernel, refresh FFT pins


samuelburnham Jul 30, 2026
f3c3583

bench: aiur-shard backend — planner metrics + heavy-shard execution


samuelburnham Jul 30, 2026
08ef90c

bench: register Init as a benchmark env


samuelburnham Jul 30, 2026
60b9457

fmt: rustfmt aiur execute + kernel shard


samuelburnham Jul 30, 2026
cf0c47e

remove diag_duplicate_wrappers forensics probe


samuelburnham Jul 30, 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


8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

20 changes: 14 additions & 6 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)

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

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

/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
 blocks ingressed as type-only axioms; only the partition knows which those
 are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
 disabled) is the keyed stub-consultation cache directory (normally
 `~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
 classification execute. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob foreignBlob stubbedBlob : ByteArray)
 (consultCacheDir : String := "") :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 (shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
 stubbedBlob consultCacheDir).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

@[extern "rs_aiur_system_verify"]
Expand Down

8 changes: 5 additions & 3 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →

@[extern "rs_aiur_toplevel_shard_check_with_env"]
private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
 @& ByteArray → Bool →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
 `checkAddrWithEnv` for `useBytecode` semantics. -/
def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (useBytecode : Bool := false)
 (ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
 : Except String (Array G × IOBuffer × Array QueryCount) :=
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
 stubbedBlob useBytecode).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

end Bytecode.Toplevel
Expand Down

32 changes: 26 additions & 6 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -137,11 +137,27 @@ Five variants in three families:
 the merkle tree rooted at `tree`. Used by aggregation to discharge
 leaves from a conditional claim's assumption set. Carries no
 assumptions.

`checkEnv` carries a second root, `stubbed`, naming the subset of
`assumptions` the claim ingressed as type-only axioms: their bodies were
withheld, so the claim holds given only their TYPES, and no reduction
passed through them.

The two roots are genuinely different sets, which is why one cannot serve
for both. A shard skips checking everything it does not own, but it must
still ingress in FULL anything it reduces through — a definition it
unfolds, or an inductive whose recursor rules it applies — even though
another shard is responsible for checking that constant. Those blocks are
in `assumptions` but NOT in `stubbed`. Folding them into the owned set
instead is not possible: owned sets partition the environment so each
constant is checked exactly once, and two shards may reduce through the
same constant.
-/
inductive Claim where
 | eval (input output : Address) (assumptions : Option Address)
 | check (const : Address) (assumptions : Option Address)
 | checkEnv (root : Address) (assumptions : Option Address)
 (stubbed : Option Address)
 | reveal (comm : Address) (info : RevealConstantInfo)
 | contains (tree : Address) (const : Address)
 deriving BEq, Repr, Inhabited
Expand DownExpand Up@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
 Serialize.put const
 putOptAddr assumptions
 | .checkEnv root assumptions => do
 | .checkEnv root assumptions stubbed => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
 Serialize.put root
 putOptAddr assumptions
 putOptAddr stubbed
 | .reveal comm info => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
 Serialize.put comm
Expand All@@ -523,7 +540,8 @@ def get : GetM Claim := do
 else if tag.size == VARIANT_CHECK_ENV_CLAIM then
 let root ← Serialize.get
 let asm ← getOptAddr
 return .checkEnv root asm
 let stubbed ← getOptAddr
 return .checkEnv root asm stubbed
 else if tag.size == VARIANT_REVEAL_CLAIM then
 return .reveal (← Serialize.get) (← RevealConstantInfo.get)
 else if tag.size == VARIANT_CONTAINS_CLAIM then
Expand All@@ -538,7 +556,7 @@ instance : ToString Claim where
 toString c := match c with
 | .eval i o asm => s!"Eval({i}, {o}, {asm})"
 | .check v asm => s!"Check({v}, {asm})"
 | .checkEnv r asm => s!"CheckEnv({r}, {asm})"
 | .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
 | .reveal comm info => s!"Reveal({comm}, {repr info})"
 | .contains t c => s!"Contains({t}, {c})"

Expand DownExpand Up@@ -566,7 +584,7 @@ namespace Proof
def variantOf : Ix.Claim → UInt64
 | .eval _ _ _ => Ix.Claim.VARIANT_EVAL_PROOF
 | .check _ _ => Ix.Claim.VARIANT_CHECK_PROOF
 | .checkEnv _ _  => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .reveal _ _ => Ix.Claim.VARIANT_REVEAL_PROOF
 | .contains _ _ => Ix.Claim.VARIANT_CONTAINS_PROOF

Expand All@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
 | .check addr asm => do
 Serialize.put addr
 Ix.Claim.putOptAddr asm
 | .checkEnv root asm => do
 | .checkEnv root asm stubbed => do
 Serialize.put root
 Ix.Claim.putOptAddr asm
 Ix.Claim.putOptAddr stubbed
 | .reveal comm info => do
 Serialize.put comm
 Ix.RevealConstantInfo.put info
Expand All@@ -609,7 +628,8 @@ def get : GetM Proof := do
 else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
 let root ← Serialize.get
 let asm ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm)
 let stubbed ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm stubbed)
 else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
 let comm ← Serialize.get
 let info ← Ix.RevealConstantInfo.get
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
feat(aiur): Measured-ingress sharding#524

New issue

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

 Sign up for GitHub

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

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
30
commits into

base:main
Choose a base branch

from

 Draft


feat(aiur): Measured-ingress sharding
#524
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


30 commits


Select commit
Hold shift + click to select a range
9b83f72

profile: per-metric block leaderboards (--top N, default 10)


samuelburnham Jul 22, 2026
41deee0

profile: record memo-unique substitutions (.ixprof v2)


samuelburnham Jul 24, 2026
ae4aab9

shard: calibrated Aiur cost model, profile/shard --backend aiur


samuelburnham Jul 24, 2026
645707b

profile: env-wide closure cost sweep (ix profile sweep)


samuelburnham Jul 24, 2026
f475ee0

shard: closure-union byte accounting for Aiur packing


samuelburnham Jul 28, 2026
5244868

shard: price Aiur ingress as frontier-trusted, not full-closure


samuelburnham Jul 28, 2026
bcfa8bc

tests: pin the const/blob classification of a non-ingressed ref


samuelburnham Jul 28, 2026
d2bf0fd

IxVM kernel: classify refs from the discriminator, poison the unresolved


samuelburnham Jul 28, 2026
0b47e09

IxVM kernel: ingress frontier constants as type-only axioms


samuelburnham Jul 28, 2026
688f2c8

claim: separate "not checked here" from "ingressed as a type-only stub"


samuelburnham Jul 28, 2026
176930a

diagnostics: name the missing IO key, count constants touched per check


samuelburnham Jul 28, 2026
9b26d2a

docs: Step 1 must be atomic — dual-field migration breaks node identity


samuelburnham Jul 28, 2026
83450a4

IxVM kernel: synthesize mutual-block member addresses


samuelburnham Jul 28, 2026
0bae7db

profile: record the measured touch graph, seed it FULL in Aiur packing


samuelburnham Jul 29, 2026
2f599ec

shard witnesses: measured ingress sets, wired end to end


samuelburnham Jul 29, 2026
be5cf4b

shard: per-shard stub-promotion rounds, price the emitted sets


samuelburnham Jul 29, 2026
cfa47a6

aiur: assert forensics in the interpreter, witness-set diagnosis probe


samuelburnham Jul 29, 2026
e16c108

repair driver: escalate divergent shards to a green partition


samuelburnham Jul 29, 2026
c86c344

kernel: report every wanted stub, making escalation fully targeted


samuelburnham Jul 29, 2026
b1e6bce

prove: batched, resumable all-shards mode with composed verdict


samuelburnham Jul 29, 2026
826f179

witness: ghost stubs — position-only entries, no bytes, no hashing


samuelburnham Jul 29, 2026
0bc3414

shard: persist whnf/def_eq/nat_arith per shard


samuelburnham Jul 30, 2026
3631500

merge prep: ghost-classification cache, shard-pipeline E2E test, pins


samuelburnham Jul 30, 2026
c029f54

caches: digest-keyed ~/.ix/cache replaces CSV sidecars; ghost -> addr…


samuelburnham Jul 30, 2026
ca25fa5

fmt: rustfmt ix-ffi


samuelburnham Jul 30, 2026
e1feae1

rebase reconcile: regen codegen against main's kernel, refresh FFT pins


samuelburnham Jul 30, 2026
f3c3583

bench: aiur-shard backend — planner metrics + heavy-shard execution


samuelburnham Jul 30, 2026
08ef90c

bench: register Init as a benchmark env


samuelburnham Jul 30, 2026
60b9457

fmt: rustfmt aiur execute + kernel shard


samuelburnham Jul 30, 2026
cf0c47e

remove diag_duplicate_wrappers forensics probe


samuelburnham Jul 30, 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


8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

20 changes: 14 additions & 6 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)

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

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

/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
 blocks ingressed as type-only axioms; only the partition knows which those
 are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
 disabled) is the keyed stub-consultation cache directory (normally
 `~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
 classification execute. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob foreignBlob stubbedBlob : ByteArray)
 (consultCacheDir : String := "") :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 (shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
 stubbedBlob consultCacheDir).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

@[extern "rs_aiur_system_verify"]
Expand Down

8 changes: 5 additions & 3 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →

@[extern "rs_aiur_toplevel_shard_check_with_env"]
private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
 @& ByteArray → Bool →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
 `checkAddrWithEnv` for `useBytecode` semantics. -/
def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (useBytecode : Bool := false)
 (ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
 : Except String (Array G × IOBuffer × Array QueryCount) :=
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
 stubbedBlob useBytecode).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

end Bytecode.Toplevel
Expand Down

32 changes: 26 additions & 6 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -137,11 +137,27 @@ Five variants in three families:
 the merkle tree rooted at `tree`. Used by aggregation to discharge
 leaves from a conditional claim's assumption set. Carries no
 assumptions.

`checkEnv` carries a second root, `stubbed`, naming the subset of
`assumptions` the claim ingressed as type-only axioms: their bodies were
withheld, so the claim holds given only their TYPES, and no reduction
passed through them.

The two roots are genuinely different sets, which is why one cannot serve
for both. A shard skips checking everything it does not own, but it must
still ingress in FULL anything it reduces through — a definition it
unfolds, or an inductive whose recursor rules it applies — even though
another shard is responsible for checking that constant. Those blocks are
in `assumptions` but NOT in `stubbed`. Folding them into the owned set
instead is not possible: owned sets partition the environment so each
constant is checked exactly once, and two shards may reduce through the
same constant.
-/
inductive Claim where
 | eval (input output : Address) (assumptions : Option Address)
 | check (const : Address) (assumptions : Option Address)
 | checkEnv (root : Address) (assumptions : Option Address)
 (stubbed : Option Address)
 | reveal (comm : Address) (info : RevealConstantInfo)
 | contains (tree : Address) (const : Address)
 deriving BEq, Repr, Inhabited
Expand DownExpand Up@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
 Serialize.put const
 putOptAddr assumptions
 | .checkEnv root assumptions => do
 | .checkEnv root assumptions stubbed => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
 Serialize.put root
 putOptAddr assumptions
 putOptAddr stubbed
 | .reveal comm info => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
 Serialize.put comm
Expand All@@ -523,7 +540,8 @@ def get : GetM Claim := do
 else if tag.size == VARIANT_CHECK_ENV_CLAIM then
 let root ← Serialize.get
 let asm ← getOptAddr
 return .checkEnv root asm
 let stubbed ← getOptAddr
 return .checkEnv root asm stubbed
 else if tag.size == VARIANT_REVEAL_CLAIM then
 return .reveal (← Serialize.get) (← RevealConstantInfo.get)
 else if tag.size == VARIANT_CONTAINS_CLAIM then
Expand All@@ -538,7 +556,7 @@ instance : ToString Claim where
 toString c := match c with
 | .eval i o asm => s!"Eval({i}, {o}, {asm})"
 | .check v asm => s!"Check({v}, {asm})"
 | .checkEnv r asm => s!"CheckEnv({r}, {asm})"
 | .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
 | .reveal comm info => s!"Reveal({comm}, {repr info})"
 | .contains t c => s!"Contains({t}, {c})"

Expand DownExpand Up@@ -566,7 +584,7 @@ namespace Proof
def variantOf : Ix.Claim → UInt64
 | .eval _ _ _ => Ix.Claim.VARIANT_EVAL_PROOF
 | .check _ _ => Ix.Claim.VARIANT_CHECK_PROOF
 | .checkEnv _ _  => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .reveal _ _ => Ix.Claim.VARIANT_REVEAL_PROOF
 | .contains _ _ => Ix.Claim.VARIANT_CONTAINS_PROOF

Expand All@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
 | .check addr asm => do
 Serialize.put addr
 Ix.Claim.putOptAddr asm
 | .checkEnv root asm => do
 | .checkEnv root asm stubbed => do
 Serialize.put root
 Ix.Claim.putOptAddr asm
 Ix.Claim.putOptAddr stubbed
 | .reveal comm info => do
 Serialize.put comm
 Ix.RevealConstantInfo.put info
Expand All@@ -609,7 +628,8 @@ def get : GetM Proof := do
 else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
 let root ← Serialize.get
 let asm ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm)
 let stubbed ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm stubbed)
 else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
 let comm ← Serialize.get
 let info ← Ix.RevealConstantInfo.get
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
feat(aiur): Measured-ingress sharding#524

New issue

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

 Sign up for GitHub

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

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
30
commits into

base:main
Choose a base branch

from

 Draft


feat(aiur): Measured-ingress sharding
#524
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


30 commits


Select commit
Hold shift + click to select a range
9b83f72

profile: per-metric block leaderboards (--top N, default 10)


samuelburnham Jul 22, 2026
41deee0

profile: record memo-unique substitutions (.ixprof v2)


samuelburnham Jul 24, 2026
ae4aab9

shard: calibrated Aiur cost model, profile/shard --backend aiur


samuelburnham Jul 24, 2026
645707b

profile: env-wide closure cost sweep (ix profile sweep)


samuelburnham Jul 24, 2026
f475ee0

shard: closure-union byte accounting for Aiur packing


samuelburnham Jul 28, 2026
5244868

shard: price Aiur ingress as frontier-trusted, not full-closure


samuelburnham Jul 28, 2026
bcfa8bc

tests: pin the const/blob classification of a non-ingressed ref


samuelburnham Jul 28, 2026
d2bf0fd

IxVM kernel: classify refs from the discriminator, poison the unresolved


samuelburnham Jul 28, 2026
0b47e09

IxVM kernel: ingress frontier constants as type-only axioms


samuelburnham Jul 28, 2026
688f2c8

claim: separate "not checked here" from "ingressed as a type-only stub"


samuelburnham Jul 28, 2026
176930a

diagnostics: name the missing IO key, count constants touched per check


samuelburnham Jul 28, 2026
9b26d2a

docs: Step 1 must be atomic — dual-field migration breaks node identity


samuelburnham Jul 28, 2026
83450a4

IxVM kernel: synthesize mutual-block member addresses


samuelburnham Jul 28, 2026
0bae7db

profile: record the measured touch graph, seed it FULL in Aiur packing


samuelburnham Jul 29, 2026
2f599ec

shard witnesses: measured ingress sets, wired end to end


samuelburnham Jul 29, 2026
be5cf4b

shard: per-shard stub-promotion rounds, price the emitted sets


samuelburnham Jul 29, 2026
cfa47a6

aiur: assert forensics in the interpreter, witness-set diagnosis probe


samuelburnham Jul 29, 2026
e16c108

repair driver: escalate divergent shards to a green partition


samuelburnham Jul 29, 2026
c86c344

kernel: report every wanted stub, making escalation fully targeted


samuelburnham Jul 29, 2026
b1e6bce

prove: batched, resumable all-shards mode with composed verdict


samuelburnham Jul 29, 2026
826f179

witness: ghost stubs — position-only entries, no bytes, no hashing


samuelburnham Jul 29, 2026
0bc3414

shard: persist whnf/def_eq/nat_arith per shard


samuelburnham Jul 30, 2026
3631500

merge prep: ghost-classification cache, shard-pipeline E2E test, pins


samuelburnham Jul 30, 2026
c029f54

caches: digest-keyed ~/.ix/cache replaces CSV sidecars; ghost -> addr…


samuelburnham Jul 30, 2026
ca25fa5

fmt: rustfmt ix-ffi


samuelburnham Jul 30, 2026
e1feae1

rebase reconcile: regen codegen against main's kernel, refresh FFT pins


samuelburnham Jul 30, 2026
f3c3583

bench: aiur-shard backend — planner metrics + heavy-shard execution


samuelburnham Jul 30, 2026
08ef90c

bench: register Init as a benchmark env


samuelburnham Jul 30, 2026
60b9457

fmt: rustfmt aiur execute + kernel shard


samuelburnham Jul 30, 2026
cf0c47e

remove diag_duplicate_wrappers forensics probe


samuelburnham Jul 30, 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


8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

20 changes: 14 additions & 6 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)

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

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

/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
 blocks ingressed as type-only axioms; only the partition knows which those
 are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
 disabled) is the keyed stub-consultation cache directory (normally
 `~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
 classification execute. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob foreignBlob stubbedBlob : ByteArray)
 (consultCacheDir : String := "") :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 (shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
 stubbedBlob consultCacheDir).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

@[extern "rs_aiur_system_verify"]
Expand Down

8 changes: 5 additions & 3 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →

@[extern "rs_aiur_toplevel_shard_check_with_env"]
private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
 @& ByteArray → Bool →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
 `checkAddrWithEnv` for `useBytecode` semantics. -/
def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (useBytecode : Bool := false)
 (ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
 : Except String (Array G × IOBuffer × Array QueryCount) :=
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
 stubbedBlob useBytecode).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

end Bytecode.Toplevel
Expand Down

32 changes: 26 additions & 6 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -137,11 +137,27 @@ Five variants in three families:
 the merkle tree rooted at `tree`. Used by aggregation to discharge
 leaves from a conditional claim's assumption set. Carries no
 assumptions.

`checkEnv` carries a second root, `stubbed`, naming the subset of
`assumptions` the claim ingressed as type-only axioms: their bodies were
withheld, so the claim holds given only their TYPES, and no reduction
passed through them.

The two roots are genuinely different sets, which is why one cannot serve
for both. A shard skips checking everything it does not own, but it must
still ingress in FULL anything it reduces through — a definition it
unfolds, or an inductive whose recursor rules it applies — even though
another shard is responsible for checking that constant. Those blocks are
in `assumptions` but NOT in `stubbed`. Folding them into the owned set
instead is not possible: owned sets partition the environment so each
constant is checked exactly once, and two shards may reduce through the
same constant.
-/
inductive Claim where
 | eval (input output : Address) (assumptions : Option Address)
 | check (const : Address) (assumptions : Option Address)
 | checkEnv (root : Address) (assumptions : Option Address)
 (stubbed : Option Address)
 | reveal (comm : Address) (info : RevealConstantInfo)
 | contains (tree : Address) (const : Address)
 deriving BEq, Repr, Inhabited
Expand DownExpand Up@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
 Serialize.put const
 putOptAddr assumptions
 | .checkEnv root assumptions => do
 | .checkEnv root assumptions stubbed => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
 Serialize.put root
 putOptAddr assumptions
 putOptAddr stubbed
 | .reveal comm info => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
 Serialize.put comm
Expand All@@ -523,7 +540,8 @@ def get : GetM Claim := do
 else if tag.size == VARIANT_CHECK_ENV_CLAIM then
 let root ← Serialize.get
 let asm ← getOptAddr
 return .checkEnv root asm
 let stubbed ← getOptAddr
 return .checkEnv root asm stubbed
 else if tag.size == VARIANT_REVEAL_CLAIM then
 return .reveal (← Serialize.get) (← RevealConstantInfo.get)
 else if tag.size == VARIANT_CONTAINS_CLAIM then
Expand All@@ -538,7 +556,7 @@ instance : ToString Claim where
 toString c := match c with
 | .eval i o asm => s!"Eval({i}, {o}, {asm})"
 | .check v asm => s!"Check({v}, {asm})"
 | .checkEnv r asm => s!"CheckEnv({r}, {asm})"
 | .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
 | .reveal comm info => s!"Reveal({comm}, {repr info})"
 | .contains t c => s!"Contains({t}, {c})"

Expand DownExpand Up@@ -566,7 +584,7 @@ namespace Proof
def variantOf : Ix.Claim → UInt64
 | .eval _ _ _ => Ix.Claim.VARIANT_EVAL_PROOF
 | .check _ _ => Ix.Claim.VARIANT_CHECK_PROOF
 | .checkEnv _ _  => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .reveal _ _ => Ix.Claim.VARIANT_REVEAL_PROOF
 | .contains _ _ => Ix.Claim.VARIANT_CONTAINS_PROOF

Expand All@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
 | .check addr asm => do
 Serialize.put addr
 Ix.Claim.putOptAddr asm
 | .checkEnv root asm => do
 | .checkEnv root asm stubbed => do
 Serialize.put root
 Ix.Claim.putOptAddr asm
 Ix.Claim.putOptAddr stubbed
 | .reveal comm info => do
 Serialize.put comm
 Ix.RevealConstantInfo.put info
Expand All@@ -609,7 +628,8 @@ def get : GetM Proof := do
 else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
 let root ← Serialize.get
 let asm ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm)
 let stubbed ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm stubbed)
 else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
 let comm ← Serialize.get
 let info ← Ix.RevealConstantInfo.get
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
feat(aiur): Measured-ingress sharding#524

New issue

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

 Sign up for GitHub

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

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
30
commits into

base:main
Choose a base branch

from

 Draft


feat(aiur): Measured-ingress sharding
#524
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


30 commits


Select commit
Hold shift + click to select a range
9b83f72

profile: per-metric block leaderboards (--top N, default 10)


samuelburnham Jul 22, 2026
41deee0

profile: record memo-unique substitutions (.ixprof v2)


samuelburnham Jul 24, 2026
ae4aab9

shard: calibrated Aiur cost model, profile/shard --backend aiur


samuelburnham Jul 24, 2026
645707b

profile: env-wide closure cost sweep (ix profile sweep)


samuelburnham Jul 24, 2026
f475ee0

shard: closure-union byte accounting for Aiur packing


samuelburnham Jul 28, 2026
5244868

shard: price Aiur ingress as frontier-trusted, not full-closure


samuelburnham Jul 28, 2026
bcfa8bc

tests: pin the const/blob classification of a non-ingressed ref


samuelburnham Jul 28, 2026
d2bf0fd

IxVM kernel: classify refs from the discriminator, poison the unresolved


samuelburnham Jul 28, 2026
0b47e09

IxVM kernel: ingress frontier constants as type-only axioms


samuelburnham Jul 28, 2026
688f2c8

claim: separate "not checked here" from "ingressed as a type-only stub"


samuelburnham Jul 28, 2026
176930a

diagnostics: name the missing IO key, count constants touched per check


samuelburnham Jul 28, 2026
9b26d2a

docs: Step 1 must be atomic — dual-field migration breaks node identity


samuelburnham Jul 28, 2026
83450a4

IxVM kernel: synthesize mutual-block member addresses


samuelburnham Jul 28, 2026
0bae7db

profile: record the measured touch graph, seed it FULL in Aiur packing


samuelburnham Jul 29, 2026
2f599ec

shard witnesses: measured ingress sets, wired end to end


samuelburnham Jul 29, 2026
be5cf4b

shard: per-shard stub-promotion rounds, price the emitted sets


samuelburnham Jul 29, 2026
cfa47a6

aiur: assert forensics in the interpreter, witness-set diagnosis probe


samuelburnham Jul 29, 2026
e16c108

repair driver: escalate divergent shards to a green partition


samuelburnham Jul 29, 2026
c86c344

kernel: report every wanted stub, making escalation fully targeted


samuelburnham Jul 29, 2026
b1e6bce

prove: batched, resumable all-shards mode with composed verdict


samuelburnham Jul 29, 2026
826f179

witness: ghost stubs — position-only entries, no bytes, no hashing


samuelburnham Jul 29, 2026
0bc3414

shard: persist whnf/def_eq/nat_arith per shard


samuelburnham Jul 30, 2026
3631500

merge prep: ghost-classification cache, shard-pipeline E2E test, pins


samuelburnham Jul 30, 2026
c029f54

caches: digest-keyed ~/.ix/cache replaces CSV sidecars; ghost -> addr…


samuelburnham Jul 30, 2026
ca25fa5

fmt: rustfmt ix-ffi


samuelburnham Jul 30, 2026
e1feae1

rebase reconcile: regen codegen against main's kernel, refresh FFT pins


samuelburnham Jul 30, 2026
f3c3583

bench: aiur-shard backend — planner metrics + heavy-shard execution


samuelburnham Jul 30, 2026
08ef90c

bench: register Init as a benchmark env


samuelburnham Jul 30, 2026
60b9457

fmt: rustfmt aiur execute + kernel shard


samuelburnham Jul 30, 2026
cf0c47e

remove diag_duplicate_wrappers forensics probe


samuelburnham Jul 30, 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


8 changes: 4 additions & 4 deletions
.github/workflows/bencher-thresholds-reset.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -22,7 +22,7 @@ name: Bencher thresholds reset
# cancel by removing it before merge. Naming convention: one label per token,
# `bencher-thresholds-reset:<token>` where <token> is a workload (a backend
# testbed in Ix/Cli/BenchCmd.lean (backendSpecs) minus its runner-arch suffix:
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `ix-compile`, `ix-decompile`, `aiur-check-execute`, `aiur-check-prove`, `aiur-check-recursive`, `aiur-recursive`, `aiur-shard`, `zisk-check-execute`, `sp1-check-execute`, `ooc-check`) or
# `all` (the merge step expands an `all` label into every workload). Labeling
# requires Triage+, so PR authors from forks cannot self-queue a reset. The
# label shares the command/workflow name; the ref it moves is
Expand All@@ -44,7 +44,7 @@ on:
 # GitHub requires literal choice options, so this list stays static:
 # keep it (and the jobs' valid= lists below) in sync with the
 # backend testbeds in Ix/Cli/BenchCmd.lean (backendSpecs).
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, zisk-check-execute, sp1-check-execute, ooc-check, all]
 options: [ix-compile, ix-decompile, aiur-check-execute, aiur-check-prove, aiur-check-recursive, aiur-recursive, aiur-shard, zisk-check-execute, sp1-check-execute, ooc-check, all]
 sha:
 description: "Commit to anchor to (default: HEAD)"
 required: false
Expand DownExpand Up@@ -77,7 +77,7 @@ jobs:
 # (backendSpecs) minus the runner-arch suffix. Static because this
 # job runs on a cheap runner with no built `ix`; keep in sync when
 # adding a backend.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 if [ "$EVENT" = workflow_dispatch ]; then
 # Reset the chosen workload(s) at the given commit; no PR scan.
 sha="${INPUT_SHA:-$HEAD_SHA}"
Expand DownExpand Up@@ -133,7 +133,7 @@ jobs:
 # which the merge job expands into every workload). Same static
 # list as the reset job; keep both in sync with backendSpecs in
 # Ix/Cli/BenchCmd.lean.
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 valid="aiur-check-execute aiur-check-prove aiur-check-recursive aiur-recursive aiur-shard ix-compile ix-decompile ooc-check sp1-check-execute zisk-check-execute"
 accepted="$valid all"
 # Parse the workload token(s) after the command, lowercased.
 workloads=$(printf '%s' "$BODY" \
Expand Down

20 changes: 14 additions & 6 deletions
Ix/Aiur/Protocol.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -138,14 +138,22 @@ def proveAddrWithEnv (system : @& AiurSystem)

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

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

/-- Per-shard prove against a Rust-owned `EnvHandle`. `stubbedBlob` names the
 blocks ingressed as type-only axioms; only the partition knows which those
 are, so it travels from the `.ixes` manifest. `consultCacheDir` (empty =
 disabled) is the keyed stub-consultation cache directory (normally
 `~/.ix/cache/stub-consults`, one file per claim digest); a hit skips the
 classification execute. -/
def shardProveWithEnv (system : @& AiurSystem)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob foreignBlob stubbedBlob : ByteArray)
 (consultCacheDir : String := "") :
 Except String (ByteArray × Proof × IOBuffer) :=
 (shardProveWithEnv' system funIdx envHandle ownedBlob).map
 (shardProveWithEnv' system funIdx envHandle ownedBlob foreignBlob
 stubbedBlob consultCacheDir).map
 fun r => (r.claimBytes, r.proof, .ofArrays r.ioData r.ioMap)

@[extern "rs_aiur_system_verify"]
Expand Down

8 changes: 5 additions & 3 deletions
Ix/Aiur/Semantics/BytecodeFfi.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -186,7 +186,8 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →

@[extern "rs_aiur_toplevel_shard_check_with_env"]
private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
 @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → @& ByteArray →
 @& ByteArray → Bool →
 Except String ExecuteResult

/-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
Expand All@@ -206,9 +207,10 @@ def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
 `checkAddrWithEnv` for `useBytecode` semantics. -/
def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
 (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
 (ownedBlob : ByteArray) (useBytecode : Bool := false)
 (ownedBlob foreignBlob stubbedBlob : ByteArray) (useBytecode : Bool := false)
 : Except String (Array G × IOBuffer × Array QueryCount) :=
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob useBytecode).map
 (shardCheckWithEnv' toplevel funIdx envHandle ownedBlob foreignBlob
 stubbedBlob useBytecode).map
 fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)

end Bytecode.Toplevel
Expand Down

32 changes: 26 additions & 6 deletions
Ix/Claim.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -137,11 +137,27 @@ Five variants in three families:
 the merkle tree rooted at `tree`. Used by aggregation to discharge
 leaves from a conditional claim's assumption set. Carries no
 assumptions.

`checkEnv` carries a second root, `stubbed`, naming the subset of
`assumptions` the claim ingressed as type-only axioms: their bodies were
withheld, so the claim holds given only their TYPES, and no reduction
passed through them.

The two roots are genuinely different sets, which is why one cannot serve
for both. A shard skips checking everything it does not own, but it must
still ingress in FULL anything it reduces through — a definition it
unfolds, or an inductive whose recursor rules it applies — even though
another shard is responsible for checking that constant. Those blocks are
in `assumptions` but NOT in `stubbed`. Folding them into the owned set
instead is not possible: owned sets partition the environment so each
constant is checked exactly once, and two shards may reduce through the
same constant.
-/
inductive Claim where
 | eval (input output : Address) (assumptions : Option Address)
 | check (const : Address) (assumptions : Option Address)
 | checkEnv (root : Address) (assumptions : Option Address)
 (stubbed : Option Address)
 | reveal (comm : Address) (info : RevealConstantInfo)
 | contains (tree : Address) (const : Address)
 deriving BEq, Repr, Inhabited
Expand DownExpand Up@@ -494,10 +510,11 @@ def put : Claim → PutM Unit
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_CLAIM⟩
 Serialize.put const
 putOptAddr assumptions
 | .checkEnv root assumptions => do
 | .checkEnv root assumptions stubbed => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_CHECK_ENV_CLAIM⟩
 Serialize.put root
 putOptAddr assumptions
 putOptAddr stubbed
 | .reveal comm info => do
 putTag4 ⟨FLAG_CLAIM, VARIANT_REVEAL_CLAIM⟩
 Serialize.put comm
Expand All@@ -523,7 +540,8 @@ def get : GetM Claim := do
 else if tag.size == VARIANT_CHECK_ENV_CLAIM then
 let root ← Serialize.get
 let asm ← getOptAddr
 return .checkEnv root asm
 let stubbed ← getOptAddr
 return .checkEnv root asm stubbed
 else if tag.size == VARIANT_REVEAL_CLAIM then
 return .reveal (← Serialize.get) (← RevealConstantInfo.get)
 else if tag.size == VARIANT_CONTAINS_CLAIM then
Expand All@@ -538,7 +556,7 @@ instance : ToString Claim where
 toString c := match c with
 | .eval i o asm => s!"Eval({i}, {o}, {asm})"
 | .check v asm => s!"Check({v}, {asm})"
 | .checkEnv r asm => s!"CheckEnv({r}, {asm})"
 | .checkEnv r asm st => s!"CheckEnv({r}, {asm}, {st})"
 | .reveal comm info => s!"Reveal({comm}, {repr info})"
 | .contains t c => s!"Contains({t}, {c})"

Expand DownExpand Up@@ -566,7 +584,7 @@ namespace Proof
def variantOf : Ix.Claim → UInt64
 | .eval _ _ _ => Ix.Claim.VARIANT_EVAL_PROOF
 | .check _ _ => Ix.Claim.VARIANT_CHECK_PROOF
 | .checkEnv _ _  => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .checkEnv _ _ _ => Ix.Claim.VARIANT_CHECK_ENV_PROOF
 | .reveal _ _ => Ix.Claim.VARIANT_REVEAL_PROOF
 | .contains _ _ => Ix.Claim.VARIANT_CONTAINS_PROOF

Expand All@@ -580,9 +598,10 @@ def put (p : Proof) : PutM Unit := do
 | .check addr asm => do
 Serialize.put addr
 Ix.Claim.putOptAddr asm
 | .checkEnv root asm => do
 | .checkEnv root asm stubbed => do
 Serialize.put root
 Ix.Claim.putOptAddr asm
 Ix.Claim.putOptAddr stubbed
 | .reveal comm info => do
 Serialize.put comm
 Ix.RevealConstantInfo.put info
Expand All@@ -609,7 +628,8 @@ def get : GetM Proof := do
 else if tag.size == Ix.Claim.VARIANT_CHECK_ENV_PROOF then do
 let root ← Serialize.get
 let asm ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm)
 let stubbed ← Ix.Claim.getOptAddr
 pure (.checkEnv root asm stubbed)
 else if tag.size == Ix.Claim.VARIANT_REVEAL_PROOF then do
 let comm ← Serialize.get
 let info ← Ix.RevealConstantInfo.get
Expand Down
Loading