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