feat(spec): check (c) proves a guidance-route retirement on a reachable def (#18301) (#18529)

Fixes #18301
Clause-②: no

Executes the **C** half of the #17356 ruling (batch #135 item 3,
maintainer 「135 同意」). A is already landed (PR #18485 advanced the
deletion-gate anchor); B and D were refused. This card adds a proof — it
retires nothing, and it reverses nothing.

> **Patch round.** The contract review of record (comment `5706880661`,
served `CONTRACT_REVIEW_TIER`) returned **FAIL** on ① item 3: the
proof's stated "the door is closed" condition described something the
gate did not compute. This round replaces that condition, corrects every
place the claim was made, and pins the case that was unpinned.
Re-measuring the review's own sweep **falsified its latency finding** —
see "The assumption that did not hold" below.

## What was wrong

Check (c) of the `authorable-surface/` deletion gate
(`packages/spec/scripts/build-schemas.ts`) admitted a deleted baseline
line on three proofs: an aged-out `[RETIRED]` tombstone, an unreachable
def, or a def the build no longer emits.

A key retired the **strict-schema / guidance way** — deleted from the
shape outright, its prescription moved into the closed shape's
`guidance` table — never carries the `[RETIRED]` mark, because there is
nothing left in the shape to mark. Proof 1 therefore could not apply to
it **at any major**: not "has not aged yet" but "has no clock". On a
reachable def that left the whole class with no proof shape at all.

The class was invisible until now because proof 2 was answering for
these defs — the BFS root set omitted the four unregistered kinds, so
whole families read as unreachable and every deletion under them was
waived as over-collection. #18131 repaired the root set, and the repair
is what exposes the gap.

## The assumption that did not hold

The review swept for a def that could satisfy proof 4's conditions while
silently STRIPPING the author's write, found none, and recorded the hole
as latent. The dispatch asked for that to be re-measured. It was, **with
the gate's own instrument** rather than by grep — a census pass over all
1525 emitted defs, running proof 4's declaration match and then asking
each def what it does with the key. It is not latent:

| def | artifact `additionalProperties` | matches one declaration by
shape identity | reachable | writing `keyBy` |
|---|---|---|---|---|
| `shared/RateLimitConfig` | `false` | yes | `root-graph` | **parse
SUCCEEDS, key dropped** |
| `system/ServerRateLimitConfig` | `false` | yes (the SAME declaration)
| `derived-clone` | refused, with the prescription |

`ServerRateLimitConfigSchema` is declared `strictObject({… guidance: {
keyBy, store } }, RateLimitConfigSchema.shape)` — built FROM the open
schema's own shape object
(`packages/spec/src/system/stack-server.zod.ts`,
`packages/spec/src/shared/http.zod.ts`). So one declaration answers for
two emitted defs, and **every fact the first cut of proof 4 read says
they are the same def**. Two keys (`keyBy`, `store`) on a root-reachable
def: had either baseline line been deleted, the shipped implementation
would have waived it while an author who keeps writing the key has it
silently dropped.

That is the review's "strip-mode clone shares a strict shape" case in
the spelling the tree actually holds — shape sharing in the other
direction, which is why a sweep for `.strip()`, `z.object(X.shape)` and
`strictObjectError()` found nothing. **No wrong verdict has shipped**:
proof 4 is not on `main`, and neither key is a pending deletion. What
changes is that the fix is now mandatory rather than prophylactic, and
the fixture below is a real specimen rather than a synthetic one.

## What this adds

**Proof 4.** A deleted baseline line is legitimate when, on a def that
is emitted and reachable, **all three** of these hold in this build's
own tree:

1. **the baseline entry was not `[RETIRED]`** — a guidance-route
retirement deletes the key from the shape instead of leaving a
`retiredKey()` in it, so it never earned the mark. This is a property of
the class, not a guard bolted on, and it is what keeps proofs 1 and 4
disjoint.
2. **a `strictObject` declaration promises a prescription for the key**
— the def resolves to exactly one `StrictObjectDeclaration` by shape
identity, and that declaration's `guidance` names the exact key, or one
of its `guidanceSets` **enumerates** it. This half says which text is
owed.
3. **the def keeps that promise** — `safeParse` of that key against the
schema `zodByDefKey` holds raises an `unrecognized_keys` issue naming
it, and that issue's message carries the declared text **verbatim**.
This half is the door.

