Rework the trace API

[TWal]

As noted by the comments in #55, there is some friction associated with the trace API.

Here is a list.

The length function on traces is shadowed by the length function on bytes, so that we need to namespace it, either by doing DY.Core.Trace.Type.length or by doing module T = DY.Core.Trace.Type … T.length. We could rename it to trace_length to simplify things. https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/9c8d4d8d300755ea6d338c8afd147ff27ba1fa24/src/lib/utils/DY.Lib.Printing.fst#L250

The DY user never has to use Snoc because the trace API takes care of that. However the DY user has to use Nil because there is no empty_trace function. https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/9c8d4d8d300755ea6d338c8afd147ff27ba1fa24/examples/iso_dh/DY.Example.DH.Debug.fst#L66

In NSL but also in the lemmas about mk_rand, we use a property on traces that the last event is some RandGen event. We could factorize this in a trace predicate. https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/9c8d4d8d300755ea6d338c8afd147ff27ba1fa24/src/core/DY.Core.Trace.Manipulation.fst#L257-L258

[TWal]

Proposed actions:

Rename DY.Core.Trace.Type.length to trace_length.

Add val empty_trace: trace

Add val rand_just_generated: trace -> bytes -> prop

[qaphla]

I support this overall, and would also propose a few related actions to consider:

• Add a general version of rand_just_generated, something like trace_entry_just_occurred, of which rand_just_generated is a specific case. I think we currently only use this with rand, but I see no inherent reason that other forms wouldn't be useable in the same way, and I would prefer to either use an approach that does not involve this at all, or to give general access to it, rather than artificially restricting it to the case of rand.
• Add list_to_trace : list trace_entry -> trace. We may not need this very much, but I can see it being useful for some kinds of debug traces, particularly if we want to give a witness for some attack.