Rules, and the state that breaks them

The last chapter’s counter had no rules, so the verifier had nothing to look for. This chapter adds the two ways a program says what must be true: a failure outcome, which is a rule about one call, and an invariant, which is a rule about the state at every moment. Then it deletes one and watches the verifier find the state that the missing rule would have prevented.

unit Account {
    state balance: money(2) = 0;
    contract deposit(amount: money(2)) {
        case amount <= 0 => fail BadAmount;
        else => Deposited: balance += amount;
    }
    contract withdraw(amount: money(2)) {
        case amount <= 0 => fail BadAmount;
        case amount > balance => fail Insufficient;
        else => Withdrawn: balance -= amount;
    }
    invariant balance >= 0;
}
scenario a_day {
    Account.deposit(10000) => Deposited;
    Account.withdraw(2500) => Withdrawn;
    Account.withdraw(9000) => Insufficient;
    Account.withdraw(0) => BadAmount;
}

Failure outcomes

withdraw has three cases. The first two are failures: fail BadAmount when the amount is not positive, fail Insufficient when it is more than the balance. A failure is an outcome like any other, with a name a caller can switch on, and one property that makes it different: a failing case changes nothing. It has no deltas and may not have any. So a contract’s failures are the rules about when it may be called, stated as answers rather than as errors.

Cases are tried in order and the first guard that holds decides, so the order is part of the rule: an amount of zero is BadAmount even when the balance is zero too, because that case comes first.

The invariant

invariant balance >= 0; is a rule the unit promises after every call to any of its contracts. It is not checked by the contracts; it is checked on them. A unit has one invariant, and several conditions are joined with &&.

Money

money(2) is an amount in minor units with two decimals: 10000 is a hundred units. Money adds to money of the same scale and multiplies by an integer, and the checker refuses to mix it with a plain int or with money of another scale. It is not a decimal type with rounding; it is an integer that knows what it counts.

Running it

scenario a_day
  Account.deposit(10000) => Deposited
  Account.withdraw(2500) => Withdrawn
  Account.withdraw(9000) => Insufficient
  Account.withdraw(0) => BadAmount
  Account = Account { balance: 7500 }
4 step(s), all as expected

verify: 0 examples, 4 scenario steps and 4000 sampled checks passed

Four scenario steps, and then four thousand sampled calls across the two contracts, from random states and from states reached by earlier calls, with a random amount each time, checking the invariant after every one. Nothing was found, because the two guards keep the balance from going below zero.

Deleting a rule

Remove the Insufficient case and its scenario step (the program is book/failures/account-noguard.vish). The checker still accepts the program; the scenario still passes. vishy verify does not:

verify FAILED: 2 failure(s):
[1] sampled check failed: Account.withdraw: Account.withdraw: invariant violated after case 2: state Account { balance: -18 } args (60,)
  (state Account { balance: 42 } args (60,))
[2] flow Account.withdraw: Account.withdraw: invariant violated after case 2: state Account { balance: -12 } args (25,)
  (world World { account: Account { balance: 13 },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (25,))

Read the first failure. The verifier started from a state with a balance of 42, called withdraw with 60, and the invariant failed after case 2 with a balance of minus 18. It shows the state before the call, the arguments, and the state after; anyone can reproduce it with the same seed. That is the whole method of the language, and it is the sentence to keep: say the rule, and let the verifier look for the state that breaks it.

The second failure is the same defect found a second way, through the one-call flow the scenario’s calls go through. Both name the contract, so the person or the model who owns that unit knows where to look.

What the verifier did not do

It did not prove that the balance can never be negative. It sampled a thousand states and a thousand arguments and found none that broke the rule in the correct program, and one in the broken one within the first few. A rule that only breaks in a state the sampler never draws is missed; the chapter on what the verifier cannot see says how deep the sampling goes and what stays outside it.

Try

Put the Insufficient case back and change the invariant to balance >= 100. The verifier fails on the very first sampled call, a deposit from the initial state: the balance starts at zero, which already breaks the new rule, and a failed case changes nothing, so the rule is still broken after it. A rule the program cannot keep from its first state is found before any guard is tested.