What the verifier does

vishy verify decides whether a program is accepted, whoever wrote its parts. This chapter is what it runs, in order, what its number counts, and how much each layer catches, measured. The program is the tool library again, whole: the bodies written, a second flow, a rule across the two units, a view, and a notice board that has nothing to do with lending.

row Tool { id: id, copies: int(1, 9), lent: int(0, 9) }
row Card { id: id, holding: int(0, 3) }

unit Shelf {
    state tools: Tool[16];
    invariant all(t in tools: t.lent <= t.copies);
    contract add(tool: id, copies: int(1, 9)) => Added: tools += [Tool { id: tool, copies, lent: 0 }];
    contract lend(tool: id) {
        case tools[tool].lent >= tools[tool].copies => fail NoneLeft;
        else => Lent: tools[tool].lent += 1;
        examples {
            { tools: [Tool { id: 1, copies: 2, lent: 1 }] } (1) => Lent { tools: [Tool { id: 1, copies: 2, lent: 2 }] };
            { tools: [Tool { id: 1, copies: 2, lent: 2 }] } (1) => NoneLeft;
        }
    }
    contract take_back(tool: id) {
        case tools[tool].lent == 0 => fail NotLent;
        else => Returned: tools[tool].lent -= 1;
        examples {
            { tools: [Tool { id: 1, copies: 2, lent: 1 }] } (1) => Returned { tools: [Tool { id: 1, copies: 2, lent: 0 }] };
            { tools: [Tool { id: 1, copies: 2, lent: 0 }] } (1) => NotLent;
        }
    }
}

unit Cards {
    state cards: Card[16];
    invariant all(c in cards: c.holding <= 3);
    contract issue(card: id) => Issued: cards += [Card { id: card, holding: 0 }];
    contract borrow(card: id) {
        case cards[card].holding >= 3 => fail AtLimit;
        else => Borrowed: cards[card].holding += 1;
        examples {
            { cards: [Card { id: 7, holding: 1 }] } (7) => Borrowed { cards: [Card { id: 7, holding: 2 }] };
            { cards: [Card { id: 7, holding: 3 }] } (7) => AtLimit;
        }
    }
    contract give_back(card: id) {
        case cards[card].holding == 0 => fail HoldsNothing;
        else => GaveBack: cards[card].holding -= 1;
        examples {
            { cards: [Card { id: 7, holding: 1 }] } (7) => GaveBack { cards: [Card { id: 7, holding: 0 }] };
            { cards: [Card { id: 7, holding: 0 }] } (7) => HoldsNothing;
        }
    }
}

unit Board {
    state notice: string(64) = "";
    contract post(text: string(64)) => Posted: notice := text;
}

// rule: every copy lent is held on some card.
invariant sum(Shelf.tools.lent) == sum(Cards.cards.holding);

flow borrow(card: id, tool: id) atomic { Cards.borrow(card); Shelf.lend(tool); }
flow bring_back(card: id, tool: id) atomic { Cards.give_back(card); Shelf.take_back(tool); }

view on_loan() = where(t in Shelf.tools: t.lent > 0);

scenario a_saturday {
    Shelf.add(1, 1) => Added; Cards.issue(7) => Issued; Cards.issue(8) => Issued;
    borrow(7, 1) => Lent;
    borrow(8, 1) => NoneLeft;
    bring_back(8, 1) => HoldsNothing;
    bring_back(7, 1) => Returned;
    borrow(8, 1) => Lent;
    on_loan() => Value([Tool { id: 1, copies: 1, lent: 1 }]);
    Board.post("closed on Sunday") => Posted;
}

verify: 8 examples, 10 scenario steps and 13000 sampled checks passed

Examples first

Every example runs its contract once on the state and arguments it names, and compares the outcome and the state after. Eight here. An example that fails, fails at any seed and any sample count.

Then scenarios

Every scenario runs from the initial world through the flows and stops at the first step whose answer differs from the one written. Ten steps here.

Then sampled checks on units

For every contract, a thousand times (the last number on the command line): a state of its unit, arguments drawn inside their bounds, one call. The state is drawn in one of two ways, half the time each:

• field by field at random, kept only if it satisfies the unit’s invariant, because a state the unit could never be in proves nothing;
• by a random walk of the unit’s own contracts, eight to sixty-four calls from its initial state, which reaches states that only a history produces.

Ids come from a small pool, so calls meet present and absent keys. After every call the verifier checks the unit’s invariant and every ensures the case or the contract states, and fails the call if no case matched, if two deltas wrote the same cell, or if anything panicked, such as first on nothing. A table’s bound and a machine act inside the call: a delta that would take a table past its bound ends as Full, a move the machine forbids as WrongStatus. Both are failed outcomes, which change nothing.

Then sampled checks on worlds

For every flow, a thousand times: a world reached by a random walk of the flows, sixteen to ninety-six flow calls from the initial world, then one call with drawn arguments. (In a program without world rules, half of these worlds are put together from units drawn one by one.) After every flow the verifier checks the world rules, the flow’s ensures, and atomicity: an atomic flow that failed must leave the world exactly as it was. The walk’s own steps are checked too, and a rule broken on the way is reported as a reachable walk. Every view is evaluated a thousand times on walked worlds, and must not panic.

The number

13000 sampled checks is thirteen jobs of a thousand: seven contracts, five flows and one view. The five flows are the two declared ones and the three that the scenario’s direct calls create, Shelf.add, Cards.issue and Board.post. Examples and scenario steps are counted once each. Commutativity checks, when a unit asks for them, are counted apart (Order and commutativity).

Then reachability

Last, every outcome a contract’s cases can produce must have been produced at least once, by an example or a sampled call; an outcome nothing produced is a case nobody tested, and the verdict fails.

Only what a flow can touch

After a flow, the verifier re-checks only the world rules that mention a unit the flow can change, and a flow’s walk draws only from the flows of its component, the group of units that flows and world rules join together. vishy graph prints the components:

3 unit(s), 5 flow(s), 1 world invariant(s), 0 world-derived field(s): 2 component(s)
component 1: units Shelf, Cards | flows borrow, bring_back, Shelf.add, Cards.issue | 1 invariant(s)
component 2: units Board | flows Board.post | 0 invariant(s)
flow borrow: touches Shelf, Cards | re-checks 1 of 1 invariant(s), recomputes 0 of 0 derived | walks 4 of 5 flow(s)
flow bring_back: touches Shelf, Cards | re-checks 1 of 1 invariant(s), recomputes 0 of 0 derived | walks 4 of 5 flow(s)
flow Shelf.add: touches Shelf | re-checks 1 of 1 invariant(s), recomputes 0 of 0 derived | walks 4 of 5 flow(s)
flow Cards.issue: touches Cards | re-checks 1 of 1 invariant(s), recomputes 0 of 0 derived | walks 4 of 5 flow(s)
flow Board.post: touches Board | re-checks 0 of 1 invariant(s), recomputes 0 of 0 derived | walks 1 of 5 flow(s)
note: the largest component has 2 of 3 units; each component verifies independently.

Board.post touches no unit the rule mentions, so it re-checks none of it, and its walks are made of notices only. A flow costs what it can reach, not what the program holds.

A failure it finds

Delete Shelf.take_back(tool); from bring_back (the program is book/failures/verifier-forgot.vish). Every contract is still right; the flow is wrong:

verify FAILED: 3 failure(s):
[1] scenario a_saturday step 7 (bring_back): flow bring_back: world invariant 1 violated: after World { shelf: Shelf { tools: [Tool { id: 1, copies: 1, lent: 1 }] }, cards: Cards { cards: [Card { id: 7, holding: 0 }, Card { id: 8, holding: 0 }] }, board: Board { notice: "" },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (7, 1) out GaveBack
  world World { shelf: Shelf { tools: [Tool { id: 1, copies: 1, lent: 1 }] }, cards: Cards { cards: [Card { id: 7, holding: 0 }, Card { id: 8, holding: 0 }] }, board: Board { notice: "" },  __now: 0, __ids: 0, __seed: 0, __caller: 0 }
[2] reachable walk, flow bring_back: flow bring_back: world invariant 1 violated: after World { shelf: Shelf { tools: [Tool { id: 10, copies: 6, lent: 0 }, Tool { id: 4, copies: 3, lent: 1 }, Tool { id: 12, copies: 4, lent: 0 }, Tool { id: 14, copies: 3, lent: 1 }] }, cards: Cards { cards: [Card { id: 10, holding: 1 }, Card { id: 14, holding: 0 }, Card { id: 13, holding: 0 }] }, board: Board { notice: "" },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (14, 13) out GaveBack
[3] flow bring_back: flow bring_back: world invariant 1 violated: after World { shelf: Shelf { tools: [Tool { id: 15, copies: 5, lent: 0 }, Tool { id: 2, copies: 8, lent: 0 }, Tool { id: 0, copies: 8, lent: 1 }, Tool { id: 6, copies: 4, lent: 0 }, Tool { id: 1, copies: 6, lent: 0 }, Tool { id: 3, copies: 5, lent: 0 }, Tool { id: 10, copies: 5, lent: 1 }] }, cards: Cards { cards: [Card { id: 6, holding: 0 }, Card { id: 10, holding: 0 }, Card { id: 1, holding: 1 }, Card { id: 2, holding: 0 }, Card { id: 3, holding: 0 }] }, board: Board { notice: "" },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (10, 0) out GaveBack
  (world World { shelf: Shelf { tools: [Tool { id: 15, copies: 5, lent: 0 }, Tool { id: 2, copies: 8, lent: 0 }, Tool { id: 0, copies: 8, lent: 1 }, Tool { id: 6, copies: 4, lent: 0 }, Tool { id: 1, copies: 6, lent: 0 }, Tool { id: 3, copies: 5, lent: 0 }, Tool { id: 10, copies: 5, lent: 1 }] }, cards: Cards { cards: [Card { id: 6, holding: 0 }, Card { id: 10, holding: 1 }, Card { id: 1, holding: 1 }, Card { id: 2, holding: 0 }, Card { id: 3, holding: 0 }] }, board: Board { notice: "" },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (10, 0))

One defect, found three ways: by the scenario’s seventh step, by a walk, and by the flow’s own sampled check. Each report names the flow, the world rule by its number in the source, the world after the call and the arguments. A failure that names a flow goes to the interface owner.

How much each layer catches

Flip one comparison in Cards.borrow, >= 3 to > 3 (the program is book/failures/verifier-flipped.vish):

verify FAILED: 4 failure(s):
[1] Cards.borrow example 2: Cards.borrow: invariant violated after case 2: state Cards { cards: [Card { id: 7, holding: 4 }] } args (7,)
[2] sampled check failed: Cards.borrow: Cards.borrow: invariant violated after case 2: state Cards { cards: [Card { id: 2, holding: 3 }, Card { id: 3, holding: 0 }, Card { id: 5, holding: 2 }, Card { id: 6, holding: 3 }, Card { id: 7, holding: 2 }, Card { id: 10, holding: 3 }, Card { id: 11, holding: 4 }, Card { id: 12, holding: 3 }, Card { id: 14, holding: 3 }] } args (11,)
  (state Cards { cards: [Card { id: 2, holding: 3 }, Card { id: 3, holding: 0 }, Card { id: 5, holding: 2 }, Card { id: 6, holding: 3 }, Card { id: 7, holding: 2 }, Card { id: 10, holding: 3 }, Card { id: 11, holding: 3 }, Card { id: 12, holding: 3 }, Card { id: 14, holding: 3 }] } args (11,))
[3] flow borrow: Cards.borrow: invariant violated after case 2: state Cards { cards: [Card { id: 6, holding: 0 }, Card { id: 14, holding: 4 }] } args (14,)
  (world World { shelf: Shelf { tools: [Tool { id: 6, copies: 8, lent: 3 }, Tool { id: 14, copies: 4, lent: 0 }, Tool { id: 15, copies: 9, lent: 0 }] }, cards: Cards { cards: [Card { id: 6, holding: 0 }, Card { id: 14, holding: 3 }] }, board: Board { notice: "" },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (14, 6))
[4] Cards.borrow: outcome `AtLimit` is never produced by an example or a sampled call (1000 sampled calls): an unreachable case, or a state the sampler does not draw; add an example that produces it

Four reports. The first is an example, the interface author’s { cards: [Card { id: 7, holding: 3 }] } (7) => AtLimit;, and it would fail at any sample count. Drop the guard altogether instead, and the program never runs: the stub declares fail AtLimit, and the checker refuses a body in which no case produces it (the program is book/refusals/verifier-dropped-guard.vish, the stub and the part assembled):

book/refusals/verifier-dropped-guard.vish:18:5: error: `Cards.borrow` declares `fail AtLimit` and no case produces it; a case must produce each declared outcome
      contract borrow(card: id) {
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^

A mutation study measured this on a larger program, the issue tracker of Where the tests went: twelve bugs of the kind writers make, planted by hand in its contract bodies, each verified at 300 and at 3,000 iterations on one seed (experiments/research/mutation-study.md):

Ten of twelve died whatever the sample count, and every example that killed one was the interface author’s, written because every declared failure needs one. An earlier run against a number pool, whose interface had few examples, killed nine of twelve; the three survivors were rules nobody had written down. The power is in the specification, examples per declared outcome and outcomes declared, and the sample count matters at the margin: one bug in twelve. It is one study, one seed, twelve bugs chosen by hand; the full matrix across seeds and sizes has not been run.

Try

In book/failures/verifier-flipped.vish, delete the AtLimit example. Three reports remain, two sampled calls and the unproduced AtLimit: the rule holding <= 3 still catches the flipped comparison, now only through sampling. Then delete that invariant too. vishy verify passes, at a thousand and at three thousand, with the bug in plain sight. The samples found it only while a rule said what to look for. The next chapter is about what nothing says.