IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface#457

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 5 commits into from
Jul 2, 2026
Merged

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7efebe6
IxVM kernel: augment addr_pos_map with blob-ref sentinels
arthurpaulino Jun 24, 2026
bae332e
IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passing
arthurpaulino Jun 27, 2026
64390ad
IxVM: per-kind IOBuffer channels with documented interface
arthurpaulino Jun 27, 2026
1fb0dd1
IxVM Blake3: inline blake3_flat at its two call sites
arthurpaulino Jul 2, 2026
b84a500
IxVM kernel: KLevel = &KLevelNode (pass universes by pointer)
arthurpaulino Jul 2, 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
88 changes: 34 additions & 54 deletions Ix/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,89 +45,69 @@ def entrypoints := ⟦
}

fn level_cmp_tests() {
let zero = store(KLevelNode.Zero);
let p0 = store(KLevelNode.Param(0));
let p1 = store(KLevelNode.Param(1));
let succ_p0 = store(KLevelNode.Succ(p0));
let succ_zero = store(KLevelNode.Succ(zero));

-- Zero ≤ anything
assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
assert_eq!(level_leq(zero, p0), 1);

-- Param(u) ≤ Param(u) (reflexivity)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1);
assert_eq!(level_leq(p0, p0), 1);

-- Param(u) ≤ Param(v) fails (u ≠ v, set u > v)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0);
assert_eq!(level_leq(p0, p1), 0);

-- Succ(u) ≤ Succ(u) (peel both succs)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, succ_p0), 1);

-- Succ(u) ≤ u fails (u+1 > u at any assignment)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Param(0)), 0);

-- === level_leq: Param ≤ Succ reduction ===

-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u)
assert_eq!(level_leq(
KLevel.Param(0),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, p0), 0);

-- === level_leq: Max distribution ===
-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1)
assert_eq!(level_leq(p0, succ_p0), 1);

-- max(u, v) ≤ max(u, v) (reflexivity via distribution)
let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1)));
let max_uv = store(KLevelNode.Max(p0, p1));
assert_eq!(level_leq(max_uv, max_uv), 1);

-- u ≤ max(u, v) (try-each-branch: first branch succeeds)
assert_eq!(level_leq(KLevel.Param(0), max_uv), 1);
-- u ≤ max(u, v)
assert_eq!(level_leq(p0, max_uv), 1);

-- max(u, v) ≤ u fails (set v > u)
assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0);
-- max(u, v) ≤ u fails
assert_eq!(level_leq(max_uv, p0), 0);

-- === level_leq: IMax case-splitting ===

-- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max)
let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1)));
-- imax(u, v) ≤ max(u, v)
let imax_uv = store(KLevelNode.IMax(p0, p1));
assert_eq!(level_leq(imax_uv, max_uv), 1);

-- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1)
-- max(u, v) ≤ imax(u, v) fails
assert_eq!(level_leq(max_uv, imax_uv), 0);

-- === level_leq: Succ ≤ Max with IMax child (the case-split fix) ===

-- u+1 = max(1, imax(u+1, u)): equal for all σ
-- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1
-- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1
-- This is the case that requires case-splitting through Max when
-- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)).
let a = KLevel.Succ(store(KLevel.Param(0)));
let b = KLevel.Max(
store(KLevel.Succ(store(KLevel.Zero))),
store(KLevel.IMax(
store(KLevel.Succ(store(KLevel.Param(0)))),
store(KLevel.Param(0)))));
-- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix)
let a = succ_p0;
let b = store(KLevelNode.Max(
succ_zero,
store(KLevelNode.IMax(succ_p0, p0))));
assert_eq!(level_equal(a, b), 1);

-- === level_equal: semantic equality ===

-- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u)
assert_eq!(level_equal(
KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))),
KLevel.Param(0)), 1);
-- imax(u, u) = u
assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1);

-- max(u, 0) = u
assert_eq!(level_equal(
KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)),
KLevel.Param(0)), 1);
assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1);

-- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0
let succ_v = KLevel.Succ(store(KLevel.Param(1)));
let succ_v = store(KLevelNode.Succ(p1));
assert_eq!(level_eq(
level_imax(KLevel.Param(0), succ_v),
KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1);
level_imax(p0, succ_v),
store(KLevelNode.Max(p0, succ_v))), 1);

assert_eq!(level_eq(
level_imax(KLevel.Param(0), KLevel.Zero),
KLevel.Zero), 1);
level_imax(p0, zero),
zero), 1);
}

pub fn kernel_unit_tests() {
Expand Down
34 changes: 34 additions & 0 deletions Ix/IxVM/Blake3.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,6 +45,40 @@ def blake3 := ⟦
blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
}

-- Hash `bytes` and assert the digest equals `expected`. Used by every
-- IOBuffer-load path that verifies the pre-image of a content-addressed
-- pointer matches the bytes the prover supplied.
fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
let h = blake3(bytes);
assert_eq!(
[h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]],
expected);
()
}

-- Hash `bytes` and intern the digest into the Store. Returned pointer is
-- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
-- site that synthesises an address from raw bytes (e.g. `expr_addr`,
-- `leaf_hash`, `node_hash`, `cprj_content_addr`).
fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
let h = blake3(bytes);
store([h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]])
}

fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
match layer {
Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),
Expand Down
63 changes: 46 additions & 17 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
| .abbrev => .ofNat 0xFFFFFFFF
| .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)

/-! ## IxVM IOBuffer interface

The host seeds blake3-keyed payloads on six channels; the Aiur kernel
consumes them via `io_get_info` + `#read_byte_stream`. One value shape
per channel — no overloading, no in-band discriminators.

Tiered by access pattern (matches kernel runtime order):

| Tier | Channel | Purpose | Key (32 G) | Value shape |
|--------|---------|--------------------------|-------------------------|-------------------|
| Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes |
| Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes |
| Const | 2 | constant wire bytes | const addr | const bytes |
| Const | 3 | Defn reducibility hint | Defn addr | single G |
| Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) |
| Blob | 5 | blob raw bytes | blob addr | raw bytes |

Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
fires per blob ref encountered during `build_ref_idxs_and_blobs`.

Soundness:
* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
against its content-addressed key.
* ch 3 — semantically optional; controls WHNF reduction heuristic
only, def-eq is sound either way.
* ch 4 — sound by erasure-correctness: a lying discriminator flips
the const/blob decision and the wrong-path load downstream fails
(a "const" blob triggers a ch 2 read returning empty → blake3
verify against the non-empty addr fails; a "blob" const dangles
references → typecheck fail).