Condition 3 replaces the condition the review failed. Nothing else in
the gate moves.

### Why the artifact read is gone rather than restated

The failed version proved "the door is closed" by reading
`additionalProperties === false` off the emitted JSON Schema. **This
repo had already measured that this does not distinguish a closed door
from a silent strip** and written it down: `build-schemas.ts` converts
with the default `io: 'output'`, and in output mode zod emits
`additionalProperties: false` for a `.strip()` object too — verified in
`docs/audits/2026-07-unknown-key-strictness-ledger.md` by regenerating
both ways to a byte-identical artifact. A condition that answers the
same for both cases cannot be the one that excludes one of them, so it
is removed, and the docblock and the author-facing remedy now say so in
the gate's own words.

The subtler half, which the review named and which the census above
confirms: **shape identity is not a door test either.**
`strictObjectError()` registers a declaration without closing the shape,
`.strip()` and `z.object(Strict.shape)` clone a shape without its door,
and `strictObject(opts, Open.shape)` — the live case — puts a closed
declaration and an open def on the same shape entries. The identity
match stays, because it is how the owed text is found; it is no longer
asked to prove closure.

### Why the probe reads `unrecognized_keys`, and why it reads the
message

`unrecognized_keys` is the **only** issue code a `guidance` table is
ever consulted from (`strictUnknownKeyError` returns undefined for every
other code), and the prescription is appended to that message verbatim,
one bullet per key. So the issue's presence is exactly "this def refused
the write", and the declared text appearing in its message is exactly
"the error map this def parses through is the one holding that table" —
which shape identity alone cannot tell, since a clone can share a shape
without sharing a map. No message WORDING is pinned by this: the needle
is read out of the tree, from the very declaration the structural half
matched, so a rewritten prescription moves both sides together.

The alternative the review offered — reading `catchall` of type `never`
off the instance — was measured to give identical verdicts on all four
shapes tried (`strict`, `.strip()` clone, plain `z.object`,
`catchall(z.string())`). It was not chosen because it proves a spelling
of the door rather than the delivery of the prescription, and it would
still have admitted a strict clone built without the declaration's error
map. The other alternative — recording `strictObject()` and
`strictObjectError()` distinctly in the registry — is a
`packages/spec/src/shared/strict-object.ts` edit, outside this card's
two files and across the clause-② path limb, and it would not have
caught the live case above at all (both twins' declaration comes from
the same `strictObject` call).

### A third verdict, and what it deliberately does not say

A key a declaration names but the def does not answer for now gets its
own violation line instead of the generic "was LIVE (never tombstoned)"
— its `guidance` entry already exists, and what is missing is a door to
deliver it through, so the generic verdict would send its reader to
write something already written. That line states only **that** the
prescription did not arrive, never **why**: on the shipped graph 7 of
the 8 defs in that state are unions, where "the door is open" would be a
guess this gate has not measured — the mistake the first cut made about
`additionalProperties`, one layer down.

### Two narrowings, both deliberate, both fail-closed

- **Exactly one matching declaration.** An empty shape is excluded
outright — it matches every other empty shape. Where two declarations
still answer, the lookup returns "no evidence" rather than unioning
them.
- **A `guidanceSets` RegExp does not count.** Only an enumerated `keys`
list NAMES the key; a pattern claims a family whose members were never
written down.

### Measured population — why this is a proof and not a blanket waiver

Census over the shipped graph, run with the gate's own code (tree
`944d773b8`; `packages/spec/src` is byte-identical at the head this PR
now carries, `git diff --name-only` over that path returns 0 lines):

| reading | value |
|---|---|
| emitted defs | 1525 |
| defs whose emitted artifact carries `additionalProperties: false` |
1117 |
| defs resolving to exactly one declaration that names an undeclared key
| 258 |
| keys those declarations promise | 779 |
| keys the def actually delivers — what proof 4 admits | **770** |
| keys promised and NOT delivered — what proof 4 refuses | **9** |

Of the 9: 2 are the live case above; 7 are union defs the probe cannot
drive to a single door, all of which the superseded artifact condition
also excluded, so no verdict moves for them.
`integration/DataSyncConfig` has no route at all (its shape is a plain
`z.object` and nothing prescribes for `schedule`), so this proof cannot
reach the 2026-09-10 ruling that withheld that tombstone.

## Evidence

