ProVerif goal: Noise protocol example extraction

[jschneider-bensch]

In a branch of hacspec/specs there's a hacspec version of the KKpsk0 noise protocol pattern that @karthikbhargavan was working on. It's already pretty much in the code style we would expect the ProVerif backend to be able to handle, which makes it an ideal intermediate goal before moving from toy example to more complicated code bases.

• Sanity: extraction works
• Translate early returns and ? to failures
• Separate Protocol flow from party internals
• generate top-level process; easier in this case since there always two parties (ProVerif: Generic top-level process #426)

We split the remaining work into the following subtasks:

• Define minimal set of necessary pre-defintions #446
• [PV/Noise] Provide PV definitions for crypto dependencies #447
• [PV/Noise] Provide PV definitions for core library functions / types #448
• [ProVerif] Insert definitions of crypto dependencies + core library #449
• [ProVerif] Coherent translation of intra-crate function calls #450

[franziskuskiefer]

Closed in favour of the sub-issues in #414 (comment)