The controller now starts a CHAT-01 `engine-exit` stop when the engine exits on its own. engineExitCohort proves the cohort from the shim's recorded engine identity (pid, start ticks, boot) and an empty member list, under a 5 s deadline that frees the escalation slot. A proven stop releases the scope; anything else ends `uncertain`. close() no longer signals a stopped binding. Dewey built it. Filbert (27087) and Darkwing (27088) approved round 1 on CHAT-01cc83ee4fand manifest deac7434 (6 files). Sage's gate onc92cfb8fplus the candidate: conversation 182/0, webui 22/0, control-board 124/0, every scripts/test-*.sh 0 failed (task 98/0), chat-01 PASS. Co-Authored-By: Claude Opus 5.5 <[email protected]>
14 KiB
Row 52 (#1538): CHAT-01 engine-exit stop and release at engine exit
Dewey, 2026-10-10. Brief: docs/plans/2026-10-10_cohort-release-follow-ups.md,
section "CHAT-01 engine-exit stop and release at engine exit" (rev 297).
Base 945440db (row 51 landed). The change has two parts, CHAT-01 first in
its own commit:
- CHAT-01 (commit
cc83ee4f, not pushed): the fourdocs/plans/chat-01/files. - Conversation (candidate, uncommitted):
src/cohort.mjs,src/controller.mjs,src/shim.mjs,tests/cohort.test.mjsand the package README.tests/ctrl-child.mjsis unchanged.
CHAT-01 hashes (each approval names all four)
a41fc4e2edb11371c275e3167774c162254e1457fd737121630dedd665431889 docs/plans/chat-01/README.md
ccceaf2653b279f5890748b40d16fae7493f199a33cecee035f82b92e80243af docs/plans/chat-01/check.mjs
941675de949c52c7fe7c4b7bcce3aff48bb26ccc1120e090574c5d25f9d9e22e docs/plans/chat-01/contracts.schema.json
c75c2b9f731bb70d0e033e8aa56f2c28accfa09384ec964fd3ecbd45974b2a7d docs/plans/chat-01/fixtures.json
node docs/plans/chat-01/check.mjs: 100 shape cases, 76 reference cases,
22 lifecycle sequences, PASS. node docs/plans/chat-00/check.mjs: 48 checks
PASS.
Darkwing's points 1–4
| Point | Model (check.mjs) |
Conversation |
|---|---|---|
| 1. Never supersede an unfinished force stop | engine-exit returns stop-owned while the current stop is a force stop (any state) or an engine exit. Sequence engine-exit-refused-during-force-stop walks all four force-stop states. |
#engineExit starts nothing while escalating is held or the current stop is a force stop or engine exit: a running force stop (E3, second half) and one that ended uncertain before it closed the execution (E5). |
| 2. Binding follows at lines 121, 334, 337 | All three use ending(mode) (force stop or engine exit). Sequence engine-exit-binding-follows-stop: stopping at the fence and on each advance, uncertain with the stop, stopped only with it. |
#startStop and #advanceStop use the same ending (E3 sees stopping at engine-exit-recorded). |
3. The proof names the engine; not members: [] |
stopped(w, s) refuses an engine-exit proof with no member. The empty-list case is in engine-exit-live-unreadable-or-empty-cohort-uncertain. |
engineExitCohort returns the engine as the one member: PID and start ticks the shim recorded, boot, and the shim's reap time as terminatedAt. #stopped also refuses an engine-exit proof with no member. E1 checks the members exactly; E6 checks that another PID or start ticks is refused. |
| 4. The proof's deadline frees the slot | The model leaves the slot to the implementation (README says so). | The observation runs under within(…, exitProof). A miss ends the stop uncertain, and finally frees escalating. E4 SIGSTOPs the shim: the stop ends uncertain at the deadline, escalating is null, and a client force stop then proves and releases. |
Engine identity comes from a shim op
Sage's condition: if the engine identity can't come from a shim op, stop
before relying on members: []. It comes from one. The shim reads the
engine's start ticks from /proc right after spawn (the exec chain keeps
the PID and start time), and its exit handler records { code, signal, at, pid, startTicks, boot }. hello returns that as engineExit.
engineExitCohort refuses, as unavailable, an engineExit whose PID or
start ticks differ from the claim's recorded engine, whose start ticks
aren't a positive integer, or whose boot differs from the shim's. Nothing
relies on an empty member list: the force stop's proof (R4, now in E4) is
unchanged and still lists no member when the engine has already gone.
CHAT-01 change
- Stop mode
engine-exit(schema enum). The server starts it like a revocation fence:request: null, no confirmation. server(w, 'engine-exit'): refusesstop-ownedunder a force stop or another engine exit; otherwisestartStop(closes admission, recovers queued drafts, marks pending decisions uncertain, supersedes an unfinished interrupt or revocation, emitsstopping). Dispatched or acknowledged input moves todelivery-unknown;workinginput keeps its state.confirm-stoppedaccepts it under the samestopped(w, s)check as a force stop, plus at least one member.- Recover after it needs its own confirmation bound to the stop (K6, K17,
K18): an unissued one, one issued but not confirmed, and the binding's
stop check are all in
engine-exit-empty-cohort-stopped. - Fixtures:
valid-engine-exit-stop,refuse-stop-mode-eof, and five sequences: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. - README: a paragraph under "Control loss, approvals and stopping", a pointer near the top, and the R3 counts. "SIGTERM, EOF, abort acknowledgment or idle does not prove death" stays; K15 and K2 are unchanged.
Model mutants (check.mjs on a scratch copy)
| Mutant | Change | Result |
|---|---|---|
| norefuse | engine-exit never refuses stop-owned |
killed |
| optionB | refuses only while the force stop is unfinished | killed |
| bind121 | startStop moves the binding only for a force stop |
killed |
| bind334 | advance-stop the same |
killed |
| bind337 | confirm-stopped accepts only a force stop |
killed |
| emptyok | no member-count check for an engine exit | killed |
| noreceipt | dispatched input keeps its state | killed |
| nostale | no current-stop check on a confirmation | killed |
Conversation change
#onEnd(EOF): after#transport(which settles in-flight inputdelivery-unknown/transport-unknownas before, H19, N18), starts#engineExit.#engineExit: only for the current execution with a recorded engine, no held slot and no current force stop or engine exit. Starts theengine-exitstop, takesescalating, pauses atengine-exit-recorded(test barrier), runsengineExitCohortunder theexitProofdeadline (5000 ms;exitSettle2000 ms for EOF before the reap), then goes touncertainor through#stopProven.#endStopUncertainand#stopProvenare#escalate's formerfailand proof tail, shared. The force-stop path is unchanged: same order, same claim writes,resumedstill in its evidence. Evidence and the release now carrystop.modeinstead of a literalforce-stop.engineExitCohort(cohort.mjs): reads only (hello,events,members), never freezes or kills. Proven when the shim has reaped the recorded engine,enginereadspopulated 0and no member is listed.- The claim: no
stoppingclaim write for an engine exit. The claim goesuncertainat EOF (#transport, as before) andstoppedonly through#claimFinishwith the proof. A restart in between finds an ordinaryuncertainorphan, never an engine-exit stop to resume.
Tests (cohort.test.mjs, needs a systemd user manager)
R4 is folded into E4; E1–E6 are new.
- E1: the engine exits with no other member. One
engine-exitstop,request: null, superseding the prior stop,stopped; the proof's members are exactly the engine (PID, boot, start ticks, reap time from the shim'shello); both claim keys stopped on it; the release isengine-exit/released/absentand the unit is gone. A recover confirmation issued before the exit is refused; a fresh one isrecovery-eligible. - E2: the engine exits while a tool child runs. The stop ends
uncertain(evidenceengine-exit/uncertain), no release, the unit and the child live, no proof. A force-stop confirmation issued before the exit is refused (H17). A fresh force stop supersedes the engine-exit stop, kills the child, proves and releases. - E3: one slot, both orders. The engine-exit stop held at
engine-exit-recorded: a client force stop is refusedfenced, and the engine exit then proves. A force stop held atforce-stop-recorded: the engine's EOF starts no engine-exit stop, and only the force stop is in the evidence. - E4: the shim SIGSTOPped. The engine-exit stop misses its deadline, ends
uncertain(reason names the deadline),escalatingisnull; after SIGCONT a force stop proves with no member (the R4 assertion) and the scope goes. - E5: a force stop whose
stoppingclaim write fails once endsuncertainbefore it closes the execution, so the engine's later EOF still reaches#onEnd. No engine-exit stop starts; the force stop stays current (point 1 after the slot is free). - E6: held at
engine-exit-recorded,engineExitCohortwith another PID or other start ticks isunavailable("the shim reaped a process that isn't the recorded engine"); the recorded identity isproven, and the controller's stop then proves.
Conversation suite on the draft at 945440db: 182/182 (was 177: R4 out,
E1–E6 in).
Mutation check
Twenty mutants on a fresh copy of the candidate, full conversation suite
each (~/dewey-scratch/r52/mut-tools). Run 1 (07:11–07:33Z) was on the
tests before E5, E6 and the E2 evidence check, and left noowncheck,
noident and evmode alive with the five equivalents. I added those
tests and ran all twenty again (run 2, 07:33–07:54Z). Run 2 base:
182/182. No shim, engine or mosaic-chat-* unit was left after any run.
| Mutant | Change | Run 2 | Killed by |
|---|---|---|---|
| noexit | #onEnd doesn't start #engineExit |
killed | E1, E2, E3, E4, E6 |
| noslottake | the engine-exit stop doesn't take escalating |
killed | E3 |
| nofree | finally doesn't free the slot |
killed | E2, E4 |
| noslotcheck | EOF ignores a held slot | survives, equivalent | – |
| noowncheck | EOF ignores a current force stop or engine exit | killed | E5 |
| nostopcheck | both checks gone | killed | E3, E5 |
| nodeadline | the observation has no deadline | killed | E4 |
| bindstart | #startStop moves the binding only for a force stop |
killed | E3 |
| bindadvance | #advanceStop the same |
survives, equivalent | – |
| emptyguard | #stopped accepts an engine-exit proof with no member |
survives, equivalent alone | – |
| emptyproof | the proof lists no member | killed | E1 |
| emptyboth | both: an empty-list proof that verifies | killed | E1 |
| noident | no PID or integer check on the shim's engineExit |
killed | E6 |
| nopopulated | a populated engine cgroup proves |
survives, equivalent | – |
| nomembers | a listed member proves | survives, equivalent | – |
| nolive | neither is read | killed | E2 |
| shimstart | the shim keeps no start ticks | killed | E1, E3, E6 |
| relwhy | the release is recorded as a force stop's | killed | E1 |
| evmode | uncertain evidence names a force stop | killed | E2 |
Why the five survivors are equivalent:
- noslotcheck:
escalatingis set only right after#startStopmade a force stop or engine exit the current stop, and the binding is thenstopping. Interrupt and revocation needb.state === "active"(controller.mjs#interruptLocked, the revocation in the connection close), so no other stop replaces it while the slot is held.ending(…)covers every state the slot check covers. The check stays as a guard. - bindadvance: the binding is already
stoppingfrom#startStop;#uncertainkeepsstopping;#endStopUncertainand#stopProvenset the binding themselves. Theendingin#advanceStopstays to match the model's line 334. - emptyguard: a proven
engineExitCohortalways lists the engine, so#stopped's guard is reachable only through a second fault. emptyproof and emptyboth test point 3. - nopopulated, nomembers: the shim's
memberswalksengineand its descendants, sopopulated 1with an empty list (orpopulated 0with a member) needs a process to start or exit between the two reads. Both reads stay; each guards the other.
Killing tests are from each mutant's failing tests: list. Run 1 and run 2
tables: ~/dewey-scratch/r52/mut-tools/results-run1.txt and
results-run2.txt.
Gate
Run in a scratch worktree at cc83ee4f with the candidate applied
(~/dewey-scratch/r52/gate/candidate.diff), 2026-10-10T07:56:23Z to
08:01:22Z, sequential, each output kept.
| Suite | rc | Result |
|---|---|---|
node docs/plans/chat-01/check.mjs |
0 | PASS: 100 shape, 76 reference, 22 lifecycle |
| conversation | 0 | 182 pass, 0 fail |
| webui | 0 | 22 pass, 0 fail |
| control-board | 0 | 124 pass, 0 fail |
test-auth.sh |
0 | 15 passed, 0 failed |
test-conductor.sh |
0 | 17 passed, 0 failed |
test-config.sh |
0 | 24 passed, 0 failed |
test-discord.sh |
0 | 66 passed, 0 failed |
test-extension-package.sh |
0 | 18 passed, 0 failed |
test-foundation.sh |
0 | 44 passed, 0 failed |
test-queue.sh |
0 | 148 node pass, suite 27 passed, 0 failed; queue verify and render --check skipped (not the canonical root) |
test-release.sh |
0 | 14 passed, 0 failed |
test-task.sh |
0 | 98 passed, 0 failed |
The test-queue.sh skip is that suite's own guard for a non-canonical
checkout; Sage's rerun in the canonical checkout covers it. After the
gate and the mutant runs no mosaic-chat-* unit is listed
(systemctl --user list-units --all 'mosaic-chat-*') and core.hooksPath
is unset.
Not tested, follow-ups
Nothing here blocks the row; I'd file them together if Sage wants them.
- The boot comparison in
engineExitCohort(exit.boot !== hello.boot) is untested: both come from the same shim process, so only a fakedhelloreaches it. - An unreadable
engine/cgroup.eventsor a failedmembersduring the engine-exit observation (the K15 shapes) is untested for this path. The tests reachunavailableonly through the deadline (E4). - On the process-group fallback a natural exit now starts an
engine-exitstop that endsuncertainat once ("a pgroup cohort can't be enumerated completely"). The binding endsuncertainas it did before row 52, but no test runs it. - The five equivalent mutants above are guards I kept on purpose; no change proposed.
- Row 51's untested
still listedretry and the noseat and recafteracq survivors are #1539, not repeated here.