crates.sage_ir.solver.alternative_isolation

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

Implementation

Implemented crates/sage-ir/src/check/solve/anti_unify.rs:25–30

sage_ir::check::solve::anti_unify · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.alternative_isolation`
pub(crate) fn merge_hints<'db>(
    db: &'db dyn crate::Db,
    next_response_param: u32,
    input_universes: &FxHashMap<AlphaEquivParam<'db>, u32>,
    input_domains: &FxHashMap<AlphaEquivParam<'db>, InferDomain>,

}

See more source ↗

Implemented crates/sage-ir/src/check/solve/boundary.rs:44–49

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

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.alternative_isolation`
pub fn instantiate_query<'db>(query: &Stashed<GoalQueryData<'db>>) -> QueryProofState<'db> {
    let (source, data) = query.open();
    let mut stash = Stash::new();
    let mut egraph = VersionedEGraph::new();
    let version = Version::ROOT;

}

See more source ↗

Implemented crates/sage-ir/src/check/solve/boundary.rs:127–132

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

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.alternative_isolation`
pub(crate) fn extract_query_result_with_output_at<'db>(
    db: &'db dyn crate::Db,
    state: &QueryProofState<'db>,
    version: Version,
    output: GoalOutput<'db>,

}

See more source ↗

Implemented crates/sage-ir/src/check/solve/merge.rs:12–17

sage_ir::check::solve::merge · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.alternative_isolation`
// {anchor}`crates.sage_ir.solver.schedule_independence`
// {anchor}`crates.sage_ir.modules.expand.completeness`
// {anchor}`crates.sage_ir.solver.candidate_completeness`
// {anchor}`crates.sage_ir.solver.canonical_outputs`
pub(crate) fn merge_candidate_results<'db>(

}

See more source ↗

Implemented crates/sage-ir/src/check/solve/prove.rs:638–643

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

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.alternative_isolation`
// {anchor}`crates.sage_ir.solver.canonical_outputs`
async fn solve_normalize_frame<'db>(
    db: &'db dyn crate::Db,
    whiteboard: &Whiteboard<'db>,
    query: &Stashed<GoalQueryData<'db>>,

}

See more source ↗

Implemented crates/sage-ir/src/check/solve/prove.rs:980–985

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

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.solver.alternative_isolation`
// {anchor}`crates.sage_ir.inference.transaction_isolation`
// {anchor}`crates.sage_ir.solver.candidate_completeness`
async fn solve_trait_frame<'db>(
    db: &'db dyn crate::Db,
    whiteboard: &Whiteboard<'db>,

}

See more source ↗

TODO crates/sage-meta/tests/semantic_spec.rs:165–170

sage_meta::todo · test:semantic_spec

TODO: Concurrent conjunction and cancellation isolation remain planned beyond current completed-answer reduction. TODO: Complete the claim-specific verification matrix:

