Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Design anti-patterns

Mistakes in how units, flows and views are cut: a fact that lives in the wrong place, a rule kept by nobody, a name that belongs to someone else. Eight items, each with a program the guide’s check runs.

A verdict carried as a value

Problem

One unit answers a question with a boolean, the flow carries the boolean into another unit, and that unit fails when the flag is false. The rule now lives in three places: the unit that computed the flag, the flow that passed it, and the guard that reads it. Any flow can pass true. Inside the second unit’s own check, the sampler draws the flag freely, since it is only a bool, so the unit is verified against a fact it never held. A bool parameter that stands for another unit’s answer is a cross-unit read in disguise; so is comparing two ids that come from different units. The unit that knows decides and fails; the flow calls it first; the next contract takes no flag.

Example

row Room { id: id, seats: int(1, 200) }
row Booking { id: id, room: id, people: int(1, 200) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id, seats: int(1, 200)) {
        else => Added: rooms += [Room { id: room, seats }];
    }
    contract fits(room: id, people: int(1, 200)) -> bool {
        case !(room in rooms) => fail Unknown;
        else => Fits(rooms[room].seats >= people);
    }
}
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id, people: int(1, 200), fits: bool) {
        case !fits => fail TooSmall;
        else => Booked: bookings += [Booking { id: booking, room, people }];
        examples { {} (1, 1, 3, true) => Booked { bookings: [Booking { id: 1, room: 1, people: 3 }] }; {} (1, 1, 3, false) => TooSmall; }
    }
}
invariant all(b in Bookings.bookings: any(r in Rooms.rooms: r.id == b.room && b.people <= r.seats));
flow book(booking: id, room: id, people: int(1, 200)) atomic { let ok = Rooms.fits(room, people); Bookings.book(booking, room, people, ok); }
scenario a_day { Rooms.add(1, 4) => Added; book(1, 1, 3) => Booked; book(2, 1, 5) => TooSmall; }

verify: 2 examples, 3 scenario steps and 5000 sampled checks passed

Nothing catches it: the one flow passes the flag correctly, the world invariant holds, and the verifier has no way to know that fits was meant to be Rooms’ answer rather than a caller’s opinion. The cost arrives with the second flow that calls book, or with the writer who reads fits: bool and guesses what it means.

Refactoring

row Room { id: id, seats: int(1, 200) }
row Booking { id: id, room: id, people: int(1, 200) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id, seats: int(1, 200)) {
        else => Added: rooms += [Room { id: room, seats }];
    }
    contract fits(room: id, people: int(1, 200)) {
        case !(room in rooms) => fail Unknown;
        case rooms[room].seats < people => fail TooSmall;
        else => Fits;
        examples { { rooms: [Room { id: 1, seats: 4 }] } (1, 4) => Fits; { rooms: [Room { id: 1, seats: 4 }] } (1, 5) => TooSmall; {} (9, 1) => Unknown; }
    }
}
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id, people: int(1, 200)) {
        else => Booked: bookings += [Booking { id: booking, room, people }];
        examples { {} (1, 1, 3) => Booked { bookings: [Booking { id: 1, room: 1, people: 3 }] }; }
    }
}
invariant all(b in Bookings.bookings: any(r in Rooms.rooms: r.id == b.room && b.people <= r.seats));
// the room decides whether the booking fits, before it is made.
flow book(booking: id, room: id, people: int(1, 200)) atomic { Rooms.fits(room, people); Bookings.book(booking, room, people); }
scenario a_day { Rooms.add(1, 4) => Added; book(1, 1, 3) => Booked; book(2, 1, 5) => TooSmall; }

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

fits fails with TooSmall itself, the flow calls it before book, and book takes no flag. A failure in the first call aborts the transaction, so the booking is never made, and there is no second place for the rule to be wrong.

Additional remarks

A carried value that is a fact, not a verdict (a room’s seat count, an order’s location), is the right thing to carry, and the next item’s refactoring does exactly that. The test is whether the value is something the second unit needs to know or something it has been told to conclude.

A query flow where a view belongs

Problem

