Cleanup DY.Lib.State.{Labeled,Typed}

[TWal]

A few things could be reworked.

As pointed by @cwaldm (https://github.com/REPROSEC/dolev-yao-star-extrinsic/issues/12#issuecomment-2092901645), the DY.Lib.State.Labeled predicates have type session_pred whereas the state predicates in DY.Core are state_predicate.

• The session vs state should be handled when fixing #6.
• The names do not convey the idea that state_predicate is a global state predicate for all states used in a protocol, whereas session_pred is a local state predicate for one state type

Other things could be cleaned.

• Do we need both Labeled and Typed state? The Labeled module apply the split predicate methodology, and the Typed module builds on top of Labeled to use Comparse. What is the value of doing it in two steps, we could do it in one step similarly to DY.Lib.Event?
• We could use a typeclass as in DY.Lib.Event to further simplify the user code.

[cwaldm]

I would prefer, if the Event and State API are similar, that is, I think we should either split the Event API as well or collapse Labeled and Typed state. Maybe there is a way to unify both even more? For example, https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/6fe7c9d40a097a5bdb2622fe95a0ebf8e9df3f75/src/lib/event/DY.Lib.Event.Typed.fst#L96-L108 is the same as https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/6fe7c9d40a097a5bdb2622fe95a0ebf8e9df3f75/src/lib/state/DY.Lib.State.Tagged.fst#L79-L91 and https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/6fe7c9d40a097a5bdb2622fe95a0ebf8e9df3f75/src/lib/event/DY.Lib.Event.Typed.fst#L83-L86 is the same as https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/6fe7c9d40a097a5bdb2622fe95a0ebf8e9df3f75/src/lib/state/DY.Lib.State.Tagged.fst#L73-L75 although it has a different name. Similarly, https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/6fe7c9d40a097a5bdb2622fe95a0ebf8e9df3f75/src/lib/event/DY.Lib.Event.Typed.fst#L74-L81 looks like https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/6fe7c9d40a097a5bdb2622fe95a0ebf8e9df3f75/src/lib/state/DY.Lib.State.Typed.fst#L32-L35

[TWal]

Ah, your comment and my pull-request crossed each other!

I found that we could not merge DY.Lib.State.Tagged and DY.Lib.State.Typed as easily as it is done in DY.Lib.Event.Typed (we can merge the crypto functions, but not much more, see the PR for more info). But we can do it anyway for consistency between state and event APIs.

I agree that there is a lot of similar code between DY.Lib.State.Tagged and DY.Lib.Event but I don't think we can factor them much more, I already tried to put as much things in DY.Lib.SplitPredicate.