Contract anti-patterns

Mistakes inside one contract or one row. Seven items, each with a program the guide’s check runs.

Unbounded quantity

Problem

A quantity declared int can be any integer, so every rule about it (never negative, never more than the shelf holds) is a guard that some contract must write, and every writer of every contract that touches it must remember to write. Miss one and the bad value reaches the state; the verifier finds it only if a sample happens to draw it before the run ends. In the experiments that shaped the language, the one bug found late was a negative quantity that reached a stock level through an unbounded field. A bound, int(1, 999), makes the bad value unwritable in an example, undrawable by the sampler, and refused at the door with a 400 that names the parameter, before any contract runs.

Example

row Level { id: id, on_hand: int }
unit Stock {
    state levels: Level[8];
    invariant all(l in levels: l.on_hand >= 0);
    contract receive(sku: id, qty: int) {
        case !(sku in levels) => Received: levels += [Level { id: sku, on_hand: qty }];
        else => Received: levels[sku].on_hand += qty;
    }
    contract ship(sku: id, qty: int) {
        case levels[sku].on_hand < qty => fail Short;
        else => Shipped: levels[sku].on_hand -= qty;
    }
}
scenario a_day { Stock.receive(1, 10) => Received; Stock.ship(1, 4) => Shipped; Stock.ship(1, 7) => Short; }

qty is a plain int. The invariant says a level is never negative, and nothing keeps a negative quantity out of receive. The verifier draws one:

verify FAILED: 2 failure(s):
[1] sampled check failed: Stock.receive: Stock.receive: invariant violated after case 1: state Stock { levels: [Level { id: 2, on_hand: 14 }, Level { id: 3, on_hand: 1 }, Level { id: 4, on_hand: 11 }, Level { id: 6, on_hand: -15 }] } args (6, -15)
  (state Stock { levels: [Level { id: 2, on_hand: 14 }, Level { id: 3, on_hand: 1 }, Level { id: 4, on_hand: 11 }] } args (6, -15))
