Jonas Schneider-Bensch

[Meta] ProVerif backend tracking issue

2

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 `fn`s...

As one part of addressing #563, this PR replaces the stub definitions for designated-as-handwritten translations by commented-out inclusion markers of the form `(* {{ proofs/proverif/handwritten/.pvl }} *)` that indicate where...

While the ProVerif backend at the moment allows marking items for manual modelling, it does not offer a convenient way to integrate a set of handwritten models after extraction. To...

Say we have the following crate: ```rust mod a { fn need_b() { crate::b::need_c() } } mod b { pub(super) fn need_c() { crate::c::c() } } mod c { pub(super)...

- [ ] `Alloc__slice__Impl__to_vec` - [ ] `Core__ops__deref__Deref__deref` - [ ] `Core__ops__index__Index__index` - [ ] `Rust_primitives__unsize` - [ ] `Core__num__Impl_9__to_le_bytes` - [ ] `Alloc__slice__Impl__into_vec` - [ ] `Alloc__vec__Impl_1__truncate` - [...

[PV/Noise] Provide PV definitions for crypto dependencies

1

- [ ] `Hax_lib_protocol__crypto__hash` - [ ] `Hax_lib_protocol__crypto__hmac` - [ ] `Hax_lib_protocol__crypto__aead_decrypt` - [ ] `Hax_lib_protocol__crypto__aead_encrypt` - [ ] `Hax_lib_protocol__crypto__dh_scalar_multiply` - [ ] `Hax_lib_protocol__crypto__dh_scalar_multiply_base` - [ ] `Hax_lib_protocol__crypto__Impl__from_bytes` (`hax_lib_protocol::cal::impl__DHScalar__from_bytes`) -...

we might want to move this renaming to the name policy thing at some point. Otherwise, name collisions are possible But for now that's completely fine, let's see that later...

Given that we want an abstraction, we should have traits to make it easier to implement this again for other backends. But that's not urgent. Let's open an issue for...