Skip to content

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

Description

@os-elon-musk

Filed by the director seat (session_01WCEaPsmKY4UyoivKkkaUHt) executing the ruling on #17356 — batch #135 item 3, maintainer 「135 同意」 on the seat's recommendation A + C as its own card. This is the C half. ⛔ Not a decision: the direction is ruled; this card is execution.

What is wrong

packages/spec/scripts/build-schemas.ts check (c) admits a deleted authorable-surface/ baseline line on three proofs: (1) a [RETIRED] mark from a retiredKey() tombstone, (2) the def is unreachable from the metadata-type roots, (3) the ADR-0087 disposition entry. A key retired the strict-schema / guidance way — removed from the shape, prescription left in a UNKNOWN_KEY_GUIDANCE / guidance entry — never gets the [RETIRED] mark, so proof 1 can never apply to it. On a reachable def that leaves it with no proof shape at all.

It passed until now only because proof 2 was broken (#17356: the BFS root set omitted the four unregistered kinds, so connector/analytics_cube/sharing_rule/webhook defs read as unreachable and every deletion under them was waived). PR #18131 repairs proof 2; the repaired gate then reds on data/Metric:filters — a completed guidance-route retirement on a reachable def (MetricSchema ← root analytics_cube .measures, 2 hops) with nothing to prove itself with.

Measured by the #17356 dev (report 5659442175): over 1523 emitted defs the repaired root set moves 24 verdicts; 17 defs stop being waivable. Metric:filters is the live specimen of this class; DataSyncConfig:schedule is a different case (an explicit maintainer ruling, 2026-09-10, that deliberately withheld the tombstone) and is handled by advancing the anchor under the same ruling's A half, ⛔ not by this card.

What to build

A fourth proof for check (c): a deleted baseline line is legitimate when the key's def is reachable AND the tree carries a guidance entry (UNKNOWN_KEY_GUIDANCE or the equivalent strict-schema prescription) naming that key — i.e. the author who keeps writing it gets a prescriptive rejection rather than a silent parse. The proof must be read from the tree, not from prose.

Suggested acceptance

  • --self-test case: a reachable def whose key is removed from the shape with a guidance entry passes check (c) via proof 4; the same deletion without the guidance entry still fails (the conservative direction is kept).
  • data/Metric:filters passes on main via proof 4 once fix(spec): the authorable-surface reachability roots include the unregistered kind schemas #18131's repaired root set is in.
  • Proof 2's repaired conservatism is untouched: a genuinely unreachable def still reads null and is still waived only by proof 2.
  • The gate's docblock names four proofs.

Governing text

Refs: #17356 · PR #18131 · #4650 · #6245 (the unregistered kinds stay unregistered) · #16320 (the schedule retirement).


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

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions