The unit as a whole: fixtures, capabilities, ownership

The chapters of this part took a unit apart: its values, its tables, its deltas, its expressions, its machines and functions. This one puts a unit back together with the declarations that belong to the unit as a whole, and ends where the next part begins: at the edge of the unit, which nothing crosses.

events { Opened(ticket: id, at: instant) }
row Ticket { id: id, opened: instant, closed: option<instant>, open: bool }
unit Desk {
    caps ids, outbox, storage;
    state tickets: Ticket[8];
    derived tickets.open = for t => t.closed == none;
    derived open_count: int = count(t in tickets: t.closed == none);
    fixture Two = { tickets: [
        Ticket { id: 1, opened: 1000, closed: none },
        Ticket { id: 2, opened: 2000, closed: some(3000) } ] };
    invariant all(t in tickets: match t.closed { some c => c >= t.opened, none => true });
    commutes { close };
    contract open(now: instant) -> id {
        uses ids;
        else => let t = fresh(); Opened(t): tickets += [Ticket { id: t, opened: now, closed: none }], emit Opened(t, now);
        examples {
            {} (1000) => Opened(1) { tickets: [Ticket { id: 1, opened: 1000, closed: none, open: true }] };
            Two (5000) => Opened(3) Two with { tickets: [
                Ticket { id: 1, opened: 1000, closed: none, open: true },
                Ticket { id: 2, opened: 2000, closed: some(3000), open: false },
                Ticket { id: 3, opened: 5000, closed: none, open: true } ] };
        }
    }
    contract close(ticket: id, now: instant) {
        case tickets[ticket].closed != none => fail AlreadyClosed;
        else => Closed: tickets[ticket].closed := some(max(now, tickets[ticket].opened));
        examples {
            Two (1, 4000) => Closed Two with { tickets: [
                Ticket { id: 1, opened: 1000, closed: some(4000), open: false },
                Ticket { id: 2, opened: 2000, closed: some(3000), open: false } ] };
            Two (2, 4000) => AlreadyClosed;
            Two with { tickets: [Ticket { id: 5, opened: 9000, closed: none }] } (5, 4000)
                => Closed { tickets: [Ticket { id: 5, opened: 9000, closed: some(9000), open: false }] };
        }
    }
    contract waiting() -> int => Waiting(open_count);
}
flow open() uses clock, ids atomic { Desk.open(now); }
flow close(ticket: id) uses clock atomic { Desk.close(ticket, now); }
scenario a_morning {
    at 1000 open() => Opened(first);
    at 2500 open() => Opened(_);
    at 4000 close(first) => Closed;
    Desk.waiting() => Waiting(1);
}

Capabilities

A unit’s contracts compute from their arguments and the unit’s state, and nothing else. Anything more is a capability, declared on the unit with caps, so that what a unit can do to the world is written in one line at its top:

• caps ids lets a contract that says uses ids; call fresh(), a new id above every id the unit knows. open mints the ticket’s id this way, so no caller chooses it. In an example the new id is one more than the largest present: 1 in an empty desk, 3 in the fixture Two.
• caps outbox lets a contract emit events, as the chapter on deltas showed.
• caps storage makes the unit’s state persist when the program is served, and changes nothing else; the chapter on storage shows it.

A contract that uses a capability its unit did not declare is refused (book/refusals/unit-emit.vish):

book/refusals/unit-emit.vish:5:105: error: `emit` needs `caps outbox` on unit `Desk`
      contract open(ticket: id, now: instant) => Opened: tickets += [Ticket { id: ticket, opened: now }], emit Opened(ticket);
                                                                                                          ^^^^^^^^^^^^^^^^^^^

The time is not among them. A contract does not read a clock: open and close take now: instant as an argument. The clock belongs to the flow, the transaction that calls the contract: flow open() uses clock, ids atomic { Desk.open(now); } binds now and passes it in, and a scenario sets it with at 1000. Flows are the next part’s subject; here the point is that a contract’s result depends only on what it is given, which is why an example can pin it down.

Fixtures

fixture Two = { … }; names a state, written like an example’s before-state. An example may start from it by name: Two (2, 4000) => AlreadyClosed; is the whole example for closing a closed ticket. Two with { … } is the fixture with some fields replaced, and it may stand on either side of an example: the third close example starts from Two with a single late ticket, and the first ends at Two with both tickets closed. A fixture is shared vocabulary for examples, so a reader learns the state once.

Derived fields

derived tickets.open = for t => t.closed == none; is a derived column: a field of every row, defined by an equation and kept up to date by the compiler after every call. No contract assigns it; a row literal in a delta leaves it out, and the run shows it filled in. derived open_count: int = count(…) is a derived scalar of the unit, read like any state field by waiting. A derived field says a fact once instead of in every contract that could change it.

The invariant

A unit has one invariant, several conditions joined with &&. Here it says a ticket is never closed before it was opened, which close keeps with max(now, opened). The verifier checks it after every call, from every state it samples.

scenario a_morning
  open() => Opened(1)
  open() => Opened(2)
  close(1) => Closed
  Desk.waiting() => Waiting(1)
  Desk = Desk { tickets: [Ticket { id: 1, opened: 1000, closed: Some(4000), open: false }, Ticket { id: 2, opened: 2500, closed: None, open: true }], open_count: 1, outbox: [Opened { ticket: 1, at: 1000 }, Opened { ticket: 2, at: 2500 }] }
4 step(s), all as expected

verify: 5 examples, 4 scenario steps, 6000 sampled checks and 1000 commutativity checks passed

Commutes

commutes { close }; declares that calls to close may happen in either order with the same result. The verifier takes a sampled state, applies pairs of such calls in both orders, and reports when the results differ: the thousand commutativity checks in the verdict. The chapter on order and commutativity says why that matters when many writers touch one unit.

Ownership

The first removal, stated at the start of this part, is the one this chapter ends on: nothing outside a unit reads or writes its state. Here is a second unit that wants to refuse a shift change while tickets are waiting, by looking at the desk (book/refusals/unit-reach.vish):

row Ticket { id: id, opened: instant, closed: option<instant> }
unit Desk {
    state tickets: Ticket[8];
    contract open(ticket: id, now: instant) => Opened: tickets += [Ticket { id: ticket, opened: now, closed: none }];
}
unit Staff {
    state on_duty: int = 0;
    contract leave() {
        case any(t in Desk.tickets: t.closed == none) => fail TicketsWaiting;
        else => Left: on_duty -= 1;
    }
}

book/refusals/unit-reach.vish:9:23: error: unknown name `Desk`
          case any(t in Desk.tickets: t.closed == none) => fail TicketsWaiting;
                        ^^^^

Inside a unit, another unit is not even a name, so there is nothing to make public and no modifier to relax. Only flows compose units: a flow asks the desk how many tickets are open, receives the answer as a value, and passes it to the staff unit’s contract as an argument. That is the next part of the book.

What the rule buys is everything in this part. A unit’s rules are about its own state, so they can be checked on the unit alone, from sampled states of that unit alone; its examples are complete, since no other code can change what they describe; and a person or a model given one unit to write needs to know nothing about the others but the flows’ arguments.

Try

In close, replace some(max(now, tickets[ticket].opened)) with some(now). The program checks. vishy verify fails the third close example first: the ticket opened at 9000 is now closed at 4000, and the invariant is broken after the call. The sampled checks and the flow walk find the same defect from random states.