docs(framing): revision 13 round 2 --- the algorithm still implemented r12

Five blocking inconsistencies, all upheld. The first was the worst: the
document specified a validated pair and then printed an algorithm that
emits no tokens and a consumer flow that proceeds on exit 0 alone ---
accepting 0 with a missing token, the exact defect revision 13 forbids.

  1. The algorithm now emits exactly one token per arm on stdout with
     diagnostics on stderr; the consumer flow is pair-validation with
     explicit normalisation (strip one trailing newline, trim ASCII
     whitespace, require exactly one line); and the outcome table is
     keyed on pairs, with a fourth row for boundary error including
     macOS's status 1 with no token. `safe` is validated like the
     others --- a status arriving without its token did not come from
     this helper.

  2. A6a is SCOPED TO THE GATE. R-d never sees a shell status: the gate
     goes through /bin/sh, which turns an exec failure into an exit
     status, while Rust's Command returns a spawn error with no status
     at all --- conformance row 12, not row 5. And macOS CI does not
     compile R-d's test, which is crdt-gated while the macOS jobs build
     without crdt. R-d on macOS is unexercised, and the framing says so
     rather than implying coverage.

  3. A7 is restated against measurement. It cannot still say no
     non-Linux unix was tried when macOS ran and went red: five of six
     helper/gate rows pass there, one defect is named, R-d is recorded
     Linux-only, and the remaining portability claim is labelled a
     contract argument.

  4. "Both consumers use the same helper so they can never disagree" is
     withdrawn --- true when the status WAS the verdict, false once each
     consumer validates a pair independently in a different language.
     Replaced by a twelve-case conformance matrix both validators must
     agree on, including the macOS case and a normalisation case.

  5. The token-to-stderr mutation is remapped from A2 to A1/A3, with
     the reasoning recorded: with stdout empty every outcome becomes
     boundary error, which still satisfies A2 as written since A2 only
     requires "not the deadline message". A2 stays broad and A6 pins
     which diagnosis appears.

The ledger is aligned: the mechanism is established rather than
hypothesised, the "stderr prints the raw status" claim is corrected ---
the number appears only in the catch-all, and this failure took the
other branch --- and revision 12 is marked superseded.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
Levi Neuwirth 2026-08-19 20:27:43 +02:00
parent 343eabd897
commit 8b8a692528
No known key found for this signature in database
2 changed files with 165 additions and 51 deletions

View File

