Boundary anti-patterns

Mistakes at the edge of the core, where sealed functions and effects take on work the verifier could have seen, or a program’s shape changes without telling the store. Four items, each with a program the guide’s check runs.

The sealed layer or an effect where the core suffices

Problem

A sum, a count, a lookup, a selection by rank: the core has a quantifier for each, and a quantifier is sampled in every state the verifier draws. The same computation written as a sealed function with a while, or as an effect with a Rust body, is tested by its examples and nothing else: a sealed function is never sampled on its own, and an effect’s body is never run by the verifier at all. What was one checked expression becomes a boundary the verifier stops at, with a step budget and a declared type on the far side. The core is closed so that everything in it is checkable; leaving it for what it already does gives that up for nothing.

Example

row Line { id: id, qty: int(1, 99) }
sealed fn total_qty(xs: int[]) -> int {
    var i = 0; var t = 0;
    while i < len(xs) { t := t + xs[i]; i := i + 1; }
    t
}
examples total_qty { ([]) => 0; ([2, 3]) => 5; }
unit Cart {
    state lines: Line[8];
    contract add(line: id, qty: int(1, 99)) { else => Added: lines += [Line { id: line, qty }]; }
    contract total() -> int {
        else => Total(total_qty(lines.qty));
        examples { {} () => Total(0); }
    }
}
scenario two { Cart.add(1, 2) => Added; Cart.add(2, 3) => Added; Cart.total() => Total(5); }

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

Nothing catches it. The sealed function has three examples and they pass; the contract that calls it has one. What the verifier does not do is draw a thousand carts and check that the total is the sum of the lines, because no rule says so, and the loop that would compute it is behind the boundary.

Refactoring

row Line { id: id, qty: int(1, 99) }
unit Cart {
    state lines: Line[8];
    contract add(line: id, qty: int(1, 99)) { else => Added: lines += [Line { id: line, qty }]; }
    contract total() -> int {
        ensures result == sum(lines.qty);
        else => Total(sum(lines.qty));
        examples { {} () => Total(0); }
    }
}
scenario two { Cart.add(1, 2) => Added; Cart.add(2, 3) => Added; Cart.total() => Total(5); }

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

sum over the column is the whole computation, and the property on the contract says it is the answer, so every sampled state checks it. The sealed function, its examples and its loop are gone.

Additional remarks

The sealed layer is for what the core cannot say: recursion, a tree, unbounded text, a parser. The test is whether the computation can be written as a quantifier over a table; when it can, it belongs in the core. The chapter on functions draws the line in detail, and the three-kinds-of-code table on What Vishy is not says what each side is trusted with.

Print-like effects

Problem

An effect that exists to write a line somewhere, a log, a console, a notification, is called from a flow and returns a value nobody uses. It is not a fact the program needs from the world; it is a side effect the program wants the world to have. Vishy’s form for that is an event: emitted by the unit that did the thing, in the same transaction, checked by scenarios and by ensures emitted, and carried out of the program by a deliver declaration. A print-like effect is checked by nothing, appears in no outcome, has already happened when a later call fails and the transaction rolls back, and, placed last, leaves the flow with no outcome to name.

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 }]; }
}
effect log_line(msg: string(200)) -> bool
  impl { eprintln!("{}", msg); true }
  fixtures { ("room added") => true; }
flow add_room(room: id) atomic { log_line("room added"); Rooms.add(room); }
scenario one { add_room(1) => Added; }

scenario one
  add_room(1) => Added
  Rooms = Rooms { rooms: [Room { id: 1, closed: false }] }
1 step(s), all as expected

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

Nothing catches it. In verification the effect answers from its fixture; in a service it runs the Rust, before the state change commits and whether or not it does. The line is written; the program does not know it was.

Refactoring

row Room { id: id, closed: bool }
events { RoomAdded(room: id) }
unit Rooms {
    caps outbox;
    state rooms: Room[8];
    contract add(room: id) {
        else => Added: rooms += [Room { id: room, closed: false }], emit RoomAdded(room) ensures emitted([RoomAdded(room)]);
        examples { {} (1) => Added { rooms: [Room { id: 1, closed: false }] }; }
    }
}
flow add_room(room: id) atomic { Rooms.add(room); }
scenario one { add_room(1) => Added; }

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

The unit emits RoomAdded as part of the change, the case’s ensures emitted holds it, and the example runs it. A deliver RoomAdded to … line, which this program leaves out, is where the world learns of it: one outbox row per event, written in the flow’s transaction, never lost and never recorded without its cause.

Additional remarks

An effect is right when the program needs an answer from outside (a rate, a lookup, a hash) or when the outside must act before the flow can continue. A record of what the program did is an event.

Logic inside an effect the verifier cannot see

Problem

