Flows: one transaction across units

Everything so far lived inside one unit, and the first removal says a unit cannot see another. A program with two units needs one more thing: a place where they meet. That place is a flow, a named sequence of contract calls on several units that runs as one transaction. It is the only thing in the language that composes units.

row Ticket { id: id, seat: int(1, 3), holder: id, sold: instant }
unit Seats {
    state left: int(0, 3) = 3;
    contract take() -> int(1, 3) {
        case left == 0 => fail SoldOut;
        else => Taken(left): left -= 1;
    }
}
unit Tickets {
    state tickets: Ticket[3];
    contract issue(ticket: id, seat: int(1, 3), holder: id, at: instant) -> id {
        case count(t in tickets: t.holder == holder) >= 2 => fail Limit;
        else => Issued(ticket): tickets += [Ticket { id: ticket, seat, holder, sold: at }];
    }
}
flow buy() uses clock, ids, caller atomic {
    let ticket = fresh();
    let seat = Seats.take();
    Tickets.issue(ticket, seat, caller, now);
    ensures Seats.left == old(Seats.left) - 1;
}
scenario a_sale {
    at 1000 as 7 buy() => Issued(_);
    at 2000 as 7 buy() => Issued(_);
    at 3000 as 7 buy() => Limit;
    at 4000 as 8 buy() => Issued(_);
    at 5000 as 9 buy() => SoldOut;
}

A sequence of calls

flow buy() calls Seats.take, then Tickets.issue, in that order. Each step names a unit and one of its contracts. Neither unit knows the other exists; the flow knows both, and it is the only code that does.

Carried values travel

let seat = Seats.take(); binds the value that take carries, the seat number in Taken(left), and the next step passes it to issue. This is how a fact one unit holds reaches another: as a value, through a flow, never by reading.

A value can be bound only when every success case of the contract carries one. Add a case that answers a plain outcome and the name would be empty whenever that case applies, so the checker refuses the flow:

unit Seats {
    state left: int(0, 3) = 3;
    contract take() -> int(1, 3) {
        case left == 0 => fail SoldOut;
        case left == 1 => LastSeat: left -= 1;
        else => Taken(left): left -= 1;
    }
}
unit Tickets {
    state sold: int(0, 3) = 0;
    contract issue(seat: int(1, 3)) => Issued: sold += 1;
}
flow buy() atomic {
    let seat = Seats.take();
    Tickets.issue(seat);
}

book/refusals/flows-no-value.vish:14:9: error: `let seat = Seats.take(...)`: every success case of the contract must carry a value to be bound
      let seat = Seats.take();
          ^^^^

Which outcome the caller hears

The steps run in order, and the first one that fails ends the flow: its failure is the flow’s answer. When every step succeeds, the flow’s outcome is the last call’s. So buy answers Issued with the new ticket’s id, SoldOut when the first step finds no seat (and issue never runs), and Limit when the second step finds that the buyer already holds two tickets.

scenario a_sale
  buy() => Issued(10)
  buy() => Issued(0)
  buy() => Limit
  buy() => Issued(4)
  buy() => SoldOut
  Seats = Seats { left: 0 }
  Tickets = Tickets { tickets: [Ticket { id: 10, seat: 3, holder: 7, sold: 1000 }, Ticket { id: 0, seat: 2, holder: 7, sold: 2000 }, Ticket { id: 4, seat: 1, holder: 8, sold: 4000 }] }
5 step(s), all as expected

One transaction

The flow is atomic: when any step fails, the whole world is restored to what it was before the flow began. Step 3 shows it. Buyer 7 asks for a third ticket; take succeeds and a seat is gone; then issue answers Limit. The seat comes back with the failure, which is why buyer 8 still gets one at step 4, and why the final world holds three tickets for three seats. The other mode, serial, keeps each step’s writes when a later step fails; the section below on kept steps shows the middle ground, and the Try section shows what serial does here.

What a flow may use

Beyond its arguments, a flow sees only what its header’s uses names. clock binds now, the time of the call; a scenario sets it with at 1000, and the tickets’ sold times are the scenario’s. caller binds caller, the identity of whoever called; a scenario sets it with as 7. ids allows let ticket = fresh();, an id that no table in the world holds. The run drew 10, 0 and 4: a scenario cannot know in advance which id it will get, so it expects Issued(_), any value.

A promise about the whole flow

ensures Seats.left == old(Seats.left) - 1; is checked after the flow commits, where Seats.left is the value after and old(Seats.left) the value before. It is a rule about one flow, the way an invariant is a rule about every moment:

verify: 0 examples, 5 scenario steps and 3000 sampled checks passed

Among the sampled checks are runs of buy from sampled worlds, each followed by that check. A failed flow changes nothing, so the promise is only asked of a flow that ran to its end.

Stop and keep

Two more step forms cover flows that should neither simply succeed nor simply roll back.

row Parcel { id: id, delivered: bool }
row Attempt { parcel: id, at: instant }
unit Log {
    state attempts: Attempt[8] ordered;
    contract note(parcel: id, at: instant) => Noted: attempts += [Attempt { parcel, at }];
}
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 owed: money(2) = 0;
    contract pay(fee: money(2)) => Paid: owed += fee;
}
flow attempt(parcel: id) uses clock atomic {
    keep Log.note(parcel, now);
    Parcels.deliver(parcel);
    Courier.pay(500);
}
scenario a_round {
    Parcels.add(1) => Added;
    at 1000 attempt(2) => NoSuchParcel;
    at 2000 attempt(1) => Paid;
    at 3000 attempt(1) => AlreadyDelivered;
}

A case may answer stop AlreadyDelivered. A stop outcome is a success that ends the flow at that call: its writes and the earlier steps’ writes commit, the later steps do not run, and it carries no value. Here a repeated delivery is not an error, and it must not pay the courier twice.

keep Log.note(parcel, now); is a kept step. It commits what the flow has written so far: a later failure restores the world to how it was right after the kept step, not to the start. So a refused attempt is still recorded.

scenario a_round
  Parcels.add(1) => Added
  attempt(2) => NoSuchParcel
  attempt(1) => Paid
  attempt(1) => AlreadyDelivered
  Log = Log { attempts: [Attempt { parcel: 2, at: 1000 }, Attempt { parcel: 1, at: 2000 }, Attempt { parcel: 1, at: 3000 }] }
  Parcels = Parcels { parcels: [Parcel { id: 1, delivered: true }] }
  Courier = Courier { owed: 500 }
4 step(s), all as expected

Three attempts, three lines in the log. The first was for a parcel that does not exist: deliver failed, the flow answered NoSuchParcel, and only the kept line survived. The second delivered and paid, and answered Paid, the last call’s outcome. The third stopped at AlreadyDelivered, a success, before the payment; the courier is owed 500, once. The scenario’s first step, Parcels.add(1), calls a contract with no flow around it, which the chapter on scenarios explains.

An outcome’s kind, success, failure or stop, is one for the whole program, because a caller switches on the name. A parcel that is already delivered cannot be both a harmless repeat and a refusal:

row Parcel { id: id, delivered: bool }
unit Parcels {
    state parcels: Parcel[4];
    contract deliver(parcel: id) {
        case parcels[parcel].delivered => stop AlreadyDelivered;
        else => Delivered: parcels[parcel].delivered := true;
    }
    contract recall(parcel: id) {
        case parcels[parcel].delivered => fail AlreadyDelivered;
        else => Recalled: remove parcels[parcel];
    }
}

book/refusals/flows-stop-kind.vish:9:48: error: outcome `AlreadyDelivered` is declared differently elsewhere (fail / carried value / type must agree across the program)
          case parcels[parcel].delivered => fail AlreadyDelivered;
                                                 ^^^^^^^^^^^^^^^^

Name the refusal differently, TooLate, and both contracts check.

A contract cannot do this itself

The line that is a step in a flow is refused inside a contract:

row Ticket { id: id, seat: int(1, 3) }
unit Seats {
    state left: int(0, 3) = 3;
    contract take() -> int(1, 3) {
        case left == 0 => fail SoldOut;
        else => Taken(left): left -= 1;
    }
}
unit Tickets {
    state tickets: Ticket[3];
    contract issue(ticket: id) -> id {
        else => let seat = Seats.take(); Issued(ticket): tickets += [Ticket { id: ticket, seat }];
    }
}

book/refusals/flows-call.vish:12:38: error: expected `;`, found `(`
          else => let seat = Seats.take(); Issued(ticket): tickets += [Ticket { id: ticket, seat }];
                                       ^

The checker reads Seats.take and stops at the parenthesis: a contract has no call to parse, only its own cases and deltas. This is the first removal again, and it pays: a contract changes one unit, so it is checked against that unit’s invariant alone, and everything that crosses units is in a flow, where the verifier checks the whole world.

Try

In flows-tickets.vish, change atomic to serial. The program still checks, but the scenario now fails at step 4: expected Issued(_), got SoldOut from Seats.take. Buyer 7’s refused third purchase took a seat, and with nothing restored, the seat was never given back.