Channel numbers MUST stay in sync with the inlined `io_get_info` /
`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
`Ix/IxVM/Kernel/Claim.lean`.
-/

/-- Insert all per-address entries for `addr`s satisfying `keep` into
`ioBuffer`. Each address kind lives on its own channel; the key is
always the 32-G blake3 hash, with no disambiguating suffix.

| channel | key (32 G) | value | meaning |
|---------|------------|----------------|---------|
| 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) |
| 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) |
| 2 | `addr` | single G | Defn `ReducibilityHints` encoding |

Blob addrs also get an empty entry on channel 0 so the kernel's
constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
works without a separate query path. -/
`ioBuffer`. See the channel table above. -/
def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
(ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
let mut ioBuffer := ioBuffer
Expand All@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
-- serialized form the lazy entry holds — no materialization needed.
let bytes := lc.rawBytes
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
-- Discriminator: this addr resolves to a constant.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
for (addr, rawBytes) in ixonEnv.blobs do
if !keep addr then continue
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
ioBuffer := ioBuffer.extend 0 key #[]
ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
-- Discriminator: this addr resolves to a blob.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
for (_, named) in ixonEnv.named do
if !keep named.addr then continue
match named.constMeta with
| .defn _ _ hints _ _ _ _ _ =>
let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
| _ => pure ()
return ioBuffer

Expand DownExpand Up@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
match trees.get? root with
| some tree =>
let bytes := Ix.AssumptionTree.ser tree
.ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
.ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
| none => .error s!"no assumption tree supplied for root {root}"

/-- Build the witness for `verify_claim` against `claim`.
Expand Down
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all \u003cpre\u003e\u003ccode\u003e blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks"); } } catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); } })(); (function(){ try { var __m = "github.com"; var __re = new RegExp('^' + "github\\.com" + '
Skip to content

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface#457

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 5 commits into from
Jul 2, 2026
Merged

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7efebe6
IxVM kernel: augment addr_pos_map with blob-ref sentinels
arthurpaulino Jun 24, 2026
bae332e
IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passing
arthurpaulino Jun 27, 2026
64390ad
IxVM: per-kind IOBuffer channels with documented interface
arthurpaulino Jun 27, 2026
1fb0dd1
IxVM Blake3: inline blake3_flat at its two call sites
arthurpaulino Jul 2, 2026
b84a500
IxVM kernel: KLevel = &KLevelNode (pass universes by pointer)
arthurpaulino Jul 2, 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
88 changes: 34 additions & 54 deletions Ix/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,89 +45,69 @@ def entrypoints := ⟦
}

fn level_cmp_tests() {
let zero = store(KLevelNode.Zero);
let p0 = store(KLevelNode.Param(0));
let p1 = store(KLevelNode.Param(1));
let succ_p0 = store(KLevelNode.Succ(p0));
let succ_zero = store(KLevelNode.Succ(zero));

-- Zero ≤ anything
assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
assert_eq!(level_leq(zero, p0), 1);

-- Param(u) ≤ Param(u) (reflexivity)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1);
assert_eq!(level_leq(p0, p0), 1);

-- Param(u) ≤ Param(v) fails (u ≠ v, set u > v)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0);
assert_eq!(level_leq(p0, p1), 0);

-- Succ(u) ≤ Succ(u) (peel both succs)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, succ_p0), 1);

-- Succ(u) ≤ u fails (u+1 > u at any assignment)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Param(0)), 0);

-- === level_leq: Param ≤ Succ reduction ===

-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u)
assert_eq!(level_leq(
KLevel.Param(0),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, p0), 0);

-- === level_leq: Max distribution ===
-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1)
assert_eq!(level_leq(p0, succ_p0), 1);

-- max(u, v) ≤ max(u, v) (reflexivity via distribution)
let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1)));
let max_uv = store(KLevelNode.Max(p0, p1));
assert_eq!(level_leq(max_uv, max_uv), 1);

-- u ≤ max(u, v) (try-each-branch: first branch succeeds)
assert_eq!(level_leq(KLevel.Param(0), max_uv), 1);
-- u ≤ max(u, v)
assert_eq!(level_leq(p0, max_uv), 1);

-- max(u, v) ≤ u fails (set v > u)
assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0);
-- max(u, v) ≤ u fails
assert_eq!(level_leq(max_uv, p0), 0);

-- === level_leq: IMax case-splitting ===

-- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max)
let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1)));
-- imax(u, v) ≤ max(u, v)
let imax_uv = store(KLevelNode.IMax(p0, p1));
assert_eq!(level_leq(imax_uv, max_uv), 1);

-- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1)
-- max(u, v) ≤ imax(u, v) fails
assert_eq!(level_leq(max_uv, imax_uv), 0);

-- === level_leq: Succ ≤ Max with IMax child (the case-split fix) ===

-- u+1 = max(1, imax(u+1, u)): equal for all σ
-- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1
-- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1
-- This is the case that requires case-splitting through Max when
-- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)).
let a = KLevel.Succ(store(KLevel.Param(0)));
let b = KLevel.Max(
store(KLevel.Succ(store(KLevel.Zero))),
store(KLevel.IMax(
store(KLevel.Succ(store(KLevel.Param(0)))),
store(KLevel.Param(0)))));
-- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix)
let a = succ_p0;
let b = store(KLevelNode.Max(
succ_zero,
store(KLevelNode.IMax(succ_p0, p0))));
assert_eq!(level_equal(a, b), 1);

-- === level_equal: semantic equality ===

-- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u)
assert_eq!(level_equal(
KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))),
KLevel.Param(0)), 1);
-- imax(u, u) = u
assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1);

-- max(u, 0) = u
assert_eq!(level_equal(
KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)),
KLevel.Param(0)), 1);
assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1);

-- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0
let succ_v = KLevel.Succ(store(KLevel.Param(1)));
let succ_v = store(KLevelNode.Succ(p1));
assert_eq!(level_eq(
level_imax(KLevel.Param(0), succ_v),
KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1);
level_imax(p0, succ_v),
store(KLevelNode.Max(p0, succ_v))), 1);

assert_eq!(level_eq(
level_imax(KLevel.Param(0), KLevel.Zero),
KLevel.Zero), 1);
level_imax(p0, zero),
zero), 1);
}

pub fn kernel_unit_tests() {
Expand Down
34 changes: 34 additions & 0 deletions Ix/IxVM/Blake3.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,6 +45,40 @@ def blake3 := ⟦
blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
}

-- Hash `bytes` and assert the digest equals `expected`. Used by every
-- IOBuffer-load path that verifies the pre-image of a content-addressed
-- pointer matches the bytes the prover supplied.
fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
let h = blake3(bytes);
assert_eq!(
[h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]],
expected);
()
}

-- Hash `bytes` and intern the digest into the Store. Returned pointer is
-- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
-- site that synthesises an address from raw bytes (e.g. `expr_addr`,
-- `leaf_hash`, `node_hash`, `cprj_content_addr`).
fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
let h = blake3(bytes);
store([h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]])
}

fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
match layer {
Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),
Expand Down
63 changes: 46 additions & 17 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
| .abbrev => .ofNat 0xFFFFFFFF
| .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)

/-! ## IxVM IOBuffer interface

The host seeds blake3-keyed payloads on six channels; the Aiur kernel
consumes them via `io_get_info` + `#read_byte_stream`. One value shape
per channel — no overloading, no in-band discriminators.

Tiered by access pattern (matches kernel runtime order):

| Tier | Channel | Purpose | Key (32 G) | Value shape |
|--------|---------|--------------------------|-------------------------|-------------------|
| Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes |
| Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes |
| Const | 2 | constant wire bytes | const addr | const bytes |
| Const | 3 | Defn reducibility hint | Defn addr | single G |
| Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) |
| Blob | 5 | blob raw bytes | blob addr | raw bytes |

Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
fires per blob ref encountered during `build_ref_idxs_and_blobs`.

Soundness:
* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
against its content-addressed key.
* ch 3 — semantically optional; controls WHNF reduction heuristic
only, def-eq is sound either way.
* ch 4 — sound by erasure-correctness: a lying discriminator flips
the const/blob decision and the wrong-path load downstream fails
(a "const" blob triggers a ch 2 read returning empty → blake3
verify against the non-empty addr fails; a "blob" const dangles
references → typecheck fail).