[2] flow Stock.receive: Stock.receive: invariant violated after case 1: state Stock { levels: [Level { id: 1, on_hand: 3 }, Level { id: 15, on_hand: -49 }] } args (15, -49)
  (world World { stock: Stock { levels: [Level { id: 1, on_hand: 3 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (15, -49))

The first failure is a sampled call of receive with a quantity of minus fifteen from a state of three levels; the second is the same defect reached through the one-call flow. This is the good case: the invariant was written, so the verifier had a rule to break. Without the invariant, the negative level would have been stored and served.

Refactoring

row Level { id: id, on_hand: int(0, 9999) }
unit Stock {
    state levels: Level[8];
    invariant all(l in levels: l.on_hand >= 0);
    contract receive(sku: id, qty: int(1, 999)) {
        case !(sku in levels) => Received: levels += [Level { id: sku, on_hand: qty }];
        else => Received: levels[sku].on_hand += qty;
    }
    contract ship(sku: id, qty: int(1, 999)) {
        case levels[sku].on_hand < qty => fail Short;
        else => Shipped: levels[sku].on_hand -= qty;
    }
}
scenario a_day { Stock.receive(1, 10) => Received; Stock.ship(1, 4) => Shipped; Stock.ship(1, 7) => Short; }

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

Both quantities carry the bound, and the row’s field carries its own, so the sampler never draws what the bound forbids and the invariant has nothing to find. The guard the anti-pattern would have needed in every contract is written once, in the type.

Additional remarks

The compiler accepts int and string without a bound, and this guide asks you never to write one in a program that matters. A bound is also a decision: when the requirement does not give the number, choose one and record it as an assumption on the declaration, which the appendix on authoring an interface says how to do.

A rule left only in prose

Problem

A comment states a rule; nothing in the program does. “The screen checks it before calling”, “amount checks are another unit’s job”: in two experiments a sentence like that in a contract’s comment became a guard that a writer invented, differently in each unit, and in the third it became nothing at all. The verifier confirms a program against the rules it can read, and a comment is not one of them, so a program that breaks a prose rule passes.

Example

row Booking { id: id, room: id, people: int }
unit Bookings {
    state bookings: Booking[8];
    // people is at least 1; the screen checks it before calling.
    contract book(booking: id, room: id, people: int) {
        else => Booked: bookings += [Booking { id: booking, room, people }];
    }
}
scenario zero_people { Bookings.book(1, 1, 0) => Booked; }

The comment says a booking has at least one person. The scenario books a room for nobody, and expects success:

scenario zero_people
  Bookings.book(1, 1, 0) => Booked
  Bookings = Bookings { bookings: [Booking { id: 1, room: 1, people: 0 }] }
1 step(s), all as expected

verify: 0 examples, 1 scenario steps and 2000 sampled checks passed

Nothing catches it. The verifier has no rule to check, the scenario states the wrong behaviour and passes, and a served door, which enforces only the declared bounds, would take a request for zero people the same way. This is the first of the verifier’s blind spots: a rule nobody wrote is implemented faithfully.

Refactoring

row Booking { id: id, room: id, people: int(1, 200) }
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id, people: int(1, 200)) {
        else => Booked: bookings += [Booking { id: booking, room, people }];
    }
}
scenario one_person { Bookings.book(1, 1, 1) => Booked; }

verify: 0 examples, 1 scenario steps and 2000 sampled checks passed

The rule is now the type, and the comment is gone because there is nothing left to say in prose. The old scenario step is refused by the checker before anything runs (the program with that step is book/refusals/anti-prose-zero.vish):

book/refusals/anti-prose-zero.vish:8:44: error: scenario `zero_people` step 1: argument `people` is outside its type
  scenario zero_people { Bookings.book(1, 1, 0) => Booked; }
                                             ^

Additional remarks

A rule that is not a bound is an outcome (fail BadAmount, with an example that produces it) or an invariant. The test for whether a rule is still prose: delete the comment and ask what the checker or the verifier would now miss. If the answer is nothing, the rule was already in the program; if the answer is the rule, it was only in the comment.

A declared failure without an example

Problem

An interface declares that a contract can fail TooBig and gives no example of when. The writer who fills the body has the outcome’s name and a sentence, and writes a guard from the sentence, or none at all. A missing guard fails locally and at once when there is an example, as a failed example that names the contract; without one it fails when a deep sample happens to reach the state, or never. The example is the rule for when the failure occurs, and the interface check refuses a declared failure that has none.

Example

row Room { id: id, seats: int(1, 200) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id, seats: int(1, 200)) {
        // Added when the room is new; TooBig when it would have more seats than the building allows.
        outcomes Added, fail TooBig;
        examples { {} (1, 4) => Added { rooms: [Room { id: 1, seats: 4 }] }; }
    }
}
flow add_room(room: id, seats: int(1, 200)) atomic { Rooms.add(room, seats); }

Checked as an interface (vishy check --interface), which is how an interface is checked before writers start:

book/refusals/interface/anti-no-example.vish:6:30: error: `Rooms.add` declares `fail TooBig` without an acceptance example that produces it; write the example (it is the rule for when the failure occurs)
          outcomes Added, fail TooBig;
                               ^^^^^^

Refactoring

row Room { id: id, seats: int(1, 200) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id, seats: int(1, 200)) {
        // Added when the room is new; TooBig when it would have more than 120 seats, the building's largest hall.
        outcomes Added, fail TooBig;
        examples {
            {} (1, 4) => Added { rooms: [Room { id: 1, seats: 4 }] };
            {} (1, 121) => TooBig;
        }
    }
}
flow add_room(room: id, seats: int(1, 200)) atomic { Rooms.add(room, seats); }

ok: 1 row(s), 0 event(s), 0 fn(s), 1 unit(s), 1 contract(s), 1 flow(s)

The example says which seat count is too big, so the comment can name the number and the writer’s guard is checked against it on the first run.

Additional remarks

Only the interface check refuses this; vishy check on a whole program accepts a stub without an example, because a program may carry stubs that a part will fill. Run the interface check on the interface, always. A failure that a rule makes impossible (a balanced ledger is never Unbalanced) is not declared at all; the flow says in a comment why the outcome is unreachable, which the design page returns to.

Two examples that disagree

Problem

Two examples of one contract start from the same state with the same arguments and expect different outcomes. No body can satisfy both, so the writer’s part fails whichever way it is written, and the repair rounds spend themselves on a contract that cannot be fixed. The disagreement is a sign about the interface, not the body: the contract is being asked to decide on a fact it does not hold.

Example

