Effect State Machine: Client-Side Orchestration

The Effect State Machine is the client-side layer that sits between user actions and the network. It decides when to flush pending actions to the server, how to handle responses, and how to recover from network errors — all in a pure, verified Step function. JavaScript handles only I/O: making network calls and feeding responses back as events.

EffectState

datatype NetworkStatus = Online | Offline

datatype EffectMode =
  | Idle                          // Not currently dispatching
  | Dispatching(retries: nat)     // Sending action to server

datatype EffectState = EffectState(
  network: NetworkStatus,
  mode: EffectMode,
  client: MC.ClientState,
  serverVersion: nat
)

const MaxRetries: nat := 5

client is the verified ClientState from MultiCollaboration, holding baseVersion, present, and pending. The serverVersion field tracks the last known server version for freshness checks.

Events

Every input to the state machine is one of these events:

Event	Trigger
`UserAction(action)`	User performs an action in the UI
`DispatchAccepted(newVersion, newModel)`	Server accepted the dispatched action
`DispatchConflict(freshVersion, freshModel)`	Server rejected due to version conflict
`DispatchRejected(freshVersion, freshModel)`	Server rejected due to domain invalidity
`NetworkError`	Network request failed
`NetworkRestored`	Network reconnected automatically
`ManualGoOffline`	User explicitly went offline
`ManualGoOnline`	User explicitly went online
`Tick`	Periodic check to start a flush

Commands

The step function returns a command alongside the new state:

datatype Command =
  | NoOp
  | SendDispatch(baseVersion: nat, action: Action)
  | FetchFreshState

The JavaScript layer only executes commands — it never inspects or mutates EffectState directly.

Step function

function Step(es: EffectState, event: Event): (EffectState, Command)

The step function is pure and total. Selected transitions:

case UserAction(action) =>
  var newClient := MC.ClientLocalDispatch(es.client, action);
  var newState := es.(client := newClient);
  if CanStartDispatch(newState) then
    (newState.(mode := Dispatching(0)),
     SendDispatch(MC.ClientVersion(newState.client), FirstPendingAction(newState)))
  else
    (newState, NoOp)

case DispatchConflict(freshVersion, freshModel) =>
  if es.mode.Dispatching? then
    var retries := es.mode.retries;
    if retries >= MaxRetries then
      (es.(mode := Idle), NoOp)     // pause; next Tick retries with fresh count
    else
      var newClient := MC.HandleRealtimeUpdate(es.client, freshVersion, freshModel);
      var newState := EffectState(es.network, Dispatching(retries + 1), newClient, freshVersion);
      (newState, SendDispatch(freshVersion, FirstPendingAction(newState)))
  else
    (es, NoOp)

case NetworkError =>
  (es.(network := Offline, mode := Idle), NoOp)

A dispatch can be triggered by UserAction, DispatchAccepted (when more pending exist), NetworkRestored, ManualGoOnline, or Tick. CanStartDispatch is:

function CanStartDispatch(es: EffectState): bool {
  IsOnline(es) && IsIdle(es) && HasPending(es)
}

Invariant

predicate ModeConsistent(es: EffectState) {
  es.mode.Dispatching? ==> HasPending(es)
}

predicate RetriesBounded(es: EffectState) {
  es.mode.Dispatching? ==> es.mode.retries <= MaxRetries
}

predicate Inv(es: EffectState) {
  ModeConsistent(es) && RetriesBounded(es)
}

ModeConsistent ensures that dispatching mode always has pending actions to dispatch. RetriesBounded ensures retries never exceed MaxRetries.

Proved properties

StepPreservesInv — all transitions preserve the invariant

lemma StepPreservesInv(es: EffectState, event: Event)
  requires Inv(es)
  ensures Inv(Step(es, event).0)

Proved by case analysis on all eight event variants. Every branch either goes to Idle (satisfying ModeConsistent trivially) or only sets Dispatching when HasPending is confirmed.

RetriesAreBounded — retries never exceed MaxRetries

lemma RetriesAreBounded(es: EffectState, event: Event)
  requires Inv(es)
  ensures RetriesBounded(Step(es, event).0)

Only DispatchConflict increments retries, and it checks retries >= MaxRetries before doing so. When max is hit, the mode goes Idle.

TickStartsDispatch — Tick initiates dispatch when eligible

lemma TickStartsDispatch(es: EffectState)
  requires Inv(es)
  requires IsOnline(es) && IsIdle(es) && HasPending(es)
  ensures Step(es, Tick).0.mode.Dispatching?
  ensures Step(es, Tick).1.SendDispatch?

When the client is online, idle, and has pending actions, a Tick always starts dispatch. This enables the retry-after-max-retries pattern: go idle, wait for Tick, retry with fresh retry count.

MaxRetriesLeadsToIdle — conflict at max retries transitions to Idle

lemma MaxRetriesLeadsToIdle(es: EffectState, freshVersion: nat, freshModel: Model)
  requires es.mode.Dispatching? && es.mode.retries >= MaxRetries
  ensures Step(es, DispatchConflict(freshVersion, freshModel)).0.mode.Idle?

Bounded immediate retries prevent hammering the server. The action remains in pending and will be retried on the next Tick.

PendingNeverLost — pending actions are never arbitrarily lost

