The formal shape: finite control, accumulators, cadence

3.1 Not a plain FSM - finite control PLUS accumulators

A plain finite state machine is not enough. Flood & Goodenough proved a loan agreement is a deterministic finite automaton - but a pure FSM has no memory beyond which circle you’re standing in: it cannot count. A ramavtal is nothing BUT counting: hours drawn, SEK consumed, invoices submitted this month. So the mechanical contract’s machine class is:

finite control   contract lifecycle: draft → active ⇄ suspended → expired | terminated
      +
accumulators     every quantity money flows through: pools, balances, counters,
                 cadence buckets - read by guards, changed ONLY by declared effects
      +
guards           if / which conditions over (control state, accumulators, event fields)
      +
cadences         per-port rate guards over event timestamps (3.2)
      +
receipts         output on every transition (a Mealy machine's output function)

Formal relatives, each contributing one insight:

• Petri nets / vector addition systems (Petri, 1962): places = pools, tokens = resources, transitions = events. Petri nets are the sixty-year-old mathematics of parallel draws on shared pools - many units consuming the same framework concurrently without double-counting - with decidability results (boundedness, coverability) that map directly onto “can any event sequence breach the takvolym?”.
• Counter/register machines: finite control + counters is Turing-complete when unrestricted (Minsky) - precisely what we must NOT be. The mechanical contract’s starvation diet (accumulators change only via declared effects, all guarded, no loops, no arithmetic on control flow) is what keeps every safety question decidable. The accumulators add memory without adding cleverness.
• Timed automata (Alur & Dill): clock guards on transitions - the formal home of cadence. Our variant is stricter: no running clocks, guards compare event timestamps already in the log, so determinism survives (same log, same verdicts, replayed at any speed on any machine).
• Mealy machines: the receipt is the output function - every transition emits.

The satisfying theoretical footnote: because every accumulator has a declared capacity and money is quantized (öre; hours in minutes), the state space is finite after all - the mechanical contract IS a finite machine, just one whose states are counted in pool balances rather than drawn as circles. That is why the linter’s promises (pool safety, ceiling safety, exhaustiveness) are genuinely checkable, not aspirational: they are reachability questions on a bounded system.

3.2 Cadence: rate limiting as a contract primitive

Every real contract is full of rate clauses; no contract system has them as first-class primitives. The mapping is embarrassingly direct:

The clause, in avtalssvenska	The cadence primitive
“Fakturering sker månadsvis i efterskott”	invoice.submit at-most 1 per month, not-before delivery
“Betalning 30 dagar netto”	payment.confirm due within 30 days of invoice accept
“Avrop får ske löpande under avtalsperioden”	allocation.request unlimited within validity
“Max ett uttag per dygn” (rental, staffing)	X at-most 1 per day
pay-per-call API / metered compute / energy settlement	usage.report at-most 1000 per second

Semantics: token bucket, made deterministic. The bucket is just another accumulator; “refill” is event-timestamp arithmetic, never a wall-clock read. at-most 1 per month compiles to a guard comparing this submission’s timestamp against the last accepted one - pure, replayable, and identical from per-month down to per-second. The evaluator does not know or care whether the contract breathes monthly (kommunal invoicing) or at machine speed; only the numbers differ.

Two bonuses that fall out for free:

• due within is the enforcement side of cadence: a payment that does not arrive in its window flips an obligation to breached - dröjsmålsränta (late-payment interest) becomes a computed claim instead of a forgotten right. Cadence guards both directions: too often IN, too late OUT.
• Anti-splitting: invoice splitting (many small invoices to sneak under attest thresholds or direktupphandling ceilings) stops being a detection heuristic and becomes a cadence violation - structurally rejected, like everything else in this design.

3.3 Machine-speed execution (the edge story)

“Thousands of executions per second” sounds ambitious until you look at what evaluation IS: a pure fold of if/which guards over a handful of decimal accumulators. Microseconds, no I/O. So the real constraints:

• Throughput is an ordering problem, not a compute problem. Receipts hash-chain, so authoritative acceptance needs a total order of events per contract. The solved shape: a single-writer append log per contract - boring sequencer technology comfortably does tens of thousands of appends/second, three orders of magnitude above any procurement workload and enough for machine-speed metering.
• Pre-validation is stateless and runs anywhere. Given (contract file, latest state hash), any node - an edge worker, the supplier’s own stack, a phone - computes the verdict without talking to anyone. Embarrassingly parallel; only acceptance serializes.
• The aperture this opens: the same artifact that governs a monthly-rhythm ramavtal governs machine-to-machine commerce - metered APIs, compute, energy spot settlement - where the counterparties are machines and cadence is per-second. The contract becomes the API gate; the receipt chain becomes the billing record; disputes are replays. Same primitives, same standards bindings, same boring determinism.

Honesty clause: the product wedge remains the slow economy - kommunal invoices at monthly cadence. Machine-speed commerce is not a phase, not a promise, and not on the roadmap; it is the thing this design must not PRECLUDE. Sections 3.1-3.2 are why it doesn’t: nothing in the machine class, the cadence semantics, or the receipt chain has a “per month” assumption baked in.

3.4 Scheduled money: reserve now, fall due later, anyone may claim

“Allocate now, disburse later” decomposes into three primitives - none of which hands the machine a clock:

1. reserve - the allocation, now. Pools get stages: available → reserved → disbursed. Reserving moves money between stages as the effect of an event (contract.sign, order.accept) - deterministic, replayable. This is encumbrance accounting (pre-encumbrance -> encumbrance -> expenditure, sixty years of public-sector practice), so a kommunal ekonomichef reads it on sight. A reservation may carry an expiry: not drawn within its window, it releases back - by event-timestamp math, like everything else. (§2’s allocation.request already reserves hours; money is no different.)
2. due - the schedule is an obligation, not an action. The machine never does anything at date x - it has no clock (§3.2: time enters only as event timestamps already in the log). due disburse 120_000 SEK by 2027-06-25 window 5 working-days declares an obligation that FALLS due; whether it is pending, met, or breached is a pure predicate over (contract, event log). Two trigger kinds cover every real schedule: date-due (rent, license fees, amortization rows) and event-due (milestones - “30% vid beställning, 40% vid leverans”: the obligation opens the moment the named receipt exists). And a payment plan is data: the betalplan, amortization table, or vesting schedule is a schedule artifact - a §5 lookup table (hash-referenced, effective-dated, governed) whose rows compile to obligations. A vesting schedule is literally one of these.
3. claim - anyone may wake a due obligation. Marlowe’s timeout lesson: because the outcome is deterministic, WHO pokes the contract forward is irrelevant - so poking requires no trust. In referee mode the rails execute the schedule themselves (autogiro, standing orders; ISO 20022 pain.001 carries a requested execution date - “scheduled” is already a bank-side concept) and the contract judges the resulting payment.confirm against the due window. In gateway mode a payment.claim event - from the beneficiary, or from a dumb cron - makes the contract emit payment.instruct through the out-port. Either way the scheduler is an untrusted alarm clock: claiming late changes nothing, because breach and dröjsmålsränta run from the due date in the log, not from when somebody noticed.

state:
  pool projekt.budget   capacity 400_000 SEK   stages available|reserved|disbursed

artifacts:
  betalplan   art:betalplan-bilaga-3   pin v1   sha256:1a2b...   # 30/40/30 milestone plan
              class contract-bilaga                              # §5.6: signed by the parties

rule on contract.sign:     reserve pool projekt.budget amount 400_000 SEK      # encumbrance
rule on order.accept:      due disburse 120_000 SEK from projekt.budget within 30 days  # 30%
rule on delivery.approve:  due disburse 160_000 SEK from projekt.budget within 30 days  # 40%
# the date-due shape (rent, subscriptions, amortization):
#   schedule from betalplan: each row -> due disburse row.amount by row.date

due-handling:
  satisfy  payment.confirm (iso20022) matching amount + reference  # referee mode: rails paid,
  claim    port payment.claim from supplier | any                  #   the contract judged
           -> emit payment.instruct (pain.001,                     # gateway mode: anyone-may-
                   requested-execution = due-date)                 #   wake, machine instructs
  breach   window passed -> throw payment.overdue                  # §4.2 escalation catches;
           interest per räntelagen from due-date                   #   computed from the log

Both halves of “allocate now, disburse later” are visible state, which is the quiet payoff: the reserved stage is committed-but-unpaid money (the encumbrance picture, per contract and in aggregate), and the open due obligations ARE the cash-flow forecast - “what falls due next quarter across every contract this kommun signed” becomes a pure query over signed data instead of a spreadsheet someone maintains.

Prior art, so nothing here is invented: encumbrance accounting (the reserve stages), Marlowe (contracts advance only via submitted transactions; after a timeout anyone may submit - the anyone-may-claim design), CSL/Hvitved (deadline obligations with breach as a first-class outcome, not an exception), pain.001 requested execution date + autogiro (the rails already execute schedules; we judge them rather than rebuild them), and escrow (reserve-with-expiry is escrow, generalized).

3.5 The execution model: optimistic, log-first, retry-forever (thinking ahead, prior art mapped)

There is a straight line of prior art, and the design already contains the mechanism without knowing its name. Determinism is what makes optimism free: evaluation is a pure function, so an execution attempt has no side effects to regret - losing a race costs a redo, never a wrong verdict or a torn state. The loop:

read      snapshot = fold(log up to version N)          no locks, any replica, any machine
evaluate  verdict  = rules(snapshot, event)             pure - §3.3's stateless pre-validation
apply     append event+receipt IF log head still == N   the conditional write
conflict  someone appended N+1 first -> re-fold the      cheap: fold the delta, re-evaluate,
          new events, re-evaluate, retry                 idempotency key makes retry safe

And the ETag intuition is not “something like” our design - it is ALREADY IN the receipt: state-before is the ETag. An append is accepted iff the log’s current state hash equals the receipt’s state-before; the hash chain of §2 doubles as the optimistic-concurrency token. Nothing new to add - only to name.

The prior art, each piece one insight:

• Kung & Robinson, “On Optimistic Methods for Concurrency Control” (ACM TODS, 1981): the read/validate/write loop itself, forty-five years old.
• HTTP conditional requests (RFC 7232 ETag + If-Match): the ETag intuition - optimistic concurrency as a web standard; our version is If-Match on a state hash.
• Event-store conditional appends (EventStoreDB expectedVersion, DynamoDB conditional writes): append-iff-version-unchanged against an event log - the exact mechanic, in production everywhere event sourcing lives.
• Tango/Corfu (SOSP 2013): many state machines as views over one shared log, transactions via optimistic appends with commit/abort records - many state machines on different machines as a built system.
• Calvin (SIGMOD 2012) and deterministic databases: the deep result for us - once transactions are deterministic, replicas need only agree on the LOG ORDER; state agreement follows for free, no cross-machine 2PC at apply time. The mechanical contract is deterministic by construction, so it inherits this: consensus on sequence, never on outcome.
• FoundationDB / MVCC+SSI (PostgreSQL): read-version at start, conflict detection at commit, abort-and-retry - optimistic serializability at industrial scale.

What this buys, concretely: §3.3’s single-writer sequencer stops being a special box and becomes just the thing that orders conditional appends - and evaluation scales out to any number of stateless workers, edge nodes, or the counterparties’ own machines, racing harmlessly. Within one platform’s trust domain, a multi-contract operation (draw the ramavtal pool + admit the avrop order) CAN commit atomically as a Tango-style multi-log append - two-phase commit on multiple states, done optimistically, no held locks. Across autonomous parties, §7.3 stands unchanged: sagas and compensation, because there is no shared log to conditionally append to.

Two rules keep it honest: effects only after commit (an optimistic attempt must launch nothing - out-port emissions, notifications, payment instructions all fire post-append, idempotently; an aborted attempt leaves zero trace), and external dependencies are reservations (the §3.4 reserve-with-expiry / §7.3 TCC machinery - “we basically cancel them” is the expiry auto-release, already specified). Version scoping, honestly: v1 at monthly kommunal cadence needs none of this - a single writer per contract is comically sufficient. This section exists so the machine-speed story (§3.3) has its execution model named and its prior art shelved before anyone needs it.

3.6 Signals, confirmations, and the executor as a party

The contract signals; something else executes. Three moves keep that split honest without giving the machine a clock or the design a new subsystem:

Move 1: the executor is just another party. The ERP, the bank, the payment rail - each is a counterparty with ports and obligations, exactly like the supplier. It receives instructions through an out-port; it owes acknowledgments and results through in-ports, on declared windows; it is judged, receipted, and escalated against like everyone else. The contract never trusts that a signal was executed - it holds the signed record of what was promised, what was confirmed, and what is overdue as of the last event. This is not the contract growing into an ERP by accident; it is the POETS thesis on purpose (ERP = event log + contracts as expected-transaction specs + derived reports). The contract is the kernel; executors orbit it.

Move 2: every emission opens an expectation ladder - and the rungs are already standardized. Acknowledged and executed ARE different things, and the payments world graded them decades ago: pain.001 (instruct) → pain.002 ACCP (accepted/acked) → ACSC/camt.054 (settled - money actually moved) → camt.053 (end-of-day statement, the ground truth). The document stack has the same ladder at its own levels (AS4 transport receipt → CONTRL/MLR syntax ack → application response → business outcome). So an emitted signal is never fire-and-forget; it declares its ladder:

rule on due-claim payment.claim:
  emit payment.instruct (pain.001, idempotent submission-id)
    expect ack     within 1 banking-day    satisfied-by pain.002 ACCP
                   -> else throw executor.silent           # §4.2 catches
    expect result  within 6 days           satisfied-by camt.054 credit
                   -> else throw disbursement.unconfirmed
reconcile monthly: camt.053 statement as signed artifact   # ground truth sweep:
                   unmatched entries -> throw reconciliation.mismatch

Zero new machinery in those lines: expect ... within is §3.2’s due within pointed at the executor, the throws land in §4.2’s escalation, the banking-day calendar is a §5 artifact, and the idempotent submission-id makes re-emission always safe. The singular view falls out: for every signal ever emitted, the fold answers expected / acked / executed / confirmed / overdue-as-of - every disbursement in flight, visible, per contract and in aggregate. (This is the same picture §3.4 gives for money: reserved = committed-not-paid; expectation states = promised-not-confirmed.)

Move 3: timeouts are predicates, not events - and the heartbeat is an optional cadence obligation, not a clock. “No confirmation within 6 days” never happens; it is a pure function of (log, as-of time), evaluated at the timestamp of whatever event or query comes next. State changes only on events; overdue-ness is derived, lazily, deterministically. The impulse that makes the world react stays outside and untrusted (§3.4’s alarm clock) - and for the silence-squared case (executor dead AND nobody poking), the contract may declare a liveness floor:

heartbeat:
  tick.daily     from platform  at-least 1 per day                        # liveness floor
  tick.business  from platform  at-least 1 per hour within working-hours  # window = named
                                                                          # abstraction from the
                                                                          # calendar artifact (§5)
  on tick.daily:     evaluate expectations scope invoices, dues
  on tick.business:  evaluate expectations scope resource-usage, pools    # different rhythms,
                                                                          # same machinery

Heartbeats are named, because monitoring rhythms differ: invoices once a day, resource usage hourly inside working hours - each named tick carries its own at-least cadence and optional window, where windows are abstractions (working-hours, banking-days) resolving from the §5 calendar artifact, and each tick’s liveness is guarded independently (a silent tick.business escalates even while tick.daily is healthy). And that evaluate expectations names something real: the expectation register - the derived, queryable store of everything currently open and dated: due obligations in their windows (§3.4), awaited expectation-ladder rungs, reservations approaching expiry, alert thresholds (§2’s alerts block is assertions in this same register), escalation deadlines (§4.2). It is not stored state - it is a view over the log, recomputed by the fold, so it can never disagree with the receipts.

A tick is one boring signed event per declared rhythm, platform-wide, subject to the same cadence machinery as everything else - just pointed the other way: at-least is the liveness mirror of at-most. It cannot change any outcome (a late heartbeat surfaces a breach late; the breach itself dates from the log), it is optional per contract, and a missing heartbeat is itself visible in the log and escalatable - the watchdog is watched by the same mechanism it implements. Replay stays sacred: ticks are ordinary events in the chain.

3.7 Flow: fork, join, signals, channels - concurrency without threads

The need is real, and the mathematics was already bought: §3.1’s Petri nets ARE fork/join - a transition with several output places forks, one with several input places joins; it is the sixty-year-old formalism of exactly this. What matters is what fork/join means in a machine that never executes:

• Ports ARE the channels; events ARE the signals. Both were named long ago (§1, §3.6) - “join on channels” = a guard over facts that arrived through different ports.
• Fork = one event opens many obligations. on delivery.approve: due disburse 160k within 30d; due warranty-inspection within 90d; open return-window 14d - three “parallel branches” that are nothing but three open entries in the expectation register (§3.6). No thread forked; three questions became open at once.
• Join = a conjunctive guard over the log. Generalize §3.4’s event-due from one trigger to a set: due disburse X when all-of(delivery.approve, quality.certificate, approval.grant) - the transition fires when all its input places hold a token, i.e. when all named receipts exist. any-of(...) gives the OR-join (first-of-N wins); N-of(...) gives quorum joins (multi-party consent, board approvals) for free.
• Waiting = an unfired guard, nothing more. PENDING (awaiting: {...set}) already generalizes approval and call-outs (§7.5); a waiting branch consumes nothing, runs nothing, and cannot deadlock the machine - because there is no machine running. The log stays linear; the world is what’s concurrent: parties act in parallel and their submissions interleave in log order, judged as they land.
• Orthogonal control regions. §3.1’s finite control refines the same way Harel statecharts did: a contract’s lifecycle facets (delivery-track, payment-track, dispute-track) each hold their own control state concurrently - active in delivery while level-2 in dispute - which is how real contracts actually live.

Why this stays boring where workflow engines get hairy: BPMN needs parallel gateways, token semantics, and deadlock analysis because its engine EXECUTES the flow. A referee doesn’t execute; fork is several open obligations, join is a conjunction, and the deadlock question (“can this join ever fire?”) is a Petri coverability query the linter already knows how to ask (§3.1) - dead joins and unreachable branches become authoring-time lint findings, not 3 A.M. production incidents.

Prior art: Petri nets (native fork/join, already our formal home), join calculus (Fournet & Gonthier - join patterns over channels are precisely multi-port guards; JoCaml productized it), CSP/π-calculus (channels = typed ports), BPMN AND/OR/complex gateways (the rendering vocabulary lawyers’ process people already read), van der Aalst’s workflow patterns + YAWL (the canonical catalog of split/join shapes - the checklist to test the corpus against, adopting only what real contracts demand), and Harel statecharts (orthogonal regions for the control story).

The honest residue - two things no design removes. (1) Two generals: “executed but confirmation lost” and “never executed” are indistinguishable, forever, by any protocol. The correct response is idempotent re-instruction plus periodic reconciliation against ground truth (the camt.053 sweep above) - lost confirmations are healed by retry + reconciliation, never by stronger promising. (2) Latency of truth: between events the contract knows nothing new; the heartbeat bounds that staleness at a declared cadence, it does not eliminate it. Both are properties of distributed reality, not of this design - the design’s job is to make them visible and dated rather than pretend they’re gone.