Channel numbers MUST stay in sync with the inlined `io_get_info` /
`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
`Ix/IxVM/Kernel/Claim.lean`.
-/

/-- Insert all per-address entries for `addr`s satisfying `keep` into
`ioBuffer`. Each address kind lives on its own channel; the key is
always the 32-G blake3 hash, with no disambiguating suffix.

| channel | key (32 G) | value | meaning |
|---------|------------|----------------|---------|
| 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) |
| 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) |
| 2 | `addr` | single G | Defn `ReducibilityHints` encoding |

Blob addrs also get an empty entry on channel 0 so the kernel's
constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
works without a separate query path. -/
`ioBuffer`. See the channel table above. -/
def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
(ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
let mut ioBuffer := ioBuffer
Expand All@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
-- serialized form the lazy entry holds — no materialization needed.
let bytes := lc.rawBytes
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
-- Discriminator: this addr resolves to a constant.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
for (addr, rawBytes) in ixonEnv.blobs do
if !keep addr then continue
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
ioBuffer := ioBuffer.extend 0 key #[]
ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
-- Discriminator: this addr resolves to a blob.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
for (_, named) in ixonEnv.named do
if !keep named.addr then continue
match named.constMeta with
| .defn _ _ hints _ _ _ _ _ =>
let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
| _ => pure ()
return ioBuffer

Expand DownExpand Up@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
match trees.get? root with
| some tree =>
let bytes := Ix.AssumptionTree.ser tree
.ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
.ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
| none => .error s!"no assumption tree supplied for root {root}"

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

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface#457

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 5 commits into from
Jul 2, 2026
Merged

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7efebe6
IxVM kernel: augment addr_pos_map with blob-ref sentinels
arthurpaulino Jun 24, 2026
bae332e
IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passing
arthurpaulino Jun 27, 2026
64390ad
IxVM: per-kind IOBuffer channels with documented interface
arthurpaulino Jun 27, 2026
1fb0dd1
IxVM Blake3: inline blake3_flat at its two call sites
arthurpaulino Jul 2, 2026
b84a500
IxVM kernel: KLevel = &KLevelNode (pass universes by pointer)
arthurpaulino Jul 2, 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
88 changes: 34 additions & 54 deletions Ix/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,89 +45,69 @@ def entrypoints := ⟦
}

fn level_cmp_tests() {
let zero = store(KLevelNode.Zero);
let p0 = store(KLevelNode.Param(0));
let p1 = store(KLevelNode.Param(1));
let succ_p0 = store(KLevelNode.Succ(p0));
let succ_zero = store(KLevelNode.Succ(zero));

-- Zero ≤ anything
assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
assert_eq!(level_leq(zero, p0), 1);

-- Param(u) ≤ Param(u) (reflexivity)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1);
assert_eq!(level_leq(p0, p0), 1);

-- Param(u) ≤ Param(v) fails (u ≠ v, set u > v)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0);
assert_eq!(level_leq(p0, p1), 0);

-- Succ(u) ≤ Succ(u) (peel both succs)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, succ_p0), 1);

-- Succ(u) ≤ u fails (u+1 > u at any assignment)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Param(0)), 0);

-- === level_leq: Param ≤ Succ reduction ===

-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u)
assert_eq!(level_leq(
KLevel.Param(0),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, p0), 0);

-- === level_leq: Max distribution ===
-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1)
assert_eq!(level_leq(p0, succ_p0), 1);

-- max(u, v) ≤ max(u, v) (reflexivity via distribution)
let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1)));
let max_uv = store(KLevelNode.Max(p0, p1));
assert_eq!(level_leq(max_uv, max_uv), 1);

-- u ≤ max(u, v) (try-each-branch: first branch succeeds)
assert_eq!(level_leq(KLevel.Param(0), max_uv), 1);
-- u ≤ max(u, v)
assert_eq!(level_leq(p0, max_uv), 1);

-- max(u, v) ≤ u fails (set v > u)
assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0);
-- max(u, v) ≤ u fails
assert_eq!(level_leq(max_uv, p0), 0);

-- === level_leq: IMax case-splitting ===

-- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max)
let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1)));
-- imax(u, v) ≤ max(u, v)
let imax_uv = store(KLevelNode.IMax(p0, p1));
assert_eq!(level_leq(imax_uv, max_uv), 1);

-- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1)
-- max(u, v) ≤ imax(u, v) fails
assert_eq!(level_leq(max_uv, imax_uv), 0);

-- === level_leq: Succ ≤ Max with IMax child (the case-split fix) ===

-- u+1 = max(1, imax(u+1, u)): equal for all σ
-- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1
-- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1
-- This is the case that requires case-splitting through Max when
-- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)).
let a = KLevel.Succ(store(KLevel.Param(0)));
let b = KLevel.Max(
store(KLevel.Succ(store(KLevel.Zero))),
store(KLevel.IMax(
store(KLevel.Succ(store(KLevel.Param(0)))),
store(KLevel.Param(0)))));
-- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix)
let a = succ_p0;
let b = store(KLevelNode.Max(
succ_zero,
store(KLevelNode.IMax(succ_p0, p0))));
assert_eq!(level_equal(a, b), 1);

-- === level_equal: semantic equality ===

-- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u)
assert_eq!(level_equal(
KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))),
KLevel.Param(0)), 1);
-- imax(u, u) = u
assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1);

-- max(u, 0) = u
assert_eq!(level_equal(
KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)),
KLevel.Param(0)), 1);
assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1);

-- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0
let succ_v = KLevel.Succ(store(KLevel.Param(1)));
let succ_v = store(KLevelNode.Succ(p1));
assert_eq!(level_eq(
level_imax(KLevel.Param(0), succ_v),
KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1);
level_imax(p0, succ_v),
store(KLevelNode.Max(p0, succ_v))), 1);

assert_eq!(level_eq(
level_imax(KLevel.Param(0), KLevel.Zero),
KLevel.Zero), 1);
level_imax(p0, zero),
zero), 1);
}

pub fn kernel_unit_tests() {
Expand Down
34 changes: 34 additions & 0 deletions Ix/IxVM/Blake3.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,6 +45,40 @@ def blake3 := ⟦
blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
}

-- Hash `bytes` and assert the digest equals `expected`. Used by every
-- IOBuffer-load path that verifies the pre-image of a content-addressed
-- pointer matches the bytes the prover supplied.
fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
let h = blake3(bytes);
assert_eq!(
[h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]],
expected);
()
}

-- Hash `bytes` and intern the digest into the Store. Returned pointer is
-- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
-- site that synthesises an address from raw bytes (e.g. `expr_addr`,
-- `leaf_hash`, `node_hash`, `cprj_content_addr`).
fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
let h = blake3(bytes);
store([h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]])
}

fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
match layer {
Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),
Expand Down
63 changes: 46 additions & 17 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
| .abbrev => .ofNat 0xFFFFFFFF
| .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)

/-! ## IxVM IOBuffer interface

The host seeds blake3-keyed payloads on six channels; the Aiur kernel
consumes them via `io_get_info` + `#read_byte_stream`. One value shape
per channel — no overloading, no in-band discriminators.

Tiered by access pattern (matches kernel runtime order):

| Tier | Channel | Purpose | Key (32 G) | Value shape |
|--------|---------|--------------------------|-------------------------|-------------------|
| Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes |
| Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes |
| Const | 2 | constant wire bytes | const addr | const bytes |
| Const | 3 | Defn reducibility hint | Defn addr | single G |
| Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) |
| Blob | 5 | blob raw bytes | blob addr | raw bytes |

Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
fires per blob ref encountered during `build_ref_idxs_and_blobs`.

Soundness:
* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
against its content-addressed key.
* ch 3 — semantically optional; controls WHNF reduction heuristic
only, def-eq is sound either way.
* ch 4 — sound by erasure-correctness: a lying discriminator flips
the const/blob decision and the wrong-path load downstream fails
(a "const" blob triggers a ch 2 read returning empty → blake3
verify against the non-empty addr fails; a "blob" const dangles
references → typecheck fail).

