[Meta] ProVerif backend tracking issue

[jschneider-bensch]

This issue collects sub-tasks for the ProVerif backend.

• [ ] Basic translation phases
  • [x] Extract structs to generic concstructors
  • [x] Extract ProVerif process macros from Rust fns
  • [ ] Extract ProVerif processes from annotated Rust fns
  • [ ] Automatic generation of generic top-level process
• [ ] hax-pv-lib Rust component (this let's us define top-level processes)
  • [ ] Protocol runtime
• [ ] hax-pv-lib ProVerif component (this let's us translate known API calls)
  • [ ] function definitions for libcrux APIs
  • [ ] state management facilities
• [ ] When basic translation works: restrict Rust inputs to valid subset

[jschneider-bensch]

Tracking the more specific issues for the current milestone (Extracting the Bertie TLS handshake) in #541.

[github-actions[bot]]

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.