ProVerif protocol traits

[jschneider-bensch]

This PR introduces two helper libraries:

• hax-lib-protocol which defines traits for building protocol implementations in hax.
• hax-lib-protocol-macros which defines macros that automatically implement the traits from hax-lib-protocol

The two libraries are exemplified in a new test for the ProVerif backend.

The PR also introduced new macros in hax-lib-macros to mark process components, although these are not yet acted on in the ProVerif backend.

[franziskuskiefer]

Generally looks good. I added a couple comments and questions.

Please add comments everywhere to make it easier to understand what's going on.

I have a couple of design questions that we may want to leave for a second iteration after this got merged.

[franziskuskiefer]

Thanks, let's get it in to get it used.