Functions, total and sealed

An expression that is used twice, or that needs a name to be read, becomes a function. Vishy has two kinds. A core function is total: it always finishes, which is what lets contracts and rules call it and the verifier reason about it. A sealed function may do anything a general-purpose language does, recursion and unbounded loops included, and sits behind a boundary that keeps it away from the state.

Core functions

enum Tier { basic, gold }
fn fee(amount: money(2), tier: Tier) -> money(2) = if tier == Tier.gold then percent(amount, 1) else percent(amount, 3);
examples fee { (10000, Tier.basic) => 300; (10000, Tier.gold) => 100; }
fn digits(n: int(0, 999999)) -> int {
    var k = n;
    var d = 0;
    repeat 6 {
        if k == 0 { break; }
        k := k / 10;
        d := d + 1;
    }
    if d == 0 then 1 else d
}
examples digits { (0) => 1; (7) => 1; (42) => 2; (999999) => 6; }
unit Till {
    state takings: money(2) = 0;
    state fees: money(2) = 0;
    contract charge(amount: money(2), tier: Tier) -> money(2) {
        case amount <= 0 => fail BadAmount;
        else => Charged(fee(amount, tier)): takings += amount - fee(amount, tier), fees += fee(amount, tier);
        examples {
            {} (10000, Tier.basic) => Charged(300) { takings: 9700, fees: 300 };
        }
    }
    contract code_length(code: int(0, 999999)) -> int => Length(digits(code));
}
scenario a_sale {
    Till.charge(10000, Tier.gold) => Charged(100);
    Till.code_length(4711) => Length(4);
}

fn fee(…) -> money(2) = …; is a function whose body is one expression. examples fee { … } are its acceptance tests, written like a contract’s without the states: arguments and the result they must give. vishy verify runs them with the contracts’ examples, so the seven examples in this program are two for fee, four for digits and one for charge:

verify: 7 examples, 2 scenario steps and 4000 sampled checks passed

A contract calls a function like a builtin: Charged(fee(amount, tier)). A function may also be declared inside a unit, where it can read the unit’s state; the one above is at the top level and reads only its arguments.

Block bodies

digits needs a loop, so its body is a block: statements in braces, then the result expression.

let x = e; names a value; var x = e; names one that may change, with x := e;.
if c { … } else { … } chooses between statements.
repeat n { … } runs its body at most n times, and break; leaves it early.

repeat 6 is the loop’s bound, written where the loop is: a number of at most six digits needs at most six divisions. Every loop in a core function has one. There is no while, and a function may not call itself, directly or through another function (book/refusals/recursion.vish):

unit Counter {
    state n: int = 0;
    contract set(k: int(0, 10)) => Done: n := fact(k);
}
fn fact(k: int) -> int = if k <= 1 then 1 else k * fact(k - 1);

book/refusals/recursion.vish:5:4: error: `fact` calls itself; a core function is total, recursion belongs to a `sealed fn`
  fn fact(k: int) -> int = if k <= 1 then 1 else k * fact(k - 1);
     ^^^^

So every core function finishes, on every input, in a number of steps its bounds limit. That is what makes a rule that calls one checkable: the verifier calls it thousands of times on sampled states and never waits. Blocks are for functions only; a contract stays a list of cases and deltas.

Sealed functions

Some computation does not fit: a parser, a walk over a tree of unknown depth, a search that stops when it finds something. That is the sealed layer:

sealed row Node { name: string, kids: Node[] }
sealed fn size(n: Node) -> int = 1 + fold(k in n.kids, acc = 0: acc + size(k));
examples size { (Node { name: "a", kids: [Node { name: "b", kids: [] }, Node { name: "c", kids: [Node { name: "d", kids: [] }] }] }) => 4; }
sealed fn words(s: string) -> int = len(split(s, " "));
examples words { ("to be or not") => 4; }
sealed fn first_long(s: string, n: int) -> int {
    let ws = split(s, " ");
    var i = 0;
    while i < len(ws) {
        if len(ws[i]) >= n { return i; }
        i := i + 1;
    }
    -1
}
examples first_long { ("a tiny example", 5) => 2; ("a b c", 5) => -1; }
unit Notes {
    state longest: int = 0;
    contract note(text: string(64)) -> int {
        else => Words(words(text)): longest max= words(text);
        examples {
            { longest: 2 } ("to be or not") => Words(4) { longest: 4 };
        }
    }
}
scenario two_notes {
    Notes.note("hello world") => Words(2);
    Notes.note("hi") => Words(1);
}

A sealed fn may:

call itself, as size does to count the nodes of a tree;
loop with while, and leave early with return e;, as first_long does;
take and return string and lists with no bound, string rather than string(64).

A sealed row may contain itself: Node has a list of Nodes, which a core row may not, as the chapter on rows showed. Sealed rows exist only inside sealed functions.

The contract note calls words, a sealed function, on its string(64) argument, and stores the result in the unit. That is how the two layers meet: a core value goes in, a core value comes out, and the result is trusted only to its declared type.

scenario two_notes
  Notes.note("hello world") => Words(2)
  Notes.note("hi") => Words(1)
  Notes = Notes { longest: 2 }
2 step(s), all as expected

verify: 5 examples, 2 scenario steps and 2000 sampled checks passed

The boundary

Sealed code never touches unit state or events. A sealed function has no unit in scope and cannot emit; and nothing in a unit may hold a sealed value (book/refusals/functions-sealed-state.vish):

book/refusals/functions-sealed-state.vish:3:5: error: state field `root` of unit `Outline` cannot hold the sealed row `Node`; sealed rows live only in sealed functions
      state root: Node;
      ^^^^^^^^^^^^^^^^^

The rule is what keeps the rest of the book true. Everything the verifier reasons about, the state, the deltas, the rules, is core, with bounds it knows; the sealed layer is a pure function it can call and nothing else.

The step budget

A sealed function is not promised to finish, so the verifier runs it under a budget: ten million steps by default, one per call and one per loop iteration, set with the variable VISHY_FUEL. A function that runs out fails the example or the sampled check that reached it (book/failures/functions-fuel.vish):

sealed fn collatz(n: int) -> int {
    var k = n;
    var steps = 0;
    while k != 1 {
        if k % 2 == 0 { k := k / 2; } else { k := 3 * k + 1; }
        steps := steps + 1;
    }
    steps
}
examples collatz { (1) => 0; (6) => 8; (0) => 0; }

verify FAILED: 1 failure(s):
[1] examples collatz case 3: sealed function `collatz` did not finish within 10000000 steps

The third example starts the loop at zero, which halves to zero forever. In a core function the same loop would need a repeat bound and would stop; here the budget is what stops it, and the failure names the function and the example. The verifier never samples a sealed function on its own, since it has no bounded inputs to draw from: its examples are its tests, together with every call a contract makes during the sampled checks.

Try

Delete the example (0) => 0; from collatz and verify again: it passes, since the other two finish. Now run it as VISHY_FUEL=5 vishy verify book/failures/functions-fuel.vish 7 1000. The example (6) => 8 fails, because it needs nine steps, one for the call and one for each of its eight iterations.

Keyboard shortcuts