Verified

High-level combinators for writing kernel-checked implementations. Write programs with these combinators, then call v.verify to type-check and extract a Nix function that is correct by construction.

Example

# Verified successor: Nat → Nat
v.verify (H.forall "x" H.nat (_: H.nat))
         (v.fn "x" H.nat (x: H.succ x))
# → Nix function: n → n + 1

Literals

• nat : Int → Hoas — natural number literal (S^n(zero))
• str : String → Hoas — string literal
• int_ : Int → Hoas — integer literal
• float_ : Float → Hoas — float literal
• true_, false_ — boolean literals
• null_ — unit value (tt)

Binding

• fn : String → Hoas → (Hoas → Hoas) → Hoas — lambda abstraction
• let_ : String → Hoas → Hoas → (Hoas → Hoas) → Hoas — let binding

Data Operations

• pair, fst, snd — Σ-type construction and projection
• field : Hoas → String → Hoas → Hoas — record field projection by name
• inl, inr — Sum injection
• app — function application

Eliminators (Constant Motive)

These auto-generate the motive λ_.resultTy, so you only supply the result type and the branches:

• if_ : Hoas → Hoas → { then_; else_; } → Hoas — Bool elimination
• match : Hoas → Hoas → { zero; succ : k → ih → Hoas; } → Hoas — Nat elimination
• matchList : Hoas → Hoas → Hoas → { nil; cons : h → t → ih → Hoas; } → Hoas — List elimination
• matchSum : Hoas → Hoas → Hoas → Hoas → { left; right; } → Hoas — Sum elimination

Derived Combinators

• map : Hoas → Hoas → Hoas → Hoas → Hoas — map f over a list
• fold : Hoas → Hoas → Hoas → Hoas → Hoas → Hoas — fold over a list
• filter : Hoas → Hoas → Hoas → Hoas — filter a list by predicate

Pipeline

• verify : Hoas → Hoas → NixValue — type-check + eval + extract
• verifiedFn : Hoas → Hoas → VerifiedValue — callable value with _hoasImpl for full kernel body verification in parent types

app

app: HOAS function application — app f arg builds the redex; β-reduces during normalisation when f is a lambda.

app : Hoas -> Hoas -> Hoas

false_

false: HOAS literal — the False constructor of H.bool as inl tt; reflects the bool-as-sum levitation discipline._

false_ : Hoas

field

field: HOAS record field-projection by name — derives the universal-property eliminator for a mono-constructor datatype and applies it to extract the named field.

field : Hoas -> String -> Hoas -> Hoas

Requires recordTy to carry _dtypeMeta with exactly one constructor (records are mono-constructor datatypes via H.record). Throws at build time if the type is multi-constructor, has no fields, or the requested field name is absent. The 1-field special case reduces via ι (elim P (λa.a) (mk a) ≡ a); no surface branching is needed. Field positions are read from meta.constructors[0].fields in declaration order, so renaming a field in source is a breaking change.

filter

filter: HOAS list-filter combinator — keeps elements where pred : elemTy -> Bool returns true_; built on listElim plus per-element boolElim.

filter : Hoas -> Hoas -> Hoas -> Hoas

Annotates pred with H.forall "_" elemTy (_: H.bool) so the application infers. pred must be a HOAS function term producing a bool HOAS value (e.g. via if_, match, or a direct true_/false_). Element order is preserved; the accumulator threads via the inductive hypothesis.

float_

float: HOAS literal — lift a Nix float to a floatLit HOAS term checkable against H.float_._

float_ : Float -> Hoas

fn

fn: HOAS lambda — fn name domTy body builds λ(name:domTy). body, with body a Nix function receiving the bound variable as a HOAS term.

fn : String -> Hoas -> (Hoas -> Hoas) -> Hoas

fold

fold: HOAS list-fold combinator — combines elements right-to-left using f : elemTy -> resultTy -> resultTy starting from init.

fold : Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas

Annotates f with H.forall "_" elemTy (_: H.forall "_" resultTy (_: resultTy)) so the applications f h ih infer correctly. f must be a HOAS function term built with fn (or nested fn for the curried two-argument case). The accumulator threads through ih; the empty-list case returns init.

fst

fst: first projection on a HOAS Σ-pair; reduces by π₁ during normalisation.

fst : Hoas -> Hoas

if_

if: bool-elimination wrapper — supplies a constant motive λ_.resultTy so callers write only the result type and the two branches._

if_ : Hoas -> Hoas -> { then_ : Hoas; else_ : Hoas; } -> Hoas

Use when the branch result type does not depend on the scrutinee. For a dependent motive (different result type per branch), drop to H.boolElim directly. The synthesised motive is λ_:bool.resultTy; boolElim's level argument is fixed at 0 here, so cross-universe branching also needs H.boolElim.

inl

inl: HOAS sum left-injection — inl leftTy rightTy term builds an A + B term carrying term : A in the left branch.

inl : Hoas -> Hoas -> Hoas -> Hoas

inr

inr: HOAS sum right-injection — inr leftTy rightTy term builds an A + B term carrying term : B in the right branch.

inr : Hoas -> Hoas -> Hoas -> Hoas

int_

int: HOAS literal — lift a Nix integer to an intLit HOAS term checkable against H.int_ (the kernel Int axiom, distinct from nat)._

int_ : Int -> Hoas

let_

let: HOAS let binding — let_ name ty val body builds let name : ty = val in body; body is a Nix function receiving the bound variable._

let_ : String -> Hoas -> Hoas -> (Hoas -> Hoas) -> Hoas

