crates.sage_ir.inference.numeric_domains

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

Implementation

Implemented crates/sage-ir/src/check/infer/egraph.rs:109–114

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

#![allow(unused)]
fn main() {
    // {anchor}`crates.sage_ir.inference.numeric_domains`
    pub fn effective_domain(
        &self,
        version: Version,
        stash: &Stash,
        ty: Ptr<Ty<'db>>,

}

See more source ↗

Implemented crates/sage-ir/src/check/infer/unify.rs:42–47

sage_ir::check::infer::unify · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.inference.numeric_domains`
pub fn try_unify<'db>(
    egraph: &mut VersionedEGraph<'db>,
    stash: &mut Stash,
    parent: Version,
    left: Ptr<Ty<'db>>,

}

See more source ↗

Implemented crates/sage-ir/src/check/infer/version.rs:16–21

sage_ir::check::infer::version · lib:sage_ir

#![allow(unused)]
fn main() {
    // {anchor}`crates.sage_ir.inference.numeric_domains`
    pub fn intersect(self, other: Self) -> Option<Self> {
        match (self, other) {
            (Self::Any, domain) | (domain, Self::Any) => Some(domain),
            (Self::Integer, Self::Integer) => Some(Self::Integer),
            (Self::Float, Self::Float) => Some(Self::Float),

}

See more source ↗

Implemented crates/sage-ir/src/check/infer_ctx.rs:2215–2220

sage_ir::check::infer_ctx · lib:sage_ir

#![allow(unused)]
fn main() {
    // {anchor}`crates.sage_ir.inference.numeric_domains`
    // {anchor}`crates.sage_ir.checking.body.isolated_completion`
    // {anchor}`crates.sage_ir.inference.terminal_obligations`
    pub fn finalize(&self) {
        // First consume every proof that current inference already enables.
        self.process_ready_obligations();

}

See more source ↗

Implemented crates/sage-ir/src/check/operator.rs:23–28

sage_ir::check::operator · lib:sage_ir

#![allow(unused)]
fn main() {
// {anchor}`crates.sage_ir.inference.numeric_domains`
pub(crate) fn check_binary_operator<'db>(
    cx: &InferCtx<'_, 'db>,
    scope: &Scope<'db>,
    operation: BinaryOp,
    left: Ptr<TyExpr<'db>>,

}

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::infer::unify::tests::domain_narrowing_follows_child_commit_and_discard

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.numeric_domains)]
    fn domain_narrowing_follows_child_commit_and_discard() {
        let mut egraph = VersionedEGraph::new();
        let mut stash = Stash::new();
        let any = variable(&mut egraph, &mut stash, Version::ROOT, Universe::ROOT);
        let integer = variable_in_domain(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            Universe::ROOT,
            InferDomain::Integer,
        );
        let any_index = variable_index(&stash, any);

        let discarded = egraph.branch_from(Version::ROOT);
        unify_in_probe(&mut egraph, &mut stash, discarded, any, integer).unwrap();
        assert_eq!(
            egraph.effective_domain(discarded, &stash, any),
            Some(InferDomain::Integer)
        );
        assert_eq!(
            egraph.effective_domain(Version::ROOT, &stash, any),
            Some(InferDomain::Any)
        );
        egraph.discard(discarded);
        assert_eq!(
            egraph.effective_domain(Version::ROOT, &stash, any),
            Some(InferDomain::Any)
        );

        let committed = egraph.branch_from(Version::ROOT);
        unify_in_probe(&mut egraph, &mut stash, committed, integer, any).unwrap();
        let effects = egraph.collapse_into(committed, Version::ROOT);
        assert_eq!(
            egraph.effective_domain(Version::ROOT, &stash, any),
            Some(InferDomain::Integer)
        );
        assert!(effects.wakes.contains(&any_index));
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::infer::unify::tests::exact_bounds_enforce_domains_transactionally

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.numeric_domains)]
    fn exact_bounds_enforce_domains_transactionally() {
        let mut egraph = VersionedEGraph::new();
        let mut stash = Stash::new();
        let integer = variable_in_domain(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            Universe::ROOT,
            InferDomain::Integer,
        );
        let float = stash.alloc(Ty::Float(FloatTy::F64));
        let revision = egraph.semantic_revision(Version::ROOT);

        assert!(matches!(
            try_set_bound(
                &mut egraph,
                &mut stash,
                Version::ROOT,
                integer,
                Bound::Exactly(float)
            ),
            Err(UnifyError::DomainConflict { .. })
        ));
        assert_eq!(egraph.get_bound(Version::ROOT, integer), Bound::None);
        assert_eq!(
            egraph.effective_domain(Version::ROOT, &stash, integer),
            Some(InferDomain::Integer)
        );
        assert_eq!(egraph.semantic_revision(Version::ROOT), revision);
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::infer::unify::tests::exact_bounds_join_the_validated_equality_class

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.numeric_domains)]
    fn exact_bounds_join_the_validated_equality_class() {
        let mut egraph = VersionedEGraph::new();
        let mut stash = Stash::new();
        let any = variable(&mut egraph, &mut stash, Version::ROOT, Universe::ROOT);
        let integer = variable_in_domain(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            Universe::ROOT,
            InferDomain::Integer,
        );

        try_set_bound(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            any,
            Bound::Exactly(integer),
        )
        .unwrap();
        assert_eq!(egraph.find(Version::ROOT, any), integer);
        assert_eq!(
            egraph.effective_domain(Version::ROOT, &stash, any),
            Some(InferDomain::Integer)
        );

        let float = stash.alloc(Ty::Float(FloatTy::F32));
        let revision = egraph.semantic_revision(Version::ROOT);
        assert!(matches!(
            try_set_bound(
                &mut egraph,
                &mut stash,
                Version::ROOT,
                any,
                Bound::Exactly(float),
            ),
            Err(UnifyError::DomainConflict { .. })
        ));
        assert_eq!(egraph.find(Version::ROOT, any), integer);
        assert_eq!(egraph.semantic_revision(Version::ROOT), revision);

        let mut egraph = VersionedEGraph::new();
        let mut stash = Stash::new();
        let any = variable(&mut egraph, &mut stash, Version::ROOT, Universe::ROOT);
        let float = stash.alloc(Ty::Float(FloatTy::F32));
        try_set_bound(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            any,
            Bound::Exactly(float),
        )
        .unwrap();
        let integer = variable_in_domain(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            Universe::ROOT,
            InferDomain::Integer,
        );
        assert!(matches!(
            try_unify(&mut egraph, &mut stash, Version::ROOT, integer, any,),
            Err(UnifyError::DomainConflict { .. })
        ));
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::infer::unify::tests::incompatible_transitive_domain_union_rolls_back

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.numeric_domains)]
    #[sage::test(crates.sage_ir.inference.transaction_isolation)]
    fn incompatible_transitive_domain_union_rolls_back() {
        let mut egraph = VersionedEGraph::new();
        let mut stash = Stash::new();
        let any = variable(&mut egraph, &mut stash, Version::ROOT, Universe::ROOT);
        let integer = variable_in_domain(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            Universe::ROOT,
            InferDomain::Integer,
        );
        let float = variable_in_domain(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            Universe::ROOT,
            InferDomain::Float,
        );
        try_unify(&mut egraph, &mut stash, Version::ROOT, any, integer).unwrap();
        let integer_root = egraph.find(Version::ROOT, any);
        let float_root = egraph.find(Version::ROOT, float);
        let revision = egraph.semantic_revision(Version::ROOT);

        assert!(matches!(
            try_unify(&mut egraph, &mut stash, Version::ROOT, any, float),
            Err(UnifyError::DomainConflict {
                left_domain: Some(InferDomain::Integer),
                right_domain: Some(InferDomain::Float),
                ..
            })
        ));
        assert_eq!(egraph.find(Version::ROOT, any), integer_root);
        assert_eq!(egraph.find(Version::ROOT, float), float_root);
        assert_eq!(
            egraph.effective_domain(Version::ROOT, &stash, any),
            Some(InferDomain::Integer)
        );
        assert_eq!(egraph.semantic_revision(Version::ROOT), revision);
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::infer::unify::tests::numeric_domains_accept_members_and_reject_other_families

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.numeric_domains)]
    fn numeric_domains_accept_members_and_reject_other_families() {
        for integer in [Ty::Int(IntTy::I128), Ty::Uint(UintTy::Usize)] {
            let mut egraph = VersionedEGraph::new();
            let mut stash = Stash::new();
            let variable = variable_in_domain(
                &mut egraph,
                &mut stash,
                Version::ROOT,
                Universe::ROOT,
                InferDomain::Integer,
            );
            let value = stash.alloc(integer);
            try_unify(&mut egraph, &mut stash, Version::ROOT, variable, value).unwrap();
            assert_eq!(egraph.find(Version::ROOT, variable), value);
        }

        for float in [FloatTy::F32, FloatTy::F64] {
            let mut egraph = VersionedEGraph::new();
            let mut stash = Stash::new();
            let variable = variable_in_domain(
                &mut egraph,
                &mut stash,
                Version::ROOT,
                Universe::ROOT,
                InferDomain::Float,
            );
            let value = stash.alloc(Ty::Float(float));
            try_unify(&mut egraph, &mut stash, Version::ROOT, variable, value).unwrap();
            assert_eq!(egraph.find(Version::ROOT, variable), value);
        }

        let mut egraph = VersionedEGraph::new();
        let mut stash = Stash::new();
        let integer = variable_in_domain(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            Universe::ROOT,
            InferDomain::Integer,
        );
        let float = stash.alloc(Ty::Float(FloatTy::F32));
        let revision = egraph.semantic_revision(Version::ROOT);
        assert!(matches!(
            try_unify(&mut egraph, &mut stash, Version::ROOT, integer, float),
            Err(UnifyError::DomainConflict { .. })
        ));
        assert_eq!(egraph.find(Version::ROOT, integer), integer);
        assert_eq!(egraph.semantic_revision(Version::ROOT), revision);

        let mut egraph = VersionedEGraph::new();
        let mut stash = Stash::new();
        let float = variable_in_domain(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            Universe::ROOT,
            InferDomain::Float,
        );
        let integer = stash.alloc(Ty::Uint(UintTy::U32));
        let revision = egraph.semantic_revision(Version::ROOT);
        assert!(matches!(
            try_unify(&mut egraph, &mut stash, Version::ROOT, float, integer,),
            Err(UnifyError::DomainConflict { .. })
        ));
        assert_eq!(egraph.find(Version::ROOT, float), float);
        assert_eq!(egraph.semantic_revision(Version::ROOT), revision);
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::infer::unify::tests::reported_error_recovery_is_admitted_by_numeric_domains

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.numeric_domains)]
    fn reported_error_recovery_is_admitted_by_numeric_domains() {
        let db = Database::default();
        let source = SourceFile::new(&db, "domain-recovery.rs".to_owned(), String::new());
        let mut diagnostics = Vec::new();
        let reported = report(
            &mut diagnostics,
            Diagnostic::error(
                Span::Absolute(AbsoluteSpan {
                    source: ParseSource::SourceFile(source),
                    start: 0,
                    end: 0,
                }),
                "test recovery",
            ),
        );
        assert_eq!(diagnostics.len(), 1);

        let mut egraph = VersionedEGraph::new();
        let mut stash = Stash::new();
        let error_ty = stash.alloc(Ty::Error(reported));
        let error_alias = variable(&mut egraph, &mut stash, Version::ROOT, Universe::ROOT);
        install_error_recovery(
            &mut egraph,
            &mut stash,
            Version::ROOT,
            error_alias,
            error_ty,
        )
        .unwrap();

        for domain in [InferDomain::Integer, InferDomain::Float] {
            let restricted = variable_in_domain(
                &mut egraph,
                &mut stash,
                Version::ROOT,
                Universe::ROOT,
                domain,
            );
            install_error_recovery(
                &mut egraph,
                &mut stash,
                Version::ROOT,
                restricted,
                error_alias,
            )
            .unwrap();
            assert_eq!(egraph.find(Version::ROOT, restricted), error_ty);
        }
    }
}

Conditional source: #[cfg(test)]

See more source ↗

Implemented sage_ir::check::infer::unify::tests::variable_union_intersects_domains_in_both_orders

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.numeric_domains)]
    fn variable_union_intersects_domains_in_both_orders() {
        for reverse in [false, true] {
            let mut egraph = VersionedEGraph::new();
            let mut stash = Stash::new();
            let any = variable(&mut egraph, &mut stash, Version::ROOT, Universe::ROOT);
            let integer = variable_in_domain(
                &mut egraph,
                &mut stash,
                Version::ROOT,
                Universe::ROOT,
                InferDomain::Integer,
            );
            let any_index = variable_index(&stash, any);
            let (left, right) = if reverse {
                (integer, any)
            } else {
                (any, integer)
            };

            let effects = try_unify(&mut egraph, &mut stash, Version::ROOT, left, right).unwrap();

            assert_eq!(
                egraph.effective_domain(Version::ROOT, &stash, any),
                Some(InferDomain::Integer)
            );
            assert_eq!(
                egraph.effective_domain(Version::ROOT, &stash, integer),
                Some(InferDomain::Integer)
            );
            assert!(effects.wakes.contains(&any_index));
        }
    }
}

Conditional source: #[cfg(test)]

See more source ↗

TODO sage_meta::todo::inference_numeric_domains

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(crates.sage_ir.inference.numeric_domains)]
    fn inference_numeric_domains() {
        // TODO: Complete the claim-specific verification matrix:
        // Egraph tests cover both union orders, transitivity, incompatible concrete bindings, branch
        // collapse/discard, revisions, and wakes. Source-driven completion tests cover contextual numeric
        // inference, generic propagation, selected-impl and where-clause constraints, preservation of an
        // ordinary `Any` operand before proof selection, unrelated-variable isolation, and explicit
        // recovery for otherwise unresolved integer and float classes. Tests prove this slice neither
        // narrows from operator spelling nor silently chooses `i32` or `f64`.
    }
}

See more source ↗

Implemented sage_test_harness::distinct_numeric_classes_take_independent_contextual_types

crates/sage-test-harness/tests/inference.rs · test:inference

#![allow(unused)]
fn main() {
#[test]
#[sage::test(crates.sage_ir.inference.numeric_domains)]
fn distinct_numeric_classes_take_independent_contextual_types() {
    compile_test! {
        source: indoc! {r#"
            fn example() -> (u8, u64, f32, f64) {
                (1, 2, 3.0, 4.0) //# ty
            }
        "#},
        observations: expect![[r#"
            src/lib.rs: literal `1`
              type: u8
            src/lib.rs: literal `2`
              type: u64
            src/lib.rs: literal `3.0`
              type: f32
            src/lib.rs: literal `4.0`
              type: f64
            src/lib.rs: tuple `(1, 2, 3.0, 4.0)`
              type: (u8, u64, f32, f64)
        "#]],
    }
}
}

See more source ↗

Implemented sage_test_harness::later_numeric_constraint_selects_an_impl_through_a_where_clause

crates/sage-test-harness/tests/inference.rs · test:inference

#![allow(unused)]
fn main() {
#[test]
#[sage::test(crates.sage_ir.inference.numeric_domains)]
fn later_numeric_constraint_selects_an_impl_through_a_where_clause() {
    compile_test! {
        source: indoc! {r#"
            enum Maybe<T> { None, Some(T) }
            trait Marker {}
            impl Marker for Maybe<u8> {}
            impl Marker for Maybe<bool> {}
            fn require_marker<T>(value: &Maybe<T>) where Maybe<T>: Marker {}
            fn example() {
                let mut value = Maybe::None;
                require_marker(&value);
                value = Maybe::Some(
                    22, //# ty
                );
                return;
            }
        "#},
        observations: expect![[r#"
            src/lib.rs: literal `22`
              type: u8
        "#]],
    }
}
}

See more source ↗

Implemented sage_test_harness::numeric_domains_reject_nonmembers

crates/sage-test-harness/tests/inference.rs · test:inference

#![allow(unused)]
fn main() {
#[test]
#[sage::test(crates.sage_ir.inference.numeric_domains)]
fn numeric_domains_reject_nonmembers() {
    compile_test! {
        source: indoc! {r#"
            fn integer_as_bool() -> bool {
                22 //# ERROR
            }
            fn integer_as_float() -> f32 {
                22 //# ERROR
            }
            fn float_as_integer() -> u32 {
                1.0 //# ERROR
            }
        "#},
        diagnostics: expect![[r#"
            error: type mismatch: expected `bool`, found an integer
             --> src/lib.rs:1:30
              |
            1 |   fn integer_as_bool() -> bool {
              |  _________________________----_^
              | |                         |
              | |                         expected `bool` because of return type
            2 | |     22 //# ERROR
            3 | | }
              | | ^
              | |_|
              |   found an integer
            error: type mismatch: expected `f32`, found an integer
             --> src/lib.rs:4:30
              |
            4 |   fn integer_as_float() -> f32 {
              |  __________________________---_^
              | |                          |
              | |                          expected `f32` because of return type
            5 | |     22 //# ERROR
            6 | | }
              | | ^
              | |_|
              |   found an integer
            error: type mismatch: expected `u32`, found a floating-point type
             --> src/lib.rs:7:30
              |
            7 |   fn float_as_integer() -> u32 {
              |  __________________________---_^
              | |                          |
              | |                          expected `u32` because of return type
            8 | |     1.0 //# ERROR
            9 | | }
              | | ^
              | |_|
              |   found a floating-point type"#]],
    }
}
}

See more source ↗

Implemented sage_test_harness::return_context_constrains_numeric_literals_through_generic_calls

crates/sage-test-harness/tests/inference.rs · test:inference

#![allow(unused)]
fn main() {
#[test]
#[sage::test(crates.sage_ir.inference.numeric_domains)]
fn return_context_constrains_numeric_literals_through_generic_calls() {
    compile_test! {
        source: indoc! {r#"
            fn id<T>(value: T) -> T { value }
            fn integer() -> u16 {
                id(22) //# ty
            }
            fn float() -> f32 {
                id(1.0) //# ty
            }
        "#},
        observations: expect![[r#"
            src/lib.rs: path `id`
              type: fn(u16) -> u16
            src/lib.rs: literal `22`
              type: u16
            src/lib.rs: call `id(22)`
              type: u16
            src/lib.rs: path `id`
              type: fn(f32) -> f32
            src/lib.rs: literal `1.0`
              type: f32
            src/lib.rs: call `id(1.0)`
              type: f32
        "#]],
    }
}
}

See more source ↗

Implemented sage_test_harness::unconstrained_numeric_literals_report_errors_instead_of_defaulting

crates/sage-test-harness/tests/inference.rs · test:inference

#![allow(unused)]
fn main() {
#[test]
#[sage::test(crates.sage_ir.inference.numeric_domains)]
fn unconstrained_numeric_literals_report_errors_instead_of_defaulting() {
    // Sage intentionally diagnoses unresolved numeric domains; rustc defaults
    // these literals to i32/f64 and accepts the same source.
    compile_test! {
        source: indoc! {r#"
            fn integer() { let value = 22; } //# ERROR if SAGE
            //# ty
            fn float() { let value = 1.0; } //# ERROR if SAGE
            //# ty
        "#},
        observations: expect![[r#"
            src/lib.rs: literal `22`
              type: <error>
            src/lib.rs: block `{ let value = 22; }`
              type: ()
            src/lib.rs: literal `1.0`
              type: <error>
            src/lib.rs: block `{ let value = 1.0; }`
              type: ()
        "#]],
        diagnostics: expect![[r#"
            error: could not infer an integer type
             --> src/lib.rs:1:1
              |
            1 | fn integer() { let value = 22; } //# ERROR if SAGE
              | ^
            error: could not infer a floating-point type
             --> src/lib.rs:3:1
              |
            3 | fn float() { let value = 1.0; } //# ERROR if SAGE
              | ^"#]],
    }
}
}

See more source ↗

Review: Accepted · Codex /root/anchor_094.

Reviewed the entire numeric_domains claim, five associated implementation files and all thirteen test entries (seven egraph/unit tests, five source-driven tests and one TODO). Captured the inference design, numeric-inference RFD domain/no-default decision and compile-test macro/preparation/assertion and observation helpers. Source inspection only; no behavioral suites rerun and no source changes.

The claim requires whole-equality-class domains narrowed only by intersection, transactional commit/rollback/revision/wake semantics, concrete numeric choices justified by constraints, no operator-token narrowing and no quiescence default. version.rs defines Any intersected with a restriction as that restriction, same-family intersections unchanged and Integer/Float intersection failure. egraph.rs effective_domain follows the representative and version ancestry; set_domain_in checks narrowing and marks semantic changes/wakes. unify.rs checks intersections or concrete membership before committing and uses child probes to discard failed relations. Exact bounds join validated equality classes rather than bypassing domain checks. infer_ctx.rs finalization resolves enabled constraints and final bounds, then diagnoses unresolved classes and installs explicit error recovery; it does not choose i32/f64 for integer/float domains. The separate never fallback is not numeric defaulting. operator.rs maps overloadable spelling to a trait-method obligation with separate operands; signature/proof relationships supply constraints, not a blanket numeric restriction or operand equality from the token.

The unit assertions are specific: variable_union_intersects_domains_in_both_orders requires Integer for both representatives and a wake for the narrowed Any variable; domain_narrowing_follows_child_commit_and_discard checks child-only visibility, unchanged parent after discard and parent narrowing plus wake after collapse; incompatible_transitive_domain_union_rolls_back rejects Integer/Float after an earlier Any/Integer union and preserves both roots/domain/revision. numeric_domains_accept_members_and_reject_other_families accepts signed/unsigned integer representatives and f32/f64 while rejecting cross-family bindings without root/revision changes. exact_bounds_enforce_domains_transactionally rejects an incompatible exact float bound without changing bound/domain/revision. exact_bounds_join_the_validated_equality_class checks transitive restriction through exact bounds, subsequent conflict rollback and rejection when a prebound float meets Integer. reported_error_recovery_is_admitted_by_numeric_domains creates an actual diagnostic and verifies Integer/Float classes can resolve through an error alias to its Ty::Error. This is recovery, not successful numeric inference.

The five compile tests expose exact source and expectations. distinct_numeric_classes_take_independent_contextual_types requires independent u8/u64/f32/f64 literal and tuple types. return_context_constrains_numeric_literals_through_generic_calls requires matching id signatures, literals and calls at u16/f32. later_numeric_constraint_selects_an_impl_through_a_where_clause requires 22 to become u8 with competing Maybe<u8>/Maybe<bool> implementations. numeric_domains_reject_nonmembers requires exact diagnostics for integer-to-bool, integer-to-float and float-to-integer. unconstrained_numeric_literals_report_errors_instead_of_defaulting requires both literal types to be <error> and exact integer/float inference diagnostics, using SAGE-specific error annotations because rustc defaults those programs. The captured harness runs real Sage checking, matches supplied observations/diagnostics exactly and rejects unexpected diagnostics; it independently checks compiler annotations, without claiming rustc agrees with Sage's intentional no-default behavior.

The inference_numeric_domains TODO retains the full verification matrix beyond these examples, notably ordinary Any operands before proof selection and direct proof that operator spelling cannot narrow them, plus exhaustive completion/selected-impl/isolation combinations. Its prerequisite is completing and associating those targeted domain/solver/operator tests. It remains deferred evidence rather than being treated as an additional passing test; the substantial ordinary assertions do not erase that limitation. All implementation entries, test entries and claim requirements are accounted for. No concrete defect was identified in the inspected paths and no additional edits are requested.

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