Deltas: saying what changes

A contract’s case ends with its deltas: the list, after the colon, of what the call changes. There is no other way for a contract to change anything, and nothing a delta does not name changes. That is the second of the language’s two removals, and this chapter is the full list of what a delta can say.

events { Restocked(item: id, qty: int) }
row Item { id: id, qty: int, price: money(2), on_sale: bool }
unit Stock {
    caps outbox;
    state items: Item[8];
    state peak: int = 0;
    state sales: int = 0;
    contract add(item: id, price: money(2)) => Added: items += [Item { id: item, qty: 0, price: price, on_sale: false }];
    contract restock(item: id, qty: int(1, 100)) {
        else => Restocked: items[item].qty += qty, peak max= items[item].qty + qty, emit Restocked(item, qty);
        examples {
            { items: [Item { id: 1, qty: 2, price: 500, on_sale: false }], peak: 4 } (1, 5)
                => Restocked { items: [Item { id: 1, qty: 7, price: 500, on_sale: false }], peak: 7 };
        }
    }
    contract sell(item: id) {
        case items[item].qty == 0 => fail SoldOut;
        else => Sold: items[item].qty -= 1, sales += 1;
    }
    contract reprice(item: id, price: money(2)) => Repriced: items[item].price := price;
    contract replace(item: id, price: money(2)) => Replaced: items[item] := Item { id: item, qty: 0, price: price, on_sale: false };
    contract drop(item: id) => Dropped: remove items[item];
    contract end_sale() => Ended: items.on_sale := false;
    contract sale_under(limit: money(2)) {
        else => OnSale: items.on_sale := for i where i.price <= limit => true;
        examples {
            { items: [Item { id: 1, qty: 3, price: 500, on_sale: false }, Item { id: 2, qty: 0, price: 900, on_sale: false }] } (600)
                => OnSale { items: [Item { id: 1, qty: 3, price: 500, on_sale: true }, Item { id: 2, qty: 0, price: 900, on_sale: false }] };
        }
    }
    contract halve_sale_prices() => Halved: items := for i where i.on_sale => with(i, price, i.price / 2);
    contract clear_empty() {
        else => Cleared: items -= where(i in items: i.qty == 0).id;
        examples {
            { items: [Item { id: 1, qty: 3, price: 500, on_sale: false }, Item { id: 2, qty: 0, price: 900, on_sale: false }], sales: 7 } ()
                => Cleared { items: [Item { id: 1, qty: 3, price: 500, on_sale: false }] };
        }
    }
}
scenario a_sale {
    Stock.add(1, 500) => Added;
    Stock.add(2, 900) => Added;
    Stock.restock(1, 5) => Restocked;
    Stock.sell(1) => Sold;
    Stock.sell(2) => SoldOut;
    Stock.reprice(9, 100) => Unknown;
    Stock.drop(9) => Dropped;
    Stock.replace(3, 700) => Replaced;
    Stock.sale_under(600) => OnSale;
    Stock.halve_sale_prices() => Halved;
    Stock.clear_empty() => Cleared;
}

Every right-hand side reads the state before the call

One rule governs every form: a delta’s expression is computed on the state as it was when the call began. In restock, items[item].qty += qty, peak max= items[item].qty + qty, the second delta reads the old quantity, so it adds qty itself to get the new one. The deltas of a case are a description of one step, not a sequence of statements.

Scalars

A scalar field takes five forms:

sales += 1 counts a sale. peak max= … keeps the highest stock level ever seen: it never goes down, whatever the new level is.

One row of a keyed table

reprice writes one field of a row, and the row must exist: reprice(9, 100) in the scenario answers Unknown, as the last chapter showed. Putting a whole row and removing one say what the table looks like afterwards, so they do not need the row to be there first. replace puts a whole row, every field given, at its key: replace(3, 700) finds no item 3 and inserts one. drop removes a row, and drop(9) of a row that is not there succeeds with nothing to remove. When “the row must exist” is part of the rule, write the case: case !(item in items) => fail Unknown;.

Every row at once

A column delta writes one field of every row: items.on_sale := false ends a sale on everything in stock. With for and where it writes only the rows a predicate selects, with the row bound to a name in both halves: items.on_sale := for i where i.price <= limit => true. The rows the predicate does not select keep their value, which the example of sale_under states exactly: item 1 at five hundred goes on sale, item 2 at nine hundred stays as it was.

