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.

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.

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.

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.

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.

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)));