crates.sage_stash.storage.immutable_entries

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 · design/crates/sage_stash/storage.sage

Implementation

Implemented crates/sage-ir/src/check/finalize.rs:24–29

sage_ir::check::finalize · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_stash.storage.immutable_entries`
pub(super) fn finalize_typed_body<'db>(
    source: &Stash,
    egraph: &VersionedEGraph<'db>,
    root: Ptr<TyExpr<'db>>,
    expr_slots: &[Ptr<TyExpr<'db>>],

}

See more source ↗

Implemented crates/sage-ir/src/check/infer/egraph.rs:306–311

sage_ir::check::infer::egraph · lib:sage_ir

#![allow(unused)]
fn main() {
    // {anchor}`crates.sage_stash.storage.immutable_entries`
    pub fn find(&self, version: Version, mut ty: Ptr<Ty<'db>>) -> Ptr<Ty<'db>> {
        self.versions.assert_live(version);
        loop {
            let parent = self.get_parent(version, ty);
            if parent == ty {

}

See more source ↗

Implemented crates/sage-stash/src/lib.rs:872–877

sage_stash · lib:sage_stash

#![allow(unused)]
fn main() {
    // {anchor}`crates.sage_stash.storage.immutable_entries`
    pub fn alloc<'db, T: AllocStashData<'db>>(&mut self, value: T) -> Ptr<T> {
        let type_id = TypeId::of::<T::StaticSelf>();
        let mut hasher = InternHasher::new();
        value.stash_hash(self, &mut hasher);
        let content_hash = hasher.finish();

}

See more source ↗

Tests and review

Indexed tests and the implementation-completeness and test-adequacy review; no test run is implied.

Implemented sage_ir::check::finalize::tests::finalized_nested_body_owns_resolved_and_imported_types_after_sources_drop

crates/sage-ir/src/check/finalize.rs · lib:sage_ir

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_stash.storage.handle_ownership)]
    #[sage::test(crates.sage_stash.storage.immutable_entries)]
    #[sage::test(crates.sage_ir.types.body.no_inference)]
    fn finalized_nested_body_owns_resolved_and_imported_types_after_sources_drop() {
        use crate::cst::expr::Literal;

        let mut imported_stash = Stash::new();
        let imported_bool = imported_stash.alloc(Ty::Bool);
        let imported = Stashed::new(imported_stash, imported_bool);
        let mut source = Stash::new();
        source.alloc(123_u64);
        let boolean = imported.copy_into(&mut source);
        let mut egraph = VersionedEGraph::new();
        let variable = egraph.alloc_var(Version::ROOT, Universe::ROOT);
        let inference = source.alloc(Ty::InferVar(variable));
        try_unify(&mut egraph, &mut source, Version::ROOT, inference, boolean).unwrap();
        let span = RelativeSpan { start: 0, end: 4 };
        let child = source.alloc(TyExpr {
            data: TyExprData::Literal(Literal::Bool(true)),
            ty: inference,
            span,
        });
        let pending = source.alloc(TyExpr {
            data: TyExprData::Unresolved(ExprSlot(0)),
            ty: inference,
            span,
        });
        let elements = source.alloc_slice(&[pending, child]);
        let types = source.alloc_slice(&[inference, boolean]);
        let tuple = source.alloc(Ty::Tuple(types));
        let root = source.alloc(TyExpr {
            data: TyExprData::Tuple(elements),
            ty: tuple,
            span,
        });
        let completed = finalize_typed_body(&source, &egraph, root, &[child], &[], span);
        assert_eq!(source[inference], Ty::InferVar(variable));
        assert_eq!(source[types], [inference, boolean]);
        assert_eq!(source[elements], [pending, child]);
        assert_eq!(source[pending].data, TyExprData::Unresolved(ExprSlot(0)));
        assert_eq!(imported.root_deref(), Ty::Bool);
        drop(egraph);
        drop(source);
        drop(imported);

        let (
            target,
            TyBodyData {
                root,
                locals,
                span: completed_span,
            },
        ) = completed.open_deref();
        assert_eq!(completed_span, span);
        assert!(target[locals].is_empty());
        let TyExpr {
            data,
            ty,
            span: root_span,
        } = target[root];
        assert_eq!(root_span, span);
        let Ty::Tuple(types) = target[ty] else {
            panic!("expected tuple type")
        };
        assert_eq!(target[types].len(), 2);
        for ty in &target[types] {
            assert_eq!(target[*ty], Ty::Bool);
        }
        let TyExprData::Tuple(elements) = data else {
            panic!("expected tuple expression")
        };
        assert_eq!(target[elements].len(), 2);
        assert_eq!(target[elements][0], target[elements][1]);
        for child in &target[elements] {
            let TyExpr {
                data,
                ty,
                span: child_span,
            } = target[*child];
            assert_eq!(data, TyExprData::Literal(Literal::Bool(true)));
            assert_eq!(target[ty], Ty::Bool);
            assert_eq!(child_span, span);
        }
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_stash::appending_and_deduplicating_preserves_existing_entries

crates/sage-stash/tests/storage_contracts.rs · test:storage_contracts

#![allow(unused)]
fn main() {
#[test]
#[sage::test(crates.sage_stash.storage.immutable_entries)]
fn appending_and_deduplicating_preserves_existing_entries() {
    let mut stash = Stash::new();
    let value = stash.alloc(42_u32);
    let slice = stash.alloc_slice(&[1_u32, 2, 3]);
    for n in 0..4096_u64 {
        stash.alloc(n);
    }
    assert_eq!(stash[value], 42);
    assert_eq!(stash[slice], [1, 2, 3]);
    assert_eq!(value, stash.alloc(42_u32));
    assert_eq!(slice, stash.alloc_slice(&[1_u32, 2, 3]));
}
}

See more source ↗

Implemented sage_stash::safe_api_rejects_mutating_interned_scalars_and_slices

crates/sage-stash/tests/storage_contracts.rs · test:storage_contracts

#[test]
#[sage::test(crates.sage_stash.storage.immutable_entries)]
fn safe_api_rejects_mutating_interned_scalars_and_slices() {
    // Keep the rejected operations in the reviewed snapshot as well as the fixtures.
    assert_eq!(
        include_str!("ui/mutate_scalar.rs"),
        r#"use sage_stash::Stash;

fn main() {
    let mut stash = Stash::new();
    let value = stash.alloc(42_u32);
    stash[value] = 99;
}
"#
    );
    assert_eq!(
        include_str!("ui/mutate_slice.rs"),
        r#"use sage_stash::Stash;

fn main() {
    let mut stash = Stash::new();
    let values = stash.alloc_slice(&[1_u32, 2]);
    stash[values][0] = 99;
}
"#
    );
    let tests = trybuild::TestCases::new();
    tests.compile_fail("tests/ui/mutate_scalar.rs");
    tests.compile_fail("tests/ui/mutate_slice.rs");
}

See more source ↗

Review: Accepted · final_quality.

Reviewed all three implementation entries and all three complete associated tests for immutable_entries. Requirements are append-only allocation, no safe mutable access to interned scalar/slice entries, and finalization of transient inference by resolution/copy into fresh storage. Captured storage-guide and architectural rationale specify that mutable inference relationships live outside the stash.

sage-stash::alloc and alloc_slice compute typed/content/count keys, return the existing entry for equal content, or append via push_raw. push_raw pads and extends the byte buffer and appends entry metadata; it does not overwrite earlier entries. Buffer growth copies the existing byte prefix, and resize_zeroed explicitly requires nondecreasing length. append_one constructs a new value vector and interns it rather than modifying the original slice. The public indexing implementations return shared references only; no IndexMut or mutable entry accessor is exposed. Stashed also exposes shared storage views, so retained results cannot be edited through those APIs.

The associated egraph::find follows version-local parent maps under shared access. Mutating inference operations update separate egraph maps; they do not replace Ty::InferVar allocations in the source stash. finalize_typed_body takes shared source/egraph references, constructs a new target stash, resolves each source type via find and expression slots via the completion table, and recursively allocates rebuilt body nodes. Its source memoization tables and target allocations are separate; unresolved infer variables panic instead of mutating source nodes into a result. The inspected copy paths include type/alias/call arguments, expression/statement/pattern slices and fields. This is an ownership/immutability assessment, not a review of authored expression semantics.

appending_and_deduplicating_preserves_existing_entries checks an existing scalar and slice after 4096 additions, then verifies reinterning equal values returns the original handles. safe_api_rejects_mutating_interned_scalars_and_slices visibly pins both attempted assignments in its body, runs trybuild compile_fail on both fixtures, and captured .stderr files require E0594 because IndexMut is absent. Thus compiler rejection is the intended API evidence, not an accidental runtime failure. finalized_nested_body_owns_resolved_and_imported_types_after_sources_drop checks source inference node, type/child slices, pending expression slot and imported bool remain unchanged after finalization; after dropping all source/proof storage it walks the destination tuple and literal children and asserts resolved bool types, stable spans and shared completed children. Together the tests exercise append/dedup stability, inaccessible safe mutation, and fresh finalization without in-place rewriting. They do not constitute an exhaustive proof for arbitrary unsafe client implementations; the claim is the safe allocated-entry API contract.

No TODO/N/A entries are associated. No source edits or tests executed in this review; commands were fresh review start/read and source inspection before record. The captured UI fixtures and expected diagnostics were inspected, not rerun. No requested edits.

Browse crates anchors

139 anchors

Specification anchors and declared coverage
Anchor	Implementation	Tests
crates (139)	114 Implemented37 TODO2 N/A	74 Implemented107 TODO
crates.sage_inspector (15)	13 Implemented1 TODO2 N/A	3 Implemented15 TODO
crates.sage_inspector.inspection (15)	13 Implemented1 TODO2 N/A	3 Implemented15 TODO
`balanced_traces`	Implemented	TODO
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
`canonical_ownership`	Implemented	ImplementedTODO
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
`derive_reflection`	Implemented	ImplementedTODO
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
`detail_free_index`	Implemented	TODO
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
`deterministic_trace`	Implemented	TODO
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
`durable_navigation`	N/A	TODO
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
`generic_browser`	N/A	TODO
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
`owned_reflection`	Implemented	ImplementedTODO
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`	Implemented	TODO
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
`revision_and_demand`	Implemented	TODO
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_phase_boundary`	Implemented	TODO
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
`source_evidence`	Implemented	TODO
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
`typed_service`	Implemented	TODO
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`	ImplementedTODO	TODO
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
`workspace_actor`	Implemented	TODO
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
crates.sage_ir (90)	67 Implemented34 TODO	40 Implemented88 TODO
crates.sage_ir.checking (12)	12 Implemented3 TODO	5 Implemented12 TODO
crates.sage_ir.checking.body (5)	5 Implemented2 TODO	3 Implemented5 TODO
`elaboration`	Implemented	ImplementedTODO
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`	ImplementedTODO	TODO
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
`interface_dependencies`	Implemented	ImplementedTODO
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
`isolated_completion`	Implemented	ImplementedTODO
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
`operator_calls`	ImplementedTODO	TODO
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
`identity_minting`	Implemented	TODO
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
`owned_products`	Implemented	ImplementedTODO
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
crates.sage_ir.checking.signature (4)	4 Implemented1 TODO	1 Implemented4 TODO
`body_independence`	Implemented	TODO
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
`narrow_detail`	ImplementedTODO	TODO
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
`owner_binder`	Implemented	ImplementedTODO
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
`storage`	Implemented	TODO
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
`symbol_keyed_interfaces`	Implemented	TODO
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
crates.sage_ir.crate (9)	9 TODO	9 TODO
`explicit_restrictions`	TODO	TODO
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
`identity_before_detail`	TODO	TODO
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_evidence`	TODO	TODO
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
`narrow_demands`	TODO	TODO
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_invalidation`	TODO	TODO
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
`represented_completeness`	TODO	TODO
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
`restrictions_and_gaps`	TODO	TODO
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
`semantic_query_boundaries`	TODO	TODO
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
`terminal_incompleteness`	TODO	TODO
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
crates.sage_ir.inference (8)	8 Implemented	6 Implemented8 TODO
`atomic_checking`	Implemented	ImplementedTODO
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
`body_local_quiescence`	Implemented	ImplementedTODO
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
`canonical_boundary`	Implemented	ImplementedTODO
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
`completed_body_boundary`	Implemented	TODO
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
`numeric_domains`	Implemented	ImplementedTODO
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_and_coercion`	Implemented	ImplementedTODO
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
`terminal_obligations`	Implemented	TODO
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
`transaction_isolation`	Implemented	ImplementedTODO
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
crates.sage_ir.metadata (4)	4 Implemented1 TODO	4 TODO
`explicit_incompleteness`	Implemented	TODO
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
`keyed_reuse`	ImplementedTODO	TODO
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
`product_boundaries`	Implemented	TODO
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
`provider_authority`	Implemented	TODO
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
crates.sage_ir.modules (8)	7 Implemented1 TODO	4 Implemented8 TODO
crates.sage_ir.modules.expand (4)	4 Implemented	2 Implemented4 TODO
`completeness`	Implemented	ImplementedTODO
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
`dependencies`	Implemented	TODO
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
`direct_members`	Implemented	TODO
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
`recursion_and_fixpoint`	Implemented	ImplementedTODO
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
crates.sage_ir.modules.parse (4)	3 Implemented1 TODO	2 Implemented4 TODO
`dependencies`	Implemented	TODO
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
`detail_firewall`	Implemented	ImplementedTODO
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
`recovery_completeness`	TODO	TODO
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
`syntax_identities`	Implemented	ImplementedTODO
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
crates.sage_ir.resolution (5)	5 Implemented1 TODO	3 Implemented4 TODO
crates.sage_ir.resolution.lookup (5)	5 Implemented1 TODO	3 Implemented4 TODO
`completeness`	ImplementedTODO	ImplementedTODO
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
`dependencies`	Implemented	TODO
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_import_ambiguity`	Implemented	Implemented
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
`identity_only`	Implemented	TODO
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
`precedence`	Implemented	ImplementedTODO
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
crates.sage_ir.solver (9)	7 Implemented7 TODO	5 Implemented9 TODO
`alternative_isolation`	ImplementedTODO	ImplementedTODO
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
`bounded_completeness`	ImplementedTODO	TODO
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_completeness`	Implemented	TODO
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
`canonical_cycles`	TODO	TODO
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
`canonical_outputs`	Implemented	ImplementedTODO
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
`local_index_firewall`	TODO	TODO
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
`normalization_demand`	ImplementedTODO	ImplementedTODO
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
`schedule_independence`	ImplementedTODO	ImplementedTODO
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
`shared_final_result`	ImplementedTODO	ImplementedTODO
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
crates.sage_ir.symbols (8)	8 Implemented	4 Implemented7 TODO
`associated_identity`	Implemented	Implemented
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
`associated_interfaces`	Implemented	TODO
Checking an associated signature reuses its owner interface and never reads a sibling associated body. Read in specification context
`body_interfaces`	Implemented	ImplementedTODO
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
`definition_identity`	Implemented	TODO
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
`external_fact_queries`	Implemented	TODO
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
`external_identity`	Implemented	TODO
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
`kind_wrappers`	Implemented	ImplementedTODO
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
`local_identity`	Implemented	ImplementedTODO
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
crates.sage_ir.types (27)	16 Implemented12 TODO	13 Implemented27 TODO
crates.sage_ir.types.aliases (2)	1 Implemented1 TODO	1 Implemented2 TODO
`identity`	Implemented	ImplementedTODO
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
`revelation`	TODO	TODO
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
crates.sage_ir.types.binder (1)	1 Implemented1 TODO	1 Implemented1 TODO
`owner_parameters`	ImplementedTODO	ImplementedTODO
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
crates.sage_ir.types.body (13)	4 Implemented9 TODO	3 Implemented13 TODO
`await`	TODO	TODO
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
`closures`	TODO	TODO
A completed closure has a typed nested body with explicit parameters and captures. Read in specification context
`conditional_patterns`	TODO	TODO
If-let, while-let, and let chains lower into structured match and control-flow forms. Read in specification context
`coroutines`	TODO	TODO
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
`diagnosed_recovery`	Implemented	ImplementedTODO
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
`elaborated`	TODO	ImplementedTODO
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
`for_iteration`	TODO	TODO
A for expression lowers into an IntoIterator call followed by a structured loop and match. Read in specification context
`indexing`	TODO	TODO
Index syntax lowers to a resolved Index or IndexMut call with typed operands. Read in specification context
`macro_expansion`	TODO	TODO
A checked expression represents its macro expansion output; a macro invocation is not itself a successful checked expression node. Read in specification context
`no_inference`	Implemented	ImplementedTODO
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
`resolved_references`	Implemented	TODO
Every path, field, variant, function, and associated-item reference in a successful completed body records its resolved definition identity. Read in specification context
`try_residual`	TODO	TODO
The question-mark operator lowers into a Try::branch call, a ControlFlow match, and a FromResidual call. Read in specification context
`typed_provenance`	Implemented	TODO
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
crates.sage_ir.types.calls (2)	1 Implemented1 TODO	1 Implemented2 TODO
`dispatch_families`	TODO	TODO
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
`selected_semantics`	Implemented	ImplementedTODO
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
crates.sage_ir.types.lifetimes (2)	2 Implemented	2 Implemented2 TODO
`dummy`	Implemented	ImplementedTODO
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
`unchecked_borrows`	Implemented	ImplementedTODO
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
crates.sage_ir.types.operators (2)	2 Implemented	1 Implemented2 TODO
`lazy_control_flow`	Implemented	TODO
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
`trait_calls`	Implemented	ImplementedTODO
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
`scoped_identities`	Implemented	TODO
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
crates.sage_ir.types.spans (4)	4 Implemented	4 Implemented4 TODO
`generated_identity`	Implemented	ImplementedTODO
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
`item_origin`	Implemented	ImplementedTODO
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
`offset_reuse`	Implemented	ImplementedTODO
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
`relative_composition`	Implemented	ImplementedTODO
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
crates.sage_oracle_harness (4)	4 Implemented2 TODO	1 Implemented4 TODO
crates.sage_oracle_harness.crate (4)	4 Implemented2 TODO	1 Implemented4 TODO
`deterministic_emission`	Implemented	TODO
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
`exact_comparison`	ImplementedTODO	ImplementedTODO
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
`fixed_projection`	Implemented	TODO
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
`independent_coverage`	ImplementedTODO	TODO
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
crates.sage_stash (5)	5 Implemented	5 Implemented
crates.sage_stash.storage (5)	5 Implemented	5 Implemented
`handle_ownership`	Implemented	Implemented
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
`immutable_entries`	Implemented	Implemented
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
`query_value`	Implemented	Implemented
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
`rooted_equality`	Implemented	Implemented
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
`typed_interning`	Implemented	Implemented
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
crates.sage_test_harness (25)	25 Implemented	25 Implemented
crates.sage_test_harness.compile_tests (25)	25 Implemented	25 Implemented
`annotation_validation`	Implemented	Implemented
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
`blessing_gate`	Implemented	Implemented
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
`callsite_updates`	Implemented	Implemented
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
`checking_scope`	Implemented	Implemented
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
`compiler_conditions`	Implemented	Implemented
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
`completed_types`	Implemented	Implemented
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
`coordinates`	Implemented	Implemented
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
`dependencies`	Implemented	Implemented
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
`diagnostic_counts`	Implemented	Implemented
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_locations`	Implemented	Implemented
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
`edition`	Implemented	Implemented
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
`fixtures`	Implemented	Implemented
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
`grouped_observations`	Implemented	Implemented
`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
`invocation`	Implemented	Implemented
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
`production_execution`	Implemented	Implemented
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
`project_isolation`	Implemented	Implemented
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
`query_capture`	Implemented	Implemented
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_projection`	Implemented	Implemented
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
`rendering`	Implemented	Implemented
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
`resolved_symbols`	Implemented	Implemented
`//# 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
`review_visibility`	Implemented	Implemented
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
`rustc_execution`	Implemented	Implemented
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_lints`	Implemented	Implemented
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
`starting_expressions`	Implemented	Implemented
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
`target_line`	Implemented	Implemented
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

Symposiun AGentic Environment (SAGE)

crates.sage_stash.storage.immutable_entries

Implementation

Tests and review