REPROSEC / dolev-yao-star-extrinsic

DY* with extrinsic proofs
https://reprosec.org/
Mozilla Public License 2.0
8 stars 0 forks source link

feat: add typeclasses for easier use of State.Typed #19

Closed TWal closed 1 month ago

TWal commented 1 month ago

Fixes #15.

In DY.Lib.State.Typed and DY.Lib.State.Map, I added a typeclass mechanism similar to DY.Lib.Event.Typed to reduce boilerplate in the user code (see the modifications in DY.Example.NSL).

I also tried to fusion DY.Lib.State.Tagged and DY.Lib.State.Typed as it is done in DY.Lib.Event.Typed, but did not do it at the end.

In DY.Lib.Event.Typed it works well to do the fusion and it allows to avoid redundant code, but in State.Typed it doesn't work well because the predicate must satisfy some nice properties (i.e. it must stay true as the trace grows, and must imply that the state content is knowable by the principal). It means that we need to compile the typed predicate (+ its nice properties, local_state_predicate) to the predicate on bytes (+ its nice properties, on bytes, local_bytes_state_predicate) before combining those predicates into the global state predicate (+ its nice properties, on bytes, on all states, state_predicate).

It means that the only thing we can fusion is the functions that operate on the trace, but it doesn't seem like a huge gain.

What do you think about it @fabian-hk? With that you should be able to remove some boilerplate in the ISO-DH example (as I did for the NSL example).