World rules: invariants and derived state

A unit’s invariant speaks only of that unit’s state, because a unit cannot see any other. Some rules are about two units at once: a courier is paid once for each delivered parcel. Parcels knows nothing of payments and Courier knows nothing of parcels, so neither can state it. Such a rule is written at the top level of the program, where every unit’s state can be named, and it is called a world invariant.

row Parcel { id: id, delivered: bool }
unit Parcels {
    state parcels: Parcel[4];
    contract add(parcel: id) => Added: parcels += [Parcel { id: parcel, delivered: false }];
    contract deliver(parcel: id) {
        case !(parcel in parcels) => fail NoSuchParcel;
        case parcels[parcel].delivered => stop AlreadyDelivered;
        else => Delivered: parcels[parcel].delivered := true;
    }
}
unit Courier {
    state payments: int(0, 8) = 0;
    contract pay() => Paid: payments += 1;
}
// the courier is paid once for each delivered parcel
invariant Courier.payments == count(p in Parcels.parcels: p.delivered);
flow deliver(parcel: id) atomic { Parcels.deliver(parcel); Courier.pay(); }
scenario a_round {
    Parcels.add(1) => Added;
    deliver(1) => Paid;
    deliver(1) => AlreadyDelivered;
    deliver(2) => NoSuchParcel;
}

A rule over several units

invariant Courier.payments == count(p in Parcels.parcels: p.delivered); stands outside every unit and names each unit’s state as Unit.field. It must hold in the initial world (no parcels, no payments) and after every flow. It is not checked between the steps of a flow: after deliver has marked the parcel and before pay has run, the rule is broken for a moment, and that is allowed, because nobody sees the world halfway through a transaction.

scenario a_round
  Parcels.add(1) => Added
  deliver(1) => Paid
  deliver(1) => AlreadyDelivered
  deliver(2) => NoSuchParcel
  Parcels = Parcels { parcels: [Parcel { id: 1, delivered: true }] }
  Courier = Courier { payments: 1 }
4 step(s), all as expected

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

Who keeps it

No unit can keep a rule it cannot see. The flow that commands both units keeps it: deliver marks the parcel and then pays, as one transaction. When the parcel does not exist, deliver fails and nothing is paid. When the parcel was already delivered, deliver stops the flow as a success before the payment. Each way through the flow leaves the rule true, and that is what the verifier checked, walking the flows from worlds that satisfy the rule.

The order of the two steps is part of how the rule is kept. Swap them, paying first and delivering second (the program is book/failures/world-order.vish; the flow and the scenario are the lines that changed):

flow deliver(parcel: id) atomic { Courier.pay(); Parcels.deliver(parcel); }
scenario a_round {
    Parcels.add(1) => Added;
    deliver(1) => Delivered;
    deliver(1) => AlreadyDelivered;
    deliver(2) => NoSuchParcel;
}

It looks harmless, since an atomic flow undoes the payment if the delivery fails. But a stop is not a failure: it ends the flow as a success, and the steps before it commit.