A read is written as a flow that calls a contract that computes a value. That costs a contract body for a writer to write, a transaction at the door for every read, and a place for the rule of who sees what to hide inside a body instead of standing in the declaration. A read is a view: an expression over the world, typed like a rule, served without a transaction, and checked by the scenarios that assert on it.

Example

row Room { id: id, closed: bool }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id) {
        else => Added: rooms += [Room { id: room, closed: false }];
    }
    contract close(room: id) {
        else => Closed: rooms[room].closed := true;
    }
    contract open_count() -> int {
        else => Count(count(r in rooms: !r.closed));
        examples { {} () => Count(0); }
    }
}
flow open_rooms() atomic { Rooms.open_count(); }
scenario counting { Rooms.add(1) => Added; Rooms.add(2) => Added; Rooms.close(2) => Closed; open_rooms() => Count(1); }

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

Nothing catches it; a flow that only reads is a legal flow. The cost is in the shape: open_count is a contract, so it waits for a writer, and its answer is a carried value, which the earlier page showed is checked only where an example states it.

Refactoring

row Room { id: id, closed: bool }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id) {
        else => Added: rooms += [Room { id: room, closed: false }];
    }
    contract close(room: id) {
        else => Closed: rooms[room].closed := true;
    }
}
view open_rooms() = count(r in Rooms.rooms: !r.closed);
scenario counting { Rooms.add(1) => Added; Rooms.add(2) => Added; Rooms.close(2) => Closed; open_rooms() => Value(1); }

scenario counting
  Rooms.add(1) => Added
  Rooms.add(2) => Added
  Rooms.close(2) => Closed
  open_rooms() => Value(1)
  Rooms = Rooms { rooms: [Room { id: 1, closed: false }, Room { id: 2, closed: true }] }
4 step(s), all as expected

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

The count is a view, one line, with no body to write. The scenario asserts on it with Value(1). A view that needs the caller says uses caller and puts the visibility rule in its expression, where the checker holds it.

Additional remarks

A read that must run inside a transaction with a write, such as a carried value the next contract needs, is a contract call in a flow, and that is the flows chapter’s subject. A view never writes and a route to it is always GET.

An internal counter named in an interface

Problem

The interface names a piece of state that is nobody’s business but the writer’s: a next-id counter, an index, a helper table. Every writer of every contract in the unit must now maintain it exactly as described, the examples must show it, and a different way of doing the same job is refused. In the experiments that shaped the language, the authoring review flagged two units of an accepted interface for this. The interface says what a unit answers and what its rows hold; how ids are minted is either the caller’s (an id parameter) or the flow’s (uses ids and fresh()).

Example

row Line { id: id, order: id, sku: id, qty: int(1, 99) }
unit Lines {
    caps storage;
    state lines: Line[16];
    // next_line is the id the next line gets; it goes up by one per add.
    state next_line: int = 1;
    contract add(order: id, sku: id, qty: int(1, 99)) -> id {
        // Inserts Line { id: as_id(next_line), order, sku, qty } and bumps next_line.
        outcomes Added(line);
        examples { {} (1, 7, 2) => Added(1) { lines: [Line { id: 1, order: 1, sku: 7, qty: 2 }], next_line: 2 }; }
    }
}
flow add_line(order: id, sku: id, qty: int(1, 99)) atomic { Lines.add(order, sku, qty); }

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

Nothing catches it; the interface check accepts any state a unit declares. The counter is a decision the interface author made for the writer, and the example pins it: the after-state must show next_line: 2.

Refactoring

row Line { id: id, order: id, sku: id, qty: int(1, 99) }
unit Lines {
    caps storage;
    state lines: Line[16];
    contract add(line: id, order: id, sku: id, qty: int(1, 99)) {
        // Inserts Line { id: line, order, sku, qty }; an existing line id is Exists.
        outcomes Added;
        examples { {} (1, 1, 7, 2) => Added { lines: [Line { id: 1, order: 1, sku: 7, qty: 2 }] }; }
    }
}
flow add_line(order: id, sku: id, qty: int(1, 99)) uses ids atomic { let line = fresh(); Lines.add(line, order, sku, qty); }

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

The line’s id comes from the flow, fresh, and the unit’s state is its rows and nothing else. The carried value is gone with the counter; the caller already knows the id it asked for.