Channel numbers MUST stay in sync with the inlined `io_get_info` /
`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
`Ix/IxVM/Kernel/Claim.lean`.
-/

/-- Insert all per-address entries for `addr`s satisfying `keep` into
`ioBuffer`. Each address kind lives on its own channel; the key is
always the 32-G blake3 hash, with no disambiguating suffix.

| channel | key (32 G) | value | meaning |
|---------|------------|----------------|---------|
| 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) |
| 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) |
| 2 | `addr` | single G | Defn `ReducibilityHints` encoding |

Blob addrs also get an empty entry on channel 0 so the kernel's
constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
works without a separate query path. -/
`ioBuffer`. See the channel table above. -/
def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
(ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
let mut ioBuffer := ioBuffer
Expand All@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
-- serialized form the lazy entry holds — no materialization needed.
let bytes := lc.rawBytes
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
-- Discriminator: this addr resolves to a constant.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
for (addr, rawBytes) in ixonEnv.blobs do
if !keep addr then continue
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
ioBuffer := ioBuffer.extend 0 key #[]
ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
-- Discriminator: this addr resolves to a blob.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
for (_, named) in ixonEnv.named do
if !keep named.addr then continue
match named.constMeta with
| .defn _ _ hints _ _ _ _ _ =>
let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
| _ => pure ()
return ioBuffer

Expand DownExpand Up@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
match trees.get? root with
| some tree =>
let bytes := Ix.AssumptionTree.ser tree
.ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
.ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
| none => .error s!"no assumption tree supplied for root {root}"

/-- Build the witness for `verify_claim` against `claim`.
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 \u003e 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms"); } } catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + '
Skip to content

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface#457

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 5 commits into from
Jul 2, 2026
Merged

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7efebe6
IxVM kernel: augment addr_pos_map with blob-ref sentinels
arthurpaulino Jun 24, 2026
bae332e
IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passing
arthurpaulino Jun 27, 2026
64390ad
IxVM: per-kind IOBuffer channels with documented interface
arthurpaulino Jun 27, 2026
1fb0dd1
IxVM Blake3: inline blake3_flat at its two call sites
arthurpaulino Jul 2, 2026
b84a500
IxVM kernel: KLevel = &KLevelNode (pass universes by pointer)
arthurpaulino Jul 2, 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
88 changes: 34 additions & 54 deletions Ix/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,89 +45,69 @@ def entrypoints := ⟦
}

fn level_cmp_tests() {
let zero = store(KLevelNode.Zero);
let p0 = store(KLevelNode.Param(0));
let p1 = store(KLevelNode.Param(1));
let succ_p0 = store(KLevelNode.Succ(p0));
let succ_zero = store(KLevelNode.Succ(zero));

-- Zero ≤ anything
assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
assert_eq!(level_leq(zero, p0), 1);

-- Param(u) ≤ Param(u) (reflexivity)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1);
assert_eq!(level_leq(p0, p0), 1);

-- Param(u) ≤ Param(v) fails (u ≠ v, set u > v)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0);
assert_eq!(level_leq(p0, p1), 0);

-- Succ(u) ≤ Succ(u) (peel both succs)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, succ_p0), 1);

-- Succ(u) ≤ u fails (u+1 > u at any assignment)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Param(0)), 0);

-- === level_leq: Param ≤ Succ reduction ===

-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u)
assert_eq!(level_leq(
KLevel.Param(0),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, p0), 0);

-- === level_leq: Max distribution ===
-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1)
assert_eq!(level_leq(p0, succ_p0), 1);

-- max(u, v) ≤ max(u, v) (reflexivity via distribution)
let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1)));
let max_uv = store(KLevelNode.Max(p0, p1));
assert_eq!(level_leq(max_uv, max_uv), 1);

-- u ≤ max(u, v) (try-each-branch: first branch succeeds)
assert_eq!(level_leq(KLevel.Param(0), max_uv), 1);
-- u ≤ max(u, v)
assert_eq!(level_leq(p0, max_uv), 1);

-- max(u, v) ≤ u fails (set v > u)
assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0);
-- max(u, v) ≤ u fails
assert_eq!(level_leq(max_uv, p0), 0);

-- === level_leq: IMax case-splitting ===

-- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max)
let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1)));
-- imax(u, v) ≤ max(u, v)
let imax_uv = store(KLevelNode.IMax(p0, p1));
assert_eq!(level_leq(imax_uv, max_uv), 1);

-- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1)
-- max(u, v) ≤ imax(u, v) fails
assert_eq!(level_leq(max_uv, imax_uv), 0);

-- === level_leq: Succ ≤ Max with IMax child (the case-split fix) ===

-- u+1 = max(1, imax(u+1, u)): equal for all σ
-- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1
-- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1
-- This is the case that requires case-splitting through Max when
-- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)).
let a = KLevel.Succ(store(KLevel.Param(0)));
let b = KLevel.Max(
store(KLevel.Succ(store(KLevel.Zero))),
store(KLevel.IMax(
store(KLevel.Succ(store(KLevel.Param(0)))),
store(KLevel.Param(0)))));
-- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix)
let a = succ_p0;
let b = store(KLevelNode.Max(
succ_zero,
store(KLevelNode.IMax(succ_p0, p0))));
assert_eq!(level_equal(a, b), 1);

-- === level_equal: semantic equality ===

-- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u)
assert_eq!(level_equal(
KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))),
KLevel.Param(0)), 1);
-- imax(u, u) = u
assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1);

-- max(u, 0) = u
assert_eq!(level_equal(
KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)),
KLevel.Param(0)), 1);
assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1);

-- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0
let succ_v = KLevel.Succ(store(KLevel.Param(1)));
let succ_v = store(KLevelNode.Succ(p1));
assert_eq!(level_eq(
level_imax(KLevel.Param(0), succ_v),
KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1);
level_imax(p0, succ_v),
store(KLevelNode.Max(p0, succ_v))), 1);

assert_eq!(level_eq(
level_imax(KLevel.Param(0), KLevel.Zero),
KLevel.Zero), 1);
level_imax(p0, zero),
zero), 1);
}

pub fn kernel_unit_tests() {
Expand Down
34 changes: 34 additions & 0 deletions Ix/IxVM/Blake3.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,6 +45,40 @@ def blake3 := ⟦
blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
}

-- Hash `bytes` and assert the digest equals `expected`. Used by every
-- IOBuffer-load path that verifies the pre-image of a content-addressed
-- pointer matches the bytes the prover supplied.
fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
let h = blake3(bytes);
assert_eq!(
[h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]],
expected);
()
}

-- Hash `bytes` and intern the digest into the Store. Returned pointer is
-- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
-- site that synthesises an address from raw bytes (e.g. `expr_addr`,
-- `leaf_hash`, `node_hash`, `cprj_content_addr`).
fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
let h = blake3(bytes);
store([h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]])
}

fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
match layer {
Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),
Expand Down
63 changes: 46 additions & 17 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
| .abbrev => .ofNat 0xFFFFFFFF
| .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)

/-! ## IxVM IOBuffer interface

The host seeds blake3-keyed payloads on six channels; the Aiur kernel
consumes them via `io_get_info` + `#read_byte_stream`. One value shape
per channel — no overloading, no in-band discriminators.

Tiered by access pattern (matches kernel runtime order):

| Tier | Channel | Purpose | Key (32 G) | Value shape |
|--------|---------|--------------------------|-------------------------|-------------------|
| Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes |
| Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes |
| Const | 2 | constant wire bytes | const addr | const bytes |
| Const | 3 | Defn reducibility hint | Defn addr | single G |
| Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) |
| Blob | 5 | blob raw bytes | blob addr | raw bytes |

Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
fires per blob ref encountered during `build_ref_idxs_and_blobs`.

Soundness:
* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
against its content-addressed key.
* ch 3 — semantically optional; controls WHNF reduction heuristic
only, def-eq is sound either way.
* ch 4 — sound by erasure-correctness: a lying discriminator flips
the const/blob decision and the wrong-path load downstream fails
(a "const" blob triggers a ch 2 read returning empty → blake3
verify against the non-empty addr fails; a "blob" const dangles
references → typecheck fail).

Channel numbers MUST stay in sync with the inlined `io_get_info` /
`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
`Ix/IxVM/Kernel/Claim.lean`.
-/

/-- Insert all per-address entries for `addr`s satisfying `keep` into
`ioBuffer`. Each address kind lives on its own channel; the key is
always the 32-G blake3 hash, with no disambiguating suffix.

| channel | key (32 G) | value | meaning |
|---------|------------|----------------|---------|
| 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) |
| 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) |
| 2 | `addr` | single G | Defn `ReducibilityHints` encoding |

Blob addrs also get an empty entry on channel 0 so the kernel's
constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
works without a separate query path. -/
`ioBuffer`. See the channel table above. -/
def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
(ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
let mut ioBuffer := ioBuffer
Expand All@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
-- serialized form the lazy entry holds — no materialization needed.
let bytes := lc.rawBytes
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
-- Discriminator: this addr resolves to a constant.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
for (addr, rawBytes) in ixonEnv.blobs do
if !keep addr then continue
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
ioBuffer := ioBuffer.extend 0 key #[]
ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
-- Discriminator: this addr resolves to a blob.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
for (_, named) in ixonEnv.named do
if !keep named.addr then continue
match named.constMeta with
| .defn _ _ hints _ _ _ _ _ =>
let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
| _ => pure ()
return ioBuffer

Expand DownExpand Up@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
match trees.get? root with
| some tree =>
let bytes := Ix.AssumptionTree.ser tree
.ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
.ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
| none => .error s!"no assumption tree supplied for root {root}"

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

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface#457

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 5 commits into from
Jul 2, 2026
Merged

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7efebe6
IxVM kernel: augment addr_pos_map with blob-ref sentinels
arthurpaulino Jun 24, 2026
bae332e
IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passing
arthurpaulino Jun 27, 2026
64390ad
IxVM: per-kind IOBuffer channels with documented interface
arthurpaulino Jun 27, 2026
1fb0dd1
IxVM Blake3: inline blake3_flat at its two call sites
arthurpaulino Jul 2, 2026
b84a500
IxVM kernel: KLevel = &KLevelNode (pass universes by pointer)
arthurpaulino Jul 2, 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
88 changes: 34 additions & 54 deletions Ix/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,89 +45,69 @@ def entrypoints := ⟦
}

fn level_cmp_tests() {
let zero = store(KLevelNode.Zero);
let p0 = store(KLevelNode.Param(0));
let p1 = store(KLevelNode.Param(1));
let succ_p0 = store(KLevelNode.Succ(p0));
let succ_zero = store(KLevelNode.Succ(zero));

-- Zero ≤ anything
assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
assert_eq!(level_leq(zero, p0), 1);

-- Param(u) ≤ Param(u) (reflexivity)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1);
assert_eq!(level_leq(p0, p0), 1);

-- Param(u) ≤ Param(v) fails (u ≠ v, set u > v)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0);
assert_eq!(level_leq(p0, p1), 0);

-- Succ(u) ≤ Succ(u) (peel both succs)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, succ_p0), 1);

-- Succ(u) ≤ u fails (u+1 > u at any assignment)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Param(0)), 0);

-- === level_leq: Param ≤ Succ reduction ===

-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u)
assert_eq!(level_leq(
KLevel.Param(0),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, p0), 0);

-- === level_leq: Max distribution ===
-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1)
assert_eq!(level_leq(p0, succ_p0), 1);

-- max(u, v) ≤ max(u, v) (reflexivity via distribution)
let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1)));
let max_uv = store(KLevelNode.Max(p0, p1));
assert_eq!(level_leq(max_uv, max_uv), 1);

-- u ≤ max(u, v) (try-each-branch: first branch succeeds)
assert_eq!(level_leq(KLevel.Param(0), max_uv), 1);
-- u ≤ max(u, v)
assert_eq!(level_leq(p0, max_uv), 1);

-- max(u, v) ≤ u fails (set v > u)
assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0);
-- max(u, v) ≤ u fails
assert_eq!(level_leq(max_uv, p0), 0);

-- === level_leq: IMax case-splitting ===

-- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max)
let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1)));
-- imax(u, v) ≤ max(u, v)
let imax_uv = store(KLevelNode.IMax(p0, p1));
assert_eq!(level_leq(imax_uv, max_uv), 1);

-- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1)
-- max(u, v) ≤ imax(u, v) fails
assert_eq!(level_leq(max_uv, imax_uv), 0);

-- === level_leq: Succ ≤ Max with IMax child (the case-split fix) ===

-- u+1 = max(1, imax(u+1, u)): equal for all σ
-- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1
-- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1
-- This is the case that requires case-splitting through Max when
-- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)).
let a = KLevel.Succ(store(KLevel.Param(0)));
let b = KLevel.Max(
store(KLevel.Succ(store(KLevel.Zero))),
store(KLevel.IMax(
store(KLevel.Succ(store(KLevel.Param(0)))),
store(KLevel.Param(0)))));
-- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix)
let a = succ_p0;
let b = store(KLevelNode.Max(
succ_zero,
store(KLevelNode.IMax(succ_p0, p0))));
assert_eq!(level_equal(a, b), 1);

-- === level_equal: semantic equality ===

-- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u)
assert_eq!(level_equal(
KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))),
KLevel.Param(0)), 1);
-- imax(u, u) = u
assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1);

-- max(u, 0) = u
assert_eq!(level_equal(
KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)),
KLevel.Param(0)), 1);
assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1);

-- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0
let succ_v = KLevel.Succ(store(KLevel.Param(1)));
let succ_v = store(KLevelNode.Succ(p1));
assert_eq!(level_eq(
level_imax(KLevel.Param(0), succ_v),
KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1);
level_imax(p0, succ_v),
store(KLevelNode.Max(p0, succ_v))), 1);

assert_eq!(level_eq(
level_imax(KLevel.Param(0), KLevel.Zero),
KLevel.Zero), 1);
level_imax(p0, zero),
zero), 1);
}

pub fn kernel_unit_tests() {
Expand Down
34 changes: 34 additions & 0 deletions Ix/IxVM/Blake3.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,6 +45,40 @@ def blake3 := ⟦
blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
}

-- Hash `bytes` and assert the digest equals `expected`. Used by every
-- IOBuffer-load path that verifies the pre-image of a content-addressed
-- pointer matches the bytes the prover supplied.
fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
let h = blake3(bytes);
assert_eq!(
[h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]],
expected);
()
}

-- Hash `bytes` and intern the digest into the Store. Returned pointer is
-- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
-- site that synthesises an address from raw bytes (e.g. `expr_addr`,
-- `leaf_hash`, `node_hash`, `cprj_content_addr`).
fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
let h = blake3(bytes);
store([h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]])
}

fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
match layer {
Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),
Expand Down
63 changes: 46 additions & 17 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
| .abbrev => .ofNat 0xFFFFFFFF
| .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)

/-! ## IxVM IOBuffer interface

The host seeds blake3-keyed payloads on six channels; the Aiur kernel
consumes them via `io_get_info` + `#read_byte_stream`. One value shape
per channel — no overloading, no in-band discriminators.

