Convert a MutCtx to a Vec<Name> ordered by index. Position i contains the name with Nat value i.

Decode a Lean Ixon.SerializeError to a Rust SerializeError.

Extract level param names from ConstantMeta.

Decompile a name from ConstantMeta.

Compare a generated definition / theorem / opaque against its orig counterpart with permutation awareness. Handles the types/values produced by `aux_

Find root with path halving (every other node → grandparent).

Generate all canonical auxiliary patches for a collapsed inductive block. Called from `compile_mutual` after `sort_consts` determines the canonical c

Generate all `.brecOn` (and `.brecOn.go` for Type-level) constants. Called after Phase 2 (`.below` generation). Uses the canonical recursors from Pha

Deserialize a raw 32-byte address.

Compute this block's selector as the sum of its immediate children's selectors. For leaf blocks (Return/Yield) this is the single selector variable. F

Strip all outermost Succ wrappers. Matches Lean's `Level.getLevelOffset`.

Returns the universe level parameter names of this constant.

Returns the name of this constant.

Extract head constant KId from expression or app spine.

Append a new entry. The key must not already be present: call sites only insert on a confirmed miss, and a same-key re-entrant call would loop forever

Convert spec_params from BVar form to FVar form. Spec_params use BVars relative to the param context: BVar(0) is the last (innermost) param, BVar(n_p

Check whether a constant name has an aux_gen suffix that should be regenerated rather than decompiled from Ixon. Used by both the decompile-time "ski

Apply `const_map` to an orig-side const name; returns the original name if no mapping exists.

Recursively flatten a level into canonical form, accumulating into `acc`. `path` tracks the imax-conditioning chain, `k` is the accumulated succ offse

Peel the outermost constant offset: returns `(base, n)` where `self = Succ^n(base)` and `base` is not `Succ`.

Like [`Self::partition`], but also returns the **bisection tree** — the binary tree of min-cut splits whose leaves are the shard ids. Reusing this as

Producer block ids unfolded by consumer block `c` (sorted, deduped, no self-edges).

Serialize a raw 32-byte address (for blob addresses not in the name index).

Raw serialized bytes (the Tag4 constant body, no length prefix).

Read a string from the blob store.

Record the fuel actually consumed by a single constant check. Updates both the running max and the cumulative total. No-op when disabled.

Resolve a list of **Lean-name-hash** addresses to `KId<M>` pairs whose `addr` is the **projection-content address** under which the corresponding KCon

Translate a source-layout scope position to its canonical-layout counterpart for an abstract section = "params + motives + minors". Returns `None` if

Deterministic DPrj content address for member `idx` of `block`.

Deterministic IPrj content address for member `idx` of `block`. Thin re-export of `ixon::constant::indc_proj_address` — the canonical projection-addr

Deterministic RPrj content address for member `idx` of `block`.

Single-pass FVar→BVar abstraction for an entire binder telescope. Replaces all FVars (identified by `fvar_map`) with the correct BVar indices in one

Convert a `BigUint` to LE-u64 limbs. The output is non-padded (trailing limbs that would all be zero are omitted), matching `klimbs_normalize`'s canon

Build a `List<U64>` chain in `memory[10]` from `limbs` (head-first order) and return the head pointer. Each entry is inserted with multiplicity 0 (unc

Build one `Option CheckError` object from a Rust check result. - `Ok(())` → `none` - `Err((Kernel, msg))` → `some (CheckError.kernelExc

Rewrite expressions to use Share(idx) references for shared subterms. Returns the rewritten expressions and the sharing vector.

Build a result array of length `count` where every slot is the same compile-kind error. Used when compile/ingress/thread setup fails before per-consta

Check that decompiled environment matches the original. Counts and logs hash mismatches (which indicate metadata loss or decompilation errors).

Validate an inductive type and its constructors.

Validate a recursor by comparing with generated canonical form.

Rewind over the currently-buffered ephemeral label (if any) so the next write lands in column 0 of the topmost affected row.

Clear worker-local state and drop backing allocations. `clear()` preserves `HashMap` capacity, which is useful for reuse but problematic for full-env

Compile a Definition. Arena persists across type + value within a constant.

Compile a mutual block with block-level sharing. Returns the Constant, its content-addressed hash, and size statistics.

Compile a Recursor. Arena grows across type and all rule RHS expressions.

Decompose this name into its components (from root to leaf).

Compute effective sizes for all subterms in topological order. Returns a map from hash to effective size (total serialized bytes).

Decompile a Definition.

Decompile a Recursor. Arena covers type + all rule RHS expressions with rule_roots.

Helper: decompile universe indices to Lean levels.

Reducibility rank by id. Higher rank = unfold first. Returns a `(class, height)` tuple compared lexicographically, so that `Abbrev` strictly dominate

Map an `is_unsafe` flag to a `DefinitionSafety`. The decompile side uses this to stay in lock-step with `ix::compile::mutual::def_safety`; if we ever

Map an `is_unsafe` flag to a `DefinitionSafety`. Isolated here so every aux-constant emission site picks up the same rule; if we ever need to distingu

Build environment with Bool + Eq as full inductives (not just axioms). Eq.{u} : {α : Sort u} → α → α → Prop (indexed, 2 params, 1 index) Eq.refl.{u} :

Build an expanded block by replacing nested inductive occurrences with auxiliary types that share the block's parameters and universe levels. Matches

Check if BVar(`target`) appears anywhere in `e`.

Clear any trailing ephemeral output so subsequent prints start on a fresh line. Safe to call when nothing is buffered.

Small helper: distinct random addresses.