Open Standard · Working Draft
mekaniskt·kontrakt

Requests for comment  ·  RFC 0004

State reads: what does a register read mean?

The standard's flagship proof that higher-level mechanics are compositions rather than keywords - the condition precedent - rests on a read whose semantics are defined nowhere. This RFC works the problem three ways: an implicit latest-wins read, a rows-only model read through combinators, and a declared latch with values and transitions. It leans toward the latch, and says plainly what that costs.

STATUS
Open for comment
TOPICS
Condition precedent, status cells, register reads, declared transitions, retention of title, revocable permission, escalation levels

This is a request for comment, not part of the specification. The syntax is a strawman and much of it is pseudo-code; it exists to be argued with, not adopted by default.

The problem in one sentence

The condition precedent - a term that can unwind a whole deal - is specified as three primitives packaged together: a register field holds the status, a write records it, a guard reads it. The read has never been defined.

What breaks, exactly

A financed property sale declares a status register and drives it from two different clauses:

state:
  register conditions   shape { financing, inspection }

record conditions.financing = cleared     # on loan commitment confirmed
record conditions.financing = failed      # on the buyer invoking the finance clause
check  conditions.financing == cleared    # the completion gate

Three defects sit in those lines:

  1. The read is undefined. Registers are append-only, so two writes to one field are two facts and a read must mean the latest one - a rule written in no part of the standard. Authors are left to infer last-write-wins.
  2. The write verb means two things. record is defined as both append a typed row and set a field. That violates the one-thing law in the same registry that states the law.
  3. “Latest” of what? The register’s shape is {financing, inspection}. If writing one field appends a row, what does that row hold in the other field? A read must skip rows that never touched the field - which means this is a per-field key-value log wearing a register’s clothes.

And a fourth, invisible in the syntax but the first thing a lawyer notices: nothing prevents failed returning to cleared. A financing condition that has fallen must not quietly un-fall. Today the machine would bless it.

The standard has had status cells all along

Before choosing a model, notice how often the shape already appears. Every row below is a cell holding exactly one of a declared set of values, changed only by declared events, read by guards:

Where The cell Values
The finite control the contract lifecycle draft -> active <-> suspended -> expired | terminated
Escalation the escalation level none -> level 1 -> ... -> level 4
Pools stages available | reserved | disbursed, plus free names
The worked framework agreement invoice payment status one cell per register row, keyed by invoice reference
Ownership title under retention of title seller | buyer, flipped on payment confirmation
Health-record access a patient’s block on sharing revocable permission, read as a guard
Consumer and property contracts a condition precedent pending | cleared | failed
Orthogonal control regions delivery / payment / dispute tracks one cell per track

Eight instances, four different spellings, no shared vocabulary. That is the finding behind this RFC: the finite control is already a latch, and the language has never let an author declare one.

Model A - field entries plus latest-wins

Writing a field appends an entry (field, value, event); a bare read resolves to the latest entry for that field in log order. Row-shaped writes stay a distinct form, read only through aggregates.

  • Buys: the smallest possible fix. No new primitive, existing contracts parse unchanged, and the vetting gate for new primitives never has to open.
  • Costs: the write verb keeps two syntaxes; the implicit latest-wins is exactly the kind of silence this design punishes everywhere else; a status cell stays invisible on the manifest, so you cannot tell from the state block that a contract holds two conditions capable of unwinding the deal; and failed -> cleared remains expressible.

Model B - rows only, reads through combinators

Everything appends full rows. A status cell becomes a register of shape {key, value} and every read goes through the aggregate combinators: latest(conditions where key == "financing").

  • Buys: the purest data model - one meaning for the write verb, one read mechanism for all register state, no implicit anything.
  • Costs: verbose exactly where contracts are read aloud - check latest(conditions where key == "financing").value == cleared is not a clause anyone reads - and it depends on a combinator grammar that is itself still open. It inherits every manifest and transition weakness of model A while reading worse.

Model C - a declared latch

The declarator - as a table, because a transition set is a table

Tabular terms in this language are tables, and a transition set is tabular. So the value list is not declared twice - it is derived from the table:

state:
  latch financing   initial: pending
    | from    | to      | on               | by               | implements |
    |---------|---------|------------------|------------------|------------|
    | pending | cleared | loan.commitment  | party:buyer-bank | #klausul-3 |
    | pending | failed  | finance.withdraw | party:buyer      | #klausul-3 |
    | cleared | failed  | finance.withdraw | party:buyer      | #klausul-3 |

Four properties follow from that shape:

  • No duplication. The value set is the union of from and to plus initial, so there is no second list to drift. failed never appears in from, so it is terminal - absence is prohibition, the same axiom that governs ports and stored fields.
  • It reuses machinery that already exists. Table parsing, the unique-hit-policy check (no two rows sharing from and on), and the shadowed-row lint are already specified for approval tiers and cancellation ladders.
  • Every transition carries its clause. The implements column links each edge to the prose it enforces, so the coverage report and the rendering both get it for free, and a receipt can cite the transition instead of quoting text.
  • A row reads aloud as the clause. “From pending to failed, on the buyer’s withdrawal, by the buyer, under § 3.”

It draws itself

A declared transition table is a state diagram. Nodes come from the value set, edges from the rows, edge labels from on, actor badges from by, and a clause citation from implements. Colour the current node from the fold, and a dashboard shows where a deal actually stands - together with the reachable next states and who is entitled to trigger them.

