Compiler fixes for auxiliary constant generation by johnchandlerburnham · Pull Request #473 · argumentcomputer/ix

johnchandlerburnham · 2026-07-04T06:34:29Z

Summary

Two related changes to the content-addressing layer and its aux-constant handling, fixing underlying issue reported in #465

1. Ixon no longer stores recr/refl/nested on Inductive. These are derivable
from constructor structure, so storing them was redundant and trusting declared values
was an adversarial surface (e.g. is_rec = false on a recursive inductive enables
improper struct-eta). The kernel now computes is_rec on demand, memoized in a new env
cache with a provisional entry to break the whnf → try_struct_eta_iota → is_struct_like
cycle; this replaces the declared-vs-computed check in check_inductive. The compile
side gains compute_lean_ind_flags to recompute Lean's block-wide
isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a
source Lean env (kernel egress, decompile), and validate_lean_ind_flags to check a
whole env against the recomputation.

2. Evaporated auxiliaries get a canonical form. When SCC splitting strands a nested
aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and
dropping the irrelevant over-merged motives leaves exactly the external inductive's
generic recursor. Canonical treatment: rec_N claims alias <Ext>.rec (e.g.
List.rec), call sites are rebuilt onto the external telescope via head-rewrite
CallSitePlans (owner-gated, single-motive targets), and below_N/brecOn_N compile as
surgered originals like _sizeOf_N. Fixes the AuxDedup kernel-check failures (28 → 0);
AuxDedup1 now generates auxiliaries identical to AuxDedup2's canonical structure.
Documented in docs/ix_canonicity.md §6.5.

Byte-exact aux roundtrip

roundtrip_block Phase A (recompile the regenerated Lean form, compare against the
stored original address) silently failed for 1529 of 1545 aux constants — including
plain stdlib like Nat.casesOn. Root cause: every production compile path preseeds the
ref/univ tables in sorted order (preseed_expr_tables) before compiling, and the
serialized constant embeds those tables; Phase A compiled without the preseed, filling
the tables in traversal order instead — every Ref/univ index permuted, byte-different
but semantically identical constants (decode resolves through the embedded table). A
debug probe recompiling the Lean original through the identical path proved
compile(original) == compile(regen) in every case: regeneration was always faithful,
the comparison context was not.

With the preseed mirrored in Phase A the invariant holds corpus-wide, so a Phase-A
recompile-hash mismatch is now a hard error with no aux exemption, and every
roundtrip arm records failures in aux_gen_errors (recovery keeps the Lean-facing env
populated for diagnosis but is never silent). Related hardening: call-site surgery
detection is durable across serialization (Named.original.is_some() alongside the
in-memory map), shift-aware instantiate_rev in the type-walking helpers (fixes fvar
leaks in .brecOn.go bodies), and the below-def roundtrip loop filters by the
original-gated members like its sibling loops. IX_ROUNDTRIP_DEBUG now dumps hashed
component summaries and runs an original-form recompile probe on any mismatch.

Test fixes and fixtures

kernel-tutorial: bad_raw_consts inductive fixtures carry recomputation-honest flags
so the whole-env validate_ind_flags no longer poisons the shared tutorial env
(73/335 → 335/335, with the kernel rejecting each bad fixture as designed).
validate-aux: seeds match module-private fixture names via privateToUserName?, the
Canonicity prefix is enabled, and Phase 4b gains per-module markers so a fully absent
identity group fails loudly when its fixture module is loaded (previously vacuous at
0 pass / 0 fail, now 109 pass / 0 fail).
New fixtures: AuxDedup1/AuxDedup2 (cross-block aux dedup), AuxDedupMixed (a perm
mixing a canonical slot and PERM_OUT_OF_SCC for the same owner), plus a
CompileMutualFixtures benchmark lib.

Gates

kernel-check-env: 201296/201296
rust-compile: all phases, 0 aux_gen errors / 0 mismatches / 0 Phase-A address
divergences on the full 213k env (live and deserialized)
validate-aux: 0 failures at 4393-constant scope
rust-serialize: byte-exact; kernel-ixon-roundtrip: 143694/0
kernel-tutorial: 335/335; cargo test workspace and lake test green;
cargo clippy --all-targets clean
lake exe ix check-rs compilemathlib.ixe: 736618/736618 passed, 0 failed (325.3s)
lake exe ix validate Benchmarks/Compile/CompileMathlib.lean: 0 failures (1528.33s total)

Remove the `recr`/`refl` bools and the `nested` count from the Ixon `Inductive` constant and its serialization (Rust and Lean), and from the `Indc` reveal-proof variant, renumbering the field-presence mask bits. These flags are derivable from constructor structure, so storing them was redundant and trusting declared values was an adversarial surface (e.g. is_rec = false on a recursive inductive enables improper struct-eta). - kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now computed on demand (computed_is_rec), memoized in the new env is_rec_cache with a provisional entry to break the whnf -> try_struct_eta_iota -> is_struct_like cycle. This replaces the declared-vs-computed H1 verification in check_inductive. - compile: new compute_lean_ind_flags recomputes Lean's block-wide isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a source Lean env (kernel egress, decompile), since Ixon no longer stores the flags; validate_lean_ind_flags checks a whole env against the recomputation. - tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising aux-constant dedup across blocks (fix forthcoming); add a CompileMutualFixtures benchmark lib building the mutual test fixtures; ignore *.ixe.

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a nested aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and dropping the irrelevant over-merged motives leaves exactly the external inductive's generic recursor. Canonical treatment: `rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are rebuilt onto the external telescope via head-rewrite CallSitePlans (owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner. Documented in docs/ix_canonicity.md 6.5. Call-site surgery guard is now durable across serialization: aux-regen detection accepts `Named.original.is_some()` in addition to the in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles no longer misapply surgery. Shift-aware `instantiate_rev` replaces unshifted substitution in the type-walking helpers (fixes fvar leaks in `.brecOn.go` bodies). Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the ref/univ tables (`preseed_expr_tables`) like every production compile path. The serialized constant embeds those tables in sorted order; compiling without the preseed filled them in traversal order instead, permuting every `Ref`/univ index — byte-different but semantically identical constants (decode resolves through the embedded table). This silently failed the Phase-A address comparison against `Named.original.0` for 1529 of 1545 aux constants (including plain stdlib like `Nat.casesOn`); a debug probe proved compile(original) == compile(regen) in every case, i.e. the regeneration itself was always faithful. With the invariant holding corpus-wide, the Phase-A recompile-hash mismatch is now a hard error with no aux exemption, and every roundtrip arm records failures in `aux_gen_errors` (recovery keeps the Lean-facing env populated for diagnosis but is never silent). Pass-2 scope hygiene: the below-def roundtrip loop filters by the original-gated `aux_members` like its sibling loops, so evaporated `below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now dumps hashed component scalars/hashes and runs an original-form recompile probe for any mismatch. Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry recomputation-honest flags so compile-side `validate_ind_flags` no longer poisons the shared tutorial env (73/335 -> 335/335, with the kernel rejecting each bad fixture as designed); validate-aux seeds match module-private fixture names via `privateToUserName?` and enable the Canonicity prefix; Phase 4b gains per-module markers so a fully absent identity group fails loudly when its fixture module is loaded (previously vacuous at 0 pass / 0 fail, now 109 pass). Gates: kernel-check-env 201296/201296; rust-compile all phases with 0 aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the full 213k env (live and deserialized); validate-aux 0 failures at 4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip 143694/0; kernel-tutorial 335/335; cargo test and lake test green.

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`: map_or over map+unwrap_or and slice::contains in surgery.rs, an enumerate loop for the motive-peeling walk in aux_motive_sigs, and let-chain collapses for the inductive-flags fixup loops in decompile.rs and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over from the previous commit.

Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).

Port of the two Rust kernel fixes on this branch: - Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand (computed_is_rec_ind), nested detection is structural (member_has_nested / ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten member-scoped without the declared nested count. Serialization packs one bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive addresses re-pinned. - collectDependencies (Ix/Common.lean) now closes over a declaration's full recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference in rule RHSs) plus each rule ctor's owning external recursor (List.rec). Without these the per-name compile either failed (MissingConstant AuxDedup1.C.rec from A.rec_1's block) or silently skipped the evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2 in original form, which the kernel rejects. AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join kernelCheckEntries; the four evaporated rec_N entries pin the identical 3_073_003 FFT cost (their claims are byte-exact List.rec: lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2). All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

…nment-machine WHNF reducer (#442) * kernel: uid identity, env-machine WHNF, and reduction-loop perf Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%. * kernel: native perf/shard examples (out-of-circuit tooling) Standalone cargo examples over a .ixe env, bypassing the Lean/FFI layer, updated to main's steps-based shard cost model (block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram): - shard_plan: profile → partition → .ixes manifest, with store-aware planning (--store-dir drops work items whose targets the proof store already covers, and excludes covered blocks from the partition hypergraph — a novel→covered edge is an assumption discharged at aggregation, not a cut to minimize); sizes N from machine RAM by default. - perf_check / check_one: native rerun of the guest check_const loop so IX_* perf-counter instrumentation can target a single expensive constant without re-checking its env. - heaviest_block / block_reduce_histo / shard_names / manifest_info: profiling forensics over blocks and manifests. * zisk+sp1: prover batch scripts and logs; bench-compile-init - zisk/scripts: prove-batch (sequential shard proving), mem-guard (MemAvailable watchdog that kills zisk-host before the OOM killer wedges the box), bench-cycles, mergesort-250k repro; reference logs. - sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with WITHOUT_VK_VERIFICATION=1). - Lean side: bench-compile-init lake exe (imports Init, empty main). * zisk: close aggregation soundness gaps (failures word, transitive vk pinning) The aggregate proof was weaker than "these subjects are well-typed": - The agg guest never read a child's committed failures word (slot 10) and hard-committed 0 for its own, so aggregation ERASED the failure bit — a kernel-rejected constant could appear under a failures=0 root, with only host-side courtesy checks in the way. Every child's failures word is now asserted 0 in-circuit. - vk pinning was not transitive: a child that is itself an aggregate was pinned only by its program vk (the shared AGG vk); its own allowed-vk set was never inspected. An agg-of-1 built against a rogue allowed set (wrapping an arbitrary program's "proof" with forged publics) would fold under an honest-looking root. The agg guest now requires every aggregate child (allowed-set index ≥ 1, by the new positional convention: index 0 = leaf vk, the rest agg vks) to commit THIS instance's vks id — the allowed set is uniform down the tree, so the pin is recursive. The convention's ordering is bound by the committed id hash, which external verifiers already check. - The host derived the allowed set FROM the untrusted child proofs (distinct_vks), so any proof admitted its own program, and a stale store folded silently under its old vk. The allowed set is now [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk after ROM setup); freshly produced proofs are asserted to match; stored proofs with a different vk are skipped (re-proven); and the root's committed vks id is checked against — and printed for — external verifiers. - A manifest bisection tree whose leaf set differs from the shard id set silently dropped proven leaves from the fold while the pre-aggregation coverage check (counting proofs PRODUCED, not folded) still passed. ShardManifest::from_bytes now rejects such trees, and the host additionally checks post-fold that every env target is in the root's actual subject set. * ixon: memoize deferred address verification (one hash per constant per load) The bench run on the rebase preview (06e1a1d) showed the whole-env ooc/InitStd row at +63.9% (10.96 s -> 17.97 s) while every per-constant row improved. Cause: LazyConstant::get() re-ran Address::hash(bytes) on every materialization, and the check loop re-ingresses each work item's closure after clear_releasing_memory() (IX_KERNEL_CHECK_CLEAR_EVERY=1), so each constant was re-hashed once per closure it appears in — inside the timed window. Pre-deferral the total was one hash per constant, at load time. Memoize the SUCCESSFUL check per entry (Arc<AtomicBool>, shared by clones, which share the bytes): the first get() still hash-checks before parsing; later get()s skip the hash. Failures are never memoized — bytes are immutable, so a mismatched entry re-fails on every call. This restores the one-hash-per-constant total while keeping load lazy. Also: unit tests for the deferred path (verify-once, failure never memoized, clones share the verdict), drop a dead 'let _ = i;' in get_anon, and note the memoization in docs/kernel_identity.md. * verify: make the pinned trust-frontier statements dischargeable ExecutionRequests' set/modifyGet constructors certified an arbitrary silent state transformation with an empty request list, so any program could be rewritten (funext + of_eq) as modifyGet-of-its-own-run bound into a pure/throw dispatch — ExecutionRequests x s [] held for every program, RunAssumptions was satisfiable with a support covering only the initial intern table, and the module docstring's central claim ("no constructor for an arbitrary silent computation") was false. Independently, the four headline statements universally quantified {semantics : CacheSemantics} — blockErrorsOnly is a lawful instance that invalidates every .expr cache insertion, refuting any run that warms a cache — and demanded the fixed support cover the POST-state intern table, refuting any run that interns. TcM.checkConst.wf was refutable outright; the other three were shielded only by the opaque StatementTrKExpr. set/modifyGet now carry intern-preservation hypotheses at the indexed state, and the new ExecutionRequests.intern_eq_of_nil proves the guarantee machine-checked: a []-certificate forces an unchanged intern table on both outcomes, so requests are an honest upper bound on a run's interning and the support quantifier matches the documented choose-final-support-up-front design. The statements pin an opaque StatementCacheSemantics stub (the K1 machinery is proved only for the whnfCacheSemantics family; arbitrary keys/fallbacks are refutable), so KernelRunInv no longer quantifies over semantics. Statement names and the four-sorry frontier are unchanged; NatFixture's satisfiability witnesses compile verbatim. * tc: mirror the kernel's Nat-offset machinery in the Lean spec The offset work landed Rust-side only, so spec and implementation disagreed on exactly the large-offset inputs it was built for: Rust strips a shared offset in one step, keeps 'Nat.add base (Lit n)' / 'Nat.div|mod base (Lit k)' stuck in compact form, and collapses symbolic-base linear Nat.rec to the compact offset, while Lean still peeled one succ per isDefEqCall level (maxRecDepth at k ≈ 2000, and succ-tower materialization in WHNF beyond 10k) and required a literal base for the linear-rec collapse. Port all three pieces: tryDefEqOffset decomposes both sides via natOffsetDecompose behind an O(1) natOffsetCandidate probe and strips the shared offset in one step (verdict-preserving by definitional +k injectivity); tryNatOffsetStuck freezes compact offset forms before delta at the same decision point as the Rust loop; and tryReduceNatSuccLinearRec gains the symbolic-base branch, gated on the recursor application carrying no post-major arguments. Verify ripple: the natRecLiteralParts totalization equation picks up majorIdx, and NatFixture's full-WHNF step walk certifies the offset-stuck probe returns none on the fixture for any primitive address assignment. Tests pin each piece against regressions: stays-compact under decoy Nat.add/div/mod definitions that delta would expose, the bulk strip at k = 2500 (one-succ peeling exceeds the def-eq depth limit there), div-derived vs add-derived stuck forms staying unequal, and the linear-rec collapse with its post-major conservatism. * tests: drop the tc-node-addr bit-parity harness Uid identity removed per-node content addresses from the Rust kernel, so the oracle dump's ty/extra columns became 16-hex intern uids — process-history-dependent values that can never byte-match the Lean side's Blake3 node addresses. The suite could only fail, and since ignored.yml runs 'lake test -- --ignored' on every push to main, it would turn Extended CI red on merge. The one column still comparable (the constant id) is read from the same serialized env bytes on both sides, so a slimmed comparison would check only traversal enumeration — coverage tc-anon-diff already provides against the real Rust verdicts. Remove the suite, its FFI oracle, and the extern binding; reword the Egress module doc that cited the harness as a level-reduction certifier. * kernel: allocate intern uids in thread-local blocks NEXT_UID was a single process-global cache line hit by a relaxed fetch_add for every node interned by every checker worker. The blake3 identity it replaced was pure per-worker work, so the old kernel scaled linearly with workers; the uid kernel is ~1.4x faster per core but its whole-env throughput plateaued near 5.7K consts/s as worker counts grew — the ooc InitStd !benchmark regression (9.96 s -> 16.97 s on the 32-thread bench runner, while every per-constant row improved; the same binaries tie at 24 local workers and the uid side wins 1.41x at 6). Hand out uids in per-thread blocks of 2^20 reserved from the global counter, touching the shared line once per block instead of once per node. Blocks are never reused (a thread's unspent remainder is abandoned on exit), so uid uniqueness and the never-reuse cache-key guarantee are unchanged; the exhaustion guard aborts a block early instead of one uid early. Local whole-env InitStd at 24 workers drops 15.58 s -> 11.04 s (old kernel: 15.49 s), and 6->24 worker scaling recovers from 1.60x to 2.02x. * bench: record tool faults as crash, not oom A 128+signal death was always recorded as an OOM row, so a zisk mem-planner segfault (exit 139) rendered as OOM and sent the investigation chasing RAM budgets instead of a heap-overflow bug. Split the kill statuses: explicit kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other signal death records status crash and renders as 💥 CRASH in the compare table. * kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2) The profiler counted whnf entries, def-eq entries, and limb-weighted Nat arithmetic per constant but dropped them at block aggregation, and nothing counted term-construction volume at all — leaving the shard cost model only heartbeats, subst, and bytes to predict guest steps from. Persist all four op counters per block (format v2) plus a new intern-table visit counter (a proxy for construction/memory traffic, bumped in intern_expr/intern_univ), and add a shard_features example that emits a per-shard feature CSV from a profile + manifest pair for calibrating the cost model against externally measured shard costs (ziskemu -X on dumped shard inputs). * zisk: dump every selected shard's input; skip ROM setup in dump mode --dump-input wrote only the first selected shard and exited, so dumping a 13-shard plan took 13 host invocations. Dump every selected shard in one run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard keeps the exact path), and skip client.setup when no proof store is involved — dump mode never runs the VM and needs the ROM setup (and thus the proving key) only to derive the shard vk for store filtering. * kernel: calibrate the shard planner in Zisk cost units Replace the heartbeat-based guest-STEP model with one denominated in ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES + BASE), so the packing target prices the axes that don't ride the main trace — DMA/blake3 precompile area and memory ops. Calibration corpus: 118 InitStd shards across 13 constants, each measured with ziskemu -X on inputs dumped via --dump-input. cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq + 28.4k*intern (+ 73.2k per cross-ingress byte) MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per work item, so intra-shard cache sharing is invisible to per-block features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram. On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on the uid-identity kernel; the intern term carries the memory-traffic/DMA axis (residual correlation 0.91 with dma_memcpy counts). Prover models refit on the same corpus. RAM comes from a guarded GPU prove sweep measured as each prover's systemd-scope cgroup memory.peak — the OOM-relevant metric CI's watchdog enforces, charging the whole process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost (was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s measured vs 411s predicted at the largest point). Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards (instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within the actual-cost ceiling; the only violations are the two INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB single-leaf), correctly flagged as not fitting the budget. * bench: per-constant ooc attribution and a compare top-movers drill-down A whole-env ooc regression previously surfaced as one env-keyed number, with drill-down only into the pre-chosen bench vectors. Now the anon whole-env check attributes itself: check-rs --per-const <csv> records one entry per work item (wall nanos, heartbeats, the op counters, and the predicted Zisk cost via the shard model) from the check loop, and the CLI joins Lean names from the env's named table (projection-name fallback for anonymized Muts blocks) so entries survive PRs that shift content addresses. An entry is ONE constant's (or Muts block's) own check — deps are lazily ingressed and trusted, each checked in its own entry, with the consulted closure slice's ingress charged to the entry — so entries sum to the env total with no double counting. NOT the full-closure scope of --consts measurements; documented at the recording site, the flag help, the renderer, and in the rendered output. The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to the results file (rotated with the local baseline), and ix bench compare renders a drill-down when both sides carry one, split by evidence quality — calibrated on a Mathlib A/A run (640K constants, twice through one binary): wall time swings up to 2.8s from scheduling alone, while the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9 absolute; worker->item assignment varies uid blocks and uid-keyed hash iteration order perturbs a few order-sensitive paths; --workers 1 is exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own cost OR >= 1e9 outright, both above the drift envelope) lead the drill-down ranked by percent change, styled like the main table ('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are quarantined in a labeled noise section capped at 5 rows. On the A/A run this renders 0 cost movers, the truthful reading. * bench: verdict-first cell layout; collapse tables past 5 rows A multi-cell !benchmark comment stacked every cell's full table; long cells (a 40-constant zisk table) buried the verdicts. Each cell now leads with its one-line verdict (and any typecheck failures / empty-side warnings, which stay unconditionally visible), and the comparison table collapses into a <details> block when it has more than 5 rows — small cells (the ooc env row, few-constant runs) stay inline. The per-constant and phase drill-downs were already collapsible. * ci: wire the ooc attribution CSV through the !benchmark pipeline bencher.dev stores metric rows only, so the per-constant drill-down needs the attribution CSVs to travel beside the results files. bench-main caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores the base SHA's entry, carries a base-run-produced CSV through the merge step (which previously renamed base.json into main.json and orphaned it), and pairs whichever CSV it has with the PR side's. The main side ends up with exactly two sources: bencher on FULL coverage (plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun for anything less — base SHA not uploaded, partial coverage, an ooc attribution cache miss, or the fresh token. A rerun measures the full default selection (a BENCH_CONSTS override still narrows it) and its rows take priority; bencher-fetched rows only fill rows the rerun failed to produce, and the table's main-source label says which path ran. This retires the gap-filling machinery (--consts from missing.txt, the bencher-priority merge arm) — a full rerun is simpler and self-consistent, at the cost of re-measuring a cell when a PR adds constants. * zisk: drop the vendored guest linker script Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the riscv64ima-zisk-zkvm-elf linker script in the target spec again, and passing the vendored copy on top double-defines the rom/ram memory regions. Both guest build scripts existed only to pass it — remove them and the script; the toolchain's embedded script is the single source of the memory layout. * zisk: pin the fork branch with the mem-planner fill_padding fix Bump every zisk fork pin from blake3-precompile (e4057c4) to blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows the mem-planner offsets array before fill_padding pads the last page — the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the shard that crashed 4/4 on the old pin executes clean on the new one (634M cycles, failures=0), as does the full 13-shard plan on the locally-patched build the fix was developed against. * chore: fix clippy lints (casts, qualifications, poison error, let-chain) u32::try_from over as-truncation and u64::from over as-widening in shard_features; drop redundant std::sync:: qualifications; carry the PoisonError text instead of discarding it; collapse the texray if into a let-chain; contains() over iter().any() in the holed-work filter. * chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build deliberately skips the guest compilation under clippy, but include_elf! still demanded the ELF bytes. Gate the embed (and its import) on cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes under clippy. Also collapse the texray if into a let-chain, matching the zisk host. A real release build of the host still works. * ci: clippy gates for the zisk and sp1 host workspaces The root rust-test clippy never enters the standalone zkVM workspaces, so their warnings accumulated ungated. Add cargo clippy --release --all-targets -D warnings to both host jobs, after the build so the release dep artifacts are shared (and, for zisk, the guest ELFs its build scripts already produced). * chore: String.dropEnd over deprecated String.dropRight * Unpin ziskup install * ci: align install-zisk comments with the unpinned toolchain * Clean up dev tooling and experiment artifacts for PR - Untrack sp1/zisk benchmark logs and scripts - Remove dev-tooling examples from ix-kernel: examples are for showing users how to use the crate; the shard-planning and perf binaries live on in git history - Remove the env-machine design doc; the as-built machine is documented at the code (whnf.rs machine_whnf, subst.rs Clo) --------- Co-authored-by: John C. Burnham <john@agathic.com>

johnchandlerburnham · 2026-07-04T06:34:29Z

Summary

Two related changes to the content-addressing layer and its aux-constant handling, fixing underlying issue reported in #465

1. Ixon no longer stores recr/refl/nested on Inductive. These are derivable
from constructor structure, so storing them was redundant and trusting declared values
was an adversarial surface (e.g. is_rec = false on a recursive inductive enables
improper struct-eta). The kernel now computes is_rec on demand, memoized in a new env
cache with a provisional entry to break the whnf → try_struct_eta_iota → is_struct_like
cycle; this replaces the declared-vs-computed check in check_inductive. The compile
side gains compute_lean_ind_flags to recompute Lean's block-wide
isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a
source Lean env (kernel egress, decompile), and validate_lean_ind_flags to check a
whole env against the recomputation.

2. Evaporated auxiliaries get a canonical form. When SCC splitting strands a nested
aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and
dropping the irrelevant over-merged motives leaves exactly the external inductive's
generic recursor. Canonical treatment: rec_N claims alias <Ext>.rec (e.g.
List.rec), call sites are rebuilt onto the external telescope via head-rewrite
CallSitePlans (owner-gated, single-motive targets), and below_N/brecOn_N compile as
surgered originals like _sizeOf_N. Fixes the AuxDedup kernel-check failures (28 → 0);
AuxDedup1 now generates auxiliaries identical to AuxDedup2's canonical structure.
Documented in docs/ix_canonicity.md §6.5.

Byte-exact aux roundtrip

roundtrip_block Phase A (recompile the regenerated Lean form, compare against the
stored original address) silently failed for 1529 of 1545 aux constants — including
plain stdlib like Nat.casesOn. Root cause: every production compile path preseeds the
ref/univ tables in sorted order (preseed_expr_tables) before compiling, and the
serialized constant embeds those tables; Phase A compiled without the preseed, filling
the tables in traversal order instead — every Ref/univ index permuted, byte-different
but semantically identical constants (decode resolves through the embedded table). A
debug probe recompiling the Lean original through the identical path proved
compile(original) == compile(regen) in every case: regeneration was always faithful,
the comparison context was not.

With the preseed mirrored in Phase A the invariant holds corpus-wide, so a Phase-A
recompile-hash mismatch is now a hard error with no aux exemption, and every
roundtrip arm records failures in aux_gen_errors (recovery keeps the Lean-facing env
populated for diagnosis but is never silent). Related hardening: call-site surgery
detection is durable across serialization (Named.original.is_some() alongside the
in-memory map), shift-aware instantiate_rev in the type-walking helpers (fixes fvar
leaks in .brecOn.go bodies), and the below-def roundtrip loop filters by the
original-gated members like its sibling loops. IX_ROUNDTRIP_DEBUG now dumps hashed
component summaries and runs an original-form recompile probe on any mismatch.

Test fixes and fixtures

kernel-tutorial: bad_raw_consts inductive fixtures carry recomputation-honest flags
so the whole-env validate_ind_flags no longer poisons the shared tutorial env
(73/335 → 335/335, with the kernel rejecting each bad fixture as designed).
validate-aux: seeds match module-private fixture names via privateToUserName?, the
Canonicity prefix is enabled, and Phase 4b gains per-module markers so a fully absent
identity group fails loudly when its fixture module is loaded (previously vacuous at
0 pass / 0 fail, now 109 pass / 0 fail).
New fixtures: AuxDedup1/AuxDedup2 (cross-block aux dedup), AuxDedupMixed (a perm
mixing a canonical slot and PERM_OUT_OF_SCC for the same owner), plus a
CompileMutualFixtures benchmark lib.

Gates

kernel-check-env: 201296/201296
rust-compile: all phases, 0 aux_gen errors / 0 mismatches / 0 Phase-A address
divergences on the full 213k env (live and deserialized)
validate-aux: 0 failures at 4393-constant scope
rust-serialize: byte-exact; kernel-ixon-roundtrip: 143694/0
kernel-tutorial: 335/335; cargo test workspace and lake test green;
cargo clippy --all-targets clean
lake exe ix check-rs compilemathlib.ixe: 736618/736618 passed, 0 failed (325.3s)
lake exe ix validate Benchmarks/Compile/CompileMathlib.lean: 0 failures (1528.33s total)

Remove the `recr`/`refl` bools and the `nested` count from the Ixon `Inductive` constant and its serialization (Rust and Lean), and from the `Indc` reveal-proof variant, renumbering the field-presence mask bits. These flags are derivable from constructor structure, so storing them was redundant and trusting declared values was an adversarial surface (e.g. is_rec = false on a recursive inductive enables improper struct-eta). - kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now computed on demand (computed_is_rec), memoized in the new env is_rec_cache with a provisional entry to break the whnf -> try_struct_eta_iota -> is_struct_like cycle. This replaces the declared-vs-computed H1 verification in check_inductive. - compile: new compute_lean_ind_flags recomputes Lean's block-wide isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a source Lean env (kernel egress, decompile), since Ixon no longer stores the flags; validate_lean_ind_flags checks a whole env against the recomputation. - tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising aux-constant dedup across blocks (fix forthcoming); add a CompileMutualFixtures benchmark lib building the mutual test fixtures; ignore *.ixe.

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a nested aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and dropping the irrelevant over-merged motives leaves exactly the external inductive's generic recursor. Canonical treatment: `rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are rebuilt onto the external telescope via head-rewrite CallSitePlans (owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner. Documented in docs/ix_canonicity.md 6.5. Call-site surgery guard is now durable across serialization: aux-regen detection accepts `Named.original.is_some()` in addition to the in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles no longer misapply surgery. Shift-aware `instantiate_rev` replaces unshifted substitution in the type-walking helpers (fixes fvar leaks in `.brecOn.go` bodies). Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the ref/univ tables (`preseed_expr_tables`) like every production compile path. The serialized constant embeds those tables in sorted order; compiling without the preseed filled them in traversal order instead, permuting every `Ref`/univ index — byte-different but semantically identical constants (decode resolves through the embedded table). This silently failed the Phase-A address comparison against `Named.original.0` for 1529 of 1545 aux constants (including plain stdlib like `Nat.casesOn`); a debug probe proved compile(original) == compile(regen) in every case, i.e. the regeneration itself was always faithful. With the invariant holding corpus-wide, the Phase-A recompile-hash mismatch is now a hard error with no aux exemption, and every roundtrip arm records failures in `aux_gen_errors` (recovery keeps the Lean-facing env populated for diagnosis but is never silent). Pass-2 scope hygiene: the below-def roundtrip loop filters by the original-gated `aux_members` like its sibling loops, so evaporated `below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now dumps hashed component scalars/hashes and runs an original-form recompile probe for any mismatch. Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry recomputation-honest flags so compile-side `validate_ind_flags` no longer poisons the shared tutorial env (73/335 -> 335/335, with the kernel rejecting each bad fixture as designed); validate-aux seeds match module-private fixture names via `privateToUserName?` and enable the Canonicity prefix; Phase 4b gains per-module markers so a fully absent identity group fails loudly when its fixture module is loaded (previously vacuous at 0 pass / 0 fail, now 109 pass). Gates: kernel-check-env 201296/201296; rust-compile all phases with 0 aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the full 213k env (live and deserialized); validate-aux 0 failures at 4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip 143694/0; kernel-tutorial 335/335; cargo test and lake test green.

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`: map_or over map+unwrap_or and slice::contains in surgery.rs, an enumerate loop for the motive-peeling walk in aux_motive_sigs, and let-chain collapses for the inductive-flags fixup loops in decompile.rs and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over from the previous commit.

Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).