A row replacement does the same with whole rows: items := for i where i.on_sale => with(i, price, i.price / 2) replaces each selected row with a new one, here the old row with its price halved. The ids must not change; it is an edit of rows in place, not a new table.

To remove the rows a predicate selects, subtract their ids: items -= where(i in items: i.qty == 0).id. The chapter on reading the state explains where.

A keyed table is never assigned whole. Rows enter with +=, leave with -= or remove, and change through one of the forms above, so every change to a table says which rows it touches.

Events

emit Restocked(item, qty) appends an event to the unit’s outbox, the record of what happened that the world outside may need to hear about. Events are declared at the top, events { Restocked(item: id, qty: int) }, and a unit that emits declares caps outbox. The run shows the outbox as part of the unit’s state:

scenario a_sale
  Stock.add(1, 500) => Added
  Stock.add(2, 900) => Added
  Stock.restock(1, 5) => Restocked
  Stock.sell(1) => Sold
  Stock.sell(2) => SoldOut
  Stock.reprice(9, 100) => Unknown
  Stock.drop(9) => Dropped
  Stock.replace(3, 700) => Replaced
  Stock.sale_under(600) => OnSale
  Stock.halve_sale_prices() => Halved
  Stock.clear_empty() => Cleared
  Stock = Stock { items: [Item { id: 1, qty: 4, price: 250, on_sale: true }], peak: 5, sales: 1, outbox: [Restocked { item: 1, qty: 5 }] }
11 step(s), all as expected

Item 1 went on sale and was halved to 250. Items 2 and 3 had no stock, so clear_empty removed them, item 3 only a few steps after replace put it there. peak is five, from the restock; sales is one, because the second sale failed and a failure changes nothing.

verify: 3 examples, 11 scenario steps and 19000 sampled checks passed

Two deltas, one cell

Because every delta reads the old state, two deltas that write the same cell of a table in one case would each compute from the old value, and one of the two writes would be lost. The verifier reports it as a conflict (book/failures/deltas-conflict.vish):

row Account { id: id, balance: money(2) }
unit Bank {
    state accounts: Account[8];
    contract transfer(from: id, to: id, amount: money(2)) {
        case amount <= 0 => fail BadAmount;
        else => Moved: accounts[from].balance -= amount, accounts[to].balance += amount;
        examples {
            { accounts: [Account { id: 1, balance: 500 }, Account { id: 2, balance: 0 }] } (1, 2, 200)
                => Moved { accounts: [Account { id: 1, balance: 300 }, Account { id: 2, balance: 200 }] };
        }
    }
}

verify FAILED: 1 failure(s):
[1] sampled check failed: Bank.transfer: Bank.transfer: conflicting deltas: `accounts[k].balance` is written twice in one case for the same key 2 (state Bank { accounts: [Account { id: 0, balance: 37 }, Account { id: 3, balance: -3 }, Account { id: 2, balance: 6 }, Account { id: 6, balance: 8 }] } args (2, 2, 44)); guard the case so the keys differ, or write a single delta
  (state Bank { accounts: [Account { id: 0, balance: 37 }, Account { id: 3, balance: -3 }, Account { id: 2, balance: 6 }, Account { id: 6, balance: 8 }] } args (2, 2, 44))

The example, from account 1 to account 2, passes. The sampler then called transfer(2, 2, 44): a transfer from an account to itself. Both deltas write the balance of account 2, one subtracting and one adding, and there is no single right answer for the order in which they apply. The verifier names the cell, the key and the arguments, and says what to do: guard the case so the keys differ, or write one delta. Here the guard is a rule the bank wants anyway, case from == to => fail SameAccount;, placed before the else; with it the program verifies.

Everything else is unchanged

Read any case of the stock unit and you know everything it can change. sell touches one row’s quantity and the sales count; it cannot touch a price, another row, or peak, because it does not name them. There is no method that changes something on the side and no statement three calls deep. Examples rely on it: an after-state lists what the deltas name, and the verifier checks that the rest stayed put.

Try

In restock, change peak max= items[item].qty + qty to peak max= items[item].qty, forgetting that the delta reads the quantity before the restock. The program still checks, and the scenario still passes, since it never asks for peak; its final state shows peak: 0. vishy verify fails on restock’s example, which starts at a peak of four and restocks two to seven: it expected peak: 7 and got peak: 4. The example was the only thing in the program that said what peak means.