Declared writes

A declared write is a change to one row, written down as data: which row, what it sets, what it adds to, and what the row must hold for the change to make sense. Because it is data, every party reads the same declaration. The server's writer turns it into one compare-and-set statement, the guard decides it over the row version that statement will change, and the client shows it before the answer comes. Nothing reads the row in one statement and writes it in another, so nothing another request does in between is written over.

This guide covers preconditions, increments, computed assignments, invariants over a row and over a change, a guard that holds where the write commits, operation ids, a write ledger, durable writes, a revision the database moves, and what the client shows and refuses before the answer. The runnable version is examples/writes.