A rule of the product is written in an effect’s Rust body: whether a booking fits, whether a discount applies. The verifier never runs Rust. In verification an effect answers with a fixture’s value when the arguments match one, and otherwise with a sampled value, so the rule is invisible to every check: a scenario that states the product’s real behaviour fails or passes by what the sampler drew, and no invariant can be held to the rule because the verifier cannot see it. The cost is a program verified against a rule that is not there, and a service that behaves differently from what was verified.

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 seats_of(room: id) -> int {
        case !(room in rooms) => fail Unknown;
        else => Seats(rooms[room].seats);
    }
}
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 }];
    }
}
effect fits(seats: int(1, 200), people: int(1, 200)) -> bool
  impl { seats >= people }
  fixtures { (4, 3) => true; (4, 5) => false; }
flow book(booking: id, room: id, people: int(1, 200)) atomic { let seats = Rooms.seats_of(room); let ok = fits(seats, 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; book(3, 1, 1) => Booked; }

The last step books one person into a room of four, which the Rust says fits. The verifier did not run the Rust:

verify FAILED: 1 failure(s):
[1] scenario a_day step 4 (book): expected Booked, got TooSmall from Bookings.book
  world World { rooms: Rooms { rooms: [Room { id: 1, seats: 4 }] }, bookings: Bookings { bookings: [Booking { id: 1, room: 1, people: 3 }] },  __now: 0, __ids: 0, __seed: 0, __caller: 0 }

No fixture covers a room of four and one person, so the effect answered with a drawn value, false, and the step that states the product’s behaviour failed. The same program with a different scenario would pass, for the same reason.

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 }];
    }
}
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; book(3, 1, 1) => Booked; }

scenario a_day
  Rooms.add(1, 4) => Added
  book(1, 1, 3) => Booked
  book(2, 1, 5) => TooSmall
  book(3, 1, 1) => Booked
  Rooms = Rooms { rooms: [Room { id: 1, seats: 4 }] }
  Bookings = Bookings { bookings: [Booking { id: 1, room: 1, people: 3 }, Booking { id: 3, room: 1, people: 1 }] }
4 step(s), all as expected

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

The rule is a guard in the unit that owns the seats, with examples for each outcome; the effect is gone. Every sampled state checks the guard, and the scenario passes because the rule is now in the program.

Additional remarks

The rule in the example was a comparison the core writes in one guard. A computation that genuinely needs Rust (a cryptographic check, a call to a service) stays an effect, and the rule about its answer is written in the core around it: the contract that consumes the answer states what the answer must satisfy, with an outcome for when it does not.

A row change deployed without a version and a migration

Problem

A row’s field is renamed or its meaning changes, the program is rebuilt, and the new service meets a store written by the old one. Without a version the compiler has nothing to compare; without a migrate it has nothing to run. The language derives what it can (an added field with a default, a widened bound, a new table) and refuses what would lose data, naming the declaration to write. The anti-pattern is to skip the comparison: to build the new program alone, where it checks, and deploy it onto a store it was never checked against.

Example

version 2;
row Customer { id: id, full_name: string(64) }
unit Customers {
    caps storage;
    state customers: Customer[8];
    contract add(customer: id, full_name: string(64)) { else => Added: customers += [Customer { id: customer, full_name }]; }
}

Checked alone, this program is accepted. Checked against the program that wrote the store (vishy check … --from= the version 1 program, book/refusals/migrate/anti-migration.from.vish), it is refused:

book/refusals/migrate/anti-migration.vish:1:1: error: `Customer.name` is gone and `Customer.full_name` is new with the same type: if that is a rename write `migrate Customer from 1 { full_name = old.name; }`; if the data is to be dropped write `migrate Customer from 1 { drop name; }`
  version 2;
  ^

The message names the field that is gone, the field that is new, and the two declarations that would say which of the two things happened.

Refactoring

version 2;
row Customer { id: id, full_name: string(64) }
migrate Customer from 1 { full_name = old.name; }
    examples { { id: 1, name: "Ada" } => { id: 1, full_name: "Ada" }; }
unit Customers {
    caps storage;
    state customers: Customer[8];
    contract add(customer: id, full_name: string(64)) { else => Added: customers += [Customer { id: customer, full_name }]; }
}

Checked against version 1:

migrate: 1 step(s) from version 1 to 2; 1 example(s) passed
ok: 1 row(s), 0 event(s), 0 fn(s), 1 unit(s), 1 contract(s), 0 flow(s)

The migration says the rename, its example shows one row carried forward, and a service built with --from carries the store forward exactly once and records the version.

Additional remarks

A program without caps storage has no store and no versions. A change the per-row form cannot say (data from another table, a backfill in batches) is written by hand as an effect or a script, and the chapter on versions and migrations lists what is and is not covered.