Value

Values are the semantic domain produced by evaluation. They use de Bruijn levels (counting outward from the top of the context), not indices, which makes weakening trivial.

Closures

mkClosure : Env → Tm → Closure — defunctionalized closure. No Nix lambdas in the TCB; a closure is { env, body } where body is a kernel Tm evaluated by eval.instantiate.

Value Constructors

Each v* constructor mirrors a term constructor:

• vLam, vPi — function values/types (carry name, domain, closure)
• vSigma, vPair — pair types/values
• vUnit, vTt — unit
• vBootSum, vBootInl, vBootInr — bootstrap coproduct values
• vBootEq, vBootRefl — identity values
• vU — universe values
• vString, vInt, vFloat, vAttrs, vPath, vDerivation, vFunction, vAny — primitive types
• vStringLit, vIntLit, vFloatLit, vAttrsLit, vPathLit, vDerivationLit, vFnLit, vAnyLit — primitive literals

Neutrals

vNe : Level → Spine → Val — a stuck computation: a variable (identified by de Bruijn level) applied to a spine of eliminators.

freshVar : Depth → Val — neutral with empty spine at the given depth. Used during type-checking to introduce fresh variables under binders.

Elimination Frames (Spine Entries)

• eApp, eFst, eSnd — function/pair eliminators
• eBootSumElim, eBootJ — inductive eliminators

eAbsurd

eAbsurd: elimination frame for absurd on a neutral Empty-typed scrutinee — carries the target type P; sound because Empty has no canonical inhabitants, so this frame can only arise on a stuck spine.

eAbsurd : Val -> SpineEntry  -- type P

eAllD

eAllD: elimination frame for allD on a neutral description — carries motive P plus shape parameters.

eAllD : Val -> Val -> Val -> Val -> Val -> Val -> SpineEntry

eApp

eApp: elimination frame for function application — pushes an argument onto a neutral spine.

eApp : Val -> SpineEntry

eBootJ

eBootJ: elimination frame for the J eliminator on a neutral identity proof — carries A, a, motive, refl-case, b.

eBootJ : Val -> Val -> Val -> Val -> Val -> SpineEntry

eBootSumElim

eBootSumElim: elimination frame for bootSumElim on a neutral sum scrutinee — carries motive and case arms.

eBootSumElim : Val -> Val -> Val -> Val -> Val -> SpineEntry

eDescInd

eDescInd: elimination frame for descInd on a neutral μ-typed scrutinee — carries I, D, motive, step.

eDescInd : Val -> Val -> Val -> Val -> SpineEntry

eEverywhereD

eEverywhereD: elimination frame for everywhereD on a neutral description — carries per-node f plus shape parameters.

eEverywhereD : Val -> Val -> Val -> Val -> Val -> Val -> Val -> SpineEntry

eFst

eFst: elimination frame for first-projection on a Σ neutral.

eIntEq

eIntEq: intEq frame on a neutral int operand — carries the other operand (symmetric).

eIntEq : Val -> SpineEntry

eIntLeL

eIntLeL: intLe frame where the neutral operand is the lhs — carries the rhs.

eIntLeL : Val -> SpineEntry

eIntLeR

eIntLeR: intLe frame where the neutral operand is the rhs — carries the lhs.

eIntLeR : Val -> SpineEntry

eInterpD

eInterpD: elimination frame for interpD on a neutral description — carries k, I, X, i for completion when the neutral resolves.

eInterpD : Val -> Val -> Val -> Val -> SpineEntry

eLiftElim

eLiftElim: elimination frame for liftElim on a neutral Lift l m A — carries l, m, A for level lowering.

eLiftElim : Val -> Val -> Val -> SpineEntry

eSnd

eSnd: elimination frame for second-projection on a Σ neutral.

eSquashElim

eSquashElim: elimination frame for squashElim on a neutral Squash-typed scrutinee — carries motive shape (A, B) and case function f.

eSquashElim : Val -> Val -> Val -> SpineEntry

