Name decoding with global cache

Look up a compiled constant's address (with `aux_name_to_addr` fallback).

Content-addressed key for cache lookups. Returns the blake3 hash by value — `Addr` is `Copy`, so this is a 32-byte memcpy.

Returns the name of this mutual constant.

Largest single cache size. Cheap proxy for "how big did this block get" without summing. (Sum is misleading because the same content hash can appear i

The entry for block id `i`.

Allocate a new node in the arena, returning its index.

Clear all worker-local kernel state before checking another scheduled block or when a caller needs a fresh environment.

Build `op a b` using the canonical primitive address for `op`.

Build a forall chain by batch-abstracting all FVars in a single pass per sub-expression. `binders` is outermost-first. Each domain and the body are w

Build a lambda chain by batch-abstracting all FVars in a single pass. Same semantics as `mk_forall` but produces `λ (x : T), body`.

Serialize an expression to bytes (iterative to avoid stack overflow).

Record that `consumer` delta-unfolds the body of `producer`. Self-edges are ignored. Ensures both endpoints exist as blocks (with zeroed stats if not

`Nat` from a u64 via the public `From<u64>` impl. (The `Nat` type itself is a private re-export in `env.rs`.)

Helper: build `λ (_ : a), b`

Instantiate the outermost `n = fvars.len()` loose bound variables in `body` by the corresponding fvars, in reverse order (mirrors `Lean.Expr.instantia

Resolve a Lean Name to an Address, using real Ixon address if available. Checks `name_to_ixon_addr` first (real compiled address), falls back to `Add

Convert a Lean `Nat` to `usize`, returning `CompileError` on overflow. Use in functions that return `Result<_, CompileError>`.

Check that a Lean-side Expr matches a zero Expr<Anon> structurally.

Look up a declaration by its [`FVarId`]. Returns `None` if the fvar is not bound in this context.

Compile an entire Lean environment to Ixon format. Work-stealing compilation using crossbeam channels. Instead of processing blocks in waves (which u

Look up a Name by its address.

Calculate the encoded size of this tag in bytes.

Convenience: Eq.{u} α a b

Shift free de Bruijn indices ≥ `cutoff` up by `shift`. Used when substituting an argument into a deeper context. Like `subst`, memoizes by content ha

Perform single substitution: `body[arg/Var(depth)]`. Replaces `Var(depth)` with `arg` (lifted by `depth`), shifts free variables above `depth` down b

Env with: Nat (axiom), id (definition)

Decompile an Ixon environment back to Lean format. Single-pass parallel work-stealing scheduler. Computes SCCs over the name-level reference graph, t

WHNF, then ensure it's a Sort. Returns the universe level.

Convenience: Eq.refl.{u} α a

Whether any [`ExprData::FVar`] occurrence is reachable. Computed at construction time and propagated via OR through composite nodes, so the check is O

Infer the sort level of a type expression in the current context. Uses a fast path matching Lean's `inferAppType` (InferType.lean:79-91): for fully-a

Substitute universe parameters: replace `Param(i)` with `us[i]`. Returns `Err(UnivParamOutOfRange)` if any interior `Param(i)` has `i >= us.len()`. C

Convert a Lean `Nat` to `u64`, panicking on overflow.

Constructs a dependent function type (forall / Pi).

Compile a Lean expression to an Ixon expression. Builds arena-based metadata in cache.arena with bottom-up allocation.

Push additional locals (e.g. minor premise lambda binders). Must be balanced by a later `pop_locals` call.

Check if the head of `dom` (after peeling foralls) is one of the given `motive_fvars`. Returns `Some(class_index)` if matched. Substitute all occurre

Run a closure with `infer_only` mode enabled. Restores the previous mode on exit. In this mode, `infer` skips def-eq checks for App arg types and Let

Serialize with tag and compute content address: `blake3(0xE1 + secret + payload)`.

Build a constant with the given refs (for BFS tests). `discriminator` is folded into `lvls` so callers can produce content-distinct constants when the

Decode Ix.RawEnvironment from Lean object into HashMap. RawEnvironment = { consts : Array (Name × ConstantInfo) } NOTE: Unboxed to just Array. This ve

Decode a Lean environment in parallel with hybrid caching.