Exploit parallelism

[alastairreid]

cargo-verify currently exploits parallelism between verification targets but not within each individual verification.
To exploit parallelism. we need some way of doing a case split on input values (which hopefully makes values more concrete).
It is not clear whether this needs to be under user control (allowing the user to indicate case splits that may make sense) or whether it can be automatic.

Some places to get ideas from

• Proptest-derive modifiers
  (see also recursive strategies).
  Weights are used to modify the probability of generating particular random values.
  In a verification context, do they also indicate something about useful case splits or the number of parallel verification processes to assign to a particular case or the order in which to explore case splits in a sequential verification effort?

• DeepState: Symbolic Unit Testing for C and C++ - sections II, III and IV describe various optimizations

Challenges:

• Is there an effective way to apply sharding?
• If we add hints to aid verification:
  • do they work for all verification tools?
  • do different tools need conflicting annotations?
  • can fuzz-testers use the annotations as well?