Back to Dyad

Correct State Machines by Construction — Unified Plan

plans/correct-state-machines.md

1.10.061.7 KB
Original Source

Correct State Machines by Construction — Unified Plan

Generated by a swarm planning session on 2026-07-28

Status: Proposed

Evidence window: First-parent merges after 1014afff63622100bbf2e8a76fb536afc8cb9c88 through 9d4b4d2 on main

Source plans: plans/claude-correct-state-machines.md and plans/codex-correct-state-machines.md

Decision

The Codex plan is the better plan overall. It has the accurate evidence set, the stronger assurance boundary, the better conformance model, safer compatibility strategy, clearer renderer semantics, and more credible persistence sequencing.

The Claude plan is the better compact mechanics checklist. Its two-phase fence, non-creating producer handle, rendered-revision discipline, canonical fingerprinting, envelope-budget test, typed refusal handling, and concrete failure taxonomy sharpen the implementation.

Neither should be adopted unchanged:

  • The Codex plan is too broad. A monolithic MachineSpec, universal lifetime substrate, full ActorHost representation rewrite, generated renderer bindings, and eighteen-PR rollout would create a second framework before its first primitives are proven.
  • The Claude plan still leaves ordinary authors composing many temporal primitives manually. Some proposed enforcement is incomplete or unsound, notably afterCommands, automatic rendered-revision inference, field-name identity heuristics, and a universal remote manager.

The unified direction is therefore:

Keep Codex's evidence, assurance model, compatibility posture, conformance, and pilot discipline. Replace its broad framework with layered contracts and five narrow mechanisms. Import Claude's strongest concrete mechanics. Commit to a bounded MVP with two vertical pilots and a stop/go decision before routing, durability, or chat work.

Comparison

DimensionClaude planCodex planUnified choice
EvidenceRich examples, but says “~150” findings and mixes pre-baseline PRs into the stated waveExact 21-merge, 169-commit, 256-thread inventory with methodology and linksCodex evidence
DiagnosisExcellent E1–E11 failure taxonomyEqually strong mapping from failures to missing guaranteesCombine and condense
AssuranceSometimes says an API makes a failure unrepresentable when ordering or inventory is still requiredSeparates type, runtime, finite-model, and domain-owned guaranteesCodex boundary
AuthoringTwelve sibling primitives remain visible to authorsOne recipe/facade path, but too much in one MachineSpecThin index over layered contracts
Host lifecycleAdds a concrete fence without replacing the hostProposes a risky lifetime-map rewriteAdd a host gate; preserve internals
OperationsNarrow waiters, but not the full safe request boundaryOversized OperationScope owns many resource kindsTwo-stage request handle plus narrow admitted OperationRegistry
RendererBetter receipts but callers still assemble bootstrap, admission, completion, and presentationGenerated handle/hook has the right UX but is prematureShared handwritten typed helper; generate later if pilots converge
Remote lifecycleOne broad createRemoteManagerGenerated subscription/action facadeExtend the client with a subscription lease; keep domain managers
TestingUseful named conformance cases and envelope budgetsTiered conformance, historical mutants, leak accounting, explicit boundsCodex tiers plus Claude's concrete helpers
PersistenceGeneralizes claim/CAS/checkpoints too earlyFixes the known bug now and pilots executable durability laterCodex sequencing
RolloutEight nominal PRs, several containing multiple risky domain migrationsEighteen narrow PRs, but too long-lived a partial migrationEight logical MVP stages, split into narrow PRs when needed
Success“Materially fewer iterations” is not measurableBetter metrics, but pilot refactors are not comparable to authority migrationsPilot safety/glue gates plus normalized future churn

Claude elements retained

  • Two-phase deletion/reset fences: drain declared cleanup, then seal through the destructive commit.
  • A captured non-creating actor sink for late producers.
  • Explicit conflict and observed-revision policy for mutations.
  • Canonical dispatch-address fingerprints and settlement-aware receipt retention.
  • assertEnvelopeBudget using the actual codec and structured-clone measurement.
  • Typed authorization decisions and distinct refusal/failure channels.
  • Concrete review-derived adversarial cases.

Claude elements rejected or changed

  • afterCommands: rejected. The current scheduler promise means handoff, not completion of async commands, emitted terminal events, or compensation. Route cleanup must follow authoritative operation settlement.
  • Automatic rendered-revision stamping: rejected. The client knows its latest received revision, not which revision a component rendered. The hook must capture an explicit observed-revision token.
  • createRemoteManager: deferred. Common subscription mechanics belong in RemoteMachineClient; domain managers keep their product-specific surfaces.
  • Schema field-name identity checks: rejected. appId/chatId heuristics are brittle. Use entity-relative intents or an explicit key/intent relationship contract.
  • Generic durable claim/CAS state machine: deferred. GitHub claims, plan handoff, and chat queue ownership have different durable authorities.

Codex elements narrowed or deferred

  • MachineSpec becomes a thin index over layered production contracts and a separate test-only conformance sidecar.
  • The universal LifetimeLease becomes three concrete MVP mechanisms: KeyedAdmissionGate, RemoteSubscriptionLease, and PendingReceiptLedger.
  • OperationScope becomes a two-stage request protocol: a pre-admission request handle plus a narrow admitted OperationRegistry that composes existing TaskScope, TimerLeaseScope, and later route/subscription leases.
  • The full ActorHost lifetime-slot rewrite is deferred. The MVP integrates one final admission gate around the reviewed host implementation.
  • Generated server/client/renderer code is deferred. Two pilots first use one shared handwritten typed helper behind existing domain façades.
  • Full JSON schedule minimization, a graphical inspector, route backfill, durability, chat, and transition-table syntax are follow-ups.

Summary

The pure transition layer held up. The churn occurred in implicit protocols around it: admission across await, construction/disposal, request settlement, subscription ownership, deletion fences, retry/deduplication, late producer output, presentation routing, and persistence.

The MVP will make framework-owned admission, lifetime, receipt, and in-process settlement invariants unavailable through the normal API for two migrated pilot surfaces. It will use deterministic adversarial tests for properties TypeScript cannot prove, while preserving current IPC envelopes, renderer façades, and product behavior.