@ -288,18 +288,39 @@ from #171 and #215.
otherwise exercised there. otherwise exercised there.
- **The gate returned 1 = `ignored` for a helper it could not - **The gate returned 1 = `ignored` for a helper it could not
execute** — the exact conflation §7c forbids. execute** — the exact conflation §7c forbids.
- **Leading hypothesis, NOT yet established: the ABI's `1` is - **ESTABLISHED, not a hypothesis.** The macOS log shows the shell's
ambiguous by construction.** `1` means "ignored", and `1` is also a `Permission denied` followed by the gate's `1 | 2)` message — so
status shells return for assorted failures. On Linux an `sigint_status` was **1**: macOS `/bin/sh` returns **1** for an
unexecutable file yields 126, so the catch-all maps it to 2; if exec failure where Linux returns **126**. The status-only ABI
macOS's `/bin/sh` returns 1, the two cases are **the same number** cannot separate that from the helper's own `ignored`.
at the call boundary and no catch-all can separate them. If that - **The raw status was NOT printed.** An earlier entry here said the
holds, the fix is to move the verdicts out of the range shells stderr carries it; the gate interpolates the number only in its
produce, or to carry them by something other than exit status catch-all branch, and this failure took the `1 | 2)` branch. The
alone — a design change needing its own revision. path was identified by **which message text appeared**, not by a
- The assertion now carries the gate's stderr, which prints the raw number.
probe status, because the first failure could not say which status - **A proposed repair was REJECTED in review and is recorded so it is
produced it. not retried:** moving `ignored` from 1 to 3 relocates the collision
without closing it, because an exec failure can return **any**
nonzero status. The generalisation: **no exit status can prove the
helper ran.**
- **Framing revision 13 — AWAITING APPROVAL — replaces the ABI with a
validated `(status, token)` pair**: `0`/`1`/`2` with
`pmacs-sigint-v1:safe|ignored|error`, token alone on stdout,
diagnostics on stderr, and any other pair — including macOS's
status 1 with no token — a boundary error mapped to 2. Every
refusing branch must print the observed status and token state as
diagnostic context, never as the classifier. A shared **conformance
matrix** replaces revision 12's withdrawn "both consumers use the
same helper so they can never disagree", which stopped being true
once each consumer validates the pair independently.
- **A6a is scoped to the GATE.** R-d never sees a shell status: Rust's
`Command` returns a spawn error with no exit status, and R-d's test
is crdt-gated so macOS CI does not compile it. R-d on macOS is
**unexercised**, recorded as a gap.
- **A7 is no longer "satisfied by disclosure"** — macOS was reached
and measured: five of six helper/gate rows pass, one defect
(`gate_maps_an_unexecutable_helper_to_error_not_ignored`), R-d
Linux-only.
- **PR #241** (`https://github.com/levineuwirth/pmacs/pull/241`), opened - **PR #241** (`https://github.com/levineuwirth/pmacs/pull/241`), opened
2026-08-19 from `gpu-probe-sigint-teardown` into `main`. **Not merged; 2026-08-19 from `gpu-probe-sigint-teardown` into `main`. **Not merged;
awaiting review rounds.** awaiting review rounds.**
@ -340,7 +361,8 @@ from #171 and #215.
result line immediately below `gate_script_acceptance`'s in the sweep result line immediately below `gate_script_acceptance`'s in the sweep
log, misread as this suite's.) log, misread as this suite's.)
- **Framing revision 12 at `docs/gpu-probe-sigint-framing.md`, - **Framing revision 12 at `docs/gpu-probe-sigint-framing.md`,
APPROVED 2026-08-19 at `1fc0df6`** — revision 10 was approved at approved 2026-08-19 at `1fc0df6` and IMPLEMENTED; **superseded by
revision 13, awaiting approval** — revision 10 was approved at
`4fba9f6` and revision 9 at `15c25ec`; neither approval covered the `4fba9f6` and revision 9 at `15c25ec`; neither approval covered the
later mechanism finding and remedy selection. **D1/D2 HAVE RUN and later mechanism finding and remedy selection. **D1/D2 HAVE RUN and
found the mechanism: `SIGINT` was ignored group-wide found the mechanism: `SIGINT` was ignored group-wide

View File

