What the verifier cannot see
The verifier checks that a program’s bodies, examples, scenarios and rules agree with each other in every state it samples. That leaves four kinds of mistake it cannot see, by construction, whatever it samples. This chapter shows each one passing, then says what closes it and what does not. The list is the one in the repository’s docs/blind-spots.md, with a run for each.
A rule that is wrong or missing
Here is the lending program of the last chapter with another scenario in place of its own (the program is book/programs/verifier-anycard.vish):
scenario a_mixup {
Shelf.add(1, 1) => Added; Shelf.add(2, 1) => Added;
Cards.issue(7) => Issued; Cards.issue(8) => Issued;
borrow(7, 1) => Lent;
borrow(8, 2) => Lent;
bring_back(8, 1) => Returned;
on_loan() => Value([Tool { id: 2, copies: 1, lent: 1 }]);
}
scenario a_mixup
Shelf.add(1, 1) => Added
Shelf.add(2, 1) => Added
Cards.issue(7) => Issued
Cards.issue(8) => Issued
borrow(7, 1) => Lent
borrow(8, 2) => Lent
bring_back(8, 1) => Returned
on_loan() => Value([Tool { id: 2, copies: 1, lent: 1 }])
Shelf = Shelf { tools: [Tool { id: 1, copies: 1, lent: 0 }, Tool { id: 2, copies: 1, lent: 1 }] }
Cards = Cards { cards: [Card { id: 7, holding: 1 }, Card { id: 8, holding: 0 }] }
Board = Board { notice: "" }
8 step(s), all as expected
verify: 8 examples, 8 scenario steps and 12000 sampled checks passed
Card 8 borrowed the saw and brought back the drill that card 7 borrowed. Every rule the program states still holds: no tool has more copies lent than it owns, no card holds more than three, and the copies lent equal the tools held. The rule the library means, that a member brings back only what they borrowed, is written nowhere, so no example, scenario or sample can find it broken; the scenario above even asserts the wrong behaviour, and passes.
Nothing in the toolchain closes this. The interface author closes it by writing the rule, here a loan row per card and tool kept by the flows, and the reviewer closes it by reading the interface against the brief. In the mutation study’s earlier run, the three planted bugs that survived out of twelve were exactly this: rules nobody had written.
A rule can also be one you believe you wrote. A bound on a stored field is the range the sampler draws from, not a rule checked after a call:
row Card { id: id, holding: int(0, 3) }
unit Cards {
state cards: Card[16];
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;
}
}
scenario a_greedy_member {
Cards.issue(7) => Issued;
Cards.borrow(7) => Borrowed; Cards.borrow(7) => Borrowed; Cards.borrow(7) => Borrowed; Cards.borrow(7) => Borrowed;
}
scenario a_greedy_member
Cards.issue(7) => Issued
Cards.borrow(7) => Borrowed
Cards.borrow(7) => Borrowed
Cards.borrow(7) => Borrowed
Cards.borrow(7) => Borrowed
Cards = Cards { cards: [Card { id: 7, holding: 4 }] }
5 step(s), all as expected
verify: 0 examples, 5 scenario steps and 4000 sampled checks passed
The field is typed int(0, 3) and the card holds four. Only an invariant is checked after every call; add invariant all(c in cards: c.holding <= 3); and the fifth step fails.
Doing nothing is safe
Every check the sampler runs is a safety check: after the call, does the rule still hold? A contract that changes nothing breaks no rule. Here lend answers Lent and lends nothing (the program is book/failures/verifier-lazy.vish):
row Tool { id: id, copies: int(1, 9), lent: int(0, 9) }
unit Shelf {
state tools: Tool[16];
invariant all(t in tools: t.lent <= t.copies);
fixture Drill = { tools: [Tool { id: 1, copies: 2, lent: 1 }] };
contract lend(tool: id) {
case tools[tool].lent >= tools[tool].copies => fail NoneLeft;
else => Lent;
examples {
Drill (1) => Lent { tools: [Tool { id: 1, copies: 2, lent: 2 }] };
{ tools: [Tool { id: 1, copies: 2, lent: 2 }] } (1) => NoneLeft;
}
}
}
verify FAILED: 1 failure(s):
[1] Shelf.lend example 1: expected state Shelf { tools: [Tool { id: 1, copies: 2, lent: 2 }] }, got Shelf { tools: [Tool { id: 1, copies: 2, lent: 1 }] }
One failure, and it is the example’s. The thousand sampled calls found nothing, because the lazy body keeps the invariant perfectly. What closes this hole is the rule that examples say what changed: a success example states the state after the call, and a body that does not produce it fails, whatever the sample. The other half is reachability, from the last chapter: a success case whose guard is never true never produces its outcome, and the verdict says so. What does not close it is more sampling.
A carried value with no oracle
A carried value, Count(n) or Price(p), has nothing to be held to in a sampled state: the invariant speaks about the state, not the answer. It is checked where an example or a scenario step states the expected number, and on every sampled call only when the contract states a property of result with ensures. The Contract anti-patterns page shows a count that includes closed rooms passing its examples and two thousand sampled checks, then failing on the first sampled state with a closed room once the property is written. So ensures closes the hole for the property it states, and a scenario assertion closes it on the states the scenario visits. Neither closes it for a property nobody states.
Trusted code
Under vishy verify, an effect’s Rust body never runs. The verifier answers an effect call from the effect’s fixtures, and for any other arguments with a random value of its type:
row Card { id: id, fees: int(0, 9999) }
unit Cards {
state cards: Card[16];
contract issue(card: id) => Issued: cards += [Card { id: card, fees: 0 }];
contract charge(card: id, cents: int(0, 999)) => Charged: cards[card].fees += cents;
}
// the late fee: ten cents a day after the first fourteen days
effect late_fee(days: int(0, 60)) -> int(0, 999)
impl { days * 10 }
fixtures { (20) => 60; (10) => 0; }
flow check_in(card: id, days: int(0, 60)) atomic { let fee = late_fee(days); Cards.charge(card, fee); }
scenario a_late_drill { Cards.issue(7) => Issued; check_in(7, 20) => Charged; check_in(7, 10) => Charged; }
scenario a_late_drill
Cards.issue(7) => Issued
check_in(7, 20) => Charged
check_in(7, 10) => Charged
Cards = Cards { cards: [Card { id: 7, fees: 60 }] }
3 step(s), all as expected
verify: 0 examples, 3 scenario steps and 4000 sampled checks passed
The fixtures say twenty days cost 60 and ten days cost nothing, which is the rule in the comment. The body says days * 10, which is 200 for twenty days; the service runs the body. Nothing compares the two. The random answers close part of the hole: the program’s rules must hold for any answer the effect gives. The body itself is ordinary Rust, tested the ordinary way. The same holds for the runtime: the generated store, door and JSON are compiler output, held by the repository’s regression scripts, not by the verifier, and a served flow does not re-check the world rules on each request.
What more samples buy
More samples reach deeper states: the one planted bug in the mutation study that depended on sampling was found at 3,000 iterations and missed at 300, which is why the handbook asks for three seeds at 3,000 before anything is served. More samples never buy a rule nobody wrote, a value nobody stated, a state larger than a table’s declared size, or a line of an effect’s Rust. And the verdict is never a proof: it is a thousand tries per contract, flow and view, that found nothing.
What to write, therefore
- An example for every declared outcome, and for every success the state after it.
- A scenario for every rule the product promises, reaching each failure through a flow.
- An
ensureswherever a contract’s answer, or a function’s result, matters. - An invariant for every bound you mean as a rule.
Try
In book/failures/verifier-lazy.vish, shorten the first example to Drill (1) => Lent;. The lazy body passes: an example with no after-state means nothing changed, and nothing did. Now give lend its real delta, else => Lent: tools[tool].lent += 1;, and the same example fails: it gives no after-state, which means unchanged, but the state changed. An example without an after-state is a claim, and the verifier holds you to it.