Add panics_if precondition to express panic-freedom

[tautschnig]

Implements a solution towards #3567, following up on the RFC discussion in #3893.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[remi-delmas-3000]

Could we instead name that clause may_panic_if ? the current encoding checks that the function does not panic when the negation of the condition holds, not that it panics when the condition holds. The function may or may not panic when this condition does not hold.

Suggestion: add two clauses:

• no_panic_if(P), specifies panic-freedom conditions (passes if function does not panic whenever the condition holds)

  • verified by checking that function does not panic under kani::assume(P);
  • or by checking that when function panics then !P held initially on inputs

• panic_if(Q): specifies panic conditions (passes if function panics whenever the condition holds)

  • verified by checking that function panics under kani::assume(Q);
    • or by check that when function does not panics then !Q held initially on inputs

• consistency check: assert!(!P || !Q); (are the conditions disjoint?)

• completeness check : assert!(P || Q); (are we covering the whole input space?)

• if both consistency and completeness hold we have a partition of the input domain