[ProVerif] Define abstraction for deserialization

[jschneider-bensch]

We want to treat deserialization abstractly in ProVerif, ideally just as a constructor fun deserialize_X(bitstring) : X. that we assume will work for deserializing a type X (or deserializing into a variant of X, more generally).

Then we can annotate our Rust source such that the backend can recognize deserialization code and translate it abstractly as above. Proving correctness of deserialization should be done using another backend.

[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?