# Verified Functions


`fx.types.verified.verify` checks a HOAS implementation against a type,
evaluates it, and extracts a Nix value. The result can be called like an
ordinary function, but it first passed through the kernel.

## First functions

The smallest verified programs are ordinary unary functions. The
type says what the extracted Nix function accepts and returns; the
implementation is written with verified HOAS constructors.

```nix
succFn = v.verify (H.forall "x" H.nat (_: H.nat))
  (v.fn "x" H.nat (x: H.succ x));

succApply5 = succFn 5 == 6;

notFn = v.verify (H.forall "b" H.bool (_: H.bool))
  (v.fn "b" H.bool (b:
    v.if_ H.bool b { then_ = v.false_; else_ = v.true_; }));
```

## Recursion over naturals

`v.match` builds the eliminator for naturals. Addition uses the
first argument as the scrutinee and returns a function awaiting the
second argument.

```nix
addFn = v.verify (H.forall "m" H.nat (_: H.forall "n" H.nat (_: H.nat)))
  (v.fn "m" H.nat (m: v.fn "n" H.nat (n:
    v.match H.nat m {
      zero = n;
      succ = _k: ih: H.succ ih;
    })));

add2and3 = addFn 2 3 == 5;
```

## Lists and pipelines

List combinators remain checked HOAS terms until extraction. The
composed example filters zeros out of a list and folds the remaining
values into a sum.

```nix
mapSuccResult = v.verify (H.listOf H.nat)
  (v.map H.nat H.nat
    (v.fn "x" H.nat (x: H.succ x))
    (H.cons (v.nat 0) (H.cons (v.nat 1)
      (H.cons (v.nat 2) H.nil))));

composedResult =
  let
    input = H.cons (v.nat 0) (H.cons (v.nat 3)
      (H.cons (v.nat 0) (H.cons (v.nat 2)
        (H.cons (v.nat 1) H.nil))));
    nonZero = v.fn "n" H.nat (n:
      v.match H.bool n {
        zero = v.false_;
        succ = _k: _ih: v.true_;
      });
  in
  v.verify H.nat (v.fold H.nat H.nat (v.nat 0) addCombine
    (v.filter H.nat nonZero input));
```

## Sums, lets, pairs, and records

Verified extraction also covers the richer HOAS constructors used by
nix-effects types: coproduct elimination, local bindings, sigma
pairs, and record field projection.

```nix
sumLeftResult = v.verify H.nat
  (v.matchSum H.nat H.bool H.nat (v.inl H.nat H.bool (v.nat 5)) {
    left = x: H.succ x;
    right = b: v.if_ H.nat b { then_ = v.nat 1; else_ = v.nat 0; };
  });

recordGetX = v.verify
  (H.forall "r"
    (H.record [{ name = "x"; type = H.nat; } { name = "y"; type = H.bool; }])
    (_: H.nat))
  (v.fn "r"
    (H.record [{ name = "x"; type = H.nat; } { name = "y"; type = H.bool; }])
    (r: v.field
      (H.record [{ name = "x"; type = H.nat; } { name = "y"; type = H.bool; }])
      "x"
      r));
```

## Strings and records

The final examples use kernel-verified string predicates directly
and then combine them with record projection.

```nix
strEqFn = v.verify (H.forall "a" H.string (_: H.forall "b" H.string (_: H.bool)))
  (v.fn "a" H.string (a: v.fn "b" H.string (b: v.strEq a b)));

recordStrEqFn =
  let
    recTy = H.record [
      { name = "name"; type = H.string; }
      { name = "target"; type = H.string; }
    ];
  in
  v.verify (H.forall "r" recTy (_: H.bool))
    (v.fn "r" recTy (r:
      v.strEq (v.field recTy "name" r) (v.field recTy "target" r)));
```