Build outward

Who may: a guard that holds where it commits#

Reading the row to check a rule and writing it are two statements, so a change of owner between them could let a stale decision write. Name a revision and the guard pins the write to the revision its rules were decided over. With Product carrying its guards (Guards.attach) and Policy their implementation, as in examples/writes/src:

const Db = bind(
  { Product },
  { Product: { table: products, visible: GuardDrizzle.visible(Policy, [Product]).Product } },
)
const guarded = GuardServer.writer(Product, Policy, writer(Db.Product), { revision: 'revision' })

The binding's visible rule is how the guard reads a row as its caller may see it; the guarded writer refuses a binding without one.

Every update and delete then lands only at that revision. If the row moved after the check, it is decided again over the row as it now is, up to three times, and then fails with "changed while it was written". Nothing is written over a version no rule saw. GuardServer.validate reports each write through a guarded writer with no revision that a change can come between (UnpinnedWrites).

A rule that reads another row ("the viewer holds a seat on the note's team") cannot be decided over the row alone. For an update or a delete, the guard hands it to the writer as requires, and the writer adds it to the same where, so it is judged against the other row as the statement runs; a row that fails it is Forbidden. A write that would change what such a rule reads of its own row is refused. See Guard's "Rules that read another row".

The guard speaks before the writer, in this order, so a refusal discloses nothing the caller may not read:

1. A row hidden from the caller, then a rule that does not hold: both Forbidden.
2. An input revision the row is not at: Conflict, not retried.
3. The precondition: Unmet, so it reaches only someone the rules let write.

A when or an expect over a member with a Read rule would answer for that member (Unmet or written), so the guarded writer refuses such a write before any rule, whether or not validate ran. The full rules are in Guard's "Serving writes".

How much: an increment#

increment adds an unmapped number from the input to a number field, in the statement (stock = stock + ?), so a concurrent change to the field is never lost:

const Restock = Mutation.write(
  'Restock',
  Write.update(
    Entity.input(
      Product,
      Schema.Struct({ id: Schema.String, revision: Schema.Number, quantity: Schema.Int }),
      { quantity: Entity.unmapped },
    ),
    { id: 'id', expect: 'revision', increment: { stock: 'quantity' } },
  ),
)

The field must be stored as a plain number. A nullable field, the id, the revision, and a field another key sets are refused at definition. The guard holds the row's rules over the sum the writer will store, so a rule stock >= 0 refuses a sale past zero.

An increment is not idempotent: applied twice, it adds twice. So it needs one of two protections, and RemoteServer.write refuses one with neither:

• expect a revision. A retry of a write that landed finds the row a revision on and is a Conflict. Simple, but two increments made from one read conflict too, though they would commute.
• A writer with a ledger (below). Two increments from one read both land, and a retry is recognised by its operation id. Such a write expects no revision:

const Sell = Mutation.write(
  'Sell',
  Write.update(
    Entity.input(Product, Schema.Struct({ id: Schema.String, quantity: Schema.Int }), {
      quantity: Entity.unmapped,
    }),
    { id: 'id', increment: { stock: 'quantity' } },
  ),
)

What it computes: a computed assignment#

compute sets a field from the row before the write and the input, in the same statement (name = <expression over name and ?>). The expression is data over operators, so the writer compiles it to SQL and the client predicts it with the same operators:

const suffixed = Expr.operator('acme.suffixed', {
  input: [Schema.String, Schema.String],
  output: Schema.String,
})

const Rebrand = Mutation.write(
  'Rebrand',
  Write.update(
    Entity.input(
      Product,
      Schema.Struct({ id: Schema.String, revision: Schema.Number, suffix: Schema.String }),
      { suffix: Entity.unmapped },
    ),
    {
      id: 'id',
      expect: 'revision',
      compute: { name: ({ row, input }) => suffixed(row.name, input.suffix) },
    },
  ),
)

• It reads the row before the write, never another assignment's result, and is refused where it is declared when it reads another Entity, writes a field another key sets, or comes to a kind its field does not store.
• The operator needs an implementation on each side that runs it: the binding's SQL table and memory table on the server, and Remote.make({ operators }) on the client (see An operator the application implements). A binding that cannot run it is refused where the write is served.
• It is held to a retry as an increment is: with expect as here, or, with none, only under a ledger where the writer commutes the operator or a guard with a revision pins the row it read.

What every row holds: an invariant#

A precondition says whether this write applies now; an invariant says what every stored row must hold, whoever writes it. With quantity = 10, reserved = 5, an update setting quantity = 3 decodes, passes every rule, and leaves a row holding more reserved than there is. An invariant is declared once on the Entity:

const StockFields = Entity.define(
  'Stock',
  Schema.Struct({ id: Schema.String, quantity: Schema.Number, reserved: Schema.Number }),
)
const Stock = StockFields.pipe(
  Entity.invariant(
    'reservedWithinQuantity',
    ({ after }) => Expr.lte(after.reserved, after.quantity),
    { message: 'Reserved stock cannot exceed the quantity', path: ['reserved'] },
  ),
)

