fix(sshx): tear down the carrier's process tree on interruption

skills/sshx/CODEX_WORKER_SPEC.md

@@ -178,9 +178,10 @@ when that wait's own return status equals the recorded signal status. It joins
 every recorded child before publication. It then publishes the report with
 `interrupted: true` and exits nonzero when a signal was recorded. This preserves
 ownership of recorded children but does not promise prompt cancellation or
-carrier teardown. The runner may itself defer traps during its synchronous
-carrier call and does not propagate signals, so teardown of the whole job tree
-remains the host's responsibility.
+carrier teardown from a dispatcher-only signal. The host signals each runner
+for cancellation; on a trappable `INT` or `TERM`, each runner tears down its own
+carrier tree before publishing `INTERRUPTED`. Time limits and signalling the
+runners remain the host's responsibility.
 
 The dispatcher's `INT` half has the same inherited-disposition limit as its
 children: if the host starts it with `SIGINT` ignored, Bash cannot make its
@@ -363,23 +364,35 @@ terminal status intentionally leaves its flight ineligible.
 ## Carrier
 
 After `jq`, directory, brief, log, and executable `codex` preflight checks, the
-runner performs one synchronous foreground call:
+runner launches one carrier as its own background job, records `carrier_pid=$!`,
+and joins it with the Bash `wait` builtin:
 
 ```text
 codex exec --json -C <work-target> --sandbox <sandbox> \
   --skip-git-repo-check -o <last-message.txt> -
 ```
 
-The command's stdout and stderr go to the fixed diagnostic logs. There is no
-timeout, supervisor, helper, PID state, signal propagation, process-group
-handling, or KILL escalation. The carrier wait status is written atomically to
+The command's stdout and stderr go to the fixed diagnostic logs, and stdin
+comes from the same brief. The runner remains attached to its host job while
+waiting. On normal return, the carrier wait status is written atomically to
 `carrier.exit`. A missing executable is `LAUNCH_FAILED`; once invoked, any
 nonzero carrier status is `CARRIER_EXIT_NONZERO`.
 
-`INT` and `TERM` traps set `reason_code=INTERRUPTED` and exit through the
-normal `EXIT` trap. Bash may defer these traps while the synchronous foreground
-command is running. The runner does not promise signal reachability in every
-phase and does not tear down descendants.
+`pgrep` is required before carrier launch. On a trappable `INT` or `TERM`, the
+runner ignores further `INT` and `TERM`, records `reason_code=INTERRUPTED`, and
+recursively collects the carrier's descendants with `pgrep -P`. It retains that
+snapshot before sending individual `TERM` signals to descendants, deepest
+first, and then to the carrier. It polls the recorded PIDs for up to fifty
+0.1-second grace intervals, sends individual `KILL` signals to those still
+present, and reaps its direct carrier before the existing `finish` path
+publishes terminal status. It does not signal process groups or processes
+outside the recorded carrier tree. A descendant-discovery or signal-delivery
+failure emits a diagnostic; `pgrep` exit 1 means no children.
+
+Teardown does not write `carrier.exit` or replace `carrier_exit` with its own
+wait result. The normal artifact validation and completion predicate retain
+their existing order. A signal during terminal publication remains ignored so
+publication cannot be interrupted. There is no runner-owned time limit.
 
 ## Status Projection
 
@@ -392,6 +405,15 @@ references, `started_at`, `finished_at`, `duration_seconds`, `work_target`,
 both lookups succeed. A failed time lookup writes `null` and does not fail the
 flight.
 
+An interrupted run additionally contains `teardown`, an object with integer
+`descendants_signalled` and `killed_after_grace` counts. The first counts
+successful descendant `TERM` sends, excluding the carrier; the second counts
+successful `KILL` sends after grace, including the carrier. These are signal
+send counts, not proof that every process is reaped: Bash reaps only its direct
+carrier, and an orphan zombie can remain present until the system reaper runs.
+A normal run omits `teardown`. The timestamped teardown log line carries the
+same counts.
+
 Exit code is the sole authority: `0` means complete, `1` means not complete,
 and `64` means usage error. `status.json` is a terminal, machine-readable
 projection for callers that need structured data. stdout is a human-readable
@@ -401,9 +423,9 @@ parseable, and is not byte-for-byte identical to any file.
 `status.json` and the batch report are mechanical projections only. Neither is
 a completion or verdict source under `SKILL.md`.
 
-Before the synchronous carrier call, stdout reports all then-known invocation
-identity and derived artifact paths followed by `carrier starting`. After the
-call returns, it reports the carrier exit status; terminal cleanup then reports
+Before carrier launch, stdout reports all then-known invocation identity and
+derived artifact paths followed by `carrier starting`. After the normal wait
+returns, it reports the carrier exit status; terminal cleanup then reports
 `status`, `reason_code`, `verdict`, and duration. Every stdout line begins with
 a UTC ISO-8601 timestamp. stdout write failure is diagnostic only and cannot
 change the authoritative exit decision.
@@ -433,7 +455,8 @@ contains invocation identity, `status` (`COMPLETE` or
 `NOT_COMPLETE`), `reason_code`, `carrier_exit` (or `null`), derived artifact
 references, diagnostic log references, the six fields `started_at`,
 `finished_at`, `duration_seconds`, `work_target`, `sandbox`, and `brief_ref`,
-and a verdict only when the stage has a verdict mapping. Before either
+a verdict only when the stage has a verdict mapping, and the interruption-only
+`teardown` counts described above. Before either
 runner-owned projection is written, its temporary
 and final target must be absent or a non-symbolic-link regular file. After each
 rename, the fixed `carrier.exit` or `status.json` path must be a non-symbolic-link
@@ -458,17 +481,20 @@ the POSIX text-line contract.
 
 ## Teardown Prerequisite
 
-Verified in two independent Claude Code harness experiments: `TaskStop`
-terminates the entire process tree, including a child that actively ignores
-`TERM` and `INT`; this indicates the harness uses SIGKILL or process-group
-teardown. The runner therefore does not propagate signals.
-
-Codex, Cursor, and Gemini host teardown behavior is unverified. An interactive
-Ctrl-C normally sends `INT` to the foreground process group, which includes the
-synchronous carrier. A default `TERM` sent only to the runner PID may be
-deferred by Bash until the foreground carrier returns. An uncatchable `SIGKILL`
-sent only to the runner PID can leave the carrier orphaned and running. The
-runner does not attempt to compensate for any of these host behaviors.
+The host owns time limits and delivery of cancellation signals to the runner
+itself, including each runner in a batch. The runner owns teardown of its own
+carrier tree on trappable `INT` and `TERM`; the background carrier and builtin
+`wait` let the handler run while the carrier is alive. A `TERM` sent only to
+the runner PID therefore initiates carrier-tree teardown without waiting for
+normal carrier exit.
+
+Bash cannot trap a signal inherited as ignored, including `INT` on a normal
+non-job-control background launch. The host uses a trappable signal for runner
+cancellation. An uncatchable `SIGKILL` sent only to the runner PID can leave the
+carrier orphaned and running; host teardown remains necessary for uncatchable
+termination. The runner contract does not assume that any particular host
+already kills descendants. Codex, Cursor, and Gemini host teardown behavior
+remains unverified.
 
 ## Threat Model
 
@@ -478,18 +504,21 @@ missing artifacts, and accidental projection-path type collisions, but it is
 not a sandbox against a hostile carrier. This design does not defend TOCTOU
 races, including caller-brief replacement after the dispatcher's readability
 probe or flight changes after cleanup's repeated eligibility check; those checks
-narrow their respective windows but do not make object identity immutable. It
-also does not defend an active `setsid` escape, forged runner artifact paths, or
-deliberate replacement of files inside the owned attempt directory. An
+narrow their respective windows but do not make object identity immutable.
+Process-tree discovery is a PID snapshot, not an atomic process-ownership
+boundary: concurrent forks, reparenting, and PID reuse are outside its
+guarantee. It also does not defend an active `setsid` escape, forged runner
+artifact paths, or deliberate replacement of files inside the owned attempt directory. An
 untrusted carrier or a requirement to cover those attacks requires a new design
 review rather than more checks in this runner.
 
 ## Boundaries
 
 The runner has no git, GitHub, label, release, host lifecycle, cleanup, or
