Materialize the `Constant`. If this entry was built via [`Self::from_constant`], returns the pre-populated cached `Arc` (zero-cost clone). Otherwise

Open lambda binders into FVars (matching forall_telescope but for lambdas).

Build `PProd.{u, v} a b` with separate universe levels for each component. Matches Lean's `mkPProd` which infers levels from the actual types. Caller

Number of blocks (vertices).

Anonymous variant of [`Self::open_binder`] that uses `Name::anon()` / `BinderInfo::Default`. Convenient for kernel-internal walks (inductive validatio

Read exactly 32 bytes (Address) from a byte slice, advancing the cursor.

Register a Name in `stt.env.names` so `decompile_name` can resolve it. Mirrors `compile_name` (content-address the name, insert into names map).

Reset thread-local state between constants. Global caches in `KEnv` are NOT cleared — they grow monotonically and are shared across all TCs.

Recursively compute the root hash.

Compile a batch of regenerated `MutConst`s as a mutual block (mirroring `compile_aux_block`), then decompile each member with original metadata from `

Write bytes to the store and return their address (blake3 hash)

Apply sharing analysis to a set of expressions. Returns the rewritten expressions, sharing vector, and hash-consed size. Hash-consed size tracking is

Build a Lean Nat from a usize.

Check with custom primitives (needed for Nat literal tests etc.)

Compare two Lean expressions structurally for canonical ordering. Strips `Mdata` wrappers, compares by constructor tag, then recurses into subexpressi

Compile a single constant.

Compile a mutual block. When `aux` is true, auxiliary constants (`.rec`, `.below`, `.brecOn`) are regenerated for alpha-collapsed blocks via `generat

True iff `target` appears as a `Leaf` somewhere in the tree.

Compute content address of an Ixon `Constant` by serializing and hashing.

Decode Ix.Int from Lean object. Ix.Int: ofNat (tag 0, 1 field) | negSucc (tag 1, 1 field)

Discover all inductives in a mutual block.

Convert a zero kernel universe to a Lean level.

Get the major premise's inductive KId from a recursor type. Strategy: peel `skip` foralls per Lean's stored `params + motives + minors + indices` cou

Get a name by address.

Get the result sort level of a type after peeling `n` foralls.

Extract the value expression from a ConstantInfo, if it has one.

Check that two Lean levels are equal modulo the same simplifications `Level::max_smart` / `Level::imax_smart` perform. Why normalize: `aux_gen::expr_

Install per-constant metadata extension tables. - `meta_sharing` → dedicated `self.meta_sharing` (separate from the block sharing, see struct docs).

Helper: build test `name : PropStructure.{0,1} → resType := fun x => .proj PropStructure idx x`

`∀ (a : α) (b : β) (c : γ), body`

Total source-layout motive count: `n_primary + n_source_aux`.

Promote a constant from `aux_name_to_addr` to `name_to_addr`, setting `Named.original` to the given `(orig_addr, orig_meta)` from the ephemeral no-aux

Build PUnit.{u} + Eq + PropStructure.{u,v} env.

Build `PUnit.{u}` (the type, at `Sort (u+1)`)

Delegate indexed serialization to the inner enum, then serialize extension tables.

Helper: write an `Option<Address>` as `[0x00]` (None) or `[0x01][addr:32]` (Some). Single byte for absence avoids a 33-byte gap when assumptions are a

Quick structural: same constructor, recursively same children (no WHNF).

Serialize to a fresh Vec.

Sort mutual constants into a canonical ordering and group equal ones. Uses iterative refinement: sort by structure, group equals, re-sort with updated

Store `c` at its true content address; returns the address. Tests that serialize+deserialize through `Env::put`/`Env::get` must use canonical addresse

Strip Mdata wrappers from an expression.

Substitute universe params in a universe level. Fails with `UnivParamOutOfRange { idx, bound }` if an interior `Param(idx)` references beyond `us.len

Serialize to the `.ixes` binary format.

Two tight clusters {1,2,3} and {4,5,6} with heavy intra-cluster delta and a single thin cross edge. A good bisection cuts only the thin edge.

Build a rec type: `∀ {motive : P → Prop} (mk : motive P.mk) (t : P), motive t`

Build an env that includes the full USize.size reduction chain: System.Platform.numBits (handled by try_reduce_native → 64) Nat.pow at the correct pri

Convert a Vec<Name> to a MutCtx. Each name gets its position as the Nat value.

Apply sharing to a Recursor and return a Constant with stats.

BFS-collect all addresses transitively reachable from `root` via the `Constant.refs` field. The returned set includes `root` itself. Addresses that a

Predicted Zisk guest STEPS contributed by a single block (reduction + its own ingress). The per-shard floor and any cross-shard re-ingress are added a

The block entries, indexed by block id.

Build a check claim for the constant at `const_addr` in `env`. Sets `assumptions: None` when the constant has no transitive deps, else `Some(root)` w

Build a flat block from an ordered list of original inductives. Detects nested inductive occurrences in constructor fields and creates auxiliary entr

Helper: build a minimal Lean environment with mutual inductives.

Validate a standalone constructor against its parent inductive. Runs the same A1–A4 checks that `check_inductive_member` runs per-ctor.

Compare two block-eligible `KConst`s with full structural ordering. Different kinds order by `kconst_kind_ord`; same-kind dispatch goes to the kind-sp

Like `compile_aux_block`, but applies an optional name-rename map when registering named entries in the env. The rename maps *canonical* constant nam

Compare a canonical-layout generated constant against a Lean source-order original, with [`PermCtx`] describing how positions map between the two layo

Compute the content-addressed hash for a Constant.

Count leading foralls (local helper to avoid name collision with the pub(super) count_foralls in below.rs).