Generate a bounded-depth `KExpr<Anon>` with de Bruijn indices in `0..=max_var`. Leaf distribution is biased toward concrete data (Var/Sort/Const) to p

Deserialize a Name component using a lookup table for parents.

Deserialize a Named entry with indexed metadata.

Check whether the leafmost segment of `suffixes` (or the first segment underneath an `_N` suffix like `brecOn_1`) matches `base`. Accepted forms (wit

Raw `Level::imax`.

Insert a `Defn` with the given reducibility hints under `name`, returning its `KId`. Used by `def_rank_id` ordering tests.

Multi-argument reverse instantiation: replace BVar(0)..BVar(n-1) with `args[0]..args[n-1]` simultaneously, and decrement BVar(i >= n) by n. Matches L

Intern a universe: if one with the same hash exists, return the existing Arc (ensuring pointer uniqueness). Otherwise insert and return.

Check if expression is the Bool.true constant.

Check if a constant is delta-reducible.

Whether the context is trivial: identity permutation, empty const_map, and no rec heads to permute. If so, [`const_alpha_eq_with_perm`] delegates to p

Check if expression is nat zero (literal 0 or Nat.zero constructor).

A stable kind ordinal for cross-kind `KConst` comparison. Matches the compile-side `mut_const_kind` (`src/ix/compile.rs:2590`) tagging: Defn=0, Indc=1

Treat `limbs` as a little-endian sequence of 64-bit limbs and convert to a `BigUint`. Aiur's `klimbs_normalize` strips trailing zero limbs but a non-n

Construct `max(a, b)` with Lean-style simplifications: - `max(k₁, k₂) = max(k₁, k₂)` when both are explicit numerals - `max(a, a) = a` - `max(0, a) =

Build `@HEq.{u} α a β b`.

Replace the innermost return type of a forall chain with `unit`. Matches Lean's `mk_pi_unit` in `cases_on.cpp`: `∀ (x : A) (y : B), C x y` → `∀ (x :

Build a synthetic `Name` for a mutual block's `Named` entry: `Ix.<hex>.<first_member_name>`. Disambiguates alpha-equivalent blocks that share an `addr

Total canonical-layout minor count.

Total source-layout minor count.

Build N (Nat-like) environment with working recursor rules.

If expression is nat-succ, return the predecessor. Matches both `Nat(n+1)` → `Nat(n)` and `Nat.succ e` → `e`.

Dispatch `imax(a, b)` normalization based on `b`'s shape.

Normalize a level by applying `Level::max_smart` / `Level::imax_smart` bottom-up. Idempotent. `Succ` is left raw (see [`level_alpha_eq`]).

Normalize a universe level to Géran's canonical form.

Anonymous-name variant of [`Self::open_binder_with_fv`].

Size a partition to a per-shard **cycle** (guest-STEP) budget by **bin-packing to the cap**, not by balancing into a fixed shard count. `max_cycles`

Identify the `ConstantInfo` variant by reading just the outer `Tag4` head byte — no allocation, no body parse. `Tag4` encoding (see `src/ix/ixon/tag.

Build Quot environment: Quot, Quot.mk, Quot.lift, Quot.ind as KConst::Quot. Also includes Eq as full inductive (needed for Quot.lift validation).

Read raw bytes from the blob store.

Walk a `List<U64>` chain from `head_ptr` in `memory[10]`, returning the u64 limbs in head-first order. Each memory[10] entry is the standard Aiur tagg

Build a fresh `Named` entry for a reconstructed constant, preserving the original's `meta` and `original` (aux_gen regeneration hint) fields but with

Like [`replace_const_names`] but accepts a caller-managed memoization cache. Use this when calling the rewriter many times with the SAME `map` in a ti

Perform simultaneous substitution: replace `Var(depth)..Var(depth+n-1)` with `substs[0]..substs[n-1]`, shifting free variables above by `-n`. Uses th

Compute the source-walk discovery order of nested auxiliaries by running `expand_nested_block` on **source-order originals** (no alias rewriting, no c

Store a constant at its true content address and return that address. Use this instead of `store_const(Address::hash(b"a"), ...)` for tests that round

Store a Nat as a blob and return its address.

Serialize the verifying key `System<AiurCircuit>` (preprocessed traces are skipped — see the module docs).

Transitive dep addresses of `root`, excluding `root` itself. Sorted lex-ascending for canonical use (e.g., feeding `merkle_root_canonical`).

Try native reduction, matching C++ kernel's `reduce_native`. - `Lean.reduceBool arg`: look up `arg` (a constant), evaluate its body, return Bool - `Le

String literal expansion (C++ kernel: try_string_lit_expansion_core). When `t` is a string literal, expand it to constructor form via `str_lit_to_con

If the head of `e` is a projection, try reducing it via whnf_no_delta. Returns the reduced form if it changed, None otherwise (lean4lean tryUnfoldProj

Read a u64 from minimal little-endian bytes.

Write a u64 in minimal little-endian bytes.

Validate that a stored primary block ships in canonical (sort_consts) order. Walks adjacent pairs under the singleton partition and requires strong s

Validate declaration expressions before inference. This is the Ix equivalent of Lean's declaration-admission closure and universe-param checks: decla

Verify a merkle membership proof against any root (canonical or free-form). The path is shape-agnostic — verification just hashes upward using each si

Verify that a projection address computed from a block's structure is actually present in the env's consts. Wrapped here so the four dispatch arms in

WHNF without delta: whnf_core → proj-app → nat/native/string → quot. Projection values use full WHNF, preserving the public/full semantics.

Add `k` `Succ` wrappers to `l`. Matches Lean's `Level.addOffset`.

Collect every (field_name, addr) pair from `PrimAddrs` via reflection over a macro invocation at the caller — done here by an inline array. Keep in lo

Lower the bisection tree to an arity-bounded fold plan. The binary tree is collapsed* so each agg call folds up to `arity` whole subtrees (never split

Build And : Prop → Prop → Prop with And.intro constructor.

Deterministic CPrj content address for ctor `(idx, cidx)` of `block`.

Convert a `BelowIndc` (Prop-level `.below`) to an `InductiveVal` and its constructors. Safety mirrors the parent via `BelowIndc::is_unsafe` (see the

The ingress-block address that owns `addr`: a projection (IPrj/CPrj/RPrj/ DPrj) maps to its Muts `block`; anything else is its own block. Used to map

Build Bool environment with working recursor rules.

Emit `node`'s plan entries; return the index of the entry representing it.

Build an `IO (Array (Option CheckError))` from Rust results. The Lean caller pairs each slot with `names[i]` (the input array) for display, so there'

Build a simple Type-level inductive (Nat-like): T | Z : T | S : T → T