# Closeout and editor-delivery churn contract

## Architecture contract

- **Invariant:** A remote delivery identity may be decoded into a local replica at most once while its visible editor projection or ACK is outstanding. Exact visible editor content is sufficient ACK proof even when disk persistence is deliberately deferred; disk-save status cannot gate the ACK. Repeated pulls of that identity coalesce into the retained projection/ACK state; they do not mutate the replica again, enqueue another EDT apply, or count as forward progress.
- **Invariant:** A remote canonical rejected by the template-structure guard is never left as the attached native replica frontier. When the unchanged live editor baseline is itself structurally exact, each editor replica manager performs one fenced text-adopt and atomic re-registration; otherwise it fails closed with bounded retry and never overwrites the editor.
- **Invariant:** An admitted operator edit is never projected away because disk is older or a native replica frontier is stale. If the native frontier does not equal the edit's shadow baseline, the plugin adopts the exact structurally-valid visible editor text once and atomically re-registers before accepting another delta.
- **Invariant:** Save is a durability acknowledgement, not a second logical mutation. Unsaved and saved forms of one queue edit share one semantic identity and produce exactly one canonical queue item.
- **Invariant:** Any disk change while an editor is open is an independent pending candidate, never CRDT authority and never the pending-response slot. Accept propagates the exact visible editor cut before clearing; a newer editor edit or exact save-flush clears the candidate; final editor close clears it and falls back to disk. Authority order is editor/CRDT, disk, then Git recovery evidence.
- **Invariant:** Closeout reports `committed` only when the authoritative response projection is durable and the session document at `HEAD` equals the proven closeout snapshot. A binary-owned compacted projection may cross the historical-response guard only with durable compaction evidence; arbitrary response-bearing drift remains fail-closed.
- **Invariant:** Commit-seam free-text cleanup is a bounded disk transaction. It performs no controller lookup while holding the document lock; ordinary editor-authoritative cleanup finishes its controller read before lock acquisition.
- **Invariant:** A baseline overlay is a cache paired with a named explicit markdown baseline, never implicit merge authority. With no baseline path, a stale `.overlay.yrs` sidecar cannot resurrect a consumed queue head.
- **Invariant:** Controller recycle invalidates a JetBrains replica registration and starts bounded re-registration. A disconnected relay cannot remain permanently idle while its document is still open.
- **Invariant:** Editor-buffer authority and editor-delivery routability are separate leases. A live IDE process keeps an unsaved buffer authoritative, but only a fresh plugin-owner worker heartbeat may receive a canonical delivery. If that worker heartbeat expires, closeout retains the exact target without writing disk and schedules a safe-checkpoint recycle.
- **Invariant:** A stale editor-delivery worker breaks the ordinary open-cycle recycle deferral. Once no IPC handler is in flight, the supervisor may hot-reexec while the capture-backed cycle remains open because waiting for that same cycle to close would wait circularly on the missing ACK.
- **Invariant:** Delivery convergence requires positive visible evidence. Zero live replicas is not an editor-visible quorum; after the last replica disappears, only an exact durable visible-write receipt may settle the target.
- **Invariant:** A transient failure to sample tmux pane liveness cannot become an empty liveness set. Destructive registry pruning aborts on sampling failure and preserves actor records for the next successful observation.
- **Invariant:** Force-disk authorization is revalidated at the mutation boundary. If an editor relay registers or editor authority otherwise changes after authorization, the force-disk transaction aborts before projection/commit; it cannot race the relay, duplicate a response, or advance the boundary from stale content.
- **Invariant:** A timed-out preflight cannot retain document/controller work after its owner exits. Cleanup may signal another process only with same-document, command-shape, age, and orphan/owner-death proof; wrapper exit 144 after an intentional kill is cancellation evidence, not a new product failure.
- **Invariant:** Controller backpressure is a shared-capacity signal, not a retry prompt. Idle watchers use one controller-wide bounded backoff/coalescing gate, and a live-editor response already materialized by semantic response identity is retired instead of resubmitted to the merge/write path.
- **Invariant:** A foreground editor-ACK deadline is not response-write failure when canonical CRDT authority and the applied receipt still prove the exact complete target and asynchronous recovery has been successfully signaled. That state returns retained success and continues one binary-owned retry; it never instructs the agent or operator to retry finalize, force disk, or recycle the controller.
- **Invariant:** A retained document write owns its exact capture until settlement. Concurrent repair cannot retire that capture from a reused heading or temporarily missing body; a historical false retirement may reactivate only the identical capture ID, cycle ID, and response hash after the full response body is proven in converged editor, canonical, and disk authority.
- **Invariant:** ACK retry backoff is an admission gate, not only a timer. External CRDT events may mark pending work while backoff is active, but cannot start another drain or decode the retained delivery until the gate expires.
- **Invariant:** A controller commit request is sent on the same acquired stream that established controller liveness. A recycle after acquisition is a transport failure, not permission to reconnect ambiguously or fall back to a local commit.
- **Invariant:** Response recovery is cell-idempotent. A complete retry atomically supersedes stale uncommitted response tails, preserves intervening operator prompts, and an exact subsequent replay performs no mutation, leaving one final response and one boundary.
- **Invariant:** Release and local-install automation must produce an artifact accepted by its destination and must select a JetBrains target from explicit or runtime-proven evidence. Ambiguous targets fail with an actionable selector instead of consuming stdin implicitly.
- **Invariant:** A supervisor hot-reexec that preserves a live harness child preserves its successful capability proof instead of launching a competing proof child. Reuse requires the same surviving child plus an exact launch/capability fingerprint; any missing, changed, pending, or failed evidence re-proves.
- **Invariant:** A network probe proves the effective sandbox boundary, not the existence of a second model turn. `danger-full-access` Codex has no child sandbox, so the exact DNS/HTTPS command runs directly with the resolved child environment; sandboxed Codex/OpenCode still prove through their harness child.
- **Policy owners:** the JetBrains and VS Code `CrdtReplicaManager` adapters implement the same typed in-flight delivery, template-projection, fenced live-editor recovery, ACK-retention, and recycle re-registration policy; `agent-doc-workflow::capture::decide_stale_capture_retirement` owns whether a capture may retire; capture/cycle IO apply the exact-identity reactivation effect; `agent-doc-closeout-runtime-io` and `agent-doc-document-realtime-io` own the converged full-body settlement proof; `agent-doc-queue-io` owns strike read/lock ordering and commit-seam disk authority; `agent-doc-write-runtime-io` owns explicit baseline selection; `agent-doc-document-realtime-io` owns the force-disk authorization scope and mutation fence while write/compact entrypoints hold that scope across response generation; `agent-doc-turn-executor::capability_proof` owns exact proof-contract fingerprinting and the reuse/re-prove decision while `agent-doc-start-runtime-io` owns the same-child reexec handoff effect; `agent-doc-agent-io` owns timeout process-group cleanup/classification; `agent-doc-commit-io` plus the preflight/session-check closeout projection owns durable HEAD proof and compaction authorization; the executable model owns cross-layer trace semantics; the `Makefile` owns PyPI wheel compatibility; `src/plugin.rs` owns editor target discovery and selection.
- **Evidence inputs:** remote `patch_id` and `generation`, update bytes/content hash, current forwarder identity, controller instance/transport failure, pending EDT projection and retained ACK map, retained document-write presence, capture/cycle IDs and response hash, full-body materialization in converged editor/canonical/disk text, remote/editor template-normalization states, exact live editor text, unchanged shadow-baseline proof, recovery-in-flight state, strike mode and disk/controller source, document-lock boundary, explicit baseline path and paired markdown/model content, force-disk authority epoch and relay count immediately before mutation, process command line/document/parent/start age, surviving reexec child PID/master FD and proof-contract fingerprint, editor/disk/shadow hashes, cycle phase and response marker, snapshot/file/HEAD hashes, authoritative-compaction scope and archived exchange evidence, host wheel compatibility, explicit plugin directory and active IDE `idea.plugins.path` evidence.
- **Allowed edit surfaces:** JetBrains and VS Code replica-manager policy/recovery boundaries and focused parity tests/spec; an agent-doc-owned executable model and trace fixtures; queue consume read/lock policy and focused tests; write-runtime baseline and force-disk scope entrypoints; document-realtime force-disk authority/focused tests; agent backend child-process lifecycle and focused tests; compact force-disk scope port; closeout commit, preflight/session-check proof code only if evidence requires it; plugin installer CLI/discovery/tests; Makefile release target and release documentation; generated skill/version surfaces required by a patch release.
- **Verification:** reproduce duplicate pull behavior in deterministic replica-delivery tests for both editors; prove one decode/apply and retained ACK retry; prove every template-projection decision row, including fenced valid-editor adoption and invalid/stale-editor fail-closed behavior; prove controller loss triggers bounded replica re-registration; run generated fault traces through the reference model and assert safety invariants; compare legacy and Lazily-backed adapter observations or emit typed `CapabilityMissing` gaps; prove commit-seam strike performs no controller lookup and ordinary strike reads before lock; prove absent explicit baseline ignores stale overlay; prove a relay appearing after force-disk authorization aborts without write/commit while an already-live authorization retains its explicit semantics; prove a timed-out backend process group reaps a real background descendant and records cancellation; unit-test explicit/proven/ambiguous editor selection; build a `manylinux_2_17` wheel; run `make check`, editor suites, installation, and release validation.
- **Out of scope:** redesigning the controller CRDT or observable-set history, broad queue cleanup, automatic GUI restart, adopting arbitrary unsaved editor text without exact structure and unchanged-baseline proof, and unrelated working-tree changes.