The MVP does not claim crash-safe arbitrary side effects or prove domain policy. It ends with a stop/go decision. Presentation backfill, generic durability, and chat/queue work proceed only if the pilots reduce glue, kill the historical failure shapes, preserve behavior, and remain understandable to authors.

Evidence

Reproducible scope

The authoritative sample is the 21 first-parent merges after the requested baseline:

sh
git log --first-parent \
  1014afff63622100bbf2e8a76fb536afc8cb9c88..9d4b4d2

GitHub review-thread counts are a 2026-07-28 snapshot. Top-level review threads are counted once; replies are analyzed separately. Review can continue after merge, as demonstrated by the newest version-preview recovery finding.

EvidenceCount
First-parent merges21
Commits169
Top-level review findings256
HIGH/P1 findings70
MEDIUM/P2 findings185
State-machine-program findings after excluding unrelated #4124252
Findings in the five main migrations192
Commits in the five main migrations95
Foundation findings in #4097–#410646
New rules/state-machines.md bullets since baseline47

The five main migrations—#4108 app run, #4116 GitHub operations, #4121 image generation, #4119 chat/plan, and #4123 version preview—account for 75% of all findings.

PRCommitsFindingsDominant churn
#41001414construction, reentry, disposal, retention
#4105910authorization, dedupe, subscriptions
#41081431request/runtime identity, waiters, deletion
#4116511claims, routing, reset
#41211019effects, UI admission, deletion, retention
#41195096queue ownership, settlement, finalization
#41231635persistence, Git recovery, window interest

The Claude plan's broader chronology is useful background, but PRs such as #4086, #4090, #4092, #4093, and #4095 are not in the requested post-baseline first-parent set. Its “~150” figure should not be used as the program baseline.

What the evidence says

The foundation's 46 findings break down as:

Primary causeFindings
Actor/subscription lifetime, admission, and disposal barriers17
Identity, correlation, authorization, and deduplication9
Retention, backpressure, and resource ownership8
Cross-window projection and delivery compatibility5
Error isolation and classification4
Abort and terminal-settlement semantics3

Only six of thirteen inventoried machine directories currently use shared matrix/reachability drivers. Only three of six distributed definitions have reachability coverage, and no domain machine uses runCosim.

The conclusion is not that review was noisy. At least 123 of 139 replies to findings explicitly said “Fixed” or “Addressed,” while only five were clearly rebutted or intentional by conservative phrase matching. Review was discovering real protocol defects after implementation.

Problem statement

Correctness-critical state is still encoded in maps, promises, callbacks, authorizers, renderer hooks, and destructive handlers surrounding otherwise explicit reducers.

The same implicit protocols are repeatedly reimplemented:

  • an async authorization lease;
  • a subscription generation;
  • a delivery receipt and dedupe record;
  • a request waiter and replay cursor;
  • a deletion/reset tombstone;
  • a command continuation lifetime;
  • an initiating-window route; and
  • a durable checkpoint/claim.

The documented invariant is not enough if an author can bypass it through a normal API. Review then becomes the mechanism that discovers missing ordering, identity, and cleanup edges.

The goal is:

Make framework-owned protocol invariants structural for migrated surfaces, require domain policy to be explicit, and turn review-discovered interleavings into reusable deterministic conformance.

Assurance boundary

“Correct by construction” has four distinct levels.

Type and contract guarantees

For migrated surfaces:

  • Renderer RemoteIntent is structurally distinct from trusted internal Event.
  • Sender/session provenance is main-derived.
  • Delivery message, idempotency, request, runtime invocation, actor revision, domain revision, and window session roles are not conflated.
  • Every intent declares:
    • authorization and key relationship;
    • admission-only versus tracked completion;
    • observed-revision requirements;
    • retry/idempotency policy;
    • authoritative UI acceptance milestone;
    • refusal mapping; and
    • wire/snapshot budgets.
  • Every correlated effect handler declares success, failure, and cancellation output.
  • Applicable conformance tiers and explicit exclusions are registered.

In-process runtime guarantees

For migrated surfaces:

  • Subscribe and dispatch use different single-use preparations. A prepared subscribe is bound to the untrusted encoded address, window/host generation, and key-slot reservation; a prepared dispatch is additionally bound to the admitted subscription, canonical key, and actor instance/revision.
  • Object keys are interned/canonicalized only after subscription authorization.
  • Final subscribe or dispatch admission consumes its preparation synchronously.
  • A fence publishes before its first await.
  • Every external ingress encounters the same final key/machine/host gate.
  • A stale release cannot release a newer subscription or fence generation.
  • Refresh/resync cannot acquire another subscription reference.
  • Unresolved receipt and operation entries are never evicted.
  • A client/pre-admission request handle registers synchronously before IPC or authorization. The authoritative actor operation is created atomically only when final admission accepts the intent.
  • Each admitted in-process operation settles at most once; disposal settles every unresolved admitted operation.
  • Late producer output uses a captured non-creating sink and cannot resurrect a deleted actor.

These guarantees end at the declared process, host, actor, or window-session lifetime. An in-memory ledger does not provide exactly-once behavior across process crashes.

Deterministic test evidence

  • Finite declared variants are checked for totality and reachability.
  • Async authorization, bootstrap, disposal, reentry, duplicate, retry, and capacity interleavings are systematically injected.
  • A test reports whether exploration was exhaustive or hit its bound.
  • Terminal/disposal scenarios assert zero owned waiters, tasks, timers, subscriptions, routes, and actor references.
  • Persistent crash/recovery and cross-machine cosimulation are required only after those assurance tiers exist.

Explicitly domain-owned

The framework does not generically prove:

  • scheduling, supersession, staleness, or retry eligibility;
  • the product meaning of ignored, refused, cancelled, or superseded work;
  • exactly-once Git, filesystem, database, network, or provider effects;
  • compensation correctness after a partially applied side effect;
  • correctness over an unbounded payload/state domain; or
  • crash safety before a persistent machine adopts the durable tier.

Domains must declare and test these policies. The framework must not infer them.

Product and developer principles

