jason.woltjeandClaude Opus 5.5
0aa5e7b51b
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]>
246 lines
14 KiB
Markdown
246 lines
14 KiB
Markdown
# 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 four `docs/plans/chat-01/` files.
|
||
- Conversation (candidate, uncommitted): `src/cohort.mjs`,
|
||
`src/controller.mjs`, `src/shim.mjs`, `tests/cohort.test.mjs` and the
|
||
package README. `tests/ctrl-child.mjs` is 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')`: refuses `stop-owned` under a force stop or
|
||
another engine exit; otherwise `startStop` (closes admission, recovers
|
||
queued drafts, marks pending decisions uncertain, supersedes an
|
||
unfinished interrupt or revocation, emits `stopping`). Dispatched or
|
||
acknowledged input moves to `delivery-unknown`; `working` input keeps its
|
||
state.
|
||
- `confirm-stopped` accepts it under the same `stopped(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 input
|
||
`delivery-unknown`/`transport-unknown` as 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 the
|
||
`engine-exit` stop, takes `escalating`, pauses at `engine-exit-recorded`
|
||
(test barrier), runs `engineExitCohort` under the `exitProof` deadline
|
||
(5000 ms; `exitSettle` 2000 ms for EOF before the reap), then goes to
|
||
`uncertain` or through `#stopProven`.
|
||
- `#endStopUncertain` and `#stopProven` are `#escalate`'s former `fail` and
|
||
proof tail, shared. The force-stop path is unchanged: same order, same
|
||
claim writes, `resumed` still in its evidence. Evidence and the release
|
||
now carry `stop.mode` instead of a literal `force-stop`.
|
||
- `engineExitCohort` (cohort.mjs): reads only (`hello`, `events`,
|
||
`members`), never freezes or kills. Proven when the shim has reaped the
|
||
recorded engine, `engine` reads `populated 0` and no member is listed.
|
||
- The claim: no `stopping` claim write for an engine exit. The claim goes
|
||
`uncertain` at EOF (`#transport`, as before) and `stopped` only through
|
||
`#claimFinish` with the proof. A restart in between finds an ordinary
|
||
`uncertain` orphan, 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-exit` stop,
|
||
`request: null`, superseding the prior stop, `stopped`; the proof's
|
||
members are exactly the engine (PID, boot, start ticks, reap time from
|
||
the shim's `hello`); both claim keys stopped on it; the release is
|
||
`engine-exit`/`released`/`absent` and the unit is gone. A recover
|
||
confirmation issued before the exit is refused; a fresh one is
|
||
`recovery-eligible`.
|
||
- E2: the engine exits while a tool child runs. The stop ends `uncertain`
|
||
(evidence `engine-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 refused `fenced`, and the
|
||
engine exit then proves. A force stop held at `force-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), `escalating` is `null`; after
|
||
SIGCONT a force stop proves with no member (the R4 assertion) and the
|
||
scope goes.
|
||
- E5: a force stop whose `stopping` claim write fails once ends `uncertain`
|
||
before 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`, `engineExitCohort` with another PID
|
||
or other start ticks is `unavailable` ("the shim reaped a process that
|
||
isn't the recorded engine"); the recorded identity is `proven`, 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: `escalating` is set only right after `#startStop` made a
|
||
force stop or engine exit the current stop, and the binding is then
|
||
`stopping`. Interrupt and revocation need `b.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 `stopping` from `#startStop`;
|
||
`#uncertain` keeps `stopping`; `#endStopUncertain` and `#stopProven`
|
||
set the binding themselves. The `ending` in `#advanceStop` stays to match
|
||
the model's line 334.
|
||
- emptyguard: a proven `engineExitCohort` always 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 `members` walks `engine` and its
|
||
descendants, so `populated 1` with an empty list (or `populated 0` with
|
||
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 faked
|
||
`hello` reaches it.
|
||
- An unreadable `engine/cgroup.events` or a failed `members` during the
|
||
engine-exit observation (the K15 shapes) is untested for this path. The
|
||
tests reach `unavailable` only through the deadline (E4).
|
||
- On the process-group fallback a natural exit now starts an
|
||
`engine-exit` stop that ends `uncertain` at once ("a pgroup cohort
|
||
can't be enumerated completely"). The binding ends `uncertain` as 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 listed` retry and the noseat and recafteracq
|
||
survivors are #1539, not repeated here.
|