crates.sage_ir.inference.canonical_boundary

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

Implementation

Implemented crates/sage-ir/src/check/infer_ctx.rs:1980–1985

sage_ir::check::infer_ctx · lib:sage_ir

#![allow(unused)]
fn main() {
    // {anchor}`crates.sage_ir.inference.canonical_boundary`
    // {anchor}`crates.sage_ir.solver.canonical_outputs`
    fn apply_normalization_relation(
        &self,
        canonical_goal: &Stashed<super::solve::GoalQueryData<'db>>,
        mapping: &super::solve::CanonicalMapping<'db>,

}

See more source ↗

Implemented crates/sage-ir/src/check/solve/boundary.rs:305–310

sage_ir::check::solve::boundary · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.inference.canonical_boundary`
// {anchor}`crates.sage_ir.inference.transaction_isolation`
// {anchor}`crates.sage_ir.inference.terminal_obligations`
pub fn apply_query_response<'db>(
    db: &'db dyn crate::Db,
    caller_stash: &mut Stash,

}

See more source ↗

Implemented crates/sage-ir/src/check/solve/canonical.rs:88–93

sage_ir::check::solve::canonical · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.inference.canonical_boundary`
pub fn canonicalize_solver_goal<'db>(
    db: &'db dyn crate::Db,
    source: &Stash,
    egraph: &VersionedEGraph<'db>,
    version: Version,

}

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::inference_canonical_boundary

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.canonical_boundary)]
    fn inference_canonical_boundary() {
        // TODO: Complete the claim-specific verification matrix:
        // Canonical round-trip tests cover rigid and flexible inputs, nested binders, universe lowering,
        // shared response-local variables, residual obligations, and type outputs. An incompatible
        // expected type does not select among otherwise ambiguous normalization candidates.
    }
}

See more source ↗