row Booking { id: id, holder: id }
unit Bookings {
    state bookings: Booking[8];
    fixture One = { bookings: [Booking { id: 1, holder: 100 }] };
    contract cancel(booking: id) {
        case !(booking in bookings) => fail Unknown;
        case bookings[booking].holder != 100 => fail NotHolder;
        else => Cancelled: bookings -= [booking];
        examples {
            One (1) => Cancelled { bookings: [] };
            One (1) => NotHolder;
        }
    }
}

cancel is told only which booking. One example expects the holder to succeed, the other expects a stranger to be refused, and nothing in the state or the arguments tells the two calls apart. The body here is one a writer might try, comparing the holder with the fixture’s; the verifier fails the second example:

verify FAILED: 1 failure(s):
[1] Bookings.cancel example 2: expected NotHolder, got Cancelled (state before Bookings { bookings: [Booking { id: 1, holder: 100 }] } after Bookings { bookings: [] })

The interface check does not catch this: it types the examples and accepts both. The verifier catches it as soon as a body exists, on whichever example the body does not satisfy.

Refactoring

row Booking { id: id, holder: id }
unit Bookings {
    state bookings: Booking[8];
    fixture One = { bookings: [Booking { id: 1, holder: 100 }] };
    contract cancel(booking: id, holder: id) {
        case !(booking in bookings) => fail Unknown;
        case bookings[booking].holder != holder => fail NotHolder;
        else => Cancelled: bookings -= [booking];
        examples {
            One (1, 100) => Cancelled { bookings: [] };
            One (1, 101) => NotHolder;
            One (9, 100) => Unknown;
        }
    }
}

verify: 3 examples, 0 scenario steps and 1000 sampled checks passed

The missing fact, who is asking, becomes a parameter; the flow that calls cancel passes caller in. The two examples now start from different arguments and agree with each other, and a third one shows the absent booking.

Additional remarks

Two examples from the same state and arguments that expect the same outcome are merely redundant. The rule is about the outcome: when the expected outcomes differ, find the fact that should tell the calls apart and carry it in.

A carried value without a property

Problem

A contract that carries a value, Count(n) or Price(p), is checked against the examples that state the expected number and against nothing else: deltas are held to the invariant in every sampled state, but a carried value has no rule to be held to. A wrong formula that happens to agree with the examples passes. This is the third of the verifier’s blind spots, and it is closed by the interface author, with a contract-level ensures that states the property; then every sampled call checks it, whatever the writer wrote.

Example

row Room { id: id, closed: bool }
unit Rooms {
    state rooms: Room[8];
    fixture Two = { rooms: [Room { id: 1, closed: false }, Room { id: 2, closed: false }] };
    contract close(room: id) {
        else => Closed: rooms[room].closed := true;
        examples { Two (1) => Closed { rooms: [Room { id: 1, closed: true }, Room { id: 2, closed: false }] }; }
    }
    contract open_count() -> int {
        else => Count(len(rooms));
        examples { {} () => Count(0); Two () => Count(2); }
    }
}

open_count returns the number of rooms, closed ones included. Both examples are on states where no room is closed, so both pass, and the verifier has no other rule to try:

verify: 3 examples, 0 scenario steps and 2000 sampled checks passed

Nothing catches it. Adding the property to the same wrong body (the program is book/failures/anti-no-ensures-caught.vish) gives the verifier its rule, and the first sampled state with a closed room breaks it:

verify FAILED: 1 failure(s):
[1] sampled check failed: Rooms.open_count: Rooms.open_count: ensures of case 1 violated: state Rooms { rooms: [Room { id: 1, closed: true }, Room { id: 3, closed: true }, Room { id: 4, closed: false }, Room { id: 5, closed: true }, Room { id: 7, closed: false }, Room { id: 8, closed: true }] } args () out Count(6)
  (state Rooms { rooms: [Room { id: 1, closed: true }, Room { id: 3, closed: true }, Room { id: 4, closed: false }, Room { id: 5, closed: true }, Room { id: 7, closed: false }, Room { id: 8, closed: true }] } args ())

Six rooms, four of them closed, and the contract answered six.

Refactoring

row Room { id: id, closed: bool }
unit Rooms {
    state rooms: Room[8];
    fixture Two = { rooms: [Room { id: 1, closed: false }, Room { id: 2, closed: false }] };
    contract close(room: id) {
        else => Closed: rooms[room].closed := true;
        examples { Two (1) => Closed { rooms: [Room { id: 1, closed: true }, Room { id: 2, closed: false }] }; }
    }
    contract open_count() -> int {
        ensures result == count(r in rooms: !r.closed);
        else => Count(count(r in rooms: !r.closed));
        examples { {} () => Count(0); Two () => Count(2); }
    }
}

