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_via / relation-axiom

relation-axiom
LineCoverageSource
36N/A(let (skel_c, parameters_c) = rel_1.debone())
37N/A(let (skel_g, parameters_g) = rel_2.debone())
38✗(if skel_c == skel_g)
39✗(if parameters_c == parameters_g)
──────── ("relation-axiom")
418(prove_via(_decls, env, _assumptions, WcData::Relation(rel_1), WcData::Relation(rel_2)) => Constraints::none(env))

8 tests exercised this rule:

Source location: crates/formality-rust/src/prove/test/eq_assumptions.rs:15

#[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

#[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: tests/borrowck.rs:4618

#[test]
fn flow_sensitive_invariance_use_it() {
    // [nll]: rustc errors
    FormalityTest::new(feature_gate_program(
        NLL_GATE,
        FLOW_SENSITIVE_INVARIANCE_USE_IT,
    ))
    .skip_execute()
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);

    // [polonius]: rustc errors
    FormalityTest::new(feature_gate_program(
        POLONIUS_ALPHA_GATE,
        FLOW_SENSITIVE_INVARIANCE_USE_IT,
    ))
    .skip_execute()
    .err(expect_test::expect![[r#"
        crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

        crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);

    // [legacy]: rustc passes
    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        FLOW_SENSITIVE_INVARIANCE_USE_IT,
    ))
    .skip_execute()
    .ok();
}
Proof tree
… (200 of 1182 nodes shown)

Source location: tests/borrowck.rs:4711

#[test]
fn flow_sensitive_invariance_same_region() {
    // [nll]: rustc passes.
    FormalityTest::new(feature_gate_program(
        NLL_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();

    // [polonius]: rustc passes.
    FormalityTest::new(feature_gate_program(
        POLONIUS_ALPHA_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();

    // [legacy]: rustc passes.
    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();
}
Proof tree
… (200 of 1302 nodes shown)

Source location: tests/borrowck.rs:4719

#[test]
fn flow_sensitive_invariance_same_region() {
    // [nll]: rustc passes.
    FormalityTest::new(feature_gate_program(
        NLL_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();

    // [polonius]: rustc passes.
    FormalityTest::new(feature_gate_program(
        POLONIUS_ALPHA_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();

    // [legacy]: rustc passes.
    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();
}
Proof tree
… (200 of 1218 nodes shown)

Source location: tests/borrowck.rs:4727

#[test]
fn flow_sensitive_invariance_same_region() {
    // [nll]: rustc passes.
    FormalityTest::new(feature_gate_program(
        NLL_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();

    // [polonius]: rustc passes.
    FormalityTest::new(feature_gate_program(
        POLONIUS_ALPHA_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();

    // [legacy]: rustc passes.
    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
    ))
    .skip_execute()
    .ok();
}
Proof tree
… (200 of 1190 nodes shown)

Source location: tests/projection.rs:36

#[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} }}"]);
}
Proof tree

Source location: tests/well_formed_struct.rs:17

fn main() -> () {
    exists<'y> {
        let a: u32 = 22_u32;
        let f: Foo<'y> = Foo::<'y> { y: &'y a };
    }
}
Proof tree
… (200 of 1159 nodes shown)