# 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

```nix
# 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
- `matchData : Datatype → Hoas → Hoas → { <con>; } → Hoas` — any non-parametric `H.datatype`
- `elimData : Level → Datatype → Hoas → Hoas → { <con>; } → Hoas` — `matchData` with a dependent motive

## 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
```

## `elimData`

_elimData: generic non-parametric user-datatype eliminator with dependent motive — builds branch binders from `_dtypeMeta` and ann-wraps each body against the meta-β-reduced motive image, so branch bodies are checked rather than synthesised. Handlers keyed by ctor name, curried over fields then one IH per `recAt` field._

```
elimData : Level -> Datatype -> Hoas -> Hoas -> { <con> : field… -> ih… -> 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.

## `matchData`

_matchData: `elimData` with constant motive `λ_.resultTy` — the `matchSum`/`matchList` analogue for arbitrary non-parametric `H.datatype`s._

```
matchData : Datatype -> Hoas -> Hoas -> { <con> : field… -> ih… -> Hoas; } -> Hoas
```

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