Under models A and B that picture is not recoverable. A status cell assembled from scattered writes has no declared domain and no declared edges, so a renderer would have to infer the machine by static analysis of every rule touching the field: undecidable in general, wrong in practice, and silently wrong the moment a contract introduces a new value inside a branch nobody read.

This is the argument the standard already makes for ports. The capability manifest exists so that what may flow is readable without reading the rules; a declared status cell is the manifest for what state a contract can be in - and it is the artifact non-lawyers actually look at. A picture you must infer is a picture you cannot put in front of a judge.

Reads then need no convention at all: a latch has exactly one current value, folded from its declared transitions over the log. There is no implicit “latest” anywhere in the language, because nothing ambiguous is left to resolve.

check financing == cleared   else reject villkor-ej-uppfyllt
which financing is ...        # exhaustive for free: the domain is declared

The names are unresolved

The declarator. latch is precise and carries the one-way instinct, but it is electronics jargon in a document a public-sector lawyer signs. status is the word the domain already uses - an invoice is marked paid, and “the status of the financing condition” is how the clause reads. The counter-argument is that status loses the cannot-go-backwards connotation, except the transition table states that explicitly, so the connotation was never load-bearing. status is the recommendation; latch stays as the design-vocabulary word.

The transition verb. With record restored to meaning only append a row, the transition needs its own verb. set is the recommendation - the declared transition table is where the meaning lives, so the verb should stay dumb. advance is wrong for cleared -> failed, which advances nothing; flip implies two states; mark is already on the forbidden list. None of the three is obviously right, and naming a permanent verb is the cheapest mistake to make and the dearest to undo.

Keyed latches

The worked framework agreement already marks invoices paid: one status cell per register row. So latches must be declarable as a field of a shape, not only standalone:

register invoices   shape { ref: id<invoice>, amount: money,
                            payment: latch [ unpaid | paid ] initial: unpaid }
set invoices[payload.ref].payment -> paid

This carries a hard dependency: the keying syntax must be the same one keyed pools land, or the language grows two keying dialects. The latch question therefore cannot be settled ahead of the keyed-pool question.

What the linter gets - the actual argument

None of this is available under A or B, and all of it is decidable at authoring time:

  • Reachability. Can failed ever be reached? Is cleared terminal by accident? Dead transitions and unreachable values become drafting bugs caught before signing - the same class of finding as a shadowed row in a decision table.
  • No un-falling. failed -> cleared is not discouraged, it is unexpressible: the transition was never declared.
  • Exhaustive matching for free. A match over a latch needs no fallback branch, because the domain is declared.
  • Authority on the face of the state block. With an authorising party and port on each transition, what can unwind this deal, who can do it, and through which port is answerable by reading the manifest. This extends the capability-manifest property from flows to state, and it is the single strongest reason to prefer a declared latch.
  • It renders truthfully. The declared table is the state diagram, so a dashboard, the two-spine projection and a judge’s whiteboard all draw the same picture from the same signed rows.
  • Confidentiality falls out. A latch is computational by definition - rules branch on it - so the secrecy rules classify it automatically: it may be sealed from a viewer, never purged. Under model A, whether a field is computational depends on whether some rule happens to read it, which is a whole-document analysis instead of a declaration.

Side by side

A - field entries B - rows only C - latch
New core primitive no no yes
Write verb means one thing two forms, both declared yes yes
Implicit magic in reads latest-wins, implicit none none
Status cell visible on the manifest no no yes
Transition discipline no no yes
Authority per transition readable no no yes
Exhaustive matching needs a fallback needs a fallback free
Renders as a state diagram inferred, unsoundly inferred, unsoundly declared
Confidentiality classification inferred inferred declared
Depends on another open question no the combinator grammar the keying syntax
Reads aloud as a clause yes no yes

The vetting gate, answered honestly

A new primitive is admissible only when a real corpus proves no composition suffices. Model A proves a composition does suffice. So the honest case for a latch is not expressiveness - it is declarability, lintability, manifest readability and renderability - and the standard has already accepted that argument twice:

  • A pool is, in principle, a stored integer with guards. It is a primitive in fact because capacity, stages and pool-safety want to be declared and checked rather than re-derived in every contract.
  • A cadence is, in principle, a counter and a timestamp comparison. It is a primitive in fact for the same reason - and because “you may invoice once per month” is a clause, not an idiom.

A latch earns its place on exactly that precedent or not at all. If the precedent is rejected, model A is the fallback, and the standard must at minimum write down the latest-wins rule and admit that the write verb has two forms.

Honest creaks

  1. A latch kills a teaching example. The condition-precedent module exists to prove that higher-level mechanics are named compositions, not keywords. Adopt a latch and the condition precedent becomes a declaration, and that flagship composition dissolves. The standard gains a primitive and loses its best argument for restraint. Make that trade with eyes open.
  2. The core grows. Every primitive is permanent, and a latch carrying values, transitions and per-transition authority is not a small one.
  3. Unifying pool stages with latches is elegant on paper and may not survive conservation. Stages move quantities, where conservation applies and both legs are receipted; a latch moves a cell, where nothing is conserved. One mechanism at two arities reads well until the linter must decide which rules apply to which. Not in one pass.
  4. Nothing here is tested. Every other adopted mechanic in this standard arrived with a golden fixture or a green test. This one has three sketches and an argument. The reference implementation should carry the chosen model before the standard does.

This RFC is exploratory. It is published as a basis for discussion, not as normative text; where it touches the standard, the standard governs until a decision is recorded.