verify: 3 examples, 0 scenario steps and 2000 sampled checks passed

The ensures line belongs in the interface, above the stub, so that it survives the merge with the writer’s part and holds whatever body arrives. When there is no formula to state, state the bounds and relations that must hold: result >= 0, result <= len(old(rooms)).

Additional remarks

A carried value whose examples cover every state it can see (a contract on a unit with a single scalar, say) is checked by them, and the property adds nothing. The rule is for values computed over tables, where the exampled states are a few of many.

A derived amount whose domain is not in the row’s type

Problem

A world-derived column takes its value when a flow commits, from other units’ state. Inside a unit’s own sampled check no flow runs, so the sampler draws the column freely, and the only thing it respects is the field’s declared type. A field declared int that the world keeps at zero or more is drawn negative, and a correct contract that relies on the world’s rule fails on a state the world can never reach. The cost is a false failure that sends a writer to repair a body that was right, and it was found by a sample at three thousand iterations on a program that had passed at one thousand.

Example

row Payment { id: id, captured: int(0, 9999), refunded: int }
row Refund { id: id, payment: id, amount: int(1, 9999) }
unit Payments {
    state payments: Payment[8];
    fixture One = { payments: [Payment { id: 1, captured: 5000, refunded: 0 }] };
    contract capture(payment: id, amount: int(1, 9999)) {
        else => Captured: payments += [Payment { id: payment, captured: amount, refunded: 0 }];
        examples { {} (1, 5000) => Captured One; }
    }
    contract remaining(payment: id) -> int {
        ensures result <= payments[payment].captured;
        case !(payment in payments) => fail Unknown;
        else => Remaining(payments[payment].captured - payments[payment].refunded);
        examples { One (1) => Remaining(5000); One (9) => Unknown; }
    }
}
unit Refunds {
    state refunds: Refund[8];
    contract refund(refund: id, payment: id, amount: int(1, 9999)) {
        else => Refunded: refunds += [Refund { id: refund, payment, amount }];
    }
}
derived Payments.payments.refunded = for p => sum(where(r in Refunds.refunds: r.payment == p.id).amount);
invariant all(p in Payments.payments: p.refunded <= p.captured);
flow refund(refund: id, payment: id, amount: int(1, 9999)) atomic { let left = Payments.remaining(payment); Refunds.refund(refund, payment, amount); }

refunded is derived from the refunds and, in the world, never exceeds captured or falls below zero: the flow that refunds asks remaining first, and the world invariant says so. But the row declares it int. In the unit’s check, the sampler draws a refund of minus fifty:

verify FAILED: 1 failure(s):
[1] sampled check failed: Payments.remaining: Payments.remaining: ensures of case 2 violated: state Payments { payments: [Payment { id: 1, captured: 3046, refunded: -50 }, Payment { id: 4, captured: 1611, refunded: 25 }, Payment { id: 6, captured: 2330, refunded: 8 }, Payment { id: 7, captured: 8904, refunded: 39 }, Payment { id: 8, captured: 7643, refunded: 22 }] } args (1,) out Remaining(3096)
  (state Payments { payments: [Payment { id: 1, captured: 3046, refunded: -50 }, Payment { id: 4, captured: 1611, refunded: 25 }, Payment { id: 6, captured: 2330, refunded: 8 }, Payment { id: 7, captured: 8904, refunded: 39 }, Payment { id: 8, captured: 7643, refunded: 22 }] } args (1,))

The property result <= captured is true in every real state and false in this drawn one, and the contract is blamed.

Refactoring

row Payment { id: id, captured: int(0, 9999), refunded: int(0, 9999) }
row Refund { id: id, payment: id, amount: int(1, 9999) }
unit Payments {
    state payments: Payment[8];
    fixture One = { payments: [Payment { id: 1, captured: 5000, refunded: 0 }] };
    contract capture(payment: id, amount: int(1, 9999)) {
        else => Captured: payments += [Payment { id: payment, captured: amount, refunded: 0 }];
        examples { {} (1, 5000) => Captured One; }
    }
    contract remaining(payment: id) -> int {
        ensures result <= payments[payment].captured;
        case !(payment in payments) => fail Unknown;
        else => Remaining(payments[payment].captured - payments[payment].refunded);
        examples { One (1) => Remaining(5000); One (9) => Unknown; }
    }
}
unit Refunds {
    state refunds: Refund[8];
    contract refund(refund: id, payment: id, amount: int(1, 9999)) {
        else => Refunded: refunds += [Refund { id: refund, payment, amount }];
    }
}
derived Payments.payments.refunded = for p => sum(where(r in Refunds.refunds: r.payment == p.id).amount);
invariant all(p in Payments.payments: p.refunded <= p.captured);
flow refund(refund: id, payment: id, amount: int(1, 9999)) atomic { let left = Payments.remaining(payment); Refunds.refund(refund, payment, amount); }

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

