Every tracked invocation has a balanced lifecycle span. The span begins before memo lookup, including already-current reuse, and ends on execution, validation, reuse, cancellation, or unwinding.

Read in specification context

Navigation uses backend-authored canonical ownership paths. Local and external semantic references carry opaque canonical paths distinct from labels. Paths whose ownership segments are all named survive unrelated/detail edits, sibling movement, and host reconstruction; rename, move, deletion, or a forged path fails explicitly.

Paths containing anonymous ownership segments are best-effort navigation identities, not persistent identities across edits or host reconstruction. Changing or deleting an anonymous entity can invalidate its link or cause it to select another indistinguishable occurrence. The same limitation applies to links to its descendants. Within the current host and source revision, paths still distinguish represented entities, and nonexistent paths fail explicitly. This qualification concerns inspector navigation only; import routes to the same definition do not give that definition different semantic identities. Anonymous import identity derives from its import paths and binding kinds, excluding source positions and database-local handles.

Read in specification context

Representation growth flows through the derive. Product producers do not hand-serialize Sage CST, type, signature, or Typed-IR structures. Adding an ordinary field or variant changes reflected output through the Reflect implementation unless an explicit semantic override is documented.

Read in specification context

Local search starts from one complete detail-free index. The browser filters the returned local directory without sending search text or fetching branches. Dependency symbols are excluded. Index construction may use external facts needed for macro expansion, but no broader semantic metadata or item details.

Read in specification context

Checked trace assertions use a deterministic projection. Dynamic parentage and dispositions are retained; only explicitly unordered siblings are canonically sorted. Tests assert closed sets or extensible required/forbidden patterns and do not assign semantic meaning to scheduler order or raw Salsa IDs.

Read in specification context

The URL stores durable intent, not response state. Selection, product, search, grown panel, and revision views update browser history. A revision mismatch discards every response-derived value, fetches the current directory, and replays the URL’s canonical symbol/product intent. Each event stream connection checks the current revision, closing any notification gap while the browser was disconnected.

Read in specification context

The browser is a generic protocol interpreter. Symbol presentation, positive product descriptors, render nodes, value nodes, and trace nodes determine the UI; JavaScript does not branch on Sage symbol kinds or known product IDs.

Read in specification context

Product reflection is faithful, bounded, and owned. Ordinary structure is derived, semantic leaves are explicit, storage handles expose their values inline, actual recursive reentry is explicit, and limits yield immutable continuations which require no later database borrow.

Read in specification context

Product availability is positive and non-eager. Selecting a symbol returns opaque product IDs, labels, and URLs without requesting any advertised product. Local and external symbols use the same mechanism; unsupported products are absent.

Read in specification context

Input revisions and demanded work are separate facts. Revision advancement records exact changed inputs even when no inspection follows; retained runs record only actual demand. A workspace reconstruction is distinct from a fine-grained source-input revision.

Read in specification context

Semantic work ends before serialization and browser rendering. Every tracked read used to reflect a product lies inside the recorded analysis/reflection boundary; view assembly is explicit and later JSON/DOM work has no database access.

Read in specification context

Inspector integration evidence starts from Rust source. A checked-in Cargo sample project enters through the production workspace host, live inspection provider, actor, and Axum server. Reviewed snapshots record returned values and demand; precomputed JSON and scripted semantic providers never supply results to an integration test. This is the Inspector-local consequence of Semantic evidence starts from source.

Read in specification context

The typed inspection service is below transport. Service request and result types do not depend on Axum, React, terminal state, LSP, or the Oracle schema. HTTP handlers only decode, call InspectionClient, and encode.

Read in specification context

Unknown work is visible rather than omitted. Supported Sage and metadata operations use stable operation families; any query without a semantic-key projection is retained as unmapped with its raw diagnostic ingredient. A checked closed dependency claim fails in the presence of an unexpected fallback.

Read in specification context

One actor owns one coherent live workspace. Axum and the file watcher communicate through a bounded typed client; only the actor owns and mutates the host. Source edit batches are applied serially to the retained database, while configuration changes reconstruct it at an explicit reload boundary.

Read in specification context

A completed body is an elaborated semantic tree. Successful output contains final types and semantic identities and materializes all type-directed operations used by the source. Method syntax, unresolved names, inference variables, pending obligations, and adjustment recipes do not survive in CheckedBody; Completed bodies are elaborated typed trees owns the cross-cutting representation decision.

Read in specification context

Expected types flow into expression checking without selecting semantic candidates. A caller supplies an available expected type before checking the expression beneath that boundary. Expression forms may use it to guide local inference and explicit coercion, but trait proof, method provider discovery, and alias normalization retain their independent candidate-selection rules.

Read in specification context

Body checking depends on interfaces, never other bodies. The body query reads only its own CST and signature plus the name-resolution, interface, metadata, candidate, and solver facts demanded by that body. A call may read its callee’s signature but cannot read the callee body. This is the body-phase consequence of Cross-item dependencies stop at semantic interfaces.

Read in specification context

Speculation is isolated and completion is quiescent. Candidate matching and other speculative relations occur in child inference versions; failure discards their equalities, wakeups, and staged obligations, while a successful operation commits them atomically. The public result is frozen only after fallback and terminal obligation processing leave no live work. Versioned egraph children are inference transactions defines the shared transaction rules.

Read in specification context

Overloadable operators remain resolved calls in Typed IR. Every non-short-circuit binary operator retains its trait operation and method result through inference; its token alone neither narrows nor equates operand types. Every proven operation completes as a resolved trait-method call, including primitive and generic cases. Ambiguity and unsupported operands cannot be represented as success, and primitive specialization occurs only at the future codegen boundary defined by the operator representation decision.

Read in specification context

Semantic identities have exactly one minting boundary. An owning query creates each generic parameter or associated-item symbol once. Every dependent query reopens or references that identity instead of reconstructing it from its name or source position. The identity family is defined by Symbols form the uniform semantic identity family.

Read in specification context

Checked products own their semantic storage. CST is immutable input; each checked signature or body allocates into a fresh output stash and returns a self-contained Stashed<T>. Its deterministic content fingerprint, rather than allocation address or source-tree lifetime, is the value used for backdating. Stash for type-level interning owns this representation choice.

Read in specification context

A checked signature is the body-independent cross-item interface. Consumers obtain the types, generic binder, and parameter environment needed to use a definition without checking that definition’s body. No signature query reads any function body. This is the signature-phase consequence of Cross-item dependencies stop at semantic interfaces.

Read in specification context

Interface detail is split at semantic reuse boundaries. Fields and associated-item enumeration remain independently keyed from the owner signature, and selecting one associated item reads only that item’s signature. Enumeration never checks sibling signatures or bodies eagerly.

Read in specification context

Generic identities are minted once by their owner and reused. An owner signature creates its parameters under one binder. Associated-item, field, and body queries reopen that binder and add only genuinely new item-level parameters; they never reconstruct an existing GenericParam or owner Self identity.

Read in specification context

Checked interfaces are self-contained semantic values. Signature lowering reads CST from one stash and writes all checked types, binders, predicates, and retained alias applications into a separate result stash. No checked value points into tree-sitter state or the source CST stash. This is the signature-level ownership boundary established by Stash for type-level interning.

Read in specification context

Public checking queries are symbol-keyed semantic boundaries. A caller supplies the definition symbol and the query derives scope and environment from it. Signatures are the primary cross-item interface; field, member, and other language-required interfaces may be separate narrow products. Bodies and checking temporaries are not interfaces. This is the shared query design required by Cross-item dependencies stop at semantic interfaces.

Read in specification context

A language restriction is explicit at its semantic boundary. An intentionally unsupported Rust construct states what is excluded, why Sage excludes it, its user-visible impact, and the response at the responsible phase. That response is normally a diagnostic or conservative incomplete result; any temporary semantic approximation, such as Lifetime::Dummy, is identified explicitly as a soundness exception rather than silently presented as full Rust semantics.

Read in specification context

Semantic identity precedes semantic detail. A definition’s semantic identity is created and retained independently from its signature, members, fields, body, and other lazily computed facts. Symbol-bearing item definitions use their symbol; generic parameters, fields, and locals use their appropriate scoped identity family. Downstream semantic values refer to that identity rather than reconstructing it from those details. This is the pipeline-wide consequence of Symbols form the uniform semantic identity family.

Read in specification context

Incremental guarantees are verified as executions and semantic reads, not timings. Evidence distinguishes a tracked function body which executed from a memoized request and records owned external-metadata reads separately. Independent scheduling order and elapsed time are excluded unless a specific ordering or count is itself the invariant.

Read in specification context

Demand follows the narrowest semantic boundary. Asking for one semantic product requests only the interfaces and metadata needed for that product. In particular, checking a caller may read a callee signature but never the callee body. This is the pipeline-wide consequence of Cross-item dependencies stop at semantic interfaces.

Read in specification context

Reexecution and downstream invalidation are distinct. A coarse input change may cause a cheap producer or keyed lookup to execute again. When its semantic result is equal, backdating must stop the change before expensive consumers; the architecture does not claim that every unrelated edit prevents all upstream execution.

Read in specification context

Unrepresented source never becomes negative evidence. Published symbols from an incomplete phase may support their own positive facts, but omitted or unsupported source cannot justify a false proof, failed lookup, or exhaustive ground No in a downstream consumer.

Read in specification context

Deliberate restrictions define Sage’s supported language contract and explain its limits. Temporary implementation gaps in otherwise supported Rust appear as TODO entries on the relevant specification anchors, with their limitations and evidence. Such gaps do not silently narrow the supported contract; RFDs record plans for closing them.

Read in specification context

Query boundaries follow stable semantic products. Each public tracked query has a semantic key and returns the narrowest independently reusable product at that key. Temporary algorithm state is kept inside its owning query rather than exposed merely to obtain finer-grained memoization.

Read in specification context

Phase incompleteness is a terminal semantic outcome. A phase distinguishes a complete result from a conservative result limited by user error, unsupported functionality, unavailable facts, or an explicit resource bound. It never presents such a result as computation which merely needs more scheduling. This is the pipeline-wide consequence of Incompleteness is an explicit terminal outcome.

Read in specification context

Speculative checking changes commit atomically. A candidate or multi-part compatibility check stages its inference changes and obligations in an isolated child version. The whole operation either commits to its direct parent or is discarded; no equality, wake, or obligation from a rejected alternative reaches the requester. The version invariants are defined by Versioned egraph children are inference transactions.

Read in specification context

One body owns inference through quiescence. An InferCtx and all of its variables, versions, tasks, and obligations belong to one body query. A successful CheckedBody is published only after every type in its tree is resolved and no task, obligation, or speculative branch remains live.

Read in specification context

Solver knowledge crosses one canonical, transactional boundary. Goals and their local environment are canonicalized together; rigid inputs, flexible inputs, universes, substitutions, residuals, and goal-specific outputs all round-trip without capture or lost sharing. A normalization output is imported before it is related to the caller’s expected type. This is the inference consequence of Solver operations return goal-specific semantic outputs.

Read in specification context

The completed body is the incremental and scheduling boundary. Mutable inference steps are not separately memoized or externally visible. Reuse is determined by the completed CheckedBody and its semantic query dependencies, and internal branch or polling order cannot change that body. This is the inference consequence of Cross-item dependencies stop at semantic interfaces.

Read in specification context

Inference domains narrow transactionally without selecting a default. An effective domain follows its complete equality class, narrows only by intersection, and obeys the versioned egraph’s commit, rollback, revision, and wake rules. Only proof-derived constraints make a numeric class concrete in this slice; overloadable operator spelling does not narrow a domain, and scheduler quiescence does not authorize defaulting.

Read in specification context

Subtyping preserves representation; coercion is an explicit conversion. A successful subtype relation requires source and target to have the same memory layout and introduces no runtime conversion. A coercion is selected only at a coercion site, may change layout, and is materialized in the completed Typed IR. Never-to-any belongs only to the coercion relation.

Read in specification context

A checked body cannot publish residual inference work. Solver responses may add substitutions and residual goals during checking, but fallback and a mandatory terminal pass must discharge them or emit a diagnostic before CheckedBody is created. Incomplete solver results are terminal outcomes under Incompleteness is an explicit terminal outcome, not work silently left running after return.

Read in specification context

Speculation is an all-or-nothing inference transaction. Every operation which may partially constrain inference executes in an isolated child version. Complete success may atomically collapse an exclusive leaf; failure or cancellation discards all of its equalities, bounds, universe changes, wakes, tasks, and staged obligations. This is the inference consequence of Versioned egraph children are inference transactions and Inference-variable identities are unique across egraph versions.

Read in specification context

Missing metadata remains explicit incompleteness. A missing, unsupported, or conservatively incomplete external fact is never replaced by an inferred default, a successful interface, or exhaustive logical failure. This is the metadata consequence of Incompleteness is an explicit terminal outcome.

Read in specification context

Raw and lowered metadata share the same narrow reuse key. Each lowered semantic fact observes only its corresponding owned provider fact. Repeating an unchanged request reuses the lowered value without another raw request, and changing an unrelated provider fact does not invalidate it.

Read in specification context

External demand is decomposed by semantic product. Identity enumeration, signatures, impl headers, and individual associated values are separate tracked products. Consumers enumerate identities before requesting selected details, and no external function body is available to checking. This is the metadata consequence of Cross-item dependencies stop at semantic interfaces.

Read in specification context

External metadata supplies owned facts, never Sage decisions. The provider may state facts authored by a reachable dependency or the compiler, but it cannot resolve local syntax, select a Sage candidate, prove a Sage goal, normalize an alias, or type-check a Sage body. This is the typed metadata boundary established by External providers supply facts, not Sage semantic answers.

Read in specification context

Exhaustive absence requires complete expansion. Published symbols are safe to use even when expansion is incomplete, but an omitted symbol supports a definite negative answer only when expansion is complete for that semantic question. This is the expansion consequence of Incompleteness is an explicit terminal outcome.

Read in specification context

Expansion observes expansion inputs, never checked semantic detail. A module expansion may depend on parsed item identities, macro resolution and definitions, generated output, and completeness facts. It must not depend on item signatures, trait solutions, or function bodies.

Read in specification context

Expansion returns direct module members, not a visible-name environment. The result preserves deterministic order and provenance for source and generated direct items. Child-module members remain in the child, while imports and namespace lookup are interpreted later by resolution.

Read in specification context

Recursive expansion and same-module fixed points are distinct. Recursive processing expands invocations emitted directly by another invocation. Salsa fixed-point recovery is used only when resolving a macro requires the provisional expanded members of that same module; convergence does not imply completeness.

Read in specification context

The parse query depends only on parse inputs. Parsing one module may read its source, scope, edition, compilation configuration, and generated parse source, but never resolved names, checked interfaces, bodies of other items, or trait results.

Read in specification context

Item identity is separate from tracked syntax detail. Rebuilding a module may update an item’s CST or absolute location without minting a new symbol when its semantic identity is unchanged. Every represented definition owns a separate CST stash so an equal sibling can be backdated independently. This applies Symbols form the uniform semantic identity family and Stash for type-level interning at the parse boundary.

Read in specification context

Parse recovery never makes absence conclusive. An error item or error CST node is terminal for the current parse, but any consumer asking an exhaustive question must treat the surrounding represented set as incomplete unless it can prove the error irrelevant to that question. This is the parsing consequence of Incompleteness is an explicit terminal outcome.

Read in specification context

Parsing publishes syntax-backed identities, not semantic conclusions. A represented item has stable local identity, self-contained CST, ordering, ownership, and provenance. Resolution and checking remain downstream operations, and malformed or unsupported top-level syntax is represented explicitly rather than accepted as a definition. Tree-sitter is temporary parser machinery under Tree-sitter for parsing, not the published identity or syntax representation.

Read in specification context

Negative reasoning requires explicit completeness. A resolution result preserves every represented alternative separately from the fact that the searched source is exhaustive. An empty incomplete result is never interpreted as proof that the name or provider does not exist. This is the resolution consequence of Incompleteness is an explicit terminal outcome.

Read in specification context

Resolution dependencies follow the lookup actually performed. The owning phase observes only searched lexical/module scopes and keyed external membership. Provider discovery enumerates identities before loading selected signatures, and resolution never reads a checked body. This is the resolution consequence of Cross-item dependencies stop at semantic interfaces.

Read in specification context

Expansion cannot silently change an unqualified import root. Final import validation rejects a relative import whose first segment has a macro-generated direct or named-import binding and a glob binding to a distinct definition in the same namespace. This applies to unused imports and to roots of longer import paths. Glob targets and intermediate path segments use the type namespace; conflicts confined to another namespace do not make those roots ambiguous. Repeated routes to one definition are not ambiguous. Source-written named bindings retain precedence; explicitly anchored paths bypass this unqualified-root check. Validation reports the conflict after expansion without replacing the combined named-and-glob lookup used during expansion.

Read in specification context

Resolution stops at semantic identity. Ordinary path and name lookup returns symbols and completeness information; it does not infer a receiver, normalize an associated type, prove a trait obligation, or select an applicable method candidate as a hidden side effect.

Read in specification context

Lookup precedence is determined by scope, namespace, and path form. Lexical ribs take priority only for an unqualified one-segment name; module lookup then follows the applicable Rust namespace, imports, ancestry, prelude, and external-module rules rather than combining every visible name into an unordered global set. Leaving a lexical scope restores enclosing bindings; later bindings retain their own body-local identity and type even when nested or sibling scopes have allocated other locals.

Read in specification context

Alternative state is isolated and answer reduction is output-aware. Every disjunct candidate publishes a canonical response from isolated inference state. Aggregation is order-independent, retains hard knowledge common to every live alternative, and merges value-producing answers only when their outputs agree or an explicit priority rule dominates. Conjunct cancellation is permitted only after reconciling shared hard information. This is the solver consequence of Versioned egraph children are inference transactions and Whiteboard producers own isolated proof contexts.

Read in specification context

Solver completeness is groundness-sensitive and explicitly bounded. Non-ground queries terminate with only sound knowledge but may be ambiguous; ground queries return the complete logical answer unless a named, deterministic resource limit is exhausted. Incomplete candidate sources, ambiguity, and each overflow class remain distinct and none becomes No. This is the solver consequence of Trait solving is groundness-sensitive and resource-bounded and Incompleteness is an explicit terminal outcome.

Read in specification context

Candidate discovery is global, trait-keyed, conservative, and completeness-carrying. A proof considers represented impls in the local crate and every reachable dependency, keyed first by the fixed trait. Any self-head refinement retains blanket and unclassifiable fallback candidates, and a missing or incomplete source prevents exhaustive No. This is the solver consequence of Trait impl discovery is global and trait-keyed and Incompleteness is an explicit terminal outcome.

Read in specification context

Recursive semantics follow canonical cycles, not polling order. Repeated canonical goals use explicit inductive, coinductive, or unknown path semantics and provisional fixpoint evaluation. Infinitely growing distinct goals are overflow governed by deterministic structural limits, not ordinary cycle lookup.

Read in specification context

Goal-specific output is canonical solver knowledge. Prove(P) returns Proven, while input-only Normalize(Alias) returns a Type. The output’s variables participate in response binding, validation, caching, comparison, merging, and caller import; the caller’s expected type is related only after complete candidate answers are merged. This is the solver consequence of Solver operations return goal-specific semantic outputs.

Read in specification context

The local impl index is an incremental firewall. Its stable crate-owned identity contains a private tracked map, and keyed tracked lookup is the only reader. An unrelated edit may rebuild the map and reexecute a cheap lookup, but an equal trait bucket is backdated before impl-header lowering, solving, normalization, or body checking; impl-body edits do not alter signature-level buckets.

Read in specification context

Alias normalization preserves reveal context and narrow demand. An alias retains its identity until an operation requests its value. Revealability participates in the canonical input, and projection normalization reads only the fixed trait, associated item, applicable impl headers, selected associated values, and predicates required for that value. It never reads unrelated impls or bodies. This is the solver consequence of Named, associated, and opaque aliases share one semantic family and Cross-item dependencies stop at semantic interfaces.

Read in specification context

Scheduling cannot change the canonical return value. For fixed semantic inputs and configured limits, polling order may change discovery, cancellation timing, trace order, elapsed work, and memory use, but not the answer class, output, substitutions, residuals, hints, response numbering, ambiguity/overflow distinction, or overflow kind.

Read in specification context

One whiteboard frame has one final future output. A frame owns the producer for one canonical atomic goal, and all requesters subscribe to that work. Candidate-local and frame-level progress are revisioned side information; they do not create extra future outputs or expose raw candidate state. Suspended continuations remain Rust futures, polled in bounded rounds.

Read in specification context

