Skip to content

[finding] check (c) has no proof shape for a strict-schema guidance retirement — on a reachable def such a key can never prove itself, and it passed only because proof 2 was broken #18132

Description

@claude

Reported by the os-dev round on #17356 and filed by the domain:spec seat (a dev reports the three classes; the seat files them). This is option C of that card's blocker, stated as the general defect rather than the one instance.

The gap

packages/spec/scripts/build-schemas.ts check (c) admits three proofs for an authorable-surface/ baseline line that disappeared:

  1. the key was tombstoned — retiredKey() → a [RETIRED] mark — and declared in RETIRED_KEYS_BY_MAJOR;
  2. the def is not reachable from the metadata-type roots;
  3. the whole def stopped being emitted.

A key retired the strict-schema way — removed from the shape outright, with its prescription left in a guidance / UNKNOWN_KEY_GUIDANCE entry — never produces the [RETIRED] mark at all, so proof 1 can structurally never apply to it. On a def that IS reachable, proofs 2 and 3 do not apply either.

a completed, correctly-executed retirement has no proof shape available to it.

The live specimen

data/Metric:filters, removed by #10414 under ADR-0049 with a full guidance entry on MetricSchema (packages/spec/src/data/analytics.zod.ts) carrying the prescription and an os migrate meta --from 17 line — a textbook retirement.

⚠️ It has been passing the gate only because proof 2 was broken: data/Metric was judged unreachable, so the deletion was waived for the wrong reason. #17356 fixes proof 2, and the moment it does, this key has nothing left to prove itself with and reds the build.

⇒ the gate was green on a false premise, and correcting the premise exposes the hole. ⛔ That is an argument for filling the hole, not for leaving proof 2 broken.

Why it is a finding rather than a note

Class (b), violating a declared contract: check (c)'s own documented contract is that a line may leave the file when the retirement was done properly. The strict-schema guidance route is a proper retirement — ADR-0049 sanctions it — and the gate cannot recognise it. The author did everything right and the gate refuses.

Suggested shape (⛔ not a ruling — the owning seat decides)

A fourth proof: a key whose def carries a guidance / UNKNOWN_KEY_GUIDANCE entry naming exactly that key proves its own retirement, the way a retiredKey() tombstone does. That keeps the gate's strictness — an undeclared deletion still has nothing to show — while giving the sanctioned route a machine-checkable proof.

⚠️ NOT measured and ⛔ not claimed here: how many other already-deleted keys are in this same position. #17356's round measured that exactly 2 of the anchor's 927 already-deleted keys flip waived→refused under the corrected roots, and only one of those two (Metric:filters) is a guidance-route retirement — but that is a count against one anchor, ⛔ not a census of the shape.

查重词

check (c) proof · strict schema guidance · UNKNOWN_KEY_GUIDANCE · RETIRED mark · tombstone proof shape

⛔ Not de-duplicated by this seat — 「立卡者不查重,只附 3–5 个查重词」. Filed bare (no domain:*, no priority:*): 「执行席永不定级或路由裸卡」.


Generated by Claude Code

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions