docs(chat-01): engine-exit stop mode (#1538, row 52)

A server-started stop for an engine that exits on its own: no request,
no confirmation; it closes admission and supersedes the current stop
(H17), but refuses stop-owned under a force stop or another engine
exit. The binding follows it like a force stop at startStop,
advance-stop and confirm-stopped, and its proof needs a member.
Dispatched or acknowledged input goes delivery-unknown; working input
keeps its state. Five lifecycle sequences and two shape cases.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

docs/plans/chat-01/README.md

@@ -9,6 +9,9 @@ findings are Filbert 26119, Dewey 26120 and Rocko's adversarial re-review via
 agent-send. All three accept the named companion gates below. Approval must name
 all four current file hashes; prior reviews do not approve changed bytes.
 
+Row 52 (#1538) adds the server-started `engine-exit` stop mode, described under
+"Control loss, approvals and stopping". No other rule changes.
+
 These are proposed contracts and synthetic reference models. They implement no
 endpoint, engine adapter, permission grant or live migration. Version 2 is a draft
 revision, not a migration of an existing Mosaic record. Q21 publication does not
@@ -324,6 +327,26 @@ signal observations are not mandatory invented events. Only trusted
 cohort/effects observations may promote stopped, and the binding cannot lead its
 stop record. SIGTERM, EOF, abort acknowledgment or idle does not prove death.
 
+An `engine-exit` stop records an engine that ended on its own. The server starts
+it at end of output, as it does a revocation fence: `request` is null and no
+confirmation is needed, because nothing is signalled. It closes admission,
+recovers queued drafts, marks pending decisions uncertain and becomes the current
+stop, so a confirmation issued before it no longer matches. Input already
+dispatched or acknowledged moves to `delivery-unknown`; working input keeps its
+state. No outcome is inferred. It never supersedes a force stop, in any state, or another
+`engine-exit` stop: a force stop's kill also ends output. An exit after a force
+stop ended uncertain needs a new confirmed force stop. It may supersede an
+unfinished interrupt or revocation fence. The binding follows it as it follows a
+force stop: `stopping` at the fence and on each advance, `uncertain` when the stop
+is, and `stopped` only with it. EOF only starts the observation. Promotion to
+stopped takes the same trusted cohort and effects proof as a force stop, and the
+proof must list at least one member, the engine; an empty member list proves
+nothing. A live, incomplete or empty cohort leaves the stop to advance to
+uncertain, after which a confirmed force stop remains available. Recover after an
+`engine-exit` stop needs its own exact confirmation bound to that stop. The
+escalation slot that keeps a force stop from running beside an `engine-exit`
+observation belongs to the implementation, not this model.
+
 `cohortProof` binds stop, authority, conversation/execution/cohort and membership
 epoch; it includes complete membership, boot/pid/start identity, per-member death
 time, observation time and verification digest. `effectReport` lists invocation
@@ -352,8 +375,8 @@ node docs/plans/chat-00/check.mjs
 ```
 
 Node plus installed Python jsonschema 4.26.0, no install/network. Missing validator
-or invalid schema fails closed. R3 currently tests 98 shapes, 322 required-field
-omissions, 76 reference cases and seventeen named lifecycle sequences, plus per-item
+or invalid schema fails closed. R3 currently tests 100 shapes, 322 required-field
+omissions, 76 reference cases and twenty-two named lifecycle sequences, plus per-item
 recovery, immutable queue-edit, bootstrap and multipart-stream regressions. These
 are finite synthetic examples, not comprehensive model checking or runtime proof.
 

docs/plans/chat-01/check.mjs

@@ -99,10 +99,13 @@ function proof(w, id, kind, stopId) {
   return digest === p.verificationDigest && w.trustedProofs[p.id] === digest ? p : null;
 }
 function effects(w, id, stopId) { const p = proof(w, id, 'effectReport', stopId); return p && p.invocations.every(i => ['completed', 'uncertain', 'not-started'].includes(i.disposition) && (i.disposition === 'not-started' || i.evidence)); }
+// The binding follows only stops that end the engine.
+const ending = mode => ['force-stop', 'engine-exit'].includes(mode);
 function stopped(w, s) {
   if (!s || s.state !== 'stopped' || w.binding.stop !== s.id || !scopeMatch(s.target, targetOf(w))) return false;
   const p = proof(w, s.supervisorEvidence, 'cohortProof', s.id);
-  return p && p.membershipComplete && p.membershipEpoch === w.membershipEpoch &&
+  // An engine exit is proven on the engine itself, never on an empty list.
+  return p && p.membershipComplete && p.membershipEpoch === w.membershipEpoch && (s.mode !== 'engine-exit' || p.members.length > 0) &&
     new Set(p.members.map(m => `${m.boot}:${m.pid}:${m.startTicks}`)).size === p.members.length &&
     p.members.every(m => m.terminatedAt && Date.parse(m.terminatedAt) <= Date.parse(p.observedAt)) && effects(w, s.effectsEvidence, s.id);
 }
@@ -118,7 +121,7 @@ function startStop(w, r, mode) {
     for (const d of w.decisions) if (d.state === 'pending') d.state = 'uncertain';
     for (const a of w.approvals) if (a.state === 'pending') a.state = 'uncertain';
   }
-  if (mode === 'force-stop') w.binding.state = 'stopping';
+  if (ending(mode)) w.binding.state = 'stopping';
   if (mode !== 'revocation') emit(w, 'stopping', s.id);
   return `${mode}-fenced`;
 }
@@ -327,14 +330,28 @@ function server(w, op, fields = {}) {
     }
     w.binding.admission = 'open'; emit(w, 'reconciled', s.id); return 'reconciled';
   }
+  if (op === 'engine-exit') {
+    // EOF starts an observation; it proves nothing. A force stop's kill also
+    // ends output, so an engine exit never supersedes a force stop, finished
+    // or not, nor a second engine exit.
+    const current = w.stops.find(s => s.id === w.binding.stop);
+    if (ending(current?.mode)) return bad('stop-owned');
+    const outcome = startStop(w, { id: null, connection: null, target: targetOf(w) }, 'engine-exit');
+    // Dispatched input has no engine left to report it: unknown, not failed.
+    // Working input was delivered; it keeps its state and no outcome is inferred.
+    const unknown = w.queue.filter(q => ['dispatched', 'acknowledged'].includes(q.state));
+    for (const q of unknown) q.state = 'delivery-unknown';
+    if (unknown.length) emit(w, 'queue-changed');
+    return outcome;
+  }
   if (op === 'advance-stop') {
     const s = w.stops.find(s => s.id === w.binding.stop);
     const next = { fenced: ['cancelling', 'stopping', 'uncertain'], cancelling: ['stopping', 'uncertain'], stopping: ['uncertain'], uncertain: [] };
     if (!s || !next[s.state]?.includes(fields.state)) return bad('stop-transition');
-    s.state = fields.state; if (s.mode === 'force-stop') w.binding.state = fields.state === 'uncertain' ? 'uncertain' : 'stopping'; return fields.state;
+    s.state = fields.state; if (ending(s.mode)) w.binding.state = fields.state === 'uncertain' ? 'uncertain' : 'stopping'; return fields.state;
   }
   if (op === 'confirm-stopped') {
-    const s = w.stops.find(s => s.id === w.binding.stop); if (!s || s.mode !== 'force-stop') return bad('stop-proof');
+    const s = w.stops.find(s => s.id === w.binding.stop); if (!s || !ending(s.mode)) return bad('stop-proof');
     const trial = { ...s, state: 'stopped', supervisorEvidence: fields.proof, effectsEvidence: fields.effects };
     if (!stopped(w, trial)) return bad('stop-proof');
     Object.assign(s, trial); w.binding.state = 'stopped'; w.binding.admission = 'closed'; emit(w, 'stopped', s.id); return 'stopped';
@@ -640,6 +657,69 @@ sequence('empty-history-new-user-assistant-roles', () => {
   assert.deepEqual(consumeFinalParts(overlapPage, [user, assistant]), rows);
   assert.throws(() => consumeFinalParts(page, [user, assistant, { ...assistant, id: 'conflict-role', sequence: 3, role: 'user' }]), /conflicting message attribution/);
 });
+sequence('engine-exit-empty-cohort-stopped', () => {
+  const w = clone(f.world); evaluate(w, command(w, 'interrupt')); const predecessor = w.stops.at(-1);
+  assert.equal(server(w, 'engine-exit'), 'engine-exit-fenced'); const s = w.stops.at(-1);
+  assert.equal(s.mode, 'engine-exit'); assert.equal(s.request, null); assert.equal(s.supersedes, predecessor.id); assert.equal(predecessor.state, 'superseded');
+  assert.equal(w.binding.state, 'stopping'); assert.equal(w.binding.admission, 'closed'); assert.equal(w.events.at(-1).type, 'stopping');
+  trustedProof(w, 'effectReport', s.id); const turn = trustedProof(w, 'turnProof', s.id);
+  assert.equal(server(w, 'reconcile-interrupt', { proof: turn }), bad('reconciliation'));
+  const p = trustedProof(w, 'cohortProof', s.id), e = `effectReport-${s.id}`;
+  assert.ok(w.proofs.find(x => x.id === p).members.every(m => m.boot && m.pid && m.startTicks && m.terminatedAt));
+  assert.equal(server(w, 'confirm-stopped', { proof: p, effects: e }), 'stopped');
+  assert.equal(w.binding.state, 'stopped'); assert.equal(w.binding.admission, 'closed');
+  assert.equal(server(w, 'engine-exit'), bad('stop-owned'));
+  assert.equal(evaluate(w, command(w, 'recover', 'connection-1', { stop: s.id, confirmation: 'confirmation-never-issued' })), bad('confirmation'));
+  assert.equal(evaluate(w, command(w, 'issue-confirmation', 'connection-1', { operationToConfirm: 'recover' })), 'confirmation-issued');
+  assert.equal(evaluate(w, command(w, 'recover', 'connection-1', { stop: s.id, confirmation: w.confirmations.at(-1).id })), bad('confirmation'));
+  const resume = confirmation(w, 'recover'); assert.equal(w.confirmations.at(-1).stop, s.id);
+  assert.equal(evaluate(w, command(w, 'recover', 'connection-1', { stop: s.id, confirmation: resume })), 'recovery-eligible');
+  assert.equal(w.outbox.length, 0); assert.equal(w.binding.admission, 'closed');
+});
+sequence('engine-exit-live-unreadable-or-empty-cohort-uncertain', () => {
+  for (const change of [{ members: [{ pid: 101, boot: 'boot-1', startTicks: 20, terminatedAt: null }] }, { membershipComplete: false }, { members: [] }]) {
+    const w = clone(f.world); assert.equal(server(w, 'engine-exit'), 'engine-exit-fenced'); const s = w.stops.at(-1);
+    const p = trustedProof(w, 'cohortProof', s.id), e = trustedProof(w, 'effectReport', s.id);
+    Object.assign(w.proofs.find(x => x.id === p), change); reseal(w, p);
+    assert.equal(server(w, 'confirm-stopped', { proof: p, effects: e }), bad('stop-proof'));
+    assert.equal(s.state, 'fenced'); assert.equal(w.binding.state, 'stopping');
+    assert.equal(server(w, 'advance-stop', { state: 'uncertain' }), 'uncertain'); assert.equal(w.binding.state, 'uncertain');
+    const id = confirmation(w, 'force-stop');
+    assert.equal(evaluate(w, command(w, 'force-stop', 'connection-1', { confirmation: id })), 'force-stop-fenced');
+    const force = w.stops.at(-1); assert.equal(force.supersedes, s.id); assert.equal(s.state, 'superseded');
+    assert.equal(server(w, 'confirm-stopped', { proof: trustedProof(w, 'cohortProof', force.id), effects: trustedProof(w, 'effectReport', force.id) }), 'stopped');
+  }
+});
+sequence('engine-exit-stale-confirmation-dispatched-receipt', () => {
+  const w = clone(f.world), r = command(w, 'prompt'); assert.equal(evaluate(w, r), 'queued'); const q = w.queue.at(-1);
+  assert.equal(dispatch(w, q.id), 'dispatched'); const old = confirmation(w, 'force-stop');
+  const busy = { ...clone(q), id: 'queue-working', state: 'working' }; w.queue.push(busy);
+  assert.equal(server(w, 'engine-exit'), 'engine-exit-fenced');
+  assert.equal(q.state, 'delivery-unknown'); assert.equal(busy.state, 'working'); assert.equal(w.queue[0].state, 'recovered-as-draft'); assert.equal(w.outbox.length, 1);
+  assert.equal(evaluate(w, r), 'existing:delivery-unknown');
+  assert.equal(evaluate(w, command(w, 'force-stop', 'connection-1', { confirmation: old })), bad('confirmation'));
+  assert.equal(w.stops.at(-1).mode, 'engine-exit');
+});
+sequence('engine-exit-refused-during-force-stop', () => {
+  const w = clone(f.world); const id = confirmation(w, 'force-stop');
+  assert.equal(evaluate(w, command(w, 'force-stop', 'connection-1', { confirmation: id })), 'force-stop-fenced');
+  const s = w.stops.at(-1), pending = confirmation(w, 'force-stop'), events = w.events.length, stops = w.stops.length;
+  for (const state of ['fenced', 'cancelling', 'stopping', 'uncertain']) {
+    if (state !== 'fenced') assert.equal(server(w, 'advance-stop', { state }), state);
+    assert.equal(server(w, 'engine-exit'), bad('stop-owned'));
+    assert.equal(w.binding.stop, s.id); assert.equal(w.stops.length, stops); assert.equal(w.events.length, events);
+  }
+  assert.equal(evaluate(w, command(w, 'force-stop', 'connection-1', { confirmation: pending })), 'force-stop-fenced');
+  assert.equal(w.stops.at(-1).supersedes, s.id);
+});
+sequence('engine-exit-binding-follows-stop', () => {
+  const w = clone(f.world); assert.equal(server(w, 'engine-exit'), 'engine-exit-fenced');
+  const seen = [w.binding.state];
+  for (const state of ['cancelling', 'stopping', 'uncertain']) { assert.equal(server(w, 'advance-stop', { state }), state); seen.push(w.binding.state); }
+  const s = w.stops.at(-1);
+  assert.equal(server(w, 'confirm-stopped', { proof: trustedProof(w, 'cohortProof', s.id), effects: trustedProof(w, 'effectReport', s.id) }), 'stopped'); seen.push(w.binding.state);
+  assert.deepEqual(seen, ['stopping', 'stopping', 'stopping', 'uncertain', 'stopped']);
+});
 console.log('Additional regressions PASS: queue recovery, immutable queue edit, safe bootstrap and multipart snapshot/event reconstruction');
 assert.deepEqual(results, f.sequences);
 console.log(`CHAT-01 R3 PASS: ${f.shapeCases.length} shape cases, ${f.stateCases.length} reference cases, ${results.length} lifecycle sequences. All synthetic; runtime/authentication/protocol/cohort evidence producers NOT VERIFIED.`);

docs/plans/chat-01/contracts.schema.json

@@ -2620,7 +2620,8 @@
           "enum": [
             "interrupt",
             "force-stop",
-            "revocation"
+            "revocation",
+            "engine-exit"
           ]
         },
         "state": {

docs/plans/chat-01/fixtures.json

@@ -991,6 +991,8 @@
   {"id":"valid-approval","valid":true,"value":{"version":2,"kind":"approval","id":"approval-1","target":{"conversation":"conversation-1","branch":"branch-1","execution":"execution-1","controllerGeneration":2},"nativeRequest":"native-approval-1","toolCall":"call-1","tool":"read","intentDigest":"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa","policyRevision":"policy-1","choices":[{"id":"deny","label":"Deny","nativeChoice":"native-deny","effect":"deny","enabled":true,"disabledReason":null,"cancelSafety":"not-cancel","mappingEvidence":null},{"id":"once","label":"Allow once","nativeChoice":"native-once","effect":"allow-once","enabled":true,"disabledReason":null,"cancelSafety":"not-cancel","mappingEvidence":null},{"id":"always","label":"Allow for session","nativeChoice":"native-always","effect":"permission-change","enabled":false,"disabledReason":"policy-expansion-not-authorized","cancelSafety":"not-cancel","mappingEvidence":null},{"id":"cancel","label":"Cancel","nativeChoice":"native-cancel","effect":"cancel","enabled":false,"disabledReason":"cancel-native-outcome-unverified","cancelSafety":"unverified","mappingEvidence":null}],"state":"pending","deadline":null,"chosen":null,"createdAt":"2026-09-13T12:00:00Z","decision":"decision-1","resolvedBy":null,"dialogForm":"permission","intentDisplay":{"text":"Synthetic request: read approved file example.txt","visibility":"available","complete":true},"unsupportedReason":null}},
   {"id":"valid-confirmation","valid":true,"value":{"version":2,"kind":"confirmation","id":"confirmation-1","actor":"actor-1","connection":"connection-1","target":{"conversation":"conversation-1","branch":"branch-1","execution":"execution-1","controllerGeneration":2},"operation":"force-stop","intentDigest":"0ec8416f50478fe507fd3a1ec755082a4cb4cb277c7860652893ede80a7de066","expiresAt":"2026-09-13T12:01:00Z","state":"confirmed","connectionGeneration":1,"stop":null}},
   {"id":"valid-stop","valid":true,"value":{"version":2,"kind":"stop","id":"stop-1","request":"request-1","target":{"conversation":"conversation-1","branch":"branch-1","execution":"execution-1","controllerGeneration":2},"mode":"force-stop","state":"stopped","queueDrafts":["draft-1"],"cohortRef":"cohort-1","supervisorEvidence":"proof-1","effectsEvidence":"effects-1","externalEffects":"uncertain","createdAt":"2026-09-13T12:00:00Z","nativeQueue":"cleared","approvalDisposition":"cancelled","turnEvidence":"turn-proof-1","supersedes":null,"queueFailures":[],"revokedConnection":null}},
+  {"id":"valid-engine-exit-stop","valid":true,"value":{"version":2,"kind":"stop","id":"stop-1","request":null,"target":{"conversation":"conversation-1","branch":"branch-1","execution":"execution-1","controllerGeneration":2},"mode":"engine-exit","state":"fenced","queueDrafts":[],"cohortRef":"cohort-1","supervisorEvidence":null,"effectsEvidence":null,"externalEffects":"uncertain","createdAt":"2026-09-13T12:00:00Z","nativeQueue":"pending","approvalDisposition":"pending","turnEvidence":null,"supersedes":null,"queueFailures":[],"revokedConnection":null}},
+  {"id":"refuse-stop-mode-eof","valid":false,"value":{"version":2,"kind":"stop","id":"stop-1","request":null,"target":{"conversation":"conversation-1","branch":"branch-1","execution":"execution-1","controllerGeneration":2},"mode":"eof","state":"fenced","queueDrafts":[],"cohortRef":"cohort-1","supervisorEvidence":null,"effectsEvidence":null,"externalEffects":"uncertain","createdAt":"2026-09-13T12:00:00Z","nativeQueue":"pending","approvalDisposition":"pending","turnEvidence":null,"supersedes":null,"queueFailures":[],"revokedConnection":null}},
   {"id":"valid-frozenPayload","valid":true,"value":{"version":2,"kind":"frozenPayload","id":"payload-1","actor":"actor-1","conversation":"conversation-1","branch":"branch-1","draft":"draft-1","draftRevision":1,"text":"hello","uploads":[{"version":2,"kind":"upload","id":"upload-1","actor":"actor-1","conversation":"conversation-1","revision":1,"filename":"example.png","mimeType":"image/png","size":20,"digest":"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa","state":"staged","privateBlobRef":"blob-1","recipientScope":{"host":"host-1","seat":"seat-1","project":"project-1","workspace":"workspace-1","conversation":"conversation-1"},"transferAck":null,"createdAt":"2026-09-13T12:00:00Z","receivedBytes":20}],"digest":"4e06080f131b6e7d87e692ffebe8ccd1f78e25aedc24a10aaf68e7c3191f9f48","createdAt":"2026-09-13T12:00:00Z"}},
   {"id":"valid-nativeDecision","valid":true,"value":{"version":2,"kind":"nativeDecision","id":"decision-1","conversation":"conversation-1","branch":"branch-1","execution":"execution-1","nativeRequest":"native-approval-1","toolCall":"call-1","intentDigest":"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa","policyRevision":"policy-1","state":"pending","chosen":null,"resolvedBy":null,"nativeEvidence":null}},
   {"id":"valid-cohortProof","valid":true,"value":{"version":2,"kind":"cohortProof","id":"proof-1","authority":"supervisor-1","conversation":"conversation-1","execution":"execution-1","cohortRef":"cohort-1","membershipEpoch":"membership-1","membershipComplete":true,"members":[{"pid":101,"boot":"boot-1","startTicks":20,"terminatedAt":"2026-09-13T11:59:59Z"}],"observedAt":"2026-09-13T12:00:00Z","verificationDigest":"c85edd0f8ccfd03d41f738f7296dd8737777345cc8eb91eaa24870cd2cb53b46","stop":"stop-1"}},
@@ -1750,7 +1752,12 @@
   "native-resolution-requires-evidence",
   "confirmation-predecessor-and-supersession",
   "different-actor-draft-privacy",
-  "empty-history-new-user-assistant-roles"
+  "empty-history-new-user-assistant-roles",
+  "engine-exit-empty-cohort-stopped",
+  "engine-exit-live-unreadable-or-empty-cohort-uncertain",
+  "engine-exit-stale-confirmation-dispatched-receipt",
+  "engine-exit-refused-during-force-stop",
+  "engine-exit-binding-follows-stop"
 ],
 "streamRecords": [
   {