Reading the state: expressions and quantifiers

Guards, carried values, invariants and the right-hand sides of deltas are all expressions: they read the state and compute a value, and they change nothing. This chapter is the vocabulary for reading a table. Its program is a job queue whose contracts only read, each with examples that pin the answer down.

enum Priority { low, normal, urgent }
row Job { id: id, priority: Priority, size: int(1, 100), added: instant, owner: option<id> }
unit Queue {
    state jobs: Job[8];
    fixture Three = { jobs: [
        Job { id: 1, priority: Priority.normal, size: 40, added: 100, owner: none },
        Job { id: 2, priority: Priority.urgent, size: 10, added: 300, owner: some(7) },
        Job { id: 3, priority: Priority.urgent, size: 25, added: 200, owner: none } ] };
    fn weight(j: Job) -> int = match j.priority { Priority.low => 1, Priority.normal => 2, Priority.urgent => 5 };
    contract total() -> int {
        else => Total(sum(jobs.size));
        examples { Three () => Total(75); }
    }
    contract big() -> int {
        else => Big(count(jobs.size > 20));
        examples { Three () => Big(2); }
    }
    contract free() -> id[8] {
        else => Free(where(j in jobs: j.owner == none).id);
        examples { Three () => Free([1, 3]); }
    }
    contract all_small() -> bool {
        else => AllSmall(all(j in jobs: j.size < 50));
        examples { Three () => AllSmall(true); }
    }
    contract first_urgent() -> id {
        case !any(j in jobs: j.priority == Priority.urgent) => fail NoneUrgent;
        else => FirstUrgent(first(j in jobs: j.priority == Priority.urgent).id);
        examples { Three () => FirstUrgent(2); {} () => NoneUrgent; }
    }
    contract next() -> id {
        case !any(j in jobs: j.owner == none) => fail Idle;
        else => let j = best(j in jobs: j.owner == none by (j.priority < Priority.urgent, j.added)); Next(j.id);
        examples { Three () => Next(3); {} () => Idle; }
    }
    contract load() -> int {
        else => Load(fold(j in jobs, acc = 0: acc + weight(j) * j.size));
        examples { Three () => Load(255); }
    }
    contract owner_of(job: id) -> id {
        case jobs[job].owner == none => fail Unowned;
        else => Owner(match jobs[job].owner { some o => o, none => job });
        examples { Three (2) => Owner(7); Three (1) => Unowned; }
    }
    contract doubled(job: id) -> int {
        else => Doubled(let j = with(jobs[job], size, jobs[job].size * 2) in weight(j) * j.size);
        examples { Three (1) => Doubled(160); }
    }
}

fixture Three = { … } names a state, three jobs, so that every example can start from it by name instead of spelling the jobs out again. The last chapter of this part covers fixtures.

Plain expressions

Arithmetic + - * / %, comparisons, && || !, and if c then a else b are what you expect. r.f reads a field of a row, t[k] reads the row with key k, and k in t asks whether there is one. len, min, max, abs, clamp and percent are builtins.

Columns

jobs.size is a column: the size of every job, in table order, as a list. A reduction turns it into one value: sum(jobs.size) is the total work, 75. Operators apply to a column element by element, so jobs.size > 20 is a column of bools, and count(jobs.size > 20) counts the true ones: two jobs are bigger than twenty. That is the whole idea of lifting: write the question about one row and put the column where the row would be.

Quantifiers

A quantifier binds a name to each row in turn and asks a question:

where(…).id is the ids of the matching rows: the free jobs are [1, 3]. first and best return a row, so there must be one: first_urgent and next guard with any and fail with an outcome of their own when there is none.

best sorts by the key tuple and takes the smallest, ties broken by id. A bool sorts false before true, so j.priority < Priority.urgent as the first key puts urgent jobs first, and j.added as the second picks the oldest among them. Job 2 is urgent but taken, job 3 is urgent and free, so next() answers 3 although job 1 has waited longer.

fold is the general case: an accumulator, a starting value, and a body computing the next accumulator from it and the row. load weighs each job by its priority and sums, 255.

Naming things: let and with

let x = e in body names a value inside an expression. A case may also bind before its outcome, as next does: let j = best(…); Next(j.id), so the selection is computed once and read twice.

with(r, f, e) is the row r with field f replaced by e: a new value, nothing changed. doubled asks what a job would weigh at twice its size without touching the job.

match

An option is read with match: match jobs[job].owner { some o => o, none => job }, where o is the value inside for that arm. An enum is read the same way, one arm per variant, as weight does. The match must cover every variant or end with an else arm, and the checker holds you to it (book/refusals/reading-match.vish):

book/refusals/reading-match.vish:5:32: error: match on `Priority` misses Priority.urgent (add the arms or an `else`)
      fn weight(j: Job) -> int = match j.priority { Priority.low => 1, Priority.normal => 2 };
                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This is the refusal that pays for itself the day someone adds a variant: every match without an else that does not handle it becomes a line number.

What is not there

There are no list comprehensions and no loops in an expression (book/refusals/reading-comprehension.vish):

book/refusals/reading-comprehension.vish:4:49: error: expected `,` or `]` in list
      contract sizes() -> int[8] => Sizes([j.size for j in jobs]);
                                                  ^^^

The column jobs.size is that list already, and where, count and fold cover the rest. The reason is what the verifier needs from an expression: every quantifier ranges over a table or a list with a bound, so every expression finishes, and finishes in a number of steps the bound limits. An expression cannot loop forever, cannot build a structure the checker does not know the shape of, and cannot change anything while it reads. Where a computation truly needs a loop, it goes in a function, the subject of the chapter after next.

verify: 12 examples, 0 scenario steps and 9000 sampled checks passed

Twelve examples, one or two per contract, and nine thousand sampled calls on random queues, none of which found first or best asked for a row that is not there.

Try

In next, swap the keys: by (j.added, j.priority < Priority.urgent). The program checks, and vishy verify fails on next’s example: it expected job 3 and got job 1, the oldest free job, which is only normal. The order of the keys is the policy, and one example is enough to hold it.