-global-state authority. Time limits and whole-job teardown belong to the
-caller harness. Power-loss durability is not guaranteed. Deletion authority
-lives only in `clean-codex-worker-runs.sh` and is bounded to terminal-only,
+global-state authority. Time limits, signalling the runner itself, and teardown
+after uncatchable termination belong to the caller harness. The runner's
+catchable-signal teardown authority is limited to its own carrier tree.
+Power-loss durability is not guaranteed. Deletion authority lives only in `clean-codex-worker-runs.sh` and is bounded to terminal-only,
 whole-flight artifact retirement with dry-run default and no force override.
 
 No other skill may depend on these mechanisms. To reverse the exception

skills/sshx/SKILL.md

@@ -131,13 +131,13 @@ Every worker dispatch must create a prompt-level `SshxWorkerFlightRecord` before
 
 While any `SshxWorkerFlightRecord` for the same `work_target` is `in-flight` or `retrying`, the caller is read-only for that target. The caller is non-mutating for that target and its external resources. The caller must not take over the same `work_target` because a process snapshot, log text, or workspace state appears quiet.
 
-For each `codex-cli` attempt, before launch the caller must choose a unique `flight_id` and `attempt` and pass them to `skills/sshx/scripts/run-codex-worker.sh`; the runner derives and owns every artifact path, parallel attempts receive disjoint derived paths, and the caller must not supply arbitrary result, sentinel, log, or state paths. Every formal `codex-cli` flight must use this runner rather than a parallel direct-launch path. The command, sandbox, path, direct-process, and collection mechanics are owned by `CODEX_WORKER_SPEC.md`; the required dispatch shape is the runner's default `danger-full-access` sandbox, so the caller passes no sandbox selection unless the maintainer explicitly directs a narrower one. Time limits and final teardown of the whole job tree are the caller AI harness's responsibility. The caller must not poll worker artifact paths while the runner is active. The caller records `result_envelope_ref` and `completion_sentinel_ref` on the matching flight only if the runner reports completion and the envelope and sentinel validate. Completion and verdict recognition stay governed by the `## Worker Completion Contract`.
+For each `codex-cli` attempt, before launch the caller must choose a unique `flight_id` and `attempt` and pass them to `skills/sshx/scripts/run-codex-worker.sh`; the runner derives and owns every artifact path, parallel attempts receive disjoint derived paths, and the caller must not supply arbitrary result, sentinel, log, or state paths. Every formal `codex-cli` flight must use this runner rather than a parallel direct-launch path. The command, sandbox, path, direct-process, and collection mechanics are owned by `CODEX_WORKER_SPEC.md`; the required dispatch shape is the runner's default `danger-full-access` sandbox, so the caller passes no sandbox selection unless the maintainer explicitly directs a narrower one. Time limits, signalling the runner itself, and teardown after uncatchable termination are the caller AI harness's responsibility; the runner owns teardown of its own carrier tree on trappable `INT` and `TERM` as specified in `CODEX_WORKER_SPEC.md`. The caller must not poll worker artifact paths while the runner is active. The caller records `result_envelope_ref` and `completion_sentinel_ref` on the matching flight only if the runner reports completion and the envelope and sentinel validate. Completion and verdict recognition stay governed by the `## Worker Completion Contract`.
 
 The caller must launch the runner through a host-provided background job mechanism that notifies the caller when the carrier process exits. It must not use shell `&` to background the runner, because that detaches the process from host tracking and can leave an init-adopted carrier running without ever notifying the caller of completion. It must not monitor files or logs to poll for completion; doing so conflicts with the no-polling rule above.
 
 `skills/sshx/scripts/run-codex-worker-batch.sh` is the permitted one-call fan-out alternative for the `codex-cli` subset of a multi-seat stage. It never covers a whole stage because the `nyxid-oracle` and `isolated-token-subagent` seats reserved by the dispatch-time composition above remain outside the batch. The dispatcher obtains every worker artifact path from the runner's pure path projection; worker artifact paths remain runner-derived and are never caller-supplied.
 