• Judged over the row a write leaves. The writer compiles it into the same WHERE, with the fields the write sets read as their new values and each incremented field as its column moved: … and reserved <= 3. The row judged is the row written, at the version written, so a reserved raised by another request after the client's read is judged too. An insert's values are judged before it is written.
• Strictly true. A null fails it, as SQL's unknown drops a row from a WHERE. A rule that allows one says so: Expr.or(Expr.isNull(after.reserved), …).
• Not a rule. Update: [isOwner, isManager] says who may; an invariant is never one of those alternatives, so authority does not excuse an invalid row and a valid row grants no one anything. The rules speak first, so Invalid reaches only someone they let write. One over a member a Read rule hides is enforced, but its refusal names no invariant and no path.
• Repair is possible. A row already invalid is judged by the row a write leaves, so a write that fixes it lands.
• Refused before it is sent, where the client can tell. Data.mutate judges the invariants over the row the write would leave, as the store holds it. Where one is definitely broken it shows and sends nothing, and its Command answers MutationFailed with the Refusal.invalid the server would send; where the store cannot decide (a field it has not read), it refuses nothing and the server judges.
• The same declaration, everywhere it can be judged. Entity.judge(entity, { after }) is the reference; Entity.check(entity) is a Schema check; a form over an input that sets every field one reads judges it on submit and shows the message beside its path; checkConstraints(binding) (or entityChecks in the Drizzle table) gives each state invariant as a CHECK constraint, beside the field rules SQL holds exactly, which hold against handlers and raw SQL too.

What every change holds: a transition invariant#

Some rules relate two rows, each valid on its own: an order that shipped stays shipped. An invariant that reads the row before (before) as well as the row after is a transition invariant:

const OrderFields = Entity.define(
  'Order',
  Schema.Struct({ id: Schema.String, status: Schema.Literals(['placed', 'shipped']) }),
)
const Order = OrderFields.pipe(
  Entity.invariant(
    'shippedStaysShipped',
    ({ before, after }) =>
      Expr.or(Expr.not(Expr.eq(before.status, 'shipped')), Expr.eq(after.status, 'shipped')),
    { message: 'A shipped order stays shipped', path: ['status'] },
  ),
)

before is each field as the row before holds it and after each as the row after holds it. Reading before is all that makes it a transition invariant; nothing else is declared. The writer judges it beside the state invariants, in the same WHERE: the row before is the columns themselves, and after, a field the write sets is its value, one it increments its column moved, and any other unchanged. Every update is judged; a create has no row before and a delete none after. It is refused as Invalid with its id, and like every invariant it is never a guard rule, so no one is excused it. A form has no row before, so it judges none; Crud shows the server's refusal beside its path. A CHECK sees one row, so checkConstraints leaves it out, and lists it under serverOnly.

All three kinds must hold for a write to land:

authorization (Forbidden) AND precondition (Unmet) AND invariants (Invalid)

Retries: three different guarantees#

The first is an idempotent assignment, which is why the Todo examples set done = true rather than flipping it. The second is optimistic concurrency. The third is replay deduplication, and it needs an identity for the operation.

An operation id#

A Remote requestId names a request to one client only: it is a counter in the Model, so it restarts on reload, and two clients' first requests share it. Data.mutate therefore also sends an operation id, minted where the request is first sent (crypto.randomUUID(), or 128 random bits from getRandomValues on a page served over plain HTTP). A failed request keeps it, and a retry sends it again. With Data the application's Remote.make({ model, entities: [Product], mutations: [Sell] }):

const started = Data.mutate(model, Sell, { id: 'p1', quantity: -2 })
// …the request failed: send it again as itself, same input and operation.
const again = Data.retry(failedModel, started.requestId) // none unless it failed

Data.retry is Data.mutate with the failed write's own request id, input and now. The server treats the operation id as untrusted input: at most 128 characters of A–Z a–z 0–9 : . _ -, refused otherwise.

