# 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 `; 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`._