[red-knot] Property tests

[sharkdp]

Summary

This PR adds a new property_tests module with quickcheck-based tests that verify certain properties of types. The following properties are currently checked:

• is_equivalent_to:
  • is reflexive: T is equivalent to itself
• is_subtype_of:
  • is reflexive: T is a subtype of T
  • is antisymmetric: if S <: T and T <: S, then S is equivalent to T
  • is transitive: S <: T & T <: U => S <: U
• is_disjoint_from:
  • is irreflexive: T is not disjoint from T
  • is symmetric: S disjoint from T => T disjoint from S
• is_assignable_to:
  • is reflexive
• negate:
  • is an involution: T.negate().negate() is equivalent to T

There are also some tests that validate higher-level properties like:

• S <: T implies that S is not disjoint from T
• S <: T implies that S is assignable to T
• A singleton type must also be single-valued

These tests found a few bugs so far:

• [red-knot] Minor: fix Literal[True] <: int #14177
• [red-knot] Fix intersection simplification for ~Any/~Unknown #14195
• [red-knot] Fix is_assignable_to for unions #14196
• [red-knot] Fix is_disjoint_from for class literals #14210
• [red-knot] Incorrect subtyping behavior of Literal instances and _SpecialForm #14731

Some additional notes:

• Quickcheck-based property tests are non-deterministic and finding counter-examples might take an arbitrary long time. This makes them bad candidates for running in CI (for every PR). We can think of running them in a cron-job way from time to time, similar to fuzzing. But for now, it's only possible to run them locally (see instructions in source code).
• Some tests currently find false positive "counterexamples" because our understanding of equivalence of types is not yet complete. We do not understand that int | str is the same as str | int, for example. These tests are in a separate property_tests::flaky module.
• Properties can not be formulated in every way possible, due to the fact that is_disjoint_from and is_subtype_of can produce false negative answers.
• The current shrinking implementation is very naive, which leads to counterexamples that are very long (str & Any & ~tuple[Any] & ~tuple[Unknown] & ~Literal[""] & ~Literal["a"] | str & int & ~tuple[Any] & ~tuple[Unknown]), requiring the developer to simplify manually. It has not been a major issue so far, but there is a comment in the code how this can be improved.
• The tests are currently implemented using a macro. This is a single commit on top which can easily be reverted, if we prefer the plain code instead. With the macro:

  // `S <: T` implies that `S` can be assigned to `T`.
  type_property_test!(
      subtype_of_implies_assignable_to, db,
      forall types s, t. s.is_subtype_of(db, t) => s.is_assignable_to(db, t)
  );

  without the macro:

  /// `S <: T` implies that `S` can be assigned to `T`.
  #[quickcheck]
  fn subtype_of_implies_assignable_to(s: Ty, t: Ty) -> bool {
      let db = get_cached_db();
  
      let s = s.into_type(&db);
      let t = t.into_type(&db);
  
      !s.is_subtype_of(&*db, t) || s.is_assignable_to(&*db, t)
  }

Test Plan

while cargo test --release -p red_knot_python_semantic --features property_tests types::property_tests; do :; done

[carljm]

This is awesome! Thank you for doing this, I've been wanting to explore this. I think property testing is very well suited to testing type relation invariants, and I do think we should move forward with actually landing this.

[carljm]

This is great, thank you!

[carljm]

Another useful property we could test here when we fix the issue about is_subtype_of and non-fully-static types is that a non-fully-static type never participates in subtyping. (This assumes that we add Type::is_fully_static so we can check this predicate.)

[sharkdp]

Added as a task in #14524

[MichaReiser]

I think you can just ignore them and they can then be run by name

[sharkdp]

I think you can just ignore them and they can then be run by name

That's an option, but I wanted to mark some of them as #[ignore]d for another reason as well (because they yield many false positives right now). I guess I can also just comment them out for now.. but I don't like commented out committed code :-/

[MichaReiser]

I'd prefer ignoring them with different reasons. Commented out code defeats the reason why we're merging the tests in the first place

[MichaReiser]

I find the macro fairly hard to read. What I understand is that their primary benefit is to reduce the repetition of creating the cached db and dereferencing it.

