id: graph kind: intent checked_against_core: clear statement: βTHE graph tool SHALL derive, from every typed reference field in the repo, a single authoritative adjacency structure over π¦βs kinds, kept as a generated artifact that is never hand-edited, and SHALL answer transitive-closure (blast-radius) queries against it without re-walking markdown per query.β
Graph
Every checker in this repo (linter-referential_integrity.md,
linter-graph_shape.md, rename.md) already walks the reference edges
specodelic.mdβs Reference Typing table defines β but each does it
independently, on demand, by re-reading markdown. Nothing keeps a single
standing structure of βwhat points at whatβ that a tool could query
directly. This file specifies that structure: a derived artifact, not a
hand-authored one, so merge.mdβs conflict check and refactor.mdβs
fan-in signal can both query it instead of each re-deriving reachability
their own way β the same βone stated fact, not several hand-maintained
copiesβ discipline specodelic.md Revision 6 already applied to
append_only_variants, here applied to the graph itself rather than a
constraint.
Purpose
Every checker in this repo (linter-referential_integrity.md,
linter-graph_shape.md, rename.md) already walks the reference edges
specodelic.mdβs Reference Typing table defines β but each does it
independently, on demand, by re-reading markdown. Nothing keeps a single
standing structure of βwhat points at whatβ that a tool could query
directly. This file specifies that structure: a derived artifact, not a
hand-authored one, so merge.mdβs conflict check and refactor.mdβs
fan-in signal can both query it instead of each re-deriving reachability
their own way β the same βone stated fact, not several hand-maintained
copiesβ discipline specodelic.md Revision 6 already applied to
append_only_variants, here applied to the graph itself rather than a
constraint.
Constraints
| id | kind | expr | traces_to | satisfies |
|ββββββββββββ|ββββ|ββββββββββββββββββββββββββββββββββββββββββββββββββββββ|βββββββββββ|
| graph_is_derived_not_authored | invariant | every edge in the graph artifact is produced by extraction from repo files; the artifact contains no information a hand edit to it could add that isn't already present in some file's reference field | [[graph]] | |
| total_extraction | invariant | β reference field instance (traces_to/derives_from/guard/from/to/supersedes/emits/satisfies/observes) in any parsed file: exactly one corresponding edge exists in the graph β a guardβs conjunction of several [[id]] citations counts as one edge per citation, not one edge per transition; the enumeration restates the Reference Typing tableβs field set (the authority β satisfies joined it in Revision 7) and links in non-reference columns (expr, predicate, frontmatter) are total_refsβ beat, never edges | [[graph]] | |
| edge_kind_matches_typing | invariant | β edge (source, field, target): (source.kind, field, target.kind) β [[specodelic]]'s Reference Typing table β the graph never records an edge the typing table wouldn't allow, whether or not the underlying file is otherwise well-formed | [[graph]] | |
| deterministic_derivation | invariant | re-deriving the graph from an unchanged repo produces a byte-identical artifact | [[graph]] | |
| blast_radius_is_transitive_closure | invariant | blast_radius(id) == the forward and backward transitive closure of edges reachable from id, computed entirely within the derived artifact β never by re-walking source files | [[graph]] | |
| stale_graph_detected | invariant | β file whose on-disk content hash differs from the hash recorded at the artifact's last extraction βΉ the artifact reports itself stale rather than silently serving an outdated query result | [[graph]] | |
| external_boundary_derived | invariant | a file is classified as an external boundary iff it hosts β₯1 extension_point Constraint β the classification is a pure derivation over extracted structure, never an authored tag: removing the rows removes the classification, so a stale boundary tag cannot exist | [[graph]] | |
| extraction_failure | effect | graph.extraction_failure(detail) | [[graph]] | [[errors.envelope_error_kind]] β§ [[errors.exit_code_mapping]] β§ [[errors.remediation_hint_present]] |
Model
States
unindexedextractingindexedqueryablefailed(emits:[[graph.extraction_failure]])
Transitions
| id | from | to | guard |
|---|---|---|---|
| extract | unindexed | extracting | [[specodelic.parsed]] β every file in the repo has independently reached that state (see specodelic.mdβs own lifecycle) |
| extract_ok | extracting | indexed | [[graph.total_extraction]] β§ [[graph.edge_kind_matches_typing]] |
| extract_fail | extracting | failed | Β¬([[graph.total_extraction]] β§ [[graph.edge_kind_matches_typing]]) |
| publish | indexed | queryable | [[graph.deterministic_derivation]] β§ [[graph.graph_is_derived_not_authored]] |
| invalidate | queryable | unindexed | [[graph.stale_graph_detected]] |
Properties
| id | kind | derives_from | generator | predicate |
|---|---|---|---|---|
| every_edge_extracted | unit | [[graph.total_extraction]] | arbitrary_spec_repo() | count(edges(graph)) == count(reference_field_instances(repo)) |
| wrongly_typed_edge_rejected | unit | [[graph.edge_kind_matches_typing]] | hand_inserted_edge(source_kind: State, field: "guard", target_kind: Property) | check(artifact) == rejected β guard targets an invariant Constraint or a State (specodelic.md Revision 12); a Property target is still rejected |
| rerun_deterministic | unit | [[graph.deterministic_derivation]] | run_extraction_twice_against_unchanged_repo() | artifact(run_1) == artifact(run_2) |
| blast_radius_transitive | unit | [[graph.blast_radius_is_transitive_closure]] | chain(a traces_to b, b derives_from c) | c β blast_radius(a) β reachable through two hops, no direct edge required |
| blast_radius_bidirectional | unit | [[graph.blast_radius_is_transitive_closure]] | edge(a β b) | a β blast_radius(b) β§ b β blast_radius(a) β renaming a must be able to find dependent b, and vice versa |
| stale_detected_on_edit | unit | [[graph.stale_graph_detected]] | edit_one_reference_field_without_re_extracting() | check(artifact) == stale |
| hand_authored_edge_rejected | unit | [[graph.graph_is_derived_not_authored]] | graph_artifact_with_a_manually_inserted_edge_absent_from_any_file() | check(artifact) == rejected |
| boundary_tracks_extension_points | unit | [[graph.external_boundary_derived]] | file_hosting_extension_point_row_then_all_removed() | classified(file) == true before, == false after removal β no authored residue |
| observes_edge_extracted | unit | [[graph.total_extraction]] | constraint_row_carrying_observes_pointing_at_effect() | exactly one edge, kind constraints.observes β and zero edges when the column is absent |
| extraction_failure_label_asserted | unit | [[graph.extraction_failure]] | extraction_failure_raised() | error_label == "graph.extraction_failure" β renaming the label touches the error Constraint, this property, and its note together (EDGE-002) |
Notes
checked_against_core: clear (see AGENTS.mdβs convention). One resolved
ambiguity worth recording anyway: total_extraction counts each [[id]]
citation inside a conjunctive guard (A β§ B β§ C) as its own edge, not the
whole guard as one edge β otherwise blast_radius would under-count what a
transition actually depends on.
observes (specodelic.md Revision 9) joins total_extraction but no
cycle set. An observation claim is not a dependency: the acyclic
invariantβs edge set (linter-graph_shape.md) is a closed union that
observes deliberately does not join β satisfies and emits are
excluded by the same closure β so mutual cross-file observation is
well-formed. The external-boundary classification is the same
derived-not-authored discipline applied to visibility: a file is an
external boundary because it published a contract, and the fact
disappears when the publication does.
Scope boundary, Needs Human Review: this file does not replace
linter-referential_integrity.mdβs total_refs/unique_id or
linter-graph_shape.mdβs acyclic_traces/single_root_reachable β those
checkers still own those constraints. Whatβs genuinely open is whether
those two files should be refactored to query this artifact internally
rather than independently re-deriving reachability, now that a shared
artifact exists. Thatβs an efficiency and single-source-of-truth question,
not a correctness gap, so itβs flagged rather than forced β changing
either linter fileβs internal mechanism without changing what it checks
is exactly the kind of edit AGENTS.mdβs workflow should route through a
deliberate decision, not a side effect of adding this file.
Why extraction only requires parsed, not linted. Building the
adjacency structure needs a reference fieldβs syntactic presence, not its
resolution β a dangling [[typo_id]] still produces an edge (to a target
that doesnβt yet exist), which is precisely the shape total_refs needs
to check against. Requiring linted first would make the graph unable to
represent the very files whose brokenness the existing checkers need to
detect.
merge.md and refactor.md both depend on this file for blast-radius and
fan-in queries respectively, rather than each re-deriving reachability β
see each fileβs own Constraints for how.
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: every_edge_extracted
- WHEN
arbitrary_spec_repo() - THEN
count(edges(graph)) == count(reference_field_instances(repo)) - VERIFIES [[graph.every_edge_extracted]]
Scenario: wrongly_typed_edge_rejected
- WHEN
hand_inserted_edge(source_kind: State, field: "guard", target_kind: Property) - THEN
check(artifact) == rejectedβguardtargets an invariant Constraint or a State (specodelic.md Revision 12); a Property target is still rejected - VERIFIES [[graph.wrongly_typed_edge_rejected]]
Scenario: rerun_deterministic
- WHEN
run_extraction_twice_against_unchanged_repo() - THEN
artifact(run_1) == artifact(run_2) - VERIFIES [[graph.rerun_deterministic]]
Scenario: blast_radius_transitive
- WHEN
chain(a traces_to b, b derives_from c) - THEN
c β blast_radius(a)β reachable through two hops, no direct edge required - VERIFIES [[graph.blast_radius_transitive]]
Scenario: blast_radius_bidirectional
- WHEN
edge(a β b) - THEN
a β blast_radius(b) β§ b β blast_radius(a)β renamingamust be able to find dependentb, and vice versa - VERIFIES [[graph.blast_radius_bidirectional]]
Scenario: stale_detected_on_edit
- WHEN
edit_one_reference_field_without_re_extracting() - THEN
check(artifact) == stale - VERIFIES [[graph.stale_detected_on_edit]]
Scenario: hand_authored_edge_rejected
- WHEN
graph_artifact_with_a_manually_inserted_edge_absent_from_any_file() - THEN
check(artifact) == rejected - VERIFIES [[graph.hand_authored_edge_rejected]]
Scenario: boundary_tracks_extension_points
- WHEN
file_hosting_extension_point_row_then_all_removed() - THEN
classified(file) == true before, == false after removal β no authored residue - VERIFIES [[graph.boundary_tracks_extension_points]]
Scenario: observes_edge_extracted
- WHEN
constraint_row_carrying_observes_pointing_at_effect() - THEN
exactly one edge, kind constraints.observes β and zero edges when the column is absent - VERIFIES [[graph.observes_edge_extracted]]
Scenario: extraction_failure_label_asserted
- WHEN
extraction_failure_raised() - THEN
error_label == "graph.extraction_failure"β renaming the label touches the error Constraint, this property, and its note together (EDGE-002) - VERIFIES [[graph.extraction_failure_label_asserted]]