lemma PendingNeverLost(es: EffectState, event: Event)
  requires Inv(es)
  ensures var (es', _) := Step(es, event);
          match event {
            case UserAction(_)          => PendingCount(es') >= PendingCount(es)
            case DispatchAccepted(_, _) => PendingCount(es') >= PendingCount(es) - 1
            case DispatchRejected(_, _) => PendingCount(es') >= PendingCount(es) - 1
            case DispatchConflict(_, _) => PendingCount(es') == PendingCount(es)
            ...
          }

The count invariant: UserAction grows pending, DispatchAccepted/DispatchRejected remove at most one, and all other events leave pending unchanged.

PendingSequencePreserved — exact sequence equality on accept/reject

lemma PendingSequencePreserved(es: EffectState, event: Event)
  requires Inv(es)
  requires es.mode.Dispatching?
  requires event.DispatchAccepted? || event.DispatchRejected?
  ensures var (es', _) := Step(es, event);
          Pending(es') == Pending(es)[1..]

Not just a count bound: the remaining pending sequence is exactly pending[1..]. The dispatched action is removed and the rest are preserved in order.

ConflictPreservesPendingExactly — conflict leaves pending unchanged

lemma ConflictPreservesPendingExactly(es: EffectState, freshVersion: nat, freshModel: Model)
  requires Inv(es)
  requires es.mode.Dispatching?
  ensures var (es', _) := Step(es, DispatchConflict(freshVersion, freshModel));
          Pending(es') == Pending(es)

A conflict does not remove any action from pending. The action is retried after rebasing to the fresh server state.

UserActionAppendsExact — user action appends the exact action

lemma UserActionAppendsExact(es: EffectState, action: Action)
  requires Inv(es)
  ensures var (es', _) := Step(es, UserAction(action));
          Pending(es') == Pending(es) + [action]

The action is appended at the end of pending in both the optimistic-success and optimistic-failure cases.

System properties

EffectSystemProperties.dfy proves four system-level properties over sequences of events:

NoSilentDataLoss — actions never disappear without being processed

lemma NoSilentDataLoss(es: EffectState, action: Action, events: seq<Event>)
  requires E.Inv(es)
  requires action in E.Pending(es)
  ensures var es' := ApplyEvents(es, events);
          action in E.Pending(es') || ActionWasProcessed(es, events, action)

Every action in pending either remains in pending or is explicitly processed (accepted or rejected while at position 0 in dispatching mode). There is no case where an action silently disappears.

UserActionEntersPending — user actions are captured

lemma UserActionEntersPending(es: EffectState, action: Action)
  requires E.Inv(es)
  ensures var (es', _) := E.Step(es, E.Event.UserAction(action));
          action in E.Pending(es')
          && E.Pending(es') == E.Pending(es) + [action]

A user action is always captured in pending immediately, regardless of network state.

FIFOProcessing — actions are processed in order

lemma FIFOProcessing(es: EffectState, event: Event, i: nat)
  requires E.Inv(es)
  requires 0 < i < |E.Pending(es)|
  ensures var (es', _) := E.Step(es, event);
          E.Pending(es)[i] in E.Pending(es')

Only the first pending action can leave the queue. Actions at position i > 0 are never removed by any event except by first becoming position 0.

OnlineIdlePendingMakesProgress — system makes progress

lemma OnlineIdlePendingMakesProgress(es: EffectState)
  requires E.Inv(es)
  requires E.IsOnline(es) && E.IsIdle(es) && E.HasPending(es)
  ensures var (es', cmd) := E.Step(es, E.Event.Tick);
          cmd.SendDispatch?

When the system is in the right state, a Tick always produces a SendDispatch command. This connects the bounded retry mechanism to eventual progress.

Retry design

The retry design provides two layers of protection:

Bounded immediate retries — DispatchConflict retries up to MaxRetries (default 5) times, rebasing each time.
Persistent eventual retry — after exceeding MaxRetries, the mode goes Idle but the action stays in pending. The next Tick resets retries to 0 and tries again.

This prevents hammering the server under sustained contention while ensuring the action is never abandoned.

Integration boundary (trusted)

Mapping browser/network events to EffectStateMachine events
Actual I/O execution of SendDispatch and FetchFreshState commands
End-to-end liveness assumptions (fairness of Tick delivery)

Multi-Collaboration kernel

The ClientState that the Effect State Machine wraps.

Multi-Project kernel

Extends the Effect State Machine to multi-project operations.

CollabTodo app

Full example of the Effect State Machine with Supabase or Cloudflare.

React integration guide

How to wire the Effect State Machine into a React app.

Introduction

Kernels

Building with dafny-replay

Example Apps

Backend Integration

Reference

Effect State Machine: Client-Side Orchestration

EffectState

Events

Commands

Step function

Invariant

Proved properties

System properties

Retry design

Integration boundary (trusted)

Multi-Collaboration kernel

Multi-Project kernel

CollabTodo app

React integration guide

Build docs developers (and LLMs) love

Introduction

Kernels

Building with dafny-replay

Example Apps

Backend Integration

Reference

Documentation Index

​EffectState

​Events

​Commands

​Step function

​Invariant

​Proved properties

​System properties

​Retry design

​Integration boundary (trusted)

​Related pages

Multi-Collaboration kernel

Multi-Project kernel

CollabTodo app

React integration guide

Build docs developers (and LLMs) love

EffectState

Events

Commands

Step function

Invariant

Proved properties

System properties

Retry design

Integration boundary (trusted)

Related pages