feat: add support for intrinsic proofs in states

[TWal]

While porting some proofs from DY-intrinsic to DY-extrinsic, I noticed that sometimes, intrinsic proofs are useful!

Indeed, in DY*, the state invariant roughly contain two kind of properties:

• security properties (e.g. properties on labels, usage, etc)
• functional properties (e.g. "this binary tree is a binary search tree")

In DY-intrinsic, when you do get_state, you obtain (as a post-condition) that its output satisfy the security properties, and the functional properties. The functional properties might then be used to call pure functions that require this property as a precondition (e.g. adding a node in a binary search tree requires the BST invariant on the input and ensure the BST invariant on the output). In DY-extrinsic, doing such things is impossible: when you do get_state, you cannot have the functional post-condition, because for that you would need the precondition that the trace satisfy the trace invariants, which we don't know because we do extrinsic proofs.

This pull-request is an attempt to allow such kind of intrinsic proofs in DY*-extrinsic. The crypto monad will now preserve the trace_functional_invariant, which is parametrized by state_functional_predicate. The state_functional_predicate is a predicate on states that deals with state contents in a trace, namely it is a bytes -> prop. In particular, this predicate do not have the trace as input, because its purpose is not to express trace properties.

What do you think about such an addition to DY*? I was too lazy to do it starting from DY.Lib.State.Map (hence PKI and PrivateKeys), but if people agree it's a good idea I will propagate the changes properly.

As a showcase, get_tagged_state can now assert that the state content can be parsed into a tagged_state, or DY.Lib.State.Typed.get_state can now assert that the state content can be parsed into an a. Roughly, it means that we can now remove some amount of dynamic checks by proving these checks are invariants of the protocol. This may not be necessary when these checks are computable (i.e. in bool), but it might be useful when they are not computable (i.e. in prop).

[TWal]

To add more explanations: this is only about proving functional properties intrinsically, to be able to use pure APIs that come with pre-conditions (e.g. binary search trees). Security properties would still be proved extrinsically.

This is useful because state content must be embedded into bytes, because we need to express what the attacker learns when a state is compromised. bytes is an abstraction that is bigger than what we encode in it, e.g. some bytes instances do not represent valid (i.e. parseable) states, or represent valid states but that do not respecting some invariants (which we might encode using a refinement).