IxVM: cheaper shard checking via an addr-first kernel, plus soundness hardening

[arthurpaulino]

Motivation

Make sharded environment checking cheap. A large environment is partitioned across shards, and each shard proves its own constants well-typed against a thin-frontier assumption cutoff, so every constant is checked in exactly one shard and cross-shard assumption trees stay minimal.

Delivering that required migrating the IxVM Aiur kernel from a positional constant table to a content-addressed, lazily-faulted design — and then auditing the result, which turned up five soundness holes with working exploits, including three separate routes to proving False.

Sharded environment checking

A shard proves CheckEnv{root, assumptions}: root is a merkle root over the shard's owned constants, assumptions a merkle root over the thin frontier — the direct out-of-owned walk edges. The kernel's env_walk starts from the owned set, checks each reachable constant, and stops at a frontier member (assumed well-typed by its owning shard: not re-checked, not recursed into).

• Sub-frontier constants are never re-checked here; they are covered transitively by the frontier members' own shard claims. This is the cost win over checking each constant's full closure: no cross-shard duplication, and the assumption tree is one layer deep instead of the whole closure.
• Strict membership: a walk-reachable constant in neither owned nor the frontier is a bad partition and hard-errors, so a shard cannot silently drop coverage of its own closure.
• Byte scope ≠ check scope: delta unfolding reads through the frontier, so a witness ships the full dependency closure of owned even though only the strict-membership set is checked. The witness IOBuffer is built in Rust (aiur_ixvm_witness) rather than Lean, removing the per-byte boxing that dominated shard wall time.

Addr-first kernel

• KExprNode.Const / Proj key on a 32-byte content Addr, not a numeric position; KConstantInfo Induct/Ctor/Rec carry a (block_addr, ind_idx) parent pair instead of indices. The positional top: List<KCI> table threaded through the kernel is gone.
• get_ci(addr) is the sole resolver, Aiur-memoized per addr, faulting constant bytes lazily from an IOBuffer. load_verified_constant re-derives blake3 over the bytes and asserts key == addr; the io_get_info idx/len are unconstrained witness and are never branched on.
• IOBuffer channels: 0 claim, 1 assumption tree, 2 constant bytes, 3 Defn reducibility hint (advisory), 4 blob bytes. The kernel derives blob-vs-constant from Expr context, so no wire discriminator ships. The two sets are not disjoint — one address can be read both ways — so each channel is seeded independently.
• Kernel/Inductive.lean and Kernel/Primitive.lean deleted (~6.6k lines); inductive validation absorbed into Kernel/Check.lean, primitives split into Kernel/Klimbs.lean (bignum gadgets) and Kernel/NatPrim.lean (Nat/Str addr dispatch). New Kernel/InferOnly.lean breaks the DefEq↔Infer cycle. Ingress.lean collapsed 1700→298 lines.

Recursor validation

• build_rec_type reconstructs a recursor's canonical type and asserts it def-eq to the declared type, on both the kind-aware and address-only lookup paths. Without it a recursor could declare ... -> False while its rules still reconstructed correctly.
• spec_params are lowered from the major-premise frame into the recursor-param frame at extraction: the root cause of 17 nested/aux recursor reconstruction failures, and why the canonical check accepted a superset.
• k_flag and parent-inductive-shape checks hoisted out of the attacker-selectable is_aux gate; the canonical rules comparison, which formerly never ran, now runs for every recursor.

Pre-existing criticals

ID	Fix
P1	blob-vs-constant derived from Expr context instead of a prover-answered io_get_info probe, retiring the ch-2 len=0 sentinel; a prover can no longer mark a walk root or owned leaf "skip me"
P2	Nat.div n 0 pins the quotient to zero (was prover-chosen)
P3	klimbs_sub/le corrected on operands with trailing zero limbs; div/mod hints normalized before use
P4	is_large_eliminator field-index arithmetic parenthesized (Aiur - is right-associative)
P5	Reveal recursor rules assert the claimed ruleIdx equals its position

Robustness

• L5: UTF-8 string-literal decode validates continuation-byte ranges and per-length overlong minimums, so distinct byte sequences (e.g. overlong NUL C0 80 vs 00) no longer decode to the same codepoint and def-eq as equal.
• L6: run_claim dispatches on the full tag4 size (was the low byte only), matching Rust Claim::get.
• L8: the K-recursor synth gate checks the major's inferred inductive against the recursor's own, not against itself, so I.rec no longer strips a major of a different inductive.