Additional remarks

A number that is part of the product, such as a sequence customers see on their invoices, is a row’s field with a rule about it, not an internal counter, and belongs in the interface. The item is about state that exists only to implement something.

A unit every flow touches

Problem

One unit, often an audit log or an activity table, is called by every flow. Then every flow’s closure includes it, the whole program is one component, and every flow’s reachable walk draws from every other flow: verification cannot be partitioned, and nothing about the program’s structure is visible in its graph. Both real applications in the repository are one component for this reason.

Example

row Room { id: id, closed: bool }
row Note { id: id, body: string(64) }
row Entry { id: id, kind: int(1, 4) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id) { else => Added: rooms += [Room { id: room, closed: false }]; }
    contract close(room: id) { else => Closed: rooms[room].closed := true; }
}
unit Notes {
    state notes: Note[8];
    contract add(note: id, body: string(64)) { else => Added: notes += [Note { id: note, body }]; }
}
unit Activity {
    state entries: Entry[16];
    contract record(entry: id, kind: int(1, 4)) { else => Recorded: entries += [Entry { id: entry, kind }]; }
}
flow add_room(room: id, entry: id) atomic { Rooms.add(room); Activity.record(entry, 1); }
flow close_room(room: id, entry: id) atomic { Rooms.close(room); Activity.record(entry, 2); }
flow add_note(note: id, body: string(64), entry: id) atomic { Notes.add(note, body); Activity.record(entry, 3); }
scenario a_day { add_room(1, 1) => Recorded; add_note(1, "hi", 2) => Recorded; close_room(1, 3) => Recorded; }

vishy graph on it (the output is book/programs/anti-hub.graph.txt):

3 unit(s), 3 flow(s), 0 world invariant(s), 0 world-derived field(s): 1 component(s)
component 1: units Rooms, Notes, Activity | flows add_room, close_room, add_note | 0 invariant(s)
note: one component spans the whole world; every flow's walk draws from every flow. Look for a unit that every flow touches.

The verifier passes the program; the graph says what it costs.

Refactoring

row Room { id: id, closed: bool }
row Note { id: id, body: string(64) }
events { RoomAdded(room: id), RoomClosed(room: id), NoteAdded(note: id) }
unit Rooms {
    caps outbox;
    state rooms: Room[8];
    contract add(room: id) { else => Added: rooms += [Room { id: room, closed: false }], emit RoomAdded(room); }
    contract close(room: id) { else => Closed: rooms[room].closed := true, emit RoomClosed(room); }
}
unit Notes {
    caps outbox;
    state notes: Note[8];
    contract add(note: id, body: string(64)) { else => Added: notes += [Note { id: note, body }], emit NoteAdded(note); }
}
flow add_room(room: id) atomic { Rooms.add(room); }
flow close_room(room: id) atomic { Rooms.close(room); }
flow add_note(note: id, body: string(64)) atomic { Notes.add(note, body); }
scenario a_day { add_room(1) => Added; add_note(1, "hi") => Added; close_room(1) => Closed; }

2 unit(s), 3 flow(s), 0 world invariant(s), 0 world-derived field(s): 2 component(s)
component 1: units Rooms | flows add_room, close_room | 0 invariant(s)
component 2: units Notes | flows add_note | 0 invariant(s)
flow add_room: touches Rooms | re-checks 0 of 0 invariant(s), recomputes 0 of 0 derived | walks 2 of 3 flow(s)
flow close_room: touches Rooms | re-checks 0 of 0 invariant(s), recomputes 0 of 0 derived | walks 2 of 3 flow(s)
flow add_note: touches Notes | re-checks 0 of 0 invariant(s), recomputes 0 of 0 derived | walks 1 of 3 flow(s)
note: the largest component has 1 of 2 units; each component verifies independently.

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

The record of what happened is an event, emitted by the unit that did it, in the same transaction; a deliver declaration says where the events go, and the outbox is written with the state change, so nothing is lost. Rooms and notes are now two components, and each verifies on its own.

Additional remarks

A unit every flow touches because the product’s rules need it (a members table that every rule reads) is a fact about the product, not an anti-pattern, and the graph’s note is then a description. The item is about units that exist to be written to and are never read by a rule.

