Hide that timestamps are Nats

[cwaldm]

Some of us previously discussed, that it would be good to hide that timestamps are Nats. For example, by defining a new

type timestamp = Nat

This prevents that timestamps can accidentally be used as session ids for example. It would also match better the comments for functions, for example: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/2a412f2766d4ebadbef5fe9a198e73bd8ac376a3/src/core/DY.Core.Trace.Type.fst#L157-L159

Additionally, we wanted to define an on_trace predicate for timestamps capturing i < length tr. Then the types of functions are easier to understand. For example, the above would read:

val get_event_at: tr:trace -> ts:timestamp{ts `on_trace` tr} -> trace_event

For this, we need to see whether we need predicates for both i < lenght tr and i <= length tr ?

We will of course also need relations between the abstract timestamps, like before for t1 < t2 ...

[TWal]

I agree that it would be good to have more type-safe API!

Hiding that timestamps are nats may be feasible, however we need to keep in mind that sometimes doing arithmetic on timestamps is a core component of the security proofs, e.g. in NSL https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/125737fdde3d67f0d3630d1c6c1f3a9674e6057f/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst#L59 saying "the random number was generated directly before the event was triggered" allows to prove this crucial injectivity lemma https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/125737fdde3d67f0d3630d1c6c1f3a9674e6057f/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst#L259-L273

While we could find a way to update this proof pattern, I would rather keep timestamps to nats but hide that state identifiers are nats: on these ones we do not care at all that they are integers, we never compare them or do arithmetic on them.

What would you think about that?

[cwaldm]

Ideally, I would like to hide both. But we can start with the session identifiers for now. To properly hide the type definition, we need to use interface files. Is there a reason, that there are none so far?

[TWal]

Indeed we would need interface files to properly hide it, or at least defining an actual new type (e.g. a record with only one field).

There is no really good reasons for having no interface files, other than personal likings. In general I feel like working with interface files is a bit cumbersome, doing back-and-forth between the .fst and the .fsti can be annoying (e.g. when you are iterating on the .fsti and have to reload the .fst each time), I also find it annoying that you cannot have a val and the corresponding let in the .fsti, and when you need to break the abstraction barrier for good reasons, you can do so using friend but it can only be done in a file that have an interface so files with interface are "contagious".

That being said, I think it would work well to have interfaces in DY*, files are relatively well self-contained (except e.g. mk_rand that is inbetween DY.Core.Trace and DY.Core.Bytes), we don't need to be able to do fast prototyping anymore, and it would be less verbose than all those opaque_to_smt and reveal_opaque things.

[cwaldm]

I agree with you on all the negative things about interface files. For me, it's fine to "just" use record new types for now.

[TWal]

Closed by #32.