Tiered by access pattern (matches kernel runtime order):

| Tier | Channel | Purpose | Key (32 G) | Value shape |
|--------|---------|--------------------------|-------------------------|-------------------|
| Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes |
| Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes |
| Const | 2 | constant wire bytes | const addr | const bytes |
| Const | 3 | Defn reducibility hint | Defn addr | single G |
| Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) |
| Blob | 5 | blob raw bytes | blob addr | raw bytes |

Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
fires per blob ref encountered during `build_ref_idxs_and_blobs`.

Soundness:
* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
against its content-addressed key.
* ch 3 — semantically optional; controls WHNF reduction heuristic
only, def-eq is sound either way.
* ch 4 — sound by erasure-correctness: a lying discriminator flips
the const/blob decision and the wrong-path load downstream fails
(a "const" blob triggers a ch 2 read returning empty → blake3
verify against the non-empty addr fails; a "blob" const dangles
references → typecheck fail).

Channel numbers MUST stay in sync with the inlined `io_get_info` /
`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
`Ix/IxVM/Kernel/Claim.lean`.
-/

/-- Insert all per-address entries for `addr`s satisfying `keep` into
`ioBuffer`. Each address kind lives on its own channel; the key is
always the 32-G blake3 hash, with no disambiguating suffix.

| channel | key (32 G) | value | meaning |
|---------|------------|----------------|---------|
| 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) |
| 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) |
| 2 | `addr` | single G | Defn `ReducibilityHints` encoding |

Blob addrs also get an empty entry on channel 0 so the kernel's
constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
works without a separate query path. -/
`ioBuffer`. See the channel table above. -/
def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
(ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
let mut ioBuffer := ioBuffer
Expand All@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
-- serialized form the lazy entry holds — no materialization needed.
let bytes := lc.rawBytes
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
-- Discriminator: this addr resolves to a constant.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
for (addr, rawBytes) in ixonEnv.blobs do
if !keep addr then continue
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
ioBuffer := ioBuffer.extend 0 key #[]
ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
-- Discriminator: this addr resolves to a blob.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
for (_, named) in ixonEnv.named do
if !keep named.addr then continue
match named.constMeta with
| .defn _ _ hints _ _ _ _ _ =>
let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
| _ => pure ()
return ioBuffer

Expand DownExpand Up@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
match trees.get? root with
| some tree =>
let bytes := Ix.AssumptionTree.ser tree
.ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
.ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
| none => .error s!"no assumption tree supplied for root {root}"

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

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface#457

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 5 commits into from
Jul 2, 2026
Merged

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7efebe6
IxVM kernel: augment addr_pos_map with blob-ref sentinels
arthurpaulino Jun 24, 2026
bae332e
IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passing
arthurpaulino Jun 27, 2026
64390ad
IxVM: per-kind IOBuffer channels with documented interface
arthurpaulino Jun 27, 2026
1fb0dd1
IxVM Blake3: inline blake3_flat at its two call sites
arthurpaulino Jul 2, 2026
b84a500
IxVM kernel: KLevel = &KLevelNode (pass universes by pointer)
arthurpaulino Jul 2, 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
88 changes: 34 additions & 54 deletions Ix/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,89 +45,69 @@ def entrypoints := ⟦
}

fn level_cmp_tests() {
let zero = store(KLevelNode.Zero);
let p0 = store(KLevelNode.Param(0));
let p1 = store(KLevelNode.Param(1));
let succ_p0 = store(KLevelNode.Succ(p0));
let succ_zero = store(KLevelNode.Succ(zero));

-- Zero ≤ anything
assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
assert_eq!(level_leq(zero, p0), 1);

-- Param(u) ≤ Param(u) (reflexivity)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1);
assert_eq!(level_leq(p0, p0), 1);

-- Param(u) ≤ Param(v) fails (u ≠ v, set u > v)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0);
assert_eq!(level_leq(p0, p1), 0);

-- Succ(u) ≤ Succ(u) (peel both succs)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, succ_p0), 1);

-- Succ(u) ≤ u fails (u+1 > u at any assignment)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Param(0)), 0);

-- === level_leq: Param ≤ Succ reduction ===

-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u)
assert_eq!(level_leq(
KLevel.Param(0),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, p0), 0);

-- === level_leq: Max distribution ===
-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1)
assert_eq!(level_leq(p0, succ_p0), 1);

-- max(u, v) ≤ max(u, v) (reflexivity via distribution)
let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1)));
let max_uv = store(KLevelNode.Max(p0, p1));
assert_eq!(level_leq(max_uv, max_uv), 1);

-- u ≤ max(u, v) (try-each-branch: first branch succeeds)
assert_eq!(level_leq(KLevel.Param(0), max_uv), 1);
-- u ≤ max(u, v)
assert_eq!(level_leq(p0, max_uv), 1);

-- max(u, v) ≤ u fails (set v > u)
assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0);
-- max(u, v) ≤ u fails
assert_eq!(level_leq(max_uv, p0), 0);

-- === level_leq: IMax case-splitting ===

-- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max)
let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1)));
-- imax(u, v) ≤ max(u, v)
let imax_uv = store(KLevelNode.IMax(p0, p1));
assert_eq!(level_leq(imax_uv, max_uv), 1);

-- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1)
-- max(u, v) ≤ imax(u, v) fails
assert_eq!(level_leq(max_uv, imax_uv), 0);

-- === level_leq: Succ ≤ Max with IMax child (the case-split fix) ===

-- u+1 = max(1, imax(u+1, u)): equal for all σ
-- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1
-- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1
-- This is the case that requires case-splitting through Max when
-- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)).
let a = KLevel.Succ(store(KLevel.Param(0)));
let b = KLevel.Max(
store(KLevel.Succ(store(KLevel.Zero))),
store(KLevel.IMax(
store(KLevel.Succ(store(KLevel.Param(0)))),
store(KLevel.Param(0)))));
-- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix)
let a = succ_p0;
let b = store(KLevelNode.Max(
succ_zero,
store(KLevelNode.IMax(succ_p0, p0))));
assert_eq!(level_equal(a, b), 1);

-- === level_equal: semantic equality ===

-- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u)
assert_eq!(level_equal(
KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))),
KLevel.Param(0)), 1);
-- imax(u, u) = u
assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1);

-- max(u, 0) = u
assert_eq!(level_equal(
KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)),
KLevel.Param(0)), 1);
assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1);

-- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0
let succ_v = KLevel.Succ(store(KLevel.Param(1)));
let succ_v = store(KLevelNode.Succ(p1));
assert_eq!(level_eq(
level_imax(KLevel.Param(0), succ_v),
KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1);
level_imax(p0, succ_v),
store(KLevelNode.Max(p0, succ_v))), 1);

assert_eq!(level_eq(
level_imax(KLevel.Param(0), KLevel.Zero),
KLevel.Zero), 1);
level_imax(p0, zero),
zero), 1);
}

pub fn kernel_unit_tests() {
Expand Down
34 changes: 34 additions & 0 deletions Ix/IxVM/Blake3.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,6 +45,40 @@ def blake3 := ⟦
blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
}

-- Hash `bytes` and assert the digest equals `expected`. Used by every
-- IOBuffer-load path that verifies the pre-image of a content-addressed
-- pointer matches the bytes the prover supplied.
fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
let h = blake3(bytes);
assert_eq!(
[h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]],
expected);
()
}

-- Hash `bytes` and intern the digest into the Store. Returned pointer is
-- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
-- site that synthesises an address from raw bytes (e.g. `expr_addr`,
-- `leaf_hash`, `node_hash`, `cprj_content_addr`).
fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
let h = blake3(bytes);
store([h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]])
}

fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
match layer {
Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),
Expand Down
63 changes: 46 additions & 17 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
| .abbrev => .ofNat 0xFFFFFFFF
| .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)

/-! ## IxVM IOBuffer interface

The host seeds blake3-keyed payloads on six channels; the Aiur kernel
consumes them via `io_get_info` + `#read_byte_stream`. One value shape
per channel — no overloading, no in-band discriminators.