A coupling rule kept by no flow and not explained

Problem

A world invariant couples two units: a booking’s room is open. Every flow that changes either unit either keeps the rule, by calling the units in the order that keeps it, or cannot break it, and says why in a comment. A flow that does neither is where the verifier finds the world that breaks the rule, and a flow that keeps the rule without saying so is rewritten by the next writer into one that does not.

Example

row Room { id: id, closed: bool }
row Booking { id: id, room: id }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id) { else => Added: rooms += [Room { id: room, closed: false }]; }
    contract close(room: id) { else => Closed: rooms[room].closed := true; }
}
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id) { else => Booked: bookings += [Booking { id: booking, room }]; }
    contract clear_room(room: id) { else => Cleared: bookings -= where(b in bookings: b.room == room).id; }
}
// rule 1: a booking's room exists and is open.
invariant all(b in Bookings.bookings: any(r in Rooms.rooms: r.id == b.room && !r.closed));
flow add_room(room: id) atomic { Rooms.add(room); }
flow book(booking: id, room: id) atomic { Bookings.book(booking, room); }
flow close_room(room: id) atomic { Rooms.close(room); }
scenario a_day { add_room(1) => Added; book(1, 1) => Booked; close_room(1) => Closed; }

book never asks whether the room is open; close_room never clears the bookings. The verifier finds both:

verify FAILED: 5 failure(s):
[1] scenario a_day step 3 (close_room): flow close_room: world invariant 1 violated: after World { rooms: Rooms { rooms: [Room { id: 1, closed: true }] }, bookings: Bookings { bookings: [Booking { id: 1, room: 1 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (1,) out Closed
  world World { rooms: Rooms { rooms: [Room { id: 1, closed: true }] }, bookings: Bookings { bookings: [Booking { id: 1, room: 1 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 }
[2] reachable walk, flow book: flow book: world invariant 1 violated: after World { rooms: Rooms { rooms: [] }, bookings: Bookings { bookings: [Booking { id: 12, room: 4 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (12, 4) out Booked
[3] reachable walk, flow close_room: flow close_room: world invariant 1 violated: after World { rooms: Rooms { rooms: [Room { id: 0, closed: true }] }, bookings: Bookings { bookings: [Booking { id: 0, room: 0 }, Booking { id: 7, room: 0 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (0,) out Closed
[4] flow book: flow book: world invariant 1 violated: after World { rooms: Rooms { rooms: [Room { id: 0, closed: true }] }, bookings: Bookings { bookings: [Booking { id: 0, room: 0 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (0, 0) out Booked
  (world World { rooms: Rooms { rooms: [Room { id: 0, closed: true }] }, bookings: Bookings { bookings: [] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (0, 0))
[5] flow close_room: flow close_room: world invariant 1 violated: after World { rooms: Rooms { rooms: [Room { id: 10, closed: true }] }, bookings: Bookings { bookings: [Booking { id: 10, room: 10 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (10,) out Closed
  (world World { rooms: Rooms { rooms: [Room { id: 10, closed: false }] }, bookings: Bookings { bookings: [Booking { id: 10, room: 10 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (10,))

The first failure is the scenario’s own third step: closing a room with a booking in it. The others are the walks and the sampled flows, each with the world before and after.

Refactoring

row Room { id: id, closed: bool }
row Booking { id: id, room: id }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id) { else => Added: rooms += [Room { id: room, closed: false }]; }
    contract close(room: id) { else => Closed: rooms[room].closed := true; }
    contract is_open(room: id) {
        case !(room in rooms) => fail Unknown;
        case rooms[room].closed => fail RoomClosed;
        else => Open;
        examples { { rooms: [Room { id: 1, closed: true }] } (1) => RoomClosed; { rooms: [Room { id: 1, closed: false }] } (1) => Open; {} (9) => Unknown; }
    }
}
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id) { else => Booked: bookings += [Booking { id: booking, room }]; }
    contract clear_room(room: id) { else => Cleared: bookings -= where(b in bookings: b.room == room).id; }
}
// rule 1: a booking's room exists and is open.
invariant all(b in Bookings.bookings: any(r in Rooms.rooms: r.id == b.room && !r.closed));
// rule 1: unchanged because the flow adds an open room and touches no booking.
flow add_room(room: id) atomic { Rooms.add(room); }
// rule 1 is kept: the room says it is open before the booking is made.
flow book(booking: id, room: id) atomic { Rooms.is_open(room); Bookings.book(booking, room); }
// rule 1 is kept: the bookings go before the room closes.
flow close_room(room: id) atomic { Bookings.clear_room(room); Rooms.close(room); }
scenario a_day { add_room(1) => Added; book(1, 1) => Booked; book(2, 9) => Unknown; close_room(1) => Closed; book(3, 1) => RoomClosed; }

scenario a_day
  add_room(1) => Added
  book(1, 1) => Booked
  book(2, 9) => Unknown
  close_room(1) => Closed
  book(3, 1) => RoomClosed
  Rooms = Rooms { rooms: [Room { id: 1, closed: true }] }
  Bookings = Bookings { bookings: [] }
5 step(s), all as expected

verify: 3 examples, 5 scenario steps and 8000 sampled checks passed

Three comments, one per flow: the two that keep the rule say in which order, and the one that cannot break it says why. The verifier held the rule; the comments are for the writer who edits the flow next.

Additional remarks

A rule kept by a bound or a machine rather than by an order of calls needs no flow comment; the item is about rules that an order of calls keeps.

One outcome name with two shapes

Problem

An outcome name means one thing across the whole program: success or failure, with or without a value, of one type. A name used as a success in one unit and a failure in another is refused by the checker, and a brief that assigns the same name two meanings produces an interface that cannot be checked until the brief is amended. In the experiments that shaped the language a new flow’s success reused a name that an earlier account had used as a failure, and another flow was asked to fail with the name of a third flow’s success.

Example

row Room { id: id, seats: int(1, 200) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id, seats: int(1, 200)) {
        else => Added: rooms += [Room { id: room, seats }];
    }
}
unit Waitlist {
    state waiting: id[8];
    contract add(room: id) {
        case room in waiting => fail Added;
        else => Waiting: waiting += [room];
    }
}

book/refusals/anti-two-shapes.vish:11:38: error: outcome `Added` is declared differently elsewhere (fail / carried value / type must agree across the program)
          case room in waiting => fail Added;
                                       ^^^^^

Refactoring

row Room { id: id, seats: int(1, 200) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id, seats: int(1, 200)) {
        else => Added: rooms += [Room { id: room, seats }];
    }
}
unit Waitlist {
    state waiting: id[8];
    contract add(room: id) {
        case room in waiting => fail AlreadyWaiting;
        else => Waiting: waiting += [room];
        examples { {} (1) => Waiting { waiting: [1] }; { waiting: [1] } (1) => AlreadyWaiting; }
    }
}

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

The waitlist’s failure gets its own name. The rule reaches the brief: name the outcomes in the brief once, and keep a list.

Additional remarks

The same name in two units with the same shape is fine and often right (Added in both units above is a success without a value). The rule is about shape, not about reuse.

An unreachable outcome without its note

Problem

A rule makes a failure impossible: a ledger kept balanced by its invariant is never Unbalanced. A contract that declares the failure anyway, with a guard, has a case the sampler never reaches, because the sampler draws only states that satisfy the invariant; the verifier refuses the program for the unreached outcome. An example that produces it would have to start from a state that cannot exist. The failure is not declared; the flow says in a comment that it is unreachable and under which rule.

Example

row Entry { id: id, debit: int(0, 9999), credit: int(0, 9999) }
unit Ledger {
    state entries: Entry[8];
    invariant sum(entries.debit) == sum(entries.credit);
    contract post(entry: id, amount: int(1, 9999)) {
        else => Posted: entries += [Entry { id: entry, debit: amount, credit: amount }];
    }
    contract balance_check() {
        case sum(entries.debit) != sum(entries.credit) => fail Unbalanced;
        else => Balanced;
        examples { {} () => Balanced; }
    }
}
scenario posting { Ledger.post(1, 100) => Posted; Ledger.balance_check() => Balanced; }

verify FAILED: 1 failure(s):
[1] Ledger.balance_check: outcome `Unbalanced` 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

Refactoring

row Entry { id: id, debit: int(0, 9999), credit: int(0, 9999) }
unit Ledger {
    state entries: Entry[8];
    invariant sum(entries.debit) == sum(entries.credit);
    contract post(entry: id, amount: int(1, 9999)) {
        else => Posted: entries += [Entry { id: entry, debit: amount, credit: amount }];
    }
    contract balance_check() {
        else => Balanced;
        examples { {} () => Balanced; }
    }
}
// Outcome: Unbalanced is unreachable under rule: balanced (the invariant); no contract declares it.
flow check_books() atomic { Ledger.balance_check(); }
scenario posting { Ledger.post(1, 100) => Posted; check_books() => Balanced; }

verify: 1 examples, 2 scenario steps and 4000 sampled checks passed

The case is gone, and the comment above the flow records that the brief’s failure was considered and why it has no outcome, so the next reader does not put it back.

Additional remarks

An outcome that is reachable but that the sampler does not draw at a thousand iterations gets an example that produces it, not a note; the verifier’s message names both possibilities. The note is for outcomes a rule forbids.

A contract that needs another unit’s fact

Problem

A contract’s guard needs something another unit knows: the room’s seat count, the customer’s tier. A unit cannot read another unit, and the checker refuses the attempt. The mistake that follows the refusal is worse than the refusal: moving the row into the wrong unit, copying the fact into a second table that goes stale, or changing the brief so the rule disappears. The fact is carried in by the flow, as a value, into the unit that owns the data.

Example

row Room { id: id, seats: int(1, 200) }
row Booking { id: id, room: id, people: int(1, 200) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id, seats: int(1, 200)) { else => Added: rooms += [Room { id: room, seats }]; }
}
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id, people: int(1, 200)) {
        case Rooms.rooms[room].seats < people => fail TooSmall;
        else => Booked: bookings += [Booking { id: booking, room, people }];
    }
}
flow book(booking: id, room: id, people: int(1, 200)) atomic { Bookings.book(booking, room, people); }

book/refusals/anti-reach.vish:10:14: error: unknown name `Rooms`
          case Rooms.rooms[room].seats < people => fail TooSmall;
               ^^^^^

Inside Bookings, Rooms is not a name.

Refactoring

row Room { id: id, seats: int(1, 200) }
row Booking { id: id, room: id, people: int(1, 200) }
unit Rooms {
    state rooms: Room[8];
    contract add(room: id, seats: int(1, 200)) { else => Added: rooms += [Room { id: room, seats }]; }
    contract seats_of(room: id) -> int {
        case !(room in rooms) => fail Unknown;
        else => Seats(rooms[room].seats);
        examples { { rooms: [Room { id: 1, seats: 4 }] } (1) => Seats(4); {} (9) => Unknown; }
    }
}
unit Bookings {
    state bookings: Booking[8];
    contract book(booking: id, room: id, people: int(1, 200), seats: int(1, 200)) {
        case seats < people => fail TooSmall;
        else => Booked: bookings += [Booking { id: booking, room, people }];
        examples { {} (1, 1, 3, 4) => Booked { bookings: [Booking { id: 1, room: 1, people: 3 }] }; {} (1, 1, 5, 4) => TooSmall; }
    }
}
// the flow carries the room's seats into the unit that owns the bookings.
flow book(booking: id, room: id, people: int(1, 200)) atomic { let seats = Rooms.seats_of(room); Bookings.book(booking, room, people, seats); }
scenario a_day { Rooms.add(1, 4) => Added; book(1, 1, 3) => Booked; book(2, 1, 5) => TooSmall; book(3, 9, 1) => Unknown; }

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

Rooms answers the seat count as a carried value, the flow binds it and passes it on, and book decides with a fact it was given. The absent room fails in Rooms, before Bookings is reached, and the scenario shows all three outcomes through the flow.

Additional remarks

When the fact is a verdict rather than a value (fits or not), the first item on this page applies instead: let the unit that knows fail. When the fact is needed by a rule that must hold at every moment, it is a world invariant or a world-derived column, which no contract reads and every flow is checked against.