• How much faster is reusing the db over creating a new database?
• Have you considered adding a snapshot method to the database instead of locking it? Databases are thread safe and can be shared (for as long as you don't update the db with a &mut Db reference

        pub fn snapshot(&self) -> Self {
            Self {
                storage: self.storage.clone(),
                files: self.files.snapshot(),
                system: self.system.clone(),
                vendored: self.vendored.clone(),
                events: Arc::clone(&self.events),
            }
        }

A test then becomes

    #[test]
    #[quickcheck_macros::quickcheck]
    fn equivalent_to_is_reflexive2(t: crate::types::tests::Ty) -> bool {
        let db = get_cached_db();
        let t = t.into_type(&db);
        t.is_equivalent_to(&db, t)
    }

Which I don't find too bad

[sharkdp]

How much faster is reusing the db over creating a new database?

Three orders of magnitude. It's essential. I found some bugs only after I added this optimization.

• Have you considered adding a snapshot method to the database instead of locking it

I have not. Would the benefit be to get rid of the let db = &*db;, or do you think that would be faster?

I find the macro fairly hard to read

Because macros are hard to read, or because this particular macro is hard to read? 😄

I don't disagree, but it's also not like we're hiding lots of complexity in there. It's really just a boilerplate-reduction macro. I personally care much more about the readability of the individual tests. The macro is ugly, yes. But I won't have to read the macro code again when writing new tests.

A test then becomes [...] Which I don't find too bad

Well, you picked the easiest example there ;-). With just one type and no logical implication. Did you see the macro-vs-non-macro comparison in the PR description? Or this example, which has three types:

#[quickcheck]
fn subtype_of_is_transitive(s: Ty, t: Ty, u: Ty) -> bool {
    let db = get_cached_db();
    let db = &*db;
    let s = s.into_type(db);
    let t = t.into_type(db);
    let u = u.into_type(db);

    !(s.is_subtype_of(db, t) && t.is_subtype_of(db, u)) || s.is_subtype_of(db, u)
}

type_property_test!(
    subtype_of_is_transitive,
    db,
    (s, t, u),
    s.is_subtype_of(db, t) && t.is_subtype_of(db, u) => s.is_subtype_of(db, u)
);

their primary benefit is to reduce the repetition of creating the cached db and dereferencing it

It also removes the necessity for lots of let t = t.into_type(db); lines, and allows us to write logical implications using premise => conclusion instead of !(premise) || (conclusion).

Let me know what you think. I'm going to be okay if we remove it again 😄.

[MichaReiser]

I have not. Would the benefit be to get rid of the let db = &*db;, or do you think that would be faster?

It would allow you to remove the mutex guard and the deref (you still need to use &db when calling any function)

Because macros are hard to read, or because this particular macro is hard to read? 😄

It's somewhat both. I had to expand the macro to understand what the different parts map to. Like what's up with the (s, t, u)? which part is even the assertion? Some extra documentation might help.

Did you see the macro-vs-non-macro comparison in the PR description? Or this example, which has three types:

I admit, I did not! I see how it simplifies the code a bit, but it doesn't significantly reduce the number of lines.

Could we implement into_type for tuples so that you can keep writing (s, t, u) = (s, t, u).into_types(db)?

It also removes the necessity for lots of let t = t.into_type(db); lines, and allows us to write logical implications using premise => conclusion instead of !(premise) || (conclusion).

I do like that. Maybe we can limit the macro part to just that?

I'm not opposed to keeping the macros. I just had to expand them, and I still spent about 5 minutes trying to figure out what was going on. But I'm also not sure if it's worth it if you spend more time on it.

[sharkdp]

Like what's up with the (s, t, u)? which part is even the assertion?

These are valid concerns. I now pushed another commit where I change the syntax to the following:

type_property_test!(
    subtype_of_implies_assignable_to, db,
    forall types s, t. s.is_subtype_of(db, t) => s.is_assignable_to(db, t)
);

The intention is that it reads like a mathematical property ∀ S, T. ….

I also simplified the macro definition (only two clauses instead of four), clarified the variable names and added some documentation.

I kind of like how this looks, and would merge it for now. I'm happy to revisit it though if I get more feedback on it (from you or others).

It would allow you to remove the mutex guard and the deref (you still need to use &db when calling any function)

I'll note it down as a task for me (low priority), thanks.

[MichaReiser]

Thanks. I like this much more!