## Transition table

| Surface | Current state | Evidence/event | Next state | Required effect |
| --- | --- | --- | --- | --- |
| managed capability proof | proven child, supervisor binary stale | same child survives `execve` and exact proof contract matches | proven | hand the fingerprint through the reexec environment, consume and strip all supervisor-only handoff variables before resolving child env, emit a new current-generation proven event, and launch no probe child |
| managed capability proof | missing/pending/failed proof, dead/fresh child, or contract mismatch | supervisor start/reexec | pending then proven/failed | launch the bounded probe; never promote historical proof for a different child or contract |
| managed network proof | fresh Codex child with `danger-full-access` | exact direct DNS/HTTPS shell command succeeds under resolved child environment | proven | record `network_probe=unrestricted_shell_dns_https`; do not launch a second inference-backed Codex child |
| managed network proof | sandboxed Codex or OpenCode | network proof required | pending then proven/failed | run the bounded harness-child probe so the effective sandbox is measured |
| JetBrains delivery | no in-flight identity | new peer delivery | projection pending | decode once, retain identity and ACK evidence, enqueue once |
| JetBrains delivery | projection pending | same delivery repeats | projection pending | coalesce/no-op; no decode, enqueue, or progress credit |
| JetBrains delivery | projection pending | distinct newer delivery | projection pending | merge only through the keyed projection owner and retain all unique ACK identities |
| JetBrains delivery | projection applied | exact visible-content proof, with or without disk persistence | ACK pending or settled | ACK through newest proven generation; retain on transport failure |
| JetBrains delivery | ACK pending | same delivery repeats | ACK pending | retry retained ACK before pull; do not decode again |
| JetBrains template projection | remote canonical is structurally exact | unchanged editor baseline | projection pending | queue the ordinary keyed editor projection |
| JetBrains template projection | remote canonical is invalid or requires repair | editor equals the captured shadow baseline and is structurally exact | recovering | adopt the exact editor text once, atomically re-register from the rebuilt canonical, retire the stale delivery frontier, then resume pull |
| JetBrains template projection | remote canonical is invalid or requires repair | editor is missing, advanced, invalid, repairable, or recovery is already active | retry/fail closed | preserve editor authority, perform no text adopt or ACK, and retry only through bounded backoff |
| editor local delta | native replica equals the captured shadow | operator edit admitted | forwarding | apply one incremental delta; a later Save may advance disk durability only |
| editor local delta | native replica differs from the captured shadow | exact visible editor text is stable | recovering | never apply the delta to stale lineage; text-adopt the editor once and atomically replace the replica |
| editor Save | queue edit was already admitted | disk write/VFS echo | durable | preserve the canonical semantic identity; do not replay or duplicate the queue item |
| external disk write | one or more editor buffers open | exact disk bytes observed | pending user decision | retain/replace one exact Lazily disk candidate; do not mutate canonical CRDT or the independent response lineage |
| external disk pending | editor accepts/reloads exact candidate | replica re-registers from visible buffer | settled | propagate the accepted editor cut through CRDT, then clear only the disk candidate |
| external disk pending | editor buffer advances | operator edit | settled | propagate editor authority and clear the candidate without component merge |
| external disk pending | editor saves exact buffer bytes to disk | file-watch save proof | settled | make the saved editor cut authoritative and clear any older candidate |
| external disk pending | final editor closes | current disk exists | disk authority | clear the candidate and fall back to disk; a non-final close preserves CRDT authority |
| external disk pending | several replicas reconnect with no exact common cut | CRDT sync incomplete | pending user decision | retain the disk candidate with an unproven-editor-cut marker and perform no mutation |
| JetBrains delivery | failed/stale projection | editor advanced | retry/reconcile | remove in-flight projection only after recording a bounded reconciliation request |
| JetBrains relay | registered | controller transport/instance is lost | re-registering | invalidate the old registration and retry registration with bounded backoff while the document stays open |
| editor delivery worker | IDE process live, worker heartbeat stale | closeout has a canonical target | retained/recycling | keep the unsaved buffer authoritative, refuse disk projection, retain the exact target, and request safe-checkpoint recycle without waiting for the open cycle |
| editor delivery convergence | pending target, zero live replicas | no exact durable visible-write receipt | retained | treat the empty replica set as no proof; preserve the target and schedule replica recovery |
| actor registry prune | existing actor records | tmux liveness sampling fails | preserved | abort pruning and retry after a successful liveness snapshot; never translate transport failure into zero panes |
| idle watch | controller model reports backpressure | other sessions are polling or a publish is active | controller-wide cooldown | coalesce observation, stop issuing per-document controller reads, and retry once after bounded quiet time |
| closeout retry | response semantic cell already exists in live editor | retained capture or component merge repeats it | absorbed | retire the duplicate capture, preserve prompts, advance the boundary once, and do not submit another merge/write candidate |
| capture repair | captured response body appears missing or its heading is already answered | matching retained document write still exists | retained | keep the capture and retry the same delivery; never classify it as a superseded orphan |
| capture repair | historical false-retirement marker and discarded capture | identical capture/cycle/hash plus full-body editor/canonical/disk convergence | reactivated then committed | reactivate the same durable capture/cycle, refresh snapshot, and commit once without recapture |
| capture repair | discarded capture | identity mismatch, missing full body, or unconverged authority | retired/blocked | perform no reactivation or mutation; preserve fail-closed evidence |
| JetBrains relay | re-registering | new controller accepts registration | registered | resume delivery/ACK from the retained frontier; do not replay an already-decoded identity |
| free-text strike | commit seam | response capture present | disk transaction | acquire the document lock, read disk once, strike disk-present heads, write atomically; never query controller |
| free-text strike | ordinary editor-authoritative cleanup | controller lookup requested | content resolved | resolve before acquiring the document lock; convergence write compares against that source |
| free-text strike | disk queue empty, controller/cache head stale | phantom head observed | no-op/recovery | preserve disk, do not resurrect/strike the phantom from cache, and log stale evidence |
| baseline resolution | no explicit baseline path | stale model sidecar exists | no baseline | ignore the sidecar; do not merge or replay it |
| baseline resolution | explicit markdown baseline supplied | paired model projection matches | explicit baseline | use the paired cache with markdown as divergence backstop |
| force-disk closeout | relay absent at authorization | relay still absent at mutation fence | writing | compose once from the fenced disk/HEAD source and commit exact projection |
| force-disk closeout | relay absent at authorization | relay appears before mutation fence | blocked | abort before write/commit and retry through editor authority |
| preflight process | prior run timed out | same-document owner proven dead and process old | reaping | terminate the proven orphan, release resources, and record cancellation |
| preflight process | prior run appears slow | owner live or identity proof incomplete | preserved | never signal; report contention with actionable evidence |
| closeout | response projected | file = snapshot = HEAD | committed | persist terminal proof and report success |
| closeout | response projected | snapshot/file differ from HEAD | interrupted | preserve recovery evidence; never report committed |
| closeout | historical response differs | no authoritative compaction proof | blocked | retain the historical-patchback guard |
| closeout | historical response differs | binary-owned compaction scope plus archived-turn proof | committing | compose/commit compacted projection, then verify HEAD equality |
| JetBrains install | explicit target supplied | target is a valid plugin root | installing | use it without prompting |
| JetBrains install | no explicit target | exactly one runtime-proven active target | installing | use the proven target and print the evidence |
| JetBrains install | no explicit target | multiple or no proven targets | blocked | list candidates and require an explicit selector |
| PyPI publish | release requested | compatibility build succeeds | publishing | upload `manylinux_2_17` wheel |
| PyPI publish | compatibility build unavailable | missing Zig/toolchain or invalid tag | blocked | fail before upload with remediation |

