Dirty Runs: freeze the bounded A → B protocol and proof envelope #700

Parent epic: #699. First implementation gate; no stateful v2 work before this contract is reviewed.

Deliverable

A short, versioned transition table and executable acceptance inventory for the internal full-schema A → B proof. Keep it in the repository's developer documentation/test notes; do not build a general design framework. The remaining subissues implement this contract.

Freeze the supported envelope

• Exactly two ordinary single-task steps and one dependency A → B; no map, condition, skip policy, or disconnected branch. Test both existing queue modes. Preserve root A dispatch before start returns and B's bounded startDelay measured from dispatch.
• Effective handler policy is maxAttempts=1, whenExhausted='fail'. Support success and exhausted handler failure only. Reject retryable-error authoring, map/condition/skip configuration, invalid timing, and later policy tuning outside this envelope before mutation. Do not alter v1 semantics.
• Fix numeric constants for input/definition bytes, task/step/leaf-result bytes, retained settlement bytes, timeout/delay range, claim-history count, and transitions/examined rows per chunk. Suggested starting test limits: 2 steps, 1 edge, 2 tasks, 64 KiB input/result, 2 claims per task, 1 semantic transition per chunk. Choose and document aggregate/history/error-byte limits too. These are internal test bounds, not production defaults.
• Restrict each v2 claim and controlled-recovery call to one explicit logical task/run and at most one supplied message ID. Reject oversized or duplicate-filled ID arrays before expansion, lookup scans, or mutation. Recovery targets that one task; it does not sweep candidates. The internal worker bridge uses singleton reservations/claims, not arbitrary cross-run batches. Bound candidate reads for any test-side reconciliation selector separately.
• One controlled takeover per task is enough to prove fencing. If that bound is reached, block further admission visibly with engine health and retain messages/history. Do not introduce an automatic business exhaustion policy or claim Terminalize tasks after the stalled-task requeue limit #689 resolved.

Freeze the transitions

Write preconditions, locks, changes, response, and replay identity for start, claim, controlled lease recovery/takeover, success, exhausted handler failure, oversized result, reconciliation dispatch, fixed-point clean, finalization, and error/backoff/attention.

Claim states must distinguish active, revoked/lost, and settled without overwriting earlier settlement evidence. An expired horizon makes a claim recoverable; the locked revocation/takeover determines ownership. State explicitly whether first settlement remains legal after horizon expiry but before revocation. Both contenders serialize under the run lock.

Settlement lookup starts from claim_id: identical settled kind/payload returns its durable prior disposition even after a new claim or terminal run; different kind/payload conflicts; unknown/revoked/current-but-ineligible submissions are stale/terminal. Check run/step/task eligibility before result validation or any queue operation. Conflict/stale responses must be typed, not transport exceptions.

For this envelope, success completes its task/step and requests orchestration but cannot dispatch B or finalize the run. Exhausted failure synchronously fails the run, terminalizes unfinished tasks, revokes claims, and archives owned run messages even with no processor. Canonicalize JSON for equality: object key order must not cause false conflicts; 0, false, "", and JSON null remain distinct valid outputs.

An oversized successful result gets a durable non-retryable disposition, not a handler retry. Choose bounded retained evidence and collision-resistant canonical replay identity before enabling that path. Bounds checked after JSON arrives do not prove bounded network parsing/hashing for arbitrary external payloads; this internal proof uses controlled handlers and makes no such production claim.

Worker result-reporting bound

Before #702, freeze the v2 acknowledgement attempt count and an absolute elapsed deadline that covers in-flight SQL waits, retry delays, and shutdown interaction. #706 implements that decision; it does not choose a new budget later. Freeze an explicit unconfirmed-acknowledgement outcome when the deadline or shutdown interrupts reporting. A timeout/cancellation does not prove rollback. While the executor remains alive, retain the same original canonical outcome and claim for bounded resubmission; observe late completion/rejection without changing the result kind or executing the handler again. Do not retry definite accepted/conflict/stale/terminal responses.

The named checks must include a reporting promise that never settles, not only a rejected promise after a real commit. Bound return to the existing worker error boundary without requiring a new retry framework, supervisor, or durable worker-result outbox.

Work and admission

Create the stable work row with the run. Start queues A synchronously and can leave work clean while A executes. A terminal settlement atomically increments requested generation; chunk progress leaves it pending; only a locked no-immediate-action check marks the captured generation processed. Catch-up can include an executing handler.

No new claims while dirty, retry-waiting, or in attention. Valid current claims may still settle. Attention in this proof retains messages; no repair or archive/reconstruction feature is implied. Fatal failure uses its synchronous terminal cleanup, not attention.

Run-first locks apply to all protocol paths, including recovery and errors. Candidate reads are not ownership. Separate transactions implement separate commits. Realtime/notifications are optional hints whose failure does not undo accepted core work.

Compatibility and stop rules

Identify every legacy pgflow writer/helper, deletion/recompile/pruning path, and startup/worker path that could touch these rows or queues. Assign enforcement to #702; direct PGMQ polling is not claim ownership, so dedicate test flows/queues and do not run old pollers on v2 queues. Privileged ad hoc SQL/externally replaced queues are outside the supported boundary, not a protection claim.

V2 is internal, opt-in, and separate from public v1 defaults. No public DSL/API replacement, production use, version-package publication, beta, or cutover. Full map/condition/skip parity, retries, worker-loss exhaustion, repair, and supervised runtime need follow-on approval.

Acceptance

• The transition table resolves every enabled outcome and has named deterministic tests/owners in the other subissues; no enabled path depends on an undecided later product policy.
• Numeric checks cover real scanned/generated/aggregated/retained work, not only a loop counter or statement timeout. Multi-ID/cross-run claims and recovery are rejected before expansion or any task/history/VT/health write; duplicate-filled arrays cannot bypass the singleton limit.
• Worker reporting attempts, in-flight deadline, unconfirmed result, shutdown, and late-response behavior are fixed with named never-settling and post-commit-loss checks in Dirty Runs: connect the typed worker path and close the A → B evidence gate #706.
• Unsupported shape/policy rejection happens before v2 runtime/message mutation; SQL and worker boundaries agree.
• The contract separates actual claims, handler failures, and infrastructure losses and fixes the in-flight policy snapshot.
• The contract explicitly lists deferred features and operational no-go conditions; a narrow proof is not described as full architecture parity.

Depends on: none. This is not a prerequisite for the independent shared worker fixes #701.