Uh oh!
There was an error while loading. Please reload this page.
feat: add initial Lean code - #1
Merged
Merged
Conversation
johnchandlerburnham added a commit
that referenced
this pull request
May 21, 2026
* Refactor Claim ADT + add merkle infrastructure for ZK aggregation
Adds the format hooks needed before recursive verification lands in
Aiur. Five-variant Claim ADT with explicit assumption commitments, a
canonical Blake3 merkle module, a serializable AssumptionTree for
recovering leaf sets, and a Contains claim for the discharge step.
Claim ADT (5 variants):
- Eval { input, output, assumptions: Option<Address> }
- Check { const_addr, assumptions: Option<Address> }
- CheckEnv { root, assumptions: Option<Address> }
- Reveal { comm, info } -- unchanged, no assumptions
- Contains { tree, const_addr } -- new, for inclusion proofs
Tag4 reorganized to keep everything in single-byte tags:
- 0xE for env, comm, AssumptionTree, and claims (slots 0-7)
- 0xF for proofs (slots 0-4; 5-7 reserved)
- Comm moved from variant 5 -> 1
Matches the "Variant (0-7)" constraint documented in docs/Ixon.md.
Env serialization:
- Every .ixe file now carries a canonical merkle root over its
consts.keys() in the on-disk header (non-optional, 32 bytes;
empty const sets use the zero-address sentinel).
- Two envs with the same const set produce byte-identical roots
regardless of insertion order. Verified on deserialize.
New modules:
- src/ix/ixon/merkle.rs + Ix/Merkle.lean: canonical sorted builder,
free-form merkle_join composition, membership proofs, domain
separation per RFC 6962.
- src/ix/ixon/assumption_tree.rs + Ix/AssumptionTree.lean: serializable
merkle tree with Leaf/Padding/Node variants. canonical() builds the
same shape merkle_root_canonical hashes; join() is O(1) free-form
composition.
- src/ix/kernel/claim.rs: builders that compute transitive-dep
assumptions from an env (build_check_claim, build_eval_claim,
build_check_env_claim, env_merkle_root).
Other:
- Extracted shared BFS walker on Env::bfs_refs +
Env::transitive_deps_excl; the inlined test-feature copy in
lean_env.rs now calls into it.
- Lean FFI export rs_env_merkle_root for cross-impl verification of
the env root.
- Proof bytes for all variants are uniform opaque ZK bytes; witness
data (e.g., Contains merkle paths) is prover-side scratch consumed
by the ZK circuit and not transmitted on the wire.
- docs/Ixon.md Tag4 tables and env section updated; .ixe extension
documented.
Recursive verification (the ZK proof generation for Contains and the
aggregation discharge transitions) is intentionally deferred to a
follow-up.
Tests: 993 Rust unit tests pass (was 953 pre-refactor), 813 Lean tests
pass with no failures; cargo clippy clean.
* Add lazy env deserialization and anon-mode kernel FFI
Two related changes to reduce kernel memory + lay groundwork for
metadata-isolated typechecking.
**Lazy constant deserialization.** `Env::consts` now stores
`LazyConstant` (`Arc<[u8]>` + `OnceLock<Arc<Constant>>`) instead of
`Constant`. Constants are materialized on first access and the
structured form is cached. Sparse access patterns (single-constant
typecheck, transitive_deps walk, claim builders) only parse the
closure they need; non-reachable constants stay as raw bytes.
The `.ixe` section-2 layout gains a Tag0 length sidecar before each
constant's Tag4 bytes:
old: [addr:32] [Tag4 constant bytes]
new: [addr:32] [Tag0 length] [Tag4 constant bytes]
The length is section-level framing, not part of the constant's
content hash. `Address::hash(raw_bytes) == addr` is preserved.
`Constant::put`/`Constant::get` are unchanged. The Lean side
(`Ix.Ixon.putEnv`/`getEnv`) reads/writes the new format.
**Anon-mode kernel FFI.** New `rs_kernel_check_consts_anon(path,
addrs, quiet)` exposes anonymous-mode typechecking by content
address. The kernel runs as `KEnv<Anon>` / `TypeChecker<Anon>` with
every `M::MField<T>` erased to `()`, so the typechecking logic
structurally cannot read metadata. Useful for zkPCC verifiers that
hold only addresses.
Supporting pieces:
- `KernelMode::HAS_META: bool` for future compile-time gating.
- `AnonEnv<'a>` wrapper (`src/ix/kernel/anon_env.rs`) exposing only
consts/blobs/transitive walks — no `named`/`names`/`comms`.
- `Env::get_anon` reads header + blobs + consts, parse-and-drops
metadata sections (3-5), returns an `Env` with empty `named`/
`names`/`comms`. Same merkle-root verification as `Env::get`.
- `rs_de_env_anon` FFI + `Ix.Ixon.rsDeEnvAnon` Lean wrapper.
- `Ix.KernelCheck.rsCheckConstsAnonFFI` Lean binding.
Caveat: `ixon_ingress::<Anon>` still consults `Env::named` internally
to enumerate work items. The resulting `KEnv<Anon>` is metadata-free
so the typechecker is anon, but full ingress-level metadata
isolation is a follow-up.
Tests: 16 new (9 lazy + sparsity; 3 AnonEnv; 4 get_anon). All 1009
Rust unit tests pass; all 813 Lean tests pass; clippy clean.
* Simplify ix check + add metadata-free anon mode
- `ix check` becomes .ixe-only with a positional `<path>`. Drops the
`--lean` compile-and-check flow and the `--env` flag; direct
Lean → kernel checks remain available through `rsCheckConstsFFI`
for tests. Removes the redundant `CheckIxonCmd.lean`.
- New `--anon` flag runs a metadata-free kernel check: loads the .ixe
via `Env::get_anon` (discards named/names/comms), enumerates work
items from `env.consts` alone, and rebuilds member + ctor projection
addresses deterministically via `Constant::commit`. Rejects
`--consts`/`--ns`/`--consts-file` since it always checks everything.
- Compiler: unwrap singleton non-inductive Muts blocks to standalone
Defn/Recr. `Expr::Rec(0, univs)` already resolves correctly against
a one-member block, so the wrapper was pure overhead; this keeps the
env structurally uniform and matches `compile_single_def`. The anon
ingress for standalones passes `mut_ctx_override = [self_id]` so
self-recursive standalones still typecheck.
- Kernel: anon parallel runner mirrors `run_checks_parallel_on_large
_stacks` (32 workers, slow-detection, RSS tracking). Genericized
`check_one_const<M>` / `check_consts_loop<M>` / `format_tc_error<M>`
to share the runner. `KernelMode::meta_field_with` / `meta_field_try`
gate metadata lookups in expression ingress at compile time.
- Anon lazy ingress (`LazyAnonIngress` in tc.rs, helpers in ingress.rs)
dedupes blocks via `kenv.blocks.contains_key(&KId<Anon>(B, ()))`
before re-running `ingress_anon_block` (prevents N² re-ingestion
when sibling projections fault separately within one worker check).
- `Env::get_anon` now harvests `ReducibilityHints` from the
otherwise-discarded Named section into a sidecar
`Env::anon_hints: FxHashMap<Address, ReducibilityHints>`. Anon
ingress threads these through a new `hints_override` parameter on
`ingress_defn` so the lazy-delta tiebreak in `def_eq::def_rank_id`
sees realistic heights instead of `Regular(0)`. Hints are
performance advice, not correctness data — supplying them in anon
mode preserves the metadata-free trust model.
- Regenerate the canonical addresses in `PrimAddrs::new()`; singleton-
unwrap changed the content hash of every self-recursive primitive
(Nat.add, String, Nat.rec, …).
End-to-end on compileinitstd.ixe (105,487 constants):
meta: 105487/105487 in 20.6s, peak RSS 7.4GB
anon: 89010/89010 in 17.8s, peak RSS 4.0GB
* Clean up cargo clippy --all-targets
- 11× `cloned_ref_to_slice_refs`: `&[x.clone()]` → `std::slice::from_ref(&x)`
in `assumption_tree.rs` + `merkle.rs` test modules. Same allocator
footprint, no clone, matches the lint's recommended idiom.
- 2× `useless_vec`: `vec![0xE3, 0x00, 0x00]` → `[0xE3, 0x00, 0x00]`
in serde-reject tests where the buffer is only borrowed.
All 1011 unit tests pass. `cargo clippy --all-targets` is now clean.
* ix check: print full content hashes + add --workers flag
- The anon-mode progress / failure-log labels and the meta-mode
hash-display fallback were truncating addresses to 16 hex chars
(`@1f4b195aefa10e26`). Drop the `[..16]` slice so the full 64-char
Blake3 hex is printed (`@1f4b195aefa10e2690d13c5b98b3d9124d3fbb5c…`),
matching what tooling like `--fail-out` records and what the
metadata-free workflow actually needs to identify a constant.
- `--workers N` flag on `ix check` plumbs through the existing
`IX_KERNEL_CHECK_WORKERS` env var that `resolve_kernel_check_workers`
in `src/ffi/kernel.rs` reads. Useful for isolating per-worker memory
cost (`--workers 1` lets you see the env's static footprint without
per-worker overhead) and for capping concurrency in resource-tight
contexts.
* Mmap .ixe + cache-free LazyConstant for anon mode
`lake exe ix check compilemathlib.ixe --anon` on a 3.2 GB env now
peaks at ~11 GB RSS, down from ~40 GB; build_anon_work is 50× faster.
Three intertwined changes:
1. Memory-map the .ixe (avoids ~3.2 GB heap copy of bytes)
- Cargo: add memmap2 = "0.9".
- `BytesSource` enum in `src/ix/ixon/lazy.rs` distinguishes
heap-resident `Arc<[u8]>` from `(Arc<Mmap>, offset, len)` windows
into a memory-mapped file. `LazyConstant::raw_bytes`,
`verify_address`, `PartialEq` route through `BytesSource::as_slice`
so every existing consumer is mmap-transparent.
- `Env::get_anon_mmap(path)` in `src/ix/ixon/serialize.rs` opens
the file, mmaps it, and stores Section-2 consts as mmap-backed
`LazyConstant`s. Sections 3-4 (names + named) are still parsed
transiently to harvest hints, then dropped before return.
- `rs_kernel_check_anon` (`src/ffi/kernel.rs`) switches to
`get_anon_mmap`; the old `std::fs::read` + `Env::get_anon` heap
path is gone for the anon FFI.
2. Strip the persistent `LazyConstant` parsed-Constant cache
- `LazyConstant.cache` was `Arc<OnceLock<Arc<Constant>>>` and
accumulated forever — for mathlib that meant ~30 GB of parsed
`Arc<Expr>` trees pinned in the env across the entire run.
- New shape: `cache: Option<Arc<Constant>>`. Populated only by
`from_constant` (compile-side, where we already own the parsed
value). `from_bytes`/`from_mmap_slice` set `None`, and their
`get()` parses fresh on every call without storing.
- Re-parse cost is bounded by the existing per-worker dedup:
`kenv.consts` already addresses each ingressed constant once
per work item, and `clear_releasing_memory()` drops the kenv
between items. The kenv is now the only persistent
materialization layer.
3. `LazyConstant::peek_variant` for `build_anon_work`
- One-byte read of the outer Tag4 head to identify the
`ConstantInfo` variant — no body parse, no allocation.
- `build_anon_work` now dispatches on `peek_variant()`; only
`Muts` blocks trigger `lc.get()` (we need the member list for
projection-address enumeration), and that `Arc<Constant>` drops
at the end of the match arm.
- Previously every constant was fully materialized at startup
just to read its variant tag. With ~95% of the env being
standalone/projection, the work-enumeration pass now skims the
env at near-IO speed.
Test updates:
- `mmap_slice_roundtrips` (already added with the earlier mmap
scaffolding) exercises the mmap window roundtrip.
- New `from_bytes_does_not_cache` and `from_constant_clones_share_cache`
document the new caching contract.
- `peek_variant_*` tests cover every variant + empty-bytes and
unknown-flag error paths.
- `lazy_sparsity_only_materializes_closure` in `src/ix/ixon/env.rs`
reframed to assert BFS-of-closure correctness instead of cache
side-effects (`is_materialized()` no longer fires for lazy loads).
End-to-end on compilemathlib.ixe (--anon, 32 workers):
before: 640658/640658 in 266s, peak RSS ~40 GB
after: 640658/640658 in 223s, peak RSS 11.3 GB
* Address review findings: correctness + small refactors
Code-review pass over the anon-mode / mmap / cache-strip work. This
commit lands the highest-value subset — the correctness fixes and the
small refactors that prevent future drift — and leaves the larger
items (format-version bump, sealed marker trait, AnonEnv audit) for
separate follow-ups.
Correctness:
- Verify per-constant address on load (#1). `LazyConstant::verify_address`
existed but was never invoked from `Env::get`, `get_anon`, or
`get_anon_mmap`. The env-level merkle root catches missing/extra
entries but not byte-tampering of a constant whose key is intact;
without this check, corruption surfaced much later inside
`LazyConstant::get` with a misleading parse error. Inline the
`Address::hash(bytes) == addr` check in each loader's Section-2 loop.
Added 3 corruption-detection tests (`env_const_bytes_tampering_*`).
This required updating a handful of existing tests that stored
constants under fake `Address::hash(b"a")` keys instead of their
true content hashes — round-tripping such envs now correctly
rejects. Added a `store_canonical(env, c) -> Address` test helper
for the canonical pattern, and `*_discriminator(refs, n)` so tests
can produce content-distinct constants when the same ref-set would
otherwise collide.
- Hard-error in `ixon_env_to_decoded` on parse failure (#6).
`src/ffi/ixon/env.rs` used `filter_map` to silently drop any const
whose bytes failed `LazyConstant::get` — the Lean caller had no
signal of the lost entries. Switch to a Result-collecting loop and
propagate the first parse error; update both FFI call sites
(`rs_de_env`, `rs_de_env_anon`).
- Doc fixes (#4, #5). `docs/Ixon.md`'s AssumptionTree section
described only `Leaf=0x00` and `Node=0x01`, missing `Padding=0x01`
(and the docs' `Node` tag collided with the real `Padding` tag —
the real `Node` is `0x02`). Also: the env-section table cell said
"opt-tagged merkle root" but the implementation writes a bare
32-byte address.
Refactors that prevent future drift:
- Canonical projection-address helpers (#9). Four production sites
reconstructed `Constant::new(IxonCI::{D,I,R,C}Prj{...}).commit().0`
by hand; the anon pipeline silently breaks if any one drifts.
Extract `defn_proj_address` / `indc_proj_address` /
`recr_proj_address` / `ctor_proj_address` (plus `_constant`
variants) in `src/ix/ixon/constant.rs`. Update `compile.rs`,
`compile/mutual.rs`, and the anon `*_proj_addr` helpers to call
them.
- `verify_proj_addr_in_env` helper (#21). `ingress_anon_block` had
the same "computed-address not in env" check repeated four times
(DPrj/RPrj/IPrj/CPrj). DRY into one helper that produces a
consistent error format.
UX:
- Anon display labels switched to `#<hex>` everywhere (#18). Rust
was emitting `@<hex>` in progress/fail-out; Lean's `runCheckAnon`
was emitting `#{i}` (result index). Standardize on `#<hex>` so
the CLI failure summary is joinable with the fail-out file.
This required exposing addresses per result slot to Lean —
`rsCheckAnonFFI` now returns `Array (String × Option CheckError)`
pairing each result with its content-address hex string. Rust
builds the pairs via a new `build_anon_result_array` helper.
- Stale "check-ixon" header in FailureLog (#16). One-line rename in
the doc comment + `# ix check-ixon failures` writeln to `# ix
check failures`.
Tests:
- `testPrimitivesParity` (PrimAddrs regen-parity test). Catches
silent drift between hardcoded primitive addresses in
`PrimAddrs::new()` and what `rsCompileEnvFFI` produces from the
live Lean primitives. Plumbing: new `PrimAddrs::lean_parity_table()`
returns `(lean_name, hex)` pairs; new `rs_prim_addrs_canonical`
FFI exposes them to Lean; new test in `BuildPrimitives.lean`
iterates `kernelPrimitives`, compares against the hardcoded
table, and fails with a printable diff on mismatch (with
instructions to regenerate).
Skipped: `eagerReduce` — synthetic kernel marker whose
PrimAddrs value (`0xff…3`) intentionally diverges from its
compiled content hash (which collides with `id`).
- 3 new corruption-detection tests in `serialize.rs` exercise the
Section-2 verify check for `Env::get`, `Env::get_anon`,
`Env::get_anon_mmap`.
Verification: `cargo test --lib` 1025 passing (3 new), `cargo clippy
--lib --all-targets` clean, `lake build` clean, `lake exe ix check
compileinitstd.ixe` 105487/105487 in ~21s, `--anon` 89010/89010 with
peak RSS 1.4 GB, `.lake/build/bin/IxTests --ignored
rust-kernel-build-primitives` shows both `build primitives dump` and
`primitive address parity (PrimAddrs vs live compile)` pass.
Out of scope (deferred to follow-ups):
- #2 Format version bump (Env::FLAG)
- #3 rs_kernel_check_consts_anon still uses Env::get on main
- #8 Sealed marker trait for the lazy_anon transmute
- #11/#12 AnonEnv audit (vestigial wrapper)
- #13, #15, #17, #19, #20, #22-25 Various quality cleanups
* Round-2 review fixes: mmap defense + small cleanup
Six small items from the round-2 review of the anon-mode work:
- N1: stat-at-open defense in `Env::get_anon_mmap`
(`src/ix/ixon/serialize.rs`). Capture the file size before mmap;
if the kernel's mapped length disagrees (file truncated between
open and map) bail with a clear error instead of letting workers
SIGBUS deep in `LazyConstant::get`. Truncate-in-place under a live
mapping is still undefined per POSIX — documented as a caller
contract — but the open-time check catches the common case.
- New `get_anon_mmap_survives_file_unlink` test: load via mmap,
unlink the path, then materialize both already-touched and
not-yet-touched constants. Locks in the inode-retention invariant
that the SIGBUS analysis depends on; a future refactor that
switched to `mmap_anonymous` or copied bytes into a tmpfile would
fail loudly here instead of letting workers SIGBUS in production.
- #11: delete `AnonEnv::as_ixon_env_unchecked`
(`src/ix/kernel/anon_env.rs`). Dead `pub(crate)` escape hatch
marked `#[allow(dead_code)]` — confirmed zero callers and removed.
- #13: `debug_assert!` on `OnceLock::set` for both result vectors
(`src/ffi/kernel.rs`, meta + anon paths). The previous
`let _ = results[idx].set(...)` silently dropped a re-set. If a
future `build_*_work` dedup refactor breaks the
one-write-per-slot invariant, debug builds now panic with the
slot index instead of silently losing results.
- #19: `allNames.contains` O(n²) preflight → `Std.HashSet` lookup
(`Ix/Cli/CheckCmd.lean`). At mathlib scale (~700k env names ×
thousands of seed names) the previous linear scan-per-name spent
measurable seconds on missing-name preflight alone.
- N4: doc imprecision in `src/ix/ixon/lazy.rs` — the cache-policy
preamble said the worker `KEnv` is "cleared between work items"
but the actual cadence is `clear_every` items
(`IX_KERNEL_CHECK_CLEAR_EVERY`, default 1 but tunable). Refined
wording so the doc matches the code.
Verification: `cargo test --lib` 1026 passing (1 new), `cargo
clippy --lib --all-targets` clean, `lake build` clean,
`lake exe ix check compileinitstd.ixe --anon` 89010/89010 in 15.2s
peak RSS 1.4 GB (regression-clean).
Out of scope, separate follow-ups:
- #2 Format version bump
- #3 rs_kernel_check_consts_anon zkPCC FFI (Env::get → mmap)
- #8 Sealed marker trait for the lazy_anon transmute
- #10 child_arena closure side-effect (widen MField to tuple)
- #12 AnonEnv duplicates bfs_refs / transitive_deps_excl
- #14 anon worker bypasses M-generic display helpers
- #17 Anon --fail-out docstring claims --consts-file compat
- #20 Singleton-unwrap duplicated across compile paths
- #22-24 Lean `partial def`, `.get!` in tests, unguarded as-u64 casts
- N2/N3 Lean is_materialized() callers + compute_const_size_breakdown
- Test gaps: rs_kernel_check_anon integration, concurrent mmap,
verify_address-on-mmap-corruption, etc.
* rustfmt
* Tests: derive RawConst addrs from content (verify_address fix)
The `Address::hash(bytes) == addr` defense added in f792102 rejects
`RawConst { addr, const }` pairs where `addr` is uncorrelated with
`serConstant const`. The Rust-side tests in `serialize.rs` were
updated at the time (`store_canonical` helper), but three Lean-side
sites still produced mismatched pairs and surface now as:
× ∃: Env serialization Lean==Rust
× ∃: serde RawEnv with data
× ∃: serde RawEnv roundtrip
deserialization failed: rs_de_env: Env::get: const at idx 0
bytes hash to 6110b739… but stored under b177ec1b…
Three fixes, all derive `addr := Address.blake3 (serConstant c)`:
- `Tests/Gen/Ixon.lean::genRawConst` — property-test generator was
`RawConst.mk <$> genAddress <*> genConstant` (uncorrelated). Now
generates the const first, then derives addr from `serConstant`.
- `Tests/FFI/Lifecycle.lean::serdeTests` (`withData` unit case) —
was using one `testAddr := Address.blake3 #[1,2,3]` for both the
const and unrelated blob/comm slots. Split into `testAddr` (still
used for the content-hash-free blob/comm) and
`testConstAddr := Address.blake3 (serConstant testConst)`. Added
a name entry for the new canonical addr.
- `Tests/FFI/Lifecycle.lean::genSerdeRawEnv` — the "pool of
addresses" pattern picked const addrs from a random pool that
couldn't possibly match content hashes. Restructured: consts
derive canonical addrs from content, each gets its own name-table
entry appended to the pool-derived entries so the serde
pipeline's "all addresses resolvable" invariant still holds.
* Regenerate Aiur primitive addresses for singleton-unwrap
Compiler's singleton non-inductive Muts unwrap (12630aa) changed the
content hashes of 48 primitives (`Nat.rec`, `Nat.add`, `Nat.mul`, …).
The Aiur kernel's `Ix/IxVM/Kernel/Primitive.lean` still held the
pre-unwrap blake3 bytes, so primitive dispatch missed every affected
constant and fell through to structural `Nat.rec` unfolding. Tests
like `IxVMPrim.nat_mul_big` then drove millions of Nat.succ
unfoldings inside the Aiur trace, OOMing the prover.
Addresses regenerated from `PrimAddrs::lean_parity_table()` (which
the branch had already updated in `src/ix/kernel/primitive.rs`).
* Fix standalone Recr ingress: typ-based inductive lookup
`find_matching_block_addr` heuristic in the standalone-Recr branch of
`build_convert_inputs_walk` picks the inductive block by matching ctor
count to rule count. When multiple in-scope inductives share the same
ctor count, it returns the wrong block — the stored rules' `ctor_idx`
then points to a sibling's ctor, while `populate_rules` (canonical)
derives `ctor_idx` from the right inductive's `ctor_indices`. The
mismatch surfaces as `compare_rules`'s `assert_eq!(s_ctor, c_ctor)`
panic (e.g. `38 != 40` for `IxVMPrim.nat_land_lit`).
Switch the standalone-Recr path to the same typ-based resolution
`build_aux_recr_ctor_idxs` already uses for aux Recr blocks: peel
`params + motives + minors + indices` foralls of `recr.typ`, take the
major's head Ref, look it up in `refs` to get the inductive's address,
then resolve `IPrj.block` for the Muts wrapper. Slice ctor positions
for the specific member via `extract_member_ctor_idxs`.
Also store the resolved Muts `block_addr` in `CKRecr` (was passing the
heuristic's wrong address through to `convert_recursor`).
---------
Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com>
Co-authored-by: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com>arthurpaulino added a commit
that referenced
this pull request
Jul 2, 2026
plumbing, unchecked cache-hit array copy
Three targeted cuts to the generated kernel (`src/ix/aiur_ixvm.rs`);
all preserve QueryRecord parity (shard 26 FFT cost unchanged at
107_006_963_281).
Every `U8*` op previously emitted a `Vec<G>` scratch (~245 sites):
let __b2_out: [G; 1] = {
let mut __scratch: Vec<G> = vec![__v_i, __v_j];
if unconstrained { __scratch.extend(vec![Bytes2::xor(...)]); }
else { bytes2_execute(0, 1, &Bytes2Op::Xor, &mut __scratch, record); }
let __arr: [G; 1] = __scratch[2..].try_into().unwrap();
__arr
};
Net cost: a 2-element `vec![]` alloc + a `__scratch.extend(vec![..])`
(another small alloc inside `Bytes2::execute`'s returned Vec) + a
slice→array `try_into().unwrap()`.
Added per-op `bytes{1,2}_*_value(args..., record) -> G | (G,G) | (G,G,G) |
[G; 8]` in `src/aiur/execute.rs` — each bumps the corresponding
`bytes{1,2}_queries.bump_*` and returns the gadget output by value.
The pure (`Bytes{1,2}::*`) helpers stay the unconstrained shortcut.
Codegen now emits:
let __v_n: G = if unconstrained { Bytes2::xor(&__v_i, &__v_j) }
else { bytes2_xor_value(__v_i, __v_j, record) };
Zero `Vec<G>` allocation per byte op. `U8Add`/`U8Sub` also gain
because `bytes2_add_value` runs the `Bytes2::add` gadget once
(returning the full `(low, carry)`) instead of the interpreter's
two `Bytes2::add` calls (one for the carry, one for the low push).
To make `bump_*` callable from `execute.rs`, all `Bytes1Queries` /
`Bytes2Queries::bump_*` methods are now `pub(crate)`. No behaviour
change.
The `Op::Call` cache-check emitted `unconstrained || OP_UN` and
`!unconstrained && !OP_UN` even when the static `OP_UN` was `false`,
which is the common case. Codegen now emits the folded shape
directly:
let __cu = unconstrained; // was: unconstrained || false
if !unconstrained { *result.multiplicity += G::ONE; }
// was: !unconstrained && !false
When `OP_UN == true`, the callee always runs unconstrained AND the
multiplicity bump is always suppressed; codegen folds to `let __cu =
true;` and elides the bump branch entirely.
LLVM was already folding these, so this is mostly source-cleanliness
and a small frontend win.
The cache-hit branch read `result.output` (an `&[G]`) and converted
it back to `[G; OUT_N]` via `.try_into().unwrap()`. The length is
statically `OUT_N` — we control the producer (the matching
`aiur_fn_{callee}::Ctrl::Return` inserts an `[G; OUT_N]`-typed array
into the same slot). The runtime bounds-check + Result discharge is
dead work.
Codegen now emits:
let __ret: [G; OUT_N] = unsafe {
*(result.output.as_ptr() as *const [G; OUT_N])
};
Sound: same-fn slot, fixed `OUT_N`, no aliasing.
| Variant | mean |
| --- | --: |
| Rust witness (parallel) + codegen | 80 s |
| + value-helper byte ops (#1) | 64 s |
| + folded `__cu` + unsafe cache copy (#2+#3) | 62 s |
The bulk of the win is #1 (#1 alone: ~−18%). #2+#3 are a further
~3% — mostly noise / Rust-frontend cleanup since LLVM already folds
the constant `false` ops.
* `src/aiur/execute.rs`: 12 value-returning byte helpers added
(`bytes1_bit_decompose_value`, `bytes1_shift_left_value`,
`bytes1_shift_right_value`, `bytes2_{xor,and,or,less_than,mul,
chain_rotr7,chain_rotr4,add,sub}_value`).
* `src/aiur/gadgets/bytes1.rs`, `src/aiur/gadgets/bytes2.rs`: all
`bump_*` upgraded to `pub(crate)` so the value helpers can call
them.
* `Ix/Aiur/Stages/Codegen.lean`: `emitU8Bytes1` / `emitU8Bytes2` /
`emitU8Add` / `emitU8Sub` rewritten to call the per-op value
helpers — no scratch Vec, no slice→array conversion. `emitCall`
constant-folds `opUn = false` and emits the unsafe cache-hit
copy. Prelude imports updated to bring the new helpers into
scope.
* `src/ix/aiur_ixvm.rs`: regenerated. 245 `Vec<G>` scratch sites
→ 11 (only `unconstrainedBigUintDivMod`'s scratch left); 3324
`unconstrained || false` → 0; 3000+ `result.output.try_into()
.unwrap()` → 0.
* `Ix/Cli/CheckCmd.lean`: incidental cleanup of probe-only timing
prints in `runShardOwnedNative` (added during measurement, no
longer needed).arthurpaulino added a commit
that referenced
this pull request
Jul 3, 2026
* Aiur Bytecode → Rust codegen for the IxVM kernel
Adds a new Aiur pipeline stage that translates `Bytecode.Toplevel`
into a Rust source module, one `fn aiur_fn_N` per Aiur function.
The generated code mirrors `src/aiur/execute.rs`'s QueryRecord
side effects exactly: same `function_queries.insert` timing, same
cache-hit multiplicity bumps, same memory-queries insertion order,
same `bytes{1,2}_queries` updates, same IO sequencing. Per-witness
trace hashes match the interpreter byte-for-byte on every const
tested (`Nat.add_comm`, `Vector.append`,
`Std.Time.Week.Offset.ofMilliseconds`).
* `Ix/Aiur/Stages/Codegen.lean`: structured Rust IR (`RustExpr` /
`RustStmt` / `RustItem` / `MatchArm` / labeled blocks) plus a
formatter. Codegen is a structural walk over the Bytecode AST,
no string templating. `EmitM = StateM EmitState` threads
`(nextVal, nextLabel)` so per-ValIdx Rust locals and per-MC
labels are fresh.
* Aiur's `map: Vec<G>` is gone in the generated kernel: every
ValIdx becomes a Rust local `__v_{i}: G`. Match-arm bodies snapshot
`nextVal` on entry so per-arm allocations don't leak to siblings.
`MatchContinue` / `Yield` use labeled-block + `break 'label
[G; OUT_SIZE]` to bubble yielded values out and rebind them at
outer scope.
* Deep Aiur recursion uses `stacker::maybe_grow(64 KiB, 4 MiB, …)`
at the top of every generated fn, so the native call stack grows
on demand rather than pre-reserving a giant thread stack. Verified
against shard 24 of the 64-way `init.ixes` partition, which
SEGFAULTs without it.
* `ix codegen`: new CLI command. Compiles the IxVM Aiur source,
walks the bytecode, writes the generated Rust to a fixed path
(`src/ix/aiur_ixvm.rs`). The output path is hard-coded; no
override.
* `src/ix/aiur_ixvm.rs`: the generated kernel, 743 `aiur_fn_*`
+ `execute_generated` dispatch. Auto-regenerated; do not edit.
`#![cfg_attr(rustfmt, rustfmt::skip)]` + a broad
`#![allow(unused_*, non_snake_case, clippy::all)]` since the
layout is for the compiler, not humans.
* `src/ix/aiur_ixvm_runner.rs`: `execute_ixvm(toplevel, fun_idx,
args, io_buffer) -> Result<(QueryRecord, Vec<G>), ExecError>`.
Same return shape as `Toplevel::execute`, but routes through
`execute_generated`.
* `src/aiur/synthesis.rs`: `AiurSystem::prove_ixvm(...)` —
same shape as `prove`, but the execute step calls
`execute_ixvm`. Verification-compatible (proofs from one path
verify under the other).
* `src/aiur/execute.rs`: helpers exposed for the codegen'd kernel
(`bytes{1,2}_execute` → `pub(crate)`,
`unconstrained_big_uint_div_mod_helper` extracted,
`CodegenBytes{1,2}{Op,}` aliases re-exported,
`QueryRecord::new` → `pub(crate)`, `ExecError::InvalidFunIdx`
added).
* `src/ffi/aiur/protocol.rs`: two new FFI exports —
`rs_aiur_toplevel_execute_ixvm` and `rs_aiur_system_prove_ixvm`.
Same wire format as the existing `_execute` / `prove` exports.
* `Ix/Aiur/Semantics/BytecodeFfi.lean`:
`Bytecode.Toplevel.executeIxVM` — mirror of `execute`.
* `Ix/Aiur/Protocol.lean`: `AiurSystem.proveIxVM`.
* `Ix/Cli/CheckCmd.lean`: `runCompiled` now dispatches through
`executeIxVM`. The Rust bytecode interpreter is no longer
reachable from `ix check` (the Lean-side `--interp` fallback
stays for richer error diagnostics).
* `Ix/Cli/ProveCmd.lean`: `proveOne` uses `proveIxVM`.
* `Cargo.toml`: `stacker = "0.1"`.
For witnesses where execute is the dominant work (single-const
checks via `ix check 'X'`), the codegen'd kernel is ~1.6× faster
than the bytecode interpreter end-to-end (measured on
`Nat.add_comm`, `Vector.append`,
`Std.Time.Week.Offset.ofMilliseconds`). Tiny consts are within
~10% (stacker probe overhead amortises). Peak RSS is within a few
MB of the interpreter — stacker grows the stack on demand, no
giant upfront reservation.
For shard-driven `ix check --shard K` runs the speedup is
invisible: per-shard wall time is dominated (~92%) by
`buildShardCheckEnvWitness` in Lean, NOT by the kernel execute
(~8%). Cutting witness construction is the next lever.
`Nat.add_comm` proof produced via `proveIxVM` verifies under the
existing `AiurSystem::verify`. End-to-end:
lake exe ix prove 'Nat.add_comm' → proof addr 0d0ab0f9…
lake exe ix verify 0d0ab0f9… → ok
* Move shard witness construction to Rust + parallelise
Replaces `IxVM.ClaimHarness.buildShardCheckEnvWitness` (Lean side,
~92% of shard wall time on heavy partitions) with a Rust port that
builds the `aiur::execute::IOBuffer` directly, without per-byte
boxing into Lean `Aiur.G` values. The two hot phases run on rayon:
* Closure walk: each owned addr's transitive `Constant.refs` +
projection-block traversal runs on its own thread; results are
deduped through a `dashmap::DashSet`.
* Byte-to-G conversion: per-const `(key, data)` tuples are built
in parallel chunks of 256; final IOBuffer assembly (channel arena
append + key→`IOKeyInfo` map insert) runs serially because the
arena index is monotonic.
* `src/ix/aiur_ixvm_witness.rs` (new): `build_shard_check_env_witness`
produces `(claim, claim_digest_input, io_buffer)` ready to feed
to `execute_ixvm`. Mirrors the 6-channel layout documented in
`Ix/IxVM/ClaimHarness.lean` (claim / asm tree / const bytes /
Defn hint / blob discriminator / blob raw bytes).
* `src/ffi/aiur/protocol.rs`: new FFI `rs_aiur_toplevel_shard_check_ixvm`
bundles witness build + `execute_ixvm` into one cross-language
trip. Returns the same `(output, ioBuffer, queryCounts)` shape
as `rs_aiur_toplevel_execute_ixvm`, so the Lean shim stays
drop-in compatible.
* `Ix/Aiur/Semantics/BytecodeFfi.lean`:
`Bytecode.Toplevel.shardCheckIxVM` wraps the FFI.
* `Ix/Cli/CheckCmd.lean`: shard-mode `ix check` (`--ixe + --ixes`)
now dispatches through `runShardOwnedNative` →
`shardCheckIxVM`, bypassing the Lean witness builder. Single-
shard and whole-partition paths share the fast route; the
legacy `runShardCheckManifest` / `runShardCheckAll` callbacks
stay live for `--interp` only.
Shard 26 of the 64-way `init.ixes` partition, on the same host:
| Variant | total | speedup |
| --- | --: | --: |
| Lean witness + bytecode-interp (baseline)| 1029 s | 1.0× |
| Lean witness + codegen kernel | 1015 s | 1.01× |
| Rust witness (serial) + codegen | 101 s | 9.95× |
| Rust witness (parallel) + codegen | 80 s | 12.9× |
The serial Rust witness collapses the 935 s of Lean per-byte boxing
into ~23 s; rayon hides that 23 s under the codegen-kernel execute
(~78 s) so witness build effectively becomes free at the shard
level.
FFT cost matches the bytecode interpreter exactly
(107_006_963_281), so the QueryRecord layout is bit-identical
across all four variants.
* Closure walk uses single-source BFS with the global visited set
shared via `DashSet::contains` checks before pushing to the
per-thread stack — avoids redundant work without a per-owned
union step.
* Per-channel ordering: each chunk's partial `ChannelEntries`
feeds the serial fold in iteration order, so channel arena
contents match the Lean side's exactly. Test still relies on
trace-hash parity from the earlier codegen commit, which
exercised the same path through the bytecode interpreter and
the codegen kernel.
* Coverage check is currently skipped on the IxVM-native
whole-partition path (`runShardManifestAllNative`); legacy
`runShardCheckAll` still does it for `--interp`. Re-enable
separately if needed.
* Codegen: value-returning byte ops, dead-fold the unconstrained
plumbing, unchecked cache-hit array copy
Three targeted cuts to the generated kernel (`src/ix/aiur_ixvm.rs`);
all preserve QueryRecord parity (shard 26 FFT cost unchanged at
107_006_963_281).
Every `U8*` op previously emitted a `Vec<G>` scratch (~245 sites):
let __b2_out: [G; 1] = {
let mut __scratch: Vec<G> = vec![__v_i, __v_j];
if unconstrained { __scratch.extend(vec![Bytes2::xor(...)]); }
else { bytes2_execute(0, 1, &Bytes2Op::Xor, &mut __scratch, record); }
let __arr: [G; 1] = __scratch[2..].try_into().unwrap();
__arr
};
Net cost: a 2-element `vec![]` alloc + a `__scratch.extend(vec![..])`
(another small alloc inside `Bytes2::execute`'s returned Vec) + a
slice→array `try_into().unwrap()`.
Added per-op `bytes{1,2}_*_value(args..., record) -> G | (G,G) | (G,G,G) |
[G; 8]` in `src/aiur/execute.rs` — each bumps the corresponding
`bytes{1,2}_queries.bump_*` and returns the gadget output by value.
The pure (`Bytes{1,2}::*`) helpers stay the unconstrained shortcut.
Codegen now emits:
let __v_n: G = if unconstrained { Bytes2::xor(&__v_i, &__v_j) }
else { bytes2_xor_value(__v_i, __v_j, record) };
Zero `Vec<G>` allocation per byte op. `U8Add`/`U8Sub` also gain
because `bytes2_add_value` runs the `Bytes2::add` gadget once
(returning the full `(low, carry)`) instead of the interpreter's
two `Bytes2::add` calls (one for the carry, one for the low push).
To make `bump_*` callable from `execute.rs`, all `Bytes1Queries` /
`Bytes2Queries::bump_*` methods are now `pub(crate)`. No behaviour
change.
The `Op::Call` cache-check emitted `unconstrained || OP_UN` and
`!unconstrained && !OP_UN` even when the static `OP_UN` was `false`,
which is the common case. Codegen now emits the folded shape
directly:
let __cu = unconstrained; // was: unconstrained || false
if !unconstrained { *result.multiplicity += G::ONE; }
// was: !unconstrained && !false
When `OP_UN == true`, the callee always runs unconstrained AND the
multiplicity bump is always suppressed; codegen folds to `let __cu =
true;` and elides the bump branch entirely.
LLVM was already folding these, so this is mostly source-cleanliness
and a small frontend win.
The cache-hit branch read `result.output` (an `&[G]`) and converted
it back to `[G; OUT_N]` via `.try_into().unwrap()`. The length is
statically `OUT_N` — we control the producer (the matching
`aiur_fn_{callee}::Ctrl::Return` inserts an `[G; OUT_N]`-typed array
into the same slot). The runtime bounds-check + Result discharge is
dead work.
Codegen now emits:
let __ret: [G; OUT_N] = unsafe {
*(result.output.as_ptr() as *const [G; OUT_N])
};
Sound: same-fn slot, fixed `OUT_N`, no aliasing.
| Variant | mean |
| --- | --: |
| Rust witness (parallel) + codegen | 80 s |
| + value-helper byte ops (#1) | 64 s |
| + folded `__cu` + unsafe cache copy (#2+#3) | 62 s |
The bulk of the win is #1 (#1 alone: ~−18%). #2+#3 are a further
~3% — mostly noise / Rust-frontend cleanup since LLVM already folds
the constant `false` ops.
* `src/aiur/execute.rs`: 12 value-returning byte helpers added
(`bytes1_bit_decompose_value`, `bytes1_shift_left_value`,
`bytes1_shift_right_value`, `bytes2_{xor,and,or,less_than,mul,
chain_rotr7,chain_rotr4,add,sub}_value`).
* `src/aiur/gadgets/bytes1.rs`, `src/aiur/gadgets/bytes2.rs`: all
`bump_*` upgraded to `pub(crate)` so the value helpers can call
them.
* `Ix/Aiur/Stages/Codegen.lean`: `emitU8Bytes1` / `emitU8Bytes2` /
`emitU8Add` / `emitU8Sub` rewritten to call the per-op value
helpers — no scratch Vec, no slice→array conversion. `emitCall`
constant-folds `opUn = false` and emits the unsafe cache-hit
copy. Prelude imports updated to bring the new helpers into
scope.
* `src/ix/aiur_ixvm.rs`: regenerated. 245 `Vec<G>` scratch sites
→ 11 (only `unconstrainedBigUintDivMod`'s scratch left); 3324
`unconstrained || false` → 0; 3000+ `result.output.try_into()
.unwrap()` → 0.
* `Ix/Cli/CheckCmd.lean`: incidental cleanup of probe-only timing
prints in `runShardOwnedNative` (added during measurement, no
longer needed).
* Wire Rust witness fast path through every check/prove entry point
Per-claim mode (a `Claim.check addr none`) builds a closure rooted at
the target address. That closure can be the whole environment when
the target is a heavily-shared root constant. The Lean witness
builder paid per-byte boxing into `Aiur.G` for every byte in that
closure — the same cost we already eliminated for shard mode.
# Surface
Five new FFIs, all bundling witness build + execute_ixvm (and STARK
prove where applicable) into one cross-language trip so the
`IOBuffer` never crosses the boundary mid-pipeline:
* `rs_aiur_toplevel_check_addr_ixvm` —
`Bytecode.Toplevel.checkAddrIxVM (toplevel) (funIdx) (ixePath) (addrBytes)`:
per-claim check; builds witness for `Claim.check addr none` via
`build_claim_check_witness`, runs `execute_ixvm`. Same return
shape as `shardCheckIxVM`.
* `rs_aiur_toplevel_check_env_bytes_ixvm` — same as above but takes
the env as a serialized byte blob (`Ixon.serEnv`) instead of a
`.ixe` path. Used by the compiled-Lean-env code path (`ix check
NAME` without `--ixe`), where the env is built in Lean memory.
* `rs_aiur_system_prove_addr_ixvm` —
`AiurSystem.proveAddrIxVM (...)`: per-claim prove
(witness + execute + STARK prove all in Rust).
* `rs_aiur_system_prove_env_bytes_ixvm` — bytes-blob counterpart.
* `rs_aiur_system_shard_prove_ixvm` —
`AiurSystem.shardProveIxVM (...)`: per-shard prove end-to-end in
Rust.
`build_claim_check_witness` lives next to
`build_shard_check_env_witness` in `src/ix/aiur_ixvm_witness.rs` and
uses the same parallel closure walk + parallel byte→G conversion.
The bytes-blob FFIs additionally harvest `anon_hints` from each
`Def` named entry after `Env::get` — `Env::get` (full form, used by
the bytes-blob path) doesn't populate `env.anon_hints` the way
`Env::get_anon` does, but the kernel's `verify_claim` reads ch 3
(Defn reducibility hints) so the hints must end up in the env. This
mirrors the harvest pass already inside `get_anon` at
`src/ix/ixon/serialize.rs:1683`.
# Wiring
`Ix.Cli.CheckCmd.WitnessSource`: a three-arm discriminated union
threaded through `forEachClaim` (the shared check/prove driver):
* `.native ixePath addr` — `.ixe`-backed env, Rust mmap.
* `.nativeBytes envBytes addr` — Lean-memory env serialized to
bytes, Rust decodes via `Env::get`.
* `.lean witness` — pre-built `ClaimWitness` (fallback).
`runCompiled` and `proveOne` dispatch on the source.
# Coverage
| Command | Path |
|---------------------------------------|-----------------------------------------------|
| `ix check NAME --ixe` | **`checkAddrIxVM`** (new) |
| `ix check NAME` (no `--ixe`) | **`checkEnvBytesIxVM`** (new) |
| `ix check --claim hex --ixe` | `checkAddrIxVM` for `check addr none` |
| `ix check --ixes --shard K` | `shardCheckIxVM` (existed) |
| `ix check --ixes` | `shardCheckIxVM` (existed) |
| `ix prove NAME --ixe` | **`proveAddrIxVM`** (new) |
| `ix prove NAME` (no `--ixe`) | **`proveEnvBytesIxVM`** (new) |
| `ix prove --ixes --shard K` | **`shardProveIxVM`** (new) |
| `ix prove --ixes` | **`shardProveIxVM`** loop (new) |
| `Benchmarks/Typecheck.lean` Phase 1 | `checkAddrIxVM` / `executeIxVM` |
| `Benchmarks/Typecheck.lean` Phase 2 | `proveAddrIxVM` / `proveIxVM` |
| `Benchmarks/IxVM.lean` | `proveIxVM` (was `prove`) |
`--interp` route is preserved: it materialises any `WitnessSource`
back into a `ClaimWitness` before driving the Aiur source
interpreter. `--claim <hex>` over non-`check addr none` variants
(`eval` / `reveal` / `contains` / `checkEnv-with-asm`) still uses
the Lean witness builder.
# Sanity
* `ix check Nat.add_comm --ixe init.ixe` (warm): 3.1 s wall,
FFT = 23_603_449.
* `ix check Nat.add_comm` (compiled env via bytes blob,
warm): 2.4 s wall, FFT = 23_603_449.
# Known overheads (tracked for a follow-up redesign)
* **Per-claim env re-parse on `--ixe + many names`**: each FFI call
re-runs `Env::get_anon_mmap` on the same path. Mathlib-scale
iteration pays the lazy-index build N times instead of once.
* **`--interp + .nativeBytes` round-trip**: Lean serializes the
compiled env then `materialise` deserializes it back, just to
feed `runInterp`.
* **`runShardProveNative` claim reconstruct**: redoes the closure
walk + canonical `AssumptionTree` build Lean-side after
`shardProveIxVM` already computed the same claim internally.
A future `EnvHandle`-based API would close all three: build the
env once into a Rust-owned handle, pass the handle to every
per-claim/per-shard FFI, and have prove FFIs return the
serialized claim bytes.
* EnvHandle: Rust-owned env shared across per-claim / per-shard FFI calls
Before: every per-claim and per-shard FFI re-parsed the Ixon env
(`Env::get_anon_mmap` per call). On `--ixe + many names` /
all-shards prove, this is the dominant overhead for iteration-heavy
workflows — O(num_consts) lazy-index build × N targets.
After: the env lives once per CLI invocation in a Rust-owned
`EnvHandle`. Lean holds an opaque `Aiur.EnvHandle` reference and
threads `@& EnvHandle` through every per-target FFI call. The env
is parsed exactly once at handle construction; downstream calls
share it.
# Surface
Five new FFIs collapse the previous six per-call variants
(`checkAddrIxVM`, `checkEnvBytesIxVM`, `shardCheckIxVM`,
`proveAddrIxVM`, `proveEnvBytesIxVM`, `shardProveIxVM` — all
deleted):
* `rs_aiur_env_handle_from_ixe(path) → LeanExternal<EnvHandle>`:
mmap-load via `Env::get_anon_mmap`. Anon parser already harvests
`anon_hints`; no post-pass.
* `rs_aiur_env_handle_from_bytes(blob) → LeanExternal<EnvHandle>`:
decode `Ixon.serEnv`-shape blob via `Env::get` + harvest
`anon_hints` from each `Def` named entry. Used by the
compiled-Lean-env path.
* `rs_aiur_toplevel_check_addr_with_env(toplevel, fun_idx, handle,
addr_bytes)`: per-claim check. Reuses handle's parsed env.
* `rs_aiur_toplevel_shard_check_with_env(toplevel, fun_idx,
handle, owned_blob)`: per-shard check.
* `rs_aiur_system_prove_addr_with_env(system, fri, fun_idx,
handle, addr_bytes) → (claim_bytes, proof, ioBuffer)`:
per-claim prove. Rust serializes the reconstructed `Ix.Claim`
via `ixon::Claim::put` so Lean can deserialize via
`Ixon.runGet Ix.Claim.get` directly — no closure walk +
canonical `AssumptionTree` recomputation Lean-side.
* `rs_aiur_system_shard_prove_with_env(system, fri, fun_idx,
handle, owned_blob) → (claim_bytes, proof, ioBuffer)`:
per-shard prove.
# Lean
* `Aiur.EnvHandle` opaque type with `fromIxe` / `fromBytes`.
* `Aiur.Bytecode.Toplevel.checkAddrWithEnv` / `shardCheckWithEnv`,
`Aiur.AiurSystem.proveAddrWithEnv` / `shardProveWithEnv`.
* `Ix.Cli.CheckCmd.Target` replaces `WitnessSource`:
```lean
inductive Target where
| addr (a : Address) -- Claim.check addr none
| shard (owned : Array Address) -- Claim.checkEnv
| leanW (w : ClaimWitness) -- --interp, --claim non-check
```
`runCompiled` / `proveOne` take `(envHandle?, target)`. The
envHandle is `none` only for `.leanW` (`--interp` legacy path).
* `runShardOwnedNative` and the manifest-driver helpers take the
envHandle as a parameter. Single-shard mode builds it once;
all-shards mode reuses the same handle across every shard's
FFI call (eliminates per-shard re-mmap).
* `runShardProveNative` deserializes the wire claim bytes via
`Ixon.runGet Ix.Claim.get` instead of re-running
`shardCheckEnvClaim`.
# Benchmarks
`Benchmarks/Typecheck.lean` builds the envHandle once before
Phase 1, reuses it across Phase 1 (execute) + Phase 2 (prove).
Both phases now go through `checkAddrWithEnv` / `proveAddrWithEnv`
on the full-closure path. `--subject-only` still uses Lean
`buildVerifyConst` + `executeIxVM` / `proveIxVM` (witnesses
intentionally small there).
# New crate
`crates/ix/src/env_handle.rs` — the `EnvHandle` struct +
constructors live in the existing `ix` crate next to the witness
builder and codegen runner.
# Sanity
* Multi-target check (warm): `ix check --ixe init.ixe Nat.add_comm Nat.add`
→ 3.3 s wall, single envHandle shared across both targets.
* Shard 26 check (warm): `ix check --ixe init.ixe --ixes init.ixes --shard 26`
→ ~78 s wall, FFT = 107_006_963_281 (parity preserved).
# Coverage
| Command | Path |
|--------------------------------------|-----------------------------------|
| `ix check NAME --ixe` | `checkAddrWithEnv` |
| `ix check NAME` (no `--ixe`) | `checkAddrWithEnv` + fromBytes |
| `ix check --claim hex --ixe` | `checkAddrWithEnv` for check-none |
| `ix check --ixes --shard K` | `shardCheckWithEnv` |
| `ix check --ixes` | `shardCheckWithEnv` × all shards |
| `ix prove NAME --ixe` | `proveAddrWithEnv` |
| `ix prove --ixes --shard K` | `shardProveWithEnv` |
| `ix prove --ixes` | `shardProveWithEnv` × all shards |
| `Benchmarks/Typecheck` Phase 1+2 | `checkAddrWithEnv` / `proveAddrWithEnv` |
Only `--interp` and `--claim hex` over a non-`check addr none`
persisted claim still build a Lean `ClaimWitness`; both go via
the `.leanW` target arm.
* ix codegen: add --check flag for CI; gate stale generated kernel
`ix codegen --check` compares the emitted Rust source against the
on-disk `crates/ix/src/aiur_ixvm.rs` and exits 0 if identical, 1
otherwise. No write side effect. ~2 s warm; fast enough to gate
on every PR.
Wired into the `lean-test` CI job so a forgotten regen on a
kernel-touching PR fails CI instead of merging stale generated
code that drifts from the Bytecode → Rust emitter.
* ix check: --interp {source|bytecode} to bypass codegen kernel
Two interpreter modes behind a single `--interp` flag:
* `--interp source`: Aiur source interpreter (`Aiur.runFunction` over
the source-level `Decls`). Richer per-step error diagnostics.
* `--interp bytecode`: generic Aiur bytecode interpreter
(`Bytecode.Toplevel.execute`, `rs_aiur_toplevel_execute` route).
Skips the `ix codegen` + `cargo build --release` cycle needed
after editing `Ix/IxVM/*.lean` — the bytecode is rebuilt Lean-side
at exe load. Slower per-check than the codegen kernel; ideal for
tight iteration on the IxVM source.
* omit the flag entirely for the native codegen kernel (default).
Invalid values (e.g. `--interp foo`) fail fast with a clear error.
# Plumbing
The `check_addr_with_env` and `shard_check_with_env` FFIs take a
`use_bytecode: bool` and dispatch via a shared `dispatch_execute`
helper. `--interp bytecode` sets it to `true`. The `.leanW` arm of
`runCompiled` also picks between `Bytecode.Toplevel.execute` and
`executeIxVM` based on the same flag.
The `--interp source` path requires a Lean `ClaimWitness`. The
existing driver had switched to `.addr`/`.shard` targets against
the Rust-owned `EnvHandle`; source-interp had no way to materialise
those. `forEachClaim` now takes a `forceLeanWitness : Bool` — when
true, it builds a Lean witness for every target (via `mkWitness` /
`loadIxonEnv` for the compiled-Lean-env path) and passes `.leanW`
so `runInterp` can consume it directly.
# Sanity
* `ix check Std.Time.Week.Offset.ofMilliseconds` (warm): 9.3 s wall,
FFT = 12_430_516_949 (codegen kernel).
* `ix check --interp bytecode Std.Time.Week.Offset.ofMilliseconds`
(warm): 14.6 s wall, FFT = 12_430_516_949 (bytecode interp).
* `ix check --interp source Eq` (warm): 6.3 s wall, output `Eq: ()`.
* `ix check --interp garbage Nat.add_comm`: exits 1 with clear
error.
* IxVM codegen: regen + rebase-fixups after KLevel port
Aligns the ap/codegen-ixvm-native stack with main's KLevel pointer
port (b84a500) and re-lands clippy-clean under the workspace lint set:
- Regen crates/ix/src/aiur_ixvm.rs from Aiur source (KLevel = &KLevelNode
changes the generated fn shapes; ~26k lines net churn).
- Extend the generated file's #![allow(...)] header (via
Ix/Aiur/Stages/Codegen.lean) with clippy::ptr_as_ptr,
clippy::match_same_arms, and clippy::large_types_passed_by_value —
three lints the codegen's straight-line style trips deterministically
on every regen and that clippy::all doesn't cover.
- rustfmt reflow in crates/aiur/src/execute.rs and a handful of ix / ffi
files that CI now enforces via the ap/aiur-aux-recursor-parity
toolchain.
- Fix 4 real clippy warnings uncovered under the workspace lint set:
* env_handle.rs: clone-on-Copy → deref (ReducibilityHints is Copy).
* aiur_ixvm_witness.rs: collapse if-let-if, drop needless continue,
slice::from_ref instead of &[x.clone()].
* aiur_ixvm_runner.rs: keep execute_ixvm's Vec<G> arg (required by
AiurSystem::prove_ixvm's fn-pointer bound) + local #[allow(
clippy::needless_pass_by_value)] with a comment explaining why.
* ffi/aiur/protocol.rs: unqualify aiur::G/IOBuffer/QueryRecord after
the workspace lint added unused_qualifications; is_multiple_of()
over % 0.
Verified: cargo clippy --workspace --all-targets --all-features
--D warnings clean; lake test -- --ignored ixvm passes.
* ix-check + ixvm tests: coverage gate, --interp source fix, codegen parity + rename ix crate to ixvm-codegen
Four review fixes on the codegen-ixvm-native stack.
- **Coverage gate on \`--ixes\` (all-shards, native path).** \`runShardManifestAllNative\`
now calls \`shardsCover\` before running any shard, matching the pre-refactor
\`runShardCheckAll\` behavior. Without this, a stale/truncated \`.ixes\` manifest
makes \`ix check --ixes\` exit 0 while some env constants are never checked
by any shard — the mundane trigger being: edit a definition, rebuild the
\`.ixe\`, forget to re-run \`ix shard\`, and the constants that go unchecked
are exactly the ones just edited. Single-shard \`--shard K\` path is
unchanged (consistent with pre-refactor). \`shardsCover\` moved above
\`runShardManifestAllNative\` to satisfy forward-decl ordering.
- **\`ix check --ixe … --claim <hex> --interp source\` regression.** The
\`claimHex\` arm in \`forEachClaim\` ignored \`forceLeanWitness\` and always
mapped \`.check addr none\` claims to \`Target.addr\`. Under \`--interp
source\`, \`runInterp\` then rejects \`.addr\` with "\`--interp requires a
Lean witness; addr/shard targets unreachable here\`". Now mirrors the
sibling name-based arms and routes through the Lean witness path when
\`forceLeanWitness\` is on. Only bit the common claim shape.
- **Codegen ↔ bytecode parity CI test.** New \`runParityCase\` + \`parityCases\`
in \`Tests/Ix/IxVM.lean\` wire every constant already listed in
\`kernelCheckEntries\` plus \`kernel_unit_tests\` through BOTH
\`Toplevel.execute\` (bytecode) and \`Toplevel.executeIxVM\` (codegen'd
Rust), and diff the returned \`(output, IOBuffer, QueryCounts)\` triples.
Turns "generated kernel ≡ interpreter on QueryRecord" from
reviewed-by-hand into checked-by-CI. 129 assertions run per suite
invocation (43 constants × output + IOBuffer + QueryCount), all pass on
this branch head.
- **Rename \`crates/ix\` → \`crates/ixvm-codegen\`.** The old \`ix\` crate held
only the codegen'd IxVM kernel + its runner + witness helpers.
\`ix-kernel\` is the hand-written Rust ix typechecker; \`ix-common\` /
\`ix-compile\` are Ix-level infrastructure. \`ixvm-codegen\` cleanly names
what this crate holds. Path updates: workspace \`members\` and
\`workspace.dependencies\`, ffi crate dep + \`use\` sites, Lean
\`codegenOutPath\` in \`Ix/Cli/CodegenCmd.lean\`, doc reference in
\`Ix/Aiur/Semantics/BytecodeFfi.lean\`. \`ix codegen\` now writes to
\`crates/ixvm-codegen/src/aiur_ixvm.rs\`.
Verified: \`cargo check --workspace\` + \`lake test -- --ignored ixvm\` both
exit 0 post-rename; parity + pinned FFT tests all pass.
* cargo-deny: allow ar_archive_writer's Apache-2.0 WITH LLVM-exception
Post-rename, ixvm-codegen pulls stacker → psm → ar_archive_writer (a
build-time transitive). ar_archive_writer is licensed under the
LLVM-exception variant of Apache-2.0 (standard for LLVM tooling; no
additional runtime obligation for downstream users), which isn't on
the workspace allow list. Add a per-crate exception scoped to
ar_archive_writer so we don't blanket-allow the license family across
the tree.arthurpaulino added a commit
that referenced
this pull request
Jul 11, 2026
Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.
arthurpaulino added a commit
that referenced
this pull request
Jul 11, 2026
Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.
arthurpaulino added a commit
that referenced
this pull request
Jul 11, 2026
Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.
arthurpaulino added a commit
that referenced
this pull request
Jul 11, 2026
Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.
arthurpaulino added a commit
that referenced
this pull request
Jul 13, 2026
Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.
arthurpaulino added a commit
that referenced
this pull request
Jul 14, 2026
Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.
arthurpaulino added a commit
that referenced
this pull request
Jul 17, 2026
Stored recursors bake the COMPILER's canonical aux order into their motive/minor layout, but build_flat_block discovers auxes in queue (traversal) order — position-by-position recursor matching only worked when the two orders happened to coincide. Mirror inductive.rs canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the queue pass, re-sort the aux suffix by partition refinement over synthetic aux views. Aiur-isms vs the Rust original: * Synthetic addresses are replaced by SENTINEL positions `|top| + ordinal`: each aux's view (ext type/ctors with occurrence universe args instantiated, spec_params substituted, block params wrapped) rewrites nested aux occurrences to sentinel Consts, fixed per ordinal so views synthesize once; each refinement round's ctx maps sentinels to their current class, so same-class refs compare weak-Equal — the same mechanism the canonical block sort uses for block-local refs. * Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is a stable merge sort; a first cut with an unstable insertion sort REVERSED tied pairs, swapping content-identical auxes whose spec params differ only in phantom parameters (IxVMInd.DedupM's Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match. * The reorder is unconditional: every env Aiur checks comes through the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean- source order case Rust skips (rs:2293) cannot reach this kernel. Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT pins re-bumped, still relative to this branch's stubbed verify_bytes_against); bytecode repros green for the multi-aux blocks Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec, IxVMInd.DepthM.rec; full mathlib shard-0 native run green (9357/9357 owned consts). Codegen regenerated. Side finding for the compile side: copying the DedupM/Bar2 fixtures into the CLI env under a different namespace (IxDbgFixtures) makes compile_env fail that block with "compute_aux_perm: no canonical match for in-SCC source aux #1" while the identical structure compiles fine as IxVMInd.* in the test env — compile-side aux matching looks name-order sensitive. Repro: re-add the four fixtures from Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh namespace and run `ix check <ns>.DedupM.rec`.
arthurpaulino added a commit
that referenced
this pull request
Jul 17, 2026
* stub verify_bytes_against
* ix name-of: reverse (address -> names) lookup
`ix name-of --ixe env.ixe <64-hex-addr>` resolves a content address
back to its Lean names. Potentially MANY names: structurally
equivalent constants collapse to the same content address, so every
entry in the env's `named` table pointing at the address is printed,
one per line (the `addrToName` reverse index keeps only one name per
address and would silently drop the aliases). Addresses of unnamed
Muts blocks fall back to scanning for projection constants into the
block and printing their names. Turns an anonymized failing address
surfaced by the IxVM kernel into an `ix check <name>` fast repro.
Lives in its own subcommand instead of overloading `ix addr-of`
(name -> address), which stays as-is.
* IxVM Aiur kernel: mirror Rust canonical-sort comparator and whnf index walks
Two mathlib-blocking divergences from the Rust kernel, found via shard 0
of the mathlib env:
1. Canonical block sort (CanonicalCheck.lean): the Indc comparator never
descended into constructors, so same-shape mutual inductives (e.g.
Mathlib.Tactic.Ring's ExBase/ExProd/ExSum: identical flags, arities
and types, differing only in ctor types) collapsed into one alpha
class and the block was rejected (assert 0 != 1 in
validate_block_canonical). Mirror compare_kindc's ctors tail
(canonical_check.rs:299-338) via compare_kctor_idxs_ctx /
compare_kctor_pair_ctx, resolving ctor positions through `top`.
Further parity fixes in the same pass:
* ctx is now a real KMutCtx mirror (from_id_classes): (position,
class idx) pairs where same-class members share ONE index (weak-
Equal, no position-derived tiebreaks) and each Indc member's ctors
map at i + cidx.
* External const refs compare by 32-byte address (addr_cmp,
lexicographic like Rust's Address Ord) instead of by ingress
position, matching the order the compile-side sort produced.
* Rec-rule comparison drops the ingress-artifact global ctor idx —
(fields, rhs) only, mirroring canonical_check.rs:280-289.
* Refinement fuel is 1 + |members| (provably reaches fixpoint)
instead of a fixed 32.
* Ctx-less compare_kexpr Const arm compares levels before ref
(field-order parity; equality-only callers unaffected).
2. Inductive index walks (Inductive.lean): get_result_sort_level and
the motive/rec-type index-dom collectors peeled literal Foralls only.
Index binders can hide under definitional wrappers — Mathlib's
`inductive εClosure (S : Set σ) : Set σ` stores a type ending in
`Set σ` that only whnf exposes as `σ → Prop` — so εNFA.εClosure died
with `no match case for value 3` (KExprNode.App). whnf before every
peel, mirroring inductive.rs get_result_sort_level (line 2101+) and
build_motive_type_flat (2521-2531).
Repros (both now pass):
ix check --ixe mathlib.ixe Mathlib.Tactic.Ring.ExSum --interp bytecode
ix check --ixe mathlib.ixe εNFA.εClosure.step --interp bytecode
`lake test -- --ignored ixvm` green (599 assertions). Codegen
regenerated; FFT pins re-bumped — pin values reflect this branch's
stubbed verify_bytes_against and need one more bump when the stub is
reverted.
Known remaining issue: shard-scale runs crawl inside
collect_block_members (per-block O(|top|) rescans whose memo keys make
the query map blow up); fix planned separately.
* Aiur codegen: emit println! for dbg! (Op::Debug)
emitDebug was a silent stub, so dbg! probes only printed under
--interp bytecode — kernel debugging was pinned to the slowest engine.
Emit the same println! the bytecode interpreter's Op::Debug arm
produces (label + comma-separated values), with the label escaped for
a Rust format-string literal. Production kernels contain no dbg!, so
generated output is unchanged there; probe builds now print at native
speed.
* IxVM Aiur kernel: block-members table, aux-synthesis parity, drop stored-aux validation
Three fixes surfaced by driving mathlib shard 0 to green:
1. Perf: derive_block_member_idxs rescanned the whole `top` list per
block, and each scan step's memo key included the block addr —
|blocks| x |top| query-map entries dominated shard-scale runs (99%
of CPU in QueryMap ops). One memoized walk now builds an rbtree from
addr_key(block_addr) to buckets of (full addr, ascending member
positions); every query is an O(log N) lookup + address_eq-confirmed
bucket walk (4-byte key collisions cost a short walk, never a wrong
member list).
2. Aux synthesis (Lean.Compiler.LCNF.Cases): synth_aux_ind_ty /
synth_aux_ctor_ty never instantiated the occurrence's universe args,
so synthesized types kept `Type u` (Param 0) where the block stores
monomorphized `Type 0`; binder peels also assumed literal Foralls.
Mirror canonical_aux_order's construction (inductive.rs:1169-1234):
instantiate occurrence_us, whnf before each peel. addrs is threaded
through the build_flat_block chain for the whnf calls.
3. Stored-aux validation removed: validate_block_auxes assumed Muts
blocks store synthesized aux inductives and classified members with
is_aux_inductive ("no own nested occurrence but some member has
one"). Stored blocks only ever contain the source originals — the
Rust kernel seeds every stored member is_aux:false (rs:537) and
flags auxes only on transient detection (rs:755) — so the heuristic
misclassified originals in mixed blocks (LCNF's Alt/FunDecl/Code,
where only Cases carries the nested occurrence) and asserted on a
legitimate block. Smuggled extra members remain rejected by the
recursor-vs-canonical-type equality over the detected flat block.
Validation: full shard-0 native run green (9357/9357 owned consts);
`lake test -- --ignored ixvm` green (599 assertions; codegen
regenerated, FFT pins re-bumped — still relative to this branch's
stubbed verify_bytes_against).
Known residual divergence (not yet observed failing): Rust reorders
the detected aux portion of a flat block via canonical_aux_order
before recursor checks; Aiur keeps discovery order.
* Drop the `lake exe check` shim
The thin Cli wrapper around Ix.Cli.CheckCmd.runCheckCmd had drifted
from the real command (its `interp` flag was still a bare bool while
`ix check --interp` takes a mode string), and `lake exe ix check`
rebuilds just as incrementally for day-to-day kernel iteration. One
entrypoint, no drift.
* IxVM Aiur kernel: canonical aux order for flat blocks
Stored recursors bake the COMPILER's canonical aux order into their
motive/minor layout, but build_flat_block discovers auxes in queue
(traversal) order — position-by-position recursor matching only worked
when the two orders happened to coincide. Mirror inductive.rs
canonical_aux_order (rs:1058+, applied at rs:2293-2321): after the
queue pass, re-sort the aux suffix by partition refinement over
synthetic aux views.
Aiur-isms vs the Rust original:
* Synthetic addresses are replaced by SENTINEL positions
`|top| + ordinal`: each aux's view (ext type/ctors with occurrence
universe args instantiated, spec_params substituted, block params
wrapped) rewrites nested aux occurrences to sentinel Consts, fixed
per ordinal so views synthesize once; each refinement round's ctx
maps sentinels to their current class, so same-class refs compare
weak-Equal — the same mechanism the canonical block sort uses for
block-local refs.
* Ties keep DISCOVERY order (stable insert). Rust's sort_by_compare is
a stable merge sort; a first cut with an unstable insertion sort
REVERSED tied pairs, swapping content-identical auxes whose spec
params differ only in phantom parameters (IxVMInd.DedupM's
Bar2⟨·,Nat⟩ / Bar2⟨·,Bool⟩) and breaking their rec-type match.
* The reorder is unconditional: every env Aiur checks comes through
the Ix compile pipeline (RecursorAuxOrder::Canonical); the Lean-
source order case Rust skips (rs:2293) cannot reach this kernel.
Validation: `lake test -- --ignored ixvm` green (599 assertions; FFT
pins re-bumped, still relative to this branch's stubbed
verify_bytes_against); bytecode repros green for the multi-aux blocks
Lean.Compiler.LCNF.Cases, Lean.Syntax.rec, IxVMInd.DedupM.rec,
IxVMInd.DepthM.rec; full mathlib shard-0 native run green
(9357/9357 owned consts). Codegen regenerated.
Side finding for the compile side: copying the DedupM/Bar2 fixtures
into the CLI env under a different namespace (IxDbgFixtures) makes
compile_env fail that block with "compute_aux_perm: no canonical match
for in-SCC source aux #1" while the identical structure compiles fine
as IxVMInd.* in the test env — compile-side aux matching looks
name-order sensitive. Repro: re-add the four fixtures from
Tests/Ix/IxVM.lean:93-108 to any ix-CLI-visible module under a fresh
namespace and run `ix check <ns>.DedupM.rec`.
* Restore verify_bytes_against; re-pin FFT costs at honest values
Reverts the probe-branch stub (b7a0336) that disabled blake3
verification of constant/blob/claim bytes during the mathlib shard-0
debugging campaign. Codegen regenerated; FFT pins re-bumped with
hashing back in the circuit.
The pins land within ±1.1% of main (median ratio 0.997): the kernel
work on this branch — canonical-sort comparator parity, whnf-aware
index walks, the block-members table, aux-synthesis parity and
canonical aux order — is cost-neutral. Nested-aux-heavy targets
(DedupM, DepthM, AuxDedup*, Lean.Syntax.rec) got 0.5-1.1% cheaper;
small stdlib targets (HEq, Nat, Eq.rec) pay 0.4-0.7% for the richer
comparator and whnf walks.
`lake test -- --ignored ixvm` green (599 assertions).johnchandlerburnham added a commit
that referenced
this pull request
Aug 7, 2026
Two fixture-driven repairs to the universe-aware nested-aux dedup introduced by #532, mirrored Rust <-> Lean throughout. 1. Lean mirror lambda-precedence bug (term axis, IxVMInd.DedupM). In Ix/AuxGen/Recursor.lean the dedup wrote (levels.zip levelHashes).all fun (a, b) => a == b && hashes.size == specHashes.size && ... and the lambda body swallowed the remaining conjuncts, so for a non-universe-polymorphic family (empty level list) the vacuous .all skipped the spec-param comparison entirely — Bar2<DedupM,Nat> and Bar2<DedupM,Bool> collapsed to one aux (2 motives instead of 3), failing decompile-diff aux-fidelity + the .rec roundtrip while Rust (explicit closure bounds) stayed correct. Parenthesized; pinned by a RecursorTests fixture (termSpecializedNested*). 2. Universe axis (new fixture IxVMInd.UnivM: PhantomBox.{0}/.{1} with the same term spec param — Lean emits distinct motives; #532 covered this at the flat-block dedup only, and no corpus fixture existed). Three downstream sites still keyed aux identity on (family, term specs) alone and are now level-aware, each with an exact-levels pass first and a level-insensitive fallback (alpha-collapse can rename a block's universe params between source and canonical): - compute_aux_perm source-canonical matching (nested.rs + AuxGen/Nested.lean): both source auxes previously mapped onto the first canonical slot, leaving slot #1 uncovered ("canonical aux #1 has no source mapping", the whole-block failure that kept this shape out of the corpus). - match_classes_against_app (recursor.rs + AuxGen/Recursor.lean): ctor-field class matching returned the first spec-matching class for both occurrences. - NestedRewriteCtx.aux_info (recursor.rs/expr_utils.rs + AuxGen/Recursor.lean/ExprUtils.lean): keyed HashMap<Name, entry>, so same-name entries overwrote and one instantiation's levels were stamped onto every occurrence (the "Succ vs Zero" congruence failures on .rec/.below/.brecOn). Now multi-valued per name: exact-levels entry preferred (identity — members store raw ctor levels post-#532), last entry as the legacy fallback for the genuine recompute case (Array.{u} occurrence vs Array.{max u v} member). source_aux_order_from_expanded widens to carry head levels; the public source_aux_order* wrappers are unchanged. AuxGen lookupConst? also routes through Environment.get? (the parent change's streaming fallback). Gates with UnivM seeded into the corpus: validate-aux 0 failures, aux-gen-diff all gates PASS (patches 1569, serialized envs byte-identical), decompile-diff all gates PASS (5442 consts, 0 errors, 0 mismatches), cargo test -p ix-compile 231 passed, clippy clean, lake test PASS.
johnchandlerburnham added a commit
that referenced
this pull request
Aug 7, 2026
* validate-lean: digest-based phase-5 oracle; release envs between phases Whole-Mathlib validate-lean previously held the canonicalized source env from phase 1 through phase 5 as the decompile-comparison oracle (plus the elaborated Lean env for its whole run), on top of the decompile working state — several whole-env copies resident at once, which pushed a 124 GiB box deep into swap. Phase 5 now compares per-name 64-bit digests by default: derive Hashable for the Ix constant types (same field coverage as the derived BEq, O(1) at the hash-consed Name/Level/Expr leaves), digest the canon view right after phase 1, and let the whole canon env free with the phase-1 output. The decompiler runs with origEnv? := none — its per-recovery debug track is subsumed by the digest comparison at gate level. The Lean source env is released after phase 4 (its last reader). Collision odds at 205k constants are ~1e-14, and any reported mismatch is re-checkable structurally: --full-oracle restores the old whole-env BEq path + decompiler debug track, intended together with --ns to debug a digest mismatch on a small closure. * compile-lean: stream proof bodies through canon; never materialize them `compileLeanConsts` previously canonicalized the whole environment into one map and held it through compile — at whole-Mathlib scale that map plus the elaborated Lean env and the compile state peaked past physical RAM (~180 GiB total footprint) regardless of worker count. The driver now streams: - A name-only pre-pass canonicalizes names, building the lazy-lookup key map, the reverse name-hash view for nameForAddr, and a THIN ground-check env — groundExpr/groundConst read only name-existence and is-it-a-ctor, so two shared placeholder constants stand in for every value. - The canon pass (chunk-parallel) canonicalizes each constant TRANSIENTLY, extracting its ref set (graphConst reads nothing else), immediate ground error, and content digest. Proof bodies (thmInfo / opaqueInfo — the bulk of Mathlib, never read by dependents) are then dropped; code kinds (definitions, inductive families, ctors, recursors — read repeatedly and with retention by aux-gen and kernel ingress) are kept and become the materialized map, preserving shared structure and O(1) dependency reads. - Compile runs against the hybrid env: `Ix.Environment` gains a pure `fallback?` resolver consulted on `consts` miss (`Environment.get?`), wired through findConst, CallSiteSurgery, and compileConstNoAuxPure (aux-gen lookupConst? follows in the level-aware aux identity change). A proof body is canonicalized on demand for its own block and freed when the block returns. Materialized-env callers (every test/gate and the decompile side) leave fallback? none and are bit-for-bit unaffected. - Per-name digests ride out via LeanPipelineOut.digests; validate-lean digest mode consumes them directly, and --full-oracle materializes the whole view post-hoc only when explicitly requested. - nameForAddr gets a nameByHash map (CompileEnv, threaded through the aux driver entry points) since the streaming env has no consts keys to scan; the materialized-env scan is preserved as fallback. Canon is per-constant deterministic (chunking was already arbitrary), so compiled output is byte-identical — verified on the 191,506-constant Ix-library env: phase 1 reproduces 472,653,224 bytes / 186,459 blocks exactly, serde byte-identical, phase 5 all 191,506 constants digest-identical, wall time within 6%. On that code-heavy env the peak is compile-state-bound (~unchanged); the win scales with the proof fraction, i.e. with Mathlib. lake test green. * compile: byte-backed constant storage `CompileEnv.constants` / `ParallelState.constants` store SERIALIZED bytes instead of structured `Ixon.Constant`s. The structured map retained a whole-env-scale object graph for the entire compile; the bytes already exist when a block merges (`result.blockBytes` / `projBytes`), readers needing structure parse on demand (`Ixon.deConstantAt` — only the commit-open path), and assembly wraps entries as byte-backed `Ixon.LazyConstant`s (`cache := none`), the representation whose lazy-load path already keeps mathlib.ixe cheap. Rust peaks ~20 GiB on the same compile largely because compiled output lives as bytes; this is the same architecture. Measured on whole Mathlib (736,624 constants, 726,519 blocks): driver-retained state grows only ~16 GB across the entire compile — RSS flat from 44.8 GB at 20k blocks to 60.9 GB at 720k, with the attribution trace (IX_COMPILE_DBG=1: phase timings + live per-20k-block RSS/structure sizes) pinpointing the remaining spike as the transient working set of the final straggler waves, not retention. aux-gen-diff: serialized envs byte-IDENTICAL vs Rust through the new path, sequential + parallel drivers; lake test green. * ixon: add ignored named-meta dump probe (dump_named_metas) * docs: specify metadata name canonicalization at alias occurrences (canonicity 10.5, 17.8) * aux_gen: level-aware nested-aux identity end to end (DedupM + UnivM) Two fixture-driven repairs to the universe-aware nested-aux dedup introduced by #532, mirrored Rust <-> Lean throughout. 1. Lean mirror lambda-precedence bug (term axis, IxVMInd.DedupM). In Ix/AuxGen/Recursor.lean the dedup wrote (levels.zip levelHashes).all fun (a, b) => a == b && hashes.size == specHashes.size && ... and the lambda body swallowed the remaining conjuncts, so for a non-universe-polymorphic family (empty level list) the vacuous .all skipped the spec-param comparison entirely — Bar2<DedupM,Nat> and Bar2<DedupM,Bool> collapsed to one aux (2 motives instead of 3), failing decompile-diff aux-fidelity + the .rec roundtrip while Rust (explicit closure bounds) stayed correct. Parenthesized; pinned by a RecursorTests fixture (termSpecializedNested*). 2. Universe axis (new fixture IxVMInd.UnivM: PhantomBox.{0}/.{1} with the same term spec param — Lean emits distinct motives; #532 covered this at the flat-block dedup only, and no corpus fixture existed). Three downstream sites still keyed aux identity on (family, term specs) alone and are now level-aware, each with an exact-levels pass first and a level-insensitive fallback (alpha-collapse can rename a block's universe params between source and canonical): - compute_aux_perm source-canonical matching (nested.rs + AuxGen/Nested.lean): both source auxes previously mapped onto the first canonical slot, leaving slot #1 uncovered ("canonical aux #1 has no source mapping", the whole-block failure that kept this shape out of the corpus). - match_classes_against_app (recursor.rs + AuxGen/Recursor.lean): ctor-field class matching returned the first spec-matching class for both occurrences. - NestedRewriteCtx.aux_info (recursor.rs/expr_utils.rs + AuxGen/Recursor.lean/ExprUtils.lean): keyed HashMap<Name, entry>, so same-name entries overwrote and one instantiation's levels were stamped onto every occurrence (the "Succ vs Zero" congruence failures on .rec/.below/.brecOn). Now multi-valued per name: exact-levels entry preferred (identity — members store raw ctor levels post-#532), last entry as the legacy fallback for the genuine recompute case (Array.{u} occurrence vs Array.{max u v} member). source_aux_order_from_expanded widens to carry head levels; the public source_aux_order* wrappers are unchanged. AuxGen lookupConst? also routes through Environment.get? (the parent change's streaming fallback). Gates with UnivM seeded into the corpus: validate-aux 0 failures, aux-gen-diff all gates PASS (patches 1569, serialized envs byte-identical), decompile-diff all gates PASS (5442 consts, 0 errors, 0 mismatches), cargo test -p ix-compile 231 passed, clippy clean, lake test PASS. * compile: block-scope kernel contexts and fix source-name hint keys (canonicity 10.5) Two fixes making synthesized-expression metadata names a deterministic, source-faithful function of the block (provenance rule, canonicity 10.5): - whnf_lean's source-name hint map keyed by KExpr::hash_key(), which is an intern uid — fresh for every un-interned to_kexpr_static construction — so collect-time and restore-time keys never matched and the restoration pass restored nothing. Key both sides with kexpr_content_key, a pure name-erased structural digest mirroring the ExprKey / Lean Ix.Tc content-address equivalence, and make the WHNF no-op test structural (==) rather than uid equality. This was the whole-Mathlib 47-byte divergence (Quiver.FreeGroupoid.redStep.{rec, casesOn,recOn}: HomRel (Paths (Symmetrify V)) reducts intern-collapsed to 'Paths (Paths V)' with restoration dead). - compile_env worker loop and aux_gen prereq loop reused one KernelCtx across blocks: name-erased caches replay alias display names recorded by earlier blocks on the same worker, schedule-dependently. Fresh KernelCtx per block compile (checker and aux-dump paths already were). Fixture: Canonicity.AliasProvenance — cross-block alpha-identical wrapper defs referenced at two spellings in one expression, both orientations, through a reducible index wrapper (the HomRel shape) and as sibling constructor fields. Benchmarks/Compile/CompileRedStep.lean: 228k-const repro closure (Rust 10.5s; compile-lean --rust-check is the aligned gate). Result: whole-Mathlib Rust and Lean outputs byte-identical (3,152,009,710 bytes, 736,624 consts; Rust wall +2.5%). * tc egress: linearize canonical roundtrip compare on pointer-shared DAGs The anon-roundtrip comparator canonicalizes both sides and compares. canonExpr's only memo was .share-INDEX-keyed, which linearizes parsed constants (explicit .share nodes) but re-materializes every pointer-shared subtree of an EGRESSED constant per occurrence — exponential tree unfolding. At whole-Mathlib scale phase 3 of validate-lean spiked past 100 GiB (multi-GiB transients from KB-sized deeply-shared constants, thread-count independent) and, once the memory was fixed, the derived tree-walking == burned 5.6 hours on the same DAGs. - canonExprImpl: @[implemented_by] runtime twin with a call-local pointer-identity memo over composite nodes (ShareCommon soundness argument: immutable values, non-moving RC heap, keys are subtrees of the live root). Canonical outputs now pointer-share repeated substructure, so equal shared inputs yield the SAME output object. - exprEqDag / constEqDag: pair-pointer-memoized equality used by roundtripCompare (reference semantics: plain ==). Covers all ConstantInfo variants including Muts members. 14k-item sequential slice: 73.4 GiB / 460 s → 5.1 GiB / 13.2 s. Full 647,127-constant phase 3: >100 GiB OOM → PASS at modest memory. * validate-lean: stream the serde and meta-roundtrip phases Whole-Mathlib validate-lean died in phase 2, not compile: serdeGate's deEnv materializes every constant and metadata arena and serEnv rebuilds the whole 3.1 GB image to compare — a >100 GiB resident spike measured in isolation (--ixe mode, no Lean env pinned), with the 48 GiB Lean import still resident for phase 4 in a real run. Phase 4 would have stacked a third whole-env copy (the merged meta KEnv) on top. - Ixon.getEnvVerifiedLazy / deEnvVerifiedLazy: streaming verified load. Every unit is parsed with the pure reader, re-serialized with the pure writer, and compared against its input span, spans covering the image gaplessly; order/root/trailing contracts the whole-image compare used to pin are asserted directly (§1/§2/§6 address order, §5 name order, §4 order equal to topologicalSortNames of the parsed set). Constants are retained as zero-copy LazyConstant.ofSlice windows and §5 rows as NamedRow metadata windows, materialized per name on demand. Coarse dbgTrace progress markers (stdout is block-buffered mid-run). - Tc.serdeGateStreaming: the gate over the new loader. - Tc.metaRoundtripEnvStreaming: chunks respect block boundaries (meta ingress resolves Muts SIBLING names), work is enumerated from a chunk-only named table while ingress-time name→address resolution reads the chunk overlaid on a whole-env ADDRESS-ONLY stub table (cross-block references read just .addr; enumerating stubs as work ingresses their empty metas — the two roles must be split). Per chunk: materialize → chunk-local ingress → egress → compare → drop; the whole-env merged MetaEnv never exists. IX_META_EAGER=1 keeps the eager driver as a closure-scale oracle: verdicts are IDENTICAL (217,324 checked / same 2 findings on the redStep closure). - validate-lean wires phases 2-4 to the lazy parts; phase 5 interim: materializeAll (named + cached consts) after the Lean env is released. - EgressLean diff describer now prints both level lists on levels-differ mismatches. - Memory-diagnosis knobs (all env-gated, zero default cost): IX_ANON_CAP / IX_ANON_SEQ / IX_ANON_STAGE / IX_SKIP_PHASES / IX_ANON_HOLD / IX_META_EAGER; CompileDriver: IX_LOG_BLOCKS tail-gated per-block BEGIN/END trace. Whole-Mathlib result (with the DAG-compare fix in the parent commit), 124 GiB box, --workers 8, peak 95.9 GiB, no swap: 1 compile PASS 3,152,009,710 B / 726,519 blocks / 0 ungrounded (1035 s) 2 serde PASS streaming gate, all units byte-identical (235 s) 3 anon PASS 647,127 constants structurally preserved (42 s) 4 meta 714,235 checked / 111 'levels differ' findings (171 s) 5 decomp PASS 736,624 digest-identical to canonical source (4269 s) The 111 phase-4 findings are one PRE-EXISTING class, independent of this change (the eager oracle reproduces them bit-for-bit): universe LEVEL normal forms disagree between the kernel meta egress path and CanonM at value-position occurrences of ubiquitous constants (DFunLike.coe, List.nil, PSigma.casesOn in WF-recursion eq_defs, …) — 0.016% of checked rows; phase 5 passing whole-Mathlib shows the stored artifacts are faithful and the gap is in phase 4's direct comparison. Tc-ingress/egress territory. * docs: specify universe-level canonicalization (canonicity 10.6, staged) * decompile: append metaRefs/metaUnivs extension tables in Lean mkBlockCtx * tc: level-spelling decorations through the kernel meta path (stage 1) * ixon: canonUniv — Géran canonical representative (canonicity 10.6, P1-P6) * ixon: level-canonicalization census probe (dump_reducible_univs) * ixon: univPatches wire format (canonicity 10.6 stage 2) * compile+kernel: rust-side universe-level canonicalization (canonicity 10.6 stage 2) Phase 1 of plans/level_canonicalization_rust_first.md — the Rust pipeline end-to-end on the Géran-canonical univ-table spec: - compile: preseed canonicalizes tables (canon_univ before sort; every primary entry canon-fixed), compile_univ_idx interns canonical forms and mints virtual indices (univs.len + slot) into per-constant metaUnivs; sort/const/rec arms emit univPatches keyed by arena root (const patches carry the FULL arg list); BuildCallSite clones a head patch onto the CallSite root (the head's own Ref root is unreachable by replay); V3 preseed-finality debug tripwire. - decompile: patch replay at sort/ref/rec arms + call-site head via load_meta_extensions' arena-index map; ctor window installs per-ctor extensions at the PRIMARY table offset (parent extension displaced), and clears the pointer-keyed univ memo per ctor — demoted metas re-parse per access, so ctor-scoped extension Univs are ephemeral and freed addresses could collide in the memo (the jcb-caught flaky Std.DHashMap.Raw.WF Subtype.mk spelling bug; 8/8 repro now clean). - kernel ingress: decorations sourced from univPatches (virtual space univs ++ metaUnivs) at sort/ref/rec + both call-site head arms, with the stage-1 mk*-rebuild rule as fallback (never fires on canonical tables, P3; keeps raw-table fixtures exercised). - kernel egress (ixon half): EgressCtx preseeds the univ table verbatim from the ORIGINAL constant so the rebuilt layout matches the original meta's patch index space by construction (V1: measured — rebuilt first-use tables diverge from originals on 61%/98% of bodies and only the absence of meta table-refs hid it); decor-interning dropped — kexpr_to_ixon always emits the kernel-held canonical level. - level.rs: norm_level_eq ignores empty subsumption entries (O1 option (b)) — univ_eq is now the exact semantic quotient; Mathlib witness pair pinned with an eval-certified vector. - prim_addrs.rs: 56 canonical pins regenerated (build-primitives parity green); LEON new_orig pins unchanged as expected. Validation: cargo suites green (kernel 674, compile 234); validate-aux 0 fail; rust-compile 0/228,770 (incl. 577 MB serde roundtrip); kernel-ixon-roundtrip 0/150,396; whole-Mathlib ix validate 0/736,624 (all 8 phases, 3.16 GB serde); regenerated compileinitstd/redstep.ixe; census probe on the new artifact: Géran-noncanonical 0 entries, collision constants 0, src==canonical bytes. * compile: canonicalize univ tables + emit univPatches (canonicity 10.6 stage 2, Lean mirror) Phase 2 L1 of plans/level_canonicalization_rust_first.md — mirror of the Rust compile half: preseed canonicalizes the primary univ table (canonUniv before sort; univsFinal V3 tripwire), compileAndInternUnivCanon interns canonical forms and mints virtual indices into per-constant metaUnivs, sort/const arms emit arena-root-keyed univPatches (const patches carry the FULL arg list), buildCallSite clones a head patch onto the callSite root (the head's own arena root is unreachable by replay), and every per-constant meta assembly drains the channels. * tc+ixvm: regenerate primitive address pins for canonical univ tables (canonicity 10.6) Phase 2 L4 — mirrors the Phase-1 prim_addrs.rs regen: 56 canonical pins in Ix/Tc/Primitive.lean and 45 IxVM address literals (NatPrim 33, Infer 11, InferOnly 1), keyed old-hex→new-hex from the Phase-1 diff. LEON orig pins unchanged. prim-addrs gate (whole-toplevel literal scan) and tc-unit primsParity green. * validate-lean: stream per-phase section headings (ix-validate parity) Each phase now prints its section heading + result the moment it completes (flushed), with phase-start markers before the long legs and a final summary + RESULT line matching ix validate's format. End-only block-buffered output twice cost us the evidence of how far a killed whole-Mathlib run got. * decompile+tc: level-spelling patch replay and stage-2 decoration source (canonicity 10.6, Lean mirror) Phase 2 L2+L3 of plans/level_canonicalization_rust_first.md: - DecompileM (L2): BlockCtx.univPatches arena-index map from ConstantMeta; replay at sort/ref/recur arms and the surgered call-site head (patch cloned onto the callSite root by the compiler). Patch indices resolve through the ctx's already-extended univs ++ metaUnivs. The per-constant withFreshBlock design (fresh immutable ctx + fresh caches, primary ++ own extension per ctor) is structurally immune to the two Rust decompiler hazards fixed in Phase 1 (parent-extension displacement; stale univ-memo entries). - Tc IngressMeta (L3): decorations sourced from univPatches (virtual space univs ++ metaUnivs; arity-checked full-list const patches) at sort/ref/recur and both callSite head arms, with the stage-1 reduceIxonUniv-fixpoint rule as fallback (never fires on canonical tables, P3; keeps raw-table fixtures exercised). Module-doc contract updated: metaUnivs/univPatches are now META-ingress-read; anon stays metadata-blind. - Tc Egress (L3): phase 3 STRICT — both canonExpr bodies intern stored universe trees EXACTLY (reduceIxonUniv dropped; canonical tables are its fixpoints); module doc reworded, pre-normal-levels artifacts now fail the roundtrip by design (D4). - Tc Level + IxVM Levels (R5 mirror, option (b)): normLevelEq / nl_eq ignore empty subsumption entries (nl_skip_empty), making univEq / level_equal the exact semantic quotient, matching Rust norm_level_eq. Gates: tc-unit 390, decompile-unit, prim-addrs 80, ixvm, aux-gen-diff (byte-identical incl. wrapper vectors), decompile-diff (aux-fidelity 2243/0), tc-ingress-meta, tc-roundtrip (148,387 meta-checked) — all green. * docs: universe-level canonicalization is live (canonicity 10.6) Drop the staged banners and row markers; record the landed linearizer (per-atom gate inversion — formerly O1), the empty-entry-insensitive univEq (exact semantic quotient), the patch-first decoration source with the stage-1 fallback and the callSite-head re-key; add the 12.4 level-spelling-twin worked example; rewrite 17.9 as the landed record with the acceptance evidence (whole-Mathlib validate/validate-lean 0 failures, phase 4 714,346/0, byte-ALIGNED compilers, probe Géran-noncanonical 0). Ixon.md: univ-table canonicity invariant and the ConstantMeta wrapper struct with all four extension vectors incl. univPatches. * benchmarks: refresh post-canonicalization (10.6) numbers Regenerated .ixe sizes (canonical tables + univPatches), Mathlib compile/serialize timings from the ALIGNED runs, and the whole-Mathlib validate-lean column that was TBD pending the below.rec fix: phases 999.1 / 232.3 / 41.2 / 183.8 / 3,926.3 s, ~89.7 min total, 0 failures. Footnote for the phase-3 inversion (older InitStd/Lean figures predate the pointer-memo canonical compare). * style: cargo fmt * ixvm: regenerate aiur codegen and re-pin FFT costs for the canonical-univ kernel (canonicity 10.6) The 10.6 kernel changes (nl_skip_empty empty-entry skip in nl_eq + regenerated primitive address literals) change the generated Aiur image: regenerate crates/ixvm-codegen/src/aiur_ixvm.rs via ix codegen (aiur_multi_stark.rs regenerates byte-identical) and acknowledge the resulting FFT cost shifts — 66 kernel-check pins and the shard pipeline pin, all within ±0.3%, every functional/parity check green (728 passing). * style: clippy --workspace --all-targets --all-features -D warnings clean manual_contains in the diff probe; documented needless_pass_by_value allows on the quickcheck properties (the macro requires by-value Arbitrary arguments). * tc verify: repair Level and AnonStructural for the 10.6 kernel changes normLevelEq_eval rewritten for the empty-entry-insensitive comparator (canonicity 10.6 R5): the positional zip check makes the two entryNonEmpty-filtered entry lists literally equal, and dropped entries evaluate to 0, so equal denotations follow by le-antisymmetry through eval_le/le_eval — simpler than the old pigeonhole-over-sorted-keys argument. entryNonEmpty hoisted to a named def in Ix/Tc/Level.lean so the proofs can speak about it (comparator unchanged). AnonStructural's anon ExprInfo mirror gains the seventh (unit) univDecor field. Statement of normLevelEq_eval unchanged; trust audit passes for all 7 theorem roots (lake build Ix.Tc.Verify.Audit.Completed Ix.Tc.Verify.Audit.Statements green). * ixon: make the manual .ixe probes skip when unconfigured dump_reducible_univs / dump_named_metas / dump_const_sizes are env-driven manual probes (IXE_A=<path> cargo test -- --ignored --nocapture); CI's run-everything-ignored sweep (nextest --run-ignored all) force-runs them without inputs, where the expect on IXE_A panicked. They now print a skip note and return, keeping the sweep green without losing the documented manual usage.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.