makeRecord

makeRecord: HOAS record construction by name — applies the mono-constructor of a μ-encoded record type to the field values in declaration order, dual to field's named projection.

makeRecord : Hoas -> { <field> = Hoas; ... } -> Hoas

Dual to field. Given a record type built by H.record (or any mono-constructor datatype carrying _dtypeMeta) and an attrset keyed by field name, produces the HOAS term mk a₀ … aₙ₋₁ where each aᵢ is read from argsAttrs by field name, and field order follows meta.constructors[0].fields (for H.record, alphabetical by name).

Throws at build time on a multi-constructor datatype, a missing required field, or an unknown extra field. The constructor term used is meta.constructors[0].ctor, exposed on the kernel datatype attrset by _datatypeImpl.

Use this in verified implementations that return records, so consumer code never needs to reach for builtins.foldl' H.app DT.mk [...] or know the μ-encoding.

map

map: HOAS list-map combinator built on listElim — applies f : elemTy -> resultTy to every element, threading the inductive hypothesis to accumulate the output list.

map : Hoas -> Hoas -> Hoas -> Hoas -> Hoas

Annotates f with H.forall "_" elemTy (_: resultTy) so the kernel can infer the application type. f must be a HOAS function term (build one with fn), not a Nix function. For element transformations that aren't expressible as a uniform HOAS function (e.g. type-dependent on element shape), drop to H.listElim directly.

match

match: nat-elimination wrapper — supplies a constant motive λ_.resultTy; the succ callback receives both predecessor k and inductive hypothesis ih.

match : Hoas -> Hoas -> { zero : Hoas; succ : Hoas -> Hoas -> Hoas; } -> Hoas

The succ callback receives two HOAS values: k (the predecessor binder, of type nat) and ih (the inductive hypothesis, of type resultTy). Use when result type is non-dependent on the scrutinee; drop to H.ind for dependent motives. Level is fixed at 0 by the synthesised motive.

matchList

matchList: list-elimination wrapper — constant motive λ_.resultTy; the cons callback binds head, tail, and inductive hypothesis.

matchList : Hoas -> Hoas -> Hoas -> { nil : Hoas; cons : Hoas -> Hoas -> Hoas -> Hoas; } -> Hoas

The cons callback receives three HOAS values: h (the head element of type elemTy), t (the tail list of type listOf elemTy), and ih (the inductive hypothesis of type resultTy). For dependent motives, drop to H.listElim. Level fixed at 0.

matchSum

matchSum: sum-elimination wrapper — constant motive λ_.resultTy; the left and right callbacks receive their respective payloads.

matchSum : Hoas -> Hoas -> Hoas -> Hoas -> { left : Hoas -> Hoas; right : Hoas -> Hoas; } -> Hoas

Each callback receives one HOAS value: the left payload for left, the right payload for right. Use when the result type doesn't depend on which case fires; drop to H.sumElim for dependent motives. Level fixed at 0.

nat

nat: HOAS literal — wrap a Nix Int as a succ^n zero natural-number HOAS term checkable against H.nat.

nat : Int -> Hoas

null_

null: HOAS literal — the unique inhabitant tt of H.unit; the conventional empty / placeholder value in verified code._

null_ : Hoas

pair

pair: HOAS Σ-pair constructor — pair fst snd packages two HOAS values; the surrounding annotation fixes which Σ-type the pair inhabits.

pair : Hoas -> Hoas -> Hoas

snd

snd: second projection on a HOAS Σ-pair; reduces by π₂ during normalisation.

snd : Hoas -> Hoas

str

str: HOAS literal — lift a Nix String to a stringLit HOAS term checkable against H.string.

str : String -> Hoas

strElem

strElem: HOAS membership check on a List String — folds strEq target across the list, accumulating true_ if any element matches.

strElem : Hoas -> Hoas -> Hoas

Built on fold plus strEq: each list element is compared to target; the accumulator starts at false_ and stays true_ once a match is seen. Use when verified code needs a membership predicate over strings; for raw kernel-level equality on a single pair, use strEq.

strEq

strEq: kernel string equality returning a Bool HOAS term; reflects the mkStrEq primitive of the kernel.

strEq : Hoas -> Hoas -> Hoas

true_

true: HOAS literal — the True constructor of H.bool as inr tt; reflects the bool-as-sum levitation discipline._

true_ : Hoas

verifiedFn

verifiedFn: extract a kernel-verified callable carrying _hoasImpl — elaborateValue's Pi case uses the HOAS body for full re-verification instead of falling back to an opaque trust boundary.

verifiedFn : Hoas -> Hoas -> { __functor; _hoasImpl }

Returns an attrset callable via __functor (so (verifiedFn piTy body) arg works) and carrying _hoasImpl = body so parent elaboration can re-check the body against a more general type instead of treating it as an opaque lambda. Use when the verified function will be embedded inside another verified type-check (e.g. as a field of a verified record); for standalone use, verify is simpler.

verify

verify: full pipeline — kernel-check a HOAS implementation against a HOAS type, then evaluate and extract a Nix value witnessing the body.

verify : Hoas -> Hoas -> NixValue

Calls fx.tc.elaborate.verifyAndExtract internally. Returns the Nix value (typically a function or data structure) that the type-checked HOAS body denotes; consume via normal Nix call or attribute access. Use as the final step of a verified-implementation pipeline. For a callable wrapper that retains the HOAS implementation so parent-type elaboration can re-check the body, use verifiedFn instead.