Implemented sage_test_harness::trait_solver_boundary_tests::canonical_equality_round_trips_transactionally

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.canonical_boundary)]
    fn canonical_equality_round_trips_transactionally() {
        with_test_crate("trait Marker {}", |db, root| {
            let krate = crate_from_root_items(db, root);
            let mut caller_stash = Stash::new();
            let mut caller_egraph = VersionedEGraph::new();
            let input_index = caller_egraph.alloc_var(Version::ROOT, Universe(1));
            let input = caller_stash.alloc(Ty::InferVar(input_index));
            let integer = caller_stash.alloc(Ty::Int(IntTy::I32));
            let assumptions = caller_stash.alloc_slice::<Assumption>(&[]);
            let canonical = canonicalize_goal(
                db,
                &caller_stash,
                &caller_egraph,
                Version::ROOT,
                krate,
                Universe(1),
                true,
                assumptions,
                Goal::Atom(Atom::Equals(input, integer)),
            );

            let mut proof = instantiate_query(&canonical.data);
            let SolverGoal::Prove(Goal::Atom(Atom::Equals(left, right))) = proof.goal else {
                panic!("expected equality goal")
            };
            try_unify(
                &mut proof.egraph,
                &mut proof.stash,
                proof.version,
                left,
                right,
            )
            .unwrap();
            let modulo = Goal::true_(&mut proof.stash);
            let response = extract_query_result(db, &proof, GoalResult::Yes { modulo });
            let applied = apply_query_response(
                db,
                &mut caller_stash,
                &mut caller_egraph,
                Version::ROOT,
                &canonical.data,
                &canonical.mapping,
                &response,
            )
            .unwrap();

            assert!(matches!(applied.certainty, AppliedCertainty::Yes { .. }));
            assert_eq!(caller_egraph.find(Version::ROOT, input), integer);
        });
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_test_harness::trait_solver_boundary_tests::canonical_response_preserves_lowered_input_universe

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.canonical_boundary)]
    fn canonical_response_preserves_lowered_input_universe() {
        with_test_crate("trait Marker {}", |db, root| {
            let krate = crate_from_root_items(db, root);
            let mut stash = Stash::new();
            let mut egraph = VersionedEGraph::new();
            let input_index = egraph.alloc_var(Version::ROOT, Universe(2));
            let input = stash.alloc(Ty::InferVar(input_index));
            let assumptions = stash.alloc_slice::<Assumption>(&[]);
            let canonical = canonicalize_goal(
                db,
                &stash,
                &egraph,
                Version::ROOT,
                krate,
                Universe(1),
                true,
                assumptions,
                Goal::Atom(Atom::Equals(input, input)),
            );
            let mut proof = instantiate_query(&canonical.data);
            let Ty::InferVar(proof_input) = proof.stash[proof.inputs[0].ty] else {
                panic!("expected flexible proof input");
            };
            proof
                .egraph
                .lower_universe(proof.version, proof_input, Universe::ROOT);
            let modulo = Goal::true_(&mut proof.stash);
            let response = extract_query_result(db, &proof, GoalResult::Yes { modulo });
            apply_query_response(
                db,
                &mut stash,
                &mut egraph,
                Version::ROOT,
                &canonical.data,
                &canonical.mapping,
                &response,
            )
            .unwrap();
            assert_eq!(
                egraph.current_universe(Version::ROOT, input_index),
                Universe(1)
            );
        });
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_test_harness::trait_solver_boundary_tests::canonical_response_preserves_lowered_unified_input_universe

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.canonical_boundary)]
    fn canonical_response_preserves_lowered_unified_input_universe() {
        with_test_crate("trait Marker {}", |db, root| {
            let krate = crate_from_root_items(db, root);
            let mut stash = Stash::new();
            let mut egraph = VersionedEGraph::new();
            let input_index = egraph.alloc_var(Version::ROOT, Universe(2));
            let input = stash.alloc(Ty::InferVar(input_index));
            let other_index = egraph.alloc_var(Version::ROOT, Universe(2));
            let other = stash.alloc(Ty::InferVar(other_index));
            let assumptions = stash.alloc_slice::<Assumption>(&[]);
            let canonical = canonicalize_goal(
                db,
                &stash,
                &egraph,
                Version::ROOT,
                krate,
                Universe(1),
                true,
                assumptions,
                Goal::Atom(Atom::Equals(input, other)),
            );
            let mut proof = instantiate_query(&canonical.data);
            let left = proof.inputs[0].ty;
            let right = proof.inputs[1].ty;
            try_unify(
                &mut proof.egraph,
                &mut proof.stash,
                proof.version,
                left,
                right,
            )
            .unwrap();
            let root = proof.egraph.find(proof.version, left);
            let Ty::InferVar(proof_input) = proof.stash[root] else {
                panic!("expected flexible proof input");
            };
            proof
                .egraph
                .lower_universe(proof.version, proof_input, Universe::ROOT);
            let modulo = Goal::true_(&mut proof.stash);
            let response = extract_query_result(db, &proof, GoalResult::Yes { modulo });
            apply_query_response(
                db,
                &mut stash,
                &mut egraph,
                Version::ROOT,
                &canonical.data,
                &canonical.mapping,
                &response,
            )
            .unwrap();
            assert_eq!(
                egraph.find(Version::ROOT, input),
                egraph.find(Version::ROOT, other)
            );
            let root = egraph.find(Version::ROOT, input);
            let Ty::InferVar(root_index) = stash[root] else {
                panic!("expected unresolved caller class");
            };
            assert_eq!(
                egraph.current_universe(Version::ROOT, root_index),
                Universe(1)
            );
        });
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_test_harness::trait_solver_proof_tests::response_local_type_output_round_trips_with_sharing

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.canonical_boundary)]
    fn response_local_type_output_round_trips_with_sharing() {
        with_test_crate(
            "trait Iterable { type Item; }\n\
             impl<T> Iterable for bool { type Item = (T, T); }",
            |db, root| {
                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 projection = AliasTy::Associated(ProjectionTy {
                    associated_ty,
                    self_ty,
                    trait_ref: TraitRef {
                        trait_sym: iterable,
                        args: stash.alloc_slice(&[]),
                    },
                    args: stash.alloc_slice(&[]),
                });
                let assumptions = stash.alloc_slice::<Assumption>(&[]);
                let mut egraph = VersionedEGraph::new();
                let canonical = canonicalize_solver_goal(
                    db,
                    &stash,
                    &egraph,
                    Version::ROOT,
                    krate,
                    Universe::ROOT,
                    true,
                    assumptions,
                    SolverGoal::Normalize(projection),
                );
                let response = GoalQuery::new(db, canonical.data.clone()).solve(db);
                assert_eq!(response.stash()[response.root().bound_vars].len(), 1);
                let applied = apply_query_response(
                    db,
                    &mut stash,
                    &mut egraph,
                    Version::ROOT,
                    &canonical.data,
                    &canonical.mapping,
                    &response,
                )
                .unwrap();
                let AppliedCertainty::Yes {
                    output: GoalOutput::Type(output),
                    modulo,
                } = applied.certainty
                else {
                    panic!("expected a caller-local type output")
                };
                assert!(modulo.is_trivially_true(&stash));
                let Ty::Tuple(elements) = stash[output] else {
                    panic!("expected tuple output")
                };
                let [left, right] = stash[elements] else {
                    panic!("expected pair")
                };
                let Ty::InferVar(left) = stash[left] else {
                    panic!("response witness should be imported as an inference variable")
                };
                let Ty::InferVar(right) = stash[right] else {
                    panic!("response witness should be imported as an inference variable")
                };
                assert_eq!(
                    left, right,
                    "the repeated response witness must retain sharing"
                );
                assert_eq!(egraph.current_universe(Version::ROOT, left), Universe::ROOT);
            },
        );
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Review: Accepted · Codex /root/final_quality.

Reviewed the complete canonical_boundary claim, three ordinary implementation associations, four ordinary tests and one TODO test. Requirements: canonicalize goal and environment together; preserve rigid/flexible inputs, relative universes, substitutions, residuals and goal-specific outputs without capture or lost sharing; apply knowledge transactionally; import normalization output before relating it to caller expectation. Captured inference design and linked architectural-foundations rationale for output-producing solver operations.

canonical.rs uses one Canonicalizer for assumptions followed by SolverGoal. It maps free rigid identities and egraph-root flexible variables through shared maps, carries kind/role/domain/universe metadata, subtracts a common universe base, and keeps the inverse caller mapping outside the query data. Nested existential binders receive distinct alpha identities with saved/restored lexical mappings. Shared traversal of types, aliases, predicates and assumptions retains repeated input identities. The canonical goal stores Normalize(alias), not an expected output type. infer_ctx canonicalize_obligation_goal likewise omits expected from the solver goal.

boundary.rs instantiate_query creates an isolated proof stash/egraph, recreates rigid placeholders and flexible inputs with their canonical universes/domains, and copies environment and goal through one mapping. ResponseExtractor traverses substitutions, output and residuals using shared response-variable maps. It reuses an input class only when the resolved root still has the original domain and universe; critically this compares the root variable's current universe, not an obsolete unified input index. Changed ceilings/domains therefore become response-bound variables and substitutions. Response-local variables carry relative universe/domain metadata. Extraction checks operation/output compatibility for successful results and asserts no proof-local inference variable escapes. IrCopier copies output/substitutions/residuals through the same map and freshens residual binders with lexical save/restore.

apply_query_response validates mapping arity, substitution keys and response binder identities, allocates imports in a child egraph version, applies substitutions there, and collapses only after all unifications succeed; errors discard the branch. Captured egraph branch/collapse/discard and unifier excerpts confirm universe ceilings and class changes are child state and are merged only on success. apply_normalization_relation creates an outer transaction, imports the solver response first, then unifies the returned Type with expected. Maybe/No/import failure/relation failure discard that outer transaction; successful relation publishes commit effects. This ordering prevents expected from selecting the normalized candidate. Captured goal/result definitions make the distinct output and residual fields explicit.

Supported-input limitation investigated: canonicalization has Const::Param handling, but IrCopier's const mapping is narrower. This is not claimed supported const round-trip behavior: captured goal.rs validation rejects const-parameter arrays, rejects non-type existential inputs/binders, and captured prove.rs solve_query validates before instantiation/execution. Captured trait_env.rs explicitly marks const-generic declarations Unsupported. Thus the suspected free-const remapping path is outside admitted solver inputs; no supported-input behavioral failure was identified. Root agreed with this restriction-based assessment. Enabling those inputs later requires completing remapping and its tests; this report does not broaden current support.

All ordinary tests read in full: canonical_equality_round_trips_transactionally constructs a boundary equality, instantiates/unifies/extracts/applies it and asserts Yes plus the caller variable resolving to i32. It establishes successful substitution application, not rollback on failure. canonical_response_preserves_lowered_input_universe lowers a proof input's universe and asserts the caller ceiling becomes Universe(1). canonical_response_preserves_lowered_unified_input_universe first unifies two proof inputs, lowers the representative, then asserts both caller inputs share a root and that root has the lowered ceiling. These directly cover the original-input and aliased-input metadata paths. response_local_type_output_round_trips_with_sharing obtains a normalization result with one response-bound variable, imports a tuple output, checks trivial residual, equal inference IDs in both tuple elements, and root universe. Its deliberately unconstrained generic impl fixture and manually constructed query exercise boundary mechanics; they are not evidence of acceptance of that program by rustc or a full body-level normalization scenario. Captured source fixture and trait/associated-item lookup helpers show production source parsing and symbol discovery; the low-level manually constructed egraph portions are treated as focused boundary tests.

The TODO inference_canonical_boundary explicitly retains the larger matrix: rigid/flexible inputs, nested binders, universes, shared response locals, residual obligations, type outputs, and incompatible expected type not choosing among ambiguous normalization candidates. It has no assertions. Completing it requires admitted-input source-backed scenarios and targeted transactional failure/ambiguity cases, plus binder/residual sharing and capture assertions; unsupported const kinds additionally require implementation support first. The four tests are useful partial evidence and do not close that TODO. No N/A evidence applies.

Executed fresh review start with coordinator instructions, source inspection, and review read captures of design/RFD, query/result types, fixture helpers, transaction/unifier helpers and supported-input restrictions. No test commands or build executed by this reviewer; central suite results are separate. No source edits. No requested edits; explicitly retained verification and input-support limits remain visible.

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