One change: refunded: int(0, 9999). The sampler now draws inside the domain, and the property holds on every drawn state.

Additional remarks

The relation between two fields (refunded <= captured) cannot go into the type, and it cannot go into the unit’s invariant either, because a unit invariant may not name a world-derived field; the checker refuses one that tries (the program is book/refusals/anti-derived-invariant.vish):

book/refusals/anti-derived-invariant.vish:5:15: error: this invariant of `Payments` mentions a world-derived field (refunded), which only takes its value when a flow commits; state it as a top-level `invariant` over `Payments.field`, checked after every flow
      invariant all(p in payments: p.refunded <= p.captured);
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It is a world invariant, as in the programs above, and the unit’s own check does not see it. So a contract’s property inside the unit must hold for every value the type allows, not only for the values the world produces; when the property needs the relation, state it on the flow’s ensures instead, where the world is in scope.

A money total in a fold

Problem

Until 30 September 2026 a total of a money column written as a fold that starts at a literal, acc = 0, or as a sum over the column, was refused in a view or a world invariant: the literal was typed as int when nothing around it said money, and sum took only integer columns. Writers worked around it with an int total, which lost the scale, or with a derived field whose declared type gave the fold its context.

Example

This is the program that was refused. The compiler now accepts it: a fold that starts at a literal takes its type from what its body combines it with, and sum keeps a money or duration column’s type (roadmap item 8). What it prints today:

row Payment { id: id, captured: money(2) }
unit Payments {
    state payments: Payment[8];
    contract capture(payment: id, amount: money(2)) {
        case amount <= 0 => fail BadAmount;
        else => Captured: payments += [Payment { id: payment, captured: amount }];
    }
}
view total() = fold(p in Payments.payments, acc = 0: acc + p.captured);

ok: 1 row(s), 0 event(s), 0 fn(s), 1 unit(s), 1 contract(s), 0 flow(s)

And the sum form (the program is book/programs/anti-money-sum.vish):

ok: 1 row(s), 0 event(s), 0 fn(s), 1 unit(s), 1 contract(s), 0 flow(s)

Refactoring

The shape that was the workaround is still the better shape, for a reason that has nothing to do with the old refusal:

row Payment { id: id, captured: money(2) }
unit Payments {
    state payments: Payment[8];
    derived total: money(2) = fold(p in payments, acc = 0: acc + p.captured);
    contract capture(payment: id, amount: money(2)) {
        case amount <= 0 => fail BadAmount;
        else => Captured: payments += [Payment { id: payment, captured: amount }];
    }
    contract captured_total() -> money(2) {
        else => Total(total);
        examples { {} () => Total(0); }
    }
}
view total() = Payments.total;
scenario two_payments { Payments.capture(1, 1000) => Captured; Payments.capture(2, 250) => Captured; Payments.captured_total() => Total(1250); total() => Value(1250); }

scenario two_payments
  Payments.capture(1, 1000) => Captured
  Payments.capture(2, 250) => Captured
  Payments.captured_total() => Total(1250)
  total() => Value(1250)
  Payments = Payments { payments: [Payment { id: 1, captured: 1000 }, Payment { id: 2, captured: 250 }], total: 1250 }
4 step(s), all as expected

verify: 1 examples, 4 scenario steps and 5000 sampled checks passed

A derived field inside the unit names the total’s type once, money(2), keeps the total in step with the table on every change without a contract doing the bookkeeping, and lets the view read a maintained value instead of folding the table on every call. The fold in the view is correct now; the derived field is what a reader of the interface expects to find.

Additional remarks

The anti-pattern that remains is the one the old refusal was protecting against: an int total for a money column, typed by hand, which loses the scale and lets the total be added to a count. Keep money as money(2) from the column to the view, and let the compiler carry the type.