A write whose request did not go, or whose answer was no Remote answer (not JSON, or a gateway's 502), fails with Unreachable: the server may or may not have run it. Sending it again is safe exactly as far as the table below says.

A write that outlives the page: durable#

A page that reloads forgets its Model, and with it the operation ids of writes still in flight. A durable write keeps them: Data.mutate(model, Sell, input, { durable: true }) stores the write in Remote's outbox (Data.outbox) before it is sent, sends stored writes one at a time and in order, and sends one again after an Unreachable and after a reload, with the same operation id and the same now. Setup and status are in Remote's outbox section.

What the server must give it is the third row of the table above: a durable write may arrive twice, so it needs a writer with a ledger (below), or a handler that records by operation. A write sent long after it was made lies past the server's clockSkew, so the server writes its own time instead (reported as ClockSkewed). The outbox keeps each principal's queue apart, so no write is sent as anyone but who made it.

A write ledger#

A ledger records each update and insert the writer lands under the operation that asked for it and the row it wrote, atomically with the write (in its transaction, or on D1 in one batch with it). ledger is the Drizzle table below and User the principal, as in examples/writes/src/server.ts:

const ledgered = writer<Option.Option<User>>(Db.Product, {
  ledger: {
    table: ledger,
    scope: principal => Option.match(principal, { onNone: () => '', onSome: user => user.id }),
  },
})

create table write_ledger (
  scope text not null, operation text not null, target text not null,
  answer text not null, at bigint not null, request text,
  primary key (scope, operation, target)
);
create index write_ledger_at on write_ledger (at);

• scope names whose operations they are, so no one is answered with another's write: an operation id is unique only per client that minted it.
• target is the row, so an operation id sent for another row is not that row's retry.
• request is a digest of what the operation asked (its mutation, keys and input), so an operation id sent again with another request is refused rather than answered as a retry. An older ledger table gains it with alter table write_ledger add column request text; a record without one is answered as a retry until its retention passes.
• Copies sent at once. On Postgres a copy of an operation sent while another is still writing waits for it (a transaction-scoped advisory lock), then finds its record. On D1 the row and its record are written in one batch; a second copy's record collides with the first's primary key, its batch rolls back whole, and it is answered from the first's record.
• Retention, a day unless given: a retry later than that is a new operation, and an increment would be applied again. Records are pruned as new ones are made; the index on at keeps that from scanning the table.
• Updates and inserts are recorded. A retried insert is answered from its record with the row it made. Any other insert of a taken id, and without a ledger a retry too, is refused as Taken, with one answer whatever the row holds, since comparing the row with the insert would tell its asker what it holds. A retried delete finds the row gone.

A retry found in the ledger is not written again, and the guard does not decide it again: it was decided when it landed, and deciding it over a row that has moved since could refuse a write that happened. It is answered, as every write is, with the row as it now is, read back under the caller's rules.

A revision the database moves#

The guard's pin sees only changes that move the revision. A handler or raw SQL that changes the row without moving it is invisible to it. revisionTrigger is the SQL that makes the database move it on every other update too:

sqlite.exec(revisionTrigger(Db.Product, 'revision'))

It moves the revision only for an update that did not set it, so the writer's own revision = revision + 1 is not doubled, and an update that sets it to a value of its own is left as set. Run it with the migration that makes the table, on SQLite or Postgres; running it again replaces it, and a Postgres table in a pgSchema is named by its schema. The revision column must be not null: the trigger compares with =, which a null never satisfies. Not for a table Sync writes, whose applyEdits keeps one revision for two changes in one operation.

What the client shows meanwhile#

Data.mutate shows a declared update before the answer: the values it sets, and each increment as an amount. The amount is added to the value the store holds whenever the row is read, not fixed when the request was sent. So:

• a live update that reaches the store meanwhile is added to, not hidden;
• two pending increments add up, and a refused one leaves only the other's;
• a list sorted by the field places the row where the predicted sum puts it;
• a field the client has not read is not guessed: it shows the server's sum when the answer comes.

The prediction is never authority. The client cannot know who may write, and its row may be stale; the server decides, and its answer replaces the prediction. Write.reads(write) names what a write reads from its row (what when reads, each incremented field, the revision), and Write.writes(write) what it may change.

Two refusals are made at once, before anything is sent, because the store can already tell: an invariant definitely broken by the row the write would leave (Invalid, above), and a write a held may says no to (Forbidden, with the rule's explain as reason; see Guard's "What the client may do"). Each spares a round trip and decides nothing for the server, which judges every write that reaches it.

Checking the prediction against the server#

The client and the server must agree: what a pending write shows should be what the server then holds, and a write the client refuses should be one the server refuses alike. Law.check (foldkit-remote/testing) runs one declared write both ways, over a Model holding what the server sends the principal and with the same now, and compares every part the client predicted: each field, whether the row is there, each held list's order, and a refusal by its refusal. Here server is the RemoteServer.make that serves Sell over a real database (remote-drizzle's law suite runs SQLite and Postgres), principal whom it answers as, and model the application's Model before the client holds anything:

import { Law } from 'foldkit-remote/testing'

const report = Law.check(Data, {
  model,
  holds: [{ entity: Product, ids: ['p1'] }],
  mutation: Sell,
  input: { id: 'p1', quantity: -2 },
  now: 0,
}).pipe(Effect.provide(Remote.clientLayer(RemoteServer.handlers(server, principal))))

What the client left unknown is not compared, and a check that compared nothing fails, since two sides that both said nothing prove nothing. In development, Remote.make({ verifyPredictions: true }) compares each answer with what its pending write showed, and reports a disagreement as a PredictionMismatch diagnostic.