Keyboard shortcuts

Press ← or β†’ to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help


id: linter.schema_shape kind: intent statement: β€œWHEN a spec file’s frontmatter has passed, THE linter SHALL reject it if any 𝒦-governed id-set (a variant table, a Constraint/Property kind value-set, or the Reference Typing table’s field set) shrinks, reorders, or silently retypes an existing member across revisions, if a Constraint or Property row’s own kind value falls outside its closed set, or if the parser has touched content inside a rationale/description field.”

Linter: Schema Shape Check

Runs after linter.frontmatter only, in parallel with linter.ears_syntax and the referential/graph/model branch β€” per specodelic.md’s Checker Ownership table, this checker and linter.ears_syntax are independent terminal nodes that both feed into linted, not a sequential continuation of one another.

Note this checker’s scope narrowed relative to its first mention in the decomposition plan: no_boolean_columns ended up owned by linter-model_shape.md instead, scoped specifically to state/transition rows where a boolean column would actually manifest as an ad-hoc state machine. What’s left here is schema evolution discipline (append_only_variants), the closed-set discipline on the kind column that Constraint and Property rows each separately carry (see kinds.md), and the parser’s own restraint around prose (prose_untouched) β€” three properties about how the tooling behaves across time, across the kind column specifically, and across fields generally, rather than about any single file’s current shape.

Purpose

Runs after linter.frontmatter only, in parallel with linter.ears_syntax and the referential/graph/model branch β€” per specodelic.md’s Checker Ownership table, this checker and linter.ears_syntax are independent terminal nodes that both feed into linted, not a sequential continuation of one another. Note this checker’s scope narrowed relative to its first mention in the decomposition plan: no_boolean_columns ended up owned by linter-model_shape.md instead, scoped specifically to state/transition rows where a boolean column would actually manifest as an ad-hoc state machine. What’s left here is schema evolution discipline (append_only_variants), the closed-set discipline on the kind column that Constraint and Property rows each separately carry (see kinds.md), and the parser’s own restraint around prose (prose_untouched) β€” three properties about how the tooling behaves across time, across the kind column specifically, and across fields generally, rather than about any single file’s current shape.

Constraints