## Executable model and Lazily migration contract

The reference model is agent-doc domain policy, not a second production runtime. Its state includes canonical/editor/disk/HEAD text, an independent pending external-disk candidate, semantic queue-item identities, delivery and ACK frontiers, controller/replica epochs, IPC queues, semantic response identities, and cycle phase. Its actions include local edit, queue-item admission, external disk change, accept pending disk, remote delivery, projection, ACK, capture, finalize, commit, save-as-durability-only, disconnect/reconnect, controller recycle, interruption, timeout, drop, duplicate, delay, and reorder.

Every reachable trace must preserve: editor text is never replaced without an exact authority proof; an accepted operator queue item is not lost and has multiplicity at most one on every plane; Save does not mutate canonical semantic identity; one semantic response identity produces at most one live response cell; ACK never advances beyond an exact visible projection; `committed` implies file, snapshot, and HEAD equality; a retained delivery is not decoded twice; timed-out work cannot outlive its proven owner; and, once injected faults stop, a live editor/controller pair can converge without force-disk or busy-looping.

Generated traces run against a pure reference reducer, the current implementation adapter, and a Lazily-backed adapter. Adapters expose only observable state and either match the reference or return a typed `CapabilityMissing` value. Capability gaps are classified separately from implementation mismatches and are promoted into Lazily only when the missing primitive is domain-neutral (for example retained cells, keyed single-flight, epoch/CAS fences, virtual-time backoff, cancellation propagation, durable-effect barriers, or an independent pending external-value decision).