A trait or impl function, type, or constant has its own stable symbol tied to its associated owner. Repeated requests and movement among siblings preserve that owner and the associated item identity.

Read in specification context

Checking an associated signature reuses its owner interface and never reads a sibling associated body.

Read in specification context

Checking and elaborating one function may read its own source and signature plus demanded signatures, fields, associated items, impl headers, metadata facts, and solver results. It must not read a callee or sibling body; a callee-body-only edit must not change or reexecute the caller’s completed body.

Read in specification context

Resolution may use names, paths, scopes, and namespaces to discover a definition, but every successful downstream semantic reference records the resulting symbol. Renaming an import or choosing another path to the same definition must not mint a different definition identity.

Read in specification context

Sage imports external facts through owned, definition-keyed queries. A metadata provider neither resolves Sage-local names nor performs Sage trait proof or normalization; those operations execute on the imported Sage values.

Read in specification context

An external symbol identifies a dependency definition by crate number and definition index, independently of the metadata facts requested about it. Metadata adapters supply one consistent definition kind for that identity.

Read in specification context

Symbol supports heterogeneous membership and resolution results. Operations whose meaning requires a definition kind accept the corresponding kind-specific wrapper; conversion into Symbol preserves identity, checked recovery accepts the right kind, and recovery of a wrong kind fails.

Read in specification context

A local symbol’s identity fields identify its definition. Independently tracked CST, spans, signatures, members, and bodies do not become part of that identity. Detail-only changes preserve the symbol, and consumers of unchanged sibling facts remain reusable; genuine identity changes are distinguishable.

Read in specification context

Named, associated, and opaque aliases retain their definition identity and generic arguments as one semantic type family across copy, fold, display, inference, canonical queries/responses, and oracle emission. A debug-formatted string is not a semantic rigid or alias type.

Read in specification context

Normalization is explicit. Completed IR need not erase every alias: named aliases reveal their substituted right-hand sides, associated projections normalize through trait solving, and opaque aliases reveal only inside their definition boundary or a future code-generation phase. An unrevealed alias retains provable declared bounds and can be related structurally by identity and arguments.

Read in specification context

Opening an associated signature reuses the owning trait or impl’s Self and generic parameter identities before introducing the associated item’s own parameters. A Binder pairs its value with the parameters binding references in that value; copying or opening it does not mint replacements for those identities.

Read in specification context

Await remains a high-level operation over an explicitly resolved IntoFuture conversion and Future::Output type; it does not contain polling, suspension-point, or state-machine lowering.

Read in specification context

A completed closure has a typed nested body with explicit parameters and captures.

Read in specification context

If-let, while-let, and let chains lower into structured match and control-flow forms.

Read in specification context

An async block or async function has a typed nested coroutine body. Typed IR does not lower it into a generator state machine.

Read in specification context

A recovery body represents failure using explicit error nodes backed by diagnostics, never an unresolved choice presented as an ordinary successful node.

Read in specification context

Completed bodies consume method syntax and temporary adjustment recipes. Implicit borrows, dereferences, and coercions are explicit typed nodes; successful output contains no source-shaped placeholder for an unresolved operation. Structured control flow remains a tree, without basic blocks, a drop schedule, generator lowering, or borrow-check results.

Read in specification context

A for expression lowers into an IntoIterator call followed by a structured loop and match.

Read in specification context

Index syntax lowers to a resolved Index or IndexMut call with typed operands.

Read in specification context

A checked expression represents its macro expansion output; a macro invocation is not itself a successful checked expression node.

Read in specification context

No live inference variable or unresolved semantic choice survives in a successful completed body. Completion resolves type edges and produces the final tree independently of temporary inference state.

Read in specification context

Every path, field, variant, function, and associated-item reference in a successful completed body records its resolved definition identity.

Read in specification context

The question-mark operator lowers into a Try::branch call, a ControlFlow match, and a FromResidual call.

Read in specification context

Every expression and pattern in a successful completed body has a type and source provenance, including nodes synthesized from a source expression.

Read in specification context

Completed calls distinguish direct function definitions, statically dispatched trait methods, dynamic trait-object methods, function pointers, and callable-trait dispatch through Fn, FnMut, or FnOnce. Receiver/coercion operations are already explicit tree nodes, not a replayable adjustment list.

Read in specification context

A completed call records the selected function, dispatch family, owner substitutions, and method substitutions. Trait-method calls retain Self and the selected trait reference; the proof justifying a call need not return a concrete impl identity.

Read in specification context

Every explicit, elided, universal, existential, imported, and synthesized lifetime lowers to Dummy. Dummy is neither static, a lifetime inference variable, nor post-analysis region erasure, and this deliberate omission does not create ambiguity.

Read in specification context

Outlives(Dummy, Dummy) holds. Reference and dereference operations remain explicit because they affect ordinary types, while Sage does not check borrow liveness, uniqueness, overlap, or validity.

Read in specification context

Non-overloadable && and || remain explicit lazy logical operations whose right-hand side is conditionally evaluated; they do not become eager trait-method calls.

Read in specification context

Every proven overloadable operator in completed Typed IR is a resolved trait-method call, whether its operands are primitive, generic, or user-defined. The call retains method identity, substitutions, explicit adjustments, and result type; no overloadable case completes as Binary. Primitive recognition belongs to later codegen with concrete substitutions.

Read in specification context

Generic parameters use their own source-backed, external, or alpha-equivalent identity family. A field is identified by its owner plus field index, and a local by its body-local ID; these are not global Symbol variants. Semantic values retain these scoped identities.

Read in specification context

Each generated parse source is identified by stable source input, generating operation, and occurrence, while generated text and current origin coordinates are mutable facts. Moving the origin must not collapse distinct occurrences or mint a replacement source identity.

Read in specification context

The parser measures each item from the earliest of its first attribute and item-node start, so attribute offsets are nonnegative. Entering an associated item establishes a new item-relative base rather than retaining the enclosing trait or impl base.

Read in specification context

An edit outside an item which only moves its absolute range may update diagnostics and position lookup, but leaves relative CST and typed content equal and must not propagate into semantic consumers which did not read the absolute coordinate.

Read in specification context

A source-root item owns an absolute span in one ParseSource. A nested definition is placed relative to its immediate represented owner, and its signature CST, body CST, and typed-body nodes use offsets relative to that definition’s own start. Resolving a nested node composes every intervening relative range with the source-root absolute range.

Read in specification context

Determinism is an emitter responsibility. Each side chooses stable definition identities and semantic ordering before emission, including forward references. The comparator never sorts, renumbers, or otherwise repairs nondeterministic or order-dependent output.

Read in specification context

Conformance is exact identity of independent emissions. Sage and rustc each produce and validate a complete value in the shared semantic schema, serialize it deterministically, and pass only when the serialized bytes are identical. A structural or textual diff may diagnose inequality but cannot decide equality.

Read in specification context

Each adapter is a fixed projection into the shared model. An emitter may translate its native identities, adjustments, and deliberately deferred lifetime representation, but the projection cannot inspect the other output or erase a distinction merely because Sage does not yet match it. Missing shared vocabulary is repaired by extending the schema and both independent projections.

Read in specification context

Equality is accepted only after independent coverage. Each emitter accounts for every in-scope item and body and rejects forbidden placeholders before comparison. Paired omission, paired unsupported nodes, or paired debug fallback values therefore cannot satisfy conformance even if the remaining serialized bytes agree.

Read in specification context

Handles never cross stash ownership implicitly. A Ptr<T> or Slice<T> is interpreted only by its allocating Stash. Retaining a value across a stash boundary requires a structural copy into the destination; a checked output tree must not contain handles back into its source CST or an imported query result.

Read in specification context

Allocated entries are immutable. Stash is append-only: alloc and alloc_slice may add entries, but safe code cannot mutate a Ptr<T> or Slice<T> allocation after it has been interned. Transient inference state is finalized by resolving and copying the completed value into a fresh output stash.

Read in specification context

A stash-owned tree is one incremental value. Salsa compares and backdates a Stashed<T> root as a unit; nodes below that root are not independent tracked identities. Finer incremental boundaries are introduced as semantic queries outside the tree, not by exposing its internal handles.

Read in specification context

Query-result equality follows rooted semantic content. The equality, ordering, hashing, and Salsa update behavior of Stashed<T> use a deterministic structural fingerprint of the reachable root, not stash addresses, allocation order, padding, or unreachable allocations.

Read in specification context

Allocation is content-addressed within one stash. Every value and slice allocation is hash-consed by its typed structural content. Equal content of the same stash data type yields the same handle, while hash collisions are resolved by actual content comparison rather than sharing.

Read in specification context

Unknown or malformed directives, invalid compiler conditions, missing or unused observation expectations, and invalid selections fail the test. A fixture containing any //# ty or //# sym marker requires one combined observations: expect![...] expectation; a observations expectation without observation markers is rejected. Annotation validation is independent of snapshot blessing, and no directive is silently ignored because it is misspelled or cannot be resolved.

Read in specification context

Before any expectation in one test invocation is compared in updating mode, the runner completes fixture validation, compilation, annotation validation, observation collection, independent exhaustive diagnostic matching for both Sage and rustc, requested query projection, and rendering of every requested output. All resulting snapshot strings are prepared before any updating expectation assertion runs. A failure in any of those steps prevents all snapshot writes for that invocation. After they succeed, UPDATE_EXPECT=1 may update observation, diagnostic, and requested query representations. It never adds source markers, changes compiler conditions, or accepts an unmatched diagnostic. Other independent Cargo tests may update their own expectations; this is not a workspace-wide filesystem transaction.

The implementation separates preparation from expectation comparison. Preparation returns either all validated, rendered results or a failure, without invoking expect-test assertions. The caller stops on failure and compares the returned results against the supplied expectations only on success. An implementation comment at that boundary explains why this ordering prevents partial updates when preparation fails; no separate transaction mechanism is required.

Read in specification context

Expectations passed through compile_test! retain their author-written source locations. Blessing edits those expectation literals at the test call site, not the macro implementation or a generated temporary file. Normal test runs compare expectations without modifying sources. Updates must be verified with an independent subsequent run with updating disabled.

Read in specification context

V1 requests signatures and checks every supported body in the selected local crate, including reachable submodules, associated bodies, and expanded items, regardless of visibility or selector presence. It does not eagerly check external dependency bodies. Unsupported in-scope work must be reported as a failure or explicit diagnostic, never silently omitted as success. Adding a type marker cannot change this demand policy. A future explicit entry-point mode may select a narrower demand; it is not part of v1.

