Tutorial: proof harness patterns

[tedinski]

We should document common patterns for proof harnesses, along with explanations/justifications for why they're common or interesting to know about.

For example:

No assumptions or assertions

fn check_fn() {
  let input = kani::any();
  function_under_test(input);
}

It might be surprising to someone used to writing test harnesses to see a harness with no assertions, but remember that we're checking for panic-freedom by default. (Kind of like how a unit test would ensure an exception isn't thrown by default in Java.) Most functions require some assumptions to write interesting proof harnesses, but many do not. For example, function_under_test might return a Result, and we may wish to prove that it's handling all possible error cases by returning an error Result rather than by panicking.

Ideas for more welcome

• Assumptions, but no assertions
• Basic validity assertions
• Meets specification
• Agrees with model
• Bounding input sizes

[tedinski]

Possibly this should be written less as patterns and more as "writing specifications"

A reasonable progression might start with:

1. No assertion in harness. ("What Kani checks for" so we still find lack of panics, assertions, termination)
2. Instrumenting your code. Adding assert or debug_assert
3. Object/representation invariants
4. A "write the specification for sort" tutorial specifically

Then we should mine the property testing literature for more suggestions about how to write specifications, as property tests are often interesting kinds of specifications. Including things like

5. Model-based checking (compare output of optimized implementation against high-level "oracle" implementation)
6. Metamorphic testing
7. other good ideas in the community