What every row and change must hold: invariants

A Schema judges a value, and a write's when the row before it. Neither judges the row a write leaves: with quantity = 10, reserved = 5, an update setting quantity = 3 decodes, and leaves a row that holds more reserved than there is. An invariant is what every stored row must hold, read over the row after a write (after):

import { Schema } from 'effect'
import { Entity, Expr } from 'foldkit-entity'

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

Entity.judge(Inventory, { after: { id: 'i1', quantity: 3, reserved: 5 } })
// { _tag: 'Invalid', failures: [{ id: 'reservedWithinQuantity', … }] }

One that reads the row before too (before) relates the two, each of which may be valid on its own: an order that shipped stays shipped.

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'] },
  ),
)

const shipped = { id: 'o1', status: 'shipped' }
Entity.judge(Order, { before: shipped, after: { ...shipped, status: 'placed' } })
// { _tag: 'Invalid', failures: [{ id: 'shippedStaysShipped', … }] }

What an invariant reads decides when it is judged; nothing else is declared:

reads after only   -> state invariant:      every create and update; a CHECK constraint
reads before too   -> transition invariant: every update, the only write with a row before

Entity.readsBefore(invariant) says which one is, for each of Entity.invariants(entity).

before and after hold each field as the store does, encoded, and are typed so: a date stored as ISO text is compared with ISO text (Expr.eq(after.at, '2026-01-01T00:00:00.000Z')), since a Date would never equal it.

Entity.invariant returns the step that attaches it, carrying its id and, once attached, its Entity's name as entity: an id is unique only within an Entity, so a refusal names both. A declaration attaches to one Entity; reading entity before it is attached throws. Hoist it to export it, naming the Entity's type (what it reads is checked against it), and match a refusal against it rather than spelling the id again:

export const reservedWithinQuantity = Entity.invariant<typeof InventoryFields>(
  'reservedWithinQuantity',
  ({ after }) => Expr.lte(after.reserved, after.quantity),
  { message: 'Reserved stock cannot exceed the quantity', path: ['reserved'] },
)
export const Inventory = InventoryFields.pipe(reservedWithinQuantity)

// Where a write's refusal is read (foldkit-remote):
Refusal.isInvalidBy(refusal, reservedWithinQuantity)

• before is each field as the row before holds it (Expr.field), and after each as the row after holds it (Expr.next), both typed as the field. Each is an expression already, so it goes on either side as it is; Expr.field wraps an Entity's own field, and refuses one of these:

  Write	Not
  Expr.gte(after.quantity, before.quantity)	Expr.gte(after.quantity, Expr.field(before.quantity))

• It is declared once, on the Entity's metadata, and attaching more adds to it; the Entity stays the same (Entity.same). Its interpreters read it from there.
• It reads stored rows only: one over another Entity, or reading an input, is refused where it is declared, as is an id declared twice or a path naming no field. So is one reading nothing of after: which rows a write may start from is its when. Who may write is a guard's; whether a write applies now is its when's.
• Entity.judge(entity, { after, before? }) judges rows as the store holds them (encoded) and is pure. Without before (a create) it skips transition invariants. A row holds one only when it is true: a null fails it, as SQL's unknown drops a row from a WHERE. A row without a field it reads is Undecided, never Valid.
• Entity.check(entity) is the state invariants as a Schema check over the row type (entity.schema.check(Entity.check(entity))): it encodes the value, and reports each failure at its path with its message. It throws where it is made when an invariant calls an operator its table does not run, since it could judge no value by that invariant and would pass them all.

Text compares only under a declared collation, here too: a date stored as text needs { collation: Collation.binary } on its comparison. An interpreter that judges stored rows alone refuses after's nodes as the operation next; Expr.substituteNext reads the ones a write sets as their values.