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
uncheckedkind_checkingdiffingparser_auditedpassedkind_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
| id | from | to | guard |
|---|---|---|---|
| begin | unchecked | kind_checking | file passed linter.frontmatter |
| kind_ok | kind_checking | diffing | [[linter.schema_shape.constraint_kind_closed]] β§ [[linter.schema_shape.property_kind_closed]] |
| kind_fail | kind_checking | kind_failed | Β¬([[linter.schema_shape.constraint_kind_closed]] β§ [[linter.schema_shape.property_kind_closed]]) |
| diff_ok | diffing | parser_audited | [[linter.schema_shape.id_set_grows_only]] β§ [[linter.schema_shape.id_set_order_stable]] |
| diff_skip | diffing | parser_audited | no prior revision exists in repo history β nothing to diff against yet |
| diff_fail | diffing | diff_failed | Β¬([[linter.schema_shape.id_set_grows_only]] β§ [[linter.schema_shape.id_set_order_stable]]) |
| accept | parser_audited | passed | [[linter.schema_shape.no_prose_field_parsed]] β§ [[linter.schema_shape.prose_field_passthrough]] |
| reject | parser_audited | parser_audit_failed | Β¬([[linter.schema_shape.no_prose_field_parsed]] β§ [[linter.schema_shape.prose_field_passthrough]]) |
Properties
| id | kind | derives_from | generator | predicate |
|---|---|---|---|---|
| shrunk_id_set_rejected | unit | [[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 table | check(revisions) == failed β one generator, parametrized over which of the three id-sets it targets |
| reordered_id_set_rejected | unit | [[linter.schema_shape.id_set_order_stable]] | (revision_n, revision_n_plus_1) where two existing members of any π¦-governed id-set swapped order | check(revisions) == failed |
| silent_narrowing_rejected | unit | [[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 cited | check(revisions) == failed |
| constraint_kind_invalid_rejected | unit | [[linter.schema_shape.constraint_kind_closed]] | constraint_row_with(kind: "made_up") | check(file) == failed |
| property_kind_invalid_rejected | unit | [[linter.schema_shape.property_kind_closed]] | property_row_with(kind: "audit") | check(file) == failed |
| kind_closed_passes | unit | [[linter.schema_shape.constraint_kind_closed]] | arbitrary_file_with(only_closed_kind_values: true) | check(file) == passed |
| prose_roundtrips | unit | [[linter.schema_shape.prose_field_passthrough]] | arbitrary_unicode_string() as rationale content | compile(parse(s)).rationale == s β no normalization, no truncation |
| appended_id_set_member_passes | unit | [[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-sets | check(revisions) == passed |
| constraint_kind_advisory_passes | unit | [[linter.schema_shape.constraint_kind_closed]] | constraint_row_with(kind: "advisory") | check(file) == passed |
| constraint_kind_effect_passes | unit | [[linter.schema_shape.constraint_kind_closed]] | constraint_row_with(kind: "effect") | check(file) == passed |
| constraint_kind_extension_point_passes | unit | [[linter.schema_shape.constraint_kind_closed]] | constraint_row_with(kind: "extension_point") | check(file) == passed |
| parser_ast_prose_free | unit | [[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_asserted | unit | [[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_asserted | unit | [[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_asserted | unit | [[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]]