Tiered by access pattern (matches kernel runtime order):

| Tier | Channel | Purpose | Key (32 G) | Value shape |
|--------|---------|--------------------------|-------------------------|-------------------|
| Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes |
| Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes |
| Const | 2 | constant wire bytes | const addr | const bytes |
| Const | 3 | Defn reducibility hint | Defn addr | single G |
| Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) |
| Blob | 5 | blob raw bytes | blob addr | raw bytes |

Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
fires per blob ref encountered during `build_ref_idxs_and_blobs`.

Soundness:
* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
against its content-addressed key.
* ch 3 — semantically optional; controls WHNF reduction heuristic
only, def-eq is sound either way.
* ch 4 — sound by erasure-correctness: a lying discriminator flips
the const/blob decision and the wrong-path load downstream fails
(a "const" blob triggers a ch 2 read returning empty → blake3
verify against the non-empty addr fails; a "blob" const dangles
references → typecheck fail).

Channel numbers MUST stay in sync with the inlined `io_get_info` /
`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
`Ix/IxVM/Kernel/Claim.lean`.
-/

/-- Insert all per-address entries for `addr`s satisfying `keep` into
`ioBuffer`. Each address kind lives on its own channel; the key is
always the 32-G blake3 hash, with no disambiguating suffix.

| channel | key (32 G) | value | meaning |
|---------|------------|----------------|---------|
| 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) |
| 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) |
| 2 | `addr` | single G | Defn `ReducibilityHints` encoding |

Blob addrs also get an empty entry on channel 0 so the kernel's
constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
works without a separate query path. -/
`ioBuffer`. See the channel table above. -/
def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
(ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
let mut ioBuffer := ioBuffer
Expand All@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
-- serialized form the lazy entry holds — no materialization needed.
let bytes := lc.rawBytes
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
-- Discriminator: this addr resolves to a constant.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
for (addr, rawBytes) in ixonEnv.blobs do
if !keep addr then continue
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
ioBuffer := ioBuffer.extend 0 key #[]
ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
-- Discriminator: this addr resolves to a blob.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
for (_, named) in ixonEnv.named do
if !keep named.addr then continue
match named.constMeta with
| .defn _ _ hints _ _ _ _ _ =>
let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
| _ => pure ()
return ioBuffer

Expand DownExpand Up@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
match trees.get? root with
| some tree =>
let bytes := Ix.AssumptionTree.ser tree
.ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
.ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
| none => .error s!"no assumption tree supplied for root {root}"

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

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface#457

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 5 commits into from
Jul 2, 2026
Merged

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7efebe6
IxVM kernel: augment addr_pos_map with blob-ref sentinels
arthurpaulino Jun 24, 2026
bae332e
IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passing
arthurpaulino Jun 27, 2026
64390ad
IxVM: per-kind IOBuffer channels with documented interface
arthurpaulino Jun 27, 2026
1fb0dd1
IxVM Blake3: inline blake3_flat at its two call sites
arthurpaulino Jul 2, 2026
b84a500
IxVM kernel: KLevel = &KLevelNode (pass universes by pointer)
arthurpaulino Jul 2, 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
88 changes: 34 additions & 54 deletions Ix/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,89 +45,69 @@ def entrypoints := ⟦
}

fn level_cmp_tests() {
let zero = store(KLevelNode.Zero);
let p0 = store(KLevelNode.Param(0));
let p1 = store(KLevelNode.Param(1));
let succ_p0 = store(KLevelNode.Succ(p0));
let succ_zero = store(KLevelNode.Succ(zero));

-- Zero ≤ anything
assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
assert_eq!(level_leq(zero, p0), 1);

-- Param(u) ≤ Param(u) (reflexivity)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1);
assert_eq!(level_leq(p0, p0), 1);

-- Param(u) ≤ Param(v) fails (u ≠ v, set u > v)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0);
assert_eq!(level_leq(p0, p1), 0);

-- Succ(u) ≤ Succ(u) (peel both succs)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, succ_p0), 1);

-- Succ(u) ≤ u fails (u+1 > u at any assignment)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Param(0)), 0);

-- === level_leq: Param ≤ Succ reduction ===

-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u)
assert_eq!(level_leq(
KLevel.Param(0),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, p0), 0);

-- === level_leq: Max distribution ===
-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1)
assert_eq!(level_leq(p0, succ_p0), 1);

-- max(u, v) ≤ max(u, v) (reflexivity via distribution)
let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1)));
let max_uv = store(KLevelNode.Max(p0, p1));
assert_eq!(level_leq(max_uv, max_uv), 1);

-- u ≤ max(u, v) (try-each-branch: first branch succeeds)
assert_eq!(level_leq(KLevel.Param(0), max_uv), 1);
-- u ≤ max(u, v)
assert_eq!(level_leq(p0, max_uv), 1);

-- max(u, v) ≤ u fails (set v > u)
assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0);
-- max(u, v) ≤ u fails
assert_eq!(level_leq(max_uv, p0), 0);

-- === level_leq: IMax case-splitting ===

-- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max)
let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1)));
-- imax(u, v) ≤ max(u, v)
let imax_uv = store(KLevelNode.IMax(p0, p1));
assert_eq!(level_leq(imax_uv, max_uv), 1);

-- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1)
-- max(u, v) ≤ imax(u, v) fails
assert_eq!(level_leq(max_uv, imax_uv), 0);

-- === level_leq: Succ ≤ Max with IMax child (the case-split fix) ===

-- u+1 = max(1, imax(u+1, u)): equal for all σ
-- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1
-- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1
-- This is the case that requires case-splitting through Max when
-- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)).
let a = KLevel.Succ(store(KLevel.Param(0)));
let b = KLevel.Max(
store(KLevel.Succ(store(KLevel.Zero))),
store(KLevel.IMax(
store(KLevel.Succ(store(KLevel.Param(0)))),
store(KLevel.Param(0)))));
-- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix)
let a = succ_p0;
let b = store(KLevelNode.Max(
succ_zero,
store(KLevelNode.IMax(succ_p0, p0))));
assert_eq!(level_equal(a, b), 1);

-- === level_equal: semantic equality ===

-- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u)
assert_eq!(level_equal(
KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))),
KLevel.Param(0)), 1);
-- imax(u, u) = u
assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1);

-- max(u, 0) = u
assert_eq!(level_equal(
KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)),
KLevel.Param(0)), 1);
assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1);

-- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0
let succ_v = KLevel.Succ(store(KLevel.Param(1)));
let succ_v = store(KLevelNode.Succ(p1));
assert_eq!(level_eq(
level_imax(KLevel.Param(0), succ_v),
KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1);
level_imax(p0, succ_v),
store(KLevelNode.Max(p0, succ_v))), 1);

assert_eq!(level_eq(
level_imax(KLevel.Param(0), KLevel.Zero),
KLevel.Zero), 1);
level_imax(p0, zero),
zero), 1);
}

pub fn kernel_unit_tests() {
Expand Down
34 changes: 34 additions & 0 deletions Ix/IxVM/Blake3.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,6 +45,40 @@ def blake3 := ⟦
blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
}

-- Hash `bytes` and assert the digest equals `expected`. Used by every
-- IOBuffer-load path that verifies the pre-image of a content-addressed
-- pointer matches the bytes the prover supplied.
fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
let h = blake3(bytes);
assert_eq!(
[h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]],
expected);
()
}

-- Hash `bytes` and intern the digest into the Store. Returned pointer is
-- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
-- site that synthesises an address from raw bytes (e.g. `expr_addr`,
-- `leaf_hash`, `node_hash`, `cprj_content_addr`).
fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
let h = blake3(bytes);
store([h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]])
}

fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
match layer {
Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),
Expand Down
63 changes: 46 additions & 17 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
| .abbrev => .ofNat 0xFFFFFFFF
| .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)

/-! ## IxVM IOBuffer interface

The host seeds blake3-keyed payloads on six channels; the Aiur kernel
consumes them via `io_get_info` + `#read_byte_stream`. One value shape
per channel — no overloading, no in-band discriminators.

Tiered by access pattern (matches kernel runtime order):

| Tier | Channel | Purpose | Key (32 G) | Value shape |
|--------|---------|--------------------------|-------------------------|-------------------|
| Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes |
| Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes |
| Const | 2 | constant wire bytes | const addr | const bytes |
| Const | 3 | Defn reducibility hint | Defn addr | single G |
| Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) |
| Blob | 5 | blob raw bytes | blob addr | raw bytes |

Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
fires per blob ref encountered during `build_ref_idxs_and_blobs`.

Soundness:
* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
against its content-addressed key.
* ch 3 — semantically optional; controls WHNF reduction heuristic
only, def-eq is sound either way.
* ch 4 — sound by erasure-correctness: a lying discriminator flips
the const/blob decision and the wrong-path load downstream fails
(a "const" blob triggers a ch 2 read returning empty → blake3
verify against the non-empty addr fails; a "blob" const dangles
references → typecheck fail).

Channel numbers MUST stay in sync with the inlined `io_get_info` /
`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
`Ix/IxVM/Kernel/Claim.lean`.
-/

/-- Insert all per-address entries for `addr`s satisfying `keep` into
`ioBuffer`. Each address kind lives on its own channel; the key is
always the 32-G blake3 hash, with no disambiguating suffix.

| channel | key (32 G) | value | meaning |
|---------|------------|----------------|---------|
| 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) |
| 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) |
| 2 | `addr` | single G | Defn `ReducibilityHints` encoding |

Blob addrs also get an empty entry on channel 0 so the kernel's
constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
works without a separate query path. -/
`ioBuffer`. See the channel table above. -/
def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
(ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
let mut ioBuffer := ioBuffer
Expand All@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
-- serialized form the lazy entry holds — no materialization needed.
let bytes := lc.rawBytes
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
-- Discriminator: this addr resolves to a constant.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
for (addr, rawBytes) in ixonEnv.blobs do
if !keep addr then continue
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
ioBuffer := ioBuffer.extend 0 key #[]
ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
-- Discriminator: this addr resolves to a blob.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
for (_, named) in ixonEnv.named do
if !keep named.addr then continue
match named.constMeta with
| .defn _ _ hints _ _ _ _ _ =>
let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
| _ => pure ()
return ioBuffer

Expand DownExpand Up@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
match trees.get? root with
| some tree =>
let bytes := Ix.AssumptionTree.ser tree
.ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
.ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
| none => .error s!"no assumption tree supplied for root {root}"

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

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface#457

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
arthurpaulino merged 5 commits into from
Jul 2, 2026
Merged

IxVM ingress: blob-ref index, sidecar→rbtree, IOBuffer interface #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7efebe6
IxVM kernel: augment addr_pos_map with blob-ref sentinels
arthurpaulino Jun 24, 2026
bae332e
IxVM ingress: plumbing helpers + sidecar→rbtree migrations + ptr-passing
arthurpaulino Jun 27, 2026
64390ad
IxVM: per-kind IOBuffer channels with documented interface
arthurpaulino Jun 27, 2026
1fb0dd1
IxVM Blake3: inline blake3_flat at its two call sites
arthurpaulino Jul 2, 2026
b84a500
IxVM kernel: KLevel = &KLevelNode (pass universes by pointer)
arthurpaulino Jul 2, 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
88 changes: 34 additions & 54 deletions Ix/IxVM.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,89 +45,69 @@ def entrypoints := ⟦
}

fn level_cmp_tests() {
let zero = store(KLevelNode.Zero);
let p0 = store(KLevelNode.Param(0));
let p1 = store(KLevelNode.Param(1));
let succ_p0 = store(KLevelNode.Succ(p0));
let succ_zero = store(KLevelNode.Succ(zero));

-- Zero ≤ anything
assert_eq!(level_leq(KLevel.Zero, KLevel.Param(0)), 1);
assert_eq!(level_leq(zero, p0), 1);

-- Param(u) ≤ Param(u) (reflexivity)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(0)), 1);
assert_eq!(level_leq(p0, p0), 1);

-- Param(u) ≤ Param(v) fails (u ≠ v, set u > v)
assert_eq!(level_leq(KLevel.Param(0), KLevel.Param(1)), 0);
assert_eq!(level_leq(p0, p1), 0);

-- Succ(u) ≤ Succ(u) (peel both succs)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, succ_p0), 1);

-- Succ(u) ≤ u fails (u+1 > u at any assignment)
assert_eq!(level_leq(
KLevel.Succ(store(KLevel.Param(0))),
KLevel.Param(0)), 0);

-- === level_leq: Param ≤ Succ reduction ===

-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1, reduces to u ≤ u)
assert_eq!(level_leq(
KLevel.Param(0),
KLevel.Succ(store(KLevel.Param(0)))), 1);
assert_eq!(level_leq(succ_p0, p0), 0);

-- === level_leq: Max distribution ===
-- Param(u) ≤ Succ(Param(u)) (u ≤ u+1)
assert_eq!(level_leq(p0, succ_p0), 1);

-- max(u, v) ≤ max(u, v) (reflexivity via distribution)
let max_uv = KLevel.Max(store(KLevel.Param(0)), store(KLevel.Param(1)));
let max_uv = store(KLevelNode.Max(p0, p1));
assert_eq!(level_leq(max_uv, max_uv), 1);

-- u ≤ max(u, v) (try-each-branch: first branch succeeds)
assert_eq!(level_leq(KLevel.Param(0), max_uv), 1);
-- u ≤ max(u, v)
assert_eq!(level_leq(p0, max_uv), 1);

-- max(u, v) ≤ u fails (set v > u)
assert_eq!(level_leq(max_uv, KLevel.Param(0)), 0);
-- max(u, v) ≤ u fails
assert_eq!(level_leq(max_uv, p0), 0);

-- === level_leq: IMax case-splitting ===

-- imax(u, v) ≤ max(u, v) (case-split on v: v=0 gives 0 ≤ max(0,0)=0; v>0 gives max=max)
let imax_uv = KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(1)));
-- imax(u, v) ≤ max(u, v)
let imax_uv = store(KLevelNode.IMax(p0, p1));
assert_eq!(level_leq(imax_uv, max_uv), 1);

-- max(u, v) ≤ imax(u, v) fails (set v=0: max(u,0) = u but imax(u,0) = 0; take u=1)
-- max(u, v) ≤ imax(u, v) fails
assert_eq!(level_leq(max_uv, imax_uv), 0);

-- === level_leq: Succ ≤ Max with IMax child (the case-split fix) ===

-- u+1 = max(1, imax(u+1, u)): equal for all σ
-- σ(u)=0: 1 = max(1, imax(1,0)) = max(1,0) = 1
-- σ(u)=n>0: n+1 = max(1, max(n+1,n)) = n+1
-- This is the case that requires case-splitting through Max when
-- neither branch (Succ(Zero) or IMax) alone dominates Succ(Param(u)).
let a = KLevel.Succ(store(KLevel.Param(0)));
let b = KLevel.Max(
store(KLevel.Succ(store(KLevel.Zero))),
store(KLevel.IMax(
store(KLevel.Succ(store(KLevel.Param(0)))),
store(KLevel.Param(0)))));
-- u+1 = max(1, imax(u+1, u)): equal for all σ (case-split fix)
let a = succ_p0;
let b = store(KLevelNode.Max(
succ_zero,
store(KLevelNode.IMax(succ_p0, p0))));
assert_eq!(level_equal(a, b), 1);

-- === level_equal: semantic equality ===

-- imax(u, u) = u (when u=0: imax(0,0)=0=u; when u>0: max(u,u)=u)
assert_eq!(level_equal(
KLevel.IMax(store(KLevel.Param(0)), store(KLevel.Param(0))),
KLevel.Param(0)), 1);
-- imax(u, u) = u
assert_eq!(level_equal(store(KLevelNode.IMax(p0, p0)), p0), 1);

-- max(u, 0) = u
assert_eq!(level_equal(
KLevel.Max(store(KLevel.Param(0)), store(KLevel.Zero)),
KLevel.Param(0)), 1);
assert_eq!(level_equal(store(KLevelNode.Max(p0, zero)), p0), 1);

-- level_imax reduces imax(u, 1+v) to max(u, 1+v) and imax(u, 0) to 0
let succ_v = KLevel.Succ(store(KLevel.Param(1)));
let succ_v = store(KLevelNode.Succ(p1));
assert_eq!(level_eq(
level_imax(KLevel.Param(0), succ_v),
KLevel.Max(store(KLevel.Param(0)), store(succ_v))), 1);
level_imax(p0, succ_v),
store(KLevelNode.Max(p0, succ_v))), 1);

assert_eq!(level_eq(
level_imax(KLevel.Param(0), KLevel.Zero),
KLevel.Zero), 1);
level_imax(p0, zero),
zero), 1);
}

pub fn kernel_unit_tests() {
Expand Down
34 changes: 34 additions & 0 deletions Ix/IxVM/Blake3.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -45,6 +45,40 @@ def blake3 := ⟦
blake3_compress_layer(load(blake3_compress_chunks(input, store(ListNode.Nil), 0, 0, store([0u8; 8]), store(IV), store(Layer.Nil))))
}

-- Hash `bytes` and assert the digest equals `expected`. Used by every
-- IOBuffer-load path that verifies the pre-image of a content-addressed
-- pointer matches the bytes the prover supplied.
fn verify_bytes_against(bytes: ByteStream, expected: [U8; 32]) {
let h = blake3(bytes);
assert_eq!(
[h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]],
expected);
()
}

-- Hash `bytes` and intern the digest into the Store. Returned pointer is
-- the canonical content-addressed `Addr` shape (`&[U8;32]`). Used by every
-- site that synthesises an address from raw bytes (e.g. `expr_addr`,
-- `leaf_hash`, `node_hash`, `cprj_content_addr`).
fn bytes_to_addr(bytes: ByteStream) -> &[U8; 32] {
let h = blake3(bytes);
store([h[0][0], h[0][1], h[0][2], h[0][3],
h[1][0], h[1][1], h[1][2], h[1][3],
h[2][0], h[2][1], h[2][2], h[2][3],
h[3][0], h[3][1], h[3][2], h[3][3],
h[4][0], h[4][1], h[4][2], h[4][3],
h[5][0], h[5][1], h[5][2], h[5][3],
h[6][0], h[6][1], h[6][2], h[6][3],
h[7][0], h[7][1], h[7][2], h[7][3]])
}

fn blake3_next_layer(layer: Layer, digest: [[U8; 4]; 8], root: G) -> (MaybeDigest, Layer) {
match layer {
Layer.Nil => (MaybeDigest.Some(digest), Layer.Nil),
Expand Down
63 changes: 46 additions & 17 deletions Ix/IxVM/ClaimHarness.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -124,19 +124,45 @@ private def hintToG : Lean.ReducibilityHints → Aiur.G
| .abbrev => .ofNat 0xFFFFFFFF
| .regular n => .ofNat (min (1 + n.toNat) 0xFFFFFFFE)

/-! ## IxVM IOBuffer interface

The host seeds blake3-keyed payloads on six channels; the Aiur kernel
consumes them via `io_get_info` + `#read_byte_stream`. One value shape
per channel — no overloading, no in-band discriminators.