This framework work follows the repository product principles:

  • Intuitive but power-user friendly: ordinary authors use a small contract plus safe façades; low-level escapes are named, inventoried, and tested.
  • Transparent over magical: admission, refusal, execution, and settlement are distinct; retries and stale writes are never hidden defaults.
  • Productionizable: lifecycle and recovery behavior is explicit, bounded, observable, and compatible with real renderer/process failure.
  • Backend-flexible: shared persistence/effect contracts do not encode Git, SQLite, Electron renderer, or provider-specific policy.
  • Bridge, don't replace: keep the existing pure reducers, dispatcher, managers, IPC, and renderer APIs; add enforcement around their unsafe seams.
  • Delightful: refused work preserves input, errors are actionable, and spinners/panes do not become stuck or lie about authoritative state.

Scope

Core MVP

  1. Immediate #4123 interrupted-restore regression and focused safety fix.
  2. Exact finding/inventory catalog and layered conformance registration.
  3. PendingReceiptLedger, adopted by remote transport and MCP OAuth.
  4. RemoteIntentContract, trusted-event conversion, typed authorization, transport-private PreparedSubscribe/PreparedDispatch, and RemoteSubscriptionLease.
  5. Host-integrated KeyedAdmissionGate with two-phase fence semantics and non-creating producer sinks.
  6. Two-stage request handling: a pre-admission PreparedRequest, narrow admitted OperationRegistry, safe actor.request() facade, and an optional post-commit transition outcome channel.
  7. Minimal one-shot defineEffectHandlers.
  8. Shared handwritten useMachineMutation behind existing renderer façades.
  9. App-run and image-generation vertical pilots.
  10. Migrated-surface enforcement, compatibility checks, and a stop/go report.

Conditional follow-up

In order:

  1. Main-only OperationRouteRegistry and version-preview window-interest ownership.
  2. Remaining remote-intent migrations; add a manager recipe only if concrete lifecycle duplication remains after lease adoption.
  3. Checkpoint-before-effect persistence on version preview, then plan handoff.
  4. A narrow chat/plan owned-queue protocol and required composition cosims.
  5. Full unsafe-API removal and remaining machine backfill.
  6. Optional generated renderer bindings, host lifetime representation refactor, property-based expansion, or transition-table helper when evidence supports them.

Explicitly out of the MVP

  • Full ActorHost lifetime-map rewrite.
  • Universal lifetime or workflow scope.
  • Shared remote-manager superclass/generator.
  • Generated renderer source/bindings.
  • Global route-table migration.
  • Generic crash-safe persistence or durable dedupe.
  • Generic durable claim/CAS workflow.
  • Chat/plan queue abstraction.
  • Full machine backfill.
  • Transition-table DSL.
  • Property-testing dependency.
  • Graphical state-machine inspector.
  • Database migration.

Unified technical design

1. Layered contracts, one thin index

Do not ship one deeply generic object that owns transitions, wire protocol, lifecycle, effects, outcomes, persistence, test fixtures, and renderer code.

Use composable layers:

  • RemoteIntentContract<Key, Intent, Event, Snapshot>
  • a small lifecycle/admission declaration;
  • optional EffectContract<Command, Event>;
  • optional OutcomeContract<RequestId, Outcome>; and
  • test-only MachineConformance.

A thin defineMachine(...)/manifest may index these layers for inventory and review output. It does not own runtime behavior and does not put fixtures into production bundles.

Conceptual shape:

ts
const remote = defineRemoteIntentContract({
  keyCodec,
  intentCodec,
  snapshotCodec,
  intents: {
    START: {
      completion: "tracked",
      revision: "required",
      retry: "none",
      acceptance: "admission",
      inputDisposition: "preserve-until-accepted",
    },
  },
  authorizeSubscribe,
  authorizeDispatch,
  toInternalEvent,
  budgets,
});

export const definition = defineDistributedMachine({
  ...existingDefinition,
  remote,
  lifecycle,
  outcomes,
  effectHandlers,
});

export const conformance = defineMachineConformance({
  definition,
  states,
  intents,
  invariants,
  faultScenarios,
  exclusions,
});

The MVP contract must declare only facts that generate enforcement or tests. Add new declarations after pilot evidence, not in anticipation of every future machine.

2. Remote intent, provenance, and revision contracts

Split the renderer's wire type from the actor's internal event:

ts
interface RemoteIntentContract<Key, Intent, Event, Snapshot> {
  keyCodec: z.ZodType<Key>;
  intentCodec: z.ZodType<Intent>;
  snapshotCodec: z.ZodType<Snapshot>;
  authorizeSubscribe(
    context: SubscribeAuthorizationContext<Key>,
  ): AuthorizationDecision | Promise<AuthorizationDecision>;
  authorizeDispatch(
    context: DispatchAuthorizationContext<Key, Intent>,
  ): AuthorizationDecision | Promise<AuthorizationDecision>;
  toInternalEvent(context: AdmittedIntentContext<Key, Intent>): Event;
  policy(intent: Intent): IntentPolicy;
  budgets: EnvelopeBudgets;
}

Requirements:

  • Prefer entity-relative intents. If an intent repeats identity, require an explicit relationship function and mismatched conformance fixtures.
  • toInternalEvent creates a new immutable trusted event. It never mutates the decoded renderer object.
  • Producer/completion events are not in the renderer codec.
  • Main derives window/session provenance from the IPC sender.
  • Expected authorization denial returns { kind: "deny", error: DyadError }.
  • Unexpected authorization/dependency/programming failure throws and remains telemetry-visible.
  • The current protocol v1 and messageId remain compatible.

Observed revision

RemoteMachineClient cannot infer what React rendered. A renderer hook returns an opaque token beside the selected view:

ts
const { view, observedRevision } = useDistributedMachine(...);

await mutate(intent, {
  expected: observedRevision,
});

The intent contract declares whether actor revision, a domain revision such as queue revision, or no revision is required. There is:

  • no fallback to the client's newer hidden snapshot;
  • no generic allowStaleWrite; and
  • no automatic conflict retry.

An intent may explicitly implement resync/recheck/retry with one stable prepared identity when its domain policy says that is safe.

Fingerprint and envelope budget

Add:

  • canonicalDispatchFingerprint(contract, address, intent), computed in main over the protocol version, machine identity, canonical encoded wire address, codec-parsed immutable intent, expected revision token, RequestId, and declared idempotency identity;
  • exclusion of main-injected sender/session metadata from the payload fingerprint;
  • verification rather than trust of any renderer-supplied digest; and
  • assertEnvelopeBudget(contract, worstCaseFactory) using the actual codec and structured-clone-compatible measurement.

The dispatch messageId is the ledger key and the window session is the ledger scope; neither is duplicated inside the fingerprint. Mutable facts such as the current actor instance are admission bindings, not retry payload identity. Volatile main-injected provenance is also excluded.

Apply the untrusted envelope byte bound before codec traversal or hashing. Hash large payloads only once per prepared delivery and store only the digest in ledgers.

3. PendingReceiptLedger

Extract the data structure independently implemented in remote transport and MCP OAuth:

ts
ledger.claim({
  scope: windowSessionId,
  messageId,
  fingerprint,
  start: () => admit(),
});

Outcomes:

  • fresh;
  • duplicate/replay;
  • same-ID payload conflict;
  • in-flight capacity rejected; or
  • transient pre-admission failure.

Guarantees:

  • unresolved entries are pinned;
  • in-flight capacity is separate from settled-history capacity;
  • settled retention starts when the result settles;
  • capacity pressure rejects new admission rather than evicting live entries;
  • same identity with a different authoritative fingerprint conflicts;
  • transient pre-admission transport-lifetime failures are removed only after settlement;
  • old continuations compare entry identity before deleting; and
  • the renderer reuses one prepared message ID for an allowed retry.

This ledger owns delivery idempotency within its declared session/host lifetime. It does not own domain request completion and is not durable across restart.

4. Prepared subscribe/dispatch and subscription ownership

Subscription creation and event dispatch have different prerequisites and must not share one universal preparation capability.

Both PreparedSubscribe and PreparedDispatch are framework-private, single-use values.

Subscribe flow

A new subscription has no actor instance/revision yet:

  1. Bound and decode the envelope without interning an object key.
  2. Reserve pending quota/key-slot ownership by canonical encoded address.
  3. Capture the window session plus host, machine, and gate generations.
  4. Await typed subscription authorization over the decoded, uninterned address.
  5. Revalidate the sender, pending attach identity, quota reservation, and captured generations.
  6. Only now intern/canonicalize the object key, recheck the final keyed gate, and construct or retain the actor.
  7. Consume PreparedSubscribe at final synchronous subscription admission.

Rejected untrusted IDs never enter a process-lifetime interner.

Dispatch flow

Remote dispatch addresses an existing actor established by an admitted subscription:

  1. Bound and decode the complete immutable dispatch address and intent.
  2. Resolve the canonical actor through that subscription.
  3. Capture window session, actor instance/revision, gate generation, dispatch fingerprint, and expected observed revision.
  4. Await typed dispatch authorization.
  5. Revalidate every captured fact.
  6. Create an immutable trusted internal event.
  7. Consume PreparedDispatch at final synchronous ActorHost admission.

If any captured fact changed, admission returns a typed refusal. It never silently subscribes or dispatches against a successor lifetime.

RemoteSubscriptionLease

Extend RemoteMachineClient with:

ts
interface RemoteSubscriptionLease {
  readonly ready: Promise<void>;
  refresh(): Promise<void>;
  release(): void;
}

Guarantees:

  • retain increments ownership once;
  • refresh() never acquires ownership;
  • release is idempotent and generation-bound;
  • failed bootstrap is retryable and not cached forever;
  • unsubscribe/window destruction/disposal invalidates pending authorization;
  • bootstrap-before-dispatch is enforced where dispatch cannot create;
  • in-flight completion can retain the subscription through terminal delivery; and
  • React Strict Mode replay cannot release a replacement generation.

Keep app-run, chat, and plan managers. They compose the lease while preserving their domain APIs.

5. KeyedAdmissionGate

Integrate one gate at the final ActorHost ingress without replacing its reviewed lifetime maps.

ts
interface KeyedAdmissionGate<Key, Event> {
  beginFence(options: {
    key: Key;
    allowDuringDrain(event: Event): boolean;
  }): FenceHandle<Key>;

  assertCreateAllowed(key: Key): void;
  assertDispatchAllowed(key: Key, event: Event): void;
  track<Result>(key: Key, start: () => Promise<Result>): Promise<Result>;
}

Fence lifecycle:

  1. Draining: published synchronously before the first await; admits only declared cleanup/cancellation events.
  2. Sealed: admits nothing after the actor and continuations quiesce.
  3. Committed: destructive domain work succeeded; disposal and waiter settlement finalize.
  4. Aborted/reopened: destructive work failed; only the generation-bound fence handle can reopen admission and request client resync.

The fence remains held through the domain's database/filesystem destructive commit. The host cannot infer whether that operation succeeded.

The gate applies to:

  • subscription-driven creation;
  • remote dispatch;
  • legacy handler/main-service dispatch;
  • local actor refs;
  • command/timer/producer ingress; and
  • actors whose synchronous construction began before the fence.

Command runners and external producers receive a captured non-creating sink bound to the expected actor instance. They cannot call a creating ensure(). The fence drain includes the full admitted command continuation and terminal events it synchronously creates.

6. Two-stage requests and authoritative outcomes

A remote request spans a pre-admission lifetime in the client/transport and an authoritative admitted lifetime in main. No actor-owned registry can exist before authorization without either touching or creating unauthorized actor state.

Client/pre-admission PreparedRequest

actor.request(intent) synchronously creates a client request handle before it starts IPC:

ts
interface PreparedRequest<Admission, Outcome> {
  readonly requestId: RequestId;
  readonly admission: Promise<Admission>;
  readonly settled: Promise<Outcome | NotAdmitted>;
  readonly retry:
    | { kind: "disabled" }
    | { kind: "enabled"; dispatch(): Promise<Admission> };
}

It owns:

  • stable RequestId, transport message ID, and declared idempotency identity;
  • local admission/refusal/disconnect settlement;
  • retry with the same immutable dispatch identity; and
  • invalidation when the client/window lifetime ends.

It is not authoritative domain state. Refusal creates no actor operation. Renderer loss cannot prevent main-owned work that was already admitted from settling.

Main admitted OperationRegistry

At final synchronous actor admission, main atomically creates or reattaches the authoritative operation entry before enqueuing the trusted event:

ts
class OperationRegistry<RequestId, Outcome> {
  admit(id: RequestId, actor: ActorInstanceId): OperationTicket<Outcome>;
  settle(id: RequestId, outcome: Outcome): boolean;
  dispose(outcome: Outcome): void;
}