verify FAILED: 3 failure(s):
[1] scenario a_round step 3 (deliver): flow deliver: world invariant 1 violated: after World { parcels: Parcels { parcels: [Parcel { id: 1, delivered: true }] }, courier: Courier { payments: 2 },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (1,) out AlreadyDelivered
  world World { parcels: Parcels { parcels: [Parcel { id: 1, delivered: true }] }, courier: Courier { payments: 2 },  __now: 0, __ids: 0, __seed: 0, __caller: 0 }
[2] reachable walk, flow deliver: flow deliver: world invariant 1 violated: after World { parcels: Parcels { parcels: [Parcel { id: 4, delivered: true }] }, courier: Courier { payments: 2 },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (4,) out AlreadyDelivered
[3] flow deliver: flow deliver: world invariant 1 violated: after World { parcels: Parcels { parcels: [Parcel { id: 4, delivered: true }] }, courier: Courier { payments: 2 },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (4,) out AlreadyDelivered
  (world World { parcels: Parcels { parcels: [Parcel { id: 4, delivered: true }] }, courier: Courier { payments: 1 },  __now: 0, __ids: 0, __seed: 0, __caller: 0 } args (4,))

Read the first failure. The scenario’s third step delivers parcel 1 again; the flow deliver answered AlreadyDelivered, and world invariant 1 (the first in source order) is violated after it: one delivered parcel, two payments. The second and third failures find the same thing by walking the flows from sampled worlds, and the third shows the world before the call, with one delivered parcel and one payment. Every failure names the flow, because the flow is the only code that could have kept the rule. The scenario’s second step now expects Delivered, because a flow’s outcome is its last call’s.

Derived state

Some facts about several units are not rules to keep but numbers to compute: how many parcels are waiting, how many each courier has delivered. Both follow from the parcels. A derived field is defined by an equation and kept by the compiler, which recomputes it after every flow. No contract writes it.

row Parcel { id: id, courier: id, delivered: bool }
row Courier { id: id, deliveries: int(0, 4) }
unit Parcels {
    state parcels: Parcel[4];
    contract add(parcel: id, courier: id) => Added: parcels += [Parcel { id: parcel, courier, delivered: false }];
    contract deliver(parcel: id) -> id {
        case !(parcel in parcels) => fail NoSuchParcel;
        case parcels[parcel].delivered => fail AlreadyDelivered;
        else => Delivered(parcels[parcel].courier): parcels[parcel].delivered := true;
    }
}
unit Couriers {
    state couriers: Courier[2];
    state waiting: int(0, 4);
    contract hire(courier: id) => Hired: couriers += [Courier { id: courier }];
    contract tally(courier: id) -> int(0, 4) {
        case !(courier in couriers) => fail NoSuchCourier;
        else => Tally(couriers[courier].deliveries);
    }
}
// a scalar: the parcels not yet delivered
derived Couriers.waiting = count(p in Parcels.parcels: !p.delivered);
// a column: for each courier, the parcels it has delivered
derived Couriers.couriers.deliveries = for c => count(p in Parcels.parcels: p.courier == c.id && p.delivered);
flow deliver(parcel: id) atomic { let courier = Parcels.deliver(parcel); Couriers.tally(courier); }
scenario a_round {
    Couriers.hire(7) => Hired;
    Parcels.add(1, 7) => Added;
    Parcels.add(2, 7) => Added;
    Parcels.add(3, 7) => Added;
    deliver(1) => Tally(0);
    deliver(2) => Tally(1);
    Couriers.tally(7) => Tally(2);
}

derived Couriers.waiting = … is a scalar: the unit declares the field as state, and the equation at the top level says what its value is. derived Couriers.couriers.deliveries = for c => … is a column: for each row c of the couriers table, the value of its deliveries field. The row that hire inserts leaves deliveries out, because the value is not the contract’s to give.

scenario a_round
  Couriers.hire(7) => Hired
  Parcels.add(1, 7) => Added
  Parcels.add(2, 7) => Added
  Parcels.add(3, 7) => Added
  deliver(1) => Tally(0)
  deliver(2) => Tally(1)
  Couriers.tally(7) => Tally(2)
  Parcels = Parcels { parcels: [Parcel { id: 1, courier: 7, delivered: true }, Parcel { id: 2, courier: 7, delivered: true }, Parcel { id: 3, courier: 7, delivered: false }] }
  Couriers = Couriers { couriers: [Courier { id: 7, deliveries: 2 }], waiting: 1 }
7 step(s), all as expected

verify: 0 examples, 7 scenario steps and 8000 sampled checks passed

The final world shows both: courier 7 has two deliveries, and one parcel is waiting. Nothing in the program ever wrote either number.

The value at the flow’s start

Read the fifth step. deliver(1) marks parcel 1 delivered and then, in the same flow, asks for courier 7’s tally; the answer is 0. Inside a flow, a unit reads its world-derived column as it was when the flow began, and the column is recomputed when the flow commits. The next flow answers 1, and the direct call after it answers 2. So a later step that reads a derived value sees the world before the flow, not the work of the steps before it; a fact that must be fresh travels as a carried value instead.

Never written

A derived field is the one piece of state that changes without a delta naming it, and in exchange no delta may name it:

row Parcel { id: id, courier: id, delivered: bool }
row Courier { id: id, deliveries: int(0, 4) }
unit Parcels {
    state parcels: Parcel[4];
    contract deliver(parcel: id) => Delivered: parcels[parcel].delivered := true;
}
unit Couriers {
    state couriers: Courier[2];
    contract credit(courier: id) => Credited: couriers[courier].deliveries += 1;
}
derived Couriers.couriers.deliveries = for c => count(p in Parcels.parcels: p.courier == c.id && p.delivered);

book/refusals/world-derived-write.vish:9:65: error: `couriers.deliveries` is a world-derived column and cannot be assigned
      contract credit(courier: id) => Credited: couriers[courier].deliveries += 1;
                                                                  ^^^^^^^^^^

The equation is the field’s only writer, so the rule “deliveries counts the delivered parcels” cannot be broken by a contract that forgot to update it; there is nothing to forget.

Try

In world-courier.vish, start the courier at one payment: state payments: int(0, 8) = 1;. The verifier fails, and among its four failures is the initial world violates a world invariant. A world rule must hold before the first flow, not only after it.