improve the proptest of the resolver.

[Eh2406]

We have some proptests that are used to fuzz the resolver. They were introduced in #5921. However, not all the good ideas from that discussion got implemented in the initial push. This is a list of good ideas related to using proptests on the resolver to act as a hub.

The current strategy does not:

• generate features.
• generate dev-dependencies.
• generate system specific dependencies.
• generate patch sources. cc Handle activation conflicts for [patch] sources #7118

The current properties do not test:

• If resolution was successful, then all the transitive requirements are met.
• The resolver agrees with some orical. Maybe an SAT solver, or the cargo that we are being built with, or the last cargo on crates.io.
• Anything about error messages.
• @maurer suggested testing for consistency. Same registry, same cargo version, same lockfile, every time.
• @maurer suggested a pareto optimality property (if all else stays the same, but new package versions are released, we don't get a new lockfile where every version is <= the old one, and at least one is < the old one)

[Eh2406]

Cc, @necaris

[Eh2406]

Another property, that I think will shrink well, that will take some design work, is order randomization.
For example, we address more constrained deps before lease constrained once, but we do not guarantee what order we address equale constrained deps. We guarantee that it is deterministic, but not what it is. We use BinaryHeap's default, I think it is FIFO, we could test that resolve(..., FIFO).is_ok() == resolve(..., FILO).is_ok().

[Eh2406]

Just came across this excellent summary of how to make properties.

[Eh2406]

The resolver agrees with some orical.

varisat is on crates.io, and may work. At the moment @jix recommendations for xor constraints are in this comment.