Port of the two Rust kernel fixes on this branch: - Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand (computed_is_rec_ind), nested detection is structural (member_has_nested / ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten member-scoped without the declared nested count. Serialization packs one bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive addresses re-pinned. - collectDependencies (Ix/Common.lean) now closes over a declaration's full recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference in rule RHSs) plus each rule ctor's owning external recursor (List.rec). Without these the per-name compile either failed (MissingConstant AuxDedup1.C.rec from A.rec_1's block) or silently skipped the evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2 in original form, which the kernel rejects. AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join kernelCheckEntries; the four evaporated rec_N entries pin the identical 3_073_003 FFT cost (their claims are byte-exact List.rec: lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2). All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

…nment-machine WHNF reducer (#442) * kernel: uid identity, env-machine WHNF, and reduction-loop perf Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%. * kernel: native perf/shard examples (out-of-circuit tooling) Standalone cargo examples over a .ixe env, bypassing the Lean/FFI layer, updated to main's steps-based shard cost model (block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram): - shard_plan: profile → partition → .ixes manifest, with store-aware planning (--store-dir drops work items whose targets the proof store already covers, and excludes covered blocks from the partition hypergraph — a novel→covered edge is an assumption discharged at aggregation, not a cut to minimize); sizes N from machine RAM by default. - perf_check / check_one: native rerun of the guest check_const loop so IX_* perf-counter instrumentation can target a single expensive constant without re-checking its env. - heaviest_block / block_reduce_histo / shard_names / manifest_info: profiling forensics over blocks and manifests. * zisk+sp1: prover batch scripts and logs; bench-compile-init - zisk/scripts: prove-batch (sequential shard proving), mem-guard (MemAvailable watchdog that kills zisk-host before the OOM killer wedges the box), bench-cycles, mergesort-250k repro; reference logs. - sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with WITHOUT_VK_VERIFICATION=1). - Lean side: bench-compile-init lake exe (imports Init, empty main). * zisk: close aggregation soundness gaps (failures word, transitive vk pinning) The aggregate proof was weaker than "these subjects are well-typed": - The agg guest never read a child's committed failures word (slot 10) and hard-committed 0 for its own, so aggregation ERASED the failure bit — a kernel-rejected constant could appear under a failures=0 root, with only host-side courtesy checks in the way. Every child's failures word is now asserted 0 in-circuit. - vk pinning was not transitive: a child that is itself an aggregate was pinned only by its program vk (the shared AGG vk); its own allowed-vk set was never inspected. An agg-of-1 built against a rogue allowed set (wrapping an arbitrary program's "proof" with forged publics) would fold under an honest-looking root. The agg guest now requires every aggregate child (allowed-set index ≥ 1, by the new positional convention: index 0 = leaf vk, the rest agg vks) to commit THIS instance's vks id — the allowed set is uniform down the tree, so the pin is recursive. The convention's ordering is bound by the committed id hash, which external verifiers already check. - The host derived the allowed set FROM the untrusted child proofs (distinct_vks), so any proof admitted its own program, and a stale store folded silently under its old vk. The allowed set is now [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk after ROM setup); freshly produced proofs are asserted to match; stored proofs with a different vk are skipped (re-proven); and the root's committed vks id is checked against — and printed for — external verifiers. - A manifest bisection tree whose leaf set differs from the shard id set silently dropped proven leaves from the fold while the pre-aggregation coverage check (counting proofs PRODUCED, not folded) still passed. ShardManifest::from_bytes now rejects such trees, and the host additionally checks post-fold that every env target is in the root's actual subject set. * ixon: memoize deferred address verification (one hash per constant per load) The bench run on the rebase preview (06e1a1d) showed the whole-env ooc/InitStd row at +63.9% (10.96 s -> 17.97 s) while every per-constant row improved. Cause: LazyConstant::get() re-ran Address::hash(bytes) on every materialization, and the check loop re-ingresses each work item's closure after clear_releasing_memory() (IX_KERNEL_CHECK_CLEAR_EVERY=1), so each constant was re-hashed once per closure it appears in — inside the timed window. Pre-deferral the total was one hash per constant, at load time. Memoize the SUCCESSFUL check per entry (Arc<AtomicBool>, shared by clones, which share the bytes): the first get() still hash-checks before parsing; later get()s skip the hash. Failures are never memoized — bytes are immutable, so a mismatched entry re-fails on every call. This restores the one-hash-per-constant total while keeping load lazy. Also: unit tests for the deferred path (verify-once, failure never memoized, clones share the verdict), drop a dead 'let _ = i;' in get_anon, and note the memoization in docs/kernel_identity.md. * verify: make the pinned trust-frontier statements dischargeable ExecutionRequests' set/modifyGet constructors certified an arbitrary silent state transformation with an empty request list, so any program could be rewritten (funext + of_eq) as modifyGet-of-its-own-run bound into a pure/throw dispatch — ExecutionRequests x s [] held for every program, RunAssumptions was satisfiable with a support covering only the initial intern table, and the module docstring's central claim ("no constructor for an arbitrary silent computation") was false. Independently, the four headline statements universally quantified {semantics : CacheSemantics} — blockErrorsOnly is a lawful instance that invalidates every .expr cache insertion, refuting any run that warms a cache — and demanded the fixed support cover the POST-state intern table, refuting any run that interns. TcM.checkConst.wf was refutable outright; the other three were shielded only by the opaque StatementTrKExpr. set/modifyGet now carry intern-preservation hypotheses at the indexed state, and the new ExecutionRequests.intern_eq_of_nil proves the guarantee machine-checked: a []-certificate forces an unchanged intern table on both outcomes, so requests are an honest upper bound on a run's interning and the support quantifier matches the documented choose-final-support-up-front design. The statements pin an opaque StatementCacheSemantics stub (the K1 machinery is proved only for the whnfCacheSemantics family; arbitrary keys/fallbacks are refutable), so KernelRunInv no longer quantifies over semantics. Statement names and the four-sorry frontier are unchanged; NatFixture's satisfiability witnesses compile verbatim. * tc: mirror the kernel's Nat-offset machinery in the Lean spec The offset work landed Rust-side only, so spec and implementation disagreed on exactly the large-offset inputs it was built for: Rust strips a shared offset in one step, keeps 'Nat.add base (Lit n)' / 'Nat.div|mod base (Lit k)' stuck in compact form, and collapses symbolic-base linear Nat.rec to the compact offset, while Lean still peeled one succ per isDefEqCall level (maxRecDepth at k ≈ 2000, and succ-tower materialization in WHNF beyond 10k) and required a literal base for the linear-rec collapse. Port all three pieces: tryDefEqOffset decomposes both sides via natOffsetDecompose behind an O(1) natOffsetCandidate probe and strips the shared offset in one step (verdict-preserving by definitional +k injectivity); tryNatOffsetStuck freezes compact offset forms before delta at the same decision point as the Rust loop; and tryReduceNatSuccLinearRec gains the symbolic-base branch, gated on the recursor application carrying no post-major arguments. Verify ripple: the natRecLiteralParts totalization equation picks up majorIdx, and NatFixture's full-WHNF step walk certifies the offset-stuck probe returns none on the fixture for any primitive address assignment. Tests pin each piece against regressions: stays-compact under decoy Nat.add/div/mod definitions that delta would expose, the bulk strip at k = 2500 (one-succ peeling exceeds the def-eq depth limit there), div-derived vs add-derived stuck forms staying unequal, and the linear-rec collapse with its post-major conservatism. * tests: drop the tc-node-addr bit-parity harness Uid identity removed per-node content addresses from the Rust kernel, so the oracle dump's ty/extra columns became 16-hex intern uids — process-history-dependent values that can never byte-match the Lean side's Blake3 node addresses. The suite could only fail, and since ignored.yml runs 'lake test -- --ignored' on every push to main, it would turn Extended CI red on merge. The one column still comparable (the constant id) is read from the same serialized env bytes on both sides, so a slimmed comparison would check only traversal enumeration — coverage tc-anon-diff already provides against the real Rust verdicts. Remove the suite, its FFI oracle, and the extern binding; reword the Egress module doc that cited the harness as a level-reduction certifier. * kernel: allocate intern uids in thread-local blocks NEXT_UID was a single process-global cache line hit by a relaxed fetch_add for every node interned by every checker worker. The blake3 identity it replaced was pure per-worker work, so the old kernel scaled linearly with workers; the uid kernel is ~1.4x faster per core but its whole-env throughput plateaued near 5.7K consts/s as worker counts grew — the ooc InitStd !benchmark regression (9.96 s -> 16.97 s on the 32-thread bench runner, while every per-constant row improved; the same binaries tie at 24 local workers and the uid side wins 1.41x at 6). Hand out uids in per-thread blocks of 2^20 reserved from the global counter, touching the shared line once per block instead of once per node. Blocks are never reused (a thread's unspent remainder is abandoned on exit), so uid uniqueness and the never-reuse cache-key guarantee are unchanged; the exhaustion guard aborts a block early instead of one uid early. Local whole-env InitStd at 24 workers drops 15.58 s -> 11.04 s (old kernel: 15.49 s), and 6->24 worker scaling recovers from 1.60x to 2.02x. * bench: record tool faults as crash, not oom A 128+signal death was always recorded as an OOM row, so a zisk mem-planner segfault (exit 139) rendered as OOM and sent the investigation chasing RAM budgets instead of a heap-overflow bug. Split the kill statuses: explicit kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other signal death records status crash and renders as 💥 CRASH in the compare table. * kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2) The profiler counted whnf entries, def-eq entries, and limb-weighted Nat arithmetic per constant but dropped them at block aggregation, and nothing counted term-construction volume at all — leaving the shard cost model only heartbeats, subst, and bytes to predict guest steps from. Persist all four op counters per block (format v2) plus a new intern-table visit counter (a proxy for construction/memory traffic, bumped in intern_expr/intern_univ), and add a shard_features example that emits a per-shard feature CSV from a profile + manifest pair for calibrating the cost model against externally measured shard costs (ziskemu -X on dumped shard inputs). * zisk: dump every selected shard's input; skip ROM setup in dump mode --dump-input wrote only the first selected shard and exited, so dumping a 13-shard plan took 13 host invocations. Dump every selected shard in one run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard keeps the exact path), and skip client.setup when no proof store is involved — dump mode never runs the VM and needs the ROM setup (and thus the proving key) only to derive the shard vk for store filtering. * kernel: calibrate the shard planner in Zisk cost units Replace the heartbeat-based guest-STEP model with one denominated in ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES + BASE), so the packing target prices the axes that don't ride the main trace — DMA/blake3 precompile area and memory ops. Calibration corpus: 118 InitStd shards across 13 constants, each measured with ziskemu -X on inputs dumped via --dump-input. cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq + 28.4k*intern (+ 73.2k per cross-ingress byte) MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per work item, so intra-shard cache sharing is invisible to per-block features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram. On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on the uid-identity kernel; the intern term carries the memory-traffic/DMA axis (residual correlation 0.91 with dma_memcpy counts). Prover models refit on the same corpus. RAM comes from a guarded GPU prove sweep measured as each prover's systemd-scope cgroup memory.peak — the OOM-relevant metric CI's watchdog enforces, charging the whole process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost (was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s measured vs 411s predicted at the largest point). Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards (instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within the actual-cost ceiling; the only violations are the two INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB single-leaf), correctly flagged as not fitting the budget. * bench: per-constant ooc attribution and a compare top-movers drill-down A whole-env ooc regression previously surfaced as one env-keyed number, with drill-down only into the pre-chosen bench vectors. Now the anon whole-env check attributes itself: check-rs --per-const <csv> records one entry per work item (wall nanos, heartbeats, the op counters, and the predicted Zisk cost via the shard model) from the check loop, and the CLI joins Lean names from the env's named table (projection-name fallback for anonymized Muts blocks) so entries survive PRs that shift content addresses. An entry is ONE constant's (or Muts block's) own check — deps are lazily ingressed and trusted, each checked in its own entry, with the consulted closure slice's ingress charged to the entry — so entries sum to the env total with no double counting. NOT the full-closure scope of --consts measurements; documented at the recording site, the flag help, the renderer, and in the rendered output. The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to the results file (rotated with the local baseline), and ix bench compare renders a drill-down when both sides carry one, split by evidence quality — calibrated on a Mathlib A/A run (640K constants, twice through one binary): wall time swings up to 2.8s from scheduling alone, while the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9 absolute; worker->item assignment varies uid blocks and uid-keyed hash iteration order perturbs a few order-sensitive paths; --workers 1 is exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own cost OR >= 1e9 outright, both above the drift envelope) lead the drill-down ranked by percent change, styled like the main table ('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are quarantined in a labeled noise section capped at 5 rows. On the A/A run this renders 0 cost movers, the truthful reading. * bench: verdict-first cell layout; collapse tables past 5 rows A multi-cell !benchmark comment stacked every cell's full table; long cells (a 40-constant zisk table) buried the verdicts. Each cell now leads with its one-line verdict (and any typecheck failures / empty-side warnings, which stay unconditionally visible), and the comparison table collapses into a <details> block when it has more than 5 rows — small cells (the ooc env row, few-constant runs) stay inline. The per-constant and phase drill-downs were already collapsible. * ci: wire the ooc attribution CSV through the !benchmark pipeline bencher.dev stores metric rows only, so the per-constant drill-down needs the attribution CSVs to travel beside the results files. bench-main caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores the base SHA's entry, carries a base-run-produced CSV through the merge step (which previously renamed base.json into main.json and orphaned it), and pairs whichever CSV it has with the PR side's. The main side ends up with exactly two sources: bencher on FULL coverage (plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun for anything less — base SHA not uploaded, partial coverage, an ooc attribution cache miss, or the fresh token. A rerun measures the full default selection (a BENCH_CONSTS override still narrows it) and its rows take priority; bencher-fetched rows only fill rows the rerun failed to produce, and the table's main-source label says which path ran. This retires the gap-filling machinery (--consts from missing.txt, the bencher-priority merge arm) — a full rerun is simpler and self-consistent, at the cost of re-measuring a cell when a PR adds constants. * zisk: drop the vendored guest linker script Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the riscv64ima-zisk-zkvm-elf linker script in the target spec again, and passing the vendored copy on top double-defines the rom/ram memory regions. Both guest build scripts existed only to pass it — remove them and the script; the toolchain's embedded script is the single source of the memory layout. * zisk: pin the fork branch with the mem-planner fill_padding fix Bump every zisk fork pin from blake3-precompile (e4057c4) to blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows the mem-planner offsets array before fill_padding pads the last page — the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the shard that crashed 4/4 on the old pin executes clean on the new one (634M cycles, failures=0), as does the full 13-shard plan on the locally-patched build the fix was developed against. * chore: fix clippy lints (casts, qualifications, poison error, let-chain) u32::try_from over as-truncation and u64::from over as-widening in shard_features; drop redundant std::sync:: qualifications; carry the PoisonError text instead of discarding it; collapse the texray if into a let-chain; contains() over iter().any() in the holed-work filter. * chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build deliberately skips the guest compilation under clippy, but include_elf! still demanded the ELF bytes. Gate the embed (and its import) on cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes under clippy. Also collapse the texray if into a let-chain, matching the zisk host. A real release build of the host still works. * ci: clippy gates for the zisk and sp1 host workspaces The root rust-test clippy never enters the standalone zkVM workspaces, so their warnings accumulated ungated. Add cargo clippy --release --all-targets -D warnings to both host jobs, after the build so the release dep artifacts are shared (and, for zisk, the guest ELFs its build scripts already produced). * chore: String.dropEnd over deprecated String.dropRight * Unpin ziskup install * ci: align install-zisk comments with the unpinned toolchain * Clean up dev tooling and experiment artifacts for PR - Untrack sp1/zisk benchmark logs and scripts - Remove dev-tooling examples from ix-kernel: examples are for showing users how to use the crate; the shard-planning and perf binaries live on in git history - Remove the env-machine design doc; the as-built machine is documented at the code (whnf.rs machine_whnf, subst.rs Clo) --------- Co-authored-by: John C. Burnham <john@agathic.com>

johnchandlerburnham · 2026-07-04T06:34:29Z

Summary

Two related changes to the content-addressing layer and its aux-constant handling, fixing underlying issue reported in #465

1. Ixon no longer stores recr/refl/nested on Inductive. These are derivable
from constructor structure, so storing them was redundant and trusting declared values
was an adversarial surface (e.g. is_rec = false on a recursive inductive enables
improper struct-eta). The kernel now computes is_rec on demand, memoized in a new env
cache with a provisional entry to break the whnf → try_struct_eta_iota → is_struct_like
cycle; this replaces the declared-vs-computed check in check_inductive. The compile
side gains compute_lean_ind_flags to recompute Lean's block-wide
isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a
source Lean env (kernel egress, decompile), and validate_lean_ind_flags to check a
whole env against the recomputation.

2. Evaporated auxiliaries get a canonical form. When SCC splitting strands a nested
aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and
dropping the irrelevant over-merged motives leaves exactly the external inductive's
generic recursor. Canonical treatment: rec_N claims alias <Ext>.rec (e.g.
List.rec), call sites are rebuilt onto the external telescope via head-rewrite
CallSitePlans (owner-gated, single-motive targets), and below_N/brecOn_N compile as
surgered originals like _sizeOf_N. Fixes the AuxDedup kernel-check failures (28 → 0);
AuxDedup1 now generates auxiliaries identical to AuxDedup2's canonical structure.
Documented in docs/ix_canonicity.md §6.5.

Byte-exact aux roundtrip

roundtrip_block Phase A (recompile the regenerated Lean form, compare against the
stored original address) silently failed for 1529 of 1545 aux constants — including
plain stdlib like Nat.casesOn. Root cause: every production compile path preseeds the
ref/univ tables in sorted order (preseed_expr_tables) before compiling, and the
serialized constant embeds those tables; Phase A compiled without the preseed, filling
the tables in traversal order instead — every Ref/univ index permuted, byte-different
but semantically identical constants (decode resolves through the embedded table). A
debug probe recompiling the Lean original through the identical path proved
compile(original) == compile(regen) in every case: regeneration was always faithful,
the comparison context was not.

With the preseed mirrored in Phase A the invariant holds corpus-wide, so a Phase-A
recompile-hash mismatch is now a hard error with no aux exemption, and every
roundtrip arm records failures in aux_gen_errors (recovery keeps the Lean-facing env
populated for diagnosis but is never silent). Related hardening: call-site surgery
detection is durable across serialization (Named.original.is_some() alongside the
in-memory map), shift-aware instantiate_rev in the type-walking helpers (fixes fvar
leaks in .brecOn.go bodies), and the below-def roundtrip loop filters by the
original-gated members like its sibling loops. IX_ROUNDTRIP_DEBUG now dumps hashed
component summaries and runs an original-form recompile probe on any mismatch.

Test fixes and fixtures

kernel-tutorial: bad_raw_consts inductive fixtures carry recomputation-honest flags
so the whole-env validate_ind_flags no longer poisons the shared tutorial env
(73/335 → 335/335, with the kernel rejecting each bad fixture as designed).
validate-aux: seeds match module-private fixture names via privateToUserName?, the
Canonicity prefix is enabled, and Phase 4b gains per-module markers so a fully absent
identity group fails loudly when its fixture module is loaded (previously vacuous at
0 pass / 0 fail, now 109 pass / 0 fail).
New fixtures: AuxDedup1/AuxDedup2 (cross-block aux dedup), AuxDedupMixed (a perm
mixing a canonical slot and PERM_OUT_OF_SCC for the same owner), plus a
CompileMutualFixtures benchmark lib.

Gates

kernel-check-env: 201296/201296
rust-compile: all phases, 0 aux_gen errors / 0 mismatches / 0 Phase-A address
divergences on the full 213k env (live and deserialized)
validate-aux: 0 failures at 4393-constant scope
rust-serialize: byte-exact; kernel-ixon-roundtrip: 143694/0
kernel-tutorial: 335/335; cargo test workspace and lake test green;
cargo clippy --all-targets clean
lake exe ix check-rs compilemathlib.ixe: 736618/736618 passed, 0 failed (325.3s)
lake exe ix validate Benchmarks/Compile/CompileMathlib.lean: 0 failures (1528.33s total)

Remove the `recr`/`refl` bools and the `nested` count from the Ixon `Inductive` constant and its serialization (Rust and Lean), and from the `Indc` reveal-proof variant, renumbering the field-presence mask bits. These flags are derivable from constructor structure, so storing them was redundant and trusting declared values was an adversarial surface (e.g. is_rec = false on a recursive inductive enables improper struct-eta). - kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now computed on demand (computed_is_rec), memoized in the new env is_rec_cache with a provisional entry to break the whnf -> try_struct_eta_iota -> is_struct_like cycle. This replaces the declared-vs-computed H1 verification in check_inductive. - compile: new compute_lean_ind_flags recomputes Lean's block-wide isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a source Lean env (kernel egress, decompile), since Ixon no longer stores the flags; validate_lean_ind_flags checks a whole env against the recomputation. - tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising aux-constant dedup across blocks (fix forthcoming); add a CompileMutualFixtures benchmark lib building the mutual test fixtures; ignore *.ixe.

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a nested aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and dropping the irrelevant over-merged motives leaves exactly the external inductive's generic recursor. Canonical treatment: `rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are rebuilt onto the external telescope via head-rewrite CallSitePlans (owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner. Documented in docs/ix_canonicity.md 6.5. Call-site surgery guard is now durable across serialization: aux-regen detection accepts `Named.original.is_some()` in addition to the in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles no longer misapply surgery. Shift-aware `instantiate_rev` replaces unshifted substitution in the type-walking helpers (fixes fvar leaks in `.brecOn.go` bodies). Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the ref/univ tables (`preseed_expr_tables`) like every production compile path. The serialized constant embeds those tables in sorted order; compiling without the preseed filled them in traversal order instead, permuting every `Ref`/univ index — byte-different but semantically identical constants (decode resolves through the embedded table). This silently failed the Phase-A address comparison against `Named.original.0` for 1529 of 1545 aux constants (including plain stdlib like `Nat.casesOn`); a debug probe proved compile(original) == compile(regen) in every case, i.e. the regeneration itself was always faithful. With the invariant holding corpus-wide, the Phase-A recompile-hash mismatch is now a hard error with no aux exemption, and every roundtrip arm records failures in `aux_gen_errors` (recovery keeps the Lean-facing env populated for diagnosis but is never silent). Pass-2 scope hygiene: the below-def roundtrip loop filters by the original-gated `aux_members` like its sibling loops, so evaporated `below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now dumps hashed component scalars/hashes and runs an original-form recompile probe for any mismatch. Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry recomputation-honest flags so compile-side `validate_ind_flags` no longer poisons the shared tutorial env (73/335 -> 335/335, with the kernel rejecting each bad fixture as designed); validate-aux seeds match module-private fixture names via `privateToUserName?` and enable the Canonicity prefix; Phase 4b gains per-module markers so a fully absent identity group fails loudly when its fixture module is loaded (previously vacuous at 0 pass / 0 fail, now 109 pass). Gates: kernel-check-env 201296/201296; rust-compile all phases with 0 aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the full 213k env (live and deserialized); validate-aux 0 failures at 4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip 143694/0; kernel-tutorial 335/335; cargo test and lake test green.

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`: map_or over map+unwrap_or and slice::contains in surgery.rs, an enumerate loop for the motive-peeling walk in aux_motive_sigs, and let-chain collapses for the inductive-flags fixup loops in decompile.rs and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over from the previous commit.

Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).

Port of the two Rust kernel fixes on this branch: - Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand (computed_is_rec_ind), nested detection is structural (member_has_nested / ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten member-scoped without the declared nested count. Serialization packs one bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive addresses re-pinned. - collectDependencies (Ix/Common.lean) now closes over a declaration's full recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference in rule RHSs) plus each rule ctor's owning external recursor (List.rec). Without these the per-name compile either failed (MissingConstant AuxDedup1.C.rec from A.rec_1's block) or silently skipped the evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2 in original form, which the kernel rejects. AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join kernelCheckEntries; the four evaporated rec_N entries pin the identical 3_073_003 FFT cost (their claims are byte-exact List.rec: lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2). All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

…nment-machine WHNF reducer (#442) * kernel: uid identity, env-machine WHNF, and reduction-loop perf Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%. * kernel: native perf/shard examples (out-of-circuit tooling) Standalone cargo examples over a .ixe env, bypassing the Lean/FFI layer, updated to main's steps-based shard cost model (block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram): - shard_plan: profile → partition → .ixes manifest, with store-aware planning (--store-dir drops work items whose targets the proof store already covers, and excludes covered blocks from the partition hypergraph — a novel→covered edge is an assumption discharged at aggregation, not a cut to minimize); sizes N from machine RAM by default. - perf_check / check_one: native rerun of the guest check_const loop so IX_* perf-counter instrumentation can target a single expensive constant without re-checking its env. - heaviest_block / block_reduce_histo / shard_names / manifest_info: profiling forensics over blocks and manifests. * zisk+sp1: prover batch scripts and logs; bench-compile-init - zisk/scripts: prove-batch (sequential shard proving), mem-guard (MemAvailable watchdog that kills zisk-host before the OOM killer wedges the box), bench-cycles, mergesort-250k repro; reference logs. - sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with WITHOUT_VK_VERIFICATION=1). - Lean side: bench-compile-init lake exe (imports Init, empty main). * zisk: close aggregation soundness gaps (failures word, transitive vk pinning) The aggregate proof was weaker than "these subjects are well-typed": - The agg guest never read a child's committed failures word (slot 10) and hard-committed 0 for its own, so aggregation ERASED the failure bit — a kernel-rejected constant could appear under a failures=0 root, with only host-side courtesy checks in the way. Every child's failures word is now asserted 0 in-circuit. - vk pinning was not transitive: a child that is itself an aggregate was pinned only by its program vk (the shared AGG vk); its own allowed-vk set was never inspected. An agg-of-1 built against a rogue allowed set (wrapping an arbitrary program's "proof" with forged publics) would fold under an honest-looking root. The agg guest now requires every aggregate child (allowed-set index ≥ 1, by the new positional convention: index 0 = leaf vk, the rest agg vks) to commit THIS instance's vks id — the allowed set is uniform down the tree, so the pin is recursive. The convention's ordering is bound by the committed id hash, which external verifiers already check. - The host derived the allowed set FROM the untrusted child proofs (distinct_vks), so any proof admitted its own program, and a stale store folded silently under its old vk. The allowed set is now [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk after ROM setup); freshly produced proofs are asserted to match; stored proofs with a different vk are skipped (re-proven); and the root's committed vks id is checked against — and printed for — external verifiers. - A manifest bisection tree whose leaf set differs from the shard id set silently dropped proven leaves from the fold while the pre-aggregation coverage check (counting proofs PRODUCED, not folded) still passed. ShardManifest::from_bytes now rejects such trees, and the host additionally checks post-fold that every env target is in the root's actual subject set. * ixon: memoize deferred address verification (one hash per constant per load) The bench run on the rebase preview (06e1a1d) showed the whole-env ooc/InitStd row at +63.9% (10.96 s -> 17.97 s) while every per-constant row improved. Cause: LazyConstant::get() re-ran Address::hash(bytes) on every materialization, and the check loop re-ingresses each work item's closure after clear_releasing_memory() (IX_KERNEL_CHECK_CLEAR_EVERY=1), so each constant was re-hashed once per closure it appears in — inside the timed window. Pre-deferral the total was one hash per constant, at load time. Memoize the SUCCESSFUL check per entry (Arc<AtomicBool>, shared by clones, which share the bytes): the first get() still hash-checks before parsing; later get()s skip the hash. Failures are never memoized — bytes are immutable, so a mismatched entry re-fails on every call. This restores the one-hash-per-constant total while keeping load lazy. Also: unit tests for the deferred path (verify-once, failure never memoized, clones share the verdict), drop a dead 'let _ = i;' in get_anon, and note the memoization in docs/kernel_identity.md. * verify: make the pinned trust-frontier statements dischargeable ExecutionRequests' set/modifyGet constructors certified an arbitrary silent state transformation with an empty request list, so any program could be rewritten (funext + of_eq) as modifyGet-of-its-own-run bound into a pure/throw dispatch — ExecutionRequests x s [] held for every program, RunAssumptions was satisfiable with a support covering only the initial intern table, and the module docstring's central claim ("no constructor for an arbitrary silent computation") was false. Independently, the four headline statements universally quantified {semantics : CacheSemantics} — blockErrorsOnly is a lawful instance that invalidates every .expr cache insertion, refuting any run that warms a cache — and demanded the fixed support cover the POST-state intern table, refuting any run that interns. TcM.checkConst.wf was refutable outright; the other three were shielded only by the opaque StatementTrKExpr. set/modifyGet now carry intern-preservation hypotheses at the indexed state, and the new ExecutionRequests.intern_eq_of_nil proves the guarantee machine-checked: a []-certificate forces an unchanged intern table on both outcomes, so requests are an honest upper bound on a run's interning and the support quantifier matches the documented choose-final-support-up-front design. The statements pin an opaque StatementCacheSemantics stub (the K1 machinery is proved only for the whnfCacheSemantics family; arbitrary keys/fallbacks are refutable), so KernelRunInv no longer quantifies over semantics. Statement names and the four-sorry frontier are unchanged; NatFixture's satisfiability witnesses compile verbatim. * tc: mirror the kernel's Nat-offset machinery in the Lean spec The offset work landed Rust-side only, so spec and implementation disagreed on exactly the large-offset inputs it was built for: Rust strips a shared offset in one step, keeps 'Nat.add base (Lit n)' / 'Nat.div|mod base (Lit k)' stuck in compact form, and collapses symbolic-base linear Nat.rec to the compact offset, while Lean still peeled one succ per isDefEqCall level (maxRecDepth at k ≈ 2000, and succ-tower materialization in WHNF beyond 10k) and required a literal base for the linear-rec collapse. Port all three pieces: tryDefEqOffset decomposes both sides via natOffsetDecompose behind an O(1) natOffsetCandidate probe and strips the shared offset in one step (verdict-preserving by definitional +k injectivity); tryNatOffsetStuck freezes compact offset forms before delta at the same decision point as the Rust loop; and tryReduceNatSuccLinearRec gains the symbolic-base branch, gated on the recursor application carrying no post-major arguments. Verify ripple: the natRecLiteralParts totalization equation picks up majorIdx, and NatFixture's full-WHNF step walk certifies the offset-stuck probe returns none on the fixture for any primitive address assignment. Tests pin each piece against regressions: stays-compact under decoy Nat.add/div/mod definitions that delta would expose, the bulk strip at k = 2500 (one-succ peeling exceeds the def-eq depth limit there), div-derived vs add-derived stuck forms staying unequal, and the linear-rec collapse with its post-major conservatism. * tests: drop the tc-node-addr bit-parity harness Uid identity removed per-node content addresses from the Rust kernel, so the oracle dump's ty/extra columns became 16-hex intern uids — process-history-dependent values that can never byte-match the Lean side's Blake3 node addresses. The suite could only fail, and since ignored.yml runs 'lake test -- --ignored' on every push to main, it would turn Extended CI red on merge. The one column still comparable (the constant id) is read from the same serialized env bytes on both sides, so a slimmed comparison would check only traversal enumeration — coverage tc-anon-diff already provides against the real Rust verdicts. Remove the suite, its FFI oracle, and the extern binding; reword the Egress module doc that cited the harness as a level-reduction certifier. * kernel: allocate intern uids in thread-local blocks NEXT_UID was a single process-global cache line hit by a relaxed fetch_add for every node interned by every checker worker. The blake3 identity it replaced was pure per-worker work, so the old kernel scaled linearly with workers; the uid kernel is ~1.4x faster per core but its whole-env throughput plateaued near 5.7K consts/s as worker counts grew — the ooc InitStd !benchmark regression (9.96 s -> 16.97 s on the 32-thread bench runner, while every per-constant row improved; the same binaries tie at 24 local workers and the uid side wins 1.41x at 6). Hand out uids in per-thread blocks of 2^20 reserved from the global counter, touching the shared line once per block instead of once per node. Blocks are never reused (a thread's unspent remainder is abandoned on exit), so uid uniqueness and the never-reuse cache-key guarantee are unchanged; the exhaustion guard aborts a block early instead of one uid early. Local whole-env InitStd at 24 workers drops 15.58 s -> 11.04 s (old kernel: 15.49 s), and 6->24 worker scaling recovers from 1.60x to 2.02x. * bench: record tool faults as crash, not oom A 128+signal death was always recorded as an OOM row, so a zisk mem-planner segfault (exit 139) rendered as OOM and sent the investigation chasing RAM budgets instead of a heap-overflow bug. Split the kill statuses: explicit kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other signal death records status crash and renders as 💥 CRASH in the compare table. * kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2) The profiler counted whnf entries, def-eq entries, and limb-weighted Nat arithmetic per constant but dropped them at block aggregation, and nothing counted term-construction volume at all — leaving the shard cost model only heartbeats, subst, and bytes to predict guest steps from. Persist all four op counters per block (format v2) plus a new intern-table visit counter (a proxy for construction/memory traffic, bumped in intern_expr/intern_univ), and add a shard_features example that emits a per-shard feature CSV from a profile + manifest pair for calibrating the cost model against externally measured shard costs (ziskemu -X on dumped shard inputs). * zisk: dump every selected shard's input; skip ROM setup in dump mode --dump-input wrote only the first selected shard and exited, so dumping a 13-shard plan took 13 host invocations. Dump every selected shard in one run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard keeps the exact path), and skip client.setup when no proof store is involved — dump mode never runs the VM and needs the ROM setup (and thus the proving key) only to derive the shard vk for store filtering. * kernel: calibrate the shard planner in Zisk cost units Replace the heartbeat-based guest-STEP model with one denominated in ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES + BASE), so the packing target prices the axes that don't ride the main trace — DMA/blake3 precompile area and memory ops. Calibration corpus: 118 InitStd shards across 13 constants, each measured with ziskemu -X on inputs dumped via --dump-input. cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq + 28.4k*intern (+ 73.2k per cross-ingress byte) MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per work item, so intra-shard cache sharing is invisible to per-block features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram. On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on the uid-identity kernel; the intern term carries the memory-traffic/DMA axis (residual correlation 0.91 with dma_memcpy counts). Prover models refit on the same corpus. RAM comes from a guarded GPU prove sweep measured as each prover's systemd-scope cgroup memory.peak — the OOM-relevant metric CI's watchdog enforces, charging the whole process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost (was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s measured vs 411s predicted at the largest point). Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards (instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within the actual-cost ceiling; the only violations are the two INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB single-leaf), correctly flagged as not fitting the budget. * bench: per-constant ooc attribution and a compare top-movers drill-down A whole-env ooc regression previously surfaced as one env-keyed number, with drill-down only into the pre-chosen bench vectors. Now the anon whole-env check attributes itself: check-rs --per-const <csv> records one entry per work item (wall nanos, heartbeats, the op counters, and the predicted Zisk cost via the shard model) from the check loop, and the CLI joins Lean names from the env's named table (projection-name fallback for anonymized Muts blocks) so entries survive PRs that shift content addresses. An entry is ONE constant's (or Muts block's) own check — deps are lazily ingressed and trusted, each checked in its own entry, with the consulted closure slice's ingress charged to the entry — so entries sum to the env total with no double counting. NOT the full-closure scope of --consts measurements; documented at the recording site, the flag help, the renderer, and in the rendered output. The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to the results file (rotated with the local baseline), and ix bench compare renders a drill-down when both sides carry one, split by evidence quality — calibrated on a Mathlib A/A run (640K constants, twice through one binary): wall time swings up to 2.8s from scheduling alone, while the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9 absolute; worker->item assignment varies uid blocks and uid-keyed hash iteration order perturbs a few order-sensitive paths; --workers 1 is exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own cost OR >= 1e9 outright, both above the drift envelope) lead the drill-down ranked by percent change, styled like the main table ('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are quarantined in a labeled noise section capped at 5 rows. On the A/A run this renders 0 cost movers, the truthful reading. * bench: verdict-first cell layout; collapse tables past 5 rows A multi-cell !benchmark comment stacked every cell's full table; long cells (a 40-constant zisk table) buried the verdicts. Each cell now leads with its one-line verdict (and any typecheck failures / empty-side warnings, which stay unconditionally visible), and the comparison table collapses into a <details> block when it has more than 5 rows — small cells (the ooc env row, few-constant runs) stay inline. The per-constant and phase drill-downs were already collapsible. * ci: wire the ooc attribution CSV through the !benchmark pipeline bencher.dev stores metric rows only, so the per-constant drill-down needs the attribution CSVs to travel beside the results files. bench-main caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores the base SHA's entry, carries a base-run-produced CSV through the merge step (which previously renamed base.json into main.json and orphaned it), and pairs whichever CSV it has with the PR side's. The main side ends up with exactly two sources: bencher on FULL coverage (plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun for anything less — base SHA not uploaded, partial coverage, an ooc attribution cache miss, or the fresh token. A rerun measures the full default selection (a BENCH_CONSTS override still narrows it) and its rows take priority; bencher-fetched rows only fill rows the rerun failed to produce, and the table's main-source label says which path ran. This retires the gap-filling machinery (--consts from missing.txt, the bencher-priority merge arm) — a full rerun is simpler and self-consistent, at the cost of re-measuring a cell when a PR adds constants. * zisk: drop the vendored guest linker script Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the riscv64ima-zisk-zkvm-elf linker script in the target spec again, and passing the vendored copy on top double-defines the rom/ram memory regions. Both guest build scripts existed only to pass it — remove them and the script; the toolchain's embedded script is the single source of the memory layout. * zisk: pin the fork branch with the mem-planner fill_padding fix Bump every zisk fork pin from blake3-precompile (e4057c4) to blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows the mem-planner offsets array before fill_padding pads the last page — the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the shard that crashed 4/4 on the old pin executes clean on the new one (634M cycles, failures=0), as does the full 13-shard plan on the locally-patched build the fix was developed against. * chore: fix clippy lints (casts, qualifications, poison error, let-chain) u32::try_from over as-truncation and u64::from over as-widening in shard_features; drop redundant std::sync:: qualifications; carry the PoisonError text instead of discarding it; collapse the texray if into a let-chain; contains() over iter().any() in the holed-work filter. * chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build deliberately skips the guest compilation under clippy, but include_elf! still demanded the ELF bytes. Gate the embed (and its import) on cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes under clippy. Also collapse the texray if into a let-chain, matching the zisk host. A real release build of the host still works. * ci: clippy gates for the zisk and sp1 host workspaces The root rust-test clippy never enters the standalone zkVM workspaces, so their warnings accumulated ungated. Add cargo clippy --release --all-targets -D warnings to both host jobs, after the build so the release dep artifacts are shared (and, for zisk, the guest ELFs its build scripts already produced). * chore: String.dropEnd over deprecated String.dropRight * Unpin ziskup install * ci: align install-zisk comments with the unpinned toolchain * Clean up dev tooling and experiment artifacts for PR - Untrack sp1/zisk benchmark logs and scripts - Remove dev-tooling examples from ix-kernel: examples are for showing users how to use the crate; the shard-planning and perf binaries live on in git history - Remove the env-machine design doc; the as-built machine is documented at the code (whnf.rs machine_whnf, subst.rs Clo) --------- Co-authored-by: John C. Burnham <john@agathic.com>

johnchandlerburnham · 2026-07-04T06:34:29Z

Summary

Two related changes to the content-addressing layer and its aux-constant handling, fixing underlying issue reported in #465

1. Ixon no longer stores recr/refl/nested on Inductive. These are derivable
from constructor structure, so storing them was redundant and trusting declared values
was an adversarial surface (e.g. is_rec = false on a recursive inductive enables
improper struct-eta). The kernel now computes is_rec on demand, memoized in a new env
cache with a provisional entry to break the whnf → try_struct_eta_iota → is_struct_like
cycle; this replaces the declared-vs-computed check in check_inductive. The compile
side gains compute_lean_ind_flags to recompute Lean's block-wide
isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a
source Lean env (kernel egress, decompile), and validate_lean_ind_flags to check a
whole env against the recomputation.

2. Evaporated auxiliaries get a canonical form. When SCC splitting strands a nested
aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and
dropping the irrelevant over-merged motives leaves exactly the external inductive's
generic recursor. Canonical treatment: rec_N claims alias <Ext>.rec (e.g.
List.rec), call sites are rebuilt onto the external telescope via head-rewrite
CallSitePlans (owner-gated, single-motive targets), and below_N/brecOn_N compile as
surgered originals like _sizeOf_N. Fixes the AuxDedup kernel-check failures (28 → 0);
AuxDedup1 now generates auxiliaries identical to AuxDedup2's canonical structure.
Documented in docs/ix_canonicity.md §6.5.

Byte-exact aux roundtrip

roundtrip_block Phase A (recompile the regenerated Lean form, compare against the
stored original address) silently failed for 1529 of 1545 aux constants — including
plain stdlib like Nat.casesOn. Root cause: every production compile path preseeds the
ref/univ tables in sorted order (preseed_expr_tables) before compiling, and the
serialized constant embeds those tables; Phase A compiled without the preseed, filling
the tables in traversal order instead — every Ref/univ index permuted, byte-different
but semantically identical constants (decode resolves through the embedded table). A
debug probe recompiling the Lean original through the identical path proved
compile(original) == compile(regen) in every case: regeneration was always faithful,
the comparison context was not.

With the preseed mirrored in Phase A the invariant holds corpus-wide, so a Phase-A
recompile-hash mismatch is now a hard error with no aux exemption, and every
roundtrip arm records failures in aux_gen_errors (recovery keeps the Lean-facing env
populated for diagnosis but is never silent). Related hardening: call-site surgery
detection is durable across serialization (Named.original.is_some() alongside the
in-memory map), shift-aware instantiate_rev in the type-walking helpers (fixes fvar
leaks in .brecOn.go bodies), and the below-def roundtrip loop filters by the
original-gated members like its sibling loops. IX_ROUNDTRIP_DEBUG now dumps hashed
component summaries and runs an original-form recompile probe on any mismatch.

Test fixes and fixtures

kernel-tutorial: bad_raw_consts inductive fixtures carry recomputation-honest flags
so the whole-env validate_ind_flags no longer poisons the shared tutorial env
(73/335 → 335/335, with the kernel rejecting each bad fixture as designed).
validate-aux: seeds match module-private fixture names via privateToUserName?, the
Canonicity prefix is enabled, and Phase 4b gains per-module markers so a fully absent
identity group fails loudly when its fixture module is loaded (previously vacuous at
0 pass / 0 fail, now 109 pass / 0 fail).
New fixtures: AuxDedup1/AuxDedup2 (cross-block aux dedup), AuxDedupMixed (a perm
mixing a canonical slot and PERM_OUT_OF_SCC for the same owner), plus a
CompileMutualFixtures benchmark lib.

Gates

kernel-check-env: 201296/201296
rust-compile: all phases, 0 aux_gen errors / 0 mismatches / 0 Phase-A address
divergences on the full 213k env (live and deserialized)
validate-aux: 0 failures at 4393-constant scope
rust-serialize: byte-exact; kernel-ixon-roundtrip: 143694/0
kernel-tutorial: 335/335; cargo test workspace and lake test green;
cargo clippy --all-targets clean
lake exe ix check-rs compilemathlib.ixe: 736618/736618 passed, 0 failed (325.3s)
lake exe ix validate Benchmarks/Compile/CompileMathlib.lean: 0 failures (1528.33s total)

Remove the `recr`/`refl` bools and the `nested` count from the Ixon `Inductive` constant and its serialization (Rust and Lean), and from the `Indc` reveal-proof variant, renumbering the field-presence mask bits. These flags are derivable from constructor structure, so storing them was redundant and trusting declared values was an adversarial surface (e.g. is_rec = false on a recursive inductive enables improper struct-eta). - kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now computed on demand (computed_is_rec), memoized in the new env is_rec_cache with a provisional entry to break the whnf -> try_struct_eta_iota -> is_struct_like cycle. This replaces the declared-vs-computed H1 verification in check_inductive. - compile: new compute_lean_ind_flags recomputes Lean's block-wide isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a source Lean env (kernel egress, decompile), since Ixon no longer stores the flags; validate_lean_ind_flags checks a whole env against the recomputation. - tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising aux-constant dedup across blocks (fix forthcoming); add a CompileMutualFixtures benchmark lib building the mutual test fixtures; ignore *.ixe.

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a nested aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and dropping the irrelevant over-merged motives leaves exactly the external inductive's generic recursor. Canonical treatment: `rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are rebuilt onto the external telescope via head-rewrite CallSitePlans (owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner. Documented in docs/ix_canonicity.md 6.5. Call-site surgery guard is now durable across serialization: aux-regen detection accepts `Named.original.is_some()` in addition to the in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles no longer misapply surgery. Shift-aware `instantiate_rev` replaces unshifted substitution in the type-walking helpers (fixes fvar leaks in `.brecOn.go` bodies). Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the ref/univ tables (`preseed_expr_tables`) like every production compile path. The serialized constant embeds those tables in sorted order; compiling without the preseed filled them in traversal order instead, permuting every `Ref`/univ index — byte-different but semantically identical constants (decode resolves through the embedded table). This silently failed the Phase-A address comparison against `Named.original.0` for 1529 of 1545 aux constants (including plain stdlib like `Nat.casesOn`); a debug probe proved compile(original) == compile(regen) in every case, i.e. the regeneration itself was always faithful. With the invariant holding corpus-wide, the Phase-A recompile-hash mismatch is now a hard error with no aux exemption, and every roundtrip arm records failures in `aux_gen_errors` (recovery keeps the Lean-facing env populated for diagnosis but is never silent). Pass-2 scope hygiene: the below-def roundtrip loop filters by the original-gated `aux_members` like its sibling loops, so evaporated `below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now dumps hashed component scalars/hashes and runs an original-form recompile probe for any mismatch. Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry recomputation-honest flags so compile-side `validate_ind_flags` no longer poisons the shared tutorial env (73/335 -> 335/335, with the kernel rejecting each bad fixture as designed); validate-aux seeds match module-private fixture names via `privateToUserName?` and enable the Canonicity prefix; Phase 4b gains per-module markers so a fully absent identity group fails loudly when its fixture module is loaded (previously vacuous at 0 pass / 0 fail, now 109 pass). Gates: kernel-check-env 201296/201296; rust-compile all phases with 0 aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the full 213k env (live and deserialized); validate-aux 0 failures at 4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip 143694/0; kernel-tutorial 335/335; cargo test and lake test green.

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`: map_or over map+unwrap_or and slice::contains in surgery.rs, an enumerate loop for the motive-peeling walk in aux_motive_sigs, and let-chain collapses for the inductive-flags fixup loops in decompile.rs and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over from the previous commit.

Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).

Port of the two Rust kernel fixes on this branch: - Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand (computed_is_rec_ind), nested detection is structural (member_has_nested / ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten member-scoped without the declared nested count. Serialization packs one bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive addresses re-pinned. - collectDependencies (Ix/Common.lean) now closes over a declaration's full recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference in rule RHSs) plus each rule ctor's owning external recursor (List.rec). Without these the per-name compile either failed (MissingConstant AuxDedup1.C.rec from A.rec_1's block) or silently skipped the evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2 in original form, which the kernel rejects. AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join kernelCheckEntries; the four evaporated rec_N entries pin the identical 3_073_003 FFT cost (their claims are byte-exact List.rec: lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2). All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

…nment-machine WHNF reducer (#442) * kernel: uid identity, env-machine WHNF, and reduction-loop perf Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%. * kernel: native perf/shard examples (out-of-circuit tooling) Standalone cargo examples over a .ixe env, bypassing the Lean/FFI layer, updated to main's steps-based shard cost model (block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram): - shard_plan: profile → partition → .ixes manifest, with store-aware planning (--store-dir drops work items whose targets the proof store already covers, and excludes covered blocks from the partition hypergraph — a novel→covered edge is an assumption discharged at aggregation, not a cut to minimize); sizes N from machine RAM by default. - perf_check / check_one: native rerun of the guest check_const loop so IX_* perf-counter instrumentation can target a single expensive constant without re-checking its env. - heaviest_block / block_reduce_histo / shard_names / manifest_info: profiling forensics over blocks and manifests. * zisk+sp1: prover batch scripts and logs; bench-compile-init - zisk/scripts: prove-batch (sequential shard proving), mem-guard (MemAvailable watchdog that kills zisk-host before the OOM killer wedges the box), bench-cycles, mergesort-250k repro; reference logs. - sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with WITHOUT_VK_VERIFICATION=1). - Lean side: bench-compile-init lake exe (imports Init, empty main). * zisk: close aggregation soundness gaps (failures word, transitive vk pinning) The aggregate proof was weaker than "these subjects are well-typed": - The agg guest never read a child's committed failures word (slot 10) and hard-committed 0 for its own, so aggregation ERASED the failure bit — a kernel-rejected constant could appear under a failures=0 root, with only host-side courtesy checks in the way. Every child's failures word is now asserted 0 in-circuit. - vk pinning was not transitive: a child that is itself an aggregate was pinned only by its program vk (the shared AGG vk); its own allowed-vk set was never inspected. An agg-of-1 built against a rogue allowed set (wrapping an arbitrary program's "proof" with forged publics) would fold under an honest-looking root. The agg guest now requires every aggregate child (allowed-set index ≥ 1, by the new positional convention: index 0 = leaf vk, the rest agg vks) to commit THIS instance's vks id — the allowed set is uniform down the tree, so the pin is recursive. The convention's ordering is bound by the committed id hash, which external verifiers already check. - The host derived the allowed set FROM the untrusted child proofs (distinct_vks), so any proof admitted its own program, and a stale store folded silently under its old vk. The allowed set is now [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk after ROM setup); freshly produced proofs are asserted to match; stored proofs with a different vk are skipped (re-proven); and the root's committed vks id is checked against — and printed for — external verifiers. - A manifest bisection tree whose leaf set differs from the shard id set silently dropped proven leaves from the fold while the pre-aggregation coverage check (counting proofs PRODUCED, not folded) still passed. ShardManifest::from_bytes now rejects such trees, and the host additionally checks post-fold that every env target is in the root's actual subject set. * ixon: memoize deferred address verification (one hash per constant per load) The bench run on the rebase preview (06e1a1d) showed the whole-env ooc/InitStd row at +63.9% (10.96 s -> 17.97 s) while every per-constant row improved. Cause: LazyConstant::get() re-ran Address::hash(bytes) on every materialization, and the check loop re-ingresses each work item's closure after clear_releasing_memory() (IX_KERNEL_CHECK_CLEAR_EVERY=1), so each constant was re-hashed once per closure it appears in — inside the timed window. Pre-deferral the total was one hash per constant, at load time. Memoize the SUCCESSFUL check per entry (Arc<AtomicBool>, shared by clones, which share the bytes): the first get() still hash-checks before parsing; later get()s skip the hash. Failures are never memoized — bytes are immutable, so a mismatched entry re-fails on every call. This restores the one-hash-per-constant total while keeping load lazy. Also: unit tests for the deferred path (verify-once, failure never memoized, clones share the verdict), drop a dead 'let _ = i;' in get_anon, and note the memoization in docs/kernel_identity.md. * verify: make the pinned trust-frontier statements dischargeable ExecutionRequests' set/modifyGet constructors certified an arbitrary silent state transformation with an empty request list, so any program could be rewritten (funext + of_eq) as modifyGet-of-its-own-run bound into a pure/throw dispatch — ExecutionRequests x s [] held for every program, RunAssumptions was satisfiable with a support covering only the initial intern table, and the module docstring's central claim ("no constructor for an arbitrary silent computation") was false. Independently, the four headline statements universally quantified {semantics : CacheSemantics} — blockErrorsOnly is a lawful instance that invalidates every .expr cache insertion, refuting any run that warms a cache — and demanded the fixed support cover the POST-state intern table, refuting any run that interns. TcM.checkConst.wf was refutable outright; the other three were shielded only by the opaque StatementTrKExpr. set/modifyGet now carry intern-preservation hypotheses at the indexed state, and the new ExecutionRequests.intern_eq_of_nil proves the guarantee machine-checked: a []-certificate forces an unchanged intern table on both outcomes, so requests are an honest upper bound on a run's interning and the support quantifier matches the documented choose-final-support-up-front design. The statements pin an opaque StatementCacheSemantics stub (the K1 machinery is proved only for the whnfCacheSemantics family; arbitrary keys/fallbacks are refutable), so KernelRunInv no longer quantifies over semantics. Statement names and the four-sorry frontier are unchanged; NatFixture's satisfiability witnesses compile verbatim. * tc: mirror the kernel's Nat-offset machinery in the Lean spec The offset work landed Rust-side only, so spec and implementation disagreed on exactly the large-offset inputs it was built for: Rust strips a shared offset in one step, keeps 'Nat.add base (Lit n)' / 'Nat.div|mod base (Lit k)' stuck in compact form, and collapses symbolic-base linear Nat.rec to the compact offset, while Lean still peeled one succ per isDefEqCall level (maxRecDepth at k ≈ 2000, and succ-tower materialization in WHNF beyond 10k) and required a literal base for the linear-rec collapse. Port all three pieces: tryDefEqOffset decomposes both sides via natOffsetDecompose behind an O(1) natOffsetCandidate probe and strips the shared offset in one step (verdict-preserving by definitional +k injectivity); tryNatOffsetStuck freezes compact offset forms before delta at the same decision point as the Rust loop; and tryReduceNatSuccLinearRec gains the symbolic-base branch, gated on the recursor application carrying no post-major arguments. Verify ripple: the natRecLiteralParts totalization equation picks up majorIdx, and NatFixture's full-WHNF step walk certifies the offset-stuck probe returns none on the fixture for any primitive address assignment. Tests pin each piece against regressions: stays-compact under decoy Nat.add/div/mod definitions that delta would expose, the bulk strip at k = 2500 (one-succ peeling exceeds the def-eq depth limit there), div-derived vs add-derived stuck forms staying unequal, and the linear-rec collapse with its post-major conservatism. * tests: drop the tc-node-addr bit-parity harness Uid identity removed per-node content addresses from the Rust kernel, so the oracle dump's ty/extra columns became 16-hex intern uids — process-history-dependent values that can never byte-match the Lean side's Blake3 node addresses. The suite could only fail, and since ignored.yml runs 'lake test -- --ignored' on every push to main, it would turn Extended CI red on merge. The one column still comparable (the constant id) is read from the same serialized env bytes on both sides, so a slimmed comparison would check only traversal enumeration — coverage tc-anon-diff already provides against the real Rust verdicts. Remove the suite, its FFI oracle, and the extern binding; reword the Egress module doc that cited the harness as a level-reduction certifier. * kernel: allocate intern uids in thread-local blocks NEXT_UID was a single process-global cache line hit by a relaxed fetch_add for every node interned by every checker worker. The blake3 identity it replaced was pure per-worker work, so the old kernel scaled linearly with workers; the uid kernel is ~1.4x faster per core but its whole-env throughput plateaued near 5.7K consts/s as worker counts grew — the ooc InitStd !benchmark regression (9.96 s -> 16.97 s on the 32-thread bench runner, while every per-constant row improved; the same binaries tie at 24 local workers and the uid side wins 1.41x at 6). Hand out uids in per-thread blocks of 2^20 reserved from the global counter, touching the shared line once per block instead of once per node. Blocks are never reused (a thread's unspent remainder is abandoned on exit), so uid uniqueness and the never-reuse cache-key guarantee are unchanged; the exhaustion guard aborts a block early instead of one uid early. Local whole-env InitStd at 24 workers drops 15.58 s -> 11.04 s (old kernel: 15.49 s), and 6->24 worker scaling recovers from 1.60x to 2.02x. * bench: record tool faults as crash, not oom A 128+signal death was always recorded as an OOM row, so a zisk mem-planner segfault (exit 139) rendered as OOM and sent the investigation chasing RAM budgets instead of a heap-overflow bug. Split the kill statuses: explicit kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other signal death records status crash and renders as 💥 CRASH in the compare table. * kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2) The profiler counted whnf entries, def-eq entries, and limb-weighted Nat arithmetic per constant but dropped them at block aggregation, and nothing counted term-construction volume at all — leaving the shard cost model only heartbeats, subst, and bytes to predict guest steps from. Persist all four op counters per block (format v2) plus a new intern-table visit counter (a proxy for construction/memory traffic, bumped in intern_expr/intern_univ), and add a shard_features example that emits a per-shard feature CSV from a profile + manifest pair for calibrating the cost model against externally measured shard costs (ziskemu -X on dumped shard inputs). * zisk: dump every selected shard's input; skip ROM setup in dump mode --dump-input wrote only the first selected shard and exited, so dumping a 13-shard plan took 13 host invocations. Dump every selected shard in one run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard keeps the exact path), and skip client.setup when no proof store is involved — dump mode never runs the VM and needs the ROM setup (and thus the proving key) only to derive the shard vk for store filtering. * kernel: calibrate the shard planner in Zisk cost units Replace the heartbeat-based guest-STEP model with one denominated in ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES + BASE), so the packing target prices the axes that don't ride the main trace — DMA/blake3 precompile area and memory ops. Calibration corpus: 118 InitStd shards across 13 constants, each measured with ziskemu -X on inputs dumped via --dump-input. cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq + 28.4k*intern (+ 73.2k per cross-ingress byte) MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per work item, so intra-shard cache sharing is invisible to per-block features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram. On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on the uid-identity kernel; the intern term carries the memory-traffic/DMA axis (residual correlation 0.91 with dma_memcpy counts). Prover models refit on the same corpus. RAM comes from a guarded GPU prove sweep measured as each prover's systemd-scope cgroup memory.peak — the OOM-relevant metric CI's watchdog enforces, charging the whole process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost (was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s measured vs 411s predicted at the largest point). Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards (instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within the actual-cost ceiling; the only violations are the two INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB single-leaf), correctly flagged as not fitting the budget. * bench: per-constant ooc attribution and a compare top-movers drill-down A whole-env ooc regression previously surfaced as one env-keyed number, with drill-down only into the pre-chosen bench vectors. Now the anon whole-env check attributes itself: check-rs --per-const <csv> records one entry per work item (wall nanos, heartbeats, the op counters, and the predicted Zisk cost via the shard model) from the check loop, and the CLI joins Lean names from the env's named table (projection-name fallback for anonymized Muts blocks) so entries survive PRs that shift content addresses. An entry is ONE constant's (or Muts block's) own check — deps are lazily ingressed and trusted, each checked in its own entry, with the consulted closure slice's ingress charged to the entry — so entries sum to the env total with no double counting. NOT the full-closure scope of --consts measurements; documented at the recording site, the flag help, the renderer, and in the rendered output. The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to the results file (rotated with the local baseline), and ix bench compare renders a drill-down when both sides carry one, split by evidence quality — calibrated on a Mathlib A/A run (640K constants, twice through one binary): wall time swings up to 2.8s from scheduling alone, while the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9 absolute; worker->item assignment varies uid blocks and uid-keyed hash iteration order perturbs a few order-sensitive paths; --workers 1 is exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own cost OR >= 1e9 outright, both above the drift envelope) lead the drill-down ranked by percent change, styled like the main table ('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are quarantined in a labeled noise section capped at 5 rows. On the A/A run this renders 0 cost movers, the truthful reading. * bench: verdict-first cell layout; collapse tables past 5 rows A multi-cell !benchmark comment stacked every cell's full table; long cells (a 40-constant zisk table) buried the verdicts. Each cell now leads with its one-line verdict (and any typecheck failures / empty-side warnings, which stay unconditionally visible), and the comparison table collapses into a <details> block when it has more than 5 rows — small cells (the ooc env row, few-constant runs) stay inline. The per-constant and phase drill-downs were already collapsible. * ci: wire the ooc attribution CSV through the !benchmark pipeline bencher.dev stores metric rows only, so the per-constant drill-down needs the attribution CSVs to travel beside the results files. bench-main caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores the base SHA's entry, carries a base-run-produced CSV through the merge step (which previously renamed base.json into main.json and orphaned it), and pairs whichever CSV it has with the PR side's. The main side ends up with exactly two sources: bencher on FULL coverage (plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun for anything less — base SHA not uploaded, partial coverage, an ooc attribution cache miss, or the fresh token. A rerun measures the full default selection (a BENCH_CONSTS override still narrows it) and its rows take priority; bencher-fetched rows only fill rows the rerun failed to produce, and the table's main-source label says which path ran. This retires the gap-filling machinery (--consts from missing.txt, the bencher-priority merge arm) — a full rerun is simpler and self-consistent, at the cost of re-measuring a cell when a PR adds constants. * zisk: drop the vendored guest linker script Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the riscv64ima-zisk-zkvm-elf linker script in the target spec again, and passing the vendored copy on top double-defines the rom/ram memory regions. Both guest build scripts existed only to pass it — remove them and the script; the toolchain's embedded script is the single source of the memory layout. * zisk: pin the fork branch with the mem-planner fill_padding fix Bump every zisk fork pin from blake3-precompile (e4057c4) to blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows the mem-planner offsets array before fill_padding pads the last page — the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the shard that crashed 4/4 on the old pin executes clean on the new one (634M cycles, failures=0), as does the full 13-shard plan on the locally-patched build the fix was developed against. * chore: fix clippy lints (casts, qualifications, poison error, let-chain) u32::try_from over as-truncation and u64::from over as-widening in shard_features; drop redundant std::sync:: qualifications; carry the PoisonError text instead of discarding it; collapse the texray if into a let-chain; contains() over iter().any() in the holed-work filter. * chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build deliberately skips the guest compilation under clippy, but include_elf! still demanded the ELF bytes. Gate the embed (and its import) on cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes under clippy. Also collapse the texray if into a let-chain, matching the zisk host. A real release build of the host still works. * ci: clippy gates for the zisk and sp1 host workspaces The root rust-test clippy never enters the standalone zkVM workspaces, so their warnings accumulated ungated. Add cargo clippy --release --all-targets -D warnings to both host jobs, after the build so the release dep artifacts are shared (and, for zisk, the guest ELFs its build scripts already produced). * chore: String.dropEnd over deprecated String.dropRight * Unpin ziskup install * ci: align install-zisk comments with the unpinned toolchain * Clean up dev tooling and experiment artifacts for PR - Untrack sp1/zisk benchmark logs and scripts - Remove dev-tooling examples from ix-kernel: examples are for showing users how to use the crate; the shard-planning and perf binaries live on in git history - Remove the env-machine design doc; the as-built machine is documented at the code (whnf.rs machine_whnf, subst.rs Clo) --------- Co-authored-by: John C. Burnham <john@agathic.com>

johnchandlerburnham · 2026-07-04T06:34:29Z

Summary

Two related changes to the content-addressing layer and its aux-constant handling, fixing underlying issue reported in #465

1. Ixon no longer stores recr/refl/nested on Inductive. These are derivable
from constructor structure, so storing them was redundant and trusting declared values
was an adversarial surface (e.g. is_rec = false on a recursive inductive enables
improper struct-eta). The kernel now computes is_rec on demand, memoized in a new env
cache with a provisional entry to break the whnf → try_struct_eta_iota → is_struct_like
cycle; this replaces the declared-vs-computed check in check_inductive. The compile
side gains compute_lean_ind_flags to recompute Lean's block-wide
isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a
source Lean env (kernel egress, decompile), and validate_lean_ind_flags to check a
whole env against the recomputation.

2. Evaporated auxiliaries get a canonical form. When SCC splitting strands a nested
aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and
dropping the irrelevant over-merged motives leaves exactly the external inductive's
generic recursor. Canonical treatment: rec_N claims alias <Ext>.rec (e.g.
List.rec), call sites are rebuilt onto the external telescope via head-rewrite
CallSitePlans (owner-gated, single-motive targets), and below_N/brecOn_N compile as
surgered originals like _sizeOf_N. Fixes the AuxDedup kernel-check failures (28 → 0);
AuxDedup1 now generates auxiliaries identical to AuxDedup2's canonical structure.
Documented in docs/ix_canonicity.md §6.5.

Byte-exact aux roundtrip

roundtrip_block Phase A (recompile the regenerated Lean form, compare against the
stored original address) silently failed for 1529 of 1545 aux constants — including
plain stdlib like Nat.casesOn. Root cause: every production compile path preseeds the
ref/univ tables in sorted order (preseed_expr_tables) before compiling, and the
serialized constant embeds those tables; Phase A compiled without the preseed, filling
the tables in traversal order instead — every Ref/univ index permuted, byte-different
but semantically identical constants (decode resolves through the embedded table). A
debug probe recompiling the Lean original through the identical path proved
compile(original) == compile(regen) in every case: regeneration was always faithful,
the comparison context was not.

With the preseed mirrored in Phase A the invariant holds corpus-wide, so a Phase-A
recompile-hash mismatch is now a hard error with no aux exemption, and every
roundtrip arm records failures in aux_gen_errors (recovery keeps the Lean-facing env
populated for diagnosis but is never silent). Related hardening: call-site surgery
detection is durable across serialization (Named.original.is_some() alongside the
in-memory map), shift-aware instantiate_rev in the type-walking helpers (fixes fvar
leaks in .brecOn.go bodies), and the below-def roundtrip loop filters by the
original-gated members like its sibling loops. IX_ROUNDTRIP_DEBUG now dumps hashed
component summaries and runs an original-form recompile probe on any mismatch.

Test fixes and fixtures

kernel-tutorial: bad_raw_consts inductive fixtures carry recomputation-honest flags
so the whole-env validate_ind_flags no longer poisons the shared tutorial env
(73/335 → 335/335, with the kernel rejecting each bad fixture as designed).
validate-aux: seeds match module-private fixture names via privateToUserName?, the
Canonicity prefix is enabled, and Phase 4b gains per-module markers so a fully absent
identity group fails loudly when its fixture module is loaded (previously vacuous at
0 pass / 0 fail, now 109 pass / 0 fail).
New fixtures: AuxDedup1/AuxDedup2 (cross-block aux dedup), AuxDedupMixed (a perm
mixing a canonical slot and PERM_OUT_OF_SCC for the same owner), plus a
CompileMutualFixtures benchmark lib.

Gates

kernel-check-env: 201296/201296
rust-compile: all phases, 0 aux_gen errors / 0 mismatches / 0 Phase-A address
divergences on the full 213k env (live and deserialized)
validate-aux: 0 failures at 4393-constant scope
rust-serialize: byte-exact; kernel-ixon-roundtrip: 143694/0
kernel-tutorial: 335/335; cargo test workspace and lake test green;
cargo clippy --all-targets clean
lake exe ix check-rs compilemathlib.ixe: 736618/736618 passed, 0 failed (325.3s)
lake exe ix validate Benchmarks/Compile/CompileMathlib.lean: 0 failures (1528.33s total)

Remove the `recr`/`refl` bools and the `nested` count from the Ixon `Inductive` constant and its serialization (Rust and Lean), and from the `Indc` reveal-proof variant, renumbering the field-presence mask bits. These flags are derivable from constructor structure, so storing them was redundant and trusting declared values was an adversarial surface (e.g. is_rec = false on a recursive inductive enables improper struct-eta). - kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now computed on demand (computed_is_rec), memoized in the new env is_rec_cache with a provisional entry to break the whnf -> try_struct_eta_iota -> is_struct_like cycle. This replaces the declared-vs-computed H1 verification in check_inductive. - compile: new compute_lean_ind_flags recomputes Lean's block-wide isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a source Lean env (kernel egress, decompile), since Ixon no longer stores the flags; validate_lean_ind_flags checks a whole env against the recomputation. - tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising aux-constant dedup across blocks (fix forthcoming); add a CompileMutualFixtures benchmark lib building the mutual test fixtures; ignore *.ixe.

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a nested aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and dropping the irrelevant over-merged motives leaves exactly the external inductive's generic recursor. Canonical treatment: `rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are rebuilt onto the external telescope via head-rewrite CallSitePlans (owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner. Documented in docs/ix_canonicity.md 6.5. Call-site surgery guard is now durable across serialization: aux-regen detection accepts `Named.original.is_some()` in addition to the in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles no longer misapply surgery. Shift-aware `instantiate_rev` replaces unshifted substitution in the type-walking helpers (fixes fvar leaks in `.brecOn.go` bodies). Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the ref/univ tables (`preseed_expr_tables`) like every production compile path. The serialized constant embeds those tables in sorted order; compiling without the preseed filled them in traversal order instead, permuting every `Ref`/univ index — byte-different but semantically identical constants (decode resolves through the embedded table). This silently failed the Phase-A address comparison against `Named.original.0` for 1529 of 1545 aux constants (including plain stdlib like `Nat.casesOn`); a debug probe proved compile(original) == compile(regen) in every case, i.e. the regeneration itself was always faithful. With the invariant holding corpus-wide, the Phase-A recompile-hash mismatch is now a hard error with no aux exemption, and every roundtrip arm records failures in `aux_gen_errors` (recovery keeps the Lean-facing env populated for diagnosis but is never silent). Pass-2 scope hygiene: the below-def roundtrip loop filters by the original-gated `aux_members` like its sibling loops, so evaporated `below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now dumps hashed component scalars/hashes and runs an original-form recompile probe for any mismatch. Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry recomputation-honest flags so compile-side `validate_ind_flags` no longer poisons the shared tutorial env (73/335 -> 335/335, with the kernel rejecting each bad fixture as designed); validate-aux seeds match module-private fixture names via `privateToUserName?` and enable the Canonicity prefix; Phase 4b gains per-module markers so a fully absent identity group fails loudly when its fixture module is loaded (previously vacuous at 0 pass / 0 fail, now 109 pass). Gates: kernel-check-env 201296/201296; rust-compile all phases with 0 aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the full 213k env (live and deserialized); validate-aux 0 failures at 4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip 143694/0; kernel-tutorial 335/335; cargo test and lake test green.

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`: map_or over map+unwrap_or and slice::contains in surgery.rs, an enumerate loop for the motive-peeling walk in aux_motive_sigs, and let-chain collapses for the inductive-flags fixup loops in decompile.rs and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over from the previous commit.

Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).

Port of the two Rust kernel fixes on this branch: - Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand (computed_is_rec_ind), nested detection is structural (member_has_nested / ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten member-scoped without the declared nested count. Serialization packs one bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive addresses re-pinned. - collectDependencies (Ix/Common.lean) now closes over a declaration's full recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference in rule RHSs) plus each rule ctor's owning external recursor (List.rec). Without these the per-name compile either failed (MissingConstant AuxDedup1.C.rec from A.rec_1's block) or silently skipped the evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2 in original form, which the kernel rejects. AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join kernelCheckEntries; the four evaporated rec_N entries pin the identical 3_073_003 FFT cost (their claims are byte-exact List.rec: lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2). All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

…nment-machine WHNF reducer (#442) * kernel: uid identity, env-machine WHNF, and reduction-loop perf Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%. * kernel: native perf/shard examples (out-of-circuit tooling) Standalone cargo examples over a .ixe env, bypassing the Lean/FFI layer, updated to main's steps-based shard cost model (block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram): - shard_plan: profile → partition → .ixes manifest, with store-aware planning (--store-dir drops work items whose targets the proof store already covers, and excludes covered blocks from the partition hypergraph — a novel→covered edge is an assumption discharged at aggregation, not a cut to minimize); sizes N from machine RAM by default. - perf_check / check_one: native rerun of the guest check_const loop so IX_* perf-counter instrumentation can target a single expensive constant without re-checking its env. - heaviest_block / block_reduce_histo / shard_names / manifest_info: profiling forensics over blocks and manifests. * zisk+sp1: prover batch scripts and logs; bench-compile-init - zisk/scripts: prove-batch (sequential shard proving), mem-guard (MemAvailable watchdog that kills zisk-host before the OOM killer wedges the box), bench-cycles, mergesort-250k repro; reference logs. - sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with WITHOUT_VK_VERIFICATION=1). - Lean side: bench-compile-init lake exe (imports Init, empty main). * zisk: close aggregation soundness gaps (failures word, transitive vk pinning) The aggregate proof was weaker than "these subjects are well-typed": - The agg guest never read a child's committed failures word (slot 10) and hard-committed 0 for its own, so aggregation ERASED the failure bit — a kernel-rejected constant could appear under a failures=0 root, with only host-side courtesy checks in the way. Every child's failures word is now asserted 0 in-circuit. - vk pinning was not transitive: a child that is itself an aggregate was pinned only by its program vk (the shared AGG vk); its own allowed-vk set was never inspected. An agg-of-1 built against a rogue allowed set (wrapping an arbitrary program's "proof" with forged publics) would fold under an honest-looking root. The agg guest now requires every aggregate child (allowed-set index ≥ 1, by the new positional convention: index 0 = leaf vk, the rest agg vks) to commit THIS instance's vks id — the allowed set is uniform down the tree, so the pin is recursive. The convention's ordering is bound by the committed id hash, which external verifiers already check. - The host derived the allowed set FROM the untrusted child proofs (distinct_vks), so any proof admitted its own program, and a stale store folded silently under its old vk. The allowed set is now [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk after ROM setup); freshly produced proofs are asserted to match; stored proofs with a different vk are skipped (re-proven); and the root's committed vks id is checked against — and printed for — external verifiers. - A manifest bisection tree whose leaf set differs from the shard id set silently dropped proven leaves from the fold while the pre-aggregation coverage check (counting proofs PRODUCED, not folded) still passed. ShardManifest::from_bytes now rejects such trees, and the host additionally checks post-fold that every env target is in the root's actual subject set. * ixon: memoize deferred address verification (one hash per constant per load) The bench run on the rebase preview (06e1a1d) showed the whole-env ooc/InitStd row at +63.9% (10.96 s -> 17.97 s) while every per-constant row improved. Cause: LazyConstant::get() re-ran Address::hash(bytes) on every materialization, and the check loop re-ingresses each work item's closure after clear_releasing_memory() (IX_KERNEL_CHECK_CLEAR_EVERY=1), so each constant was re-hashed once per closure it appears in — inside the timed window. Pre-deferral the total was one hash per constant, at load time. Memoize the SUCCESSFUL check per entry (Arc<AtomicBool>, shared by clones, which share the bytes): the first get() still hash-checks before parsing; later get()s skip the hash. Failures are never memoized — bytes are immutable, so a mismatched entry re-fails on every call. This restores the one-hash-per-constant total while keeping load lazy. Also: unit tests for the deferred path (verify-once, failure never memoized, clones share the verdict), drop a dead 'let _ = i;' in get_anon, and note the memoization in docs/kernel_identity.md. * verify: make the pinned trust-frontier statements dischargeable ExecutionRequests' set/modifyGet constructors certified an arbitrary silent state transformation with an empty request list, so any program could be rewritten (funext + of_eq) as modifyGet-of-its-own-run bound into a pure/throw dispatch — ExecutionRequests x s [] held for every program, RunAssumptions was satisfiable with a support covering only the initial intern table, and the module docstring's central claim ("no constructor for an arbitrary silent computation") was false. Independently, the four headline statements universally quantified {semantics : CacheSemantics} — blockErrorsOnly is a lawful instance that invalidates every .expr cache insertion, refuting any run that warms a cache — and demanded the fixed support cover the POST-state intern table, refuting any run that interns. TcM.checkConst.wf was refutable outright; the other three were shielded only by the opaque StatementTrKExpr. set/modifyGet now carry intern-preservation hypotheses at the indexed state, and the new ExecutionRequests.intern_eq_of_nil proves the guarantee machine-checked: a []-certificate forces an unchanged intern table on both outcomes, so requests are an honest upper bound on a run's interning and the support quantifier matches the documented choose-final-support-up-front design. The statements pin an opaque StatementCacheSemantics stub (the K1 machinery is proved only for the whnfCacheSemantics family; arbitrary keys/fallbacks are refutable), so KernelRunInv no longer quantifies over semantics. Statement names and the four-sorry frontier are unchanged; NatFixture's satisfiability witnesses compile verbatim. * tc: mirror the kernel's Nat-offset machinery in the Lean spec The offset work landed Rust-side only, so spec and implementation disagreed on exactly the large-offset inputs it was built for: Rust strips a shared offset in one step, keeps 'Nat.add base (Lit n)' / 'Nat.div|mod base (Lit k)' stuck in compact form, and collapses symbolic-base linear Nat.rec to the compact offset, while Lean still peeled one succ per isDefEqCall level (maxRecDepth at k ≈ 2000, and succ-tower materialization in WHNF beyond 10k) and required a literal base for the linear-rec collapse. Port all three pieces: tryDefEqOffset decomposes both sides via natOffsetDecompose behind an O(1) natOffsetCandidate probe and strips the shared offset in one step (verdict-preserving by definitional +k injectivity); tryNatOffsetStuck freezes compact offset forms before delta at the same decision point as the Rust loop; and tryReduceNatSuccLinearRec gains the symbolic-base branch, gated on the recursor application carrying no post-major arguments. Verify ripple: the natRecLiteralParts totalization equation picks up majorIdx, and NatFixture's full-WHNF step walk certifies the offset-stuck probe returns none on the fixture for any primitive address assignment. Tests pin each piece against regressions: stays-compact under decoy Nat.add/div/mod definitions that delta would expose, the bulk strip at k = 2500 (one-succ peeling exceeds the def-eq depth limit there), div-derived vs add-derived stuck forms staying unequal, and the linear-rec collapse with its post-major conservatism. * tests: drop the tc-node-addr bit-parity harness Uid identity removed per-node content addresses from the Rust kernel, so the oracle dump's ty/extra columns became 16-hex intern uids — process-history-dependent values that can never byte-match the Lean side's Blake3 node addresses. The suite could only fail, and since ignored.yml runs 'lake test -- --ignored' on every push to main, it would turn Extended CI red on merge. The one column still comparable (the constant id) is read from the same serialized env bytes on both sides, so a slimmed comparison would check only traversal enumeration — coverage tc-anon-diff already provides against the real Rust verdicts. Remove the suite, its FFI oracle, and the extern binding; reword the Egress module doc that cited the harness as a level-reduction certifier. * kernel: allocate intern uids in thread-local blocks NEXT_UID was a single process-global cache line hit by a relaxed fetch_add for every node interned by every checker worker. The blake3 identity it replaced was pure per-worker work, so the old kernel scaled linearly with workers; the uid kernel is ~1.4x faster per core but its whole-env throughput plateaued near 5.7K consts/s as worker counts grew — the ooc InitStd !benchmark regression (9.96 s -> 16.97 s on the 32-thread bench runner, while every per-constant row improved; the same binaries tie at 24 local workers and the uid side wins 1.41x at 6). Hand out uids in per-thread blocks of 2^20 reserved from the global counter, touching the shared line once per block instead of once per node. Blocks are never reused (a thread's unspent remainder is abandoned on exit), so uid uniqueness and the never-reuse cache-key guarantee are unchanged; the exhaustion guard aborts a block early instead of one uid early. Local whole-env InitStd at 24 workers drops 15.58 s -> 11.04 s (old kernel: 15.49 s), and 6->24 worker scaling recovers from 1.60x to 2.02x. * bench: record tool faults as crash, not oom A 128+signal death was always recorded as an OOM row, so a zisk mem-planner segfault (exit 139) rendered as OOM and sent the investigation chasing RAM budgets instead of a heap-overflow bug. Split the kill statuses: explicit kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other signal death records status crash and renders as 💥 CRASH in the compare table. * kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2) The profiler counted whnf entries, def-eq entries, and limb-weighted Nat arithmetic per constant but dropped them at block aggregation, and nothing counted term-construction volume at all — leaving the shard cost model only heartbeats, subst, and bytes to predict guest steps from. Persist all four op counters per block (format v2) plus a new intern-table visit counter (a proxy for construction/memory traffic, bumped in intern_expr/intern_univ), and add a shard_features example that emits a per-shard feature CSV from a profile + manifest pair for calibrating the cost model against externally measured shard costs (ziskemu -X on dumped shard inputs). * zisk: dump every selected shard's input; skip ROM setup in dump mode --dump-input wrote only the first selected shard and exited, so dumping a 13-shard plan took 13 host invocations. Dump every selected shard in one run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard keeps the exact path), and skip client.setup when no proof store is involved — dump mode never runs the VM and needs the ROM setup (and thus the proving key) only to derive the shard vk for store filtering. * kernel: calibrate the shard planner in Zisk cost units Replace the heartbeat-based guest-STEP model with one denominated in ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES + BASE), so the packing target prices the axes that don't ride the main trace — DMA/blake3 precompile area and memory ops. Calibration corpus: 118 InitStd shards across 13 constants, each measured with ziskemu -X on inputs dumped via --dump-input. cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq + 28.4k*intern (+ 73.2k per cross-ingress byte) MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per work item, so intra-shard cache sharing is invisible to per-block features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram. On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on the uid-identity kernel; the intern term carries the memory-traffic/DMA axis (residual correlation 0.91 with dma_memcpy counts). Prover models refit on the same corpus. RAM comes from a guarded GPU prove sweep measured as each prover's systemd-scope cgroup memory.peak — the OOM-relevant metric CI's watchdog enforces, charging the whole process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost (was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s measured vs 411s predicted at the largest point). Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards (instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within the actual-cost ceiling; the only violations are the two INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB single-leaf), correctly flagged as not fitting the budget. * bench: per-constant ooc attribution and a compare top-movers drill-down A whole-env ooc regression previously surfaced as one env-keyed number, with drill-down only into the pre-chosen bench vectors. Now the anon whole-env check attributes itself: check-rs --per-const <csv> records one entry per work item (wall nanos, heartbeats, the op counters, and the predicted Zisk cost via the shard model) from the check loop, and the CLI joins Lean names from the env's named table (projection-name fallback for anonymized Muts blocks) so entries survive PRs that shift content addresses. An entry is ONE constant's (or Muts block's) own check — deps are lazily ingressed and trusted, each checked in its own entry, with the consulted closure slice's ingress charged to the entry — so entries sum to the env total with no double counting. NOT the full-closure scope of --consts measurements; documented at the recording site, the flag help, the renderer, and in the rendered output. The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to the results file (rotated with the local baseline), and ix bench compare renders a drill-down when both sides carry one, split by evidence quality — calibrated on a Mathlib A/A run (640K constants, twice through one binary): wall time swings up to 2.8s from scheduling alone, while the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9 absolute; worker->item assignment varies uid blocks and uid-keyed hash iteration order perturbs a few order-sensitive paths; --workers 1 is exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own cost OR >= 1e9 outright, both above the drift envelope) lead the drill-down ranked by percent change, styled like the main table ('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are quarantined in a labeled noise section capped at 5 rows. On the A/A run this renders 0 cost movers, the truthful reading. * bench: verdict-first cell layout; collapse tables past 5 rows A multi-cell !benchmark comment stacked every cell's full table; long cells (a 40-constant zisk table) buried the verdicts. Each cell now leads with its one-line verdict (and any typecheck failures / empty-side warnings, which stay unconditionally visible), and the comparison table collapses into a <details> block when it has more than 5 rows — small cells (the ooc env row, few-constant runs) stay inline. The per-constant and phase drill-downs were already collapsible. * ci: wire the ooc attribution CSV through the !benchmark pipeline bencher.dev stores metric rows only, so the per-constant drill-down needs the attribution CSVs to travel beside the results files. bench-main caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores the base SHA's entry, carries a base-run-produced CSV through the merge step (which previously renamed base.json into main.json and orphaned it), and pairs whichever CSV it has with the PR side's. The main side ends up with exactly two sources: bencher on FULL coverage (plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun for anything less — base SHA not uploaded, partial coverage, an ooc attribution cache miss, or the fresh token. A rerun measures the full default selection (a BENCH_CONSTS override still narrows it) and its rows take priority; bencher-fetched rows only fill rows the rerun failed to produce, and the table's main-source label says which path ran. This retires the gap-filling machinery (--consts from missing.txt, the bencher-priority merge arm) — a full rerun is simpler and self-consistent, at the cost of re-measuring a cell when a PR adds constants. * zisk: drop the vendored guest linker script Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the riscv64ima-zisk-zkvm-elf linker script in the target spec again, and passing the vendored copy on top double-defines the rom/ram memory regions. Both guest build scripts existed only to pass it — remove them and the script; the toolchain's embedded script is the single source of the memory layout. * zisk: pin the fork branch with the mem-planner fill_padding fix Bump every zisk fork pin from blake3-precompile (e4057c4) to blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows the mem-planner offsets array before fill_padding pads the last page — the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the shard that crashed 4/4 on the old pin executes clean on the new one (634M cycles, failures=0), as does the full 13-shard plan on the locally-patched build the fix was developed against. * chore: fix clippy lints (casts, qualifications, poison error, let-chain) u32::try_from over as-truncation and u64::from over as-widening in shard_features; drop redundant std::sync:: qualifications; carry the PoisonError text instead of discarding it; collapse the texray if into a let-chain; contains() over iter().any() in the holed-work filter. * chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build deliberately skips the guest compilation under clippy, but include_elf! still demanded the ELF bytes. Gate the embed (and its import) on cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes under clippy. Also collapse the texray if into a let-chain, matching the zisk host. A real release build of the host still works. * ci: clippy gates for the zisk and sp1 host workspaces The root rust-test clippy never enters the standalone zkVM workspaces, so their warnings accumulated ungated. Add cargo clippy --release --all-targets -D warnings to both host jobs, after the build so the release dep artifacts are shared (and, for zisk, the guest ELFs its build scripts already produced). * chore: String.dropEnd over deprecated String.dropRight * Unpin ziskup install * ci: align install-zisk comments with the unpinned toolchain * Clean up dev tooling and experiment artifacts for PR - Untrack sp1/zisk benchmark logs and scripts - Remove dev-tooling examples from ix-kernel: examples are for showing users how to use the crate; the shard-planning and perf binaries live on in git history - Remove the env-machine design doc; the as-built machine is documented at the code (whnf.rs machine_whnf, subst.rs Clo) --------- Co-authored-by: John C. Burnham <john@agathic.com>

johnchandlerburnham · 2026-07-04T06:34:29Z

Summary

Two related changes to the content-addressing layer and its aux-constant handling, fixing underlying issue reported in #465

1. Ixon no longer stores recr/refl/nested on Inductive. These are derivable
from constructor structure, so storing them was redundant and trusting declared values
was an adversarial surface (e.g. is_rec = false on a recursive inductive enables
improper struct-eta). The kernel now computes is_rec on demand, memoized in a new env
cache with a provisional entry to break the whnf → try_struct_eta_iota → is_struct_like
cycle; this replaces the declared-vs-computed check in check_inductive. The compile
side gains compute_lean_ind_flags to recompute Lean's block-wide
isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a
source Lean env (kernel egress, decompile), and validate_lean_ind_flags to check a
whole env against the recomputation.

2. Evaporated auxiliaries get a canonical form. When SCC splitting strands a nested
aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and
dropping the irrelevant over-merged motives leaves exactly the external inductive's
generic recursor. Canonical treatment: rec_N claims alias <Ext>.rec (e.g.
List.rec), call sites are rebuilt onto the external telescope via head-rewrite
CallSitePlans (owner-gated, single-motive targets), and below_N/brecOn_N compile as
surgered originals like _sizeOf_N. Fixes the AuxDedup kernel-check failures (28 → 0);
AuxDedup1 now generates auxiliaries identical to AuxDedup2's canonical structure.
Documented in docs/ix_canonicity.md §6.5.

Byte-exact aux roundtrip

roundtrip_block Phase A (recompile the regenerated Lean form, compare against the
stored original address) silently failed for 1529 of 1545 aux constants — including
plain stdlib like Nat.casesOn. Root cause: every production compile path preseeds the
ref/univ tables in sorted order (preseed_expr_tables) before compiling, and the
serialized constant embeds those tables; Phase A compiled without the preseed, filling
the tables in traversal order instead — every Ref/univ index permuted, byte-different
but semantically identical constants (decode resolves through the embedded table). A
debug probe recompiling the Lean original through the identical path proved
compile(original) == compile(regen) in every case: regeneration was always faithful,
the comparison context was not.

With the preseed mirrored in Phase A the invariant holds corpus-wide, so a Phase-A
recompile-hash mismatch is now a hard error with no aux exemption, and every
roundtrip arm records failures in aux_gen_errors (recovery keeps the Lean-facing env
populated for diagnosis but is never silent). Related hardening: call-site surgery
detection is durable across serialization (Named.original.is_some() alongside the
in-memory map), shift-aware instantiate_rev in the type-walking helpers (fixes fvar
leaks in .brecOn.go bodies), and the below-def roundtrip loop filters by the
original-gated members like its sibling loops. IX_ROUNDTRIP_DEBUG now dumps hashed
component summaries and runs an original-form recompile probe on any mismatch.

Test fixes and fixtures

kernel-tutorial: bad_raw_consts inductive fixtures carry recomputation-honest flags
so the whole-env validate_ind_flags no longer poisons the shared tutorial env
(73/335 → 335/335, with the kernel rejecting each bad fixture as designed).
validate-aux: seeds match module-private fixture names via privateToUserName?, the
Canonicity prefix is enabled, and Phase 4b gains per-module markers so a fully absent
identity group fails loudly when its fixture module is loaded (previously vacuous at
0 pass / 0 fail, now 109 pass / 0 fail).
New fixtures: AuxDedup1/AuxDedup2 (cross-block aux dedup), AuxDedupMixed (a perm
mixing a canonical slot and PERM_OUT_OF_SCC for the same owner), plus a
CompileMutualFixtures benchmark lib.

Gates

kernel-check-env: 201296/201296
rust-compile: all phases, 0 aux_gen errors / 0 mismatches / 0 Phase-A address
divergences on the full 213k env (live and deserialized)
validate-aux: 0 failures at 4393-constant scope
rust-serialize: byte-exact; kernel-ixon-roundtrip: 143694/0
kernel-tutorial: 335/335; cargo test workspace and lake test green;
cargo clippy --all-targets clean
lake exe ix check-rs compilemathlib.ixe: 736618/736618 passed, 0 failed (325.3s)
lake exe ix validate Benchmarks/Compile/CompileMathlib.lean: 0 failures (1528.33s total)

Remove the `recr`/`refl` bools and the `nested` count from the Ixon `Inductive` constant and its serialization (Rust and Lean), and from the `Indc` reveal-proof variant, renumbering the field-presence mask bits. These flags are derivable from constructor structure, so storing them was redundant and trusting declared values was an adversarial surface (e.g. is_rec = false on a recursive inductive enables improper struct-eta). - kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now computed on demand (computed_is_rec), memoized in the new env is_rec_cache with a provisional entry to break the whnf -> try_struct_eta_iota -> is_struct_like cycle. This replaces the declared-vs-computed H1 verification in check_inductive. - compile: new compute_lean_ind_flags recomputes Lean's block-wide isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a source Lean env (kernel egress, decompile), since Ixon no longer stores the flags; validate_lean_ind_flags checks a whole env against the recomputation. - tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising aux-constant dedup across blocks (fix forthcoming); add a CompileMutualFixtures benchmark lib building the mutual test fixtures; ignore *.ixe.

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a nested aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and dropping the irrelevant over-merged motives leaves exactly the external inductive's generic recursor. Canonical treatment: `rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are rebuilt onto the external telescope via head-rewrite CallSitePlans (owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner. Documented in docs/ix_canonicity.md 6.5. Call-site surgery guard is now durable across serialization: aux-regen detection accepts `Named.original.is_some()` in addition to the in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles no longer misapply surgery. Shift-aware `instantiate_rev` replaces unshifted substitution in the type-walking helpers (fixes fvar leaks in `.brecOn.go` bodies). Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the ref/univ tables (`preseed_expr_tables`) like every production compile path. The serialized constant embeds those tables in sorted order; compiling without the preseed filled them in traversal order instead, permuting every `Ref`/univ index — byte-different but semantically identical constants (decode resolves through the embedded table). This silently failed the Phase-A address comparison against `Named.original.0` for 1529 of 1545 aux constants (including plain stdlib like `Nat.casesOn`); a debug probe proved compile(original) == compile(regen) in every case, i.e. the regeneration itself was always faithful. With the invariant holding corpus-wide, the Phase-A recompile-hash mismatch is now a hard error with no aux exemption, and every roundtrip arm records failures in `aux_gen_errors` (recovery keeps the Lean-facing env populated for diagnosis but is never silent). Pass-2 scope hygiene: the below-def roundtrip loop filters by the original-gated `aux_members` like its sibling loops, so evaporated `below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now dumps hashed component scalars/hashes and runs an original-form recompile probe for any mismatch. Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry recomputation-honest flags so compile-side `validate_ind_flags` no longer poisons the shared tutorial env (73/335 -> 335/335, with the kernel rejecting each bad fixture as designed); validate-aux seeds match module-private fixture names via `privateToUserName?` and enable the Canonicity prefix; Phase 4b gains per-module markers so a fully absent identity group fails loudly when its fixture module is loaded (previously vacuous at 0 pass / 0 fail, now 109 pass). Gates: kernel-check-env 201296/201296; rust-compile all phases with 0 aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the full 213k env (live and deserialized); validate-aux 0 failures at 4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip 143694/0; kernel-tutorial 335/335; cargo test and lake test green.

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`: map_or over map+unwrap_or and slice::contains in surgery.rs, an enumerate loop for the motive-peeling walk in aux_motive_sigs, and let-chain collapses for the inductive-flags fixup loops in decompile.rs and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over from the previous commit.

Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).

Port of the two Rust kernel fixes on this branch: - Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand (computed_is_rec_ind), nested detection is structural (member_has_nested / ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten member-scoped without the declared nested count. Serialization packs one bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive addresses re-pinned. - collectDependencies (Ix/Common.lean) now closes over a declaration's full recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference in rule RHSs) plus each rule ctor's owning external recursor (List.rec). Without these the per-name compile either failed (MissingConstant AuxDedup1.C.rec from A.rec_1's block) or silently skipped the evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2 in original form, which the kernel rejects. AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join kernelCheckEntries; the four evaporated rec_N entries pin the identical 3_073_003 FFT cost (their claims are byte-exact List.rec: lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2). All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

…nment-machine WHNF reducer (#442) * kernel: uid identity, env-machine WHNF, and reduction-loop perf Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%. * kernel: native perf/shard examples (out-of-circuit tooling) Standalone cargo examples over a .ixe env, bypassing the Lean/FFI layer, updated to main's steps-based shard cost model (block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram): - shard_plan: profile → partition → .ixes manifest, with store-aware planning (--store-dir drops work items whose targets the proof store already covers, and excludes covered blocks from the partition hypergraph — a novel→covered edge is an assumption discharged at aggregation, not a cut to minimize); sizes N from machine RAM by default. - perf_check / check_one: native rerun of the guest check_const loop so IX_* perf-counter instrumentation can target a single expensive constant without re-checking its env. - heaviest_block / block_reduce_histo / shard_names / manifest_info: profiling forensics over blocks and manifests. * zisk+sp1: prover batch scripts and logs; bench-compile-init - zisk/scripts: prove-batch (sequential shard proving), mem-guard (MemAvailable watchdog that kills zisk-host before the OOM killer wedges the box), bench-cycles, mergesort-250k repro; reference logs. - sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with WITHOUT_VK_VERIFICATION=1). - Lean side: bench-compile-init lake exe (imports Init, empty main). * zisk: close aggregation soundness gaps (failures word, transitive vk pinning) The aggregate proof was weaker than "these subjects are well-typed": - The agg guest never read a child's committed failures word (slot 10) and hard-committed 0 for its own, so aggregation ERASED the failure bit — a kernel-rejected constant could appear under a failures=0 root, with only host-side courtesy checks in the way. Every child's failures word is now asserted 0 in-circuit. - vk pinning was not transitive: a child that is itself an aggregate was pinned only by its program vk (the shared AGG vk); its own allowed-vk set was never inspected. An agg-of-1 built against a rogue allowed set (wrapping an arbitrary program's "proof" with forged publics) would fold under an honest-looking root. The agg guest now requires every aggregate child (allowed-set index ≥ 1, by the new positional convention: index 0 = leaf vk, the rest agg vks) to commit THIS instance's vks id — the allowed set is uniform down the tree, so the pin is recursive. The convention's ordering is bound by the committed id hash, which external verifiers already check. - The host derived the allowed set FROM the untrusted child proofs (distinct_vks), so any proof admitted its own program, and a stale store folded silently under its old vk. The allowed set is now [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk after ROM setup); freshly produced proofs are asserted to match; stored proofs with a different vk are skipped (re-proven); and the root's committed vks id is checked against — and printed for — external verifiers. - A manifest bisection tree whose leaf set differs from the shard id set silently dropped proven leaves from the fold while the pre-aggregation coverage check (counting proofs PRODUCED, not folded) still passed. ShardManifest::from_bytes now rejects such trees, and the host additionally checks post-fold that every env target is in the root's actual subject set. * ixon: memoize deferred address verification (one hash per constant per load) The bench run on the rebase preview (06e1a1d) showed the whole-env ooc/InitStd row at +63.9% (10.96 s -> 17.97 s) while every per-constant row improved. Cause: LazyConstant::get() re-ran Address::hash(bytes) on every materialization, and the check loop re-ingresses each work item's closure after clear_releasing_memory() (IX_KERNEL_CHECK_CLEAR_EVERY=1), so each constant was re-hashed once per closure it appears in — inside the timed window. Pre-deferral the total was one hash per constant, at load time. Memoize the SUCCESSFUL check per entry (Arc<AtomicBool>, shared by clones, which share the bytes): the first get() still hash-checks before parsing; later get()s skip the hash. Failures are never memoized — bytes are immutable, so a mismatched entry re-fails on every call. This restores the one-hash-per-constant total while keeping load lazy. Also: unit tests for the deferred path (verify-once, failure never memoized, clones share the verdict), drop a dead 'let _ = i;' in get_anon, and note the memoization in docs/kernel_identity.md. * verify: make the pinned trust-frontier statements dischargeable ExecutionRequests' set/modifyGet constructors certified an arbitrary silent state transformation with an empty request list, so any program could be rewritten (funext + of_eq) as modifyGet-of-its-own-run bound into a pure/throw dispatch — ExecutionRequests x s [] held for every program, RunAssumptions was satisfiable with a support covering only the initial intern table, and the module docstring's central claim ("no constructor for an arbitrary silent computation") was false. Independently, the four headline statements universally quantified {semantics : CacheSemantics} — blockErrorsOnly is a lawful instance that invalidates every .expr cache insertion, refuting any run that warms a cache — and demanded the fixed support cover the POST-state intern table, refuting any run that interns. TcM.checkConst.wf was refutable outright; the other three were shielded only by the opaque StatementTrKExpr. set/modifyGet now carry intern-preservation hypotheses at the indexed state, and the new ExecutionRequests.intern_eq_of_nil proves the guarantee machine-checked: a []-certificate forces an unchanged intern table on both outcomes, so requests are an honest upper bound on a run's interning and the support quantifier matches the documented choose-final-support-up-front design. The statements pin an opaque StatementCacheSemantics stub (the K1 machinery is proved only for the whnfCacheSemantics family; arbitrary keys/fallbacks are refutable), so KernelRunInv no longer quantifies over semantics. Statement names and the four-sorry frontier are unchanged; NatFixture's satisfiability witnesses compile verbatim. * tc: mirror the kernel's Nat-offset machinery in the Lean spec The offset work landed Rust-side only, so spec and implementation disagreed on exactly the large-offset inputs it was built for: Rust strips a shared offset in one step, keeps 'Nat.add base (Lit n)' / 'Nat.div|mod base (Lit k)' stuck in compact form, and collapses symbolic-base linear Nat.rec to the compact offset, while Lean still peeled one succ per isDefEqCall level (maxRecDepth at k ≈ 2000, and succ-tower materialization in WHNF beyond 10k) and required a literal base for the linear-rec collapse. Port all three pieces: tryDefEqOffset decomposes both sides via natOffsetDecompose behind an O(1) natOffsetCandidate probe and strips the shared offset in one step (verdict-preserving by definitional +k injectivity); tryNatOffsetStuck freezes compact offset forms before delta at the same decision point as the Rust loop; and tryReduceNatSuccLinearRec gains the symbolic-base branch, gated on the recursor application carrying no post-major arguments. Verify ripple: the natRecLiteralParts totalization equation picks up majorIdx, and NatFixture's full-WHNF step walk certifies the offset-stuck probe returns none on the fixture for any primitive address assignment. Tests pin each piece against regressions: stays-compact under decoy Nat.add/div/mod definitions that delta would expose, the bulk strip at k = 2500 (one-succ peeling exceeds the def-eq depth limit there), div-derived vs add-derived stuck forms staying unequal, and the linear-rec collapse with its post-major conservatism. * tests: drop the tc-node-addr bit-parity harness Uid identity removed per-node content addresses from the Rust kernel, so the oracle dump's ty/extra columns became 16-hex intern uids — process-history-dependent values that can never byte-match the Lean side's Blake3 node addresses. The suite could only fail, and since ignored.yml runs 'lake test -- --ignored' on every push to main, it would turn Extended CI red on merge. The one column still comparable (the constant id) is read from the same serialized env bytes on both sides, so a slimmed comparison would check only traversal enumeration — coverage tc-anon-diff already provides against the real Rust verdicts. Remove the suite, its FFI oracle, and the extern binding; reword the Egress module doc that cited the harness as a level-reduction certifier. * kernel: allocate intern uids in thread-local blocks NEXT_UID was a single process-global cache line hit by a relaxed fetch_add for every node interned by every checker worker. The blake3 identity it replaced was pure per-worker work, so the old kernel scaled linearly with workers; the uid kernel is ~1.4x faster per core but its whole-env throughput plateaued near 5.7K consts/s as worker counts grew — the ooc InitStd !benchmark regression (9.96 s -> 16.97 s on the 32-thread bench runner, while every per-constant row improved; the same binaries tie at 24 local workers and the uid side wins 1.41x at 6). Hand out uids in per-thread blocks of 2^20 reserved from the global counter, touching the shared line once per block instead of once per node. Blocks are never reused (a thread's unspent remainder is abandoned on exit), so uid uniqueness and the never-reuse cache-key guarantee are unchanged; the exhaustion guard aborts a block early instead of one uid early. Local whole-env InitStd at 24 workers drops 15.58 s -> 11.04 s (old kernel: 15.49 s), and 6->24 worker scaling recovers from 1.60x to 2.02x. * bench: record tool faults as crash, not oom A 128+signal death was always recorded as an OOM row, so a zisk mem-planner segfault (exit 139) rendered as OOM and sent the investigation chasing RAM budgets instead of a heap-overflow bug. Split the kill statuses: explicit kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other signal death records status crash and renders as 💥 CRASH in the compare table. * kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2) The profiler counted whnf entries, def-eq entries, and limb-weighted Nat arithmetic per constant but dropped them at block aggregation, and nothing counted term-construction volume at all — leaving the shard cost model only heartbeats, subst, and bytes to predict guest steps from. Persist all four op counters per block (format v2) plus a new intern-table visit counter (a proxy for construction/memory traffic, bumped in intern_expr/intern_univ), and add a shard_features example that emits a per-shard feature CSV from a profile + manifest pair for calibrating the cost model against externally measured shard costs (ziskemu -X on dumped shard inputs). * zisk: dump every selected shard's input; skip ROM setup in dump mode --dump-input wrote only the first selected shard and exited, so dumping a 13-shard plan took 13 host invocations. Dump every selected shard in one run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard keeps the exact path), and skip client.setup when no proof store is involved — dump mode never runs the VM and needs the ROM setup (and thus the proving key) only to derive the shard vk for store filtering. * kernel: calibrate the shard planner in Zisk cost units Replace the heartbeat-based guest-STEP model with one denominated in ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES + BASE), so the packing target prices the axes that don't ride the main trace — DMA/blake3 precompile area and memory ops. Calibration corpus: 118 InitStd shards across 13 constants, each measured with ziskemu -X on inputs dumped via --dump-input. cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq + 28.4k*intern (+ 73.2k per cross-ingress byte) MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per work item, so intra-shard cache sharing is invisible to per-block features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram. On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on the uid-identity kernel; the intern term carries the memory-traffic/DMA axis (residual correlation 0.91 with dma_memcpy counts). Prover models refit on the same corpus. RAM comes from a guarded GPU prove sweep measured as each prover's systemd-scope cgroup memory.peak — the OOM-relevant metric CI's watchdog enforces, charging the whole process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost (was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s measured vs 411s predicted at the largest point). Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards (instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within the actual-cost ceiling; the only violations are the two INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB single-leaf), correctly flagged as not fitting the budget. * bench: per-constant ooc attribution and a compare top-movers drill-down A whole-env ooc regression previously surfaced as one env-keyed number, with drill-down only into the pre-chosen bench vectors. Now the anon whole-env check attributes itself: check-rs --per-const <csv> records one entry per work item (wall nanos, heartbeats, the op counters, and the predicted Zisk cost via the shard model) from the check loop, and the CLI joins Lean names from the env's named table (projection-name fallback for anonymized Muts blocks) so entries survive PRs that shift content addresses. An entry is ONE constant's (or Muts block's) own check — deps are lazily ingressed and trusted, each checked in its own entry, with the consulted closure slice's ingress charged to the entry — so entries sum to the env total with no double counting. NOT the full-closure scope of --consts measurements; documented at the recording site, the flag help, the renderer, and in the rendered output. The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to the results file (rotated with the local baseline), and ix bench compare renders a drill-down when both sides carry one, split by evidence quality — calibrated on a Mathlib A/A run (640K constants, twice through one binary): wall time swings up to 2.8s from scheduling alone, while the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9 absolute; worker->item assignment varies uid blocks and uid-keyed hash iteration order perturbs a few order-sensitive paths; --workers 1 is exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own cost OR >= 1e9 outright, both above the drift envelope) lead the drill-down ranked by percent change, styled like the main table ('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are quarantined in a labeled noise section capped at 5 rows. On the A/A run this renders 0 cost movers, the truthful reading. * bench: verdict-first cell layout; collapse tables past 5 rows A multi-cell !benchmark comment stacked every cell's full table; long cells (a 40-constant zisk table) buried the verdicts. Each cell now leads with its one-line verdict (and any typecheck failures / empty-side warnings, which stay unconditionally visible), and the comparison table collapses into a <details> block when it has more than 5 rows — small cells (the ooc env row, few-constant runs) stay inline. The per-constant and phase drill-downs were already collapsible. * ci: wire the ooc attribution CSV through the !benchmark pipeline bencher.dev stores metric rows only, so the per-constant drill-down needs the attribution CSVs to travel beside the results files. bench-main caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores the base SHA's entry, carries a base-run-produced CSV through the merge step (which previously renamed base.json into main.json and orphaned it), and pairs whichever CSV it has with the PR side's. The main side ends up with exactly two sources: bencher on FULL coverage (plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun for anything less — base SHA not uploaded, partial coverage, an ooc attribution cache miss, or the fresh token. A rerun measures the full default selection (a BENCH_CONSTS override still narrows it) and its rows take priority; bencher-fetched rows only fill rows the rerun failed to produce, and the table's main-source label says which path ran. This retires the gap-filling machinery (--consts from missing.txt, the bencher-priority merge arm) — a full rerun is simpler and self-consistent, at the cost of re-measuring a cell when a PR adds constants. * zisk: drop the vendored guest linker script Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the riscv64ima-zisk-zkvm-elf linker script in the target spec again, and passing the vendored copy on top double-defines the rom/ram memory regions. Both guest build scripts existed only to pass it — remove them and the script; the toolchain's embedded script is the single source of the memory layout. * zisk: pin the fork branch with the mem-planner fill_padding fix Bump every zisk fork pin from blake3-precompile (e4057c4) to blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows the mem-planner offsets array before fill_padding pads the last page — the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the shard that crashed 4/4 on the old pin executes clean on the new one (634M cycles, failures=0), as does the full 13-shard plan on the locally-patched build the fix was developed against. * chore: fix clippy lints (casts, qualifications, poison error, let-chain) u32::try_from over as-truncation and u64::from over as-widening in shard_features; drop redundant std::sync:: qualifications; carry the PoisonError text instead of discarding it; collapse the texray if into a let-chain; contains() over iter().any() in the holed-work filter. * chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build deliberately skips the guest compilation under clippy, but include_elf! still demanded the ELF bytes. Gate the embed (and its import) on cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes under clippy. Also collapse the texray if into a let-chain, matching the zisk host. A real release build of the host still works. * ci: clippy gates for the zisk and sp1 host workspaces The root rust-test clippy never enters the standalone zkVM workspaces, so their warnings accumulated ungated. Add cargo clippy --release --all-targets -D warnings to both host jobs, after the build so the release dep artifacts are shared (and, for zisk, the guest ELFs its build scripts already produced). * chore: String.dropEnd over deprecated String.dropRight * Unpin ziskup install * ci: align install-zisk comments with the unpinned toolchain * Clean up dev tooling and experiment artifacts for PR - Untrack sp1/zisk benchmark logs and scripts - Remove dev-tooling examples from ix-kernel: examples are for showing users how to use the crate; the shard-planning and perf binaries live on in git history - Remove the env-machine design doc; the as-built machine is documented at the code (whnf.rs machine_whnf, subst.rs Clo) --------- Co-authored-by: John C. Burnham <john@agathic.com>

johnchandlerburnham · 2026-07-04T06:34:29Z

Summary

Two related changes to the content-addressing layer and its aux-constant handling, fixing underlying issue reported in #465

1. Ixon no longer stores recr/refl/nested on Inductive. These are derivable
from constructor structure, so storing them was redundant and trusting declared values
was an adversarial surface (e.g. is_rec = false on a recursive inductive enables
improper struct-eta). The kernel now computes is_rec on demand, memoized in a new env
cache with a provisional entry to break the whnf → try_struct_eta_iota → is_struct_like
cycle; this replaces the declared-vs-computed check in check_inductive. The compile
side gains compute_lean_ind_flags to recompute Lean's block-wide
isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a
source Lean env (kernel egress, decompile), and validate_lean_ind_flags to check a
whole env against the recomputation.

2. Evaporated auxiliaries get a canonical form. When SCC splitting strands a nested
aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and
dropping the irrelevant over-merged motives leaves exactly the external inductive's
generic recursor. Canonical treatment: rec_N claims alias <Ext>.rec (e.g.
List.rec), call sites are rebuilt onto the external telescope via head-rewrite
CallSitePlans (owner-gated, single-motive targets), and below_N/brecOn_N compile as
surgered originals like _sizeOf_N. Fixes the AuxDedup kernel-check failures (28 → 0);
AuxDedup1 now generates auxiliaries identical to AuxDedup2's canonical structure.
Documented in docs/ix_canonicity.md §6.5.

Byte-exact aux roundtrip

roundtrip_block Phase A (recompile the regenerated Lean form, compare against the
stored original address) silently failed for 1529 of 1545 aux constants — including
plain stdlib like Nat.casesOn. Root cause: every production compile path preseeds the
ref/univ tables in sorted order (preseed_expr_tables) before compiling, and the
serialized constant embeds those tables; Phase A compiled without the preseed, filling
the tables in traversal order instead — every Ref/univ index permuted, byte-different
but semantically identical constants (decode resolves through the embedded table). A
debug probe recompiling the Lean original through the identical path proved
compile(original) == compile(regen) in every case: regeneration was always faithful,
the comparison context was not.

With the preseed mirrored in Phase A the invariant holds corpus-wide, so a Phase-A
recompile-hash mismatch is now a hard error with no aux exemption, and every
roundtrip arm records failures in aux_gen_errors (recovery keeps the Lean-facing env
populated for diagnosis but is never silent). Related hardening: call-site surgery
detection is durable across serialization (Named.original.is_some() alongside the
in-memory map), shift-aware instantiate_rev in the type-walking helpers (fixes fvar
leaks in .brecOn.go bodies), and the below-def roundtrip loop filters by the
original-gated members like its sibling loops. IX_ROUNDTRIP_DEBUG now dumps hashed
component summaries and runs an original-form recompile probe on any mismatch.

Test fixes and fixtures

kernel-tutorial: bad_raw_consts inductive fixtures carry recomputation-honest flags
so the whole-env validate_ind_flags no longer poisons the shared tutorial env
(73/335 → 335/335, with the kernel rejecting each bad fixture as designed).
validate-aux: seeds match module-private fixture names via privateToUserName?, the
Canonicity prefix is enabled, and Phase 4b gains per-module markers so a fully absent
identity group fails loudly when its fixture module is loaded (previously vacuous at
0 pass / 0 fail, now 109 pass / 0 fail).
New fixtures: AuxDedup1/AuxDedup2 (cross-block aux dedup), AuxDedupMixed (a perm
mixing a canonical slot and PERM_OUT_OF_SCC for the same owner), plus a
CompileMutualFixtures benchmark lib.

Gates

kernel-check-env: 201296/201296
rust-compile: all phases, 0 aux_gen errors / 0 mismatches / 0 Phase-A address
divergences on the full 213k env (live and deserialized)
validate-aux: 0 failures at 4393-constant scope
rust-serialize: byte-exact; kernel-ixon-roundtrip: 143694/0
kernel-tutorial: 335/335; cargo test workspace and lake test green;
cargo clippy --all-targets clean
lake exe ix check-rs compilemathlib.ixe: 736618/736618 passed, 0 failed (325.3s)
lake exe ix validate Benchmarks/Compile/CompileMathlib.lean: 0 failures (1528.33s total)

Remove the `recr`/`refl` bools and the `nested` count from the Ixon `Inductive` constant and its serialization (Rust and Lean), and from the `Indc` reveal-proof variant, renumbering the field-presence mask bits. These flags are derivable from constructor structure, so storing them was redundant and trusting declared values was an adversarial surface (e.g. is_rec = false on a recursive inductive enables improper struct-eta). - kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now computed on demand (computed_is_rec), memoized in the new env is_rec_cache with a provisional entry to break the whnf -> try_struct_eta_iota -> is_struct_like cycle. This replaces the declared-vs-computed H1 verification in check_inductive. - compile: new compute_lean_ind_flags recomputes Lean's block-wide isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a source Lean env (kernel egress, decompile), since Ixon no longer stores the flags; validate_lean_ind_flags checks a whole env against the recomputation. - tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising aux-constant dedup across blocks (fix forthcoming); add a CompileMutualFixtures benchmark lib building the mutual test fixtures; ignore *.ixe.

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a nested aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and dropping the irrelevant over-merged motives leaves exactly the external inductive's generic recursor. Canonical treatment: `rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are rebuilt onto the external telescope via head-rewrite CallSitePlans (owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner. Documented in docs/ix_canonicity.md 6.5. Call-site surgery guard is now durable across serialization: aux-regen detection accepts `Named.original.is_some()` in addition to the in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles no longer misapply surgery. Shift-aware `instantiate_rev` replaces unshifted substitution in the type-walking helpers (fixes fvar leaks in `.brecOn.go` bodies). Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the ref/univ tables (`preseed_expr_tables`) like every production compile path. The serialized constant embeds those tables in sorted order; compiling without the preseed filled them in traversal order instead, permuting every `Ref`/univ index — byte-different but semantically identical constants (decode resolves through the embedded table). This silently failed the Phase-A address comparison against `Named.original.0` for 1529 of 1545 aux constants (including plain stdlib like `Nat.casesOn`); a debug probe proved compile(original) == compile(regen) in every case, i.e. the regeneration itself was always faithful. With the invariant holding corpus-wide, the Phase-A recompile-hash mismatch is now a hard error with no aux exemption, and every roundtrip arm records failures in `aux_gen_errors` (recovery keeps the Lean-facing env populated for diagnosis but is never silent). Pass-2 scope hygiene: the below-def roundtrip loop filters by the original-gated `aux_members` like its sibling loops, so evaporated `below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now dumps hashed component scalars/hashes and runs an original-form recompile probe for any mismatch. Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry recomputation-honest flags so compile-side `validate_ind_flags` no longer poisons the shared tutorial env (73/335 -> 335/335, with the kernel rejecting each bad fixture as designed); validate-aux seeds match module-private fixture names via `privateToUserName?` and enable the Canonicity prefix; Phase 4b gains per-module markers so a fully absent identity group fails loudly when its fixture module is loaded (previously vacuous at 0 pass / 0 fail, now 109 pass). Gates: kernel-check-env 201296/201296; rust-compile all phases with 0 aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the full 213k env (live and deserialized); validate-aux 0 failures at 4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip 143694/0; kernel-tutorial 335/335; cargo test and lake test green.

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`: map_or over map+unwrap_or and slice::contains in surgery.rs, an enumerate loop for the motive-peeling walk in aux_motive_sigs, and let-chain collapses for the inductive-flags fixup loops in decompile.rs and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over from the previous commit.

Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).

Port of the two Rust kernel fixes on this branch: - Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand (computed_is_rec_ind), nested detection is structural (member_has_nested / ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten member-scoped without the declared nested count. Serialization packs one bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive addresses re-pinned. - collectDependencies (Ix/Common.lean) now closes over a declaration's full recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference in rule RHSs) plus each rule ctor's owning external recursor (List.rec). Without these the per-name compile either failed (MissingConstant AuxDedup1.C.rec from A.rec_1's block) or silently skipped the evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2 in original form, which the kernel rejects. AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join kernelCheckEntries; the four evaporated rec_N entries pin the identical 3_073_003 FFT cost (their claims are byte-exact List.rec: lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2). All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

…nment-machine WHNF reducer (#442) * kernel: uid identity, env-machine WHNF, and reduction-loop perf Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%. * kernel: native perf/shard examples (out-of-circuit tooling) Standalone cargo examples over a .ixe env, bypassing the Lean/FFI layer, updated to main's steps-based shard cost model (block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram): - shard_plan: profile → partition → .ixes manifest, with store-aware planning (--store-dir drops work items whose targets the proof store already covers, and excludes covered blocks from the partition hypergraph — a novel→covered edge is an assumption discharged at aggregation, not a cut to minimize); sizes N from machine RAM by default. - perf_check / check_one: native rerun of the guest check_const loop so IX_* perf-counter instrumentation can target a single expensive constant without re-checking its env. - heaviest_block / block_reduce_histo / shard_names / manifest_info: profiling forensics over blocks and manifests. * zisk+sp1: prover batch scripts and logs; bench-compile-init - zisk/scripts: prove-batch (sequential shard proving), mem-guard (MemAvailable watchdog that kills zisk-host before the OOM killer wedges the box), bench-cycles, mergesort-250k repro; reference logs. - sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with WITHOUT_VK_VERIFICATION=1). - Lean side: bench-compile-init lake exe (imports Init, empty main). * zisk: close aggregation soundness gaps (failures word, transitive vk pinning) The aggregate proof was weaker than "these subjects are well-typed": - The agg guest never read a child's committed failures word (slot 10) and hard-committed 0 for its own, so aggregation ERASED the failure bit — a kernel-rejected constant could appear under a failures=0 root, with only host-side courtesy checks in the way. Every child's failures word is now asserted 0 in-circuit. - vk pinning was not transitive: a child that is itself an aggregate was pinned only by its program vk (the shared AGG vk); its own allowed-vk set was never inspected. An agg-of-1 built against a rogue allowed set (wrapping an arbitrary program's "proof" with forged publics) would fold under an honest-looking root. The agg guest now requires every aggregate child (allowed-set index ≥ 1, by the new positional convention: index 0 = leaf vk, the rest agg vks) to commit THIS instance's vks id — the allowed set is uniform down the tree, so the pin is recursive. The convention's ordering is bound by the committed id hash, which external verifiers already check. - The host derived the allowed set FROM the untrusted child proofs (distinct_vks), so any proof admitted its own program, and a stale store folded silently under its old vk. The allowed set is now [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk after ROM setup); freshly produced proofs are asserted to match; stored proofs with a different vk are skipped (re-proven); and the root's committed vks id is checked against — and printed for — external verifiers. - A manifest bisection tree whose leaf set differs from the shard id set silently dropped proven leaves from the fold while the pre-aggregation coverage check (counting proofs PRODUCED, not folded) still passed. ShardManifest::from_bytes now rejects such trees, and the host additionally checks post-fold that every env target is in the root's actual subject set. * ixon: memoize deferred address verification (one hash per constant per load) The bench run on the rebase preview (06e1a1d) showed the whole-env ooc/InitStd row at +63.9% (10.96 s -> 17.97 s) while every per-constant row improved. Cause: LazyConstant::get() re-ran Address::hash(bytes) on every materialization, and the check loop re-ingresses each work item's closure after clear_releasing_memory() (IX_KERNEL_CHECK_CLEAR_EVERY=1), so each constant was re-hashed once per closure it appears in — inside the timed window. Pre-deferral the total was one hash per constant, at load time. Memoize the SUCCESSFUL check per entry (Arc<AtomicBool>, shared by clones, which share the bytes): the first get() still hash-checks before parsing; later get()s skip the hash. Failures are never memoized — bytes are immutable, so a mismatched entry re-fails on every call. This restores the one-hash-per-constant total while keeping load lazy. Also: unit tests for the deferred path (verify-once, failure never memoized, clones share the verdict), drop a dead 'let _ = i;' in get_anon, and note the memoization in docs/kernel_identity.md. * verify: make the pinned trust-frontier statements dischargeable ExecutionRequests' set/modifyGet constructors certified an arbitrary silent state transformation with an empty request list, so any program could be rewritten (funext + of_eq) as modifyGet-of-its-own-run bound into a pure/throw dispatch — ExecutionRequests x s [] held for every program, RunAssumptions was satisfiable with a support covering only the initial intern table, and the module docstring's central claim ("no constructor for an arbitrary silent computation") was false. Independently, the four headline statements universally quantified {semantics : CacheSemantics} — blockErrorsOnly is a lawful instance that invalidates every .expr cache insertion, refuting any run that warms a cache — and demanded the fixed support cover the POST-state intern table, refuting any run that interns. TcM.checkConst.wf was refutable outright; the other three were shielded only by the opaque StatementTrKExpr. set/modifyGet now carry intern-preservation hypotheses at the indexed state, and the new ExecutionRequests.intern_eq_of_nil proves the guarantee machine-checked: a []-certificate forces an unchanged intern table on both outcomes, so requests are an honest upper bound on a run's interning and the support quantifier matches the documented choose-final-support-up-front design. The statements pin an opaque StatementCacheSemantics stub (the K1 machinery is proved only for the whnfCacheSemantics family; arbitrary keys/fallbacks are refutable), so KernelRunInv no longer quantifies over semantics. Statement names and the four-sorry frontier are unchanged; NatFixture's satisfiability witnesses compile verbatim. * tc: mirror the kernel's Nat-offset machinery in the Lean spec The offset work landed Rust-side only, so spec and implementation disagreed on exactly the large-offset inputs it was built for: Rust strips a shared offset in one step, keeps 'Nat.add base (Lit n)' / 'Nat.div|mod base (Lit k)' stuck in compact form, and collapses symbolic-base linear Nat.rec to the compact offset, while Lean still peeled one succ per isDefEqCall level (maxRecDepth at k ≈ 2000, and succ-tower materialization in WHNF beyond 10k) and required a literal base for the linear-rec collapse. Port all three pieces: tryDefEqOffset decomposes both sides via natOffsetDecompose behind an O(1) natOffsetCandidate probe and strips the shared offset in one step (verdict-preserving by definitional +k injectivity); tryNatOffsetStuck freezes compact offset forms before delta at the same decision point as the Rust loop; and tryReduceNatSuccLinearRec gains the symbolic-base branch, gated on the recursor application carrying no post-major arguments. Verify ripple: the natRecLiteralParts totalization equation picks up majorIdx, and NatFixture's full-WHNF step walk certifies the offset-stuck probe returns none on the fixture for any primitive address assignment. Tests pin each piece against regressions: stays-compact under decoy Nat.add/div/mod definitions that delta would expose, the bulk strip at k = 2500 (one-succ peeling exceeds the def-eq depth limit there), div-derived vs add-derived stuck forms staying unequal, and the linear-rec collapse with its post-major conservatism. * tests: drop the tc-node-addr bit-parity harness Uid identity removed per-node content addresses from the Rust kernel, so the oracle dump's ty/extra columns became 16-hex intern uids — process-history-dependent values that can never byte-match the Lean side's Blake3 node addresses. The suite could only fail, and since ignored.yml runs 'lake test -- --ignored' on every push to main, it would turn Extended CI red on merge. The one column still comparable (the constant id) is read from the same serialized env bytes on both sides, so a slimmed comparison would check only traversal enumeration — coverage tc-anon-diff already provides against the real Rust verdicts. Remove the suite, its FFI oracle, and the extern binding; reword the Egress module doc that cited the harness as a level-reduction certifier. * kernel: allocate intern uids in thread-local blocks NEXT_UID was a single process-global cache line hit by a relaxed fetch_add for every node interned by every checker worker. The blake3 identity it replaced was pure per-worker work, so the old kernel scaled linearly with workers; the uid kernel is ~1.4x faster per core but its whole-env throughput plateaued near 5.7K consts/s as worker counts grew — the ooc InitStd !benchmark regression (9.96 s -> 16.97 s on the 32-thread bench runner, while every per-constant row improved; the same binaries tie at 24 local workers and the uid side wins 1.41x at 6). Hand out uids in per-thread blocks of 2^20 reserved from the global counter, touching the shared line once per block instead of once per node. Blocks are never reused (a thread's unspent remainder is abandoned on exit), so uid uniqueness and the never-reuse cache-key guarantee are unchanged; the exhaustion guard aborts a block early instead of one uid early. Local whole-env InitStd at 24 workers drops 15.58 s -> 11.04 s (old kernel: 15.49 s), and 6->24 worker scaling recovers from 1.60x to 2.02x. * bench: record tool faults as crash, not oom A 128+signal death was always recorded as an OOM row, so a zisk mem-planner segfault (exit 139) rendered as OOM and sent the investigation chasing RAM budgets instead of a heap-overflow bug. Split the kill statuses: explicit kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other signal death records status crash and renders as 💥 CRASH in the compare table. * kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2) The profiler counted whnf entries, def-eq entries, and limb-weighted Nat arithmetic per constant but dropped them at block aggregation, and nothing counted term-construction volume at all — leaving the shard cost model only heartbeats, subst, and bytes to predict guest steps from. Persist all four op counters per block (format v2) plus a new intern-table visit counter (a proxy for construction/memory traffic, bumped in intern_expr/intern_univ), and add a shard_features example that emits a per-shard feature CSV from a profile + manifest pair for calibrating the cost model against externally measured shard costs (ziskemu -X on dumped shard inputs). * zisk: dump every selected shard's input; skip ROM setup in dump mode --dump-input wrote only the first selected shard and exited, so dumping a 13-shard plan took 13 host invocations. Dump every selected shard in one run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard keeps the exact path), and skip client.setup when no proof store is involved — dump mode never runs the VM and needs the ROM setup (and thus the proving key) only to derive the shard vk for store filtering. * kernel: calibrate the shard planner in Zisk cost units Replace the heartbeat-based guest-STEP model with one denominated in ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES + BASE), so the packing target prices the axes that don't ride the main trace — DMA/blake3 precompile area and memory ops. Calibration corpus: 118 InitStd shards across 13 constants, each measured with ziskemu -X on inputs dumped via --dump-input. cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq + 28.4k*intern (+ 73.2k per cross-ingress byte) MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per work item, so intra-shard cache sharing is invisible to per-block features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram. On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on the uid-identity kernel; the intern term carries the memory-traffic/DMA axis (residual correlation 0.91 with dma_memcpy counts). Prover models refit on the same corpus. RAM comes from a guarded GPU prove sweep measured as each prover's systemd-scope cgroup memory.peak — the OOM-relevant metric CI's watchdog enforces, charging the whole process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost (was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s measured vs 411s predicted at the largest point). Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards (instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within the actual-cost ceiling; the only violations are the two INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB single-leaf), correctly flagged as not fitting the budget. * bench: per-constant ooc attribution and a compare top-movers drill-down A whole-env ooc regression previously surfaced as one env-keyed number, with drill-down only into the pre-chosen bench vectors. Now the anon whole-env check attributes itself: check-rs --per-const <csv> records one entry per work item (wall nanos, heartbeats, the op counters, and the predicted Zisk cost via the shard model) from the check loop, and the CLI joins Lean names from the env's named table (projection-name fallback for anonymized Muts blocks) so entries survive PRs that shift content addresses. An entry is ONE constant's (or Muts block's) own check — deps are lazily ingressed and trusted, each checked in its own entry, with the consulted closure slice's ingress charged to the entry — so entries sum to the env total with no double counting. NOT the full-closure scope of --consts measurements; documented at the recording site, the flag help, the renderer, and in the rendered output. The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to the results file (rotated with the local baseline), and ix bench compare renders a drill-down when both sides carry one, split by evidence quality — calibrated on a Mathlib A/A run (640K constants, twice through one binary): wall time swings up to 2.8s from scheduling alone, while the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9 absolute; worker->item assignment varies uid blocks and uid-keyed hash iteration order perturbs a few order-sensitive paths; --workers 1 is exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own cost OR >= 1e9 outright, both above the drift envelope) lead the drill-down ranked by percent change, styled like the main table ('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are quarantined in a labeled noise section capped at 5 rows. On the A/A run this renders 0 cost movers, the truthful reading. * bench: verdict-first cell layout; collapse tables past 5 rows A multi-cell !benchmark comment stacked every cell's full table; long cells (a 40-constant zisk table) buried the verdicts. Each cell now leads with its one-line verdict (and any typecheck failures / empty-side warnings, which stay unconditionally visible), and the comparison table collapses into a <details> block when it has more than 5 rows — small cells (the ooc env row, few-constant runs) stay inline. The per-constant and phase drill-downs were already collapsible. * ci: wire the ooc attribution CSV through the !benchmark pipeline bencher.dev stores metric rows only, so the per-constant drill-down needs the attribution CSVs to travel beside the results files. bench-main caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores the base SHA's entry, carries a base-run-produced CSV through the merge step (which previously renamed base.json into main.json and orphaned it), and pairs whichever CSV it has with the PR side's. The main side ends up with exactly two sources: bencher on FULL coverage (plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun for anything less — base SHA not uploaded, partial coverage, an ooc attribution cache miss, or the fresh token. A rerun measures the full default selection (a BENCH_CONSTS override still narrows it) and its rows take priority; bencher-fetched rows only fill rows the rerun failed to produce, and the table's main-source label says which path ran. This retires the gap-filling machinery (--consts from missing.txt, the bencher-priority merge arm) — a full rerun is simpler and self-consistent, at the cost of re-measuring a cell when a PR adds constants. * zisk: drop the vendored guest linker script Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the riscv64ima-zisk-zkvm-elf linker script in the target spec again, and passing the vendored copy on top double-defines the rom/ram memory regions. Both guest build scripts existed only to pass it — remove them and the script; the toolchain's embedded script is the single source of the memory layout. * zisk: pin the fork branch with the mem-planner fill_padding fix Bump every zisk fork pin from blake3-precompile (e4057c4) to blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows the mem-planner offsets array before fill_padding pads the last page — the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the shard that crashed 4/4 on the old pin executes clean on the new one (634M cycles, failures=0), as does the full 13-shard plan on the locally-patched build the fix was developed against. * chore: fix clippy lints (casts, qualifications, poison error, let-chain) u32::try_from over as-truncation and u64::from over as-widening in shard_features; drop redundant std::sync:: qualifications; carry the PoisonError text instead of discarding it; collapse the texray if into a let-chain; contains() over iter().any() in the holed-work filter. * chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build deliberately skips the guest compilation under clippy, but include_elf! still demanded the ELF bytes. Gate the embed (and its import) on cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes under clippy. Also collapse the texray if into a let-chain, matching the zisk host. A real release build of the host still works. * ci: clippy gates for the zisk and sp1 host workspaces The root rust-test clippy never enters the standalone zkVM workspaces, so their warnings accumulated ungated. Add cargo clippy --release --all-targets -D warnings to both host jobs, after the build so the release dep artifacts are shared (and, for zisk, the guest ELFs its build scripts already produced). * chore: String.dropEnd over deprecated String.dropRight * Unpin ziskup install * ci: align install-zisk comments with the unpinned toolchain * Clean up dev tooling and experiment artifacts for PR - Untrack sp1/zisk benchmark logs and scripts - Remove dev-tooling examples from ix-kernel: examples are for showing users how to use the crate; the shard-planning and perf binaries live on in git history - Remove the env-machine design doc; the as-built machine is documented at the code (whnf.rs machine_whnf, subst.rs Clo) --------- Co-authored-by: John C. Burnham <john@agathic.com>

johnchandlerburnham · 2026-07-04T06:34:29Z

Summary

Two related changes to the content-addressing layer and its aux-constant handling, fixing underlying issue reported in #465

1. Ixon no longer stores recr/refl/nested on Inductive. These are derivable
from constructor structure, so storing them was redundant and trusting declared values
was an adversarial surface (e.g. is_rec = false on a recursive inductive enables
improper struct-eta). The kernel now computes is_rec on demand, memoized in a new env
cache with a provisional entry to break the whnf → try_struct_eta_iota → is_struct_like
cycle; this replaces the declared-vs-computed check in check_inductive. The compile
side gains compute_lean_ind_flags to recompute Lean's block-wide
isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a
source Lean env (kernel egress, decompile), and validate_lean_ind_flags to check a
whole env against the recomputation.

2. Evaporated auxiliaries get a canonical form. When SCC splitting strands a nested
aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and
dropping the irrelevant over-merged motives leaves exactly the external inductive's
generic recursor. Canonical treatment: rec_N claims alias <Ext>.rec (e.g.
List.rec), call sites are rebuilt onto the external telescope via head-rewrite
CallSitePlans (owner-gated, single-motive targets), and below_N/brecOn_N compile as
surgered originals like _sizeOf_N. Fixes the AuxDedup kernel-check failures (28 → 0);
AuxDedup1 now generates auxiliaries identical to AuxDedup2's canonical structure.
Documented in docs/ix_canonicity.md §6.5.

Byte-exact aux roundtrip

roundtrip_block Phase A (recompile the regenerated Lean form, compare against the
stored original address) silently failed for 1529 of 1545 aux constants — including
plain stdlib like Nat.casesOn. Root cause: every production compile path preseeds the
ref/univ tables in sorted order (preseed_expr_tables) before compiling, and the
serialized constant embeds those tables; Phase A compiled without the preseed, filling
the tables in traversal order instead — every Ref/univ index permuted, byte-different
but semantically identical constants (decode resolves through the embedded table). A
debug probe recompiling the Lean original through the identical path proved
compile(original) == compile(regen) in every case: regeneration was always faithful,
the comparison context was not.

With the preseed mirrored in Phase A the invariant holds corpus-wide, so a Phase-A
recompile-hash mismatch is now a hard error with no aux exemption, and every
roundtrip arm records failures in aux_gen_errors (recovery keeps the Lean-facing env
populated for diagnosis but is never silent). Related hardening: call-site surgery
detection is durable across serialization (Named.original.is_some() alongside the
in-memory map), shift-aware instantiate_rev in the type-walking helpers (fixes fvar
leaks in .brecOn.go bodies), and the below-def roundtrip loop filters by the
original-gated members like its sibling loops. IX_ROUNDTRIP_DEBUG now dumps hashed
component summaries and runs an original-form recompile probe on any mismatch.

Test fixes and fixtures

kernel-tutorial: bad_raw_consts inductive fixtures carry recomputation-honest flags
so the whole-env validate_ind_flags no longer poisons the shared tutorial env
(73/335 → 335/335, with the kernel rejecting each bad fixture as designed).
validate-aux: seeds match module-private fixture names via privateToUserName?, the
Canonicity prefix is enabled, and Phase 4b gains per-module markers so a fully absent
identity group fails loudly when its fixture module is loaded (previously vacuous at
0 pass / 0 fail, now 109 pass / 0 fail).
New fixtures: AuxDedup1/AuxDedup2 (cross-block aux dedup), AuxDedupMixed (a perm
mixing a canonical slot and PERM_OUT_OF_SCC for the same owner), plus a
CompileMutualFixtures benchmark lib.

Gates

kernel-check-env: 201296/201296
rust-compile: all phases, 0 aux_gen errors / 0 mismatches / 0 Phase-A address
divergences on the full 213k env (live and deserialized)
validate-aux: 0 failures at 4393-constant scope
rust-serialize: byte-exact; kernel-ixon-roundtrip: 143694/0
kernel-tutorial: 335/335; cargo test workspace and lake test green;
cargo clippy --all-targets clean
lake exe ix check-rs compilemathlib.ixe: 736618/736618 passed, 0 failed (325.3s)
lake exe ix validate Benchmarks/Compile/CompileMathlib.lean: 0 failures (1528.33s total)

Remove the `recr`/`refl` bools and the `nested` count from the Ixon `Inductive` constant and its serialization (Rust and Lean), and from the `Indc` reveal-proof variant, renumbering the field-presence mask bits. These flags are derivable from constructor structure, so storing them was redundant and trusting declared values was an adversarial surface (e.g. is_rec = false on a recursive inductive enables improper struct-eta). - kernel: KConst::Indc loses is_rec/is_refl/nested. is_rec is now computed on demand (computed_is_rec), memoized in the new env is_rec_cache with a provisional entry to break the whnf -> try_struct_eta_iota -> is_struct_like cycle. This replaces the declared-vs-computed H1 verification in check_inductive. - compile: new compute_lean_ind_flags recomputes Lean's block-wide isRec/isReflexive/numNested wherever an InductiveVal is reconstructed without a source Lean env (kernel egress, decompile), since Ixon no longer stores the flags; validate_lean_ind_flags checks a whole env against the recomputation. - tests/benchmarks: add AuxDedup1/AuxDedup2 mutual fixtures exercising aux-constant dedup across blocks (fix forthcoming); add a CompileMutualFixtures benchmark lib building the mutual test fixtures; ignore *.ixe.

Evaporated auxiliaries (over-merge splits): when SCC splitting strands a nested aux's spec-param inductives outside the owner's SCC, no SCC holds the joint family, and dropping the irrelevant over-merged motives leaves exactly the external inductive's generic recursor. Canonical treatment: `rec_N` claims alias `<Ext>.rec` (e.g. `List.rec`), call sites are rebuilt onto the external telescope via head-rewrite CallSitePlans (owner-gated, single-motive targets), and `below_N`/`brecOn_N` compile as surgered originals like `_sizeOf_N`. Fixes the AuxDedup kernel-check failures (28 -> 0); AuxDedup1 now generates identical auxiliaries to AuxDedup2 (the canonical structure). New AuxDedupMixed fixture covers a perm mixing a canonical slot and PERM_OUT_OF_SCC for the same owner. Documented in docs/ix_canonicity.md 6.5. Call-site surgery guard is now durable across serialization: aux-regen detection accepts `Named.original.is_some()` in addition to the in-memory `aux_name_to_addr`, so deserialized-state roundtrip recompiles no longer misapply surgery. Shift-aware `instantiate_rev` replaces unshifted substitution in the type-walking helpers (fixes fvar leaks in `.brecOn.go` bodies). Byte-exact aux roundtrip: `roundtrip_block` Phase A now preseeds the ref/univ tables (`preseed_expr_tables`) like every production compile path. The serialized constant embeds those tables in sorted order; compiling without the preseed filled them in traversal order instead, permuting every `Ref`/univ index — byte-different but semantically identical constants (decode resolves through the embedded table). This silently failed the Phase-A address comparison against `Named.original.0` for 1529 of 1545 aux constants (including plain stdlib like `Nat.casesOn`); a debug probe proved compile(original) == compile(regen) in every case, i.e. the regeneration itself was always faithful. With the invariant holding corpus-wide, the Phase-A recompile-hash mismatch is now a hard error with no aux exemption, and every roundtrip arm records failures in `aux_gen_errors` (recovery keeps the Lean-facing env populated for diagnosis but is never silent). Pass-2 scope hygiene: the below-def roundtrip loop filters by the original-gated `aux_members` like its sibling loops, so evaporated `below_N` keep their faithful Pass-1 decompile. IX_ROUNDTRIP_DEBUG now dumps hashed component scalars/hashes and runs an original-form recompile probe for any mismatch. Test fixes: kernel-tutorial `bad_raw_consts` inductive fixtures carry recomputation-honest flags so compile-side `validate_ind_flags` no longer poisons the shared tutorial env (73/335 -> 335/335, with the kernel rejecting each bad fixture as designed); validate-aux seeds match module-private fixture names via `privateToUserName?` and enable the Canonicity prefix; Phase 4b gains per-module markers so a fully absent identity group fails loudly when its fixture module is loaded (previously vacuous at 0 pass / 0 fail, now 109 pass). Gates: kernel-check-env 201296/201296; rust-compile all phases with 0 aux_gen errors, 0 mismatches, and 0 Phase-A address divergences on the full 213k env (live and deserialized); validate-aux 0 failures at 4393-constant scope; rust-serialize byte-exact; kernel-ixon-roundtrip 143694/0; kernel-tutorial 335/335; cargo test and lake test green.

Behavior-neutral cleanups flagged by `cargo clippy --all-targets`: map_or over map+unwrap_or and slice::contains in surgery.rs, an enumerate loop for the motive-peeling walk in aux_motive_sigs, and let-chain collapses for the inductive-flags fixup loops in decompile.rs and kernel_egress.rs. Plus `cargo fmt` line-wrapping drift left over from the previous commit.

Three interlocking bugs in the Aiur block-flattening / recursor-type builder caused `ix check --interp bytecode Lean.Syntax.rec` to fail with `assert_eq mismatch: 0 != 1` on the declared-vs-canonical type equality: - `build_flat_block` traversed originals once; nested-aux members (`Array Syntax`, `List Syntax`) never had their own ctors scanned, so `flat` had 2 motives when Lean's recursor declares 3. Replaced with a queue-based fixed point mirroring `crates/kernel/src/inductive.rs: build_flat_block:531-599`. - `is_rec_field` classified any ctor field as recursive when its spine head Const-idx matched a flat member's ind idx. For `Lean.Syntax.ident`, the field `preresolved : List Preresolved` shares the base List const idx with the block's `List Lean.Syntax` aux and got a spurious `motive_2 preresolved` IH binder. Match key is now (head_idx, spine-arg prefix ≡ member.spec_params) — direct members carry `spec_params = []` and match on idx alone, auxes require the concrete occurrence. - `build_all_minors` was iterating `flat` and passing the shrinking suffix into `build_minor_doms`, so field classification for later members was blind to earlier members. Split into a wrapper + `build_all_minors_walk` that pins the caller's full flat while the iteration state shrinks. Pin `Lean.Syntax.rec` in the ixvm test suite; rebump every FFT cost shifted by the codegen refresh (`ix codegen`).

Port of the two Rust kernel fixes on this branch: - Ixon.Inductive drops recr/refl/nested (9 -> 6 fields); KConstantInfo.Induct drops is_rec/is_reflexive/nested (10 -> 7). is_rec is computed on demand (computed_is_rec_ind), nested detection is structural (member_has_nested / ind_has_nested over detect_nested_in_orig), is_aux_inductive is rewritten member-scoped without the declared nested count. Serialization packs one bool; reveal-proof Indc masks renumber to 6 fields; all 88 primitive addresses re-pinned. - collectDependencies (Ix/Common.lean) now closes over a declaration's full recursor family (sibling <ind>.rec + nested-aux rec_N, which cross-reference in rule RHSs) plus each rule ctor's owning external recursor (List.rec). Without these the per-name compile either failed (MissingConstant AuxDedup1.C.rec from A.rec_1's block) or silently skipped the evaporated-aux alias (target_ok probe misses List.rec), compiling M.rec_2 in original form, which the kernel rejects. AuxDedup1/2/Mixed fixtures from Tests/Ix/Compile/Mutual.lean join kernelCheckEntries; the four evaporated rec_N entries pin the identical 3_073_003 FFT cost (their claims are byte-exact List.rec: lake exe ix check --interp bytecode _private...AuxDedupMixed.M.rec_2). All stdlib pins re-measured via lake test -- --ignored ixvm (flag drop shrinks serialized inductives, e.g. HEq 1_713_377 -> 1_696_277).

Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%.

…nment-machine WHNF reducer (#442) * kernel: uid identity, env-machine WHNF, and reduction-loop perf Rebase of the sb/kernel-perf kernel stack onto main (the early workspace/backend/sharding commits of this branch were superseded by their evolved forms merged in #411/#503; this carries only the novel kernel work, reconciled with main's #473 declared-flag removal and is_rec_cache): - intern-assigned uids replace per-node blake3 content hashing: KExpr/ KUniv identity is a never-reused process-global u64; InternTable keys on shallow structural keys (variant tag + child uids + payload); cache keys cannot alias across intern-table clears (a stale key can only miss). ~20% of guest cycles on reduction-heavy constants came from content hashing (app_hash 22-33% cumulative). Design + collision analysis in docs/kernel_identity.md. - adversarial hardening of the uid design: fresh_uid aborts on counter exhaustion; literal structural-equality arms compare values as well as blob addresses; uid-accepting constructors privatized so a caller-supplied uid can never enter a node. - environment-machine WHNF (design in docs/env_machine_whnf.md): Phase A — whnf_core's App arm enters a Krivine-style machine when a beta fires; beta/zeta are O(1) environment pushes and substitution materializes only at machine exits (clo_subst readback), so a beta chain ending in another beta never materializes intermediate bodies. Phase B — closure-iota at the machine's recursor exit: only the major premise materializes on the main ctor-rule path; the rule RHS re-enters the machine with original closures, so unselected minors (dropped match/Decidable branches, the UTF-8 codec class) are never substituted and never read back. - memoized prim-family dispatch in the WHNF/def-eq reduction loops: classify each head once per iteration via an allocation-free app-chain walk + per-address memo (KEnv::prim_family_cache) instead of probing all five primitive recognizers per iteration. - compact symbolic Nat offsets: Nat.add base (Lit n) / Nat.div/mod base (Lit k) stay stuck in compact form (each keeps its own head, so offset def-eq cannot equate /- and +-derived forms); linear-rec collapse; offset-aware def-eq. - H-15 whnf probe pre-filter (allocation-free spine_head_and_len before the transient-nat probes) and H-12 output-size caps on native Nat arithmetic. - suffix-aware CtxAddr keys for the is_prop / nat_succ_stuck caches; NatSuccMode::Stuck whnf cache (proves ByteArray.utf8DecodeChar?_utf8EncodeChar_append). - ixon: per-constant address verification deferred to first materialization (LazyConstant::get checks pending_addr): constants shipped in a closure but never forced by the typechecker are never hashed; everything the kernel certifies is still verified when it is forced. Guest cycles: rbmap -9.5%, natgcdcomm -6.4%, stringappend -4.2%. * kernel: native perf/shard examples (out-of-circuit tooling) Standalone cargo examples over a .ixe env, bypassing the Lean/FFI layer, updated to main's steps-based shard cost model (block_step_cost / partition_for_cycle_cap / cycle_cap_for_ram): - shard_plan: profile → partition → .ixes manifest, with store-aware planning (--store-dir drops work items whose targets the proof store already covers, and excludes covered blocks from the partition hypergraph — a novel→covered edge is an assumption discharged at aggregation, not a cut to minimize); sizes N from machine RAM by default. - perf_check / check_one: native rerun of the guest check_const loop so IX_* perf-counter instrumentation can target a single expensive constant without re-checking its env. - heaviest_block / block_reduce_histo / shard_names / manifest_info: profiling forensics over blocks and manifests. * zisk+sp1: prover batch scripts and logs; bench-compile-init - zisk/scripts: prove-batch (sequential shard proving), mem-guard (MemAvailable watchdog that kills zisk-host before the OOM killer wedges the box), bench-cycles, mergesort-250k repro; reference logs. - sp1/scripts/prove-ix.sh + GPU logs (dev-only; runs with WITHOUT_VK_VERIFICATION=1). - Lean side: bench-compile-init lake exe (imports Init, empty main). * zisk: close aggregation soundness gaps (failures word, transitive vk pinning) The aggregate proof was weaker than "these subjects are well-typed": - The agg guest never read a child's committed failures word (slot 10) and hard-committed 0 for its own, so aggregation ERASED the failure bit — a kernel-rejected constant could appear under a failures=0 root, with only host-side courtesy checks in the way. Every child's failures word is now asserted 0 in-circuit. - vk pinning was not transitive: a child that is itself an aggregate was pinned only by its program vk (the shared AGG vk); its own allowed-vk set was never inspected. An agg-of-1 built against a rogue allowed set (wrapping an arbitrary program's "proof" with forged publics) would fold under an honest-looking root. The agg guest now requires every aggregate child (allowed-set index ≥ 1, by the new positional convention: index 0 = leaf vk, the rest agg vks) to commit THIS instance's vks id — the allowed set is uniform down the tree, so the pin is recursive. The convention's ordering is bound by the committed id hash, which external verifiers already check. - The host derived the allowed set FROM the untrusted child proofs (distinct_vks), so any proof admitted its own program, and a stale store folded silently under its old vk. The allowed set is now [shard_vk, agg_vk] derived from the embedded ELFs (GuestProgram::vk after ROM setup); freshly produced proofs are asserted to match; stored proofs with a different vk are skipped (re-proven); and the root's committed vks id is checked against — and printed for — external verifiers. - A manifest bisection tree whose leaf set differs from the shard id set silently dropped proven leaves from the fold while the pre-aggregation coverage check (counting proofs PRODUCED, not folded) still passed. ShardManifest::from_bytes now rejects such trees, and the host additionally checks post-fold that every env target is in the root's actual subject set. * ixon: memoize deferred address verification (one hash per constant per load) The bench run on the rebase preview (06e1a1d) showed the whole-env ooc/InitStd row at +63.9% (10.96 s -> 17.97 s) while every per-constant row improved. Cause: LazyConstant::get() re-ran Address::hash(bytes) on every materialization, and the check loop re-ingresses each work item's closure after clear_releasing_memory() (IX_KERNEL_CHECK_CLEAR_EVERY=1), so each constant was re-hashed once per closure it appears in — inside the timed window. Pre-deferral the total was one hash per constant, at load time. Memoize the SUCCESSFUL check per entry (Arc<AtomicBool>, shared by clones, which share the bytes): the first get() still hash-checks before parsing; later get()s skip the hash. Failures are never memoized — bytes are immutable, so a mismatched entry re-fails on every call. This restores the one-hash-per-constant total while keeping load lazy. Also: unit tests for the deferred path (verify-once, failure never memoized, clones share the verdict), drop a dead 'let _ = i;' in get_anon, and note the memoization in docs/kernel_identity.md. * verify: make the pinned trust-frontier statements dischargeable ExecutionRequests' set/modifyGet constructors certified an arbitrary silent state transformation with an empty request list, so any program could be rewritten (funext + of_eq) as modifyGet-of-its-own-run bound into a pure/throw dispatch — ExecutionRequests x s [] held for every program, RunAssumptions was satisfiable with a support covering only the initial intern table, and the module docstring's central claim ("no constructor for an arbitrary silent computation") was false. Independently, the four headline statements universally quantified {semantics : CacheSemantics} — blockErrorsOnly is a lawful instance that invalidates every .expr cache insertion, refuting any run that warms a cache — and demanded the fixed support cover the POST-state intern table, refuting any run that interns. TcM.checkConst.wf was refutable outright; the other three were shielded only by the opaque StatementTrKExpr. set/modifyGet now carry intern-preservation hypotheses at the indexed state, and the new ExecutionRequests.intern_eq_of_nil proves the guarantee machine-checked: a []-certificate forces an unchanged intern table on both outcomes, so requests are an honest upper bound on a run's interning and the support quantifier matches the documented choose-final-support-up-front design. The statements pin an opaque StatementCacheSemantics stub (the K1 machinery is proved only for the whnfCacheSemantics family; arbitrary keys/fallbacks are refutable), so KernelRunInv no longer quantifies over semantics. Statement names and the four-sorry frontier are unchanged; NatFixture's satisfiability witnesses compile verbatim. * tc: mirror the kernel's Nat-offset machinery in the Lean spec The offset work landed Rust-side only, so spec and implementation disagreed on exactly the large-offset inputs it was built for: Rust strips a shared offset in one step, keeps 'Nat.add base (Lit n)' / 'Nat.div|mod base (Lit k)' stuck in compact form, and collapses symbolic-base linear Nat.rec to the compact offset, while Lean still peeled one succ per isDefEqCall level (maxRecDepth at k ≈ 2000, and succ-tower materialization in WHNF beyond 10k) and required a literal base for the linear-rec collapse. Port all three pieces: tryDefEqOffset decomposes both sides via natOffsetDecompose behind an O(1) natOffsetCandidate probe and strips the shared offset in one step (verdict-preserving by definitional +k injectivity); tryNatOffsetStuck freezes compact offset forms before delta at the same decision point as the Rust loop; and tryReduceNatSuccLinearRec gains the symbolic-base branch, gated on the recursor application carrying no post-major arguments. Verify ripple: the natRecLiteralParts totalization equation picks up majorIdx, and NatFixture's full-WHNF step walk certifies the offset-stuck probe returns none on the fixture for any primitive address assignment. Tests pin each piece against regressions: stays-compact under decoy Nat.add/div/mod definitions that delta would expose, the bulk strip at k = 2500 (one-succ peeling exceeds the def-eq depth limit there), div-derived vs add-derived stuck forms staying unequal, and the linear-rec collapse with its post-major conservatism. * tests: drop the tc-node-addr bit-parity harness Uid identity removed per-node content addresses from the Rust kernel, so the oracle dump's ty/extra columns became 16-hex intern uids — process-history-dependent values that can never byte-match the Lean side's Blake3 node addresses. The suite could only fail, and since ignored.yml runs 'lake test -- --ignored' on every push to main, it would turn Extended CI red on merge. The one column still comparable (the constant id) is read from the same serialized env bytes on both sides, so a slimmed comparison would check only traversal enumeration — coverage tc-anon-diff already provides against the real Rust verdicts. Remove the suite, its FFI oracle, and the extern binding; reword the Egress module doc that cited the harness as a level-reduction certifier. * kernel: allocate intern uids in thread-local blocks NEXT_UID was a single process-global cache line hit by a relaxed fetch_add for every node interned by every checker worker. The blake3 identity it replaced was pure per-worker work, so the old kernel scaled linearly with workers; the uid kernel is ~1.4x faster per core but its whole-env throughput plateaued near 5.7K consts/s as worker counts grew — the ooc InitStd !benchmark regression (9.96 s -> 16.97 s on the 32-thread bench runner, while every per-constant row improved; the same binaries tie at 24 local workers and the uid side wins 1.41x at 6). Hand out uids in per-thread blocks of 2^20 reserved from the global counter, touching the shared line once per block instead of once per node. Blocks are never reused (a thread's unspent remainder is abandoned on exit), so uid uniqueness and the never-reuse cache-key guarantee are unchanged; the exhaustion guard aborts a block early instead of one uid early. Local whole-env InitStd at 24 workers drops 15.58 s -> 11.04 s (old kernel: 15.49 s), and 6->24 worker scaling recovers from 1.60x to 2.02x. * bench: record tool faults as crash, not oom A 128+signal death was always recorded as an OOM row, so a zisk mem-planner segfault (exit 139) rendered as OOM and sent the investigation chasing RAM budgets instead of a heap-overflow bug. Split the kill statuses: explicit kills (137 KILL, 143 TERM) and allocator aborts (134) stay oom; any other signal death records status crash and renders as 💥 CRASH in the compare table. * kernel: persist whnf/def_eq/nat_arith/intern per block (.ixprof v2) The profiler counted whnf entries, def-eq entries, and limb-weighted Nat arithmetic per constant but dropped them at block aggregation, and nothing counted term-construction volume at all — leaving the shard cost model only heartbeats, subst, and bytes to predict guest steps from. Persist all four op counters per block (format v2) plus a new intern-table visit counter (a proxy for construction/memory traffic, bumped in intern_expr/intern_univ), and add a shard_features example that emits a per-shard feature CSV from a profile + manifest pair for calibrating the cost model against externally measured shard costs (ziskemu -X on dumped shard inputs). * zisk: dump every selected shard's input; skip ROM setup in dump mode --dump-input wrote only the first selected shard and exited, so dumping a 13-shard plan took 13 host invocations. Dump every selected shard in one run (multi-shard plans write <stem>-s<manifest index><ext>; --only-shard keeps the exact path), and skip client.setup when no proof store is involved — dump mode never runs the VM and needs the ROM setup (and thus the proving key) only to derive the shard vk for store filtering. * kernel: calibrate the shard planner in Zisk cost units Replace the heartbeat-based guest-STEP model with one denominated in ziskemu cost units (-X TOTAL: MAIN + OPCODES + MEMORY + PRECOMPILES + BASE), so the packing target prices the axes that don't ride the main trace — DMA/blake3 precompile area and memory ops. Calibration corpus: 118 InitStd shards across 13 constants, each measured with ziskemu -X on inputs dumped via --dump-input. cost = 293.6M + 196.6k*subst + 1.798M*whnf + 567.1k*def_eq + 28.4k*intern (+ 73.2k per cross-ingress byte) MAPE 10.9%, worst under-prediction -33% (the profiler runs cold-cache per work item, so intra-shard cache sharing is invisible to per-block features); COST_MODEL_HEADROOM = 1.5 covers it inside cycle_cap_for_ram. On this corpus cost/step is ~92.5 +/- 7% — blake3 is 0.6-2.4% of cost on the uid-identity kernel; the intern term carries the memory-traffic/DMA axis (residual correlation 0.91 with dma_memcpy counts). Prover models refit on the same corpus. RAM comes from a guarded GPU prove sweep measured as each prover's systemd-scope cgroup memory.peak — the OOM-relevant metric CI's watchdog enforces, charging the whole process tree plus the ASM trace shm (a VmRSS-summed sweep reads 2-8 GiB low with the gap growing with cost): peak RAM 33.1 + 0.2845 GiB/B-cost (was 50 + 33 per B-step), leaf prove time 29s + 2.25s/B-cost (419s measured vs 411s predicted at the largest point). Validation at --max-ram 108: the corpus re-plans 118 -> 55 shards (instRxcHasSize_eq 13 -> 6), every packable shard's measured cost within the actual-cost ceiling; the only violations are the two INFEASIBLE-flagged atomic monster blocks (~310 B-cost = ~121 GiB single-leaf), correctly flagged as not fitting the budget. * bench: per-constant ooc attribution and a compare top-movers drill-down A whole-env ooc regression previously surfaced as one env-keyed number, with drill-down only into the pre-chosen bench vectors. Now the anon whole-env check attributes itself: check-rs --per-const <csv> records one entry per work item (wall nanos, heartbeats, the op counters, and the predicted Zisk cost via the shard model) from the check loop, and the CLI joins Lean names from the env's named table (projection-name fallback for anonymized Muts blocks) so entries survive PRs that shift content addresses. An entry is ONE constant's (or Muts block's) own check — deps are lazily ingressed and trusted, each checked in its own entry, with the consulted closure slice's ingress charged to the entry — so entries sum to the env total with no double counting. NOT the full-closure scope of --consts measurements; documented at the recording site, the flag help, the renderer, and in the rendered output. The ooc bench cell writes the CSV as a <rows>.perconst.csv file next to the results file (rotated with the local baseline), and ix bench compare renders a drill-down when both sides carry one, split by evidence quality — calibrated on a Mathlib A/A run (640K constants, twice through one binary): wall time swings up to 2.8s from scheduling alone, while the op counters drift only on a 0.7% tail (up to ~13% relative / 0.27e9 absolute; worker->item assignment varies uid blocks and uid-keyed hash iteration order perturbs a few order-sensitive paths; --workers 1 is exactly reproducible). Cost movers (|Dcost| >= 15% of the constant's own cost OR >= 1e9 outright, both above the drift envelope) lead the drill-down ranked by percent change, styled like the main table ('+95.5% (1.96x more)', warning/green emoji); cost-flat time movers are quarantined in a labeled noise section capped at 5 rows. On the A/A run this renders 0 cost movers, the truthful reading. * bench: verdict-first cell layout; collapse tables past 5 rows A multi-cell !benchmark comment stacked every cell's full table; long cells (a 40-constant zisk table) buried the verdicts. Each cell now leads with its one-line verdict (and any typecheck failures / empty-side warnings, which stay unconditionally visible), and the comparison table collapses into a <details> block when it has more than 5 rows — small cells (the ooc env row, few-constant runs) stay inline. The per-constant and phase drill-downs were already collapsible. * ci: wire the ooc attribution CSV through the !benchmark pipeline bencher.dev stores metric rows only, so the per-constant drill-down needs the attribution CSVs to travel beside the results files. bench-main caches the ooc cell's CSV by (SHA, cell) after its run; bench-pr restores the base SHA's entry, carries a base-run-produced CSV through the merge step (which previously renamed base.json into main.json and orphaned it), and pairs whichever CSV it has with the PR side's. The main side ends up with exactly two sources: bencher on FULL coverage (plus, for ooc, a cached attribution CSV), or a full local base-SHA rerun for anything less — base SHA not uploaded, partial coverage, an ooc attribution cache miss, or the fresh token. A rerun measures the full default selection (a BENCH_CONSTS override still narrows it) and its rows take priority; bencher-fetched rows only fill rows the rerun failed to produce, and the table's main-source label says which path ran. This retires the gap-filling machinery (--consts from missing.txt, the bencher-priority merge arm) — a full rerun is simpler and self-consistent, at the cost of re-measuring a cell when a PR adds constants. * zisk: drop the vendored guest linker script Current zisk toolchains (1.0.0-alpha builds from 2026-07 on) embed the riscv64ima-zisk-zkvm-elf linker script in the target spec again, and passing the vendored copy on top double-defines the rom/ram memory regions. Both guest build scripts existed only to pass it — remove them and the script; the toolchain's embedded script is the single source of the memory layout. * zisk: pin the fork branch with the mem-planner fill_padding fix Bump every zisk fork pin from blake3-precompile (e4057c4) to blake3-precompile-1.0.0-alpha (f376d85d), whose one commit on top grows the mem-planner offsets array before fill_padding pads the last page — the heap overflow behind the WAIT_PLAN_MEM_CPP hang + SIGSEGV that the bench recorded as instRxcHasSize_eq's phantom OOM. Validated here: the shard that crashed 4/4 on the old pin executes clean on the new one (634M cycles, failures=0), as does the full 13-shard plan on the locally-patched build the fix was developed against. * chore: fix clippy lints (casts, qualifications, poison error, let-chain) u32::try_from over as-truncation and u64::from over as-widening in shard_features; drop redundant std::sync:: qualifications; carry the PoisonError text instead of discarding it; collapse the texray if into a let-chain; contains() over iter().any() in the holed-work filter. * chore: sp1-host clippy — cfg-gate the ELF embed, collapse the texray if cargo clippy in the sp1 workspace failed on a clean checkout: sp1-build deliberately skips the guest compilation under clippy, but include_elf! still demanded the ELF bytes. Gate the embed (and its import) on cfg(not(clippy)) with an empty Elf::Static stand-in — nothing executes under clippy. Also collapse the texray if into a let-chain, matching the zisk host. A real release build of the host still works. * ci: clippy gates for the zisk and sp1 host workspaces The root rust-test clippy never enters the standalone zkVM workspaces, so their warnings accumulated ungated. Add cargo clippy --release --all-targets -D warnings to both host jobs, after the build so the release dep artifacts are shared (and, for zisk, the guest ELFs its build scripts already produced). * chore: String.dropEnd over deprecated String.dropRight * Unpin ziskup install * ci: align install-zisk comments with the unpinned toolchain * Clean up dev tooling and experiment artifacts for PR - Untrack sp1/zisk benchmark logs and scripts - Remove dev-tooling examples from ix-kernel: examples are for showing users how to use the crate; the shard-planning and perf binaries live on in git history - Remove the env-machine design doc; the as-built machine is documented at the code (whnf.rs machine_whnf, subst.rs Clo) --------- Co-authored-by: John C. Burnham <john@agathic.com>

johnchandlerburnham added 3 commits July 4, 2026 02:20

johnchandlerburnham requested a review from arthurpaulino July 4, 2026 06:35

arthurpaulino added 2 commits July 4, 2026 09:55

johnchandlerburnham mentioned this pull request Jul 5, 2026
Ixon: .ixe bundle format and diff tool #474
Merged

arthurpaulino mentioned this pull request Jul 6, 2026
Aiur kernel: fix Lean.Syntax.rec (shard 53) + ix name-of#464
Closed
5 tasks

arthurpaulino approved these changes Jul 7, 2026
View reviewed changes

gabriel-barrett approved these changes Jul 7, 2026
View reviewed changes

johnchandlerburnham merged commit 547455e into mainJul 7, 2026
15 of 16 checks passed

johnchandlerburnham deleted the jcb/compiler branch July 7, 2026 23:12

johnchandlerburnham added 3 commits July 4, 2026 02:20

johnchandlerburnham requested a review from arthurpaulino July 4, 2026 06:35

arthurpaulino added 2 commits July 4, 2026 09:55

johnchandlerburnham mentioned this pull request Jul 5, 2026
Ixon: .ixe bundle format and diff tool #474
Merged

arthurpaulino mentioned this pull request Jul 6, 2026
Aiur kernel: fix Lean.Syntax.rec (shard 53) + ix name-of#464
Closed
5 tasks

arthurpaulino approved these changes Jul 7, 2026
View reviewed changes

gabriel-barrett approved these changes Jul 7, 2026
View reviewed changes

johnchandlerburnham merged commit 547455e into mainJul 7, 2026
15 of 16 checks passed

johnchandlerburnham deleted the jcb/compiler branch July 7, 2026 23:12

johnchandlerburnham added 3 commits July 4, 2026 02:20

johnchandlerburnham requested a review from arthurpaulino July 4, 2026 06:35

arthurpaulino added 2 commits July 4, 2026 09:55

johnchandlerburnham mentioned this pull request Jul 5, 2026
Ixon: .ixe bundle format and diff tool #474
Merged

arthurpaulino mentioned this pull request Jul 6, 2026
Aiur kernel: fix Lean.Syntax.rec (shard 53) + ix name-of#464
Closed
5 tasks

arthurpaulino approved these changes Jul 7, 2026
View reviewed changes

gabriel-barrett approved these changes Jul 7, 2026
View reviewed changes

johnchandlerburnham merged commit 547455e into mainJul 7, 2026
15 of 16 checks passed

johnchandlerburnham deleted the jcb/compiler branch July 7, 2026 23:12

johnchandlerburnham added 3 commits July 4, 2026 02:20

johnchandlerburnham requested a review from arthurpaulino July 4, 2026 06:35

arthurpaulino added 2 commits July 4, 2026 09:55

johnchandlerburnham mentioned this pull request Jul 5, 2026
Ixon: .ixe bundle format and diff tool #474
Merged

arthurpaulino mentioned this pull request Jul 6, 2026
Aiur kernel: fix Lean.Syntax.rec (shard 53) + ix name-of#464
Closed
5 tasks

arthurpaulino approved these changes Jul 7, 2026
View reviewed changes

gabriel-barrett approved these changes Jul 7, 2026
View reviewed changes

johnchandlerburnham merged commit 547455e into mainJul 7, 2026
15 of 16 checks passed

johnchandlerburnham deleted the jcb/compiler branch July 7, 2026 23:12

johnchandlerburnham added 3 commits July 4, 2026 02:20

johnchandlerburnham requested a review from arthurpaulino July 4, 2026 06:35

arthurpaulino added 2 commits July 4, 2026 09:55

johnchandlerburnham mentioned this pull request Jul 5, 2026
Ixon: .ixe bundle format and diff tool #474
Merged

arthurpaulino mentioned this pull request Jul 6, 2026
Aiur kernel: fix Lean.Syntax.rec (shard 53) + ix name-of#464
Closed
5 tasks

arthurpaulino approved these changes Jul 7, 2026
View reviewed changes

gabriel-barrett approved these changes Jul 7, 2026
View reviewed changes

johnchandlerburnham merged commit 547455e into mainJul 7, 2026
15 of 16 checks passed

johnchandlerburnham deleted the jcb/compiler branch July 7, 2026 23:12

johnchandlerburnham added 3 commits July 4, 2026 02:20

johnchandlerburnham requested a review from arthurpaulino July 4, 2026 06:35

arthurpaulino added 2 commits July 4, 2026 09:55

johnchandlerburnham mentioned this pull request Jul 5, 2026
Ixon: .ixe bundle format and diff tool #474
Merged

arthurpaulino mentioned this pull request Jul 6, 2026
Aiur kernel: fix Lean.Syntax.rec (shard 53) + ix name-of#464
Closed
5 tasks

arthurpaulino approved these changes Jul 7, 2026
View reviewed changes

gabriel-barrett approved these changes Jul 7, 2026
View reviewed changes

johnchandlerburnham merged commit 547455e into mainJul 7, 2026
15 of 16 checks passed

johnchandlerburnham deleted the jcb/compiler branch July 7, 2026 23:12

johnchandlerburnham added 3 commits July 4, 2026 02:20

johnchandlerburnham requested a review from arthurpaulino July 4, 2026 06:35

arthurpaulino added 2 commits July 4, 2026 09:55

johnchandlerburnham mentioned this pull request Jul 5, 2026
Ixon: .ixe bundle format and diff tool #474
Merged

arthurpaulino mentioned this pull request Jul 6, 2026
Aiur kernel: fix Lean.Syntax.rec (shard 53) + ix name-of#464
Closed
5 tasks

arthurpaulino approved these changes Jul 7, 2026
View reviewed changes

gabriel-barrett approved these changes Jul 7, 2026
View reviewed changes

johnchandlerburnham merged commit 547455e into mainJul 7, 2026
15 of 16 checks passed

johnchandlerburnham deleted the jcb/compiler branch July 7, 2026 23:12

johnchandlerburnham added 3 commits July 4, 2026 02:20

johnchandlerburnham requested a review from arthurpaulino July 4, 2026 06:35

arthurpaulino added 2 commits July 4, 2026 09:55

johnchandlerburnham mentioned this pull request Jul 5, 2026
Ixon: .ixe bundle format and diff tool #474
Merged

arthurpaulino mentioned this pull request Jul 6, 2026
Aiur kernel: fix Lean.Syntax.rec (shard 53) + ix name-of#464
Closed
5 tasks

arthurpaulino approved these changes Jul 7, 2026
View reviewed changes

gabriel-barrett approved these changes Jul 7, 2026
View reviewed changes

johnchandlerburnham merged commit 547455e into mainJul 7, 2026
15 of 16 checks passed

johnchandlerburnham deleted the jcb/compiler branch July 7, 2026 23:12

Uh oh!

Conversation

johnchandlerburnham commented Jul 4, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Byte-exact aux roundtrip

Test fixes and fixtures

Gates

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

johnchandlerburnham commented Jul 4, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Byte-exact aux roundtrip

Test fixes and fixtures

Gates

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

johnchandlerburnham commented Jul 4, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Byte-exact aux roundtrip

Test fixes and fixtures

Gates

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

johnchandlerburnham commented Jul 4, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Byte-exact aux roundtrip

Test fixes and fixtures

Gates

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

johnchandlerburnham commented Jul 4, 2026• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Byte-exact aux roundtrip

Test fixes and fixtures

Gates

johnchandlerburnham commented Jul 4, 2026•
edited
Loading

johnchandlerburnham commented Jul 4, 2026•
edited
Loading

johnchandlerburnham commented Jul 4, 2026•
edited
Loading

johnchandlerburnham commented Jul 4, 2026•
edited
Loading

johnchandlerburnham commented Jul 4, 2026•
edited
Loading

johnchandlerburnham commented Jul 4, 2026•
edited
Loading

johnchandlerburnham commented Jul 4, 2026•
edited
Loading