### The pins (`build-schemas-check-mode.test.ts`)

| fixture | expected | what it would catch |
|---|---|---|
| `data/Metric:filters` | admitted by **proof 4**, explicitly **not**
proof 2 | a proof that never fires |
| `data/Metric:zzNotPrescribed18301` | still refused, and NOT with the
third verdict | a waiver keyed off the DEF instead of the KEY |
| `integration/DataSyncConfig:schedule` | still refused | a silent
reversal of the 2026-09-10 ruling |
| `api/SessionResponse:zzOverCollected4650` | still waived by **proof
2**, in proof 2's words | proof 4 written as a widening of proof 2 |
| `data/Object:compactLayout [RETIRED]` | falls to the tombstone chain,
**not** proof 4 | the disjointness — it satisfies every other condition
proof 4 tests |
| `system/ServerRateLimitConfig:keyBy` | admitted by **proof 4** | — the
lit half of the new pair |
| `shared/RateLimitConfig:keyBy` | **REFUSED**, with the third verdict,
and not waived by proof 2 either | **the review's finding**: one
declaration, two defs, and a gate that reads the registry instead of the
door admits the open one |

The last two are ONE run and ONE declaration, which is what makes them a
discriminator rather than two assertions. The `beforeAll` guard holds
the tree fact they model in four loud halves: the two twins declare the
same key SET, share every shape ENTRY by instance identity, the open
twin ACCEPTS `keyBy` and the parsed output does not contain it, and the
closed twin rejects it with a prescription bullet. If any half rots, the
pin says so instead of going quietly green.

Every negative assertion in the proof-4 cases was also corrected: they
were written as `KEY — TOKEN` where the gate emits `KEY — def REACH;
TOKEN`, so they could not have matched even on an admitted key. They now
carry the `def .*` span and fail when they should.

### Ablations — both directions, on-disk proof, restored

Both legs prove the mutation reached disk before any colour is read, and
both restores are proved by `git hash-object` against the HEAD blob plus
a whole-tree `git status --porcelain`. Each script arms a `trap` on
EXIT, INT and TERM that restores the file from HEAD, against an absolute
path resolved from `git rev-parse --show-toplevel`.

**Ablation C — blind the door probe** (`delivers()` returns `true`
unconditionally, which is the superseded implementation's behaviour for
this def):

- marker occurrences 0 to 1, blob `322938f2` to `682ce658` — the
mutation is on disk.
- run **RED**, and in the sharpest possible direction: `eager.status`
came back **0**. With the door blinded the gate WAIVES
`shared/RateLimitConfig:keyBy` and the whole run exits green — the hole,
executed, not argued. The other two #18301 cases stayed green,
correctly: neither tests the door.
- restored: blob back to `322938f2`, marker back to 0, `git diff HEAD` 0
bytes, `git status --porcelain` 0 lines.

**Ablation D — deafen the door probe** (`delivers()` returns `false`
unconditionally):

- marker occurrences 0 to 1, blob `322938f2` to `3096b1af`.
- run **RED**, 2 cases: both positive legs fall to the third verdict —
`data/Metric:filters` and `system/ServerRateLimitConfig:keyBy` both
printed `a \`strictObject\` declaration NAMES …, but writing it`. So the
probe is load-bearing for the admissions too; proof 4 is not the
declaration match wearing a new name.
- restored: blob back to `322938f2`, marker back to 0, `git diff HEAD` 0
bytes, `git status --porcelain` 0 lines.

The previous round's ablations A and B were run against the superseded
implementation (their anchor, `prescribed?.has(leaf)`, no longer exists)
and are **not** carried forward as evidence for this head.

`scripts/ablation-dist-preflight.mjs` still reports `no dist/` for this
package and is **NOT MEASURED**, not red, for the same reason as the
previous round: the test spawns `tsx` over `scripts/build-schemas.ts` in
a sandbox that SYMLINKS the real `packages/spec/src`, so nothing here
resolves through `dist/`. The instrument that applies is the on-disk
marker count plus the run's own colour, both recorded above.

## Runs

Long runs went through `scripts/pm/os-verify-lock.sh`; exit codes were
captured by redirect-then-`$?`, never through a pipe.

`origin/main` was merged into this branch (`79a046f8c`) before this body
was written, and every reading below is on the merged head.