@ -744,41 +744,71 @@ Consumers therefore validate the exact pair and treat every mismatch as
decides, and the pair is what makes the helper's decision decides, and the pair is what makes the helper's decision
distinguishable from a shell's. distinguishable from a shell's.
Its complete POSIX-shell classification shape preserves failure rather Its complete POSIX-shell shape. Each arm emits **exactly one token on
than overwriting it: stdout** and its diagnostic on stderr, so a status is never the only
thing a consumer sees:
```sh ```sh
probe_status=0 probe_status=0
sh -c 'trap "exit 23" 2 || exit 24; kill -INT "$$" || exit 24; exit 0' \ sh -c 'trap "exit 23" 2 || exit 24; kill -INT "$$" || exit 24; exit 0' \
|| probe_status=$? || probe_status=$?
case "$probe_status" in case "$probe_status" in
23) exit 0 ;; 23)
echo 'pmacs-sigint-v1:safe'
exit 0
;;
0) 0)
echo 'pmacs-sigint-v1:ignored'
echo 'pmacs: SIGINT is ignored; run this command with SIGINT deliverable' >&2 echo 'pmacs: SIGINT is ignored; run this command with SIGINT deliverable' >&2
exit 1 exit 1
;; ;;
*) *)
echo 'pmacs-sigint-v1:error'
echo "pmacs: could not determine whether SIGINT is deliverable (probe status $probe_status)" >&2 echo "pmacs: could not determine whether SIGINT is deliverable (probe status $probe_status)" >&2
exit 2 exit 2
;; ;;
esac esac
``` ```
The helper maps inner 23 → helper 0, inner 0 → helper 1, and every The helper maps inner 23 → `(0, safe)`, inner 0 → `(1, ignored)`, and
other status → helper 2. Consumers **do not parse the raw 23/0/24 every other status → `(2, error)`. Consumers do not parse the inner
statuses and do not supply their own signal diagnosis**: they continue 23/0/24 statuses and do not supply their own signal diagnosis.
only on helper exit 0 and otherwise stop while surfacing the helper's
stderr unchanged. Failure to execute the helper at all is mechanically **The consumer flow is pair-validation, not status inspection:**
an `error` at the call boundary, never evidence that `SIGINT` is
ignored. 1. Run the helper, capturing **status**, **stdout** and **stderr**
separately. A spawn failure — the helper missing, not executable, or
unrunnable for any reason — is `error` immediately, with **no
status to inspect at all**.
2. **Normalise stdout**: strip a single trailing newline, then trim
ASCII whitespace at both ends. The result must be **exactly one
line**. Anything else — empty, multi-line, or with interior
content — is `error`.
3. Accept **only** these three pairs; every other combination is
`error`:
| status | normalised stdout | outcome |
|---|---|---|
| 0 | `pmacs-sigint-v1:safe` | `safe` |
| 1 | `pmacs-sigint-v1:ignored` | `ignored` |
| 2 | `pmacs-sigint-v1:error` | `error` |
4. Proceed only on `safe`. Otherwise stop, surfacing the helper's
stderr unchanged plus the diagnostic context below.
**`safe` is validated like the others.** Revision 12 let a consumer
proceed on exit 0 alone; under revision 13, `0` with a missing or wrong
token is `error` and the consumer stops. That is deliberate — a status
that arrives without the token did not come from this helper.
That produces one of three total outcomes: That produces one of three total outcomes:
| outcome | meaning | how it is reached | | outcome | pair required | reached when |
|---|---|---| |---|---|---|
| `safe` | `SIGINT` is deliverable | inner probe exits 23; helper exits 0 | | `safe` | `(0, pmacs-sigint-v1:safe)` | inner probe exits 23 |
| `ignored` | `SIGINT` is inherited as `SIG_IGN` | inner probe exits 0 after a successful `kill`; helper exits 1 | | `ignored` | `(1, pmacs-sigint-v1:ignored)` | inner probe exits 0 after a successful `kill` |
| `error` | the probe could not decide | `kill` failed, `sh` unavailable, unexpected exit, another signal, or helper execution failed; helper exits 2 or could not be executed | | `error` | `(2, pmacs-sigint-v1:error)` | `kill` failed, `sh` unavailable, unexpected exit, another signal |
| `error` (boundary) | **anything else**, including *no* pair | helper missing or unexecutable; a status with a missing, mismatched, unknown or malformed token; **macOS's status 1 with no token** |
`error` is **not** treated as `ignored`. It fails the gate too, but with `error` is **not** treated as `ignored`. It fails the gate too, but with
a different diagnosis, because "your environment ignores SIGINT" and a different diagnosis, because "your environment ignores SIGINT" and
@ -792,8 +822,37 @@ that every supported Unix has already exercised it; A7 keeps the
implementation record explicit about which platforms were actually implementation record explicit about which platforms were actually
tried. tried.
**Both consumers use the same helper**, so the guard and the test can **Both consumers use the same helper — but that alone no longer makes
never disagree about what "ignored" means: them agree.** Under revision 12 the helper's exit status *was* the
verdict, so a shared helper guaranteed a shared answer. Under
revision 13 each consumer **independently validates the pair**, in a
different language, so they can now disagree by validating differently.
Revision 12's claim that they "can never disagree" is withdrawn.
What replaces it is a **shared conformance matrix**: both validators
are exercised against the same twelve cases, and must agree on every
one.
| # | status | stdout | expected |
|---|---|---|---|
| 1 | 0 | `pmacs-sigint-v1:safe` | `safe` |
| 2 | 1 | `pmacs-sigint-v1:ignored` | `ignored` |
| 3 | 2 | `pmacs-sigint-v1:error` | `error` |
| 4 | 0 | *(empty)* | error |
| 5 | 1 | *(empty)* | error — **the macOS case** |
| 6 | 0 | `pmacs-sigint-v1:ignored` | error (mismatched) |
| 7 | 1 | `pmacs-sigint-v1:safe` | error (mismatched) |
| 8 | 0 | `pmacs-sigint-v2:safe` | error (unknown version) |
| 9 | 0 | `pmacs-sigint-v1:safe\npmacs-sigint-v1:safe` | error (multi-line) |
| 10 | 0 | ` pmacs-sigint-v1:safe ` | `safe` (normalisation: trim) |
| 11 | 126 | `pmacs-sigint-v1:safe` | error (status outside 0–2) |
| 12 | — (spawn failure) | — | error, with no status inspected |
Row 10 fixes normalisation: **strip one trailing newline, then trim
ASCII whitespace, then require exactly one line.** Rows 4–9 and 11 are
the ways a status can arrive without a trustworthy verdict.
The two consumers:
- **`scripts/gate` fails immediately**, before any stage, with an - **`scripts/gate` fails immediately**, before any stage, with an
explicit ignored-`SIGINT` diagnosis. explicit ignored-`SIGINT` diagnosis.
@ -866,7 +925,19 @@ show:
| consumers accept a **missing** token (status only) | A6 and the macOS row — this is exactly the shipped defect | | consumers accept a **missing** token (status only) | A6 and the macOS row — this is exactly the shipped defect |
| consumers accept a **wrong** token for the status (e.g. `…:safe` with exit 1) | A6 | | consumers accept a **wrong** token for the status (e.g. `…:safe` with exit 1) | A6 |
| consumers accept an **unknown** token (`pmacs-sigint-v2:safe`) | A6 | | consumers accept an **unknown** token (`pmacs-sigint-v2:safe`) | A6 |
| helper prints the token to **stderr** instead of stdout | A1–A3 — the pair no longer validates | | helper prints the token to **stderr** instead of stdout | **A1 and A3** — see below |
**Why that last one maps to A1/A3 and not A2.** With the token on
stderr, stdout is empty, so *every* outcome becomes boundary `error`.
A1 (gate refuses under ignored `SIGINT`) still refuses but with the
wrong diagnosis, and A3 (foreground success unaffected) breaks
outright because `safe` no longer validates — both bite. **A2 does
not**, because A2 only requires the direct test to report *a*
precondition failure rather than the 5 s deadline, and a boundary
`error` satisfies that as written. Revision 13 listed A2 here
incorrectly. Either mapping is defensible; this framing keeps A2
broad — the property it protects is "never the misleading deadline
message" — and relies on A6 to pin *which* diagnosis appears.
- **A5 — the gate is otherwise unchanged**: a normal foreground run - **A5 — the gate is otherwise unchanged**: a normal foreground run
reaches and passes every stage it did before, with no stage added, reaches and passes every stage it did before, with no stage added,
skipped, reordered, or made conditional. skipped, reordered, or made conditional.
@ -877,27 +948,48 @@ show:
revision 13 to cover the pair: a **missing**, **mismatched** or revision 13 to cover the pair: a **missing**, **mismatched** or
**unknown** token is `error` in both consumers, whatever the status **unknown** token is `error` in both consumers, whatever the status
accompanying it. accompanying it.
- **A6a — the macOS row, stated as the concrete obligation it now is.** - **A6a — the macOS row, SCOPED TO THE GATE.** An unexecutable helper
An unexecutable helper on macOS yields **status 1 with no token**. on macOS makes `/bin/sh` exit **1 with no token**; the gate must
Both consumers must classify that as **boundary error → 2**, never classify that as **boundary error → 2**, never `ignored`. Not
`ignored`. This is not a hypothetical: it is the observed CI failure hypothetical: it is the observed CI failure on `70f0bc9`
on `70f0bc9` (`Test (macos-latest / lua54)` and `… / luajit`), and (`Test (macos-latest / lua54)` and `… / luajit`), and the row is
the row is only satisfied when that platform is green. satisfied only when that platform is green.
- **A7 — SATISFIED BY DISCLOSURE**, which is the fallback this
criterion allows when no non-Linux unix is reachable. Revision 12 **It does not apply to R-d, for two independent reasons**, and
wrote A7 as "exercised there, **or** state what is claimed versus revision 13 was wrong to state it for "both consumers":
what was tried"; an earlier draft of this line said A7 "stays open", - **R-d never sees that status.** The gate invokes the helper through
which **contradicted the approved contract** and is withdrawn. `/bin/sh`, which converts an exec failure into a shell exit status.
- **Tried:** Linux `x86_64`, this machine, all three outcomes R-d uses Rust's `Command`, which returns a **spawn error with no
(`safe` 0, `ignored` 1, `error` 2), for the helper, the gate and exit status at all** — a different code path reaching `error` by a
the direct test. different route (conformance row 12, not row 5).
- **Not tried:** every non-Linux unix. None was reachable. - **macOS CI does not compile R-d's test.** It lives inside
- **Claimed:** the mechanism is POSIX, not Linux-specific — the `#[cfg(feature = "crdt")] mod crdt`, and the macOS jobs run
helper uses only `trap`, `kill -INT`, `$$`, `case` and `echo`, and `--no-default-features --features <lua>` with no `crdt`;
reads no `/proc` and calls no `sigaction`; the disposition `Test (crdt)` is `runs-on: ubuntu-latest`.
behaviour it detects is POSIX inheritance across `fork` and `exec`.
That is a contract argument, disclosed as such. Anyone porting to So R-d's macOS behaviour is **unexercised**, and this framing does not
BSD or macOS should re-run the three outcomes rather than trust it. pretend otherwise. Closing that would need either a non-crdt-gated
R-d row or a macOS crdt job — **neither is proposed here**, and A7
records the gap instead of hiding it.
- **A7 — PARTIALLY EXERCISED ON macOS, one defect found, R-d still
Linux-only.** Revision 12 closed this by disclosure because no
non-Linux unix was reachable. **That is now stale: macOS CI reached
it and measured it red**, so the disclosure fallback no longer
applies and the criterion is restated against evidence.
- **Exercised on macOS (`Test (macos-latest / lua54)` and
`… / luajit`, head `70f0bc9`):** five of the six helper/gate rows
pass — all three helper outcomes, gate refusal on `ignored`, and
gate refusal on a helper-reported `error`.
- **One known defect on macOS:**
`gate_maps_an_unexecutable_helper_to_error_not_ignored` fails,
status 1 with no token classified as `ignored`. This is the whole
reason for revision 13 (§4d), and A6a is the row that closes it.
- **R-d: Linux-only, unexercised on macOS**, because its test is
crdt-gated and the macOS jobs build without `crdt`. Stated as a
gap, not argued away.
- **Everything else remains a contract argument**: the helper is
POSIX shell only, reads no `/proc` and calls no `sigaction`. BSD
and other unixes are still untried.
## 8b. Superseded criteria, kept for the record ## 8b. Superseded criteria, kept for the record