id: linter.referential_integrity kind: intent statement: “WHEN a spec repo is parsed, THE linter SHALL reject it if any row id is duplicated within a file or any wiki-link reference fails to resolve to a defining row.”

Linter: Referential Integrity Check

Runs after linter.frontmatter passes for every file in the repo — it needs every file’s declared id to already be trustworthy before it can build the id→row index this check relies on.

Purpose

Runs after linter.frontmatter passes for every file in the repo — it needs every file’s declared id to already be trustworthy before it can build the id→row index this check relies on.

Constraints

| id | kind | expr | traces_to | satisfies | |–––––––––––|———–|—————————————————————————————––|–––––––––––––––––––––––––| | unique_within_file | invariant | ∀ file: no two rows in file share the same local id | [[linter.referential_integrity]] | | | unique_across_repo | invariant | ∀ repo: no two files declare the same fully-qualified id | [[linter.referential_integrity]] | | | ref_resolves | invariant | ∀ [[ref]] in file: qualify(ref) ∈ index(repo) | [[linter.referential_integrity]] | | | ref_kind_compatible | invariant | ∀ [[ref]] in any reference field defined by specodelic.md's Reference Typing table: target row's kind ∈ allowed_targets(field) — read from that table, not hardcoded per field name, so a Revision adding a field (supersedes, emits, …) needs no change here | [[linter.referential_integrity]] | | | index_failure | effect | linter.referential_integrity.index_failure(detail) | [[linter.referential_integrity]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | resolution_failure | effect | linter.referential_integrity.resolution_failure(detail) | [[linter.referential_integrity]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] |

Model

States

• unindexed
• indexing
• indexed
• resolving
• passed
• index_failed (emits: [[linter.referential_integrity.index_failure]])
• resolution_failed (emits: [[linter.referential_integrity.resolution_failure]])

Transitions

Properties

| index_failure_label_asserted | unit | [[linter.referential_integrity.index_failure]] | index_failure_raised() | error_label == "linter.referential_integrity.index_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002) | | resolution_failure_label_asserted | unit | [[linter.referential_integrity.resolution_failure]] | resolution_failure_raised() | error_label == "linter.referential_integrity.resolution_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002) |

Resolution algorithm

qualify(ref) (the ref_resolves expr) and spk graph share one algorithm, pinned by unit tests and documented here because it lives nowhere user-facing otherwise (gh#1: “the resolution algorithm is undocumented”):

1. Exact file id — the whole target names a file; file id wins over any split interpretation.
2. Bare-local row — a dotless target naming one of the SOURCE file’s own rows resolves to that row. In practice this arm is masked by the metasyntactic skip (a dotless target naming no file id is format prose, not a reference) — it is the safety net that keeps a dotless spelling meaningful when a file id shadows it. Revision 18 note: the old “only self-contained id: spec deltas reach this arm” reading retired with id: spec itself; every file resolves corpus-wide and authors spell rows file-qualified.
3. Every dot split, last to first — prefix must be a known file id and the remainder must be one of: a row of that file, the model.state/model.transition section anchor, or row.member where the row is the single segment right after the split and the member path may itself be dotted. Last-dot wins because dotted file ids (linter.frontmatter) are the common case; the first-dot fallback covers [[specodelic.model.state]] (file specodelic, anchor model.state) and multi-segment member paths ([[a.b.c.d]] = file a, row b, member c.d).

Row ids are single-segment: a dotted tail is always read as row.member, never as a dotted row id, so [[a.b.c.d]] does not resolve when file a declares only a row literally named b.c.

Notes

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).

Decision of record (2026-09-30, specodelic-cxq): this file’s rename_naturality law previously carried only identity + associativity; its naturality case (the cross-artifact commutation that gives the law its name, lookup_all(rename(I)) == rename(lookup_all(I))) was implicit in the Notes prose. It is now an explicit case column entry — the law the Notes describe as “the layer that enforces it” states all three cases [[specodelic.law_requires_cases]] requires.

rename_naturality is restated here rather than only living in specodelic.md, because this is the check that would actually break if a naive rename tool patched an id field without updating every [[ref]] pointing at it — the property belongs at the layer that enforces it, with specodelic.md keeping the higher-level restatement as its own traceability anchor. This is the same “same claim, two altitudes” pattern as ah reading dont’s events: one tool states the law, another is where violating it actually fails.

The open question this file’s Notes used to raise — that ref_kind_compatible assumes a fixed “which kind may fill which field” table that wasn’t specified anywhere — was resolved in specodelic.md Revision 2, which added the Reference Typing table for exactly this reason. What was never fixed, until this pass (specodelic.md Revision 6), is that this file’s own expr still named the three original fields by hand (traces_to/derives_from/guard) instead of pointing at that table generically — so it silently fell behind twice, first when supersedes was added (Revision 5) and again when emits was (Revision 6), despite specodelic.md’s own Revision 5 notes claiming this check needed zero code changes for either addition. That claim was true of the implementation (which already reads allowed_targets(field) from the table) but not of this file’s wording, which had drifted out of sync with what the implementation actually does. Reworded above to describe the table-driven behavior directly, so the next Reference Typing addition requires no follow-up here either in code or in wording.

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: duplicate_id_rejected

• WHEN spec_file_with(duplicate_row_id: true)
• THEN check(file) == failed
• VERIFIES [[linter.referential_integrity.duplicate_id_rejected]]

Scenario: cross_file_collision

• WHEN two_spec_files_sharing_id()
• THEN check(repo) == failed
• VERIFIES [[linter.referential_integrity.cross_file_collision]]

Scenario: dangling_ref_rejected

• WHEN spec_file_with(ref_to_nonexistent_id: true)
• THEN check(file) == failed
• VERIFIES [[linter.referential_integrity.dangling_ref_rejected]]

Scenario: wrong_target_kind

• WHEN guard_field_pointing_at_a_property_row()
• THEN check(file) == failed
• VERIFIES [[linter.referential_integrity.wrong_target_kind]]

Scenario: rename_naturality

• WHEN arbitrary_spec_repo(), arbitrary_id_rename()
• THEN identity: resolve(rename(I,a,a)) == resolve(I) associativity: resolve(rename(rename(I,a,b),b,c)) == resolve(rename(I,a,c)) naturality: lookup_all(rename(I)) == rename(lookup_all(I)) — every [[ref]] pointing at a renamed id is updated with it, the naturality case this checker is the enforcement layer for
• VERIFIES [[linter.referential_integrity.rename_naturality]]

Scenario: clean_repo_passes

• WHEN arbitrary_well_formed_repo()
• THEN check(repo) == passed
• VERIFIES [[linter.referential_integrity.clean_repo_passes]]

Scenario: index_failure_label_asserted

• WHEN index_failure_raised()
• THEN error_label == "linter.referential_integrity.index_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[linter.referential_integrity.index_failure_label_asserted]]

Scenario: resolution_failure_label_asserted

• WHEN resolution_failure_raised()
• THEN error_label == "linter.referential_integrity.resolution_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[linter.referential_integrity.resolution_failure_label_asserted]]