It owns only:

  • distinct RequestId;
  • accepted actor instance/revision;
  • atomic admission-before-enqueue registration;
  • exactly-once in-process settlement;
  • unresolved-entry pinning;
  • optional bounded settled replay; and
  • typed disposal settlement.

It composes existing TaskScope and TimerLeaseScope; it does not absorb tasks, timers, routes, subscriptions, persistence, or presentation.

The ordinary facade remains:

ts
const operation = actor.request(intent);
const admission = await operation.admission;
const outcome = await operation.settled;

For local actors, client preparation and admitted registration can occur in one synchronous call. For remote actors, transport admission bridges the two stages. A duplicate stable request reattaches to or replays the same admitted operation; a refused request never appears in the main registry.

actor.enqueue() remains explicitly admission-only and is unavailable to new domain completion-aware code.

Request identity is distinct from reusable runtime InvocationRef. A domain may deliberately relate them through a named mapping, not a cast or shared generic string.

Post-commit outcome channel

Prototype a backward-compatible optional outcome field on changed transition results:

ts
change(nextState, commands, {
  outcomes: [complete(requestId, outcome)],
});

ActorHost publishes outcomes after snapshot commit. The default generic is never, so existing machines remain source-compatible.

Do not settle operations from arbitrary observers, scheduler handoff, or a new afterCommands phase. Effects emit correlated terminal events; the pure transition decides whether those events settle a request.

7. Minimal effect handlers

Add a small exhaustive map for one-shot commands:

ts
defineEffectHandlers<Command, Event>()({
  StartRuntime: correlatedEffect({
    run,
    succeeded,
    failed,
    cancelled,
  }),
  PublishStatus: isolatedEffect({
    run,
    onError,
  }),
});

MVP guarantees:

  • every command variant has a handler;
  • correlated effects require success, failure, and cancellation builders;
  • synchronous throw and async rejection use the same error mapping;
  • terminal events use the captured command/request/invocation, not mutable current state;
  • effects receive a captured non-creating actor sink and owned abort signal; and
  • isolated effects declare error behavior explicitly.

Concurrency, supersession, scheduling, and point-of-no-return remain domain policy. Streaming and checkpointed effect recipes are follow-ups.

8. Renderer mutation facade

Ship one shared handwritten typed helper behind current domain hooks:

ts
useMachineMutation({
  prepare,
  request,
  observedRevision,
  acceptance,
  inputDisposition,
  concurrency,
  retry,
});

Expose orthogonal facts:

ts
connection:
  | "connecting"
  | "ready"
  | "disconnected"
  | "incompatible";

snapshot:
  | { kind: "unavailable" }
  | { kind: "available"; freshness: "live" | "cached" };

admission:
  | { kind: "idle" }
  | { kind: "dispatching" }
  | { kind: "accepted"; disposition: "fresh" | "replayed" }
  | { kind: "refused"; reason: AdmissionRefusal };

execution:
  | { kind: "untracked" }
  | { kind: "pending" | "running" }
  | {
      kind: "settled";
      outcome:
        | "succeeded"
        | "failed"
        | "cancelled"
        | "superseded"
        | "disposed";
    };

A derived convenience status is allowed, but the framework does not collapse these facts into one linear lifecycle. The connection facet preserves the existing RemoteConnectionStatus; actor snapshot/capability availability is a separate fact.

The helper:

  • preserves input until the declared authoritative milestone;
  • distinguishes expected refusal, transport/infrastructure failure, and domain failure;
  • invalidates stale completion after unmount/replacement;
  • applies single-flight only when declared;
  • defaults to no retry;
  • retries only with a stable prepared identity and receiver dedupe; and
  • consumes expected rejections for event-handler use while preserving errors for callers that await sequencing.

disposed is presentation-neutral by default. A domain may opt into error copy only when disposal is exceptional for that operation.

Current runApp, stopApp, image-generation, and other renderer façades remain the public product APIs during the pilots. Generate bindings only if both pilots converge on this shape.

9. Outcome and error channels

Keep three channels separate:

ChannelExamplesSemantics
Transport/admission resultapplied, ignored, replayed, refused, conflictTyped data; not domain completion
Infrastructure failuredependency failure, codec bug, programmer throwPromise rejection and telemetry-visible
Domain outcomesucceeded, failed, cancelled, superseded, disposedTyped terminal result correlated to RequestId

Expected denial remains a DyadError with its original DyadErrorKind internally. Do not convert broad exceptions to Auth. Expected disposal is a domain outcome; legacy IPC adapters map it to an existing appropriate error classification.

No renderer best-effort delivery may be the authoritative settlement path.

Conformance and diagnostics

Finding-to-scenario catalog

Do not implement 256 bespoke regression tests. Map duplicate findings to one reusable failure shape. Every one of the 46 foundation findings must map to:

  • an API/type prohibition;
  • a shared conformance scenario; or
  • an explicitly domain-owned invariant with a focused test.

Minimum MVP scenarios:

  1. same-key construction, disposal, and recreation;
  2. synchronous cancellation/clock reentry during activation;
  3. remote/local/subscription/producer ingress while fenced;
  4. cleanup event allowed during drain, then full seal;
  5. sender/window destruction at every authorization await;
  6. actor instance/revision changes during authorization;
  7. unsubscribe during pending bootstrap;
  8. refresh accidentally acquiring ownership;
  9. stale release against a replacement generation;
  10. unresolved receipt under capacity pressure;
  11. same message ID reused for a different address, revision, request identity, or payload fingerprint;
  12. stable-ID retry after a lost receipt;
  13. request/runtime identity alias;
  14. immediate settlement after operation registration;
  15. disposal with unresolved operations;
  16. effect success, failure, cancellation, and late output;
  17. late producer attempting creating lookup;
  18. observed-revision conflict without fallback to latest;
  19. UI input cleared before authoritative acceptance;
  20. maximum valid intent/snapshot envelope;
  21. #4123 restart after partial hard reset.

Proportional tiers

TierApplies toMVP checks
T0 pureFinite machine definitionsvariant inventories, totality, reachability, reference stability, invariants, explicit exclusions
T1 hosted/effectfulHosted actors/controllersconstruction/disposal/reentry, outcome settlement, effect terminals, non-creating late output, zero resources
T2 distributedRemote definitionsintent/event codecs, key relationship, authorization awaits, duplicate/retry, subscriptions, two windows, budgets
T3 persistentLater persistent contractscheckpoint failure, crash boundaries, hydration barrier, reconciliation
T4 compositionDeclared multi-machine protocolsbounded cosim and ownership transfer

Use existing fake clocks, controlled promises, FakeDuplexRemoteTransport, host/controller conformance, reachability exploration, two-window harness, and runCosim.

A bound hit is not a pass. CI must report exhaustive versus boundReached, and required scenarios must split their alphabets until exhaustive.

MVP diagnostic output

Do not block the primitives on a general async trace-minimization platform. Reuse the shortest schedule available from existing exploration and emit:

  1. one-line causal summary;
  2. focused critical-path timeline;
  3. aligned message/request/invocation/actor/revision/window identities;
  4. expected versus actual resource counts; and
  5. a copyable redacted structured trace record.

The internal record should be JSON-safe, but a general JSON shrinker and GUI are follow-ups. Definition-owned redaction must exclude prompts, credentials, provider payloads, filesystem contents, and other sensitive data.

Tracing/reporting failure is isolated from domain settlement.

Degraded-state behavior

The framework is incomplete unless failure states have defined product behavior:

  • Bootstrap/reconnect exposes connection: connecting and snapshot: unavailable, never fabricated idle. Disconnected and incompatible remain distinct transport states.
  • Stale prepared subscribe/dispatch returns a typed refusal and cannot target a successor actor.
  • Refused work preserves form/prompt input and never appears started.
  • Admission never appears as domain completion.
  • Expected disposal settles requests as disposed; it does not automatically synthesize a generic failure toast.
  • Capacity pressure rejects new admission and never evicts unresolved receipts or operations.
  • A stale release is an observable no-op.
  • Conflict does not retry or use a newer revision unless the intent explicitly declares that policy.
  • A destroyed renderer cannot strand authoritative main-owned settlement.
  • A conformance search that hits its bound fails.
  • Crash behavior remains the pre-existing domain behavior until the durable tier ships; the MVP does not imply crash safety.

MVP implementation plan

The MVP is eight logical stages after the immediate safety prerequisite. Split a stage into smaller PRs if its review surface is large. Never compensate by combining a new primitive with multiple domain migrations.

Prerequisite — #4123 product safety

  • Add the interrupted live-branch restore regression at the exact crash boundary.
  • Fix bespoke reconciliation so a partial hard reset cannot rehydrate as cleanly closed.
  • Preserve this case as the first later durable-runtime acceptance test.

Acceptance:

  • The regression fails before the fix and passes after it.
  • This PR contains no framework abstraction.

Stage 1 — Evidence, layered contracts, and conformance shell

  • Record the exact evidence snapshot and finding-to-scenario catalog.
  • Inventory all six remote definitions, event-schema widening casts, raw dispatch/enqueue uses, waiters, subscription counters, fences, and route maps.
  • Add RemoteIntentContract and test-only MachineConformance.
  • Add focused text/resource diagnostics.
  • Generate a concise, diff-first contract-policy report for PR review; keep the complete matrix as a test artifact.
  • Add assertEnvelopeBudget.
  • Register behavior-neutral app-run and image-generation sidecars.
  • Forbid new widening casts and unsafe helpers without breaking existing allowlisted uses.

Acceptance:

  • Missing required contract policy or conformance registration fails type-check/test with a focused diagnostic.
  • A reviewer can see changed intent, lifecycle, outcome, retry, budget, and unsafe-escape policies without reading generated matrices.
  • Test fixtures remain out of production bundles.
  • No runtime behavior changes.

Stage 2 — PendingReceiptLedger

  • Implement the ledger with distinct pending and settled capacities.
  • Add canonical fingerprint/conflict semantics.
  • Adopt it in remote transport and MCP OAuth.
  • Add lost-receipt, conflicting-address/payload, reconnect, pressure, and stale-continuation tests.

Acceptance:

  • No pending receipt is evicted.
  • Capacity rejection and payload conflict are typed.
  • Transport and OAuth lose bespoke duplicate bookkeeping.
  • The guarantee is explicitly session/host scoped.

Stage 3 — Prepared subscribe/dispatch and subscription lease

  • Split RemoteIntent from trusted Event behind a compatibility adapter.
  • Add typed allow/deny authorization.
  • Add transport-private PreparedSubscribe and PreparedDispatch.
  • Add RemoteSubscriptionLease to RemoteMachineClient.
  • Capture explicit observed-revision tokens at renderer hooks.
  • Preserve protocol v1.

Acceptance:

  • Producer events cannot pass the renderer codec.
  • Key/intent mismatch and forged sender metadata are rejected.
  • Actor/window/gate changes across authorization cannot admit.
  • Refresh does not retain and stale release cannot retire a replacement.

Stage 4 — Host KeyedAdmissionGate

  • Integrate the final gate with the current ActorHost.
  • Implement drain, seal, commit, and abort/reopen.
  • Route every external ingress through the gate.
  • Track actors already constructing and admitted continuations.
  • Provide captured non-creating producer sinks.
  • Prove behavior in host conformance and one synthetic destructive flow.

Acceptance:

  • No ingress can create or dispatch through a sealed key.
  • Cleanup events can drain without deadlocking deletion.
  • The fence remains held through the domain destructive commit.
  • Host lifetime maps are not rewritten in this stage.

Stage 5 — Request, operation, and effect contracts

  • Implement the pre-admission PreparedRequest.
  • Implement the main admitted OperationRegistry.
  • Make actor.request() synchronously create the client handle and bridge it to atomic final main registration.
  • Prototype the post-commit transition outcome channel.
  • Add the minimal one-shot effect-handler map.
  • Add shared useMachineMutation with orthogonal facets.
  • Keep raw APIs behind compatibility adapters.

Acceptance:

  • The client request handle exists before IPC/authorization, while the main operation exists only after final accepted admission.
  • Main operation registration and trusted-event enqueue are one synchronous admission transaction.
  • Request and runtime invocation identities are distinct.
  • Success, failure, cancellation, supersession, and disposal settle once.
  • No scheduler/observer timing is used as effect completion.
  • Existing task/timer scopes remain separate.