Lean should encode the stable pure transition kernel and safety invariants once. Short-trace state-space exploration/property tests own concurrency and shrinking; liveness under fairness can be checked in TLA+ or an equivalent model checker. JetBrains, VS Code, legacy binary, and Lazily paths are adapters to the shared model, not separate formal specifications.

## Binary-owned finalize and evidence rules

After the first durable response capture, finalize is a keyed operation identified
by cycle id, capture id, and response hash. The CLI, Codex Stop hook, and
route-owned supervisor all resume that same operation through the strict
repair/write/commit seam. Only one supervisor worker runs per key; retryable
editor convergence, CAS races, controller backpressure, and ACK delays use bounded
backoff. The capture remains durable across process exit and supervisor recycle.
No automatic recovery uses force-disk or kills the controller.

Ambiguity rules are evidence-based: dedupe one semantic operation; choose a
causally newer authority over its stale projection; merge compatible complete
CRDT histories. If causal lineage is missing or two concurrent edits express
incompatible semantic replacement intent, retain both candidates and return
`needs_operator` without mutation. The executable model and Lean kernel enforce
this causal-versus-semantic boundary. The Lazily adapter reports
`EvidenceBasedAmbiguityResolution` as a typed capability gap until the core can
express the rule result and retained-candidate barrier directly.