| command | verdict |
|---|---|
| `pnpm --filter @objectstack/spec run test:repo` | `VERDICT
command-exit 0` — 31 files, 529 passed |
| `pnpm --filter @objectstack/spec typecheck` | `VERDICT command-exit 0`
(`tsc --noEmit` + `check:scripts-typecheck` + `check:test-typecheck`) |
| `pnpm --filter @objectstack/spec run check:authorable-surface` | exit
0 |
| `pnpm lint` (the repo-wide `eslint . --no-inline-config`) | exit 0 —
the FULL run, not a narrowing, at `9e0324f80` |
| `node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack
--commands` | 61 families derived ON THIS HEAD, not inherited |

`pnpm lint` is normally CI's to run; it completed here, so the reading
is the whole population eslint's own config selects rather than a subset
— no narrowing claim is being made and none needs checking.

All 61 derived gates were run and reconciled with `--ran`, each line
carrying its exit code. 55 exit 0. Five exit **3 (PREREQUISITE NOT
MET)** and are **NOT MEASURED** — each needs a built `dist/`, which this
worktree has never had, and none can be moved by a diff confined to
`packages/spec/scripts/**`: `check:dts-closure`,
`check:dual-build-cjs-loads`, `check:lean-entry-closure`,
`check:sourcemap-no-sources-content`, `check:type-check-debt`.

`pnpm check:pm-dispatch-gates` needed 807s and was recorded as `exit
124` on a first pass whose 600s wrapper fired; it was re-run without the
cap and exits **0**. The record carries the real code, not the timeout.

`packages/lint/scripts/check-reference-carrier-shape.mjs` is still
present on this head and exits 0 — PR #18503, which retires it, had not
landed when this list was derived. The list was re-derived here rather
than inherited from the dispatch, exactly because of that.

## Scope and publishing

`packages/spec/scripts/**` matches none of the package's `files[]`
entries (`dist`, `json-schema`, `liveness`, `prompts`, `llms.txt`,
`README.md`, `src/**/*.zod.ts`, `CHANGELOG.md`, `api-surface`,
`spec-changes.json`), and it is not a `tsup` entry — the only `scripts/`
string in `packages/spec/tsup.config.ts` is a repo-root import, against
a lit control of 22 `src/` occurrences. Nothing publishes, so `Clause-②:
no` and `skip-changeset`.

The diff is the two files the card fenced and no others: `git diff
--name-only` against the merge base returns exactly those two. In
particular the fix did **not** need `packages/spec/src/**` — the
dispatch's stop condition on that point does not fire.

## Acceptance notes

Out-of-scope observations, noted and deliberately **not** filed — none
is a reproducible defect, a declared-contract breach, or a trap that
makes an author write metadata the runtime rejects or silently drops:

- **Superseded.** The previous round's note here claimed proof 4 "works
around" the registry's door-blindness by reading `additionalProperties:
false` off the emitted artifact. That was wrong, per the review and per
this repo's own ledger, and the section above is what replaces it.
Nothing about the registry is "worked around" now: closure is decided at
the def, and the registry is asked only for the owed text.
- `strictObject()` and `strictObjectError()` are indistinguishable in
`strictObjectDeclarations()`, so the registry alone still cannot answer
a door question. This proof no longer asks it one. Recording the two
call shapes distinctly would let a future reader ask directly. Carrier:
whoever next reads `strictObjectDeclarations()` for a door question.
(`packages/spec/src/shared/strict-object.ts`)
- 408 of the 1525 emitted defs do not carry `additionalProperties:
false` on the emitted artifact. Per the review, that counts artifacts
whose TOP-LEVEL field is not `false` — unions, loose objects, pipes —
and is **not** the #4001 ledger's strip-site population, which
`check-strictness-ledger.mts` counts by AST. Carrier: the
strictness-ledger worklist, which already owns that surface.
- `scripts/ablation-dist-preflight.mjs` reports `no dist/` as a refusal,
which is correct for a dist-mediated ablation and reads as an accusation
for one that resolves through source. Carrier: none today — the script's
header already prescribes the property-read alternative by hand.

There is one observation this round declined to file and flags for the
reviewing seat rather than burying: `shared/RateLimitConfig` is an
**open** `z.object` whose shape is reused, closed, by
`ServerRateLimitConfigSchema`, and the `guidance` entries for `keyBy` /
`store` therefore prescribe to nobody on the open twin — an author
writing `keyBy` on an API endpoint's `rateLimit` has it dropped in
silence. That is #4001's own failure mode on a live authorable surface,
and it sits in `packages/spec/src/**`, outside this card's fence. It is
a candidate class-(c) card for the triage seat, not a finding this PR
may act on.


---
_Generated by [Claude
Code](https://claude.ai/code/session_01LvwGppdonww4zGLWZo5rho)_

---

## Landing note (seat, 2026-09-17)

Contract review at `CONTRACT_REVIEW_TIER` on head `9e0324f807`: **PASS**
— record is comment `5707796462`. It supersedes the earlier **FAIL**
(`5706880661`), which bound head `121465ba16` and does not bind this
one.

⭐ **The re-review did not read this code, it ran it.** With no
`node_modules` on the box it materialised `zod@4.4.3` and `esbuild` out
of pnpm's content-addressed store, `git archive`d this head's
`packages/spec/src` (archived tree hash verified equal to `git rev-parse
9e0324f:packages/spec/src`), bundled, and executed this head's own
`computeGuidanceRoutes` — verbatim, `diff`-checked — against 11
synthetic door shapes and a full 1525-def census, with the OLD head's
function alongside as the control.

**The FAIL's one verdict-bearing item is closed, measured rather than
argued:** `Strict` → prescribed, but `Strict.strip()`,
`z.object(Strict.shape)`, `Strict.loose()`, an error-map object without
`.strict()`, and `z.object(Strict.shape).strict()` without the map are
**all refused**. Every one of those stripping forms also emits
`additionalProperties: false` — which is the superseded condition's
blindness demonstrated on the instance instead of quoted from the
ledger. And the live twin executed both ways:
`shared/RateLimitConfig:keyBy` reads `prescribed` through the OLD
function (the hole, run) and `declared-but-silent` through this one.

### ⚠️ Correction to this body

The row 「defs resolving to exactly one declaration that names an
undeclared key: **258**」 is **mislabelled**. That population measures
**147**; 258 counts defs resolving to exactly one declaration *whether
or not it names anything*. Corrected here because this repo squashes and
the body becomes the permanent commit message. A second figure, the
docblock's 「7 of the 8 defs in that state are unions」, is also wrong (9
keys on 4 defs, 3 unions) but lives **in code** — both are carried by
**#18579** rather than fixed in-branch, because a third push would move
the head and void the review described above. ⚠️ Neither figure moves a
verdict or describes a safeguard, and the rationale they support (unions
dominate the not-delivered set) survives the corrected arithmetic.

### Seat ruling on the process question the review referred here

The review declined to rule on whether a dev may read a stop instruction
by its stated rationale, and named it the seat's. **Ruling: the dev was
right, and the dispatch order was at fault.**

That order said 「if a live member exists, STOP AND REPORT — on the
reading that it would mean a wrong verdict is shipping」. That bundles a
**trigger** with a **rationale**. The dev measured the trigger TRUE,
then measured the rationale FALSE (proof 4 is not on `main`; a
`guidance`-only key is never in the shape, so it was never a baseline
line and no deletion could ever put it to proof 4 — `keyBy`/`store` 0 in
the baseline against a lit control of 1 for `enabled`), and disclosed
both rather than quietly proceeding. Stopping there would have parked a
proven-wrong proof in a draft and delayed a fix that had to land before
this PR anyway.

⛔ This is **not** a general licence to reason past a fence. The
correction belongs on the seat's side: a stop condition must be written
as a **condition**, with its rationale separate and non-operative. The
general rule stands — where a dev cannot measure the rationale false,
the trigger governs and it stops.

**Out of scope, correctly handed over rather than acted on:** the live
trap the round found — `shared/RateLimitConfig` is an open `z.object`
whose shape is reused *closed* by `ServerRateLimitConfig`, so an
authored `keyBy` is dropped in silence — is filed as **#18578**. It
lives in `packages/spec/src/**`, outside this card's fence, and ⛔ was
not folded in.

**Pre-landing checks:** ① review PASS on record ✅ · ② `--pair 18529`
exit 0; ⛔ no carriers hung (`Clause-②: no`, verified a true declaration
against both limbs) ✅ · ③ re-taken at landing time ✅. Governed-surface
predicate: **0 of 2 paths hit the register** ⇒ ordinary queue landing.


---
_Generated by [Claude Code](https://claude.ai/code)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: os-warren