Stage 6 — App-run pilot

  • Migrate app-run request settlement to OperationRegistry.
  • Use prepared dispatch, subscription lease, and keyed gate.
  • Bind external producer output to a non-creating expected actor instance.
  • Preserve multiple pending requests and runtime-invocation reuse.
  • Adapt current runApp/stopApp promise façades.
  • Preserve IPC, renderer, and golden behavior.

Acceptance:

  • Every app-run request settles across spawn/stop failure, cancellation, supersession, deletion/reset, and owner disposal.
  • No late process output recreates an actor.
  • No pilot renderer code uses raw remote dispatch.
  • Stop and revise the abstractions if glue grows or unsafe escapes are needed.

Stage 7 — Image-generation pilot

  • Migrate one-shot effects to the exhaustive handler map.
  • Use operation settlement, admission gate, and prepared mutation.
  • Preserve prompt/dialog input until authoritative acceptance.
  • Enforce declared single-flight or parallel behavior.
  • Test multi-operation retention, cancellation, deletion, and initiator presentation.
  • Preserve existing public façade and behavior.

Acceptance:

  • Refused admission does not clear the prompt or close the dialog.
  • Every job's success/failure/cancellation/disposal settles once.
  • Terminal payload retention is bounded.
  • Double submission follows explicit policy.

Stage 8 — Enforce, measure, and decide

  • Deny raw dispatch/enqueue, bespoke waiters, creating late ensure(), and independent subscription ref counting on migrated surfaces.
  • Require contracts for new definitions/intents and changes to lifecycle/protocol/effect/ownership seams.
  • Keep exact allowlists for unmigrated code.
  • Replace enforceable rules prose with references to primitives/tests.
  • Publish fault coverage, glue, type-check, test-runtime, compatibility, and review data.
  • Hold a stop/go review before conditional follow-up.

Acceptance:

  • No unresolved valid HIGH/P1 finding in a framework-covered category at the agreed pre-merge cutoff.
  • Historical failure shapes applicable to both pilots are killed.
  • Terminal/disposal cases leave zero owned resources.
  • Golden UI, IPC, and renderer behavior remains stable.
  • The common path needs no raw escape hatch.

Stop/go criteria

Proceed beyond the MVP only if all are true:

Correctness

  • Every foundation finding is mapped to prohibition, shared scenario, or explicit domain invariant.
  • Every accepted pilot operation settles exactly once within host lifetime.
  • All required generated searches are exhaustive.
  • All pilot terminal/disposal scenarios have zero owned waiters, tasks, timers, subscriptions, routes, and actor references.
  • No unresolved valid HIGH/P1 framework-covered finding remains.

Review findings discovered and fixed during the pilot are evidence, not automatic failure. “Zero initial HIGH/P1 comments” is an aspiration, not the release gate.

Maintainability and DX

  • At least 30% less defined handwritten admission/subscription/waiter/fence glue in each pilot, measured against a named pre-migration file inventory.
  • No new unsafe escape without a rationale and focused scenario.
  • Contract/conformance presubmit remains under two minutes.
  • No material npm run ts performance regression; record before/after medians.
  • A failure is diagnosable from generated output without adding instrumentation.
  • Ordinary pilot callers use domain façades backed by actor.request() and useMachineMutation, not raw lifecycle pieces.

Compatibility

  • Protocol v1, IPC endpoints, renderer methods, and golden behavior remain compatible.
  • No database migration.
  • No period with simultaneous legacy and new authority.
  • Each pilot has a domain-level rollback boundary.

Actual churn reduction

Behavior-preserving pilot refactors cannot prove reduced future review churn. Measure the next two comparable new-machine or lifecycle/protocol migration PRs:

  • accepted framework-category findings per 1,000 changed production LOC;
  • review-fix commits per 1,000 changed production LOC;
  • raw counts alongside normalized counts;
  • reviewer count/protocol and review-window differences; and
  • classification of duplicate, invalid, late, and domain-policy findings.

Target at least a 50% reduction against comparable baseline work. If two qualifying PRs do not occur, mark churn reduction unproven rather than claiming success.

Conditional follow-up plan

Follow-up A — Presentation ownership and remaining remote definitions

  • Add a main-only OperationRouteRegistry only after the pilot operation lifetime is stable.
  • First writer owns the route; unresolved routes are pinned; capacity rejects admission; stale release cannot affect a replacement.
  • Migrate GitHub operations and version-preview presentation/window interest.
  • Migrate remaining remote definitions one at a time.
  • Introduce a remote-manager recipe only if duplication remains after RemoteSubscriptionLease adoption.

Do not add afterCommands; route cleanup follows terminal operation publication and settlement.

Follow-up B — Durable checkpoint-before-effect

  • Keep the focused #4123 fix until the general runtime replaces it.
  • Pilot on version preview:
    1. commit exact phase/next step;
    2. durably flush;
    3. start the external mutation;
    4. reconcile persisted facts against actual Git HEAD after restart.
  • A checkpoint failure suppresses the external effect.
  • New mutation remains blocked during hydration/reconciliation.
  • Pilot plan handoff second.
  • Give any DB/file journal its own schema and migration review.

The guarantee is checkpoint ordering plus explicit recovery—not exactly-once external effects or generic compensation.

Follow-up C — Chat/plan owned queue

  • Add a narrow queue abstraction only if concrete duplication remains.
  • Validate/CAS revision and claim invocation-time items before external owner settlement.
  • Keep durable and ephemeral replay policy explicit.
  • Settle replaced, rejected, cancelled, and disposed items.
  • Release terminal large payloads.
  • Add T4 cosimulations for chat stream, queued prompt, user-input follow-up, plan handoff, and destructive deletion.

Scheduling and replacement remain domain policy.

Follow-up D — Final enforcement and optional ergonomics

  • Remove compatibility adapters after all six definitions migrate.
  • Deny raw production APIs outside named composition roots.
  • Backfill conformance according to the inventory.
  • Consider generated renderer bindings only if both pilots and later migrations share the same helper contract.
  • Consider an internal host lifetime-slot rewrite only if conformance identifies a remaining representational hole or proves a material simplification.
  • Consider property-based expansion, a GUI inspector, or transition helper only when their leverage is measured.

Compatibility, security, and performance