#![allow(unused)]
fn main() {
    // {anchor}`crates.sage_ir.solver.alternative_isolation`
    // TODO: Concurrent conjunction and cancellation isolation remain planned beyond current completed-answer reduction.
    #[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn solver_alternative_isolation() {
        // TODO: Complete the claim-specific verification matrix:

}

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::solve::merge::tests::anti_unification_retains_shared_constructor_and_component

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn anti_unification_retains_shared_constructor_and_component() {
        let db = Database::default();
        let key = AlphaEquivParam::new(&db, GenericParamKind::Type, 0);
        let inputs = FxHashMap::from_iter([(key, 0)]);
        fn tuple_answer<'db>(
            key: AlphaEquivParam<'db>,
            first: Ty<'db>,
        ) -> Stashed<QueryResult<'db>> {
            let mut stash = Stash::new();
            let first = stash.alloc(first);
            let boolean = stash.alloc(Ty::Bool);
            let elements = stash.alloc_slice(&[first, boolean]);
            let value = stash.alloc(Ty::Tuple(elements));
            let subst = stash.alloc_slice(&[SubstEntry { key, value }]);
            let bound_vars = stash.alloc_slice(&[]);
            let modulo = Goal::true_(&mut stash);
            Stashed::new(
                stash,
                QueryResult {
                    bound_vars,
                    value: QueryResultData::Yes {
                        output: GoalOutput::Proven,
                        subst,
                        modulo,
                    },
                },
            )
        }
        let result = merge_candidate_results(
            &db,
            1,
            &inputs,
            &FxHashMap::default(),
            vec![
                tuple_answer(key, Ty::Int(IntTy::I32)),
                tuple_answer(key, Ty::Bool),
            ],
            false,
        );
        let (stash, result) = result.open();
        let QueryResultData::Maybe { hints } = result.value else {
            panic!("incomparable answers must be ambiguous")
        };
        let [hint] = &stash[hints] else {
            panic!("shared tuple shape should remain a hard hint")
        };
        let Ty::Tuple(elements) = stash[hint.value] else {
            panic!("expected tuple hint")
        };
        let elements = &stash[elements];
        assert!(matches!(stash[elements[0]], Ty::Param(_)));
        assert_eq!(stash[elements[1]], Ty::Bool);
        assert_eq!(stash[result.bound_vars].len(), 1);
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::directional_subsumption_binds_only_repeated_consequent_witnesses

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn directional_subsumption_binds_only_repeated_consequent_witnesses() {
        let db = Database::default();
        let key = AlphaEquivParam::new(&db, GenericParamKind::Type, 0);
        let witness = AlphaEquivParam::new(&db, GenericParamKind::Type, 1);
        let inputs = FxHashMap::from_iter([(key, 0)]);
        let general = repeated_witness_answer(&db, key, witness, 0);

        fn tuple_answer<'db>(
            key: AlphaEquivParam<'db>,
            left: Ty<'db>,
            right: Ty<'db>,
        ) -> Stashed<QueryResult<'db>> {
            let mut stash = Stash::new();
            let left = stash.alloc(left);
            let right = stash.alloc(right);
            let elements = stash.alloc_slice(&[left, right]);
            let value = stash.alloc(Ty::Tuple(elements));
            let subst = stash.alloc_slice(&[SubstEntry { key, value }]);
            let bound_vars = stash.alloc_slice(&[]);
            let modulo = Goal::true_(&mut stash);
            Stashed::new(
                stash,
                QueryResult {
                    bound_vars,
                    value: QueryResultData::Yes {
                        output: GoalOutput::Proven,
                        subst,
                        modulo,
                    },
                },
            )
        }

        let repeated = tuple_answer(key, Ty::Int(IntTy::I32), Ty::Int(IntTy::I32));
        let result = merge_candidate_results(
            &db,
            2,
            &inputs,
            &FxHashMap::default(),
            vec![repeated, general.clone()],
            false,
        );
        assert_eq!(result, general);

        let non_repeated = tuple_answer(key, Ty::Int(IntTy::I32), Ty::Bool);
        let result = merge_candidate_results(
            &db,
            2,
            &inputs,
            &FxHashMap::default(),
            vec![non_repeated, general],
            false,
        );
        assert!(matches!(result.root().value, QueryResultData::Maybe { .. }));
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::distinct_response_domains_do_not_subsume_each_other

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn distinct_response_domains_do_not_subsume_each_other() {
        let db = Database::default();
        let key = AlphaEquivParam::new(&db, GenericParamKind::Type, 0);
        let witness = AlphaEquivParam::new(&db, GenericParamKind::Type, 1);
        let input_universes = FxHashMap::from_iter([(key, 0)]);
        let input_domains = FxHashMap::from_iter([(key, InferDomain::Any)]);

        let result = merge_candidate_results(
            &db,
            1,
            &input_universes,
            &input_domains,
            vec![
                domain_witness_answer(key, witness, InferDomain::Integer, None, true),
                domain_witness_answer(key, witness, InferDomain::Float, None, true),
            ],
            false,
        );

        assert!(matches!(result.root().value, QueryResultData::Maybe { .. }));
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::divergent_bare_values_produce_empty_hard_hint

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn divergent_bare_values_produce_empty_hard_hint() {
        let db = Database::default();
        let key = AlphaEquivParam::new(&db, GenericParamKind::Type, 0);
        let inputs = FxHashMap::from_iter([(key, 0)]);
        let result = merge_candidate_results(
            &db,
            1,
            &inputs,
            &FxHashMap::default(),
            vec![
                conditional_answer(key, Ty::Int(IntTy::I32)),
                conditional_answer(key, Ty::Bool),
            ],
            false,
        );
        let (stash, result) = result.open();
        let QueryResultData::Maybe { hints } = result.value else {
            panic!("incomparable answers must be ambiguous")
        };
        assert!(stash[hints].is_empty());
        assert!(stash[result.bound_vars].is_empty());
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::duplicate_identical_yes_is_one_answer

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn duplicate_identical_yes_is_one_answer() {
        let db = Database::default();
        let answer = yes(false);
        let result = merge_candidate_results(
            &db,
            0,
            &FxHashMap::default(),
            &FxHashMap::default(),
            vec![answer.clone(), answer],
            false,
        );
        assert!(matches!(result.root().value, QueryResultData::Yes { .. }));
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::final_answer_rules_are_order_independent

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    #[sage::test(crates.sage_ir.solver.schedule_independence)]
    fn final_answer_rules_are_order_independent() {
        let db = Database::default();
        let no = no_result();
        let maybe = maybe();
        let unconditional = yes(true);
        for candidates in [
            vec![no.clone(), maybe.clone(), unconditional.clone()],
            vec![unconditional.clone(), no.clone(), maybe.clone()],
            vec![maybe.clone(), unconditional.clone(), no.clone()],
        ] {
            let result = merge_candidate_results(
                &db,
                0,
                &FxHashMap::default(),
                &FxHashMap::default(),
                candidates,
                false,
            );
            assert_eq!(result, unconditional);
        }

        let all_maybe = merge_candidate_results(
            &db,
            0,
            &FxHashMap::default(),
            &FxHashMap::default(),
            vec![maybe.clone(), maybe],
            false,
        );
        assert!(matches!(
            all_maybe.root().value,
            QueryResultData::Maybe { .. }
        ));
        let all_no = merge_candidate_results(
            &db,
            0,
            &FxHashMap::default(),
            &FxHashMap::default(),
            vec![no.clone(), no],
            false,
        );
        assert!(matches!(all_no.root().value, QueryResultData::No));
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::general_conditional_answer_subsumes_specific_one

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn general_conditional_answer_subsumes_specific_one() {
        let db = Database::default();
        let key = AlphaEquivParam::new(&db, GenericParamKind::Type, 0);
        let inputs = FxHashMap::from_iter([(key, 0)]);
        let mut stash = Stash::new();
        let bound_vars = stash.alloc_slice(&[]);
        let subst = stash.alloc_slice(&[]);
        let general = Stashed::new(
            stash,
            QueryResult {
                bound_vars,
                value: QueryResultData::Yes {
                    output: GoalOutput::Proven,
                    subst,
                    modulo: Goal::Maybe,
                },
            },
        );
        let specific = {
            let answer = conditional_answer(key, Ty::Bool);
            let (source, result) = answer.open();
            let QueryResultData::Yes { subst, .. } = result.value else {
                unreachable!()
            };
            let mut target = Stash::new();
            let subst = subst.stash_copy(source, &mut target);
            let bound_vars = target.alloc_slice(&[]);
            Stashed::new(
                target,
                QueryResult {
                    bound_vars,
                    value: QueryResultData::Yes {
                        output: GoalOutput::Proven,
                        subst,
                        modulo: Goal::Maybe,
                    },
                },
            )
        };
        let result = merge_candidate_results(
            &db,
            1,
            &inputs,
            &FxHashMap::default(),
            vec![specific, general],
            false,
        );
        assert!(matches!(result.root().value, QueryResultData::Yes { .. }));
        let QueryResultData::Yes { subst, .. } = result.root().value else {
            unreachable!()
        };
        assert!(result.stash()[subst].is_empty());
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::merged_bare_hints_preserve_a_common_response_domain

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn merged_bare_hints_preserve_a_common_response_domain() {
        let db = Database::default();
        let key = AlphaEquivParam::new(&db, GenericParamKind::Type, 0);
        let witness = AlphaEquivParam::new(&db, GenericParamKind::Type, 1);
        let input_universes = FxHashMap::from_iter([(key, 0)]);
        let input_domains = FxHashMap::from_iter([(key, InferDomain::Any)]);
        let result = merge_candidate_results(
            &db,
            1,
            &input_universes,
            &input_domains,
            vec![
                domain_witness_answer(key, witness, InferDomain::Integer, None, true),
                domain_witness_answer(key, witness, InferDomain::Integer, None, false),
            ],
            false,
        );
        let (stash, result) = result.open();
        let QueryResultData::Maybe { hints } = result.value else {
            panic!("mixed certainty must remain ambiguous")
        };
        let [hint] = &stash[hints] else {
            panic!("a common restricted domain should remain a hint")
        };
        let Ty::Param(GenericParam::AlphaEquiv(param)) = stash[hint.value] else {
            panic!("expected a response-local hint witness")
        };
        let [info] = &stash[result.bound_vars] else {
            panic!("expected one response-local binder")
        };
        assert_eq!(info.param, param);
        assert_eq!(info.domain, InferDomain::Integer);
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::merged_nested_hints_preserve_a_common_response_domain

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn merged_nested_hints_preserve_a_common_response_domain() {
        let db = Database::default();
        let key = AlphaEquivParam::new(&db, GenericParamKind::Type, 0);
        let witness = AlphaEquivParam::new(&db, GenericParamKind::Type, 1);
        let input_universes = FxHashMap::from_iter([(key, 0)]);
        let input_domains = FxHashMap::from_iter([(key, InferDomain::Any)]);
        let result = merge_candidate_results(
            &db,
            1,
            &input_universes,
            &input_domains,
            vec![
                domain_witness_answer(key, witness, InferDomain::Integer, Some(Ty::Bool), true),
                domain_witness_answer(key, witness, InferDomain::Integer, Some(Ty::Char), true),
            ],
            false,
        );
        let (stash, result) = result.open();
        let QueryResultData::Maybe { hints } = result.value else {
            panic!("incomparable answers must remain ambiguous")
        };
        let [hint] = &stash[hints] else {
            panic!("the common tuple shape should remain a hint")
        };
        let Ty::Tuple(elements) = stash[hint.value] else {
            panic!("expected a tuple hint")
        };
        let Ty::Param(GenericParam::AlphaEquiv(first)) = stash[stash[elements][0]] else {
            panic!("expected a response-local first element")
        };
        let info = stash[result.bound_vars]
            .iter()
            .find(|info| info.param == first)
            .expect("hint witness must have binder metadata");
        assert_eq!(info.domain, InferDomain::Integer);
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::subsumption_witness_cannot_capture_a_newer_rigid_input

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn subsumption_witness_cannot_capture_a_newer_rigid_input() {
        let db = Database::default();
        let key = AlphaEquivParam::new(&db, GenericParamKind::Type, 0);
        let witness = AlphaEquivParam::new(&db, GenericParamKind::Type, 1);
        let newer = AlphaEquivParam::new(&db, GenericParamKind::Type, 2);
        let inputs = FxHashMap::from_iter([(key, 0), (newer, 1)]);
        let general = {
            let mut stash = Stash::new();
            let value = stash.alloc(Ty::Param(GenericParam::AlphaEquiv(witness)));
            let subst = stash.alloc_slice(&[SubstEntry { key, value }]);
            let bound_vars = stash.alloc_slice(&[super::super::ResponseVarInfo {
                param: witness,
                kind: GenericParamKind::Type,
                relative_universe: 0,
                domain: crate::check::infer::version::InferDomain::Any,
            }]);
            let modulo = Goal::true_(&mut stash);
            Stashed::new(
                stash,
                QueryResult {
                    bound_vars,
                    value: QueryResultData::Yes {
                        output: GoalOutput::Proven,
                        subst,
                        modulo,
                    },
                },
            )
        };
        let specific = conditional_answer(key, Ty::Param(GenericParam::AlphaEquiv(newer)));
        let result = merge_candidate_results(
            &db,
            3,
            &inputs,
            &FxHashMap::default(),
            vec![specific, general],
            false,
        );
        assert!(matches!(result.root().value, QueryResultData::Maybe { .. }));
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::solve::merge::tests::unconditional_type_output_does_not_hide_an_incomplete_source

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn unconditional_type_output_does_not_hide_an_incomplete_source() {
        let db = Database::default();
        let mut stash = Stash::new();
        let output = stash.alloc(Ty::Bool);
        let bound_vars = stash.alloc_slice(&[]);
        let subst = stash.alloc_slice(&[]);
        let modulo = Goal::true_(&mut stash);
        let answer = Stashed::new(
            stash,
            QueryResult {
                bound_vars,
                value: QueryResultData::Yes {
                    output: GoalOutput::Type(output),
                    subst,
                    modulo,
                },
            },
        );
        let result = merge_candidate_results(
            &db,
            0,
            &FxHashMap::default(),
            &FxHashMap::default(),
            vec![answer],
            true,
        );
        assert!(matches!(result.root().value, QueryResultData::Maybe { .. }));
    }
}

Conditional source: #[cfg(test)]

See more source ↗

TODO sage_meta::todo::solver_alternative_isolation

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn solver_alternative_isolation() {
        // TODO: Complete the claim-specific verification matrix:
        // Candidate-order permutations produce identical canonical responses; incompatible normalization
        // outputs remain ambiguous; failed or cancelled candidates leak no equality, universe change,
        // wake, or obligation; concurrent-conjunction tests reconcile sibling information before
        // accepting an absorbing result.
    }
}

See more source ↗

Implemented sage_test_harness::trait_solver_proof_tests::incompatible_normalization_outputs_are_ambiguous_but_identical_outputs_merge

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.solver.alternative_isolation)]
    fn incompatible_normalization_outputs_are_ambiguous_but_identical_outputs_merge() {
        let check = |second_value: &str, expect_yes: bool| {
            let source = format!(
                "trait Iterable {{ type Item; }}\n\
                 impl Iterable for bool {{ type Item = bool; }}\n\
                 impl Iterable for bool {{ type Item = {second_value}; }}"
            );
            let database = Database::default();
            let observer = database.clone();
            with_test_crate_files_using_db(database, &[("lib.rs", source.as_str())], |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 egraph = VersionedEGraph::new();
                let canonical = canonicalize_solver_goal(
                    db,
                    &stash,
                    &egraph,
                    Version::ROOT,
                    krate,
                    Universe::ROOT,
                    true,
                    assumptions,
                    SolverGoal::Normalize(projection),
                );
                let result = GoalQuery::new(db, canonical.data).solve(db);
                assert_eq!(
                    matches!(result.root().value, QueryResultData::Yes { .. }),
                    expect_yes,
                    "the query has no expected output with which to filter candidates"
                );
                assert_eq!(
                    matches!(result.root().value, QueryResultData::Maybe { .. }),
                    !expect_yes
                );
            });
            observer.take_inspection_log()
        };
        let identical = check("bool", true);
        let incompatible = check("i32", false);
        for events in [&identical, &incompatible] {
            let enters = events
                .iter()
                .filter(|event| {
                    matches!(
                        event,
                        sage_ir::db::InspectionEvent::SpanEnter {
                            operation: "normalization-candidates",
                            child_order: sage_ir::db::InspectionChildOrder::Unordered,
                            ..
                        }
                    )
                })
                .count();
            let exits = events
                .iter()
                .filter(|event| {
                    matches!(
                        event,
                        sage_ir::db::InspectionEvent::SpanExit {
                            operation: "normalization-candidates"
                        }
                    )
                })
                .count();
            assert!(enters > 0, "normalization alternatives must be visible");
            assert_eq!(enters, exits, "normalization spans must remain balanced");
        }
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Review: Accepted · final_quality.

Reviewed all seven implementation entries and thirteen associated tests against the complete alternative_isolation claim. Requirements are isolated candidate inference and canonical publication, order-independent answer reduction, hard knowledge common to every live possibility, compatible value outputs or justified priority, and reconciliation before concurrent conjunct cancellation. The final requirement and exhaustive isolation verification remain explicitly deferred, not implicitly certified by current tests.

The two boundary.rs entries instantiate a fresh stash/egraph for each query and extract branch-specific canonical responses into owned storage. Extraction includes substitutions, output, residual goals and response binder metadata, validates operation/output pairing, and rejects leaked InferVars. It preserves narrowed domain/current-universe information instead of silently reusing an unchanged input identity. In prove.rs, both trait and normalization frames create a fresh candidate state per task, open a local child, extract before discard, and send only stashed responses to aggregation. Trait disjunction can cancel remaining tasks only on unconditional Proven with empty substitution and true residual; this absorption does not choose a value or constrain sibling input. Normalization waits for all candidates, including environment uncertainty and normalization facts. Captured ScopedTasks cancel/drop destroys pending futures; no shared mutable candidate egraph is handed to sibling tasks.

merge.rs sorts/deduplicates completed answers before pairwise conservative subsumption. Apart-renamed response witnesses, directional matching, repeated-witness consistency, universe limits, and domain admission prevent unrelated binders from being confused. Type outputs participate in the same compatibility matching as conditions/substitutions; unlike unconditional Proven, a type output cannot absorb an unknown candidate source. There is no implemented specialization priority asserted here. anti_unify.rs keeps only substitution keys present across every live answer, preserves common constructors/components and explicit shared domains, drops vacuous bare witnesses and inaccessible input references, and adds an unconstrained possibility for incomplete enumeration. This is the documented restricted final hard-hint channel, not the planned full incremental envelope interface.

All eleven merge unit tests were read with their construction helpers. duplicate_identical_yes_is_one_answer asserts Yes after deduplication. final_answer_rules_are_order_independent compares three candidate orderings to the same unconditional result and checks all-Maybe/all-No. general_conditional_answer_subsumes_specific_one checks the remaining substitution is empty. directional_subsumption_binds_only_repeated_consequent_witnesses checks equal tuple components are subsumed and unequal ones remain Maybe. subsumption_witness_cannot_capture_a_newer_rigid_input and distinct_response_domains_do_not_subsume_each_other each assert Maybe. anti_unification_retains_shared_constructor_and_component asserts a tuple hint, retained bool component and one witness; divergent_bare_values_produce_empty_hard_hint asserts both hints and binders empty. merged_bare_hints_preserve_a_common_response_domain and merged_nested_hints_preserve_a_common_response_domain inspect the response witness binder and require Integer. unconditional_type_output_does_not_hide_an_incomplete_source explicitly requires Maybe. These are meaningful reduction-level tests, not source-level proofs of scheduling or cancellation isolation.

The harness test incompatible_normalization_outputs_are_ambiguous_but_identical_outputs_merge parses local trait/impl source, obtains the associated item, constructs an unfiltered Normalize query, and asserts Yes for equal bool outputs and Maybe for bool versus i32. It additionally requires nonempty balanced unordered normalization inspection spans. Captured fixture and symbol helpers demonstrate the production parse/member/solver route; overlapping impl source is deliberately a Sage ambiguity fixture, not a rustc-accepted coherence example. It does not test every schedule or inspect the exact returned type.

The semantic_spec TODO implementation explicitly preserves concurrent conjunction and cancellation isolation work. Its TODO test retains full candidate permutations, failure/cancellation leakage of equality/universe/wakes/obligations, and sibling-information reconciliation. Current prove_conjunction runs sequentially in one child and retries after semantic progress, so there is no implemented concurrent stale-snapshot cancellation protocol to certify. Prerequisites are that protocol and controlled suspension/cancellation fixtures observing all listed effects; the existing final-answer permutations and output tests cover only part of that matrix. Captured solver-guide and architectural-foundations sections confirm this boundary. No new source edits or test executions; only review start/read and source inspections were performed before recording. Central suite results do not discharge the TODO matrix. 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