crates.sage_ir.solver.normalization_demand

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 · design/crates/sage_ir/solver.sage

Implementation

Implemented crates/sage-ir/src/check/solve/clauses.rs:341–346

sage_ir::check::solve::clauses · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.normalization_demand`
pub(crate) fn load_prepared_associated_value<'db>(
    db: &'db dyn crate::Db,
    state: &mut QueryProofState<'db>,
    candidate: &PreparedValueCandidate<'db>,
    associated_ty: crate::symbol::TypeAliasSymbol<'db>,

}

See more source ↗

Implemented crates/sage-ir/src/check/solve/prove.rs:411–416

sage_ir::check::solve::prove · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.normalization_demand`
// {anchor}`crates.sage_ir.solver.bounded_completeness`
// {anchor}`crates.sage_ir.solver.shared_final_result`
pub(crate) fn solve_query<'db>(
    db: &'db dyn crate::Db,
    query: &Stashed<GoalQueryData<'db>>,

}

See more source ↗

Implemented crates/sage-ir/src/local_syms/impls.rs:41–46

sage_ir::local_syms::impls · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.normalization_demand`
pub fn local_impl_associated_type_value<'db>(
    db: &'db dyn crate::Db,
    impl_sym: LocalImplSym<'db>,
    associated_ty: crate::symbol::TypeAliasSymbol<'db>,
) -> Option<sage_stash::Stashed<crate::ty::Binder<'db, sage_stash::Ptr<crate::ty::Ty<'db>>>>> {

}

See more source ↗

TODO crates/sage-meta/tests/semantic_spec.rs:106–111

sage_meta::todo · test:semantic_spec

TODO: Named alias expansion and opaque reveal context remain unsupported. Local discovery still scans unrelated impl identities; excluding those reads requires the tracked private index deferred by crates.sage_ir.solver.local_index_firewall.

#![allow(unused)]
fn main() {
    // {anchor}`crates.sage_ir.solver.normalization_demand`
    // TODO: Named alias expansion and opaque reveal context remain unsupported.
    // Local discovery still scans unrelated impl identities; excluding those reads requires
    // the tracked private index deferred by crates.sage_ir.solver.local_index_firewall.
    #[test]
    #[sage::test(crates.sage_ir.solver.normalization_demand)]

}

See more source ↗

Tests and review

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

TODO sage_meta::todo::solver_normalization_demand

crates/sage-meta/tests/semantic_spec.rs · test:semantic_spec

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.normalization_demand)]
    fn solver_normalization_demand() {
        // TODO: Complete the claim-specific verification matrix:
        // Named, associated, and opaque aliases survive folding and canonical round trips with reveal
        // context intact; inside/outside opaque tests produce the appropriate different result; query
        // traces for one projection include only relevant headers and its requested value and exclude
        // sibling associated values, unrelated impls, and every body.
    }
}

See more source ↗

Implemented sage_test_harness::trait_solver_proof_tests::local_normalization_reads_one_keyed_value_without_impl_item_enumeration

crates/sage-test-harness/src/lib.rs · lib:sage_test_harness

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.normalization_demand)]
    fn local_normalization_reads_one_keyed_value_without_impl_item_enumeration() {
        use salsa::Setter as _;

        const SOURCE: &str = "trait Iterable<T> { type Item; type Unrelated; }\n\
             impl Iterable<bool> for bool { type Item = i32; type Unrelated = char; }\n\
             impl Iterable<char> for bool { type Item = u32; type Unrelated = bool; }";

        fn force(db: &dyn Db, source_file: SourceFile) {
            let (_, root) = setup_root_module(db, source_file);
            let (iterable, krate) = trait_and_crate(db, root, "Iterable");
            let associated_ty = first_associated_type(db, iterable);
            let mut stash = Stash::new();
            let self_ty = stash.alloc(Ty::Bool);
            let trait_argument = stash.alloc(Ty::Bool);
            let projection = AliasTy::Associated(ProjectionTy {
                associated_ty,
                self_ty,
                trait_ref: TraitRef {
                    trait_sym: iterable,
                    args: stash.alloc_slice(&[trait_argument]),
                },
                args: stash.alloc_slice(&[]),
            });
            let assumptions = stash.alloc_slice::<Assumption>(&[]);
            let canonical = canonicalize_solver_goal(
                db,
                &stash,
                &VersionedEGraph::new(),
                Version::ROOT,
                krate,
                Universe::ROOT,
                true,
                assumptions,
                SolverGoal::Normalize(projection),
            );
            assert!(matches!(
                GoalQuery::new(db, canonical.data).solve(db).root().value,
                QueryResultData::Yes { .. }
            ));
        }

        let mut database = Database::default();
        let source_file = database.add_source_file("lib.rs".to_owned(), SOURCE.to_owned());
        database.attach(|db| force(db, source_file));
        let cold = database.take_query_log();
        assert!(
            cold.contains("local_impl_associated_type_value"),
            "the requested value needs one keyed query:\n{cold}"
        );
        assert_eq!(
            cold.matches("local_impl_associated_type_value").count(),
            1,
            "a header-mismatched candidate must not read its value:\n{cold}"
        );
        assert_eq!(
            cold.matches("local_impl_associated_item").count(),
            1,
            "the requested value must use one canonical keyed item producer:\n{cold}"
        );
        assert!(
            !cold.contains("LocalImplSym < 'db >::items_"),
            "normalization must not enumerate or lower sibling impl items:\n{cold}"
        );

        database.attach(|db| force(db, source_file));
        let warm = database.take_query_log();
        assert!(
            !warm.contains("local_impl_associated_type_value"),
            "the unchanged value query should be reused:\n{warm}"
        );

        source_file
            .set_text(&mut database)
            .to(SOURCE.replace("type Unrelated = char", "type Unrelated = i16"));
        database.attach(|db| force(db, source_file));
        let unrelated_edit = database.take_query_log();
        assert!(
            unrelated_edit.contains("local_impl_associated_item"),
            "the keyed item producer should revalidate the edited impl CST:\n{unrelated_edit}"
        );
        assert!(
            !unrelated_edit.contains("local_impl_associated_type_value"),
            "editing an unrelated associated value must not rerun the requested value query:\n{unrelated_edit}"
        );

        let mut database = Database::default();
        let source_file = database.add_source_file("lib.rs".to_owned(), SOURCE.to_owned());
        database.attach(|db| {
            let (_, root) = setup_root_module(db, source_file);
            let first_impl = root
                .expanded_module_items(db)
                .iter()
                .find_map(|symbol| match symbol.data(db) {
                    SymbolData::ImplSymbol(sage_ir::symbol::ImplSymbol::Local(item)) => Some(item),
                    _ => None,
                })
                .expect("expected a local impl");
            first_impl.items(db);
        });
        database.take_query_log();

        database.attach(|db| force(db, source_file));
        let after_aggregate = database.take_query_log();
        assert!(
            after_aggregate.contains("local_impl_associated_type_value"),
            "normalization itself must be cold in this scenario:\n{after_aggregate}"
        );
        assert!(
            !after_aggregate.contains("local_impl_associated_item"),
            "normalization must reuse the canonical item producer first invoked by impl.items():\n{after_aggregate}"
        );
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_test_harness::trait_solver_proof_tests::nested_associated_value_remains_a_normalizable_alias

crates/sage-test-harness/src/lib.rs · lib:sage_test_harness

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.normalization_demand)]
    fn nested_associated_value_remains_a_normalizable_alias() {
        with_test_crate(
            "trait Inner { type Value; }\ntrait Outer { type Item; }",
            |db, root| {
                let (inner, _) = trait_and_crate(db, root, "Inner");
                let (outer, krate) = trait_and_crate(db, root, "Outer");
                let inner_associated_ty = first_associated_type(db, inner);
                let outer_associated_ty = first_associated_type(db, outer);
                let mut stash = Stash::new();
                let self_ty = stash.alloc(Ty::Bool);
                let inner_projection = AliasTy::Associated(ProjectionTy {
                    associated_ty: inner_associated_ty,
                    self_ty,
                    trait_ref: TraitRef {
                        trait_sym: inner,
                        args: stash.alloc_slice(&[]),
                    },
                    args: stash.alloc_slice(&[]),
                });
                let outer_projection = AliasTy::Associated(ProjectionTy {
                    associated_ty: outer_associated_ty,
                    self_ty,
                    trait_ref: TraitRef {
                        trait_sym: outer,
                        args: stash.alloc_slice(&[]),
                    },
                    args: stash.alloc_slice(&[]),
                });
                let nested_value = stash.alloc(Ty::Alias(inner_projection));
                let concrete_value = stash.alloc(Ty::Int(IntTy::I32));
                let assumptions = stash.alloc_slice(&[
                    Assumption::NormalizesTo {
                        alias: outer_projection,
                        ty: nested_value,
                    },
                    Assumption::NormalizesTo {
                        alias: inner_projection,
                        ty: concrete_value,
                    },
                ]);
                let egraph = VersionedEGraph::new();
                let canonical = canonicalize_solver_goal(
                    db,
                    &stash,
                    &egraph,
                    Version::ROOT,
                    krate,
                    Universe::ROOT,
                    true,
                    assumptions,
                    SolverGoal::Normalize(outer_projection),
                );
                let outer_result = GoalQuery::new(db, canonical.data).solve(db);
                let (outer_stash, outer_result) = outer_result.open();
                let QueryResultData::Yes {
                    output: GoalOutput::Type(output),
                    ..
                } = outer_result.value
                else {
                    panic!("Outer::Item should normalize")
                };
                let Ty::Alias(nested) = outer_stash[output] else {
                    panic!("the associated value should retain its nested projection")
                };
                let AliasTy::Associated(nested) = nested else {
                    panic!("expected an associated projection")
                };
                assert_eq!(nested.associated_ty, inner_associated_ty);

                let canonical = canonicalize_solver_goal(
                    db,
                    &stash,
                    &VersionedEGraph::new(),
                    Version::ROOT,
                    krate,
                    Universe::ROOT,
                    true,
                    assumptions,
                    SolverGoal::Normalize(inner_projection),
                );
                let nested_result = GoalQuery::new(db, canonical.data).solve(db);
                let (nested_stash, nested_result) = nested_result.open();
                let QueryResultData::Yes {
                    output: GoalOutput::Type(output),
                    ..
                } = nested_result.value
                else {
                    panic!("the nested projection should normalize independently")
                };
                assert_eq!(nested_stash[output], Ty::Int(IntTy::I32));
            },
        );
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Review: Accepted · final_quality.

Reviewed all four implementation entries and three tests for normalization_demand. The complete claim requires preserving alias identity until demanded, revealability as canonical input, projection reads limited to the fixed trait/item, applicable headers, selected values and necessary predicates, and exclusion of unrelated impls and bodies. This is a partially realized destination with explicit reveal/index deferrals.

The associated solve_query entry dispatches Normalize as a distinct input-only operation. Its solve_normalize_frame implementation currently handles associated projections, returns uncertainty for named/opaque aliases and unsupported item arguments, prepares headers before matching, proves candidate conditions, and only then calls load_prepared_associated_value on a successful candidate. A mismatched header never loads its associated value. Environment normalization facts preserve a nested alias as the value rather than recursively erasing it. Captured canonical and boundary alias-copy helpers preserve Named/Associated/Opaque identities and arguments structurally; this is not evidence that opaque reveal context is operational.

The associated clauses.rs loader requests exactly (impl, associated-item) from either local or external storage and copies the value using the prepared candidate's generic mapping. Captured external_associated_type_value uses the two identities as metadata keys and imports a complete value using the relevant impl binder; no body request occurs in this helper. The local_impl_associated_type_value entry resolves the requested item by kind/name/occurrence through the canonical keyed producer, rejects unsupported GAT/where-clause/attributed values, and checks just its type using impl signature generics. Captured associated.rs shows the keyed producer scans the owner's coarse item CST to find one matching item, mints that item through the same producer used by aggregate enumeration, and does not check sibling bodies or lower their values. Source scanning/backdating must not be confused with already having every future fine-grained input boundary.

The fourth implementation entry explicitly defers named alias expansion, opaque reveal context, and excluding unrelated local impl identity reads until local_index_firewall. Current local candidate discovery still scans module impl identities, so the absolute no-unrelated-impl portion is not complete. Captured solver-guide and associated-type-normalization RFD explicitly scope the landed slice to associated projections and provisional local discovery. Reveal-aware canonical inputs and inside/outside opaque behavior remain unimplemented rather than being approved by this report.

Read each complete test and captured fixtures, trait/member lookup helpers, and query logging implementation. local_normalization_reads_one_keyed_value_without_impl_item_enumeration uses two impl headers differing in trait argument plus sibling values. It checks Yes; exactly one value and keyed-item execution cold; no aggregate impl-items lowering; no value execution warm; keyed-item revalidation but no requested-value execution after editing the sibling value; and reuse of the canonical producer after prior aggregate enumeration in a fresh database. The log records WillExecute events and is drained between stages, so these are execution/revalidation assertions, not proof that cached queries were never requested. It does not check exact normalized i32 or comprehensive forbidden-body and unrelated-impl reads. nested_associated_value_remains_a_normalizable_alias obtains symbols from source, supplies constructed normalization assumptions, requires Outer normalization to retain the Inner associated identity, and separately requires Inner normalization to return i32. This is focused solver/boundary evidence using constructed facts, not a source-level impl-value or opaque reveal test.

The semantic_spec TODO retains named/associated/opaque fold/canonical round trips, reveal-context distinctions, and full relevant-header/value versus sibling/unrelated/body trace exclusions. Prerequisites are named/opaque operational semantics with explicit reveal input, the private local index already named in the implementation TODO, and source/trace fixtures exercising those paths. Existing tests discharge only their narrower assertions; they do not erase the deferred matrix. No edits or test execution in this review; commands were fresh review start/read and source inspection before record. No additional requested edits.

Browse crates anchors

139 anchors

Specification anchors and declared coverage
AnchorImplementationTests
crates (139)114 Implemented37 TODO2 N/A74 Implemented107 TODO
crates.sage_inspector (15)13 Implemented1 TODO2 N/A3 Implemented15 TODO
crates.sage_inspector.inspection (15)13 Implemented1 TODO2 N/A3 Implemented15 TODO
balanced_tracesImplementedTODO
canonical_ownershipImplementedImplementedTODO
derive_reflectionImplementedImplementedTODO
detail_free_indexImplementedTODO
deterministic_traceImplementedTODO
durable_navigationN/ATODO
generic_browserN/ATODO
owned_reflectionImplementedImplementedTODO
product_availabilityImplementedTODO
revision_and_demandImplementedTODO
semantic_phase_boundaryImplementedTODO
source_evidenceImplementedTODO
typed_serviceImplementedTODO
unknown_workImplementedTODOTODO
workspace_actorImplementedTODO
crates.sage_ir (90)67 Implemented34 TODO40 Implemented88 TODO
crates.sage_ir.checking (12)12 Implemented3 TODO5 Implemented12 TODO
crates.sage_ir.checking.body (5)5 Implemented2 TODO3 Implemented5 TODO
elaborationImplementedImplementedTODO
expected_typesImplementedTODOTODO
interface_dependenciesImplementedImplementedTODO
isolated_completionImplementedImplementedTODO
operator_callsImplementedTODOTODO
identity_mintingImplementedTODO
owned_productsImplementedImplementedTODO
crates.sage_ir.checking.signature (4)4 Implemented1 TODO1 Implemented4 TODO
body_independenceImplementedTODO
narrow_detailImplementedTODOTODO
owner_binderImplementedImplementedTODO
storageImplementedTODO
symbol_keyed_interfacesImplementedTODO
crates.sage_ir.crate (9)9 TODO9 TODO
explicit_restrictionsTODOTODO
identity_before_detailTODOTODO
incremental_evidenceTODOTODO
narrow_demandsTODOTODO
reexecution_and_invalidationTODOTODO
represented_completenessTODOTODO
restrictions_and_gapsTODOTODO
semantic_query_boundariesTODOTODO
terminal_incompletenessTODOTODO
crates.sage_ir.inference (8)8 Implemented6 Implemented8 TODO
atomic_checkingImplementedImplementedTODO
body_local_quiescenceImplementedImplementedTODO
canonical_boundaryImplementedImplementedTODO
completed_body_boundaryImplementedTODO
numeric_domainsImplementedImplementedTODO
subtyping_and_coercionImplementedImplementedTODO
terminal_obligationsImplementedTODO
transaction_isolationImplementedImplementedTODO
crates.sage_ir.metadata (4)4 Implemented1 TODO4 TODO
explicit_incompletenessImplementedTODO
keyed_reuseImplementedTODOTODO
product_boundariesImplementedTODO
provider_authorityImplementedTODO
crates.sage_ir.modules (8)7 Implemented1 TODO4 Implemented8 TODO
crates.sage_ir.modules.expand (4)4 Implemented2 Implemented4 TODO
completenessImplementedImplementedTODO
dependenciesImplementedTODO
direct_membersImplementedTODO
recursion_and_fixpointImplementedImplementedTODO
crates.sage_ir.modules.parse (4)3 Implemented1 TODO2 Implemented4 TODO
dependenciesImplementedTODO
detail_firewallImplementedImplementedTODO
recovery_completenessTODOTODO
syntax_identitiesImplementedImplementedTODO
crates.sage_ir.resolution (5)5 Implemented1 TODO3 Implemented4 TODO
crates.sage_ir.resolution.lookup (5)5 Implemented1 TODO3 Implemented4 TODO
completenessImplementedTODOImplementedTODO
dependenciesImplementedTODO
expansion_import_ambiguityImplementedImplemented
identity_onlyImplementedTODO
precedenceImplementedImplementedTODO
crates.sage_ir.solver (9)7 Implemented7 TODO5 Implemented9 TODO
alternative_isolationImplementedTODOImplementedTODO
bounded_completenessImplementedTODOTODO
candidate_completenessImplementedTODO
canonical_cyclesTODOTODO
canonical_outputsImplementedImplementedTODO
local_index_firewallTODOTODO
normalization_demandImplementedTODOImplementedTODO
schedule_independenceImplementedTODOImplementedTODO
shared_final_resultImplementedTODOImplementedTODO
crates.sage_ir.symbols (8)8 Implemented4 Implemented7 TODO
associated_identityImplementedImplemented
associated_interfacesImplementedTODO
body_interfacesImplementedImplementedTODO
definition_identityImplementedTODO
external_fact_queriesImplementedTODO
external_identityImplementedTODO
kind_wrappersImplementedImplementedTODO
local_identityImplementedImplementedTODO
crates.sage_ir.types (27)16 Implemented12 TODO13 Implemented27 TODO
crates.sage_ir.types.aliases (2)1 Implemented1 TODO1 Implemented2 TODO
identityImplementedImplementedTODO
revelationTODOTODO
crates.sage_ir.types.binder (1)1 Implemented1 TODO1 Implemented1 TODO
owner_parametersImplementedTODOImplementedTODO
crates.sage_ir.types.body (13)4 Implemented9 TODO3 Implemented13 TODO
awaitTODOTODO
closuresTODOTODO
conditional_patternsTODOTODO
coroutinesTODOTODO
diagnosed_recoveryImplementedImplementedTODO
elaboratedTODOImplementedTODO
for_iterationTODOTODO
indexingTODOTODO
macro_expansionTODOTODO
no_inferenceImplementedImplementedTODO
resolved_referencesImplementedTODO
try_residualTODOTODO
typed_provenanceImplementedTODO
crates.sage_ir.types.calls (2)1 Implemented1 TODO1 Implemented2 TODO
dispatch_familiesTODOTODO
selected_semanticsImplementedImplementedTODO
crates.sage_ir.types.lifetimes (2)2 Implemented2 Implemented2 TODO
dummyImplementedImplementedTODO
unchecked_borrowsImplementedImplementedTODO
crates.sage_ir.types.operators (2)2 Implemented1 Implemented2 TODO
lazy_control_flowImplementedTODO
trait_callsImplementedImplementedTODO
scoped_identitiesImplementedTODO
crates.sage_ir.types.spans (4)4 Implemented4 Implemented4 TODO
generated_identityImplementedImplementedTODO
item_originImplementedImplementedTODO
offset_reuseImplementedImplementedTODO
relative_compositionImplementedImplementedTODO
crates.sage_oracle_harness (4)4 Implemented2 TODO1 Implemented4 TODO
crates.sage_oracle_harness.crate (4)4 Implemented2 TODO1 Implemented4 TODO
deterministic_emissionImplementedTODO
exact_comparisonImplementedTODOImplementedTODO
fixed_projectionImplementedTODO
independent_coverageImplementedTODOTODO
crates.sage_stash (5)5 Implemented5 Implemented
crates.sage_stash.storage (5)5 Implemented5 Implemented
handle_ownershipImplementedImplemented
immutable_entriesImplementedImplemented
query_valueImplementedImplemented
rooted_equalityImplementedImplemented
typed_interningImplementedImplemented
crates.sage_test_harness (25)25 Implemented25 Implemented
crates.sage_test_harness.compile_tests (25)25 Implemented25 Implemented
annotation_validationImplementedImplemented
blessing_gateImplementedImplemented
callsite_updatesImplementedImplemented
checking_scopeImplementedImplemented
compiler_conditionsImplementedImplemented
completed_typesImplementedImplemented
coordinatesImplementedImplemented
dependenciesImplementedImplemented
diagnostic_countsImplementedImplemented
diagnostic_locationsImplementedImplemented
editionImplementedImplemented
fixturesImplementedImplemented
grouped_observationsImplementedImplemented
invocationImplementedImplemented
production_executionImplementedImplemented
project_isolationImplementedImplemented
query_captureImplementedImplemented
query_projectionImplementedImplemented
renderingImplementedImplemented
resolved_symbolsImplementedImplemented
review_visibilityImplementedImplemented
rustc_executionImplementedImplemented
rustc_lintsImplementedImplemented
starting_expressionsImplementedImplemented
target_lineImplementedImplemented