Compatibility

  • Keep wire protocol v1 and its messageId.
  • Preserve renderer hooks, domain managers, IPC endpoints, and promise façades through adapters.
  • Forbid new unsafe uses immediately; deny existing uses only after their surface migrates.
  • Migrate one domain per PR and retain golden characterization tests.
  • Do not run legacy and new authority paths simultaneously.
  • No database migration in the MVP.

Security

  • Bound untrusted envelopes before codec traversal, cloning, or hashing.
  • Canonicalize object keys only after authorization.
  • Derive window/session provenance in main.
  • Bind prepared subscribe to encoded address/window/gate reservation and prepared dispatch to canonical key, admitted subscription, actor/window generation, revision, gate generation, and complete dispatch digest.
  • Reject renderer access to internal producer/completion events.
  • Preserve DyadErrorKind; do not hide dependency/programming failures as denial.
  • Redact trace payloads by definition.

Performance

  • Keep conformance fixtures and exploration out of production bundles.
  • Hash large intents once and retain only their digest.
  • Separate pending capacity from settled-history retention.
  • Keep histories bounded and opt-in.
  • Keep production ownership counters O(1); detailed tracing is debug/test-only.
  • Split exploration alphabets rather than silently raising bounds.
  • Measure npm run ts and contract-suite runtime before and after each generic type/test addition.

Risks and mitigations

RiskMitigation
This creates a second frameworkUse layered contracts and five narrow mechanisms; stop after two pilots
Host changes reopen #4100-class bugsPreserve host representation; land adversarial conformance before the gate
The operation abstraction becomes a mega-scopeRegistry owns outcomes only and composes existing scopes
Authors still assemble temporal pieces manuallyOrdinary path is actor.request() plus domain façade; internal pieces stay framework-private
Types encourage casts or slow tsgoUse flat unions, few initial brands, and measured type-check baselines
Retries duplicate destructive workDefault no retry; require stable prepared identity and receiver dedupe
In-memory exactly-once is mistaken for durabilityPut the host/session boundary in APIs and reports
Renderer semantics regressKeep façades, require observed revision and explicit acceptance/input policy, run golden UI tests
State-space exploration gives false confidenceReport bounds explicitly and split required alphabets until exhaustive
Diagnostics expose sensitive dataDefinition-owned redaction and bounded capture
Review metrics are gamed or incomparableNormalize by production LOC and measure two future comparable PRs
Conditional work becomes assumed scopeStop/go decision explicitly funds each follow-up

Components affected in the MVP

Shared runtime

  • src/state_machines/types.ts — optional post-commit outcome channel
  • src/state_machines/testing.ts — tier registration and shared scenarios
  • src/state_machines/trace.ts — causal/resource diagnostics
  • new src/state_machines/operation_registry.ts
  • new src/state_machines/pending_receipt_ledger.ts
  • new minimal effect-handler helper

Distributed runtime

  • src/distributed_machines/definition.ts — layered remote intent contract
  • src/distributed_machines/actor_host.ts — final keyed admission gate
  • src/distributed_machines/remote_transport.ts — ledger and prepared subscribe/dispatch
  • src/distributed_machines/remote_client.ts — subscription lease
  • src/distributed_machines/remote_protocol.ts — intent/event-compatible wire boundary
  • src/distributed_machines/react.ts — observed revision and mutation helper
  • src/distributed_machines/boundaries.test.ts — progressive unsafe-use inventory
  • src/distributed_machines/testing/ — tiered host/transport conformance

First adopters

  • src/app_run/definition.ts
  • src/app_run/remote_manager.ts
  • src/ipc/services/image_generation_definition.ts
  • image-generation actor/presentation services and renderer dialog/hook
  • MCP OAuth registry

The exact file list should be revalidated at each implementation PR because upstream migration work may continue.

Decision log

DecisionRationale
Codex is the base planIts evidence, assurance model, testing, compatibility, and sequencing are stronger
Claude's concrete fence/hash/budget/revision details are retainedThey directly encode repeated accepted findings
No XState or statechart replacementPure transitions were not the churn source
Layered contracts, not monolithic MachineSpecLower type and abstraction risk; production and test concerns stay separate
PendingReceiptLedger is core MVPTransport and OAuth independently proved the same reusable invariant
Prepared subscribe/dispatch values stay privateEach authorization/final-admission flow must be one framework transaction
Keep current ActorHost internalsA representation rewrite would reopen heavily reviewed lifecycle behavior
Two-stage request plus narrow OperationRegistryPre-admission and admitted lifetimes differ; tasks/timers/routes remain separate
No afterCommands phaseScheduler handoff is not effect or operation completion
Explicit observed-revision tokenThe client cannot infer what React rendered
Keep domain managersOnly subscription lifetime has demonstrated commonality
Handwritten shared mutation helper firstTwo pilots must validate the renderer contract before generation
App run is the first pilotIt directly tests request/runtime identity, waiters, producer output, and disposal
Image generation is the second pilotIt tests collections, effects, form preservation, retention, and parallelism
#4123 is fixed immediately; durability is laterKnown product safety should not wait for a speculative framework
Chat/queue is lastIt has the largest domain-specific state space
Pilot safety does not prove reduced future churnNormalize the next two comparable migrations before claiming success

Domain questions each contract must answer

  • Which ignored or replayed dispositions count as semantic success?
  • Which observed revision is authoritative for this intent?
  • Which intents may retry, under which stable identity and receiver dedupe?
  • Which cleanup events may pass while a deletion/reset fence drains?
  • What is the authoritative UI acceptance milestone?
  • When should input clear: admission, durable acceptance, completion, or a domain-specific event?
  • What scheduling, supersession, and staleness policy applies?
  • Which terminal outcome should expected owner disposal produce?
  • If the initiating window is gone, should presentation drop, broadcast, or use an explicit fallback?
  • For persistent work, which external facts prove resume, compensation, or recovery is safe?

Final success claim

At MVP completion, the project may claim:

For app run and image generation, framework-owned remote admission, keyed lifetime, subscription, receipt, and in-process request-settlement invariants are enforced through the normal API and covered by deterministic adversarial tests without changing wire, IPC, or renderer behavior.

The project may claim that this program reduced review churn only after two comparable future migrations demonstrate the normalized reduction target.


Generated by dyad:swarm-to-plan.