# Kernel Formal Specification This document is the contract the implementation must satisfy. Every typing rule, compute rule, and conversion rule is stated precisely. Every test is derived from this spec. Every invariant the kernel must maintain is listed. The spec uses standard type-theoretic notation. No Nix code appears here — this document is reviewable by anyone who reads dependent type theory, regardless of implementation language. --- ## 1. Trust Model The kernel has three layers with strictly decreasing trust requirements. **Layer 0 — Trusted Computing Base (TCB).** The evaluator, quotation, and conversion checker. Pure functions. No side effects. No imports from the effect system. Bugs here compromise soundness. Every line must be auditable. - `eval : Env × Tm → Val` - `quote : ℕ × Val → Tm` - `conv : ℕ × Val × Val → Bool` **Layer 1 — Semi-trusted.** The bidirectional type checker. Uses the TCB and sends effects for error reporting. Bugs here may produce wrong error messages or reject valid terms, but cannot cause unsoundness (the TCB rejects ill-typed terms independently). - `check : Ctx × Tm × Val → Tm` - `infer : Ctx × Tm → Tm × Val` - `checkTypeLevel : Ctx × Tm → Tm × ℕ` **Layer 2 — Untrusted.** The elaborator. Translates surface syntax (named variables, implicit arguments, level inference, eta-insertion) into fully explicit core terms. Can have arbitrary bugs without compromising safety — the kernel verifies the output. ### Failure modes | Condition | Response | Rationale | |-----------|----------|-----------| | Kernel invariant violation | `throw` (crash) | TCB may be buggy; cannot trust own output | | User type error | Effect `typeError` | Normal operation; handler decides policy | | Normalization budget exceeded | `throw` (crash) | Layer 0 has no effect access; `tryEval` catches it | | Unknown term tag | `throw` (crash) | Exhaustiveness violation = kernel bug | --- ## 2. Syntax ### 2.1 Terms (Tm) The core term language. All binding uses de Bruijn indices. Name annotations are cosmetic (for error messages only). ``` Tm ::= -- Variables and binding | Var(i : ℕ) -- de Bruijn index | Let(n : Name, A : Tm, t : Tm, u : Tm) -- let n : A = t in u -- Functions | Pi(n : Name, A : Tm, B : Tm) -- Π(n : A). B | Lam(n : Name, A : Tm, t : Tm) -- λ(n : A). t | App(t : Tm, u : Tm) -- t u -- Pairs | Sigma(n : Name, A : Tm, B : Tm) -- Σ(n : A). B | Pair(a : Tm, b : Tm) -- (a, b) | Fst(t : Tm) -- π₁ t | Snd(t : Tm) -- π₂ t -- Unit | Unit -- ⊤ | Tt -- tt -- Empty | Empty -- ⊥ | Absurd(P : Tm, x : Tm) -- empty-type eliminator -- Bootstrap coproduct, private to descPlus interpretation | BootSum(A : Tm, B : Tm) -- A + B | BootInl(A : Tm, B : Tm, t : Tm) -- inl t | BootInr(A : Tm, B : Tm, t : Tm) -- inr t | BootSumElim(A : Tm, B : Tm, P : Tm, l : Tm, r : Tm, s : Tm) -- private eliminator for descPlus payloads -- Bootstrap identity, private to descRet/Lift/index transport | BootEq(A : Tm, a : Tm, b : Tm) -- internal Id_A(a, b) | BootRefl -- internal refl | BootJ(A : Tm, a : Tm, P : Tm, pr : Tm, b : Tm, eq : Tm) -- private identity eliminator | Funext -- function extensionality axiom -- Propositional truncation | Squash(A : Tm) -- proof-irrelevant truncation | SquashIntro(a : Tm) -- introduction into Squash | SquashElim(A : Tm, B : Tm, f : Tm, x : Tm) -- recTrunc: A -> Squash B, Squash A -> Squash B -- Levels (Tarski-style sort of universe levels — see §6.6, §8.5) | Level -- the Level sort itself, lives at U(0) | LevelZero -- 0 | LevelSuc(k : Tm) -- successor: k+1 | LevelMax(a : Tm, b : Tm) -- join in the level semilattice -- Universes (level-indexed, k : Level) | U(k : Tm) -- Type_k -- Descriptions (universe-polymorphic; see §7.6) | Desc(K : Tm, I : Tm) -- Desc^K I — descriptions over index type I | DescRet(j : Tm) -- ret(j) — leaf returning at index j | DescArg(K : Tm, S : Tm, T : Tm) -- arg^K S T — non-recursive Π over S : U(K) | DescRec(j : Tm, D : Tm) -- rec(j) D — recursive child at index j, then D | DescPi(K : Tm, S : Tm, f : Tm, D : Tm) -- π^K S f D — recursive Π over S : U(K), indexed by f | DescPlus(A : Tm, B : Tm) -- A + B — first-class binary coproduct of descriptions | DescDescApp(I : Tm, L : Tm) -- canonical descDesc I L reference | InterpD(level : Tm, I : Tm, D : Tm, X : Tm, i : Tm) -- interpretation of D at index i | AllD(level : Tm, I : Tm, D : Tm, K : Tm, X : Tm, M : Tm, i : Tm, d : Tm) -- all recursive positions satisfy M | EverywhereD(level : Tm, I : Tm, D : Tm, K : Tm, X : Tm, M : Tm, ih : Tm, i : Tm, d : Tm) -- builds AllD evidence from ih | DescInd(D : Tm, motive : Tm, step : Tm, i : Tm, scrut : Tm) -- generic μ-induction over D at index i -- μ-types (description-induced datatypes) | Mu(I : Tm, D : Tm, i : Tm) -- μ I D i — the i-th type in the family classified by D | DescCon(D : Tm, i : Tm, payload : Tm) -- introduction at index i with payload : interp(D, i) -- Annotations | Ann(t : Tm, A : Tm) -- (t : A); may carry trusted/label sidecars -- Lift | Lift(l : Tm, m : Tm, eq : Tm, A : Tm) | LiftIntro(l : Tm, m : Tm, eq : Tm, A : Tm, a : Tm) | LiftElim(l : Tm, m : Tm, eq : Tm, A : Tm, x : Tm) -- Axiomatized primitive types | String -- string type | Int -- integer type | Float -- float type | Attrs -- attribute set type | Path -- path type | Derivation -- derivation attrset type | Function -- opaque function type | Any -- dynamic/any type -- String operations | StrEq(lhs : Tm, rhs : Tm) -- string equality: lhs == rhs → H.bool (derived) -- Primitive literals | StringLit(s) -- string literal | IntLit(n) -- integer literal | FloatLit(f) -- float literal | AttrsLit -- attribute set literal | PathLit -- path literal | DerivationLit -- derivation attrset literal | FnLit -- opaque function literal | AnyLit -- any literal -- Opaque lambda trust boundary for extracted Nix functions | OpaqueLam(fnBox, piTy : Tm) -- Closed-Val splice (two-level TT reflection) | LitVal(v : Val) -- opaque carrier; eval is identity on v ``` Public `Nat`, `List`, `Sum`, `Bool`, `Fin`, `Vec`, `Eq`, and `W` are not primitive core syntax. The HOAS prelude generates them as descriptions: ``` H.nat = Mu(Unit, NatDT.D, Tt) H.listOf A = Mu(Unit, ListDT.D A, Tt) H.sum A B = Mu(Unit, SumDT.D 0 A B, Tt) H.eq A a b = Mu(A, EqDT.D A a, b) ``` Their constructors and eliminators elaborate to `DescCon` and `DescInd` applications through the datatype macro layer. The kernel therefore exposes one public induction principle for data: `DescInd`. The bootstrap coproduct and bootstrap identity above remain internal support for description interpretation, `DescRet`, `Lift`, and index transport. ### 2.2 Binding convention In `Pi(n, A, B)`, `Lam(n, A, t)`, `Sigma(n, A, B)`, and `Let(n, A, t, u)`: the body (`B`, `t`, or `u`) binds one variable. Index 0 in the body refers to the bound variable. All other indices shift by 1. Eliminators take their motives as ordinary function terms, not as implicit binders. Generated public eliminators build typed HOAS applications to datatype-specific eliminator functions; the core eliminator underneath is `DescInd`. ### 2.3 De Bruijn index conventions Indices count inward from the use site: 0 = most recent binder. Example: `λ(x : A). λ(y : B). x` is `Lam(x, A, Lam(y, B, Var(1)))`. --- ## 3. Values (Semantic Domain) Values are the result of evaluation. They use de Bruijn **levels** (counting outward from the top of the context) instead of indices. ``` Val ::= -- Functions | VPi(n : Name, A : Val, cl : Closure) -- Π type | VLam(n : Name, A : Val, cl : Closure) -- λ abstraction -- Pairs | VSigma(n : Name, A : Val, cl : Closure) -- Σ type | VPair(a : Val, b : Val) -- pair value -- Unit | VUnit | VTt -- Empty | VEmpty -- Bootstrap coproduct, private to descPlus interpretation | VBootSum(A : Val, B : Val) | VBootInl(A : Val, B : Val, v : Val) | VBootInr(A : Val, B : Val, v : Val) -- Bootstrap identity, private to descRet/Lift/index transport | VBootEq(A : Val, a : Val, b : Val) | VBootRefl | VFunext -- Propositional truncation | VSquash(A : Val) | VSquashIntro(a : Val) -- Levels (Tarski-style sort of universe levels — see §6.6, §8.5) | VLevel -- the Level sort itself | VLevelZero -- 0 | VLevelSuc(pred : Val) -- successor | VLevelMax(lhs : Val, rhs : Val) -- join -- Universes (level-indexed, k : VLevel) | VU(k : Val) -- Descriptions (universe-polymorphic; see §7.6) | VDesc(K : Val, I : Val) -- Desc^K I -- Description constructors are encoded as VDescCon inhabitants of -- μ Unit (descDesc I K) tt. Evaluation projects them through the private -- DViewRet/DViewArg/DViewRec/DViewPi/DViewPlus semantic view. -- μ-types | VMu(I : Val, D : Val, i : Val) -- μ I D i | VDescCon(D : Val, i : Val, d : Val) -- introduction at index i with payload d | VInterpD(level : Val, I : Val, D : Val, X : Val, i : Val) | VAllD(level : Val, I : Val, D : Val, K : Val, X : Val, M : Val, i : Val, d : Val) | VEverywhereD(level : Val, I : Val, D : Val, K : Val, X : Val, M : Val, ih : Val, i : Val, d : Val) -- Lift | VLift(l : Val, m : Val, eq : Val, A : Val) | VLiftIntro(l : Val, m : Val, eq : Val, A : Val, a : Val) -- Axiomatized primitive types | VString | VInt | VFloat | VAttrs | VPath | VDerivation | VFunction | VAny -- Primitive literal values | VStringLit(s) | VIntLit(n) | VFloatLit(f) | VAttrsLit | VPathLit | VDerivationLit | VFnLit | VAnyLit | VOpaqueLam(fnBox, piTy : Val) -- Neutrals (stuck computations) | VNe(level : ℕ, spine : [Elim]) Elim ::= | EApp(v : Val) | EFst | ESnd | EBootSumElim(A : Val, B : Val, P : Val, l : Val, r : Val) | EBootJ(A : Val, a : Val, P : Val, pr : Val, b : Val) | EStrEq(arg : Val) | EAbsurd(P : Val) | EDescInd(D : Val, motive : Val, step : Val, i : Val) | EInterpD(level : Val, I : Val, X : Val, i : Val) | EAllD(level : Val, I : Val, K : Val, X : Val, M : Val, i : Val, d : Val) | EEverywhereD(level : Val, I : Val, K : Val, X : Val, M : Val, ih : Val, i : Val, d : Val) | ELiftElim(l : Val, m : Val, eq : Val, A : Val) | ESquashElim(A : Val, B : Val, f : Val) Closure ::= (env : Env, body : Tm) Env ::= [Val] -- list indexed by de Bruijn index ``` ### 3.1 Level/index relationship De Bruijn levels count from the outermost binder: 0 = first-ever bound variable. Levels are stable under context extension. Conversion between index and level: ``` index = depth - level - 1 level = depth - index - 1 ``` where `depth` is the current binding depth (length of the context). ### 3.2 Fresh variables A fresh variable at depth `d` is `VNe(d, [])` — a neutral with level `d` and empty spine. Used in conversion checking to compare under binders. ### 3.3 Closure instantiation ``` instantiate((env, body), v) = eval([v] ++ env, body) ``` --- ## 4. Evaluation Rules `eval(ρ, t)` interprets term `t` in environment `ρ`, producing a value. All rules are deterministic. ### 4.1 Variables and let ``` eval(ρ, Var(i)) = ρ[i] eval(ρ, Let(n, A, t, u)) = eval([eval(ρ, t)] ++ ρ, u) eval(ρ, Ann(t, A)) = eval(ρ, t) ``` ### 4.2 Functions ``` eval(ρ, Pi(n, A, B)) = VPi(n, eval(ρ, A), (ρ, B)) eval(ρ, Lam(n, A, t)) = VLam(n, eval(ρ, A), (ρ, t)) eval(ρ, App(t, u)) = vApp(eval(ρ, t), eval(ρ, u)) ``` where `vApp` performs beta reduction or accumulates: ``` vApp(VLam(n, A, cl), v) = instantiate(cl, v) vApp(VNe(l, sp), v) = VNe(l, sp ++ [EApp(v)]) vApp(_, _) = THROW "kernel bug: vApp on non-function" ``` ### 4.3 Pairs ``` eval(ρ, Sigma(n, A, B)) = VSigma(n, eval(ρ, A), (ρ, B)) eval(ρ, Pair(a, b)) = VPair(eval(ρ, a), eval(ρ, b)) eval(ρ, Fst(t)) = vFst(eval(ρ, t)) eval(ρ, Snd(t)) = vSnd(eval(ρ, t)) ``` where: ``` vFst(VPair(a, b)) = a vFst(VNe(l, sp)) = VNe(l, sp ++ [EFst]) vFst(_) = THROW "kernel bug: vFst on non-pair" vSnd(VPair(a, b)) = b vSnd(VNe(l, sp)) = VNe(l, sp ++ [ESnd]) vSnd(_) = THROW "kernel bug: vSnd on non-pair" ``` ### 4.4 Generated data families Natural numbers, lists, public sums, and public equality are prelude datatypes generated from descriptions. Their types evaluate to `VMu I D i`; their constructors evaluate to `VDescCon D i payload`; their eliminators elaborate to `DescInd` over the generated description. ```text H.nat == μ Unit NatDT.D tt H.zero == descCon NatDT.D tt H.succ n == descCon NatDT.D tt H.listOf A == μ Unit (ListDT.D A) tt H.nil A == descCon (ListDT.D A) tt H.cons A h t == descCon (ListDT.D A) tt H.sum A B == μ Unit (SumDT.D 0 A B) tt H.eq A a b == μ A (EqDT.D A a) b ``` The generated constructor payloads still use private bootstrap coproduct/identity values where the description interpretation requires them. These are representation details, not public eliminators. Deep generated natural/list values are stack-safe through the constructor flattening and `desc-con` trampoline paths, rather than through primitive nat/list evaluator cases. ### 4.5 Description interpretation, Lift, Squash, and Funext The current kernel includes several small primitives used by generated datatypes and proof-oriented APIs: ```text eval(ρ, DescDescApp(I,L)) = tagged descDesc value eval(ρ, InterpD(level,I,D,X,i)) = vInterpD(level,I,D,X,i) eval(ρ, AllD(level,I,D,K,X,M,i,d)) = vAllD(level,I,D,K,X,M,i,d) eval(ρ, EverywhereD(level,I,D,K,X,M,ih,i,d)) = vEverywhereD(level,I,D,K,X,M,ih,i,d) eval(ρ, Lift(l,m,eq,A)) = vLiftF(l,m,eq,A) eval(ρ, LiftIntro(l,m,eq,A,a)) = vLiftIntroF(l,m,eq,A,a) eval(ρ, LiftElim(l,m,eq,A,x)) = vLiftElimF(l,m,eq,A,x) eval(ρ, Squash(A)) = VSquash(eval(ρ,A)) eval(ρ, SquashIntro(a)) = VSquashIntro(eval(ρ,a)) eval(ρ, SquashElim(A,B,f,x)) = vSquashElim(eval(ρ,A), eval(ρ,B), eval(ρ,f), eval(ρ,x)) eval(ρ, Funext) = VFunext eval(ρ, OpaqueLam(fnBox, piTy)) = VOpaqueLam(fnBox, eval(ρ,piTy)) eval(ρ, LitVal(v)) = v ``` `LitVal v` is the splice operator of two-level type theory (Kovács, "Staged Compilation with Two-Level Type Theory", POPL 2024; Annenkov–Capriotti–Kraus–Sattler 2019): a closed semantic value reflected into the syntactic domain. The eval rule discards the environment, so the carried `v` must be closed (free de Bruijn levels would never resolve). Quotation reads through to the underlying value — `LitVal` is invisible at the Val layer, so conv, quote, and the ι/β/η rules operate on `v` directly without any new transparency rule. The kernel uses `LitVal` as the canonical Val→Tm lift on paths that would otherwise call `quote 0 v` on a value destined for re-evaluation (notably the effect-handler bridge in `src/experimental/desc-interp/trampoline.nix`). Reflection avoids the O(size v) structural walk of `quote`, which would compound across iterated bridge steps. `Lift l m eq A` collapses definitionally to `A` when `l` and `m` are level-convertible; nested Lifts compose; `lower (lift a)` reduces to `a`; and `lift (lower x)` eta-reduces on stuck neutrals. The `eq` witness is irrelevant for conversion once the levels and underlying type match. `Squash A` is proof-irrelevant. Any two `SquashIntro` inhabitants at a shared `Squash A` type are definitionally equal, and neutral inhabitants of `Squash A` convert against introductions by the shared-type invariant. `DescDescApp` stamps a canonical reference on the generated `descDesc I L` value so quotation and conversion can avoid descending into the self-describing universe spiral. `InterpD`, `AllD`, and `EverywhereD` are the kernel primitives behind description interpretation and the generated `desc-ind` iota rule. ### 4.6 Unit ``` eval(ρ, Unit) = VUnit eval(ρ, Tt) = VTt ``` Unit has no eliminator in the core. The kernel implements ⊤-η: any neutral of type ⊤ converts against `VTt` (see §6.3). Sound in the type-free conv because conv is always called on values sharing a type; if one side is `VTt`, the shared type is ⊤ and the neutral's only inhabitant is `Tt`. ### 4.6′ Empty ``` eval(ρ, Empty) = VEmpty ``` Empty has no introduction. The eliminator `Absurd` (§4.6″) discharges any neutral of type Empty. ### 4.6″ Absurd ``` eval(ρ, Absurd(P, x)) = vAbsurd(eval(ρ, P), eval(ρ, x)) vAbsurd(P, VNe(l, sp)) = VNe(l, sp ++ [EAbsurd(P)]) vAbsurd(P, _) = THROW "kernel bug: vAbsurd on non-neutral" ``` `Absurd(P, x)` is the unique map from the initial object to any type `P` at any universe level. It is well-typed only when `x : Empty`; since `Empty` has no canonical inhabitants, `x` is always neutral in sound code. The non-neutral case is a kernel invariant violation — THROW rather than silently propagate, matching `vFst`/`vBootJ` hygiene. There is no β-rule for `Absurd`: it only fires on neutrals, and no canonical inhabitant of `Empty` exists to trigger reduction. Two `Absurd` redexes on the same neutral with definitionally equal `P` are conv-equal via the `EAbsurd` spine frame (§6.4). ### 4.7 Bootstrap coproduct ``` eval(ρ, BootSum(A, B)) = VBootSum(eval(ρ, A), eval(ρ, B)) eval(ρ, BootInl(A, B, t)) = VBootInl(eval(ρ, A), eval(ρ, B), eval(ρ, t)) eval(ρ, BootInr(A, B, t)) = VBootInr(eval(ρ, A), eval(ρ, B), eval(ρ, t)) eval(ρ, BootSumElim(A,B,P,l,r,s)) = vBootSumElim(eval(ρ,A), eval(ρ,B), eval(ρ,P), eval(ρ,l), eval(ρ,r), eval(ρ,s)) ``` where: ``` vBootSumElim(A, B, P, l, r, VBootInl(_, _, v)) = vApp(l, v) vBootSumElim(A, B, P, l, r, VBootInr(_, _, v)) = vApp(r, v) vBootSumElim(A, B, P, l, r, VNe(k, sp)) = VNe(k, sp ++ [EBootSumElim(A, B, P, l, r)]) vBootSumElim(_, _, _, _, _, _) = THROW "kernel bug: vBootSumElim on non-boot-sum" ``` This coproduct is private to `descPlus` interpretation. Public `H.sum`, `H.inl`, `H.inr`, and `H.sumElim` route through generated `SumDT`. ### 4.8 Bootstrap identity ``` eval(ρ, BootEq(A, a, b)) = VBootEq(eval(ρ, A), eval(ρ, a), eval(ρ, b)) eval(ρ, BootRefl) = VBootRefl eval(ρ, BootJ(A, a, P, pr, b, eq)) = vBootJ(eval(ρ,A), eval(ρ,a), eval(ρ,P), eval(ρ,pr), eval(ρ,b), eval(ρ,eq)) ``` where: ``` vBootJ(A, a, P, pr, b, VBootRefl) = pr vBootJ(A, a, P, pr, b, VNe(l,sp)) = VNe(l, sp ++ [EBootJ(A, a, P, pr, b)]) vBootJ(_, _, _, _, _, _) = THROW "kernel bug: vBootJ on non-refl" ``` This identity substrate is private to `descRet`, Lift witnesses, index transport, and no-confusion helpers. Public `H.eq`, `H.refl`, and `H.j` route through generated `EqDT`. ### 4.9 Universes ``` eval(ρ, U(i)) = VU(i) ``` ### 4.10 Axiomatized primitives Type formers evaluate to their corresponding values. Literals carry their payload through. No computation, no recursion — these are axiomatized constants. ``` eval(ρ, String) = VString eval(ρ, Int) = VInt eval(ρ, Float) = VFloat eval(ρ, Attrs) = VAttrs eval(ρ, Path) = VPath eval(ρ, Derivation) = VDerivation eval(ρ, Function) = VFunction eval(ρ, Any) = VAny eval(ρ, StringLit(s)) = VStringLit(s) eval(ρ, IntLit(n)) = VIntLit(n) eval(ρ, FloatLit(f)) = VFloatLit(f) eval(ρ, AttrsLit) = VAttrsLit eval(ρ, PathLit) = VPathLit eval(ρ, DerivationLit) = VDerivationLit eval(ρ, FnLit) = VFnLit eval(ρ, AnyLit) = VAnyLit ``` Most primitives have no eliminators. They exist to integrate Nix's native types into the kernel's type system as opaque, axiomatized constants. The exception is String, which has `StrEq` (§4.11). ### 4.11 String equality (StrEq) ``` eval(ρ, StrEq(lhs, rhs)) = vStrEq(eval(ρ, lhs), eval(ρ, rhs)) ``` where: ``` -- trueV / falseV are the plus-encoded derived booleans: -- trueV = VDescCon boolDescV VTt (VBootInl eqTtV eqTtV VBootRefl) -- falseV = VDescCon boolDescV VTt (VBootInr eqTtV eqTtV VBootRefl) -- where boolDescV is the generated encoded BoolDT description. vStrEq(VStringLit(s₁), VStringLit(s₂)) = if s₁ == s₂ then trueV else falseV vStrEq(VNe(l, sp), rhs) = VNe(l, sp ++ [EStrEq(rhs)]) vStrEq(lhs, VNe(l, sp)) = VNe(l, sp ++ [EStrEq(lhs)]) vStrEq(_, _) = THROW "kernel bug: vStrEq on non-string" ``` `StrEq` is a binary predicate on strings. Both arguments must be of type `String`. The result type is the derived `H.bool` — `μ ⊤ (plus (retI tt) (retI tt)) tt` — which is the kernel representation of booleans after their retirement as primitives. Unlike other eliminators, StrEq has no motive: it always returns `H.bool`, not a dependent type. When both arguments are concrete string literals, `vStrEq` reduces to the plus-encoded `true_` or `false_` value by Nix-level string comparison. When either argument is neutral, the neutral's spine is extended with `EStrEq` carrying the other argument. This is sound because `StrEq` is symmetric: `StrEq(a, b) ≡ StrEq(b, a)` for all `a, b : String`. --- ## 5. Quotation Rules `quote(d, v)` converts a value back to a term, converting levels to indices. `d` is the current binding depth. ``` quote(d, VPi(n, A, cl)) = Pi(n, quote(d, A), quote(d+1, instantiate(cl, fresh(d)))) quote(d, VLam(n, A, cl)) = Lam(n, quote(d, A), quote(d+1, instantiate(cl, fresh(d)))) quote(d, VSigma(n, A, cl)) = Sigma(n, quote(d, A), quote(d+1, instantiate(cl, fresh(d)))) quote(d, VPair(a, b)) = Pair(quote(d, a), quote(d, b), _) quote(d, VUnit) = Unit quote(d, VTt) = Tt quote(d, VEmpty) = Empty quote(d, VBootSum(A, B)) = BootSum(quote(d, A), quote(d, B)) quote(d, VBootInl(A, B, v)) = BootInl(quote(d, A), quote(d, B), quote(d, v)) quote(d, VBootInr(A, B, v)) = BootInr(quote(d, A), quote(d, B), quote(d, v)) quote(d, VBootEq(A, a, b)) = BootEq(quote(d, A), quote(d, a), quote(d, b)) quote(d, VBootRefl) = BootRefl quote(d, VU(i)) = U(i) quote(d, VString) = String quote(d, VInt) = Int quote(d, VFloat) = Float quote(d, VAttrs) = Attrs quote(d, VPath) = Path quote(d, VDerivation) = Derivation quote(d, VFunction) = Function quote(d, VAny) = Any quote(d, VStringLit(s)) = StringLit(s) quote(d, VIntLit(n)) = IntLit(n) quote(d, VFloatLit(f)) = FloatLit(f) quote(d, VAttrsLit) = AttrsLit quote(d, VPathLit) = PathLit quote(d, VDerivationLit) = DerivationLit quote(d, VFnLit) = FnLit quote(d, VAnyLit) = AnyLit quote(d, VNe(l, sp)) = quoteSp(d, Var(d - l - 1), sp) quoteSp(d, head, []) = head quoteSp(d, head, [EApp(v) | rest]) = quoteSp(d, App(head, quote(d, v)), rest) quoteSp(d, head, [EFst | rest]) = quoteSp(d, Fst(head), rest) quoteSp(d, head, [ESnd | rest]) = quoteSp(d, Snd(head), rest) quoteSp(d, head, [EBootSumElim(A,B,P,l,r) | rest]) = quoteSp(d, BootSumElim(quote(d,A), quote(d,B), quote(d,P), quote(d,l), quote(d,r), head), rest) quoteSp(d, head, [EBootJ(A,a,P,pr,b) | rest]) = quoteSp(d, BootJ(quote(d,A), quote(d,a), quote(d,P), quote(d,pr), quote(d,b), head), rest) quoteSp(d, head, [EStrEq(arg) | rest]) = quoteSp(d, StrEq(head, quote(d, arg)), rest) quoteSp(d, head, [EAbsurd(P) | rest]) = quoteSp(d, Absurd(quote(d, P), head), rest) fresh(d) = VNe(d, []) ``` --- ## 6. Conversion Rules `conv(d, v₁, v₂)` checks definitional equality of two values at binding depth `d`. Returns boolean. **No type information is used** — conversion is purely structural on normalized values. ### 6.1 Structural rules ``` conv(d, VU(i), VU(j)) = (i == j) conv(d, VUnit, VUnit) = true conv(d, VTt, VTt) = true conv(d, VEmpty, VEmpty) = true conv(d, VBootRefl, VBootRefl) = true conv(d, VString, VString) = true conv(d, VInt, VInt) = true conv(d, VFloat, VFloat) = true conv(d, VAttrs, VAttrs) = true conv(d, VPath, VPath) = true conv(d, VDerivation, VDerivation) = true conv(d, VFunction, VFunction) = true conv(d, VAny, VAny) = true conv(d, VStringLit(s₁), VStringLit(s₂)) = (s₁ == s₂) conv(d, VIntLit(n₁), VIntLit(n₂)) = (n₁ == n₂) conv(d, VFloatLit(f₁), VFloatLit(f₂)) = (f₁ == f₂) conv(d, VAttrsLit, VAttrsLit) = true conv(d, VPathLit, VPathLit) = true conv(d, VDerivationLit, VDerivationLit) = true conv(d, VFnLit, VFnLit) = true conv(d, VAnyLit, VAnyLit) = true ``` ### 6.2 Binding forms To compare under binders, generate a fresh variable and instantiate: ``` conv(d, VPi(_, A₁, cl₁), VPi(_, A₂, cl₂)) = conv(d, A₁, A₂) ∧ conv(d+1, instantiate(cl₁, fresh(d)), instantiate(cl₂, fresh(d))) conv(d, VLam(_, _, cl₁), VLam(_, _, cl₂)) = conv(d+1, instantiate(cl₁, fresh(d)), instantiate(cl₂, fresh(d))) conv(d, VLam(_, _, cl), v) = -- Π-η conv(d+1, instantiate(cl, fresh(d)), vApp(v, fresh(d))) -- only fires when v is not a VLam conv(d, v, VLam(_, _, cl)) = -- Π-η conv(d+1, vApp(v, fresh(d)), instantiate(cl, fresh(d))) -- only fires when v is not a VLam conv(d, VSigma(_, A₁, cl₁), VSigma(_, A₂, cl₂)) = conv(d, A₁, A₂) ∧ conv(d+1, instantiate(cl₁, fresh(d)), instantiate(cl₂, fresh(d))) ``` The two Π-η rules fire when exactly one side is a VLam; both sides being VLam falls through to the symmetric VLam/VLam rule above. Sound because conv is always called on values sharing a type — if one side is VLam, that type is VPi, and the other side's only inhabitants up to definitional equality are its η-expansions. Termination: each rule strictly decreases VLam-depth on the side it fires on, so no nested firing can loop. ### 6.3 Compound values ``` conv(d, VPair(a₁, b₁), VPair(a₂, b₂)) = conv(d, a₁, a₂) ∧ conv(d, b₁, b₂) conv(d, VPair(a, b), VNe(l, sp)) = conv(d, a, vFst(VNe(l, sp))) ∧ conv(d, b, vSnd(VNe(l, sp))) -- Σ-η conv(d, VNe(l, sp), VPair(a, b)) = conv(d, vFst(VNe(l, sp)), a) ∧ conv(d, vSnd(VNe(l, sp)), b) -- Σ-η conv(d, VTt, VNe(_, _)) = true -- ⊤-η conv(d, VNe(_, _), VTt) = true -- ⊤-η conv(d, VBootSum(A₁, B₁), VBootSum(A₂, B₂)) = conv(d, A₁, A₂) ∧ conv(d, B₁, B₂) conv(d, VBootInl(A₁, B₁, v₁), VBootInl(A₂, B₂, v₂)) = conv(d, A₁, A₂) ∧ conv(d, B₁, B₂) ∧ conv(d, v₁, v₂) conv(d, VBootInr(A₁, B₁, v₁), VBootInr(A₂, B₂, v₂)) = conv(d, A₁, A₂) ∧ conv(d, B₁, B₂) ∧ conv(d, v₁, v₂) conv(d, VBootEq(A₁, a₁, b₁), VBootEq(A₂, a₂, b₂)) = conv(d, A₁, A₂) ∧ conv(d, a₁, a₂) ∧ conv(d, b₁, b₂) ``` ### 6.4 Neutrals ``` conv(d, VNe(l₁, sp₁), VNe(l₂, sp₂)) = (l₁ == l₂) ∧ convSp(d, sp₁, sp₂) convSp(d, [], []) = true convSp(d, [e₁|r₁], [e₂|r₂]) = convElim(d, e₁, e₂) ∧ convSp(d, r₁, r₂) convSp(d, _, _) = false -- different lengths convElim(d, EApp(v₁), EApp(v₂)) = conv(d, v₁, v₂) convElim(d, EFst, EFst) = true convElim(d, ESnd, ESnd) = true convElim(d, EBootSumElim(A₁,B₁,P₁,l₁,r₁), EBootSumElim(A₂,B₂,P₂,l₂,r₂)) = conv(d, A₁, A₂) ∧ conv(d, B₁, B₂) ∧ conv(d, P₁, P₂) ∧ conv(d, l₁, l₂) ∧ conv(d, r₁, r₂) convElim(d, EBootJ(A₁,a₁,P₁,pr₁,b₁), EBootJ(A₂,a₂,P₂,pr₂,b₂)) = conv(d, A₁, A₂) ∧ conv(d, a₁, a₂) ∧ conv(d, P₁, P₂) ∧ conv(d, pr₁, pr₂) ∧ conv(d, b₁, b₂) convElim(d, EStrEq(arg₁), EStrEq(arg₂)) = conv(d, arg₁, arg₂) convElim(d, EAbsurd(P₁), EAbsurd(P₂)) = conv(d, P₁, P₂) convElim(_, _, _) = false ``` ### 6.5 Catch-all ``` conv(d, _, _) = false ``` Any pair of values not matching the above rules is not definitionally equal. **Π-eta, Σ-eta, and ⊤-eta are applied** (see §6.2 for Π-η, §6.3 for Σ-η and ⊤-η): `f` converts against `λx. f x` under a fresh binder; a pair `⟨a, b⟩` converts against a neutral `x : Σ` by projecting both sides; and any neutral of type `⊤` converts against `tt`. All three η-rules are sound in the type-free conv because conv is always called on two values sharing a type — the side carrying the canonical form (VLam, VPair, VTt) witnesses the shared type's shape (VPi, VSigma, ⊤), and the other side's η-expansion is its only inhabitant up to definitional equality. **Π-η rationale.** Π-η matches the standard semantic models of MLTT (PER, presheaf, simplicial sets) and is the η-rule consistent with funext: `f ≡ λx. f x` definitionally. Without it, definitional equality on Pi-typed values diverges from the equality the surface language must reason about — every elaborator that produces a function value would have to maintain its own η-normal form before submitting to conv. With it, conv handles the canonical-vs-neutral case by descending under one binder and continues structurally; subsequent ⊤-η, Σ-η, and neutral-vs-neutral rules fire as usual on the body. This composition in particular is what closes assemblies that pair a surface `descPi k S (λ_:S. tt) D` (a 3-arg combinator that fills the kernel's `f : S → ⊤` slot with a constant lambda) against a kernel-reconstructed `descPi k S f D` whose `f` is a case-bound variable. ### 6.6 Level conversion (convLevel) Level expressions form a join-semilattice with `zero` as bottom and `max` as join. `convLevel(d, k₁, k₂)` checks definitional equality of two Level values modulo the semilattice laws. **Fast path** (syntactic equality): ``` convLevel(d, k, k) = true ``` When the same Level value reaches both sides of conv (e.g. a description's level is reused unchanged across recursive children), the syntactic-equality check skips the normaliser entirely. Allocations from re-normalising structurally-identical levels dominate hot CHECK loops, so this short-circuit is non-optional. **Normalisation.** Each Level value is reduced to its canonical form before structural comparison: - `max(k, zero) = max(zero, k) = k` (zero absorption) - `max(k, k) = k` (idempotence) - `suc(max(a, b)) = max(suc(a), suc(b))` (suc distributes over max) - `max` operands are sorted to a canonical order The canonical form is `max(s₁, …, sₙ)` where each `sᵢ = sucᵐ(zero)` or `sᵢ = sucᵐ(VNe(_, _))`, sorted lexicographically. After normalisation the comparison is structural: ``` convLevel(d, k₁, k₂) = (normLevel(k₁) ≡_struct normLevel(k₂)) ``` Used by description and universe CHECK rules (§7.6) to verify that two level expressions denote the same level. --- ## 7. Typing Rules (Bidirectional) ### 7.1 Contexts ``` Ctx ::= { env : Env, -- values for evaluation types : [Val], -- types of bound variables (indexed by de Bruijn) depth : ℕ -- current binding depth } emptyCtx = { env = [], types = [], depth = 0 } extend(Γ, n, A) = { env = [fresh(Γ.depth)] ++ Γ.env, types = [A] ++ Γ.types, depth = Γ.depth + 1 } lookupType(Γ, i) = Γ.types[i] -- THROW if i >= length(Γ.types) ``` ### 7.2 Notation ``` Γ ⊢ t ⇐ A ↝ t' checking mode: check(Γ, t, A) = t' Γ ⊢ t ⇒ A ↝ t' synthesis mode: infer(Γ, t) = (t', A) Γ ⊢ T type ↝ T' type formation: checkType(Γ, T) = T' Γ ⊢ T type@i ↝ T' type + level: checkTypeLevel(Γ, T) = (T', i) ``` The output `t'` is the elaborated core term (fully annotated). ### 7.3 Synthesis rules (infer) **Var** ``` lookupType(Γ, i) = A ────────────────────── Γ ⊢ Var(i) ⇒ A ↝ Var(i) ``` **Ann** (annotation) ``` Γ ⊢ A type ↝ A' Â = eval(Γ.env, A') Γ ⊢ t ⇐ Â ↝ t' ────────────────────── Γ ⊢ Ann(t, A) ⇒ Â ↝ Ann(t', A') ``` **App** (application) ``` Γ ⊢ f ⇒ fTy ↝ f' whnf(fTy) = VPi(n, A, cl) Γ ⊢ u ⇐ A ↝ u' B = instantiate(cl, eval(Γ.env, u')) ────────────────────── Γ ⊢ App(f, u) ⇒ B ↝ App(f', u') ``` **CRITICAL**: `whnf(fTy)` must normalize `fTy` to weak head normal form before pattern matching. If `fTy` is a let-unfolding or a neutral that reduces further, the match will fail spuriously. In this kernel, `eval` already produces WHNF, so `whnf(v) = v` for all values. But this invariant must be maintained if the value representation changes. **Fst** (first projection) ``` Γ ⊢ t ⇒ tTy ↝ t' whnf(tTy) = VSigma(n, A, cl) ────────────────────── Γ ⊢ Fst(t) ⇒ A ↝ Fst(t') ``` **Snd** (second projection) ``` Γ ⊢ t ⇒ tTy ↝ t' whnf(tTy) = VSigma(n, A, cl) B = instantiate(cl, vFst(eval(Γ.env, t'))) ────────────────────── Γ ⊢ Snd(t) ⇒ B ↝ Snd(t') ``` **Eliminator motive checking (checkMotive).** All eliminators require a motive `P : domTy → U(k)` for some `k`. The implementation provides a shared `checkMotive` helper that handles two forms: - Lambda motives (`P = λx. body`): extend the context with `x : domTy` and verify `body` is a type via `checkType`. - Non-lambda motives: infer the type and verify it has shape `VPi(_, domTy, _ → VU(k))` for some `k`. The `k` is not fixed — motives may target any universe level, enabling **large elimination** (eliminators whose return type is a type, not a value). Generated datatype eliminators use this same motive checker through `DescInd`. **Generated eliminators.** Public eliminators for natural numbers, lists, sums, equality, vectors, finite sets, W-types, and user-defined datatypes are generated as applications of `DescInd` to their datatype description. The checker validates the generated motive and branch terms against the generic indexed-description eliminator. **Public identity elimination.** `H.j A a P pr b eq` is a HOAS adapter that preserves the usual J-shaped arguments, but elaborates to `EqDT.elim`. The adapter checks `pr` against `P a (EqDT.refl A a)` and checks `eq` against `EqDT.T A a b` before emitting the generated eliminator spine. **Bootstrap identity elimination.** Internal description machinery may still use `BootJ`: ``` Γ ⊢ A type ↝ A' Â = eval(Γ.env, A') Γ ⊢ a ⇐ Â ↝ a' â = eval(Γ.env, a') Γ ⊢ P ⇐ <Π(y : A). Π(e : BootEq A a y). U(k)> ↝ P' P̂ = eval(Γ.env, P') Γ ⊢ pr ⇐ vApp(vApp(P̂, â), VBootRefl) ↝ pr' Γ ⊢ b ⇐ Â ↝ b' b̂ = eval(Γ.env, b') Γ ⊢ eq ⇐ VBootEq(Â, â, b̂) ↝ eq' ────────────────────── Γ ⊢ BootJ(A, a, P, pr, b, eq) ⇒ vApp(vApp(P̂, b̂), eval(Γ.env, eq')) ↝ BootJ(A', a', P', pr', b', eq') ``` **Bootstrap J motive verification.** For non-lambda motives, the implementation structurally verifies all three components: 1. Outer Pi domain matches `A` (conversion check) 2. Inner Pi domain matches `BootEq(A, a, y)` (conversion check) 3. Innermost codomain is `VU(k)` for some `k` For lambda motives (`P = λy. body`), the body is checked via `checkMotive` against `BootEq(A, a, y)`, which performs the same verification on the inner structure. This catches motive errors at the motive itself rather than deferring to the base case. **Axiomatized primitive type formers** (synthesis) Primitive type formers are synthesized directly — they infer as inhabitants of `U(0)`: ``` ────────────────────── Γ ⊢ String ⇒ VU(0) ↝ String ────────────────────── Γ ⊢ Int ⇒ VU(0) ↝ Int ``` (Similarly for Float, Attrs, Path, Derivation, Function, Any — all at level 0.) **Primitive literals** (synthesis) Literals synthesize their corresponding type: ``` ────────────────────── Γ ⊢ StringLit(s) ⇒ VString ↝ StringLit(s) ────────────────────── Γ ⊢ IntLit(n) ⇒ VInt ↝ IntLit(n) ────────────────────── Γ ⊢ FloatLit(f) ⇒ VFloat ↝ FloatLit(f) ``` (Similarly for AttrsLit → VAttrs, PathLit → VPath, DerivationLit → VDerivation, FnLit → VFunction, AnyLit → VAny.) **StrEq** (string equality) ``` boolDescV = eval [] (elab BoolDT.D) boolV = VMu VUnit boolDescV VTt Γ ⊢ lhs ⇐ VString ↝ lhs' Γ ⊢ rhs ⇐ VString ↝ rhs' ────────────────────── Γ ⊢ StrEq(lhs, rhs) ⇒ boolV ↝ StrEq(lhs', rhs') ``` Both arguments are checked against `VString`. The result type is the derived `H.bool` — `μ ⊤ (plus (retI tt) (retI tt)) tt` — written `boolV` above. StrEq is not a dependent eliminator: it has no motive parameter. ### 7.4 Checking rules (check) **Lam** (lambda introduction) ``` whnf(A) = VPi(n, dom, cl) Γ' = extend(Γ, n, dom) cod = instantiate(cl, fresh(Γ.depth)) Γ' ⊢ t ⇐ cod ↝ t' ────────────────────── Γ ⊢ Lam(n, _, t) ⇐ A ↝ Lam(n, quote(Γ.depth, dom), t') ``` **Pair** (pair introduction) ``` whnf(T) = VSigma(n, A, cl) Γ ⊢ a ⇐ A ↝ a' B = instantiate(cl, eval(Γ.env, a')) Γ ⊢ b ⇐ B ↝ b' ────────────────────── Γ ⊢ Pair(a, b, _) ⇐ T ↝ Pair(a', b', quote(Γ.depth, T)) ``` **Generated datatype constructors.** Public constructors such as `H.zero`, `H.succ`, `H.nil`, `H.cons`, `H.inl`, `H.inr`, and user-defined datatype constructors check as `DescCon` introductions against their generated `VMu` type. Their payloads are checked against the interpretation of the constructor's description. Deep generated natural/list constructor chains are handled by flat constructor elaboration and `desc-con` trampolines. **Tt** ``` whnf(A) = VUnit ────────────────────── Γ ⊢ Tt ⇐ A ↝ Tt ``` **BootRefl** ``` whnf(T) = VBootEq(A, a, b) conv(Γ.depth, a, b) = true ────────────────────── Γ ⊢ BootRefl ⇐ T ↝ BootRefl ``` If `conv(Γ.depth, a, b) = false`, this is a **type error**: the two sides of the equation are not definitionally equal, and `BootRefl` cannot prove the equation. Public `H.refl` is resolved by HOAS check mode against generated `EqDT.T A a a`, elaborating to `EqDT.refl A a`; unrestricted inference for bare public `refl` is rejected. **Primitive literals** (checked against their corresponding types) ``` whnf(A) = VString ────────────────────── Γ ⊢ StringLit(s) ⇐ A ↝ StringLit(s) whnf(A) = VInt ────────────────────── Γ ⊢ IntLit(n) ⇐ A ↝ IntLit(n) whnf(A) = VFloat ────────────────────── Γ ⊢ FloatLit(f) ⇐ A ↝ FloatLit(f) whnf(A) = VAttrs ────────────────────── Γ ⊢ AttrsLit ⇐ A ↝ AttrsLit whnf(A) = VPath ────────────────────── Γ ⊢ PathLit ⇐ A ↝ PathLit whnf(A) = VDerivation ────────────────────── Γ ⊢ DerivationLit ⇐ A ↝ DerivationLit whnf(A) = VFunction ────────────────────── Γ ⊢ FnLit ⇐ A ↝ FnLit whnf(A) = VAny ────────────────────── Γ ⊢ AnyLit ⇐ A ↝ AnyLit ``` **Let** ``` Γ ⊢ A type ↝ A' Â = eval(Γ.env, A') Γ ⊢ t ⇐ Â ↝ t' t̂ = eval(Γ.env, t') Γ' = { env = [t̂] ++ Γ.env, types = [Â] ++ Γ.types, depth = Γ.depth + 1 } Γ' ⊢ u ⇐ B ↝ u' ────────────────────── Γ ⊢ Let(n, A, t, u) ⇐ B ↝ Let(n, A', t', u') ``` Note: `Let` in checking mode — the expected type `B` is for the body `u`, not for the definition `t`. **Sub** (mode switch: fall through to synthesis) ``` Γ ⊢ t ⇒ A ↝ t' conv(Γ.depth, A, B) = true ────────────────────── Γ ⊢ t ⇐ B ↝ t' ``` This is the catch-all. If no other checking rule applies, try synthesis and verify the inferred type matches the expected type. ### 7.5 Type formation (checkType / checkTypeLevel) The implementation provides two variants: `checkType(Γ, T)` returns only the elaborated term, while `checkTypeLevel(Γ, T)` returns both the elaborated term and the universe level. `checkType` is a thin wrapper: `checkType(Γ, T) = checkTypeLevel(Γ, T).term`. Universe levels are computed structurally during the type formation check (see §8.2), not by post-hoc inspection of evaluated values. ``` ────────────────────── Γ ⊢ Unit type ↝ Unit ────────────────────── Γ ⊢ Empty type ↝ Empty Γ ⊢ P type ↝ P' level(P') = k Γ ⊢ x ⇐ Empty ↝ x' ────────────────────── Γ ⊢ Absurd(P, x) ⇒ P̂ (P̂ = eval(Γ.env, P')) ↝ Absurd(P', x') ────────────────────── Γ ⊢ String type ↝ String (Similarly for Int, Float, Attrs, Path, Derivation, Function, Any) ────────────────────── Γ ⊢ U(i) type ↝ U(i) Γ ⊢ A type ↝ A' Γ ⊢ B type ↝ B' ────────────────────── Γ ⊢ BootSum(A, B) type ↝ BootSum(A', B') Γ ⊢ A type ↝ A' Â = eval(Γ.env, A') Γ ⊢ a ⇐ Â ↝ a' Γ ⊢ b ⇐ Â ↝ b' ────────────────────── Γ ⊢ BootEq(A, a, b) type ↝ BootEq(A', a', b') Γ ⊢ A type ↝ A' Â = eval(Γ.env, A') Γ' = extend(Γ, n, Â) Γ' ⊢ B type ↝ B' ────────────────────── Γ ⊢ Pi(n, A, B) type ↝ Pi(n, A', B') Γ ⊢ A type ↝ A' Â = eval(Γ.env, A') Γ' = extend(Γ, n, Â) Γ' ⊢ B type ↝ B' ────────────────────── Γ ⊢ Sigma(n, A, B) type ↝ Sigma(n, A', B') -- Fallback: infer and check it's a universe Γ ⊢ T ⇒ A ↝ T' whnf(A) = VU(i) ────────────────────── Γ ⊢ T type ↝ T' ``` Public generated data types enter this judgment through the fallback: their expanded `Mu(...)` terms infer a universe. ### 7.6 Descriptions: typing rules Descriptions classify strictly-positive datatype signatures over an index type `I`. A description `D : Desc^k I` quantifies over at most universe level `k`: `descArg^k S T` requires `S : U(k)`, and `descPi^k S f D` requires `S : U(k)` and `f : S → I`. The description's level `k` is recovered from the surrounding `μ` (via `mu I D i`) at elaboration time; CHECK rules thread `k` through recursive children without re-synthesising it ("homogeneity by typing", below). **Notation.** `Desc^k I` is the kernel value `VDesc(K, Î)` where `K : Level` (§8.5). `μ I D i` is the kernel value `VMu(Î, D̂, î)`, the `i`-th type in the family classified by `D`. #### 7.6.1 Description eliminators are encoded at the HOAS layer There is no `DescElim` core term in the current kernel. The HOAS surface exposes description elimination by applying the generated `encodeDescElim` program to a `descDesc I K` value. The trusted core operations involved are `DescDescApp`, `InterpD`, `AllD`, `EverywhereD`, and `DescInd`. The level agreement once handled by a primitive `DescElim` rule is now checked by the ordinary typing rules for `Desc I K`, `interpD`, and the encoded eliminator's Pi type. `DescDescApp(I, K)` carries a canonical reference so quotation and conversion can recognize the self-describing description universe without forcing the recursive encoding. #### 7.6.2 Homogeneity by typing (desc CHECK rules) When CHECKing a description against `Desc^K I`, recursive sub-checks inherit `K` directly from the surrounding type rather than synthesising their own. The principle: > A description's recursive children inhabit the same description type > as the parent. Reconstructing `VDesc(K, Î)` per recursive call to > thread the type — only to have the recursive CHECK pattern-match > it back open — is wasted allocation. The CHECK rules pass the surrounding type directly: ``` whnf(ty) = VDesc(K, Î) Γ ⊢ S ⇐ VU(K) ↝ S' Ŝ = eval(Γ.env, S') Γ ⊢ T ⇐ VPi(_, Ŝ, ([], ty)) ↝ T' -- recursive, same ty ────────────────────── Γ ⊢ DescArg(K, S, T) ⇐ ty ↝ DescArg(K, S', T') whnf(ty) = VDesc(K, Î) Γ ⊢ S ⇐ VU(K) ↝ S' Ŝ = eval(Γ.env, S') Γ ⊢ f ⇐ VPi(_, Ŝ, ([], Î)) ↝ f' Γ ⊢ D ⇐ VPi(_, Ŝ, ([], ty)) ↝ D' -- recursive, same ty ────────────────────── Γ ⊢ DescPi(K, S, f, D) ⇐ ty ↝ DescPi(K, S', f', D') whnf(ty) = VDesc(K, Î) Γ ⊢ A ⇐ ty ↝ A' -- recursive, same ty Γ ⊢ B ⇐ ty ↝ B' -- recursive, same ty ────────────────────── Γ ⊢ DescPlus(A, B) ⇐ ty ↝ DescPlus(A', B') whnf(ty) = VDesc(K, Î) Γ ⊢ j ⇐ Î ↝ j' Γ ⊢ D ⇐ ty ↝ D' -- recursive, same ty ────────────────────── Γ ⊢ DescRec(j, D) ⇐ ty ↝ DescRec(j', D') whnf(ty) = VDesc(K, Î) Γ ⊢ j ⇐ Î ↝ j' ────────────────────── Γ ⊢ DescRet(j) ⇐ ty ↝ DescRet(j') ``` The `K` and `Î` are recovered once at the outermost CHECK, then reused unchanged by every recursive sub-check. The rules' written shape mirrors the implementation: `ty` (the surrounding `VDesc` value) flows into recursive positions verbatim, and `convLevel` on the inner description's level reduces to `convLevel(K, K)` — the syntactic-equality fast-path of §6.6 fires. #### 7.6.3 desc-con CHECK with checkDescAtAnyLevel A `μ I D i` introduction `descCon D i d` checks the description `D` against `Desc^K I`, where `K` is recovered from the surrounding `μ`'s classifier. Because `μ` at indexed positions is checked against `VMu(Î, D̂, î)` whose `D̂` field carries no externally-visible level, the CHECK rule infers the level from the type-of-`D̂` at elaboration: ``` whnf(ty) = VMu(Î, D̂, î) checkDescAtAnyLevel(Γ, D) = (D', K) conv(Γ.depth, eval(Γ.env, D'), D̂) = true Γ ⊢ i ⇐ Î ↝ i' conv(Γ.depth, eval(Γ.env, i'), î) = true Γ ⊢ payload ⇐ ↝ payload' ────────────────────── Γ ⊢ DescCon(D, i, payload) ⇐ ty ↝ DescCon(D', i', payload') ``` `checkDescAtAnyLevel(Γ, D)` is the bidirectional bridge: it elaborates `D` at the most specific admissible level synthesised from `D`'s structure, returning both the elaborated term and the inferred `K`. Equivalent to `∃K. Γ ⊢ D ⇐ Desc^K Î`. The bidirectional discipline at index positions is preserved: canonical intros (`tt`, `zero`, `refl`, …) at the index slot remain checkable-only. --- ## 8. Universe Rules ### 8.1 Universe formation ``` U(i) : U(i + 1) for all i ≥ 0 ``` ### 8.2 Type former levels Universe levels are computed by `checkTypeLevel`, which returns `{ term; level; }` from the **typing derivation**, not from post-hoc value inspection. This avoids the problem of unknown levels for neutral type variables. We write `level(A)` as shorthand for `checkTypeLevel(Γ, A).level`. ``` checkTypeLevel(Γ, Unit) = { Unit, 0 } checkTypeLevel(Γ, Empty) = { Empty, 0 } checkTypeLevel(Γ, String) = { String, 0 } checkTypeLevel(Γ, Int) = { Int, 0 } checkTypeLevel(Γ, Float) = { Float, 0 } checkTypeLevel(Γ, Attrs) = { Attrs, 0 } checkTypeLevel(Γ, Path) = { Path, 0 } checkTypeLevel(Γ, Derivation) = { Derivation, 0 } checkTypeLevel(Γ, Function) = { Function, 0 } checkTypeLevel(Γ, Any) = { Any, 0 } checkTypeLevel(Γ, BootSum(A,B))= { BootSum(A',B'), max(level(A), level(B)) } checkTypeLevel(Γ, Pi(n, A, B)) = { Pi(n,A',B'), max(level(A), level(B)) } checkTypeLevel(Γ, Sigma(n,A,B))= { Sigma(n,A',B'), max(level(A), level(B)) } checkTypeLevel(Γ, BootEq(A,a,b)) = { BootEq(A',a',b'), level(A) } checkTypeLevel(Γ, U(i)) = { U(i), i + 1 } -- Fallback: infer type, require VU(i), extract i checkTypeLevel(Γ, T) = { T', i } where Γ ⊢ T ⇒ VU(i) ``` The fallback handles neutral type expressions (variables, applications) by inferring their type and requiring it to be a universe. This correctly propagates levels through type variables: if `B : U(1)`, then `checkTypeLevel` on `B` infers `VU(1)` and returns level 1. ### 8.3 Non-cumulativity The kernel is non-cumulative: a type `A` at level `i` is **not** automatically a type at any level `j > i`. The Sub rule (§7.4) compares the inferred universe against the expected one with the ordinary structural `conv`, which decides `VU(i)` against `VU(j)` by exact level equality — `convLevel(i, j)` modulo the §6.6 semilattice laws, never by `i ≤ j`. To move a type up the hierarchy you apply the explicit `Lift` former (§4.5); there is no implicit subsumption. Conversion therefore stays a decidable equivalence rather than a preorder, and the bidirectional discipline keeps a single CHECK-to-INFER bridge (the `conv` round-trip) with no cumulativity side-channel. ### 8.4 Universe consistency The kernel MUST reject `U(i) : U(i)`. This is guaranteed by the level computation: `level(U(i)) = i + 1`, so `U(i)` lives at level `i + 1`, not `i`. Self-containing universes cannot be constructed. This prevents Girard's paradox (Girard 1972), which requires a type that contains itself. Hurkens (1995) gives the compact MLTT rendering of the inconsistency proof. Universe stratification is the standard fix, and it is why the kernel enforces `level(U(i)) = i + 1`. ### 8.5 Level sort `Level` is a Tarski-style sort of universe levels, with constructors `zero`, `suc`, and `max`. It inhabits the lowest universe: ``` ────────────────────── Γ ⊢ Level type ↝ Level ────────────────────── Γ ⊢ Level ⇒ VU(0) ↝ Level ────────────────────── Γ ⊢ LevelZero ⇐ Level ↝ LevelZero Γ ⊢ k ⇐ Level ↝ k' ────────────────────── Γ ⊢ LevelSuc(k) ⇐ Level ↝ LevelSuc(k') Γ ⊢ a ⇐ Level ↝ a' Γ ⊢ b ⇐ Level ↝ b' ────────────────────── Γ ⊢ LevelMax(a, b) ⇐ Level ↝ LevelMax(a', b') ``` Conversion modulo the semilattice laws (idempotence of `max`, `suc` distribution over `max`, zero absorption) is delegated to `convLevel` (§6.6); structural conversion on Level values without normalisation would be too coarse (e.g. `max(zero, k)` and `k` would not compare equal). The `Level` sort enables predicative universe polymorphism: the description type `Desc^k I` and universe `U(k)` quantify over arbitrary levels via `Π(k:Level). …`. Rank-1 only — `Level` itself has no eliminator, and admitting one would break parametricity over the semilattice quotient (any eliminator would be observably sensitive to the canonical form chosen by `convLevel`). --- ## 9. Fuel Mechanism ### 9.1 Evaluation fuel Every call to `evalF` receives a fuel parameter and decrements it by one before evaluating the term. When fuel reaches 0: ``` evalF(fuel=0, ρ, t) = THROW "normalization budget exceeded" ``` The kernel aborts via `throw`. Layer 0 (TCB) has no access to the effect system by design, so fuel exhaustion and kernel invariant violations both manifest as Nix-level throws caught by `tryEval`. Callers should treat any throw from the evaluator as "term not verified" — the distinction between fuel exhaustion and a kernel bug is in the error message text, not the failure mechanism. ### 9.2 Default budget The default fuel budget is 10,000,000 reduction steps. This is configurable by the caller via `evalF`. No minimum is enforced — callers may pass arbitrarily low fuel, which will cause immediate `throw` on the first eval step. ### 9.3 Fuel accounting Fuel is **per-path**, not a global counter. Each call to `evalF` captures `f = fuel - 1` and passes `f` to all sub-evaluations of that term. When evaluating `App(t, u)`, both `evalF(f, ρ, t)` and `evalF(f, ρ, u)` receive the same `f`. This means fuel bounds the **depth** of any single evaluation path, not the total work across all paths. For a balanced binary tree of N applications, the total work is O(2^depth × fuel), not O(fuel). This is inherent to pure Nix — there is no mutable global counter. The fuel mechanism guarantees termination (every path eventually hits 0) but does not bound total computation time. All fuel consumption flows through `evalF`: - Direct term evaluation (each `evalF` call decrements fuel by 1) - Beta-reduction in `vApp` consumes fuel indirectly via `instantiateF`, which calls `evalF` - Iota-reduction in generated recursive eliminators consumes fuel through `vDescIndF`, `vAllDF`, `vEverywhereDF`, and `vAppF` `BootJ` completes in O(1) on `BootRefl`. `BootSumElim` is non-recursive, but branch selection calls `vAppF` on the selected branch. Structural operations (building values, pattern matching on tags) do not consume fuel. ### 9.4 Fuel threading in generated eliminators Generated natural/list eliminators route through datatype-specific wrappers and the generic `DescInd` evaluator. Deep constructor chains are not handled by hard-coded nat/list cases: `DescCon` evaluation recognizes homogeneous linear recursive payloads from the description profile and flattens them into `builtins.foldl'` loops. Each fold step threads fuel through the accumulator: ``` foldl'(λ{acc, fuel}. λi. if fuel ≤ 0 then THROW "normalization budget exceeded" else { acc = step(fuel, acc, chain[i]); fuel = fuel - 1; }) {acc = base; fuel = fuel} [1..n] ``` This ensures that an N-element chain consumes N units of fuel from the fold, plus whatever fuel each step application consumes internally. Without this threading, each step would get the original fuel budget, giving an effective budget of N × fuel. The worst-case complexity of a threaded fold is O(fuel²): at step *i*, the inner `vAppF` receives `fuel - i` as its own per-path budget. Summing over all steps gives Σ(fuel - i) ≈ fuel²/2. To achieve O(fuel), `vAppF` would need to return remaining fuel — an invasive signature change. The quadratic residual is inherent to per-path fuel semantics and is a strict improvement over the pre-threading O(N × fuel) with unbounded N. ### 9.5 Fuel consumption in constructor chains Generated constructor evaluation flattens chains of n `DescCon` layers when the description's linear profile proves the recursion is structurally homogeneous. The evaluator deducts n fuel units from the budget before rebuilding the semantic value. Generated natural and list constructors are instances of this generic path, so the 5000-deep stress tests are evidence for the description-level trampoline rather than for datatype-specific hard-coding. --- ## 10. Properties the Implementation Must Satisfy ### 10.1 Soundness (non-negotiable) If the kernel accepts `Γ ⊢ t : A`, then `t` is a valid term of type `A` in MLTT with the specified type formers and universe hierarchy. Formally: **If `check(Γ, t, A)` succeeds, then `Γ ⊢ t : A` is derivable in the declarative typing rules of MLTT.** Equivalently: the kernel never accepts an ill-typed term. ### 10.2 Determinism For any input `(Γ, t, A)`, the kernel produces the same result on every invocation. There is no randomness, no system-dependent behavior, no sensitivity to evaluation order (beyond fuel exhaustion, which always rejects). ### 10.3 Termination For any input `(Γ, t, A)`, the kernel terminates. It either: - Accepts (returns the elaborated term) - Rejects with a type error (via effect) - Rejects with fuel exhaustion - Crashes with a kernel bug diagnostic (throw) It never loops. The fuel mechanism guarantees this. ### 10.4 Evaluation roundtrip For any well-typed term `t` and environment `ρ` consistent with the context: ``` quote(d, eval(ρ, quote(d, eval(ρ, t)))) = quote(d, eval(ρ, t)) ``` Evaluation followed by quotation is idempotent. The result is a normal form. ### 10.5 Conversion reflexivity For any value `v`: ``` conv(d, v, v) = true ``` ### 10.6 Conversion symmetry For any values `v₁, v₂`: ``` conv(d, v₁, v₂) = conv(d, v₂, v₁) ``` ### 10.7 Conversion transitivity For any values `v₁, v₂, v₃`: ``` conv(d, v₁, v₂) ∧ conv(d, v₂, v₃) ⟹ conv(d, v₁, v₃) ``` ### 10.8 Type preservation under evaluation If `Γ ⊢ t : A` and `eval(Γ.env, t) = v`, then `v` represents a value of type `A`. This is not directly testable (values don't carry types) but is ensured by the correctness of the evaluation rules. ### 10.9 Strong normalization (for well-typed terms) For any well-typed term `t`, `eval` terminates without exhausting fuel for a sufficiently large fuel budget. The fuel mechanism is a practical safeguard, not a theoretical necessity for well-typed terms. --- ## 11. Derived Test Cases Every rule in this spec generates at least one positive test (the rule applies and succeeds) and one negative test (the rule's premises are violated and the kernel rejects). ### 11.1 Required positive tests (kernel must ACCEPT) ``` -- Public generated identity ⊢ H.refl : H.eq H.nat H.zero H.zero -- Function type ⊢ Lam(x, H.nat, Var(0)) : Pi(x, H.nat, H.nat) -- Application f : Pi(x, H.nat, H.nat) ⊢ App(f, H.zero) : H.nat -- Dependent function ⊢ Lam(A, U(0), Lam(x, Var(0), Var(0))) : Pi(A, U(0), Pi(x, A, A)) -- Sigma pair ⊢ Pair(H.zero, Tt, Sigma(x, H.nat, Unit)) : Sigma(x, H.nat, Unit) -- Generated natural induction: 0 + 0 = 0 ⊢ H.refl : H.eq H.nat (H.ind ... H.zero) H.zero -- List ⊢ H.cons H.nat H.zero (H.nil H.nat) : H.listOf H.nat -- Sum injection ⊢ H.inl H.nat Unit H.zero : H.sum H.nat Unit -- Universe hierarchy ⊢ U(0) : U(1) ⊢ U(1) : U(2) ⊢ H.nat : U(0) ⊢ Pi(x, H.nat, H.nat) : U(0) -- Let binding ⊢ Let(x, H.nat, H.zero, Var(0)) : H.nat -- StrEq: type inference returns the derived H.bool -- (= μ ⊤ (plus (retI tt) (retI tt)) tt; see §4.11) ⊢ StrEq(StringLit("a"), StringLit("b")) : H.bool -- StrEq reduction: equal strings reduce to the derived true_ value; -- unequal strings reduce to false_. Both witnessed via H.refl over the -- derived-bool form. Expressing this rule at the Tm level requires -- the plus/μ machinery; see the examples/verified-functions.nix -- fixture `recordStrEqMatch` for an executable test. ``` ### 11.2 Required negative tests (kernel must REJECT) ``` -- Type mismatch ⊢ H.zero : Unit REJECT -- Universe violation ⊢ U(0) : U(0) REJECT -- Non-cumulativity: a U(0) type is not accepted at U(1) ⊢ H.nat : U(1) REJECT (no subsumption; use Lift, §8.3) -- H.refl on unequal terms ⊢ H.refl : H.eq H.nat H.zero (H.succ H.zero) REJECT -- Application of non-function ⊢ App(H.zero, H.zero) REJECT -- Projection of non-pair ⊢ Fst(H.zero) REJECT -- Wrong eliminator scrutinee ⊢ H.ind ... Tt REJECT (Tt : Unit, not H.nat) -- Unbound variable ⊢ Var(0) (in empty context) REJECT -- StrEq on non-string ⊢ StrEq(H.zero, StringLit("foo")) REJECT (lhs is H.nat, expected String) -- Ill-typed pair under expected Sigma ⊢ Pair(H.zero, H.zero) ⇐ Sigma(x, H.nat, Unit) REJECT ``` ### 11.3 Required stress tests ``` -- Large H.nat: H.succ^5000(H.zero) : H.nat ACCEPT (trampoline) -- Large H.listOf: H.cons^5000 : H.listOf H.nat ACCEPT (trampoline) -- H.ind on H.succ^5000(H.zero) ACCEPT (trampoline) -- H.listElim on H.cons^5000 ACCEPT (trampoline) -- Succ elaboration: elab-succ-5000 ACCEPT (trampoline) -- Cons elaboration: elab-cons-5000 ACCEPT (trampoline) -- Deeply nested Pi: Pi(x₁, ..., Pi(xₙ, H.nat, H.nat)...) for n=500 ACCEPT -- Fuel exhaustion: artificially low fuel on complex term REJECT (fuel) -- Fuel threading: generated natural fold decrements fuel per step ACCEPT -- Fuel threading: generated list fold decrements fuel per step ACCEPT ``` ### 11.4 Required roundtrip tests For each value form, verify: ``` quote(d, eval(ρ, t)) = normal_form(t) ``` where `normal_form(t)` is the expected normal form. --- ## 12. Notation Index | Symbol | Meaning | |--------|---------| | Γ | Typing context | | ρ | Value environment | | d | Binding depth (for levels ↔ indices) | | ⊢ | Typing judgment | | ⇐ | Checking mode | | ⇒ | Synthesis mode | | ↝ | Elaborates to | | ≡ | Definitional equality | | Π | Dependent function type | | Σ | Dependent pair type | | ℕ | Natural numbers | | 𝔹 | Booleans (derived: `μ ⊤ (plus (retI tt) (retI tt)) tt`) | | ⊤ | Unit type | | ⊥ | Empty type | | U(i) | Universe at level i | | Id_A(a,b) | Identity type | | TCB | Trusted computing base | | WHNF | Weak head normal form | | NbE | Normalization by evaluation | | THROW | Kernel invariant violation (crash) | | REJECT | Term rejected (via effect or fuel) | --- ## 13. Known Limitations The following are documented implementation choices or limitations, not bugs. They are recorded here so auditors do not rediscover them. ### 13.1 Trusted annotation sidecars are semantically erased `Ann` terms may carry implementation sidecars such as `trusted`, `_descRef`, `_label`, and `_conLabel`. Evaluation may propagate those sidecars to values for performance, source maps, or generated datatype metadata, but conversion ignores them. They must never affect definitional equality. ### 13.2 Lambda domain annotations discarded in checking mode When checking `Lam(n, A, t)` against `VPi(n, dom, cl)`, the lambda's domain annotation `A` is discarded and replaced by `dom` from the Pi type. This is standard bidirectional type checking (Dunfield & Krishnaswami 2021, §4): in checking mode, the expected type provides the domain, not the term. The elaborated output uses `quote(d, dom)`, making the original annotation unrecoverable. ### 13.3 Term constructors do not validate argument types Term constructors (`mkVar`, `mkApp`, etc.) accept arbitrary Nix values without type validation. `mkVar "hello"` produces `{ tag = "var"; idx = "hello"; }`, which crashes at eval time. The trust boundary is the HOAS layer (`src/tc/hoas/`), which is the public API — direct term construction is internal to the kernel. ### 13.4 `tryEval` only catches `throw` and `assert false` `builtins.tryEval` in the elaborator's `isConstantFamily` sentinel detection only catches explicit `throw` and `assert false`. Nix coercion errors (e.g., "cannot convert a function to JSON"), missing attribute access, and type comparison errors are uncatchable. The elaborator uses `builtins.typeOf` in error paths to avoid triggering coercion errors. ### 13.5 HOAS sentinel comparison The `isConstantFamily` sentinel test in the elaborator applies two distinct sentinel values and compares the results to detect whether a binding body is dependent. Both Pi and Sigma paths compare **elaborated kernel terms** (`H.elab r1.value == H.elab r2.value`) rather than raw HOAS trees. This avoids false negatives from Nix's function identity comparison (`==` on lambdas). However, if `H.elab` itself produces structurally different terms for semantically equivalent types (e.g., through different elaboration paths), false negatives remain possible. This is a safe failure mode — the kernel still type-checks correctly, but elaboration may require explicit `_kernel` annotations unnecessarily. ### 13.6 StrEq neutral canonicalization When one argument to `vStrEq` is neutral and the other is a literal, the neutral's spine is extended with `EStrEq(literal)`. When both arguments are neutral, the **left** neutral's spine is extended with `EStrEq(right)`. This means `StrEq(x, y)` and `StrEq(y, x)` (where both are neutral) produce different normal forms: `VNe(x, [EStrEq(y)])` vs `VNe(y, [EStrEq(x)])`. Therefore `conv` will report them as **not** definitionally equal, even though `StrEq` is semantically symmetric. This is a safe conservatism: the kernel may reject some provable equalities but never accepts a false one. ### 13.7 Extract uses type value threading (not sentinels) The `extract` function threads kernel type values (`tyVal`) through recursive extraction, rather than using sentinel-based non-dependence tests. For Pi extraction, the codomain type is computed per-invocation via `instantiate(tyVal.closure, kernelArg)`, supporting both dependent and non-dependent function extraction. For Sigma extraction (records), the second component's type is computed via `instantiate(tyVal.closure, val.fst)`. A `reifyType : Val → HoasTree` fallback converts kernel type values back to HOAS when the HOAS body cannot be applied (e.g., when the body accesses record fields from a neutral). `reifyType` loses sugar (VSigma → `H.sigma`, not `H.record`) so the HOAS body is preferred when available. ### 13.8 Spine comparison complexity `convSp` uses `builtins.elemAt` in a fold to compare neutral spines. In Nix, `builtins.elemAt` on lists is O(1) (Nix lists are internally vectors/arrays), so the actual complexity is O(n), not O(n²). This was incorrectly flagged in an earlier audit. --- ## References 1. Coquand, T. et al. (2009). *A simple type-theoretic language: Mini-TT.* 2. Dunfield, J. & Krishnaswami, N. (2021). *Bidirectional Typing.* ACM Computing Surveys. 3. Kovács, A. (2022). *Generalized Universe Hierarchies.* CSL 2022. 4. Abel, A. & Chapman, J. (2014). *Normalization by Evaluation in the Delay Monad.* 5. Girard, J.-Y. (1972). *Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur.* Thèse d'État, Université Paris 7. 6. Hurkens, A. J. C. (1995). *A Simplification of Girard's Paradox.* TLCA 1995. 7. de Bruijn, N. (1972). *Lambda Calculus Notation with Nameless Dummies.* 8. Martin-Löf, P. (1984). *Intuitionistic Type Theory.* Bibliopolis. 9. Felicissimo, T. (2023). *Generic Bidirectional Typing for Dependent Type Theories.*