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