eStrEq

eStrEq: elimination frame for strEq on a neutral string operand — carries the other operand for completion when the neutral resolves.

eStrEq : Val -> Val -> SpineEntry

eStrLen

eStrLen: elimination frame for strLen on a neutral string operand — nullary; the stuck operand is the spine head, so the frame carries nothing.

eStrLen : SpineEntry

envCons

envCons: O(1) environment extension — prepend a value as index 0; no list copy, no cached field.

envCons : Val -> Env -> Env

envFromList

envFromList: normalize a Nix-list environment to cons cells (index 0 = list head); idempotent on cons (isList guard) so evaluator entry points normalize in O(1) on already-cons inputs.

envFromList : [Val] | Env -> Env

envLen

envLen: environment length (binder depth) via an iterative genericClosure spine walk — O(N) time, O(1) stack (overflow-free); no cached field, which would recurse N-deep at read or build.

envLen : Env -> Int

envNil

envNil: empty de Bruijn environment (the cons-cell nil).

envNth

envNth: iterative de Bruijn lookup (foldl' over a range) — clears the C-stack and max-call-depth on deep environments; a plain Nix list is indexed verbatim (isList guard) so elaborate-layer list-contexts pass through unchanged.

envNth : Env -> Int -> Val

envPrepend

envPrepend: prepend a short Nix list of values (index 0 first) onto an environment.

envPrepend : [Val] -> Env -> Env

envToList

envToList: materialize a de Bruijn spine into an index-ordered Nix list (index 0 = most recent) via an iterative genericClosure walk — O(N) time, O(1) stack (overflow-free). For whole-context reads (any/map/filter over every binding); a plain Nix list passes through verbatim (isList guard), null yields the empty list. Inverse of envFromList on cons inputs.

envToList : Env -> [Val]

freshVar

freshVar: introduce a fresh neutral variable at the given depth — used during type-checking to bind a fresh witness under Π / Σ / let binders.

freshVar : Int -> Val  -- depth

mkClosure

mkClosure: defunctionalised closure { env, body } — captures the evaluation environment and the kernel Tm body; instantiated by eval.instantiate without Nix lambdas in the TCB.

mkClosure : Env -> Tm -> Closure

vAllD

vAllD: value-domain induction-hypothesis collector — threads motive P through every recursive position in a payload.

vAllD : Val -> Val -> Val -> Val -> Val -> Val -> Val -> Val

vAny

vAny: value-domain axiomatised top primitive Any : U(0) — accepts every Nix value.

vAnyLit

vAnyLit: value-domain literal carrying an arbitrary Nix value v : Any — used by approximate types whose kernel slot is vAny.

vAnyLit : Any -> Val

vAttrs

vAttrs: value-domain axiomatised primitive Attrs : U(0) — inhabited by any Nix attrset.

vAttrsLit

vAttrsLit: value-domain literal carrying an opaque Nix attrset a : Attrs.

vAttrsLit : Attrs -> Val

vBootEq

vBootEq: value-domain bootstrap identity type Eq(A, a, b) — propositional equality used by descRet's level transport and by the J eliminator.

vBootEq : Val -> Val -> Val -> Val  -- A, a, b

vBootInl

vBootInl: value-domain left-injection inl(a) : A + B — carries leftTy and rightTy for elaboration shape recovery.

vBootInl : Val -> Val -> Val -> Val  -- leftTy, rightTy, value

vBootInr

vBootInr: value-domain right-injection inr(b) : A + B — carries leftTy and rightTy for elaboration shape recovery.

vBootInr : Val -> Val -> Val -> Val  -- leftTy, rightTy, value

vBootRefl

vBootRefl: value-domain reflexivity refl : Eq(A, a, a) — canonical inhabitant of every reflexive identity; conv collapses all proofs of refl to this.

vBootSum

vBootSum: value-domain bootstrap coproduct type A + B — used by descPlus's sum-of-descriptions before generic sums become available.

vBootSum : Val -> Val -> Val

vDerivation

vDerivation: value-domain axiomatised primitive Derivation : U(0) — Nix derivation values; the store-producing irreducible value category.

vDerivationLit

vDerivationLit: value-domain literal carrying a Nix derivation d : Derivation opaquely.

vDerivationLit : Derivation -> Val

vDesc

vDesc: value-domain level-zero description type Desc I k at index sort I : U(0) and universe level k.

vDesc : Val -> Val -> Val  -- level, I

vDescAt

vDescAt: value-domain Desc^k I carrying an explicit iLev for the universe of I. The conv unfolding rule reads iLev to construct the expected mkDescDescAppV D-slot.

vDescAt : Val -> Val -> Val -> Val  -- level, iLev, I

vDescCon

vDescCon: value-domain constructor descCon(D, i, payload) — the canonical introducer for μ I D i values.

vDescCon : Val -> Val -> Val -> Val  -- D, i, payload

vDescConChain

vDescConChain: flat-chain VDescCon for linearChain Descs. .d is stub vTt; chain lives in _layers (Nix list, outer-first) + _base. Chain-wide BootSum wrapper info on _payloadTag/_payloadLeft/_payloadRight. Outer cert is _layers[0].cert. O(1) libnix stack on deep force; non-chain-aware consumers crash on .d.fst rather than silently mis-reading a degenerate view.

vDescConChain : Val -> Val -> String -> Val -> Val -> [LayerRec] -> Val -> Val  -- D, i, payloadTag, payloadLeft, payloadRight, layers, base

vDescConTagged

vDescConTagged: value-domain descCon stamped with a canonical-reference identity _canonRef = { id; params } for conv and quote short-circuiting; skips forcing .D on known descriptions, breaking universe-level descent loops. Carries no proof or certificate — _canonRef is a conv/quote identity tag only.

vDescConTagged : Val -> Val -> Val -> Val -> Val  -- D, i, payload, _canonRef

vEmpty

vEmpty: value-domain empty type — initial type with no inhabitants; conv-equal in one step by tag identity.

vEverywhereD

vEverywhereD: value-domain payload-traversal combinator — applies per-node f at every recursive position, producing a same-shape derived payload.

vEverywhereD : Val -> Val -> Val -> Val -> Val -> Val -> Val -> Val -> Val

vFloat

vFloat: value-domain axiomatised primitive Float : U(0).

vFloatLit

vFloatLit: value-domain literal carrying a Nix float x : Float.

vFloatLit : Float -> Val

vFnLit

vFnLit: value-domain literal carrying an opaque Nix function — fnBox preserves thunk identity for conv reflexivity.

vFnLit : FnBox -> Val

vFunction

vFunction: value-domain axiomatised primitive Function : U(0) — opaque-function carrier.

vFunext

vFunext: value-domain funext axiom — given pointwise equality, produces equality of functions at Π(a:A). B a.

vFunext : Val -> Val -> Val -> Val -> Val -> Val

vInt

vInt: value-domain axiomatised primitive Int : U(0).

vIntLit

vIntLit: value-domain literal carrying a Nix integer n : Int.

vIntLit : Int -> Val

vInterpD

vInterpD: value-domain interpretation interpD D X i — yields the payload type for a constructor described by D against carrier X.

vInterpD : Val -> Val -> Val -> Val -> Val -> Val  -- k, I, D, X, i

vLam

vLam: value-domain lambda λ(name : domain). body — carries a defunctionalised closure rather than a Nix function, keeping the TCB Nix-lambda-free.

vLam : String -> Val -> Closure -> Val

vLazyDescIndAccLayer

vLazyDescIndAccLayer: MACHINE-INTERNAL deferred accumulator layer of a descInd linear chain. Applying expands via four kAppVV frames (step i d (vPair prevAcc vTt) arg); never escapes runMachineAtF.

vLazyDescIndAccLayer : Val -> Val -> Val -> Val -> Val  -- step, i, d, prevAcc

vLevel

vLevel: value-domain Level type Level : U(0).

vLevelLit

vLevelLit: value-domain concrete Level literal n : Level — derived from a Nix integer at evaluation time.

vLevelLit : Int -> Val

vLevelMax

vLevelMax: value-domain pointwise max max(l, r) : Level — used for universes of dependent products / pairs across distinct levels.

vLevelMax : Val -> Val -> Val  -- l, r

vLevelSuc

vLevelSuc: value-domain successor of a Level expression suc(l) : Level.

vLevelSuc : Val -> Val

vLevelZero

vLevelZero: value-domain level-zero literal 0 : Level.

vLift

vLift: value-domain Tarski lift Lift l m A — non-cumulative cross-level transport of type A : U(l) into U(m) with l ≤ m.

vLift : Val -> Val -> Val -> Val  -- l, m, A

vLiftIntro

vLiftIntro: value-domain introduction of Lift l m A — lifts a term a : A at level l to a term at level m.

vLiftIntro : Val -> Val -> Val -> Val -> Val  -- l, m, A, a

vMu

vMu: value-domain levitated fixpoint μ I D i — carrier type of values whose constructors are described by D at index i.

vMu : Val -> Val -> Val -> Val  -- I, D, i

vNe

vNe: neutral value — stuck computation var^lvl <spine>; head is a de Bruijn level, spine is a list of elimination frames awaiting reduction.

vNe : Int -> Spine -> Val  -- level, spine

vNeSnoc

vNeSnoc: O(1) neutral-spine extension — append one elimination frame via the skew-binary RAL backing _ral, keeping .spine a materialized in-order list. Use in place of vNe lvl (n.spine ++ [frame]) to avoid the O(N²)/overflow-prone Nix-list snoc.

vNeSnoc : Val -> SpineEntry -> Val  -- neutral, frame

vOpaqueLam

vOpaqueLam: value-domain opaque lambda over a Nix function — kernel never inspects it; fnBox thunk identity preserves conv reflexivity.

vOpaqueLam : FnBox -> Val -> Val  -- fnBox, piType

vPair

vPair: value-domain pair (fst, snd) — components held in WHNF, projected by eFst / eSnd spine frames.

vPair : Val -> Val -> Val

vPath

vPath: value-domain axiomatised primitive Path : U(0).

vPathLit

vPathLit: value-domain literal carrying a Nix path p : Path.

vPathLit : Path -> Val

vPi

vPi: value-domain dependent function type Π(name : domain). codomain — carries a closure for the codomain to permit semantic substitution.

vPi : String -> Val -> Closure -> Val

vSigma

vSigma: value-domain dependent pair type Σ(name : fst). snd — carries a closure for the snd component to permit semantic substitution.

vSigma : String -> Val -> Closure -> Val

vSquash

vSquash: value-domain propositional truncation Squash A — quotient of A collapsing all inhabitants to one for proof-irrelevant fields.

vSquash : Val -> Val

vSquashIntro

vSquashIntro: value-domain introduction of Squash A — lifts any inhabitant of A to the sole inhabitant of Squash A.

vSquashIntro : Val -> Val

vString

vString: value-domain axiomatised primitive String : U(0).

vStringLit

vStringLit: value-domain literal carrying a Nix string s : String.

vStringLit : String -> Val

vThunkTm

vThunkTm: MACHINE-INTERNAL deferred-Tm Val produced by ev on non-atomic Tms. Captures { env; tm }; the driver's Done handler forces top-level VThunkTm before returning, so external code observes it only in stored sub-Val fields.

vThunkTm : Env -> Tm -> Val

vTt

vTt: value-domain unit value tt — sole inhabitant of vUnit; conv collapses all Unit-typed values to this.

vU

vU: value-domain universe U(level) — the type of types at a given Level value.

vU : Val -> Val

vUnit

vUnit: value-domain unit type — terminal type with single inhabitant vTt; eta-converted in conv.