Tiered by access pattern (matches kernel runtime order):

| Tier | Channel | Purpose | Key (32 G) | Value shape |
|--------|---------|--------------------------|-------------------------|-------------------|
| Ctrl | 0 | claim wire bytes | `blake3(claim_bytes)` | claim bytes |
| Ctrl | 1 | assumption tree bytes | `tree.root` | tree bytes |
| Const | 2 | constant wire bytes | const addr | const bytes |
| Const | 3 | Defn reducibility hint | Defn addr | single G |
| Blob | 4 | blob discriminator | addr | one byte (1=const, 0=blob) |
| Blob | 5 | blob raw bytes | blob addr | raw bytes |

Tier 1 fires once per `verify_claim` invocation (claim + optional tree).
Tier 2 fires per constant traversed during `load_with_deps`. Tier 3
fires per blob ref encountered during `build_ref_idxs_and_blobs`.

Soundness:
* ch 0/1/2/5 — every byte stream is blake3-verified by the kernel
against its content-addressed key.
* ch 3 — semantically optional; controls WHNF reduction heuristic
only, def-eq is sound either way.
* ch 4 — sound by erasure-correctness: a lying discriminator flips
the const/blob decision and the wrong-path load downstream fails
(a "const" blob triggers a ch 2 read returning empty → blake3
verify against the non-empty addr fails; a "blob" const dangles
references → typecheck fail).

Channel numbers MUST stay in sync with the inlined `io_get_info` /
`#read_byte_stream` channel literals in `Ix/IxVM/Ingress.lean` and
`Ix/IxVM/Kernel/Claim.lean`.
-/

/-- Insert all per-address entries for `addr`s satisfying `keep` into
`ioBuffer`. Each address kind lives on its own channel; the key is
always the 32-G blake3 hash, with no disambiguating suffix.

| channel | key (32 G) | value | meaning |
|---------|------------|----------------|---------|
| 0 | `addr` | const bytes | constant data (empty marker = `addr` is a blob) |
| 1 | `addr` | raw blob bytes | referenced data (verified by Aiur via blake3) |
| 2 | `addr` | single G | Defn `ReducibilityHints` encoding |

Blob addrs also get an empty entry on channel 0 so the kernel's
constant-vs-blob detection (`io_get_info(0, addr) ⇒ len=0`) still
works without a separate query path. -/
`ioBuffer`. See the channel table above. -/
def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
(ioBuffer : Aiur.IOBuffer) : Aiur.IOBuffer := Id.run do
let mut ioBuffer := ioBuffer
Expand All@@ -146,18 +172,21 @@ def addEntries (ixonEnv : Ixon.Env) (keep : Address → Bool)
-- serialized form the lazy entry holds — no materialization needed.
let bytes := lc.rawBytes
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 0 key (bytes.data.map .ofUInt8)
ioBuffer := ioBuffer.extend 2 key (bytes.data.map .ofUInt8)
-- Discriminator: this addr resolves to a constant.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 1]
for (addr, rawBytes) in ixonEnv.blobs do
if !keep addr then continue
let key : Array Aiur.G := addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 1 key (rawBytes.data.map fun b => .ofNat b.toNat)
ioBuffer := ioBuffer.extend 0 key #[]
ioBuffer := ioBuffer.extend 5 key (rawBytes.data.map fun b => .ofNat b.toNat)
-- Discriminator: this addr resolves to a blob.
ioBuffer := ioBuffer.extend 4 key #[.ofNat 0]
for (_, named) in ixonEnv.named do
if !keep named.addr then continue
match named.constMeta with
| .defn _ _ hints _ _ _ _ _ =>
let key : Array Aiur.G := named.addr.hash.data.map .ofUInt8
ioBuffer := ioBuffer.extend 2 key #[hintToG hints]
ioBuffer := ioBuffer.extend 3 key #[hintToG hints]
| _ => pure ()
return ioBuffer

Expand DownExpand Up@@ -189,7 +218,7 @@ private def seedTreeAt (root : Address)
match trees.get? root with
| some tree =>
let bytes := Ix.AssumptionTree.ser tree
.ok (ioBuffer.extend 0 (addrKey tree.root) (bytes.data.map .ofUInt8))
.ok (ioBuffer.extend 1 (addrKey tree.root) (bytes.data.map .ofUInt8))
| none => .error s!"no assumption tree supplied for root {root}"

/-- Build the witness for `verify_claim` against `claim`.
Expand Down
Loading