PROP-014 — specmap: bidirectional spec↔code traceability and the source metamodel
01Status. Design proposal v0.1 — not implementation-locked.
02Drafted for review; every decision below is open to challenge until ratified.
03Companions (vibevm-hosted, the pilot project's spec tree — cited as context, not shipped here):
- 04PROP-000 (foundation, license policy §3),
- PROP-003 (the LLM-boundary philosophy this PROP extends),
- PROP-009 (boot/loading model — specmap becomes its intra-project counterpart),
- PROP-013 (category C "drift" — specmap mechanizes its detection),
- Red Book ch. 2 (files as IPC) and ch. 3 (Sync-from-Code — specmap is its instrumentation).
05Home. flow:org.vibevm.ai-native/core-ai-native, spec/mechanisms/ — this mechanism ships with the Discipline (URIs spec://org.vibevm.ai-native/core-ai-native/mechanisms/PROP-014#…); its Rust implementation ships in stack:org.vibevm.ai-native/rust-ai-native-lang (specmap-core + the rust-ai-native-specmap binary).
06The tag syntax shown throughout (#[spec], scope!) is the Rust projection; other language stacks ship their own projection of the same model.
1. Problem statement
07vibevm is ~52K lines of Rust governed by ~20 PROP documents plus a 99KB owner-frozen spec.
08The linkage between the two layers exists today only as (a) prose cross-references in doc comments, (b) spec:// URIs cited in commit bodies per the Rule-2 discipline, and (c) the maintainer's head.
09AUDIT category C (drift) is detected by periodic human sweep.
10As the codebase grows, the question "which code realises this decision?" and its inverse "which decision justifies this code?" become unanswerable at acceptable cost.
11The desired end-state, by analogy with JS/TS source maps: from any compiled artefact you can reach the source; from any source you can reach the artefacts.
12One spec unit may touch many code items; one code item may serve many spec units.
13Many-to-many is undesirable but real; the system must represent it while linting against its growth. Half built: the representation ships and is exercised — the host index carries 912 edges over 898 code items, so many-to-many is real in practice, not just permitted. Nothing lints its growth: no edges-per-item or fan-out check exists in the specmap ratchet, in vibe check's roster, or anywhere else, so the fan-out can rise without a signal.
1.1 Where the source-map analogy holds, and where it breaks
14Source maps work because a compiler emits them as a free, deterministic byproduct of every build.
15Between a vibevm spec and its Rust realisation there is no compiler — there is a human or an LLM session.
16Consequences:
- 17The mapping cannot be generated; it can only be carried and verified. Until M1.5's
vibe buildexists, every edge is authored metadata. - Authored metadata rots unless three forces hold simultaneously:
- Edges travel with the artefacts. Code-side links live in the code (attributes on items) and survive any refactor that moves the item. Spec-side links live in the spec (stable anchors). External sidecar maps are rejected (§5.1).
- Invariants are machine-checked. Dangling references, uncovered requirements, orphan code, and — the load-bearing one — staleness: a spec unit carries a revision + content hash; when it changes, every edge pinned to the old revision flips to suspect until re-affirmed.
- The map is load-bearing in daily work. A map that is only audited dies (the classical requirements-traceability graveyard). specmap must feed (i) agent context paging — working on a REQ pulls its code, editing an item pulls its specs; (ii)
vibe explain; (iii) error provenance — failures cite the violated REQ. Two of the three feeds ship. (ii) is real, under the nametrace explainrather thanvibe explain(specmap/src/explain.rs:199,209, driven bycargo xtask trace explainandrust-ai-native trace explain). (iii) is real and enforced: the conform ruleserror-message-cites-reqanderror-enum-cites-reqrequire thespec://REQ URI in the Display text itself — "errors are agent food" — and host errors carry it, e.g.vibe-core/src/error.rs:34emits(violates spec://org.vibevm.core/vibevm/modules/vibe-registry/PROP-008#pkgref; …). (i) agent context paging has no implementation — nothing pulls code from a REQ or specs from an item. - M1.5 convergence. Once
vibe buildgenerates code from specs, the generator emits specmap edges as a true compiler byproduct — the analogy becomes literal. Hand-authored tags remain as the human-override lane. This PROP defines the format that the future generator will target.
1.2 The runtime vision (AI-native open source)
18For an open-source project, the metamodel (and, on demand, the source behind it) is exposed to consumers of the tool at runtime: an agent driving vibe can ask not just --help but "why does vibe install behave this way, under which decisions, realised where, with which known deviations" — and receive a structured subgraph or a rendered explanation. Specified, not built (→ B-018): there is no runtime channel. The subgraph and the prose render both exist (explain_json, explain_text) but are reachable only by running a CLI against a checkout — specmap_query / specmap_explain / specmap_source return no hit anywhere, and the MCP servers that would carry it do not offer it: core-ai-native-mcp is a transport that ships no tools at all (its echo is a #[cfg(test)] fixture, server.rs), and the host's vibe-mcp explain op is PROP-018's README relay, unrelated to this map. The stacks' trace_explain is the discipline's per-project channel over a checkout, not this metamodel. An agent driving vibe cannot ask the running tool anything.
19Distribution rides the existing registry: the metamodel index ships with the package; source fragments are fetched by content hash. Specified, not built (→ B-016): no package ships an index (no vibe.toml lists specmap.json in a payload), and there is no fetch-by-content-hash path — content_hash hashes, it does not retrieve.
20Closed-source projects ship a redacted profile (§2.8.3). Specified, not built (→ B-017): the profile has no manifest key, no parser and no redaction path. [metamodel] appears in no vibe.toml, conform.toml or specmap.toml in the repository, and no code reads an open/contract/none setting. Nothing is redacted because nothing is exposed at runtime to redact — this fact cannot land before #RUNTIME-EXPOSES-THE-METAMODEL-TO-CONSUMERS above it does.
2. Decisions
21Deliverable (в) of the design brief — the binding model — is this section in its entirety.
2.1 Addressing: spec-side
22req r1
23Decision. Extend the existing spec:// URI scheme into the canonical spec-side address:
24spec://<package>/<doc-path>#<anchor> — a spec unit
spec://<package>/<doc-path>#<anchor>~r<N> — a unit at revision N
- 25
<package>is today the repo name (vibevm); the grammar reserves group-qualification (spec://org.vibevm.world/wal/...) for cross-package tracing per PROP-008, deferred (§7.1). <anchor>is the explicit{#anchor}on a heading. Its grammar is[A-Za-z][A-Za-z0-9_-]*— one law, shared with fact ids (owner ruling 2026-07-26; it was kebab-only until then, on no recorded reason beyond «already used by every PROP heading»). Kebab remains the convention every existing anchor follows and the one to keep writing; the wider set exists so a heading anchor and a fact id can never be legal in one position and illegal in the other. Anchors are immutable once published and never reused. Renaming a unit keeps its anchor; retiring a unit tombstones the anchor (<!-- RETIRED: superseded by #new-anchor -->) rather than deleting it.- Anchors are case-SENSITIVE, at every level: what may be written, duplicate detection, and resolution.
##FOOand##fooare two units;spec://…#FOOresolves only toFOOand never tofoo. Considered and rejected (owner, 2026-07-26): folding case for duplicate detection. It would flag 29 published pairs across 12 documents — a section heading{#kebab-slug}beside that section's lead normative fact##KEBAB-SLUG, which is the convention the two id registers exist for. Byte-exact detection already catches every real duplicate, including{#FOO}written beside##FOO. Revisit when: a case-only collision is observed to mislead a reader in practice. - A spec unit is the span from an anchored heading (or an explicit
REQblock, §2.2) to the next same-or-higher heading / next unit marker; fact units (below) are the sub-heading grain. - Fact anchors (fact amendment, 2026-07-24 — owner-directed). A
##<ID>written as the first token of a paragraph or a list item (at any nesting depth, outside fenced/inline code) mints a fact unit — the finest addressable grain.<ID>follows[A-Za-z][A-Za-z0-9_-]*and carries two registers by convention:UPPER-SLUGnames a normative fact,kebab-casea service one (the grammar originates in the host's Progress Control amendment — the PROP-043 §3.8 twin of this clause). The unit's span is the carrying paragraph or item, continuation lines included; an anchored nested item is its own unit. Fact ids share one address space with heading anchors per document — the samespec://<package>/<doc-path>#<ID>form cites either, and a duplicate id (fact-vs-fact or fact-vs-heading) is an extraction warning, and it is byte-exact — case distinguishes two addresses, it does not merge them. Heading anchors were kebab-only when this clause was written; since the owner ruling of 2026-07-26 (§2.1) there is one grammar for both, so the register is convention rather than a boundary the parser enforces. Immutability and tombstoning bind fact anchors exactly as heading anchors. - Fact units carry no
kind:line (§2.2 typing stays a heading-unit discipline); their normativity signal is the id register. Edges cite them exactly as heading units (implements,verifies,documents), so code can bind to a single statement instead of a whole section. - Merge behaviour — the host spec-compiler contract (its PROP-035 §7.3 fact-inheritance clause, owner-ratified 2026-07-24) owns it: facts follow their section's fate under the contract↔source merge; a source fact redeclaring a contract fact's id is a per-fact override; the merged view re-gates id uniqueness as a build error. This PROP only cites that law — one source of truth.
2.2 Spec units, normativity, and the two-tier revision discipline
26req r1
27Decision. Four unit kinds, each with a different default edge semantics:
| Kind | Carries | Typical edges |
|---|---|---|
prop |
a decision + rationale ("why") | decides, referenced by REQs — Specified, not built: decides is not a verb this system can emit. The Verb enum in specmark-grammar is Implements · Verifies · Documents · Deviates · Informs, and its own doctest states the verb set is closed (Verb::parse("fulfills") == None); decides returns zero hits across every crate. The prop kind itself parses fine (mdspec.rs:78) — it is the edge verb that has no producer, so a decision can be a node and never the tail of the edge this cell names. @status:spec/done |
req |
a normative contract (RFC-2119 MUST/SHOULD/MAY) | implements, verifies |
design |
shape of a solution ("how", non-binding) | informs |
guide |
usage documentation | documents |
29A unit declares normativity with a one-line marker directly under its heading:
30### Conditional dependencies resolve to a fixed point {#req-conditional-fixpoint}
`req r2` — predicates are evaluated against resolved project state; each
pass MUST only add requirements (monotone), guaranteeing convergence.
31Revisions are two-tier:
- 32
r<N>is an author-asserted semantic revision. Bump it only when the meaning changes. Editorial edits (typos, wording) do not bump. - The indexer computes a content hash of the unit text. Hash changed while
rdid not →vibe tracewarns: "editorial-or-forgot-to-bump — confirm." This catches the human failure mode without making typo fixes expensive. (Prior art: OpenFastTrace's~revintegers; Doorstop's reviewed-hash stamps — ideas only, see §6.)
33Asymmetric invalidation rule (load-bearing).
- 34Spec unit
rbumps → every edge pinned to the oldrbecomes suspect; CI gate lists them; each is cleared by re-affirming (updating the pin) after review. - Code item changes → linked edges stay valid (the contract didn't move; implementation detail is free to change). Exception: edges of type
deviatesflip to review on either side changing, because a deviation is a statement about both sides. The rule holds, structurally and by accident; the exception does not.CodeItemin the committed index carriescrate_name,file,item_kind,line,symboland no content hash, so a code change is invisible to the edge and cannot invalidate it — the stated behaviour is what the data model can do rather than a decision it enforces. Nothing implements the exception:deviatesexists as aVerbvariant with a grammar-mandated reason, and no code on either side treats a deviates edge differently or flips anything to review.
2.3 Addressing: code-side — tags that travel
35req r1
36Decision. Code-side links are inert attributes provided by a tiny specmark crate (workspace-internal at first; publishable later).
37The attribute is a no-op for the compiler — its consumers are (a) the source scanner and (b) rustdoc, into which the macro injects a rendered "Spec:" line so the link is visible in generated docs.
38use specmark::spec;
/// Parses the `context(<key>)` predicate grammar.
#[spec(implements = "spec://org.vibevm.core/vibevm/modules/vibe-resolver/PROP-003#conditional-deps", r = 2)]
pub enum ConditionalPredicate { /* … */ }
#[spec(deviates = "spec://org.vibevm.core/vibevm/modules/vibe-resolver/PROP-003#conditional-deps", r = 2,
reason = "boolean composition (`and`/`or`/`not`) intentionally unimplemented; \
surfaces as PredicateError::Unsupported pending PROP-014-pilot decision")]
impl ConditionalPredicate {
pub fn parse(raw: &str) -> Result<Self, PredicateError> { /* … */ }
}
#[cfg(test)]
mod tests {
use specmark::verifies;
#[test]
#[verifies("spec://org.vibevm.core/vibevm/modules/vibe-resolver/PROP-003#conditional-deps", r = 2)]
fn fixed_point_is_monotone() { /* … */ }
}
39Grammar (one edge per attribute; attributes repeat for multiple edges):
40#[spec( <verb> = "<spec-uri>" [, r = <N>] [, reason = "<text>"] )]
#[verifies("<spec-uri>" [, r = <N>])] // sugar for tests
specmark::scope!("<spec-uri>" [, r = <N>]); // module-level inheritance marker
41Rules:
- 42Verbs:
implements,verifies,documents,deviates,informs.deviatesREQUIRESreason. implementsis a claim about code that RUNS, and a bare declaration does not carry one. A trait, an abstract signature or any other declared shape that no production code implements gets noimplementsedge, however faithfully it describes the requirement. The edge arrives with the implementation.- Why, and it is the whole value of the map: an edge from a declaration is indistinguishable in the index from an edge from working code, so a reader asking «what implements this REQ» is told a shape and hears a build. The perverse gradient is the point — the more carefully a project declares its shapes ahead of time, the more false coverage it accumulates, which punishes exactly the discipline this model exists to reward. Measured instance, 2026-08-05:
vibe_settings::events::Watchercarried the edge with zero implementors in the tree, andvibe explainreported two. - Dropping the edge does not hide the declaration, which is the objection to expect: the module's
specmark::scope!still covers the item for the orphan gate (##RULE-SCOPE-INHERITANCE), the requirement keeps whatever honest edges it has from real code, and the docblock is where «this is promised here» belongs. So the choice is not between a false edge and silence — it is between a false edge and an accurate absence. - Unit of code = the item (fn, struct, enum, trait, impl block, mod). Never lines, never expressions. Line/column spans appear only in the derived index (§2.5), where volatility is harmless because the index is regenerated.
- Scope inheritance.
specmark::scope!(…)at the top of a module gives every item inside a defaultimplementsedge unless the item carries its own#[spec](own tags replace the inherited set in v0.1; merge syntax is an open question, §7.2). Private helpers therefore usually need no annotation. Rust note: a true inner attribute (#![spec(…)]) on modules is unstable for proc-macros, hence the macro-invocation form. - Generated code (e.g.
vibe-wire/src/generated/) is excluded from orphan checks via a directory marker; the generator input (JTD schema file) is the taggable unit instead. BUILT 2026-08-05 — both halves are now real. The exclusion half always was:rscanandratchetskip a path containing/generated/. The designation half was a decision nobody could act on, because no scanner opened a.jsonat all and the edge model hangs an address off a code SYMBOL, which a JSON document has no obvious equivalent of. Both are answered: a schema's units are its ROOT and eachdefinitionsentry (symbol=<stem>and<stem>::<def>,item_kind=schema/schema-def), and the tag lives in JTD's ownmetadata.specblock as a verb → URI map. The scanner is opt-in per project throughschema_roots, empty by default. Measured on the host that raised this: seven wire contracts tagged, 16 units and 7 edges in the map, andvibe explainnow answers «what implements PROP-000 §16» with all seven, by file and line. - Error enums are contract. Every public error variant whose meaning comes from a REQ carries
implementson the variant's enum (or#[spec]on the variant where precision pays). This is what lets a failing command cite the violated requirement (§2.6). - Multiplicity lint. An item carrying more than 3 spec edges is flagged by
vibe check: either the item does too much or the spec units are cut too fine. (Threshold configurable; mirrors the activation-conflict lint philosophy of PROP-003 §2.10.) Specified, not built (→ B-021): no checker in any layer counts edges per item;vibe check's checks do not include a multiplicity lint.
2.4 The edge model
43req r1
44A typed, directed property multigraph:
- 45Nodes:
SpecUnit { uri, kind, r, content_hash },CodeItem { symbol, item_kind, crate_name, file, line }, plus derivedCommand,ErrorVariantviews. Specified, not built (→ B-019):CodeItemcarries no content hash (see §2.2's own note), and there are no derivedCommandorErrorVariantnode views. (ErrorVariantexists as a conform fact —conform/src/facts.rs:66— which is a different graph.) - Edges:
(CodeItem) --implements/verifies/documents/deviates/informs--> (SpecUnit @ r), each with provenance (authored|generated|proposed) and, fordeviates, the mandatory reason. (Brownfield amendment:) spec units additionally carry a lifecycle status (planned|disputed;ratifiedis the absent default,retireda tombstone), and adisputedunit names the other anchor of its pair in adisputesfield. Specified, not built: the pairing is a unit field and not yet a spec↔specconflicts_withedge; edges intodisputedunits are not frozen — suspect detection reads only the pinned revision (index.rs:118-131); and no coverage math over spec units exists, soplannedscope is neither reported separately nor penalized. - Direction of authority: spec → code (the Red Book's top-down flow). The reverse direction is computed (the index inverts edges) plus one social channel: a
proposededge pool (§4, Phase 2) feeding the Sync-from-Code protocol when code grows meaning the spec lacks.
2.5 The index: specmap.json
46req r1
47Decision. A derived, deterministic, committed artefact, regenerated by cargo xtask specmap and gated by cargo xtask specmap --check in CI — the exact idiom check-codegen already established.
- 48Built by a source scanner (syn or tree-sitter over the workspace; markdown parser over
spec/**). No macro expansion needed —#[spec]is read as text/AST, which also makes the JS/Python bindings (§2.9) uniform. - Canonical JSON (stable ordering), schema under
schemas/specmap.jtd.json→vibe-wiretypes via the existing codegen pipeline. - Contents: all nodes (with content hashes and current file:line spans), all edges, plus computed tables: coverage per REQ (
{implemented, verified, documented}bits), orphans (public items with no edge own-or-inherited), suspects (edges whose pinnedr< unit's currentr), unbumped-hash warnings. Re-measured 2026-08-05, and one third of this note had gone stale. The host's committed index has exactly six keys —code_items,edges,schema,spec_units,suspects,warnings— so nodes, edges, suspects and the warnings table are real (5 652 spec units, 915 code items, 932 edges, 205 warnings; the earlier reading of 5 266 / 898 / 912 / 265 was a different tree). Coverage per REQ is still absent and the orphans table is still absent — orphan coverage is computed at gate time by the ratchet and deliberately never serialised (ratchet.rs,index.rs). What is no longer true is the content hash:code_itemnow carriesfingerprint, atok1:<sha256>over the element's TOKEN STREAM (doc comments count as code, ordinary comments and whitespace do not), and it stands on 915 of 915 items — so the map is no longer blind to a change in the code under a link, and a formatter run does not move it. - Determinism is a tested property, same as the resolver's (PROP-003 §3.3): index twice, assert byte-identical.
2.6 Query surface
49req r1
50vibe trace coverage [--crate X] [--kind req] # matrix: REQ × {impl, test, doc}
vibe trace impact <spec-uri> # all items/tests reachable from a unit
vibe trace orphans [--ratchet-file …] # unjustified public items
vibe trace stale # suspect edges + unbumped-hash warnings
vibe explain <command|symbol|spec-uri> [--json|--text|--prose]
- 51
--jsonemits the raw subgraph (agent-friendly);--texta deterministic structured rendering;--prosean LLM rendering of the same subgraph. The tool MUST be fully useful without an LLM —--proseis a presentation layer, never the data layer. - Error provenance:
vibe's error rendering looks up the failing error variant in the index and appendsviolates spec://…#req-… (r2) — run: vibe explain <uri>. This is the single highest-leverage consumer: every failure becomes a doorway into the metamodel. Specified, not built as an index lookup (→ B-019/B-018): error renderings citeviolates spec://…from compile-time constants —core-ai-native-mcp/src/error.rs:25,:37,:48, pinned by a doctest, and conform'sreq_message(rules/mod.rs:49) — with no revision and norun: vibe explainhint. The doorway is real; the lookup is not. - During the pilot these live behind
cargo xtask trace …to avoid touching the CLI surface prematurely; promotion tovibe trace/vibe explainis a Phase 4 decision (§4).
2.7 The LLM boundary
52Continuation of PROP-003 §2.5.3's philosophy — the LLM emits facts and renderings; deterministic machinery decides:
- 53LLM as proposer. Link mining (Phase 2) produces edges with provenance
proposed, stored inspecmap-proposals.json, never in code. A human (or an explicitly delegated agent session) affirms a proposal by writing the actual#[spec]attribute — the affirmation IS the code change, reviewed like any diff. - LLM as renderer.
vibe explain --prosefeeds the subgraph (spec unit texts + rustdoc of linked items + deviation reasons) to the provider behindvibe-llm. The subgraph is the ground truth; the prose cites URIs; hallucination risk is bounded by retrieval, and the--jsonform is always available for verification. Specified, not built (→ B-020): the prose producer is a deterministic template (ledger.rs:168) and the crate's own header says an LLM producer slots in later. - LLM never silently writes edges, bumps revisions, or clears suspects. Those are state transitions with audit cost; they pass through diffs.
2.8 Runtime exposure — the AI-native OSS channel
- 54Transport. Each stack's discipline MCP server (
rust-ai-native-mcp,typescript-ai-native-mcp,go-ai-native-mcp, all built on this package'score-ai-native-mcp) exposestrace_explain(target, {json|prose})— the subgraph and the prose render — alongsidespecmap_checkandspecmap_write. An agent that drives the stack CLI gets the same via<lang>-ai-native trace <target> --json. Specified, not built (→ B-018): there is nospecmap_source(content_hash) -> fragmenttool and no generalspecmap_query. - Distribution. The index ships inside the published package (it is small); source fragments resolve by content hash against the package's git registry — the content-addressed identity from PROP-002 already guarantees fetch integrity. Specified, not built (→ B-016): no published package ships an index. No
vibe.tomlin the repository listsspecmap.jsonin its payload, and the onlyspecmap.jsonfiles underpackages/arego-extract/ts-extracttest fixtures plus one project's own working index. Content-hash fragment resolution does not exist either —content_hashcomputes hashes for the ledger's cache keys, and nothing resolves a source fragment by one. PROP-002's fetch integrity is real and is not this. - Profiles.
open(full graph + source),contract(spec units + signatures of items, no bodies — the closed-source tier),none. Declared invibe.toml[metamodel] profile = "open". Specified, not built (→ B-017):[metamodel]is in no manifest, no schema and no parser; the three profile values have no representation. - Security (non-optional). The exposed content is instructions-shaped prose delivered into a consuming agent's context — a prompt-injection distribution channel by construction. Therefore: (a) the shipped index and fragments are signed; consumers verify before use (scheme TBD, §7.6 — sigstore-class is the default candidate); (b) the MCP tool descriptions explicitly frame returned content as reference data, not instructions; (c)
vibe checklints spec units for imperative second-person phrasing outsideguidekind. This PROP takes the position that the trust layer ships with the runtime channel, not after it. Specified, not built — all three clauses. (a) Nothing is signed: no signing or verification path exists invibe-publish,vibe-registryor any engine crate, and this document's own#OPEN-SIGNING-SCHEMEstill calls the scheme undecided and blocking. (b) No MCP tool description carries that framing; the phrase appears nowhere. (c)vibe check's roster has no imperative-phrasing or second-person lint. The position the sentence takes is the right one, and it is why the marker moves rather than the text: the trust layer has not shipped, and by this PROP's own standard the runtime channel must not ship until it does — which is consistent with#RUNTIME-EXPOSES-THE-METAMODEL-TO-CONSUMERSbeing unbuilt too.
2.9 Language neutrality
55The grammar (URIs, verbs, r, reasons) is language-neutral; only the carrier syntax is per-language.
56The spec side is one shared engine (core-ai-native-specmap), so fact-unit extraction (§2.1) reaches every language family — rust, typescript, go — identically through the vendored engine; adding a language never re-implements the spec scanner.
57Rust ships first.
58Sketches, normative later:
- 59JavaScript/TypeScript: JSDoc carrier —
/** @spec implements spec://… r2 */on declarations; scanner = tree-sitter. - Python: decorator
@spec(implements="spec://…", r=2)from aspecmarkpackage; module-level__specmap_scope__ = "spec://…"(NB: not__spec__, which importlib owns).
3. Principles
3.1 (а) Writing specifications
- 60Every normative statement is addressable. It lives in a unit with a stable
{#anchor}; anchors are immutable and never reused; retirement is a tombstone, not a deletion. - One unit, one decision. If a unit needs "and also", it is two units. The unit is the page of the context-memory hierarchy: it must make sense alone when paged into an agent's window.
- Normativity is marked, not implied. RFC-2119 verbs inside
requnits; everything else isproprationale,design, orguide. A reader (human or model) must never guess whether a sentence binds. - Norm and rationale are separated. The MUST changes rarely and bumps
r; the "why" evolves freely without invalidating implementations. PROPs hold rationale; REQs hold contract. - Semantic edits bump
r; editorial edits don't; the hash audits the difference. Forgetting to bump is detected, not punished. - Spec states what and why — never restates how. Implementation detail belongs in rustdoc next to the code (where it cannot drift from the code); the metamodel joins the two layers at query time. A spec that mirrors code is shadow code and drift fuel.
- Write testably. A
reqshould imply its verification; if you cannot imagine the#[verifies]test, it isdesign, notreq. - Deviations are first-class and honest. When reality intentionally differs, the code says
deviates+ reason — the generalisation of the existing<!-- REVIEW: … -->discipline. An undocumented deviation found by audit is a defect. - Cross-reference by URI only. No "see above", no relative prose pointers — they don't survive paging or reorganisation.
- Units fit a page. Soft target ≤ 120 lines per unit;
vibe checkwarns beyond. Long units page badly and hash-churn often. Specified, not built (→ B-021): no checker warns on spec-unit length; the 120-line figure is a target with no enforcement.
3.2 (б) Writing Rust under specmap
61Deliberately not a general style guide — only what traceability and the metamodel require. House rules (clippy
-D warnings,forbid(unsafe_code), etc.) stay where they are.
- 62The item is the unit of meaning. Shape code so each public item serves few spec units (≤ 3 edges; lint beyond). If an item needs more, split the item or merge the units.
- Tags travel with code.
#[spec]on items;scope!per module for inheritance; private helpers inherit silently. Moving a function moves its link; that is the entire point. - Typed verbs, no bare links.
implements≠documents≠deviates; the verb is what makes the graph queryable. - Tests declare what they verify.
#[verifies(uri, r)]on the test, not a comment. Coverage = REQ × {impl, test} computed, not estimated. - Rustdoc is the detail layer. Every tagged public item's doc comment states the practically important behaviour — errors, edge cases, performance traps.
vibe explaincomposes spec (contract) + rustdoc (detail); neither duplicates the other. Specified, not built (→ B-020):explaincannot compose rustdoc —CodeItemcarries no doc field and the renderer emits symbol, kind, crate, file, line and edges only. - No orphan public API. Every
pubitem is reachable from an edge, own or inherited. Ratcheted: warn → error per crate as migration lands (§4). - Generated code is excluded; its generator input is tagged. Schema files and macro definitions carry the edges; expansion output is marked generated.
- Errors are contract surface. Public error types/variants that signal a requirement carry its edge, enabling error-message provenance. An error no spec explains is an undocumented behaviour.
3.3 (в) Binding principles
63Section 2 is deliverable (в).
64For reading convenience, the five load-bearing invariants:
- 65edges travel with artefacts (§2.3);
- two-tier revisions with asymmetric invalidation (§2.2);
- derived deterministic committed index with a CI gate (§2.5);
- the tool is fully functional without an LLM, and the LLM only proposes and renders (§2.6–2.7);
- the runtime channel ships signed or not at all (§2.8.4).
4. (г) Migration playbook — transforming vibevm with Claude Code
66Strategy: easy wins first, ratchet always, never gate the whole repo on day one.
67(The maximum-perfection horizon — full backfill of all 12 crates, JS/Py bindings, signed runtime channel — is Phase 5+, listed for honesty, not for scheduling.)
Phase 0 — tooling skeleton (≈ half a day)
- 68
crates/specmark/: the no-op attribute +scope!+verifiesmacros (syn parse of the grammar, rustdoc line injection, zero runtime cost). xtask specmapsubcommand: markdown unit parser + syn-based item scanner + canonical JSON emitter;--checkmode (regenerate-and-diff, thecheck-codegenidiom).schemas/specmap.jtd.json+ codegen.- Acceptance: index builds deterministically twice on the untouched repo (zero edges, full node inventory); CI job wired but non-blocking.
Phase 1 — pilot: PROP-003 §2.6.1 × vibe-resolver/src/conditional.rs
69The smallest real loop, chosen deliberately: fresh spec, ~130-line module, and it carries a live design question (the not/monotonicity issue) that becomes the first officially traceable REQ with a recorded deviates.
- 70Unit-ify §2.6.1: add
reqmarkers + anchors for (i) the fixed-point/monotonicity contract, (ii) the predicate grammar, (iii) the host-invariance rule. Anchors added, no prose rewritten — additions only, owner-frozen text untouched pending sign-off. - Tag
conditional.rs:implementson the enum andparse,deviates(+ reason) for unimplemented boolean composition,verifieson its tests. - Drift drill (the acceptance that matters): semantically edit the fixed-point unit, bump
r→ gate flags the suspect edges; re-affirm → gate clears. Then edit a typo without bumping → hash warning fires. Both behaviours demonstrated in one PR description. xtask trace explain conditional::ConditionalPredicate::parse --textemits a correct subgraph.
Phase 2 — backfill vibe-resolver with Claude Code
71Two link sources, both flowing through the proposed pool (§2.7), affirmed by diff review:
72(a) Latent corpus mining — the repo already cites spec:// in commit bodies (Rule 2):
73git log --all --pretty='%H %s' --grep='spec://' | …
74Each (commit → files touched → URIs cited) triple seeds proposed edges with evidence pointers.
75(b) Crate sweep. Claude Code prompt (guardrails included):
76Read vibevm/vibespecs/modules/vibe-resolver/*.md and crates/vibe-resolver/src/.
For every public item, propose at most 3 specmap edges using the
PROP-014 §2.3 grammar. For each proposal output: item path, verb,
spec URI + r, a one-line evidence quote from BOTH sides, and a
confidence (high/medium/low). Do NOT edit any file. Do NOT propose
edges where you cannot quote evidence from the spec side — mark the
item "candidate orphan" instead. Emit specmap-proposals.json only.
77Affirmation session prompt:
78Take specmap-proposals.json entries marked APPROVED in the review
file. Write the corresponding #[spec]/#[verifies]/scope! annotations.
One commit per module, Conventional Commits, body citing the spec://
URIs added. Run `cargo xtask specmap --check` and `cargo test -p
vibe-resolver` before each commit. Touch nothing outside
crates/vibe-resolver and the proposals file.
- 79Acceptance:
vibe-resolvercoverage report ≥ 90% ofrequnits implemented-and-verified; orphan list for the crate empty or dispositioned in AUDIT; gate flipped to blocking for this crate only (the ratchet file lists exempt crates).
Phase 3 — expansion + metrics
- 80Crate-by-crate (suggested order:
vibe-core→vibe-install→vibe-registry→ CLI last), each flipping its ratchet entry. - Instrument the economics — the empirical answer to "will this rot": stale-edge half-life after a normal refactor week; proposals-to-affirmation lag; % of PRs touching tagged items that also touch their pins. Targets set after two weeks of data, recorded in AUDIT.
Phase 4 — surfaces
- 81Promote
xtask trace/explain→vibe trace/vibe explain(--json/--text/--prose). - Error provenance wiring in
vibe-clierror rendering. vibe-mcptools per §2.8 — blocked on the signing decision (§7.6); ships signed or not at all.
5. Rejected alternatives
- 82External sidecar map only (a
specmap.tomlmaintained by hand or by tool, no in-source tags). Rots immediately: without a compiler regenerating it, every refactor silently invalidates spans and symbol paths. Kept only as the derived index (§2.5), where regeneration is the lifecycle. - Line/range anchors ("PROP-003 lines 410–462",
src/naive.rs:118-160). Maximally precise and maximally fragile; every upstream edit shifts them. Spans are demoted to derived-index decoration. - Embedding-similarity recovered links as ground truth. Non-deterministic core, unexplainable diffs, silent drift. Allowed exactly once in the lifecycle: as a proposer in Phase 2, behind human affirmation.
- Literate programming / tangle (spec is the single source; code is extracted). Inverts authority correctly but destroys the entire Rust toolchain experience (rust-analyzer, incremental compile, grep-ability) and forces the spec to carry how. The Red Book's layer model (spec=meaning, code=detail) is the opposite bet, deliberately.
- External requirements database (DOORS/Doorstop-style items outside the repo). Violates "project facts live in the repo" (CLAUDE.md memory discipline) and splits the review surface. Everything here is files in git — the book's ch. 2 thesis.
- Full formal specification (TLA+/Kani/Dafny for the contracts). Wrong genre for prose contracts and process disciplines; complementary for isolated algorithmic kernels — the conditional-deps fixed point is a natural first candidate if we ever want a machine-checked model, and the specmap edge type for it would be
verifies.
6. Prior art and license posture
83Conventions and ideas are free; code is not.
84Per PROP-000 §3 (permissive only; GPL/AGPL/LGPL forbidden as dependencies), roles below are explicit.
85License fields to be re-verified before any code-level reuse.
| System | License (verify) | Role here |
|---|---|---|
| OpenFastTrace | GPL-3.0 | Study only. Borrowed ideas: artifact-type chains (req→dsn→impl→utest), ~rev semantics, coverage states. No code, no linkage. |
| strictdoc | Apache-2.0 | Friendly. Grammar/UI patterns for requirement documents. |
| Doorstop | LGPL-3.0 | Wrapper-zone per policy if ever executed; borrowed idea: reviewed-hash stamps (our two-tier revisions). |
| Sphinx-needs | MIT | Friendly. Typed needs/links, filter queries. |
| DO-178C / DOORS culture | n/a (standards) | The cautionary tale §1.1 is built on: traceability that is audited but not load-bearing dies. |
| JS source maps / DWARF | n/a | The analogy and its precise failure point (§1.1). |
syn / tree-sitter (syn is the live scanner dependency — Cargo.toml:44; tree-sitter is in no manifest in this repository.) |
MIT/Apache-2.0; MIT | Implementation dependencies for the scanner. |
| sigstore | Apache-2.0 | Default candidate for §2.8.4 signing. |
87Differentiators vs. classical requirements traceability:
- 88(i) the map is consumed at runtime by agents using the tool, not only at audit time;
- (ii) an LLM participates — strictly as proposer and renderer behind a deterministic core;
- (iii) the map doubles as the context-paging table for agent sessions (PROP-009's intra-project counterpart);
- (iv) specs are package-distributed artefacts (vibevm itself), so tracing composes across the registry.
7. Open questions
- 89Cross-package URIs. Group-qualified
spec://org.vibevm.world/wal/...grammar and resolution against installed packages — after PROP-008 settles live. - Inheritance merge. v0.1: item tags replace
scope!defaults. Is a+implementsextend form needed? Decide on Phase 2 evidence. - Unit moves across documents. Anchor immutability covers renames-in-place; moving a unit between files needs either URI redirect stubs (PROP-012 flavour) or doc-path-free unit IDs. Lean: redirect stubs.
- Explanation caching.
--proserenderings keyed by (subgraph hash, model id) — where cached, when invalidated. - Thresholds. 3 edges/item, 120 lines/unit — placeholders until Phase 3 metrics.
- Signing scheme. sigstore vs. minisign-class vs. registry-native git signatures; decide before Phase 4's MCP exposure; blocking for §2.8.
- Non-OSS
contractprofile. Exactly which item metadata (signatures? doc comments?) is safe to ship; needs a real closed-source consumer to decide. - Commit-message integration. Rule 2 already cites
spec://; should commits citing a REQ auto-link into the index asinformsprovenance? Cheap, probably yes; confirm noise level on Phase 2 history.
90This PROP is a design proposal.
91Ratification — and the specmark/xtask implementation start — happens through PR review against this document.
92Any mechanism specified here that is not exercised by the end of Phase 2 is either removed from the spec or annotated in place as specified, not built — never carried as unmarked aspiration.