Read in specification context

Both Sage and rustc run for every fixture. Unqualified ERROR/WARN markers apply independently to each compiler; if SAGE and if rustc apply only to the named compiler. Each compiler must have a complete one-to-one match against its applicable markers. One unqualified marker expects one diagnostic from each compiler, not two from either. rustc contributes diagnostic checks only, not observation, diagnostic-text, or query snapshots. Compiler-specific markers record intentional differences and require a semantic explanation when changed.

Read in specification context

Type observations read final types after body checking completes. They neither constrain inference nor select semantic candidates. All selected expressions are observed from that completed result. An explicit error type may be snapshotted when checking produced one, but an absent result or unresolved successful inference is an observation failure, not an invented type or an omitted entry. Expected snapshot text cannot influence compilation. When coercion changes an expression’s type, the observation includes both its completed type before coercion and the resulting type of its coercion wrapper; it does not replace the original type with the coerced type.

Read in specification context

The runner inspects the source string after indoc! or another supplied source expression has evaluated. It does not independently dedent it again. Line numbers refer to that resulting source, including annotation lines. Actual tab characters remain rejected for consistent fixture formatting. Type selection depends only on the target line: Unicode character widths and horizontal alignment do not affect which expressions are observed.

Read in specification context

The default fixture has the real standard library and its dependency metadata. V1 supplies the standard library; arbitrary third-party dependency configuration is a later extension.

Read in specification context

The diagnostic set includes all source diagnostics from parsing, expansion, resolution, signature checking, and body checking. Repeated demands reporting the same diagnostic do not duplicate it. Distinct diagnostics remain distinct even when their messages and locations are identical. Malformed source is a negative-test input, not by itself an infrastructure failure.

There must be a complete one-to-one matching between applicable ERROR/WARN markers and emitted diagnostics. Each marker consumes one diagnostic, and each diagnostic consumes one marker. Multiple diagnostics on one line require multiple markers. Matching considers the complete eligibility relation, so a greedy choice cannot reject an otherwise valid assignment. Missing diagnostics, extra diagnostics, and severity mismatches fail even if their rendered output matches a snapshot. Matching never changes diagnostic output order.

Read in specification context

Diagnostic markers match structured diagnostics by severity and logical source file/line. A diagnostic is eligible if its primary span intersects the target line, or if that primary span’s macro-expansion ancestry contains an invocation intersecting it. An empty span matches the line containing its position: for example, a missing-token diagnostic can point between characters without covering any character. A position at the start of a line belongs to that line; EOF belongs to the final source line (including an empty final line after a trailing newline). The same rule applies to empty invocation spans in expansion ancestry. Nested expansions retain this ancestry. For Sage, the primary span is Diagnostic::span; entries in Diagnostic::labels do not participate in matching, regardless of their label style. Labels, attached notes, and help remain in the rendered snapshot but do not supply additional matching locations or ERROR/WARN events. Matching does not parse rendered text. Each diagnostic counts once even if its primary span or expansion ancestry matches several lines. A source diagnostic with no matchable location remains unmatched and fails the test.

For rustc, only spans marked is_primary in structured JSON diagnostics and their recursive expansion invocation spans are eligible. Any eligible primary span may match. Child notes/help and secondary spans do not introduce events or eligible locations. rustc’s spanless final error/warning count summaries and failure-note explanations are presentation, not additional source diagnostics; other spanless errors or warnings fail matching. Distinct top-level diagnostics are never deduplicated by message text.

Read in specification context

The default fixture uses the latest Rust edition supported by the repository’s pinned toolchain. An explicit edition fixes an older supported edition; unknown editions fail setup.

Read in specification context

A fixture provides exactly one anonymous source or one files map. Anonymous source becomes src/lib.rs. A files map must contain src/lib.rs, the fixed crate root. There is no root-selection option or automatic root detection. Paths are relative to the materialized project and imply directories; files become modules only through Rust’s module-loading rules. An implicit mod child; with both child.rs and child/mod.rs present is rejected as ambiguous; an explicit #[path] selects its named file. Duplicate paths, absolute paths, parent traversal, a missing src/lib.rs, and file/directory conflicts are fixture errors. The generated Cargo.toml and Cargo.lock, .cargo configuration, and a root build.rs are reserved and cannot be supplied as fixture files. Unreferenced files are not implicitly compiled; annotations in files outside the selected crate are rejected rather than silently left unchecked.

The anonymous form supplies a Rust expression evaluating to source text:

compile_test! {
    source: indoc! {r#"
        pub fn value() -> u16 { 22 }
    "#},
}

The named-file form maps string-literal paths to source-text expressions. Slashes in a path create directories; there is no separate directory syntax:

compile_test! {
    files: {
        "src/lib.rs": indoc! {r#"
            pub mod model;
        "#},
        "src/model.rs": indoc! {r#"
            pub mod detail;
        "#},
        "src/model/detail.rs": indoc! {r#"
            pub fn value() -> u16 { 22 }
        "#},
    },
}

Top-level fields use name: value syntax, separated by commas. The files map uses "relative/path.rs": source_expression entries, also separated by commas. Both accept trailing commas. Field order is immaterial; duplicate or unknown field names are rejected. source and files are mutually exclusive and one is required. The crate root is always src/lib.rs. Source expressions may be ordinary or raw string literals, or expressions such as indoc! invocations. Both forms may also include edition, observations, diagnostics, and queries as illustrated in Authoring a test.

Read in specification context

observations: expect![...] holds one snapshot for all ty and sym markers. An expression selected by both markers has one header, then indented symbol: and type: fields in that fixed order. Only requested fields are printed. Duplicate markers are idempotent and marker order does not change output. Ordering follows the type observation source-tree postorder rule. Diagnostics and query snapshots remain separate.

Read in specification context

An inline compilation test runs inside a standard Rust #[test] under the ordinary Cargo test harness. compile_test! accepts fixture source expressions and explicit expect_test::expect! values at the call site. Assertions use the existing #[sage::test(...)] association attribute; no separate test discovery or anchor attribute is required. A failing observation fails that Rust test.

Read in specification context

Fixture evaluation uses the production workspace-loading, parsing, expansion, resolution, and checking paths with real dependency metadata. Inline sources and generated project configuration are inputs; expected types, diagnostics, and query logs are outputs, never providers of semantic answers. Invalid Rust must reach Sage even if it would fail rustc checking. Using rustc to provide standard-library metadata does not count as running a rustc conformance test. Setup and provider failures fail the test directly, not as expected source diagnostics.

Read in specification context

Each test gets an isolated materialized Cargo project whose source is the supplied fixture, with deterministic logical paths and no dependence on the caller’s working directory or enclosing workspace’s default members. The fixture is compiled as an ordinary library, with cfg(test) disabled and no enabled Cargo features; running the enclosing Rust test does not enable test compilation for the fixture.

Read in specification context

An optional query expectation observes a cold run in a fresh Sage database. Project/provider setup finishes before capture begins, without pre-demanding the fixture’s local semantic products. Capture covers local crate discovery, signature and body demands under the checking policy, and semantic reads needed to collect requested observations. It ends before rendering or comparing frozen outputs. Observation-related work is retained rather than hidden, while the set of checked bodies remains selector-independent. Warm runs, edits, and explicit point demands are later extensions.

Read in specification context

Query snapshots use stable semantic operation names and identities, retain parentage, multiplicity, and available execution/reuse dispositions, and omit allocation-dependent IDs and temporary paths. Only siblings explicitly defined as unordered may be canonically sorted. Unknown operations remain visibly unmapped rather than disappearing. An unmapped query key keeps its operation name and omits allocation-dependent debug arguments; it does not pretend to provide a semantic identity for those arguments. The projection follows the Inspector’s deterministic trace contract instead of inventing an unrelated raw-debug-string golden format.

Read in specification context

The combined type observations, the complete rendered Sage diagnostic output, and an optional query log are separate expect_test::Expect values, created with the expect_test::expect! macro from the expect-test crate. Examples use expect! after use expect_test::expect;. The runner uses that library for snapshot comparison and UPDATE_EXPECT=1 updates, subject to the blessing gate. Type descriptions and expression ordering are deterministic. Expression source descriptions occupy one line, omit annotation comments, and normalize whitespace between tokens without changing token contents or merging tokens. Literal contents are preserved; embedded line breaks and delimiter characters are escaped as needed to keep the description on one line and unambiguous. Diagnostic rendering preserves meaningful order, labels, notes, and source excerpts, including annotation comments. Paths use fixture-relative names rather than temporary directories or machine-specific roots. Normalization removes incidental presentation details only; it does not erase semantic distinctions, unresolved results, or unexpected diagnostics.

Read in specification context

//# sym observes explicit path expressions starting on the target line, including local variable uses and qualified paths. It reports the definition selected by completed checking, not the spelling of an import alias. Local item identities include their kind and a crate::-qualified name. Local bindings use their name and a one-based occurrence among same-named bindings in declaration order within the body; unrelated declarations do not renumber them. External definitions use the metadata definition path. No allocation IDs or source coordinates appear. An actual resolution error is <unresolved>; missing or unsupported semantic correspondence fails the observation. A target line containing no path expression fails rather than producing an empty result. Associated local item identities are not yet supported and fail explicitly. V1 symbol selection excludes method names, field names, type syntax, patterns, and implicit calls introduced by elaboration. These can gain selectors later. Names are frozen before ending query capture, as with types.

For example, selecting both markers on module::value() produces:

src/lib.rs: path `module::value`
  symbol: fn crate::module::value
  type: fn() -> u16
src/lib.rs: call `module::value()`
  type: u16

Read in specification context

An anchor-associated inline test contains its source fixtures, annotations, explicit configuration, and expected observations directly in the annotated Rust function. The ordinary claim/test review captures the entire macro invocation as part of that function’s source. The harness macro implementation is not included in that snapshot; it is reviewed and tested independently. Reviewers evaluate whether the visible scenario and assertions establish the associated claim. A changed ERROR/WARN marker or compiler condition is a changed assertion of intended behavior and requires semantic justification, not merely a successful blessing run.

Read in specification context

Every inline fixture is checked by both Sage and the rustc binary paired with Sage’s embedded compiler and standard-library sysroot. There is no implicit skip or opt-out. rustc checks the same materialized src/lib.rs, files, edition, and host target as an ordinary library, with no test configuration or enabled features. It emits metadata only; fixture code is never executed. rustc checking is separate from dependency metadata loading and Sage query capture. Source errors in either compiler do not prevent running the other compiler. Missing executables, malformed compiler output, abnormal termination, and an exit status inconsistent with the reported errors fail preparation as infrastructure errors.

Read in specification context

rustc starts with warning-by-default lints individually allowed, using the pinned compiler’s lint inventory, to keep incidental unused-item and naming lints out of ordinary fixtures. Deny-by-default lints remain enabled. Source-level lint attributes may enable specific warnings or deny them; emitted warnings and errors must then have matching markers. This is not a lint cap and does not suppress hard language errors.

Read in specification context

A ty observation includes every source expression whose span starts on its target line in the same file. An expression may extend across subsequent lines; its start alone determines inclusion. Expressions starting on earlier or later lines are omitted, even if they contain or intersect the target line. Multiple sibling expressions starting on one line are all included. Each selected source expression appears once, with its logical filename, expression kind and readable source description, and completed type. The snapshot omits line numbers, columns, and ranges. Blocks follow the same start-line rule; a function-body block starting earlier is not included merely because it contains the target line.

All type markers contribute to the same snapshot. Files are ordered by logical path, then marked target lines by source order. Within each target line, output follows source-tree postorder: children before parents, with siblings in source order. Repeated markers targeting the same line do not duplicate observations. Distinct source expressions remain distinct entries even if their rendered text is identical. Source nesting distinguishes expressions with equal spans. Generated elaboration nodes do not add duplicate observations, except that meaningful coercion wrappers are reported after their wrapped expression. Each wrapper belongs to the selected source expression and exposes its resulting type, preserving child-before-parent order through a chain of coercions. A target line with no expression starting on it, or lacking a reliable source-to-semantic correspondence, fails explicitly. V1 observes expressions; binding declarations and other semantic entities require future selectors.

For example, an inline marker targets the code on its own line. The observations expectation contains the complete ordered observation:

use expect_test::expect;
use indoc::indoc;

#[test]
fn tuple_types() {
    compile_test! {
        source: indoc! {r#"
            fn example() -> (u16, (bool, u8)) {
                (1u16, (true, 2u8)) //# ty
            }
        "#},
        observations: expect![[r#"
            src/lib.rs: literal `1u16`
              type: u16
            src/lib.rs: literal `true`
              type: bool
            src/lib.rs: literal `2u8`
              type: u8
            src/lib.rs: tuple `(true, 2u8)`
              type: (bool, u8)
            src/lib.rs: tuple `(1u16, (true, 2u8))`
              type: (u16, (bool, u8))
        "#]],
        diagnostics: expect![""],
    }
}

The first tuple element precedes the second element’s subtree. Within that subtree, both literals precede their tuple. The function-body block starts on the preceding line, so it is omitted. The function declaration itself is not an expression.

A multi-line call demonstrates that enclosing expressions starting on earlier lines are omitted:

use expect_test::expect;
use indoc::indoc;

#[test]
fn call_argument_types() {
    compile_test! {
        source: indoc! {r#"
            fn inner(value: u16) -> u32 { value as u32 }
            fn outer(first: u32, second: u16) -> u64 { first as u64 + second as u64 }

            fn example() -> u64 {
                outer(
                    inner(22u16), //# ty
                    33u16,
                )
            }
        "#},
        observations: expect![[r#"
            src/lib.rs: path `inner`
              type: fn(u16) -> u32
            src/lib.rs: literal `22u16`
              type: u16
            src/lib.rs: call `inner(22u16)`
              type: u32
        "#]],
        diagnostics: expect![""],
    }
}

The callee path outer, the outer(...) call, and the function-body block start on earlier lines, so they are omitted. The literal 33u16 starts on a later line and is also omitted. Moving the marker to the line immediately after outer( would instead observe the path outer followed by the complete outer(...) call, even though that call ends several lines later. These expectation literals illustrate the filename-only output. Moving an expression to another line without changing observation order does not itself change its type snapshot. Expression descriptions use the single-line rendering rules below. Type representations describe the completed types currently exposed by Sage; the runner does not manufacture distinctions absent from its typed IR.

Read in specification context

For every directive, non-whitespace source content before the annotation comment makes its target the current line. Otherwise its target is the most recent preceding nonempty line that is not an annotation-only line. Blank lines and consecutive annotation-only lines are skipped; ordinary comments are not skipped. Absence of a target is an annotation error. The same rule applies to ty, sym, ERROR, and WARN; there is no caret or range syntax.

Read in specification context

Every specification anchor has a stable page identifying the rule and showing its definition, context, implementation entries, and tests/evidence. The page includes Rust excerpts and access to surrounding source, and exposes each entry’s placeholder status and explanation. Multiple sites remain individually inspectable rather than being reduced to a single coverage badge.

Read in specification context

The book build includes the architecture explorer and its model and Rust source snapshots. An explorer chapter embeds the browser and offers a full-page view. The handwritten Crates landing page links to .sage subchapters that provide the searchable, interlinked presentation defined by the browser specification. Book generation and local serving share the model and renderer under its delivery rule. Published browsing, including the Rust source pane, works without a running sage-meta serve process. Local book rebuilds refresh the snapshot when the model or its Rust sources change.

Read in specification context

A specification rule can be defined in a Markdown or .sage Design chapter, with equal authority. Its definition records the rule’s text and source location; a .sage definition also identifies its containing declaration, method, or envelope clause. Either documentation form can reference a rule defined in the other without creating another definition. Every reference must resolve to an existing definition; a dangling reference is an error.

Read in specification context

An anchor’s content starts after its definition marker and includes every subsequent Markdown block until the first applicable closing boundary. Blank lines do not end the content: paragraphs, lists, tables, and code blocks within that extent belong to the same anchor.

Read in specification context

A standalone line containing exactly <!-- end anchor -->, apart from surrounding horizontal whitespace, ends the active anchor immediately before that line. The comment is excluded from the anchor’s content. Subsequent prose remains outside an anchor until a new definition begins; the explicit marker is optional when another closing boundary already ends the content.

Read in specification context

A Markdown section heading ends the active anchor’s content immediately before the heading, regardless of heading level. Both hash-prefixed and underline-style headings are boundaries. Prose following the heading remains outside an anchor until another definition begins.

Read in specification context

Boundary-looking text inside fenced or indented code blocks, inline code, or escaped text does not open or close an anchor. Raw HTML examples do not supply anchor definitions, section headings, or end markers. A standalone end comment acts as a boundary only outside these literal contexts and enclosing HTML blocks.

Read in specification context

A new anchor definition ends the preceding anchor’s content immediately before the new marker. The new definition belongs to its own anchor; content extents do not overlap.

Read in specification context

An anchor’s content ends at the end of its containing Markdown document or .sage triple-quoted prose block. A .sage anchor never captures surrounding language syntax or content from another prose block, declaration, or method.

Read in specification context

An explicit end marker with no active anchor is a validation error. Another end marker after an explicit or implicit end, without an intervening definition, is therefore also an error. An anchor ending at another definition, a heading, or its source boundary does not require an explicit end marker.

Read in specification context

Clicking an anchor badge opens its anchor page. The page’s context link returns to the defining Markdown paragraph or .sage location. Context permalinks remain available independently of the anchor-page URL, so navigating to the rule’s connections does not lose access to its original specification text.

Read in specification context

An implementation or test entry establishes a declared association, not proof that the rule is satisfied. Source inventories retain cfg conditions without claiming that a site was compiled or a test executed. Anchor pages distinguish test source, recorded run results, and other evidence such as traces. A passing structural check or a passing dummy test must not present a TODO or Not applicable entry as established behavioral evidence.

Read in specification context

The explorer’s selected Sage entity or specification anchor is reflected in the enclosing chapter’s URL. Opening that URL restores the selection, and browser back/forward navigation keeps the chapter and explorer in agreement. Sharing a selection preserves the book’s navigation as well as the selected context. Every entity is directly addressable under the entity-link rule; these links are also available to references from other documentation.

Read in specification context

Every specification anchor has at least one explicitly declared Rust implementation entry. An anchor without one is an error. A test annotation or #[sage::item(...)] correspondence alone does not supply this entry. A placeholder implementation counts as an entry with its explicit status.

Read in specification context

A Rust implementation entry is introduced by a <code>// {anchor}`meta.language.calls.declared`</code> comment, optionally followed immediately by <<. Its name must resolve to a specification definition; malformed and unknown references are errors. Only actual Rust comments create these entries: marker-like text inside string literals does not. Entries retain their source location and enclosing module, and multiple entries may reference the same rule, including across crates.

Read in specification context

Implementation references and test annotations inside a Rust module named todo record work not yet done; those inside not_applicable record that the implementation or test does not apply. Each entry retains this status and its accompanying explanation. Ordinary entries, TODO entries, and Not applicable entries are displayed separately, even when they reference the same rule. An empty special module creates no entry: it must contain an implementation reference or an annotated test to account for the respective requirement.

mod not_applicable {
    // {anchor}`example.documentation_rule`
    // This rule describes documentation organization and has no runtime implementation.
}

mod todo {
    #[test]
    #[sage::test(example.documentation_rule)]
    fn documentation_rule() {
        // TODO: Check the generated documentation against the rule.
    }
}

The example’s example.documentation_rule stands for an existing definition; it does not declare a rule. Placeholder status applies independently to the implementation and test sides. Nesting a module under both todo and not_applicable is an error.

Read in specification context

A point reference has no << suffix. Its initial excerpt contains the marker line and the next five source lines, truncated at end-of-file. A See more… action opens the surrounding source at that location; the five-line preview does not claim to delimit the implementation.

// {anchor}`meta.language.calls.declared`
check_declared_call(caller, callee)?;

Read in specification context

A region opener without a closing delimiter, or a closing delimiter without an open region, is an error. Delimiters in string literals do not open or close regions. Region boundaries are determined from source comments, independently of the five-line previews used for point references.

The existing // ANCHOR: name / // ANCHOR_END: name convention remains independent: it delimits explanatory excerpts for mdBook/ezanchor. Canonical implementation entries require only the specification comment syntax above.

Read in specification context

A reference ending in << opens an explicit region, and a standalone // >> comment closes the nearest open region in the same file. Regions may nest. The excerpt spans the opening marker line through its closing marker line, with access to the surrounding source. A point reference inside a region remains a point reference and does not close or replace that region.

// {anchor}`meta.language.calls.declared`<<
let caller = current_operation();
check_declared_call(caller, callee)?;
record_call(caller, callee);
// >>

Read in specification context

Every specification anchor must have at least one annotated Rust test. An anchor without a test is an error, independently of its implementation coverage. A placeholder test counts as an entry with its explicit status; an implementation placeholder alone cannot satisfy the test requirement.

Read in specification context

Every #[sage::test(...)] reference must resolve to an existing specification anchor and be attached to a Rust test. Dangling and misplaced references are errors.

One test can cover several rules and a rule can have several tests. Unlike sage::item, a test may reference a rule across crate boundaries. An eligible test entry is a module-level function with the built-in #[test] attribute in a Cargo target with tests and the standard test harness enabled. Targets with test = false or harness = false and unconditionally or conditionally ignored tests cannot satisfy the requirement.

Read in specification context

Every specification anchor has a well-formed full name and exactly one definition in the Design chapter inventory. Malformed markers and duplicate full names are errors. Names are derived from the defining chapter; moves between chapter namespaces rename the rule and require updating its references.

Resolved names are dot-separated ASCII identifiers and describe independently testable behavior. A Markdown definition uses a chapter-local name with the custom MyST-style inline-role syntax. For example, in design/meta/language.md:

{anchor}`calls.declared`
Every observed architectural call must be permitted by its caller's resolved
dependency envelope.

The marker and the opening prose form one paragraph: do not leave a blank line between them. Later blocks can continue the same claim under the content rules. The example resolves to meta.language.calls.declared. Use the same definition syntax inside .sage triple-quoted prose. In either format, {spec} followed by a backtick-quoted full name references an existing rule without creating another definition.

Read in specification context

Moving a rule within its chapter preserves its identity. Changing its local name or moving it into a different chapter namespace renames the rule and requires updating specification, implementation, and test references. Published links to the old location retain a redirect or context alias. A compatibility link does not create a second canonical definition or satisfy a stale code reference.

Read in specification context

The mdBook Design chapter tree is the canonical specification. Markdown and .sage are equally authoritative source formats within that tree. Every active rule definition belongs to a Design chapter with identifiable source context; its appearances in generated indexes or anchor pages refer to that definition and do not create additional definitions.

Read in specification context

Book generation, standalone export, and local serving use the same resolved model and renderer to implement these browsing rules. Invalid models produce diagnostics instead of a partially valid explorer. A generated book or standalone HTML artifact includes the data and assets needed for navigation, search, entity links, and Rust source display without a Sage server. Each view identifies itself as a snapshot. Model or Rust edits become visible when that snapshot is rebuilt, exported again, or regenerated by restarting the server.

Read in specification context

Method views render each declared envelope clause with its effect kind and target: invocations, input reads, context creation, and transitive prohibitions. They expose possible direct callees, reverse callers, and overriding implementations, using the validator’s conservative dispatch resolution. Inherited prohibitions retain their declaring method. Linked targets lead to the corresponding entities. These views label declared permissions and prohibitions as such; they do not imply that a permitted call happened or that runtime conformance has been established.

Read in specification context

Readers can reveal or hide a Rust source pane without leaving the selected Sage entity. The pane follows selection and uses indexed Rust correspondences, showing the file, line numbers, and highlighted declaration with surrounding source. Multiple mapped sites are individually selectable. Missing source is reported explicitly. Module markers, macro-input sites, and cfg conditions remain distinguishable from a confirmed active executable implementation. The pane identifies its contents as a source snapshot; navigating to code does not establish that the code executed or satisfied a specification rule.

Read in specification context

Search finds declared entities by name, qualified model path, descriptive prose, and corresponding Rust paths when available. Crate and entity-kind filters combine with the search text. Results identify each entity’s kind and owner and link directly to it, including named members. The view states when no entities match. Changing search or filters does not invalidate an entity’s direct link or prevent opening a linked entity outside the current results.

Read in specification context

The sage-meta serve <port> command validates and renders the selected model before serving its snapshot on the loopback interface. It reports the local URL and serves until stopped. The port must be an integer from 1 through 65535; an optional model path selects the input. Invalid arguments, model errors, and binding failures produce a failing exit status with a diagnostic. Opening the reported URL provides the specified browser without another serving command.

For example, cargo run -p sage-meta -- serve 3001 serves the snapshot at http://127.0.0.1:3001/. cargo run -p sage-meta -- browse writes a standalone HTML snapshot. The commands are ways to deliver the browser specified here.

Read in specification context

Readers can navigate from crates to modules, declarations, and their members, with the owning crate, module, and declaration visible at each level. Crate views show purpose and dependencies. Declaration views show kind, descriptive prose, generic parameters, and the modeled structure: struct fields, enum variants and their fields, or the description of an opaque type. Class and context views show fields, base classes, and methods, distinguishing declared, inherited, abstract, and overriding methods. Method views show query/function kind, signature, and prose. References to modeled types, bases, and methods link to their declarations.

Read in specification context

An anchor’s full name combines its chapter namespace with the local name written at its definition. The namespace is derived from the chapter source path relative to Design, removing the extension and joining path components with dots. For example, local point_excerpts in design/meta/anchors.md names meta.anchors.point_excerpts. The same derivation applies to .sage chapters. Section headings, chapter titles, and sidebar ordering do not change these names; only the source path and local name contribute. Ambiguous namespace derivations or duplicate full names are errors.

The intended Markdown source spelling is local:

{anchor}`point_excerpts`
A point reference displays its marker line and the next five source lines.

Rust references use the resolved full name, such as #[sage::test(meta.anchors.point_excerpts)] or <code>// {anchor}`meta.anchors.point_excerpts`</code>. Filename components must normalize to ASCII identifiers; different source paths that normalize to the same chapter namespace are rejected.

Read in specification context

Every .sage chapter lies beneath a directory identifying its Rust crate. The crate’s crate.sage manifest establishes the modeled crate boundary; the book loader checks that ownership against the Rust workspace. Book chapter namespaces and compiler-model item identities are distinct: moving a crate’s book directory preserves identities such as $sage_ir::symbols::Symbol when the modeled crate and declaration paths are unchanged.

Read in specification context

The Crates landing page preserves handwritten Markdown from design/crates/README.md. Its curated subsystem introductions link to rendered crate chapters and modeled entities. Generated crate and module chapters are children of this page; generation does not replace its prose with the explorer. Links written to .sage source chapters resolve to their rendered chapters.

Read in specification context

Every declared Sage entity has an unambiguous direct link, including crates, modules, types, classes, contexts, methods/queries, and named members such as fields and enum variants. Opening a link selects the declaration or member in its rendered context without a prior search or browser session. Links resolve through the entity’s identity and owning scope: equal local names in different owners remain distinct, and relocating a chapter does not break links to unchanged model entities. Markdown and .sage sources can reference these identities; rendered references link to the corresponding entity and unresolved references are errors.

Entity links and specification anchors have different purposes. For example, $sage_ir::symbols::Symbol identifies a modeled declaration, whereas meta.book.entity_links identifies a testable rule. Making a declaration linkable does not create a specification rule or require an extra named paragraph. The authoring syntax for entity references and URL spelling remain implementation-plan decisions. Selection URLs and browser history follow the navigation rule.

Read in specification context

The anchor index groups entries hierarchically by their name prefixes, such as meta and meta.book. Each group can reveal or hide all its descendants, and reports implementation and test status counts for that subtree. Grouping and counts are derived from the same active anchors displayed in the index.

Read in specification context

The generated Anchors landing page lists every active rule. Each namespace prefix has a page with the same table restricted to that prefix. A rule named meta.foo.bar has a direct page under design/anchor/meta/foo/bar; the page shows the rule and navigation within its surrounding namespace. If a rule’s name is also a prefix of other rules, one page presents both its own claim and its descendants. Generated pages do not create new specification definitions.

Read in specification context

The Design section includes an automatically generated index of every active anchor. Each anchor has a main row containing the final component of its name, with the namespace supplied by the enclosing group or page heading, and separate implementation and test statuses. The name’s tooltip shows its full identity. A disclosure control opens a second row containing its rendered specification text. Hiding the text preserves the main row. The linked name opens that anchor’s own page, independently of expanding or collapsing the text.

Read in specification context

Implementation and test status are computed independently from their declared entries: ordinary entries display Implemented, todo entries display TODO, and not_applicable entries display N/A. Mixed statuses remain visible, including outstanding TODOs when another entry is implemented. An absent implementation or test entry is a validation error, not an implicit TODO or N/A. These labels describe declared coverage; recorded run results remain separate evidence.

Read in specification context

An RFD branch contains both the design record and the proposed normative Design changes. The RFD records motivation, alternatives, goals, and a high-level overview of the required changes, with links to the affected Design pages and anchors. Its implementation plan develops that overview into stages. Acceptance merges the record and specification changes together; unfinished implementation or tests remain explicit TODO entries. Subsequent implementation replaces those entries with code and evidence. Completing an RFD does not require copying its rules into Design, because the normative changes were already expressed there.

Read in specification context

.sage sources reside within the book’s configured source directory and each is rendered as a Design chapter. Design contains a Crates chapter listing the modeled crates. Each crate has an overview chapter showing its purpose, dependencies, and modules, with its remaining .sage source chapters nested beneath it. These chapters present the design/crates/ source tree using the architecture browser specified below. Each source has one chapter in the shared inventory; rendering does not create a second canonical copy. Rendering requires no hand-maintained Markdown copies of .sage sources and the built book works without a running Sage server.

Read in specification context

The specification-book system is itself specified by anchors in Design. Its rules participate in the same naming, reference validation, implementation and test coverage, status reporting, index, and anchor-page generation as all other rules. A rule about the validator or renderer receives no exemption from those requirements; unfinished work uses explicit TODO entries.

Read in specification context

Book generation and sage-meta check consume the same resolved Design chapter inventory, rule identities, source provenance, and correspondence data. Plugins that contribute specification chapters participate in that inventory. A source chapter omitted from the intended Design inventory is diagnosed rather than silently checked but unpublished or published but unchecked. Generated copies of rule text are not re-indexed as new definitions. The CLI, CI, and workspace test apply the shared validation to the book system’s own rules too.

Read in specification context

The Design overview contains Meta, Tenets, Anchors, Crates, and RFDs. Meta specifies the specification system itself. Tenets explains design principles without defining specification anchors. Anchors is generated from all active specification rules. Crates combines a handwritten reading map and modeled crate chapters. RFDs record changes and reasoning without defining active rules. The User’s Guide provides non-normative usage instructions.

Read in specification context

Every annotated source invocation is checked, including query cache hits and same-operation recursion. A Salsa request and its execution represent one architectural invocation. Internal validation, dependency reexecution, and accumulator traversal remain distinguishable from source requests; reexecution establishes the executing operation’s context without attributing its work to the suspended caller or inventing a source call.

Verification covers cold, reused, validated, invalidated/reexecuted, recursive, cancelled, and panicking runs, calls through generated query APIs, and an unannotated query beneath an annotated caller. Hand-reviewed traversals identify the architectural operations, Rust declaration sites, parentage, and cache outcomes. A warm forbidden request must fail even when its body does not execute.

Read in specification context

Every Sage correspondence unit has one or more Rust locations declared through #[sage::item(...)]. Every such annotation resolves to a compatible Sage unit in its containing modeled crate. Crate and module headers, named declarations, and explicit methods are correspondence units. Multiple source locations are permitted; module markers provide source coverage but do not establish runtime execution coverage. Cargo package and target metadata determine Rust ownership.

Verification exercises missing locations, dangling annotations, wrong crates, incompatible operation kinds, multiple sites, abstract markers, Cargo library and binary roots, and declarations produced by supported generators. Arbitrary macro tokens do not establish a generated declaration’s existence.

Read in specification context

Incomplete observation cannot establish conformance. Unmapped requests, unsupported receiver checks, and uninstrumented effects remain explicit gaps. Strict acceptance requires complete checking of the declared scope, as well as absence of violations. Diagnostics identify the checking scenario, relevant model rule when one exists, and observed call path; an unknown mapping is not silently attributed to the caller.

Verification injects each gap into an otherwise passing scenario and requires an incomplete or failing result, including cached requests and unsupported async boundaries. A call-only report does not claim that input reads, context construction, ordinary uninstrumented helpers, or task propagation were checked.

Read in specification context

A checking session uses one immutable, validated contract model and its source correspondence index. Every event refers to that same snapshot. Enabled enforcement fails if its model is missing or invalid, or if the indexed Rust source cannot be paired with the running binary. Loading is cached for the session; source edits take effect only in a subsequent session.

Verification exercises cached loads, parallel first use, explicit model roots, missing and invalid files, source/build mismatch rejection, and a subsequent session seeing model edits. Independently configured fixture sessions can use different models without modifying an active session.

Read in specification context

Every observed architectural call must be permitted by its caller’s resolved dependency envelope. An undeclared call is an error, including recursive entry into the same operation and requests satisfied from a query cache.

Read in specification context

An observed operation must not violate a prohibition of any active ancestor, even when its immediate caller permits the call. A violation is an error and retains the prohibition and complete call path.

Read in specification context

A concrete class must implement every inherited abstract method.

Read in specification context

An overriding method must preserve the inherited method’s operation kind and resolved result type.

Read in specification context

A class or context declaration has at most one extends base.

Read in specification context

Contexts are a distinct declaration kind and may inherit only from contexts. An ordinary or abstract class cannot inherit from a context.

Read in specification context

invokes crate::module::Class::method(); permits a call on any instance of the named class or a known subclass. This permission does not require equality with the caller’s receiver.

Read in specification context

creates name: crate::module::Context; declares a fresh owned working context under the given binding name. Its target must resolve to a context declaration. This describes context creation; validation does not perform the allocation.

Read in specification context

Each invocation clause grants a direct dependency. Transitive reachability is derived from those direct edges and does not grant the caller permission to invoke an indirect dependency directly.

Read in specification context

An empty envelope describes a leaf operation with no modeled dependencies. It is distinct from an abstract method, which has no declared envelope.

Read in specification context

Declared calls are permissions: none must occur, and calls may occur in an order different from the order of their envelope clauses.

Read in specification context

reads self.field; permits reading a field declared on this receiver’s class or inherited from a base. Unknown fields and non-self field paths are errors.

Read in specification context

invokes self.method(); permits a call on the current semantic receiver. A matching method on a different receiver does not satisfy that permission.

Read in specification context

A state field is valid only in a context declaration.

Read in specification context

Fields retain their declared identity, input, or state kind, distinguishing identity from changing inputs and local working state.

Read in specification context

Methods retain their declared operation kind: query or fn. Resolving a method’s contract preserves that distinction.

Queries describe memoized semantic products; functions describe ordinary computation. These annotations document boundaries; the model has no evaluator or cache.

Read in specification context

Every method body begins with a triple-quoted description, followed by its envelope or abstract; declaration. The description is retained as prose; method-like text within it adds no dependency permissions.

Read in specification context

forbid transitive crate::module::Class::method; prohibits reaching its target over any permitted nonempty call path. A rejected path identifies the offending method sequence.

Read in specification context

An overriding implementation inherits the prohibitions of the base method.

Prohibitions record design intent even when the permitted graph already excludes the target. Adding a permitted edge must still fail validation if it creates a forbidden path.

Read in specification context

The checker resolves declared calls conservatively, including every known overriding implementation in the supplied model.

Read in specification context

Each named type application must supply exactly the declared number of type arguments. This applies to opaque types, built-in types, parameters, and nested applications; a type parameter takes zero arguments.

Read in specification context

A struct or enum can carry triple-quoted prose immediately inside its opening brace. The parsed declaration retains that text; omitting it is permitted.

Read in specification context

An enum contains named variants in source order. A variant can have no payload, an ordered tuple payload, or named, typed fields. These three shapes remain distinct, including when a tuple or named payload is empty.

Read in specification context

A named field can carry triple-quoted prose immediately before its name. The parsed field retains that text independently of the containing declaration or variant’s prose. At the start of a body, the first prose string describes the container; a description for its first field follows as a second string.

Read in specification context

Structs, enums, and opaque types can declare a nonempty comma-separated list of type parameters in angle brackets. Parameters are available throughout their own declaration and do not become names in other declarations.

Read in specification context

Adjacent named fields, enum variants, and tuple payload elements require a comma separator. A trailing comma before the closing delimiter is optional.

For example:

type Binder<T> {
    """A value under the generic parameters binding its references."""
}

struct Items {
    items: Vec<crate::symbols::Symbol>,
}

enum MethodReceiver {
    Value { mutable_binding: bool },
    Ref {
        """A borrowed receiver with the declared mutability."""
        mutability: Mutability,
    },
}

Read in specification context

An unqualified type name resolves first to a parameter of its declaration, then to a type, class, or context in the same module, then to the built-in prelude. An earlier match shadows a later one.

Read in specification context

An opaque type declares a name and any type parameters without fields or variants. It requires triple-quoted descriptive prose, either inside braces or before a terminating semicolon. A payload inside its body is an error.

Read in specification context

The built-in prelude contains Vec<T>, Option<T>, bool, u32, u64, and String. These names are available without declaring them in the model.

Read in specification context

A type outside the current module requires a crate:: or $cratename:: qualified path. Cross-crate type references require a declared dependency; unqualified lookup does not search other modules or the crate root.

Read in specification context

Semantic value types can refer directly to themselves or to each other, without Box or another storage indirection. Such recursion is not a validation error.

Read in specification context

A struct contains named, typed fields. The parsed declaration retains their names, types, and source order; an empty struct is permitted.

Read in specification context

Parentheses always denote a tuple, including () and a single element with or without a trailing comma. (T) is distinct from T when result types are compared for an override.

Read in specification context

Type expressions are named types with optional generic arguments, or tuples. Generic arguments and tuple elements are themselves type expressions, allowing arbitrary nesting. The parsed expression retains that nesting.

Read in specification context

Named fields have distinct names within a struct or a single enum variant. Different declarations and different variants may reuse field names.

Read in specification context

A value declaration cannot repeat a type parameter’s name.

Read in specification context

Variants have distinct names within an enum. Different enums may reuse a variant name.

Read in specification context

Every type name in a value field, variant payload, class or context field, or method result must resolve. An unknown name is an error even when nested in generic arguments or tuples.

Read in specification context

A variant can carry triple-quoted prose immediately inside its payload’s opening delimiter, or immediately after a unit variant’s name. The parsed variant retains that text independently of other variants.

Read in specification context

An anchor’s review text is the complete source content selected by the anchor-content boundaries, with surrounding whitespace removed. For .sage prose, its enclosing common indentation is removed first; remaining internal whitespace and Markdown markup are preserved. The saved input covers the same content that the generated anchor views present as the claim, including any paragraphs, lists, or examples within its extent.

Read in specification context

One review covers one anchor’s claim and its complete set of associated tests. The input records every eligible test associated with that anchor in a deterministic order. Several tests may cover different parts of a claim; each test need not establish the whole claim independently.

Read in specification context

An empty requested_edits list in a completed report means all aspects of the anchor are accounted for and no edits are required. A nonempty list means work remains and the validation cannot satisfy the gate. The reviewer must request edits for missing implementation or test coverage unless explicit TODO/N/A evidence adequately explains the gap.

Ordinary, todo, and not_applicable statuses are derived from the associated implementation and test entries. The report assesses all entries and their explanations. Accepting a justified deferral or inapplicability does not relabel it as implemented behavior; TODO/N/A remains visible in the evidence. An unfinished review has no completed output and cannot satisfy the gate, even if a draft edit list is empty.

Read in specification context

The complete association set and its metadata remain checked separately from fragment contents. Adding, removing, or changing an association invalidates the review even when all saved fragments still resolve to unchanged text.

Read in specification context

Each fragment records its workspace-relative source path, selector, and exact selected contents. Contents are stored as source lines; joining them with newline characters recovers the selected text, including its whitespace and line endings. The data model is defined below in Rust notation, without prescribing a JSON encoding:

struct InputFragment {
    path: String,           // Workspace-relative UTF-8 source file path.
    selector: Selector,
    contents: Vec<String>, // Join with '\n' to recover the selected text.
}

enum Selector {
    WholeFile,
    LineRange { start: usize, end: usize },
    Claim { anchor_id: String },
    Test {
        crate_name: String,
        target: String,
        rust_path: String,
    },
}

Read in specification context

Recording and checking resolve every fragment’s selector against current source and compare the selected text with the saved text using exact string equality. A missing or ambiguous selection, invalid selector, or changed selected text makes the validation stale or invalid. No selector kind or input origin bypasses these checks.

Read in specification context

The shared cargo meta check fails when any current specification anchor lacks an up-to-date validation satisfying meta.reviews.staleness, with an output satisfying meta.reviews.output_format and no requested edits under meta.reviews.decisions. It loads all validation directories, checks the layout and summary metadata, and compares the saved inputs with current source. At least one test and implementation entry are required.

A validation for an anchor ID absent from the current specification also fails the gate, even when every current anchor has a passing validation. Diagnostics name that directory and direct the reviewer to remove obsolete records or reconcile renamed anchors and start fresh validation. Checking and recording do not silently delete stale anchor IDs. Invalid record formats, unsupported schema/policy versions, and incomplete records fail the gate. CI and workspace Cargo tests use this same gate; checking never creates approvals.

Read in specification context

The input contains these fields:

The following anchors define each part. Source text belongs in the uniform fragment collection; association metadata identifies the evidence and its declared status. The collection contains both initial context and later reads.

Read in specification context

Every piece of source context supplied to or consulted by a validation agent is recorded in one uniform collection of input fragments, whether prepared automatically, supplied by a coordinator, or declared by the reviewer. Helpers and surrounding context used during review are additional fragments; recording only the initial claim and tests does not excuse omitting other context used. Automatic preparation and recorded reads use the same fragment representation and freshness checks. Reviewers are responsible for declaring every source dependency used in their assessment.

Read in specification context

The output contains only the reviewer, report, and requested edits:

struct ValidationOutput {
    reviewer: String,
    report: String,
    requested_edits: Vec<String>,
}

reviewer is a nonblank reviewer identity. report is a nonblank, complete, claim-specific explanation accounting for every requirement, implementation evidence, and test adequacy. It distinguishes source inspection from commands actually executed. The report is the agent’s supplied explanation, not a recording of internal reasoning. Each requested edit is a concrete, nonblank change needed before revalidation.

Read in specification context

Starting a review validates the requested anchor against the current inventory, then clears any existing validation for that anchor and sets up validations/<anchor>/. It writes summary.json and the initial input.json before printing the exact captured inputs and verification prompt for the agent to consume. The initial inputs include the complete claim, associated tests, implementation context, and association metadata defined by meta.reviews.input_format. Additional coordinator instructions supplied to the reviewer are captured under meta.reviews.review_instructions.

Starting removes the previous output. After a successful start, the validation directory must be in a state that makes cargo meta check and the shared Cargo validation test fail for that anchor, even if its previous validation passed and its source is unchanged. An interrupted or abandoned review therefore cannot fall back to an older approval. Unknown or invalid anchor IDs are rejected before clearing any record. Other anchors’ directories are unchanged. A failed start cannot leave an older output appearing to validate newly captured inputs.

Read in specification context

For every anchor requiring re-evaluation, cargo meta check and the shared Cargo validation test must fail until the assigned review subagent successfully runs cargo meta review record for that review. Starting a review, capturing inputs, reading additional context, or drafting a report cannot satisfy the gate. An interrupted, abandoned, or failed review remains failing; an older report cannot stand in for the unfinished review.

Recording is necessary but not sufficient: the recorded report must be complete, request no edits, and still match current inputs. Recording a report that requests edits, or changing inputs after recording, leaves the gate failing. Every required anchor must meet these conditions independently.

Read in specification context

The recorded-read command takes an anchor with an active review directory, a workspace-relative source path, and a selector from meta.reviews.fragment_format. A read without an explicit selector selects the whole file. It appends the selected contents and selector directly to that anchor’s input.json before returning those same contents to the reviewer. Repeated reads are retained in order. Reads outside the workspace, invalid selections, and reads without an active unfinished review are rejected. These fragments participate in the same freshness checks as the initial inputs.

Reviewers declare every additional source dependency through this command and are responsible for the completeness of those declarations.

Read in specification context

Recording takes a completed report in the format defined by meta.reviews.output_format and an anchor with an active unfinished review. It checks the inputs already stored in that anchor’s directory against current source using meta.reviews.fragment_freshness and meta.reviews.fragment_associations, and verifies the anchor and version metadata. Missing or stale inputs, an unknown anchor, an invalid report, or an absent active review rejects recording. A changed input requires a new review starting with cargo meta review start; recording never substitutes new source text for the inputs the agent actually reviewed.

On success, recording writes output.json and updates the summary’s recording time, preserving input.json exactly. Other anchors’ records are unchanged. A completed report requesting edits is saved but cannot satisfy the gate under meta.reviews.decisions. Incomplete publication cannot satisfy the gate; readers must not accept a mixture of files from different review attempts.

Read in specification context

The repository’s sage-review-checklist skill instructs the main agent to start one review subagent for each anchor requiring re-evaluation. Each subagent is given the anchor ID and an initial prompt directing it to run cargo meta review start <anchor> and evaluate the printed inputs. The main agent supplies any extra instructions or source context as recorded review inputs.

The subagent uses cargo meta review read for additional source context and cargo meta review record to save its completed report. Only one subagent owns an anchor’s active directory at a time; reviews for different anchors may run in parallel. The main agent reconciles requested edits, coordinates changes, and repeats the start/read/record cycle for affected anchors after edits, then runs cargo meta check again. TODO/N/A evidence is reviewed under the same workflow.

Read in specification context

CLI and Cargo-test failures identify every anchor requiring re-evaluation and explain why: missing or unfinished validation, changed inputs or associations, unsupported versions, malformed records, or requested edits. Changed-input diagnostics identify the affected fragment or association. Failures direct the main agent to invoke .agents/skills/sage-review-checklist/SKILL.md; they do not start reviews or alter saved records themselves.

Read in specification context

Review inputs preserve the exact verification prompt and any additional coordinator instructions supplied to the reviewer. These instructions are part of the recorded context even when they do not originate in a source file.

Read in specification context

One review judges both implementation completeness and test adequacy against an anchor’s complete claim. Its saved input includes every implementation association’s crate, target, module, file, cfg conditions, excerpt, region flag, placeholder status, and explanation, in deterministic order. Source line numbers and byte offsets are not association metadata. Source context used to assess these associations is recorded under meta.reviews.input_fragments. A point marker’s five-line preview is navigation context, not a sufficient boundary for reviewing behavior that depends on other code.

Reviewers follow relevant helpers and dependencies and record the source fragments they use. They add implementation associations for essential code in other files before approval. Reviews are source judgments, not proofs; test execution remains separate evidence.

Read in specification context

Selector::Claim { anchor_id } selects the complete claim identified by its full dotted anchor ID within the fragment’s source file, using the shared anchor-content boundaries and claim-text normalization. The containing document need not be included. The selector stores no line numbers or byte offsets; inserting unrelated lines before an unchanged claim does not make the fragment stale.

Read in specification context

Selector::LineRange { start, end } selects a one-based, inclusive range of lines within the fragment’s source file. Lines are delimited by \n; selected text retains the original line endings, including the last selected line’s ending if present. Zero, reversed, or out-of-bounds ranges are invalid. The saved line numbers are used again when checking freshness, so shifting content across those boundaries may conservatively make the fragment stale.

Read in specification context

Selector::Test { crate_name, target, rust_path } selects the complete annotated Rust test function within the fragment’s source file, including attributes, signature, body, and comments. crate_name identifies the Cargo package; target uses the correspondence target identity, including kind and name (for example lib:sage_meta or test:review); rust_path identifies the fully qualified function within that target. Identically named functions in different targets are distinct. The containing file need not be included. The selector stores no line numbers or byte offsets; inserting unrelated lines before an unchanged test does not make the fragment stale.

Read in specification context

Selector::WholeFile selects all contents of the fragment’s source file, including any trailing newline. It carries no additional selector data.

Read in specification context

Claim, implementation, and annotated test source snapshots are stored in input.json as arrays of source lines. Joining an array with newline characters recovers the snapshot’s text, including internal blank lines, whitespace, and markup.

Read in specification context

A saved review applies only when its anchor, schema version, review-policy version, complete claim, and implementation and test inputs match the current inventory. Source context must satisfy meta.reviews.fragment_freshness and associations must satisfy meta.reviews.fragment_associations. Unchanged claims and tests remain reusable when unrelated edits move them, as specified by their selectors. Changed text within a whole-file fragment, including blank-line changes, invalidates that fragment. A reusable review must also have a complete output under meta.reviews.output_format and no requested edits under meta.reviews.decisions.

Read in specification context

The summary contains these fields:

Freshness is determined by comparing the recorded inputs with current source, as defined by meta.reviews.fragment_freshness.

Read in specification context

Each associated test’s review input contains the complete annotated Rust function source, including its attributes, signature, body, and contained comments. It also records the Cargo crate and target, Rust path, file path, inherited configuration conditions, and ordinary, todo, or not_applicable status. Source line numbers and byte offsets are excluded from the input.

Read in specification context

Each anchor has one directory named by its complete dotted ID, for example:

validations/meta.reviews.gate/
    summary.json
    input.json
    output.json

summary.json identifies the review; input.json contains the context captured for it; output.json contains the completed assessment. cargo meta review start creates or resets the directory and writes the first two files. Until recording completes, output.json is absent and the validation cannot satisfy the gate. The directory name must be a valid anchor ID and match summary.json. Starting a new review discards the previous validation; earlier validations are not retained.

Read in specification context

Evidence is attached to one architectural claim. A statement that a behavior is established identifies evidence exercising that particular behavior, while a negative or partial artifact may pin a known limitation. A passing aggregate suite is not evidence for an unstated local guarantee.

Verification scenarios: Documentation review checks every implemented capability against a focused test, snapshot, normalized trace, edit experiment, exact oracle result, inspector scenario, or source anchor whose asserted behavior matches the claim.

Read in specification context

Human inspection and exact conformance remain independent. Readable Sage-only views explain semantic values and incremental work; the Oracle independently decides compatibility from Sage and rustc emissions. Neither facility consumes the other’s output to repair or reinterpret a result.

Verification scenarios: Architecture and dependency tests keep inspector adapters out of oracle comparison and rustc-oracle values out of inspector rendering, while one pinned slice supplies both independently produced forms of evidence.

Read in specification context

A review packet connects result, dependency, edit, and code evidence. For one semantic target, the packet identifies the Rust input, readable result, diagnostic/completeness outcome, cold and warm dependencies, relevant or unrelated edit behavior, focused or oracle verification, and anchored implementation entry points.

Verification scenarios: Each designated review packet contains or links all seven elements, and its reproduction commands regenerate the checked-in artifacts without relying on unrecorded setup.

Read in specification context