Aiur assert_eq! messages and circuit cleanup

• assert_eq!(a, b, "why") gains an optional diagnostic label, threaded Source.Term → Typed → Simple → Concrete → Bytecode.Op → Rust Op::AssertEq(_, _, Option<String>) → ExecError::AssertEqMismatch. The message is diagnostic-only and never enters the circuit; all ~122 IxVM assert sites are labeled.
• Unreachable _ => assert_eq!(0, 1) match arms removed: an unmatched runtime value already aborts (the kernel's reject), so the extra arm only widened the circuit.
• Address equality is a full 32-byte content comparison — never a pointer-value compare, which is unsound for distinct-pointer/same-data — packed as five base-256 field limbs behind a byte-0 prefilter.

Witness construction

witness_scope reuses Env::bfs_closure, which already follows refs, Prj → block, and the derived Muts → member/ctor projection edges, so the wrappers get_ci synthesizes ship as forward edges of a single O(closure) walk with no reverse scan of the env. Primitive addresses are seeded as additional walk roots, because def-eq delta-unfolds primitive bodies whose refs are reachable from nowhere else. The Lean seeder computes the same scope by the same rule, so the two cannot drift.

bench-typecheck's constants metric now reads check_const's unique query count — exactly the constants typechecked — instead of the shipped byte scope, which is a superset and inflated throughput.

Soundness audit

Eight parallel read-only audits covered the pipeline end-to-end (compile, Ixon serde, ingress/convert, type-theory core, declaration checking, claim/witness layer, primitives, entry points), under the zkDSL threat model: a prover authors the data and pays for its own trace, so aborts and rejections are not threats and only a wrong answer counts. Thirty findings; every claim relayed here was re-verified against the code before acting on it, and several agent claims were corrected or withdrawn in the process.

Fixed, with a working exploit

Each of these shipped with a fixture that was red before the fix and green after, paired with a minimal-pair control so the verdict is attributable to one variable.

Hole	What it bought an attacker
Self-referential definitions	theorem bad : False := bad typechecked. A standalone Defn was handed a recur slot naming itself, Rec erases to an ordinary Const, and k_infer reads a Const's declared type without checking it — so the body discharged its own type by citing itself. Now restricted to unsafe/partial, which is where Lean permits self-reference and where safe code cannot reach
Nested-inductive positivity	The nested branch dropped the parameter arguments and descended into the nested inductive's constructors without substituting them, so the occurrence being hunted was never present. Host | mk : Inner Host → Host was accepted for a negative Inner. Admits False
Recursor rules compared under the prover's context	compare_rules handed the stored rule's own binder domains to k_is_def_eq as the comparison context. Retyping them to a Prop makes both sides infer to that Prop, proof irrelevance fires, and a recursor with its computation rules swapped between constructors was accepted
Non-canonical computed Nat literals	String.utf8ByteSize built a KLimbs as one unchecked byte, and klimbs_div_mod pinned the quotient's value but not its digits. Since klimbs_eq compares limbs rather than values, the kernel had the polarity backwards: Nat.beq (String.utf8ByteSize "") 0 = false was accepted while the true equation was rejected
Tag0/Tag2 overlong payloads	Three readers, three answers on the same bytes: the circuit discarded bytes past the eighth, the Lean host folded them back in (its shift is mod 64), Rust rejected. One address denoted different constants to different readers

Fixed as defense-in-depth

No exploit demonstrated for these; each commit says so in its first line. They remove a dependence on some other check happening to hold.

• Struct-eta type equality. try_eta_struct omitted the infer(t) ≟ infer(s) side condition all three references carry, degenerating to t ≡ S.mk … (Proj S i t) … for any t of any type.
• Recursor rule labels. cidx selects a rule at reduction time but was validated only positionally; nf decides how iota splits the constructor's arguments and was never checked against the constructor. Equivalents existed only in dead code.
• Iota constructor identity. Rules were selected by index alone, so any inductive's constructor with a matching index fired one. Unreachable through a claim — inference k_checks every argument first — but reduction should not depend on that.
• Universe cache context. compile_univ memoized Level → Univ while a Level::Param compiles to a position in univ_params, and the cache outlives a constant. Now keyed by (level, univ_params_key), matching what collect_expr_tables already does one level up.

Entry points and coverage

• verify_const / verify_check / verify_check_env are DEBUG entrypoints that trust their dependencies, and they shipped in the production verifying key alongside verify_claim — leaving ix verify's funcIdx check as the only barrier, untested, with no equivalent in the recursive verifier. The production toplevel is now pruned to verify_claim alone, so such a proof cannot exist under that VK. Zero FFT cost.
• bench-typecheck reported "status": "ok" and exit 0 when verification failed, and dropped thrown constants without marking them failed.
• shardsCover skipped constants whose bytes do not parse — assigning them to no shard, counting them as neither owned nor unowned, and still including them in "covers all N consts". Now a hard failure.

Test guards that could not fail

Four of these were found by auditing the tests themselves, and they matter because they were the safety net for everything above.

• prim-addrs asserted the literal true. Keyed by address, so a permuted primitive table passed — precisely the defect its docstring claimed to catch. Now the address must resolve to the constant the function's name claims; verified by temporarily swapping nat_add_addr to Nat.mul's bytes and watching it go red.
• The arena negative corpus counted any abort as a correct rejection, so a fixture aborting on invalid IO key — never reaching the code under test — scored as a pass. That is the same failure mode that made two exploit fixtures in this series pass for the wrong reason before it was caught.
• The shard-pipeline SKIP was a passing test conflating "target absent" with "partition selected zero constants".
• A --ignored filter naming no runner executed nothing and returned 0, so a typo'd suite name reported success having run no tests.

Adversarial Ixon test suite

New Tests/Ix/IxVM/Exploits.lean, 19 cases, wired into the ixvm suite. The kernel-arena corpus attacks the layer above: its bad_* fixtures are raw Lean.ConstantInfo declarations that skip the elaborator, but they are still compiled by rsCompileEnvFFI, so the Ixon they produce is always well-formed. This suite authors Ixon.Constant values directly, and storeRawAt goes one level lower still, storing hand-authored byte strings — needed because every value-level fixture is canonical by construction and so cannot express a malformed encoding.

Each case records the false statement acceptance would buy, so a failure reads as a security statement. Rejection reasons are printed, which earned its keep repeatedly: fixtures that "passed" via invalid IO key without reaching the checker were caught this way, as was a fixture that silently corrupted nothing because non-mutual recursors are standalone constants rather than Muts members.

Testing

• lake test -- --ignored ixvm green.
• cargo test --release across all crates: 1195 passed, 0 failed. This also repaired shard_check_env_claim_is_thin_frontier, red since the claim walk moved to positive constant-use because its fixture's Exprs never referenced their own refs.
• New prim-addrs parity suite; codegen ↔ bytecode parity gate green; arena negative corpus (77 bad_*) all reject, now only via genuine in-kernel refusals.
• FFT-cost pins re-pinned per change. Cumulative effect is small (Nat.add_comm 42_747_927 → 42_986_025, +0.6% over the whole series); the largest single contributors are the nested-positivity substitution and the struct-eta guard.
• ix codegen regenerated whenever the Aiur kernel changed, so the committed Rust kernel never lags the source the parity gate compares against.

Known limitations

Recorded rather than silently dropped.

• Call-site surgery is not covered by the value pin. The compiler rewrites calls to aux-generated constants — permuting arguments, dropping some, replacing the head and its universe list — and the plans driving it live only in ConstantMeta, which prune_to_closure_anon excludes. So a verified claim says the term at address X is well-typed, not that term is the Lean declaration you wrote; the equivalence rests on the rewrite being faithful, checked today only by decompile round-trip tests. Closing it is a claim-format decision, not a patch.
• Assumption cycles are not rejected, and a conditional Check claim naming its own target is accepted. That is the specified semantics — some root means "conditional on every leaf", so the claim asserts A → A, vacuous rather than false — and the obligation sits with whoever discharges assumptions. Sharded CheckEnv is not exposed, since shardClaimDigest recomputes the claim from (env, blocks). Pinned as ACCEPT so the boundary cannot move silently.
• Alpha-collapse comparators ignore safety, so two members agreeing on kind/lvls/typ/value and disagreeing on safety collapse. Deliberately not fixed: a prover authors the environment directly and never goes through the compiler, so hardening it stops no attacker, while adding safety to the ordering would move every address and refusing the collapse would put a hard error in the compiler on the strength of an unverified assumption.
• klimbs_le / klimbs_eq are in the logical trusted base, not just the performance path: Nat.decLe mints Decidable.isTrue with a proof term whose correctness is asserted rather than checked, so one wrong verdict yields False.
• check_inductive_shape_ctors omits validate_expr_well_scoped / k_ensure_sort / assert_safety that check_const's Ctor arm performs; only an entirely unreferenced constructor escapes those.