Tracking of soundness for proofs and refutations

[Philipp15b]

This issue aims to specify the next evolution of calculus annotations (#7). The goal is to incorporate soundness of refutations as well, whereas the current design only allows guardrails for proofs.

• Sound proofs: If Caesar says the encoded program verifies, then the actual program satisfies the specification as well.
• Sound refutations: If Caesar prints a counter-example to verification, then the actual program also has a counter-example.

1. Proof rules encoded based on decision of lfp/gfp semantics only (not proc vs. coproc).
   • Proof rules such as @induction or @unroll should now obtain the direction from a calculus annotation, or, if that does not exist, based on the direction of the (co)proc. A proc is assumed to use gfp, and a coproc is assumed to use lfp semantics by default.
   • It is not a hard error anymore to use e.g. @induction in a proc annotated with @wp. If there is a @wp annotation, we just encode with the corresponding lfp encoding.
2. Tracking under- or over-approximations.
   • Caesar should have an internal analysis that collects statements that encode "real" code, collecting a list of Spans and a Direction. Proof rules may use analysis information from blocks nested in it, such as their loop body.
   • The @induction encoding for gfps under-approximates, and over-approximates for lfps.
   • The @unroll encoding for gfps over-approximates, and under-approximates for lfps.
   • The other proof rules are exact and require exact loop bodies, according to the docs.
3. From proc direction and approximation analysis to AbstractionKind.
   • If we're in a proc and all approximating statements under-approximating, then we have AbstractionKind::Proof. Dual for coproc and over-approximating. This corresponds to the guarantees we checked before with the calculus annotations.
   • Conversely, if we're in a proc and all statements are over-approximating, then we have AbstractionKind::Refutation. Dual for coproc and under-approximating. This means that if we get a counter-example, then we know that the real program also fails the specification.
   • If there's no approximations in the body, then we have AbstractionKind::Exact. If there's a mix, then we have AbstractionKind::Unknown.
4. Explaining verification output.
   • If the verification result is "verified", but AbstractionKind is not either Proof or Exact, then throw an error and let the user know (as is done now).
   • If the verification result is a counterexample, but the AbstractionKind is not either Refutation or Exact, then add a note to the error that the error might very well be spurious. In case of AbstractionKind::Refutation, let the user know that the error is real and not spurious.
   • In case of a notice, we should highlight the relevant "wrong" approximating statements in the diagnostic based on the collection before.

Notes:

• Once Limited functions #54 by @ole-thoeb gets merged, the way that recursive functions are encoded might also result in additional approximations.
• This is all orthogonal to the ModelConsistency introduced for slicing.