-Internal shell `&` followed by `wait` is permitted inside that one named batch script because it remains the foreground process of one host-tracked job, records every child, and joins every recorded child before publishing a report; its signal handling, interruption reporting, and inherited-disposition limits are owned by `CODEX_WORKER_SPEC.md` and the script's behavior tests, and whole-job-tree teardown remains the host's responsibility. Caller-authored `&`, `nohup`, `disown`, and `setsid` remain forbidden. Batching degrades host completion notification from per-carrier to per-batch. Launching one host job per seat remains permitted and is the form on which per-seat retry and fallback latency depends; batching is an alternative, not a mandate.
+Internal shell `&` followed by `wait` is permitted inside `skills/sshx/scripts/run-codex-worker.sh` for its own carrier and inside the named batch script for its runners; each script remains attached to one host-tracked job, and the batch script records every child, and joins every recorded child before publishing a report; its signal handling, interruption reporting, and inherited-disposition limits are owned by `CODEX_WORKER_SPEC.md` and the script's behavior tests, and signalling each runner for batch cancellation remains the host's responsibility. Caller-authored `&`, `nohup`, `disown`, and `setsid` remain forbidden. Batching degrades host completion notification from per-carrier to per-batch. Launching one host job per seat remains permitted and is the form on which per-seat retry and fallback latency depends; batching is an alternative, not a mandate.
 
 The caller may invoke `skills/sshx/scripts/read-codex-worker-status.sh` only after host completion notification. Status reading is a one-shot, after-terminal collection convenience and is not authorization to poll while any runner is active. The batch report is dispatcher-owned orchestration evidence, not a worker artifact, and neither it nor the status projection changes completion or verdict routing.
 

skills/sshx/formal/Sshx/Clauses/Delegation.lean

@@ -311,8 +311,9 @@ inductive TeardownOwner
   | runner
   deriving DecidableEq, Repr
 
--- SKILL[def]: "Time limits and final teardown of the whole job tree are the caller AI harness's responsibility."
-def teardownOwner : TeardownOwner := .callerHarness
+-- SKILL[def]: "Time limits, signalling the runner itself, and teardown after uncatchable termination are the caller AI harness's responsibility; the runner owns teardown of its own carrier tree on trappable `INT` and `TERM` as specified in `CODEX_WORKER_SPEC.md`."
+def teardownOwner (trappableCarrierCancellation : Bool) : TeardownOwner :=
+  if trappableCarrierCancellation then .runner else .callerHarness
 
 -- SKILL[ref]: "The caller records `result_envelope_ref` and `completion_sentinel_ref` on the matching flight only if the runner reports completion and the envelope and sentinel validate."
 abbrev refsOnlyOnCompletion := @Behavior.collectEffect
@@ -334,8 +335,8 @@ theorem batch_never_covers_whole_stage (seats : Nat) (h : 2 ≤ seats) :
 -- SKILL[ref]: "The dispatcher obtains every worker artifact path from the runner's pure path projection; worker artifact paths remain runner-derived and are never caller-supplied."
 abbrev batchPathsFromRunner := artifactPathOwner
 
--- SKILL[def]: "Internal shell `&` followed by `wait` is permitted inside that one named batch script because it remains the foreground process of one host-tracked job, records every child, and joins every recorded child before publishing a report; its signal handling, interruption reporting, and inherited-disposition limits are owned by `CODEX_WORKER_SPEC.md` and the script's behavior tests, and whole-job-tree teardown remains the host's responsibility."
-def batchInternalWaitPermitted : Bool := true
+-- SKILL[def]: "Internal shell `&` followed by `wait` is permitted inside `skills/sshx/scripts/run-codex-worker.sh` for its own carrier and inside the named batch script for its runners; each script remains attached to one host-tracked job, and the batch script records every child, and joins every recorded child before publishing a report; its signal handling, interruption reporting, and inherited-disposition limits are owned by `CODEX_WORKER_SPEC.md` and the script's behavior tests, and signalling each runner for batch cancellation remains the host's responsibility."
+def runnerAndBatchInternalWaitPermitted : Bool := true
 
 inductive NotificationGranularity
   | perCarrier