[ProVerif] Define restrictions on input language

[jschneider-bensch]

At the moment, we basically allow any AST feature that's necessary to extract an example which conforms roughly to our idea of a good input and see how to deal with translating it in the backend.
When translation of "known good" examples works reliably, I want to think about which restrictions on the input are really necessary for good translation to ProVerif and which could be addressed by suitable translation phases.

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

[W95Psp]

@jschneider-bensch was this issue supposed to be closed?