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

[os-warren]

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 check (c) has no proof shape for a guidance-route retirement on a reachable def — add a fourth proof so UNKNOWN_KEY_GUIDANCE retirements prove themselves (batch #135 item 3, C) #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 未知键静默剥离仍是全仓默认:把 #3405 的 strict 收紧从一个 schema 推广到整个可授权面(ADR-0078 完整性闸门) #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

---

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 archived this head's packages/spec/src (archived tree hash verified equal to git rev-parse 9e0324f8: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

[github-actions]

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see

• a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 298e9dde15e4e7c3b340323215e084fd60107cc3 → packageMentionDocs.

[os-litant]

Contract review

Served-tier: CONTRACT_REVIEW_TIER
Head-sha: 121465ba1681b5369725d56b172406d9629594b1

① Derived judgments

1. Gate accept set — NEW ADMISSION (proof 4). A deleted authorable-surface/ baseline line D:k is now admitted when, at head: D is emitted; D is reachable (proof 2 did not fire); the base entry was NOT [RETIRED]; the emitted JSON Schema for D has additionalProperties === false; zodShapeOf(D) is non-empty and matches exactly one strictObjectDeclarations() entry by sorted key set plus per-entry instance identity; and k is in that declaration's guidance map, or in an enumerated (non-RegExp) guidanceSets.keys, and k is not in the shape. Before this PR every such line was the violation "the entry at baseRev was LIVE (never tombstoned)". Verified at head l.1390-1440 and l.2438-2461. Characterisation: correct as to the enumerated conditions, with one exception in item 3.

2. Gate accept set — UNCHANGED. Proof 1 (the wasRetired branch, RETIRED_KEYS_BY_MAJOR dating, aging), proof 2 (unreachable), proof 3 (vanished def via the manifest gate), checks (a)/(b), the defaults ratchet and the anchor writer are byte-untouched outside the hunks listed above. Proof 4 lives only under !wasRetired, so a marked tombstone cannot be shortened by a guidance line — pinned by the data/Object:compactLayout [RETIRED] fixture. Refusals pinned in one spawned run: same-def unnamed key, integration/DataSyncConfig:schedule (letter B), unreachable key still waived in proof 2's words. Characterisation: correct.

3. Mis-declared: the "door is closed" condition. The PR (docblock l.1345-1352, body, and out-of-scope note 1) states that additionalProperties: false on the emitted artifact proves the runtime door is closed and that "on an OPEN shape the author's write is stripped in silence" is thereby excluded. The repo's own ledger (docs/audits/2026-07-unknown-key-strictness-ledger.md:1535-1541) records, measured, that under the generator's io: 'output' projection a strip-mode z.object() ALSO emits additionalProperties: false. So condition (b) does not distinguish a closed door from a silent strip; what actually excludes open shapes today is condition (c)'s identity match against a declaration that strictObject() built (which always .strict()s). That mechanism is unstated, and it has a hole the docblock promises is closed: a strip-mode clone sharing the exact shape object (Strict.strip(), z.object(Strict.shape)), or an exported open shape registered through strictObjectError(), would pass both (b) and (c) and be admitted while the author's write is dropped — the one direction the docblock says "this gate must not err in". On the head tree the sweep above finds no live member (5 .strip() sites all extend with new keys; 0 shape-sharing z.object; the sole strictObjectError shape is unexported), so the accept set as of this head is exactly as declared and no published verdict is wrong today. The declaration of the safeguard is nonetheless false against the repo's own measurement, it is not pinned (no fixture has an open def sharing a strict shape), and the PR's answer to its own flagged boundary rests on it. Verdict-bearing.

4. Generator output. No published artifact moves: the emission loop is untouched, json-schema/ is gitignored and regenerated from that loop, authorable-surface/, the manifest, api-surface, liveness, spec-changes.json are not in the diff, and Build Core plus check:authorable-surface are green on the head. Console text changes only: a new "allowed" line shape and route 4 in the remedy. Note the deletion gate runs in build mode as well as --check (pre-existing; not gated by CHECK), so gen:schema verdicts also gain proof 4. Characterisation ("nothing publishes"): correct.

5. Public surface. The script exports nothing before or after; nothing imports it; the two new imports (strictObjectDeclarations, StrictObjectDeclaration, keySetMatches) are pre-existing exports of src modules already in the eager graph; 0 lines change in packages/spec/src; exit-code semantics unchanged; no error code added or removed. Characterisation: correct.

6. Clause-②: no. Path limb misses (packages/spec/scripts/**); content limb misses (no authorable schema's accept set moves; no *.zod.ts touched). The accept set that widens is the repo gate's, by the maintainer's ruling, not the metadata contract's. The no is a true declaration.

7. Unverified self-narration (not contradicted, not measured): the population figures (1525/1117/144/772 defs and keys; 55 enumerated of 103 sets; 6 empty-shape defs × 9 declarations), the ablation blob hashes, and the local run tallies. Source: PR body and os-dev-report. CI on the head is the evidence for the test results.

② Semver level

skip-changeset is legitimate. Checked: files[] (10 entries, no scripts); tsup.config.ts (1 scripts/ hit, a repo-root helper import, against 22 src/); diff name-status (2 files, both packages/spec/scripts/**); json-schema/ gitignored with 0 tracked files and an untouched emission path; .changeset/ diff 0; AGENTS.md:1066 rule; Check Changeset skipped by the label as designed. Nothing from a released package publishes. No changeset is owed. A patch would be wrong, not merely unnecessary — there is no consumer-visible behaviour to describe.

③ Boundary flags

• open_questions: [] — none declared by the round; none needed beyond the items below.
• Out-of-scope note 1 (registry cannot tell a door from a non-door; "proof 4 works around this by reading additionalProperties: false off the emitted artifact") — the answer is wrong, per ① item 3: under io: 'output' that field is false for strip objects too (ledger l.1535-1541). The gap is latent on this head (sweep above) but the stated defence is not real. Remedy inside the card's fence: decide closure on the Zod instance (catchall of type never on the schema zodByDefKey holds) or restrict the match to declarations recorded by strictObject() rather than strictObjectError(); correct the docblock, PR body and remedy text; add a sandbox fixture where a strip-mode clone shares a strict shape and assert it is refused. Must be closed before landing, or this note must be re-filed as a card with the docblock corrected.
• Out-of-scope note 2 (408 of 1525 emitted defs "not closed") — the figure is measured with the same instrument, so it counts artifacts whose top-level additionalProperties is not false (unions, loose objects, pipes), not the 未知键静默剥离仍是全仓默认:把 #3405 的 strict 收紧从一个 schema 推广到整个可授权面(ADR-0078 完整性闸门) #4001 ledger's strip-site population, which is counted by AST (check-strictness-ledger.mts). Not a defect; the carrier statement should not be read as the strip count.
• Out-of-scope note 3 (ablation-dist-preflight.mjs reports "no dist/" as a refusal) — tooling; correctly declared NOT MEASURED; nothing to answer here.
• Letter B (integration/DataSyncConfig:schedule) not reversed — verified: DataSyncConfigSchema is plain z.object (connector.zod.ts:238), so no declaration matches and proof 4 returns null; pinned as WITHHELD_TOMBSTONE. Closed.
• ADR-0087 disposition — proof 4 does not consult RETIRED_KEYS_BY_MAJOR; the real specimen has an entry (registry.ts:12843) but the proof does not require one. The card's ruling defines the proof as the guidance entry only, and the disposition is enforced on the retiring PR by the clause-② limbs (path limb fires on packages/spec/src/**) and check:adr-0087-registration, not by check (c). Consistent with the ruling; recorded so nobody reads proof 4 as also proving the disposition.
• Enumerated guidanceSets — the PR refuses RegExp sets because a pattern "cannot distinguish retired-with-a-prescription from spelled-like-a-wrong-layer-pointer"; an enumerated wrong-layer set has the same ambiguity and IS honoured. Within the card's definition (the author gets a prescriptive rejection), so accepted; noted as a design boundary.
• charter conflict: does a Clause-②: no PR that touches no contract surface still owe an in-seat review before it can land? #18536 (charter: does a Clause-②: no, non-contract PR owe an in-seat review) — a process ruling, not a code question; must escalate to the maintainer. This record is an at-tier review of the PR; whether it satisfies the charter is charter conflict: does a Clause-②: no PR that touches no contract surface still owe an in-seat review before it can land? #18536's to answer.
• Docs — no page restates the three-proof rule (0 hits, control 2), so nothing is left stale.
• Test "lazy" leg — build-schemas.ts sets OS_EAGER_SCHEMAS=1 at l.6, but ESM import hoisting means the imported schema graph evaluates first, so the env-less spawn is genuinely lazy for the graph; a pre-existing, documented pattern in the test file (l.527-535), not this PR's.

Implemented-by: claude/issue-18301-check-c-fourth-proof
Reviewed-by: session_01LvwGppdonww4zGLWZo5rho

VERDICT: FAIL

Reason, in one line: ① item 3 — the proof's stated "door is closed" condition is a false description of what the gate computes, contradicted by the repo's own recorded measurement, unpinned, and it is the basis on which the PR dismisses its own flagged boundary (note 1); the accept set on this head is nonetheless as declared and nothing published moves, so the fix is confined to the card's two files.

---

Generated by Claude Code

[os-litant]

Contract review

Served-tier: CONTRACT_REVIEW_TIER
Head-sha: 9e0324f8075b168f479204c428e3dd2f2a6c4f58

① Derived judgments

1. Accept set, proof 4 as now built. A deleted authorable-surface/ line D:k is admitted when, at head: D is emitted; D is reachable (proof 2 did not fire); the base entry was NOT [RETIRED]; zodShapeOf(D) is non-empty and matches exactly one strictObjectDeclarations() entry by sorted key set and per-entry instance identity; that declaration's guidance names k, or an enumerated (non-RegExp) guidanceSets.keys does, and k is not in the shape; AND schema.safeParse({ [k]: null }) fails with an unrecognized_keys issue whose keys include k and whose message includes the declared prescription text verbatim. Verified at head l.1452-1553 and l.2554-2596. The artifact read (emitted.additionalProperties !== false, old head l.1405) is gone from code; it survives only as prose saying it does not distinguish. Characterisation: correct.

2. Does the closure test distinguish a closed door from a silent strip? Measured yes. Through the head's own computeGuidanceRoutes, injected as fake defs on the head tree: Strict → prescribed; Strict.strip() → refused; z.object(Strict.shape) → refused; Strict.loose() → refused; z.object(shape, { error: strictObjectError(…) }) with no .strict() → refused; z.union([Strict, Strict.strip()]) → refused; z.object(Strict.shape).strict() without the error map → refused (the case remedy (i) would admit); Strict.optional() → prescribed; Strict.transform(v ⇒ v) → prescribed; z.union([Strict, z.string()]) → refused (conservative). Every stripping form also emits additionalProperties: false, which is the old condition's blindness shown on the instance. Can it still admit a key whose write is dropped? No, by construction: delivers() returns false on result.success === true before any message is read, so a parse that carries or drops the key can never be prescribed; strictUnknownKeyError appends each prescription verbatim as a bullet (suggestions.zod.ts l.489-494), so the includes needle is sound.

3. Refuse set. Two refusals for the un-marked branch instead of one: none keeps the byte-identical "was LIVE (never tombstoned)" line; declared-but-silent is a new violation line. Both exit 1, so the third verdict changes wording only, never admission. Its text lists possible reasons without asserting one. Proofs 1-3, checks (a)/(b), the defaults ratchet and the anchor writer are byte-untouched outside the listed hunks; proof 4 stays under !wasRetired, pinned by the data/Object:compactLayout [RETIRED] leg (my census: that key IS prescribed at the def, and the call-site gate is what keeps it on proof 1's clock). Characterisation: correct.

4. The live specimen, executed. Both twins are emitted with additionalProperties: false; both resolve to the SAME declaration object (dOpen === dClosed true, surface server.security.rateLimit, and declaration.shape === RateLimitConfigSchema.shape true). shared/RateLimitConfig: safeParse({keyBy:null}) succeeds, keyBy absent from the output, HEAD verdict declared-but-silent, OLD head prescribed = true (the hole executed through the old code). system/ServerRateLimitConfig: parse fails, unrecognized_keys present, message carries the keyBy prescription verbatim, HEAD prescribed. Same for store. data/Metric:filters prescribed; data/Metric:zzNotPrescribed18301 none; integration/DataSyncConfig:schedule none (plain open object, key dropped on parse — letter B's territory, untouched).

5. Census, re-derived with the head's verbatim function. Emitted defs 1525 ✓; artifacts with additionalProperties === false 1117 ✓; keys promised 779 ✓; delivered 770 ✓; not delivered 9 ✓; of the 9, 2 on shared/RateLimitConfig ✓ and 7 keys on 3 union defs (ui/ChartGroupBy ×2, ui/RecordHighlightsField ×1, ui/ViewItem ×4). The old head's figures reproduce exactly (144 defs / 772 keys), which validates the instrument. Two figures do not reproduce: the PR body row "defs resolving to exactly one declaration that names an undeclared key: 258" measures 147; 258 is the count of defs resolving to exactly one declaration whether or not it names anything (ambiguous matches 0, empty-shape 6, no-shape 303). And the shipped docblock (l.1440-1441) says "7 of the 8 defs in that state are unions"; measured, the state holds 9 keys on 4 defs, 3 of them unions. Both are census prose, not safeguard claims, and the rationale they support (unions dominate the not-delivered set) still holds; both should be corrected on the next touch. Reachability labels (root-graph / derived-clone) NOT MEASURED, source: PR body.

6. Generator output and public surface. Emission loop untouched; json-schema/ gitignored; authorable-surface/, manifest, api-surface, liveness, spec-changes.json not in the diff; packages/spec/src tree hash unchanged; the script exports nothing; the imports (strictObjectDeclarations, StrictObjectDeclaration, keySetMatches) are pre-existing src exports. Console text: one new "allowed" line shape, one new violation shape, route 4 in the remedy. CI on head: Build Core, all Type Check jobs, Test Core (6 shards + aggregate), Governed Surface Queue Guard, Spec property liveness, Dogfood, Temporal Conformance all success; Lint & Repo Gates in progress at last poll; 0 failures. Characterisation ("nothing publishes"): correct.

7. Clause-②: no. Path limb (packages/spec/src/**, the clause-② suspect glob at dispatch-gates.mjs:22241) misses packages/spec/scripts/**; content limb misses (no *.zod.ts touched, no authorable schema's accept set moves). The accept set that widens is the repo gate's, by the [finding] the authorable-key deletion gate's reachability BFS reports integration/DataSyncConfig unreachable from the metadata-type roots — it is two hops from the connector root, so #4650 proof 2 waives a tombstone for a key a stack manifest really authors #17356 ruling. A true declaration.

8. Pre-existing vacuous negatives — verified on the old head. The five rx(K, 'shape is CLOSED') negatives (eager l.1403/1409/1415/1425, lazy l.1437) could never match: the old gate emitted K — def REACH, and its shape is CLOSED…, and the regex demanded K — shape is CLOSED; applied to the old head's own admitted line for data/Metric:filters it returns false. The claim "every negative" is one short: the sixth (def not reachable from the, l.1393) was live. What the earlier green meant: each key emits exactly one verdict line (continue after every push), and the eager positives pinned each key's correct verdict, so the vacuous negatives were redundant there; only the lazy-leg agedKey negative (l.1437) had no positive counterpart and asserted nothing. The new negatives verified able to hit their own admitted and third-verdict lines, and the allowed regex verified not to match the third verdict.

② Semver level

skip-changeset remains legitimate at +694/-11. Checked: files[] (10 entries, no scripts); tsup.config.ts (1 scripts/ hit, the repo-root tsup-drop-sources-content.mjs import, against 22 src/); three-dot name-status is the two packages/spec/scripts/** files and nothing under .changeset/; AGENTS.md:1066 (skip-changeset is for a diff that publishes nothing from any released package); Check Changeset skipped by the label as designed. Size is not the criterion; publication is, and nothing publishes. No changeset is owed and a patch would describe no consumer-visible behaviour.

③ Boundary flags

• Continued past the stop instruction — judged sound. Antecedent measured true: the old code admits shared/RateLimitConfig:keyBy (OLD prescribed = true in my run). Consequent measured false: the PR is draft and unmerged; keyBy/store are 0 in the baseline and 0 in authorable-surface/ against a lit control of 1 for enabled; a guidance-only key was never in the shape, so it was never a baseline line and no deletion could ever ask proof 4 about it, even had the old head merged. Stopping would have left a proven-wrong proof in a draft; the dev reported the deviation instead of concealing it and handed the real trap to triage rather than acting on it. The residual is process, not code: whether a dev may read a stop instruction by its stated rationale is the seat's to rule, and it was disclosed for exactly that.
• Neither remedy taken — the load-bearing claim about (ii) is TRUE. Both twins match the same declaration object, which strictObject() itself registered (strictObject is z.object(shape, { error: strictObjectError(...) }).strict(), one declarationStore().push per call), so restricting the match to strictObject()-recorded declarations admits both twins; and it would be a strict-object.ts edit across the path limb. On (i): catchall-of-never does separate the twins (open false, closed true) and agrees with the probe on 776 of 779 promised keys; it diverges on 3 (security/ObjectPermission, a transform pipe where instance unwrapping fails, fail-closed) and it admits z.object(Strict.shape).strict() without the map, which the probe refuses. On the card's own definition ("a prescriptive rejection"), the probe is strictly stronger. Refusal reasons hold.
• Real specimen instead of a synthetic fixture — pins the same property and IS a discriminator. Open def, strict declaration, identical shape entries, refused; closed twin admitted; one run, one declaration, opposite verdicts; the beforeAll guard holds the four tree facts loudly. The sandbox symlinks src/ (test l.455), so a synthetic case would have needed a src mutation or a new seam. I ran the synthetic forms myself (item ① 2) and all are refused, but note the residual: the message-includes half of delivers() (strict clone without the map) is pinned by no fixture — defended by construction and by census (0 such defs on the shipped graph).
• Third verdict and the negatives fix — in scope and fail-closed. A violation cannot widen admission; the wording states only that the prescription did not arrive. The negatives fix is inside the card's files and its claim is verified above.
• Ablations C and D — NOT re-run; consistent by inspection. delivers → true makes every promised key prescribed, so the twins case's two injected keys are both admitted and the run exits 0; delivers → false makes every promised key declared-but-silent, so both positive legs fall to the third verdict. My OLD-vs-HEAD verdicts on the open twin are the same fact as C's outcome. Blob hashes, marker counts and exit codes: source os-dev-report.
• Gate reconciliation. dispatch-gates.mjs --commands over the two paths derives 61 families here (from the shared checkout's tree at 582d3e54e, which the tool flags as 7 commits stale; the stale file is not in the list), including the five dist-needing gates and check-reference-carrier-shape (still present on origin/main at 879b5127). Deriving on c38660f5f rather than 9e0324f8 does not matter: the derivation is path-based and the path set is byte-identical; the report's "derived ON THIS HEAD" is imprecise by one wording-only commit. Which gates were re-run after that final commit is stated only for test:repo, typecheck, check:authorable-surface and lint; only test:repo could see that commit. The 5 exit-3 gates are correctly NOT MEASURED.
• 124 then 0 — honest, not a re-roll. The repo's own dispatch-gates.mjs (l.12070-12109) classifies exit 124 as "a timeout wrapper fired and signalled the child", a kill rather than a verdict; the gate is deterministic over the tree; both readings were disclosed. Timing NOT MEASURED.
• mcp_calls: 0 NOT MEASURABLE from this seat. The 3 REST writes are consistent with observables: PR body updated_at 02:32:01Z; report comment created 02:33:15Z and updated 02:34:24Z (one PATCH); labels size/l, tests, tooling, skip-changeset with size/l from the labeler.
• Two census misstatements owed a correction (item ① 5): PR body "258" mislabeled (147 for that label) and docblock "7 of the 8 defs" (9 keys on 4 defs, 3 unions). Neither moves a verdict or describes a safeguard.
• Fail-closed edges, not defects: (a) promisesFor skips RegExp sets before the !owed.has precedence check while strictUnknownKeyError walks all sets in declaration order, so a RegExp set declared before an enumerated set naming the same key would refuse a legitimate retirement — none on the shipped graph (all 9 non-deliveries explained); (b) an empty-string prescription would pass includes('') at the gate while falling through at runtime — 0 exist against 135 tables; (c) computeGuidanceRoutes() snapshots the registry at call time and my run saw it grow 553→557 as z.lazy getters fired later, a declaration built after the snapshot reads 'none' — in the gate the JSON-Schema pass precedes the call, as the docblock relies on; (d) 7 union keys refused although a member refuses with the prescription — deliberate.
• Unchanged from the FAIL record: proof 4 does not consult RETIRED_KEYS_BY_MAJOR (not a disposition proof); letter B is not reversed (DataSyncConfig has no route, measured); no doc restates the proof rule; the --self-test in the card's suggested acceptance is delivered as vitest cases, the gate having no such mode.
• Declared out of scope, correctly: the open twin drops keyBy/store in silence on a live authorable surface (packages/spec/src/**), handed to triage as a class-(c) card. packages/spec/src on origin/main has since moved in expression.zod.ts and translation.zod.ts; irrelevant to this head, the census may shift post-merge. charter conflict: does a Clause-②: no PR that touches no contract surface still owe an in-seat review before it can land? #18536 (whether a Clause-②: no PR owes this review) stays a charter question for the maintainer.

Implemented-by: claude/issue-18301-check-c-fourth-proof
Reviewed-by: session_01LvwGppdonww4zGLWZo5rho

VERDICT: PASS

Reason, in one line: the FAIL's one verdict-bearing item is closed — closure is decided at the def by a probe that, executed here through the head's own function, refuses every open form and admits only a delivered prescription; the false safeguard claim is gone from code, docblock, remedy and body; the real-specimen pin discriminates and is green in CI; nothing published moves and both declarations are true — with two census figures in prose (258; "7 of the 8 defs") measured wrong and owed a one-line correction on the next touch.

---

Generated by Claude Code