Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: prove_predicate / assumption

assumption
LineCoverageSource
47✗(a in assumptions)
4834(prove_via(decls, env, assumptions, a, goal) => c)
──────── ("assumption")
5023(prove_predicate(decls, env, assumptions, Predicate::AtomicPredicate(goal)) => c)

23 tests exercised this rule:

Source location: crates/formality-rust/src/prove/test/eq_assumptions.rs:15 (all coverage from this test)

#[test]
fn test_a() {
    test_prove(
        Program::empty(),
        term("{} => {for<T, U> if {T = u32, U = Vec<T>} U = Vec<u32>}"),
    )
    .assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree

Source location: crates/formality-rust/src/prove/test/eq_assumptions.rs:33 (all coverage from this test)

#[test]
fn test_normalize_assoc_ty() {
    test_prove(
        Program::empty(),
        term("{} => {for<T> if { <T as Iterator>::Item = u32 } <T as Iterator>::Item = u32}"),
    )
    .assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree

Source location: crates/formality-rust/src/prove/test/eq_partial_eq.rs:25 (all coverage from this test)

#[test]
fn eq_implies_partial_eq() {
    let assumptions: Predicates = Predicates::t();
    let goal: Predicate = term("for<T> if {Eq(T)} PartialEq(T)");
    let constraints = prove(decls(), (), assumptions, goal);
    constraints.assert_ok(
    expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree

Source location: tests/basic_tests.rs:58 (all coverage from this test)

#[test]
fn hello_world() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<T> where T: Bar<Self>, Self: Baz {}

        trait Bar<T> where T: Baz {}

        trait Baz {}

        impl Baz for u32 {}

        impl Bar<u32> for u32 {}
        impl<T> Bar<T> for () where T: Baz {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 3755 nodes shown)

Source location: tests/basic_tests.rs:149 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_trait_impl_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        impl<T> B for T where for<U> u32: A<U> { }
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:179 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_neg_trait_impl_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        impl<T> !A<T> for u32 where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/borrowck.rs:4831 (all coverage from this test)

fn use_it<'a, 'b>() -> u32 {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}
Proof tree
… (200 of 3596 nodes shown)

Source location: tests/borrowck.rs:4896 (all coverage from this test)

fn use_it_but_its_the_same_region<'a, 'b>() -> u32 where 'a: 'b, 'b: 'a {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}
Proof tree
… (200 of 3604 nodes shown)

Source location: tests/borrowck.rs:4970 (all coverage from this test)

fn f() -> u32 {
    exists<'r0> {
        let v: u32 = 0_u32;
        let w: Wrapper<'r0> = Wrapper::<'r0> { value: &'r0 v };
        return *w.value;
    }
}
Proof tree
… (200 of 3603 nodes shown)

Source location: tests/coherence_overlap.rs:237 (all coverage from this test)

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        #![feature(negative_impls)]
        trait CoreTrait {}
        struct CoreStruct {}
        impl !CoreTrait for CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/coherence_overlap.rs:322 (all coverage from this test)

#[test]
fn u32_T_where_T_Not_impls() {
    FormalityTest::new(crates![crate core {
        trait Foo {}
        impl Foo for u32 {}
        impl<T> Foo for T where T: Not {}

        trait Not {}
    }])
    .skip_execute()
    .ok()
}

Proof trees omitted for the remaining 13 tests; each one is on its test’s page in Coverage by test.

Source location: tests/coherence_overlap.rs:587 (all coverage from this test)

#[test]
fn is_local_unknowable_trait_ref() {
    FormalityTest::new(crates![crate core {
        trait Project {
            type Assoc: [];
        }

        impl<T> Project for T {
            type Assoc = T;
        }

        trait Foo<U> { }
    },
    crate foo {
        struct LocalType {}

        trait Overlap<U> {}
        impl<T, U> Overlap<U> for T
        where
            <T as Project>::Assoc: Foo<U> {}
        impl<T> Overlap<LocalType> for () {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/consts.rs:27 (all coverage from this test)

#[test]
fn ok() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<const C> where type_of_const C is bool {}
        trait Bar<const C> where type_of_const C is u32 {}

        impl<const C> Foo<C> for u32 where type_of_const C is bool {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/consts.rs:100 (all coverage from this test)

#[test]
fn generic_match() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<const C> where type_of_const C is bool {}

        // Here, the impl matches the trait bound.
        impl<const C> Foo<C> for u32 where type_of_const C is bool {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/consts.rs:166 (all coverage from this test)

Source location: tests/drop.rs:43 (all coverage from this test)

Source location: tests/mir_typeck.rs:987 (all coverage from this test)

fn foo<'a, T>(v1: &'a T) -> T
where
    T: Copy,
    T: 'a,
{
    exists<'r0> {
        let v2: T = *v1;
        return v2;
    }
}

Source location: tests/mir_typeck.rs:1466 (all coverage from this test)

fn main() -> () { outer::<u32>(); }
}])
tc_ok()
);
}

#[test]
bare_fn_value_with_satisfied_where_clause() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require() -> () where u32: Marker {}
fn main() -> () { require; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}

#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
 --> lib.rs
  |
7 | pub fn outer<'a00, 'a01>() -> () {
  |              ----  ---- lifetime `'a01` defined here
  |              |
  |              lifetime `'a00` defined here
8 |     require::<'a00, 'a01>;
  |     ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
  |
  = help: consider adding the following bound: `'a00: 'a01`

error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}

ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

Source location: tests/projection.rs:36 (all coverage from this test)

#[test]
fn normalize_basic() {
    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> exists<U> {} => { <Vec<T> as Iterator>::Item = U }",
    )
    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <Vec<!ty_1> as Iterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]);

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> {} => { Iterator(Vec<T>), <Vec<T> as Iterator>::Item = T }",
    )
    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> { Iterator(T), <T as Iterator>::Item = Foo } => { <T as Iterator>::Item = Foo }",
    ).assert_ok(
        expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]
    );

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = U }",
    )
    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <!ty_1 as Iterator>::Item} }}"]);

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> { Iterator(T) } => { <T as Iterator>::Item = <T as Iterator>::Item }",
    )
    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = <U as Iterator>::Item }",
    ).assert_ok(
    expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, Constraints { env: Env { variables: [!ty_1, ?ty_3, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => Vec<<!ty_1 as Iterator>::Item>, ?ty_3 => <!ty_1 as Iterator>::Item} }}"]);
}

Source location: tests/references.rs:36 (all coverage from this test)

Source location: tests/sized_trait.rs:175 (all coverage from this test)

Source location: tests/well_formed_struct.rs:17 (all coverage from this test)

fn main() -> () {
    exists<'y> {
        let a: u32 = 22_u32;
        let f: Foo<'y> = Foo::<'y> { y: &'y a };
    }
}

Source location: tests/well_formed_trait_ref.rs:19 (all coverage from this test)

#[test]
fn dependent_where_clause() {
    FormalityTest::new(crates![crate foo {
        trait Trait1 {}

        trait Trait2 {}

        struct S1<T> where T: Trait1 {
            dummy: T,
        }

        struct S2<T> where T: Trait1, S1<T> : Trait2 {
            dummy: T,
        }
    }])
    .skip_execute()
    .ok()
}

How to read this page