| id | kind | expr | traces_to | satisfies | |–––––––––––––|———–|–––––––––––––––––––––––––––––––––––––––––––––––––|—————————————————–| | id_set_grows_only | invariant | βˆ€ 𝒦-governed id-set S (a variant-table's ids, a Constraint/Property row's own kind value-set, or the Reference Typing table's field set), revision r < r': S(r) βŠ† S(r'), appended only under a new Revision heading β€” no member removed or renumbered; a member's typing may narrow only in the same Revision that introduces the kind-split it depends on, and only if it invalidates nothing valid at r | [[linter.schema_shape]] | | | id_set_order_stable | invariant | βˆ€ 𝒦-governed id-set S, revision r < r': the relative order of members present in both r and r' is unchanged | [[linter.schema_shape]] | | | constraint_kind_closed | invariant | βˆ€ Constraint row: row.kind ∈ {invariant, advisory, effect, extension_point}, extended per-file by the active packs' declared kinds (openspec/specs/packs/spec.md fiber kinds β€” base βˆͺ active-pack-fiber, never narrower; without the pack active the token stays outside the closed set and the labeled finding fires) β€” see [[kinds.constraint_row_shape]] | [[linter.schema_shape]] | | | property_kind_closed | invariant | βˆ€ Property row: row.kind ∈ {unit, law}, extended per-file by the active packs' declared kinds (openspec/specs/packs/spec.md fiber kinds β€” base βˆͺ active-pack-fiber, never narrower; without the pack active the token stays outside the closed set and the labeled finding fires) β€” see [[kinds.property_row_shape]] | [[linter.schema_shape]] | | | no_prose_field_parsed | invariant | the parser's AST never branches on the text content of a rationale/description field | [[linter.schema_shape]] | | | prose_field_passthrough | invariant | rationale/description content is stored verbatim and emitted verbatim in the compiled TOML | [[linter.schema_shape]] | | | kind_check_failure | effect | linter.schema_shape.kind_check_failure(detail) | [[linter.schema_shape]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | diff_failure | effect | linter.schema_shape.diff_failure(detail) | [[linter.schema_shape]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | parser_audit_failure | effect | linter.schema_shape.parser_audit_failure(detail) | [[linter.schema_shape]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] |

Model

States

  • unchecked
  • kind_checking
  • diffing
  • parser_audited
  • passed
  • kind_failed (emits: [[linter.schema_shape.kind_check_failure]])
  • diff_failed (emits: [[linter.schema_shape.diff_failure]])
  • parser_audit_failed (emits: [[linter.schema_shape.parser_audit_failure]])

Transitions

idfromtoguard
beginuncheckedkind_checkingfile passed linter.frontmatter
kind_okkind_checkingdiffing[[linter.schema_shape.constraint_kind_closed]] ∧ [[linter.schema_shape.property_kind_closed]]
kind_failkind_checkingkind_failed¬([[linter.schema_shape.constraint_kind_closed]] ∧ [[linter.schema_shape.property_kind_closed]])
diff_okdiffingparser_audited[[linter.schema_shape.id_set_grows_only]] ∧ [[linter.schema_shape.id_set_order_stable]]
diff_skipdiffingparser_auditedno prior revision exists in repo history β€” nothing to diff against yet
diff_faildiffingdiff_failed¬([[linter.schema_shape.id_set_grows_only]] ∧ [[linter.schema_shape.id_set_order_stable]])
acceptparser_auditedpassed[[linter.schema_shape.no_prose_field_parsed]] ∧ [[linter.schema_shape.prose_field_passthrough]]
rejectparser_auditedparser_audit_failed¬([[linter.schema_shape.no_prose_field_parsed]] ∧ [[linter.schema_shape.prose_field_passthrough]])

Properties

idkindderives_fromgeneratorpredicate
shrunk_id_set_rejectedunit[[linter.schema_shape.id_set_grows_only]](revision_n, revision_n_plus_1) where a member was removed from a variant table, a kind value-set, or the Reference Typing tablecheck(revisions) == failed β€” one generator, parametrized over which of the three id-sets it targets
reordered_id_set_rejectedunit[[linter.schema_shape.id_set_order_stable]](revision_n, revision_n_plus_1) where two existing members of any 𝒦-governed id-set swapped ordercheck(revisions) == failed
silent_narrowing_rejectedunit[[linter.schema_shape.id_set_grows_only]](revision_n, revision_n_plus_1) where a Reference Typing field’s target narrowed with no accompanying kind-split citedcheck(revisions) == failed
constraint_kind_invalid_rejectedunit[[linter.schema_shape.constraint_kind_closed]]constraint_row_with(kind: "made_up")check(file) == failed
property_kind_invalid_rejectedunit[[linter.schema_shape.property_kind_closed]]property_row_with(kind: "audit")check(file) == failed
kind_closed_passesunit[[linter.schema_shape.constraint_kind_closed]]arbitrary_file_with(only_closed_kind_values: true)check(file) == passed
prose_roundtripsunit[[linter.schema_shape.prose_field_passthrough]]arbitrary_unicode_string() as rationale contentcompile(parse(s)).rationale == s β€” no normalization, no truncation
appended_id_set_member_passesunit[[linter.schema_shape.id_set_grows_only]](revision_n, revision_n_plus_1) where only new members were added, to any of the three id-setscheck(revisions) == passed
constraint_kind_advisory_passesunit[[linter.schema_shape.constraint_kind_closed]]constraint_row_with(kind: "advisory")check(file) == passed
constraint_kind_effect_passesunit[[linter.schema_shape.constraint_kind_closed]]constraint_row_with(kind: "effect")check(file) == passed
constraint_kind_extension_point_passesunit[[linter.schema_shape.constraint_kind_closed]]constraint_row_with(kind: "extension_point")check(file) == passed
parser_ast_prose_freeunit[[linter.schema_shape.no_prose_field_parsed]]spec_file_with(prose_in_rationale_and_description: arbitrary_unicode_string())βˆ€ parsed row: the row's parsed fields contain no fragment of the planted prose β€” a planted-prose differential parse (see Notes)
kind_check_failure_label_assertedunit[[linter.schema_shape.kind_check_failure]]kind_check_failure_raised()error_label == "linter.schema_shape.kind_check_failure" β€” renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
diff_failure_label_assertedunit[[linter.schema_shape.diff_failure]]diff_failure_raised()error_label == "linter.schema_shape.diff_failure" β€” renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
parser_audit_failure_label_assertedunit[[linter.schema_shape.parser_audit_failure]]parser_audit_failure_raised()error_label == "linter.schema_shape.parser_audit_failure" β€” renaming the label touches the error Constraint, this property, and its note together (EDGE-002)

Notes

Fiber-kind acceptance (2026-10-03, beads specodelic-ung): the two closed-set walkers above walk the static base sets β€” a pack-declared fiber kind (e.g. empirical.statistic, the empirical-registry pack’s property kind, which targets the base Properties kind column directly) fired the finding even with the pack discovered. The walkers’ effective set is now base βˆͺ active-pack-fiber: the ## Kinds tokens of every pack active for the file (declared uses edge or vocabulary match, the advisory-first activation rule in openspec/specs/packs/spec.md). Never narrower than the base set β€” a base-set member is accepted unconditionally, the base sets themselves do not grow (id_set_grows_only untouched, no format Revision), and a fiber kind with no active declaring pack stays outside the closed set, firing the labeled finding β€” never a silent pass. The existing acceptance rows (constraint_kind_invalid_rejected, property_kind_invalid_rejected, kind_closed_passes) keep their meaning: made_up/audit are still outside any effective set, declared or not.

Reference-typing reconciliation (2026-09-30, specodelic-cxq): the Constraints table’s traces_to cells previously pointed at the specodelic.md rows these checks re-own β€” a Constraintβ†’Constraint target, which the Reference Typing table forbids (traces_to resolves to Intent only). Each now traces to this file’s own intent: specodelic.md keeps the corpus-wide statement of record, this file owns the checkable one (the β€œsame claim, two altitudes” pattern the Notes below already use).

Resolves the follow-up kinds.md recorded when it landed: that file defined property_row_shape’s kind ∈ {unit, law} and constraint_row_shape’s kind ∈ {invariant}, and specodelic.md Revision 4 added the corresponding top-level invariants (constraint_kind_closed, property_kind_closed), but no checker enforced either yet. This file now does, as the first gate after linter.frontmatter and before the existing revision-diffing β€” a Property row with an invalid kind should fail here regardless of whether the file has any revision history to diff against at all, which is why kind_checking sits ahead of diffing rather than folded into it: the two checks have genuinely different preconditions (kind_checking needs only the current file; diffing needs a prior revision, hence the new diff_skip edge for a file with none).

no_prose_field_parsed was originally framed as a property of the parser’s implementation, not of any spec file’s content β€” β€œno generator can produce a bad spec file to test this against, only an audit of whether the parser code path for rationale/description ever appears on the left side of a conditional.” The parser_ast_prose_free row above reflects the pre-decision audit framing and predates the decision below.

Decision of record (2026-09-30, user-approved; HITL ticket specodelic-mp1 row 5, EXCL-001): the audit framing was wrong β€” the claim is mechanically testable by a planted-prose differential parse (generate a spec with prose in rationale/description, parse, assert no parsed row contains it). The property is to be rewritten as a runnable unit row on that basis (lands with specodelic-cxq); no audit kind was added β€” kinds.md Revision 6 records the dissolution and {unit, law} stays closed. This row’s Needs Human Review flag is retired. Landed here with specodelic-cxq: parser_ast_prose_free is now the runnable planted-prose differential parse (generate a spec with prose in rationale/description, parse, assert no parsed row contains it) β€” no generator-preclusion claim remains.

Checker Ownership table in specodelic.md is now fully accounted for except linter-coverage.md, the last remaining file.

Previous pass (resolving specodelic.md Revision 5’s two pending items): constraint_kind_closed widened to {invariant, advisory} in step with kinds.md Revision 2, and a reference_table_grows_only constraint was added for the Reference Typing table specifically.

This pass (specodelic.md Revision 6): that separate reference_table_grows_only constraint, along with the older variant_set_grows_only/variant_order_stable pair, is retired and replaced by the two rows above β€” id_set_grows_only and id_set_order_stable β€” stated once, over any 𝒦-governed id-set, rather than three times over three id-sets that all follow the identical rule. No enforcement was lost: the same three id-sets (variant tables, kind value-sets, the Reference Typing table) are still covered, by the same diffing state and the same diff_skip fallback for a file with no prior revision to diff against β€” only the naming collapsed from three constraints to two. constraint_kind_closed widens again, to {invariant, advisory, effect}, in step with kinds.md Revision 3. no_prose_field_parsed remains the one row here still marked Needs Human Review; nothing in this pass touches it. (Historical note: the flag was retired 2026-09-30 β€” see the decision of record above; this paragraph predates that.)

This pass (specodelic.md Revision 7): constraint_kind_closed widens a third time, to {invariant, advisory, effect, extension_point}, in step with kinds.md Revision 4. constraint_kind_extension_point_passes added as the matching acceptance case, same shape as the advisory/ effect rows above it. Nothing else in this file changes: id_set_grows_only already covers any Constraint-kind value-set widening generically, so an extension_point addition is diffed by the same diffing state as any other, with no new branch.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: shrunk_id_set_rejected

  • WHEN (revision_n, revision_n_plus_1) where a member was removed from a variant table, a kind value-set, or the Reference Typing table
  • THEN check(revisions) == failed β€” one generator, parametrized over which of the three id-sets it targets
  • VERIFIES [[linter.schema_shape.shrunk_id_set_rejected]]

Scenario: reordered_id_set_rejected

  • WHEN (revision_n, revision_n_plus_1) where two existing members of any 𝒦-governed id-set swapped order
  • THEN check(revisions) == failed
  • VERIFIES [[linter.schema_shape.reordered_id_set_rejected]]

Scenario: silent_narrowing_rejected

  • WHEN (revision_n, revision_n_plus_1) where a Reference Typing field’s target narrowed with no accompanying kind-split cited
  • THEN check(revisions) == failed
  • VERIFIES [[linter.schema_shape.silent_narrowing_rejected]]

Scenario: constraint_kind_invalid_rejected

  • WHEN constraint_row_with(kind: "made_up")
  • THEN check(file) == failed
  • VERIFIES [[linter.schema_shape.constraint_kind_invalid_rejected]]

Scenario: property_kind_invalid_rejected

  • WHEN property_row_with(kind: "audit")
  • THEN check(file) == failed
  • VERIFIES [[linter.schema_shape.property_kind_invalid_rejected]]

Scenario: kind_closed_passes

  • WHEN arbitrary_file_with(only_closed_kind_values: true)
  • THEN check(file) == passed
  • VERIFIES [[linter.schema_shape.kind_closed_passes]]

Scenario: prose_roundtrips

  • WHEN arbitrary_unicode_string() as rationale content
  • THEN compile(parse(s)).rationale == s β€” no normalization, no truncation
  • VERIFIES [[linter.schema_shape.prose_roundtrips]]

Scenario: appended_id_set_member_passes

  • WHEN (revision_n, revision_n_plus_1) where only new members were added, to any of the three id-sets
  • THEN check(revisions) == passed
  • VERIFIES [[linter.schema_shape.appended_id_set_member_passes]]

Scenario: constraint_kind_advisory_passes

  • WHEN constraint_row_with(kind: "advisory")
  • THEN check(file) == passed
  • VERIFIES [[linter.schema_shape.constraint_kind_advisory_passes]]

Scenario: constraint_kind_effect_passes

  • WHEN constraint_row_with(kind: "effect")
  • THEN check(file) == passed
  • VERIFIES [[linter.schema_shape.constraint_kind_effect_passes]]

Scenario: constraint_kind_extension_point_passes

  • WHEN constraint_row_with(kind: "extension_point")
  • THEN check(file) == passed
  • VERIFIES [[linter.schema_shape.constraint_kind_extension_point_passes]]

Scenario: parser_ast_prose_free

  • WHEN spec_file_with(prose_in_rationale_and_description: arbitrary_unicode_string())
  • THEN βˆ€ parsed row: the row's parsed fields contain no fragment of the planted prose β€” a planted-prose differential parse (see Notes)
  • VERIFIES [[linter.schema_shape.parser_ast_prose_free]]

Scenario: kind_check_failure_label_asserted

  • WHEN kind_check_failure_raised()
  • THEN error_label == "linter.schema_shape.kind_check_failure" β€” renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
  • VERIFIES [[linter.schema_shape.kind_check_failure_label_asserted]]

Scenario: diff_failure_label_asserted

  • WHEN diff_failure_raised()
  • THEN error_label == "linter.schema_shape.diff_failure" β€” renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
  • VERIFIES [[linter.schema_shape.diff_failure_label_asserted]]

Scenario: parser_audit_failure_label_asserted

  • WHEN parser_audit_failure_raised()
  • THEN error_label == "linter.schema_shape.parser_audit_failure" β€” renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
  • VERIFIES [[linter.schema_shape.parser_audit_failure_label_asserted]]