LTL and Staged update

[mmontin]

The LTL and Staged aspects of cooked have been left as is for years (and for good reasons), but it is finally time to update them.

The main reason for the changes is the following observation: while we can express applying a modification at every step in a trace (where it must succeed everywhere), or forking at every location where it actually applies, we cannot express something like "apply a modification everywhere where it can be applied, and leave the other steps as is", which is actually very useful. For instance, the new 'labelled' idiom allows to targets transaction with a specific label, but there is no way to have it fail if the label is not present (which would be the expected behavior when used with somewhere), but still target several transactions in a trace with the label.

A new idiom, let's call it 'wheneverPossible' is in fact needed.

However, this idiom cannot be expressed for good reasons, as it requires to ensure that every step that have not been modified actually could not be modified. Otherwise, the modification should have been applied. The missing piece of the puzzle turns out to be the negation, with an appropriate semantics, where (not A) means that applying A at the current time step would fail (i.e. yield the empty set of traces). At the time of the creation of LTL, we did not find a proper way to handle negation (and implication for that matter, which spawns out of it) and also did not have any use case where it would be relevant, and thus we omitted it, arguing that it was not sound in an operational setting as ours, which seemed right at the time.

However, with the semantics of negation given above, it is actually sound. It is even possible to give a meaning to formula previously seen as obscure, such as "Next A implies B". This is the main focus of this PR: implementing such a semantics for negation, and allowing to speak about implication, or "wheneverPossible".

The main changes to make that possible are as follows:

• LtlNot is added to the Ltl builtins
• ltlSimpl moves all occurrences of LtlNot to the leaves of the formula tree
• the "now" part of nowLaterList is now a list of requirements, which either specify that a given atom should be applied, or that it should be ensured that it fails.
• the interpretation of this for the mockchain runs the tweaks that should fail and ensures that they yield the empty list of traces.

While I was at it, I took the opportunity to improve the whole framework around Ltl and Staged. Here is a non-exhaustive list of the changes:

• Staged now has its own module (and should later on be replaced with proper effects)
• There is no longer any monoid requirement for modifications. The caller decides what to do with the list of requirements they receive from the formula at a given time step.
• The caller no long has access to the StateT [Ltl mod] and thus no longer has to manually call nowLaterList, or manually update the state. Instead, they only need to provide whether their builtins will be subject to modification, and if so, how they should be.
• Some functions have been moved around in appropriate locations (such as the functions to run tweaks)
• There is no longer a StartLtl and StopLtl constructor for LtlOp which led to clunky use cases where somebody could call the latter without first calling the former, leading to the need of invoking error. Instead, a WrapLtl constructor is given, which does both, around a given computation, ensuring symmetry.
• Some definitions have been tweaked, abstracted or clarified (MonadLtl, InterpBuiltin, ...)

Overall, this should make this whole mechanism clearer, more user friendly, and more structured, while increasing the expressiveness, and paving the way to use a proper existing effect library in the future for those capabilities.