Add abstract interface to Invariant

[sim642]

This adds the intended abstract interface to clarify that "Invariants for witnesses" are not just CIL expressions: #1665 (comment).

TODO

• What to do about precondition loop invariants?
• Make WitnessUtil.InvariantExp work on Invariant.t instead of exp for full type-safety?

[sim642]

The generation of our proposed precondition loop invariants performs EvalInt queries with witness invariants, assuming they have implicit casts, etc like expressions from the program.
This would no longer be the case with #1665.

So we have to decide what to do here:

1. If we don't want to pursue precondition loop invariants and keep them, they could be removed, avoiding the issue.
2. Otherwise, Invariant.t might need to be turned into a pair of CIL expressions (with and without implicit casts) behind the abstraction. This might be desirable in the long run for Linear Two Variable Equality Domain Refining Value Domain #1635, although that uses separate expression construction from invariant anyway.

[michael-schwarz]

I think we should keep them, especially if we intend to work with LMU to extend the witness format.

[sim642]

This probably needs some separate discussion if this is still the kind of entry/invariant we want to propose. LMU+Freiburg have recently proposed function contracts as well: https://arxiv.org/abs/2501.12313.

[michael-schwarz]

Yeah! At first glance, I think we can basically encode these in the invariants as a conjunction of implications of the form pre_i \implies post_i where pre_i uses these \at(_, Pre) predicates (which would mean we need an ACSL parser, or some hacks such as functions at and a constant Pre).