try extraction from hax into ProVerif

[cfm]

Stub ticket for sprint-planning; details TK.

• In parallel with incrementally verify securedrop-protocol-minimal #173

With #174 off the table, the next approach to try is using hax to extract a ProVerif model. In https://docs.google.com/document/d/1XKqCA54nXftppjGS42JtMjzKWw5AujAFxS0wdlwmCLA/edit?usp=drivesdk I suggested:

Attempt to extract ProVerif to verify protocol conformance. See Bhargavan et al. (2025) p. 5. A particular highlight would be using F* to prove at the implementation level that a message-handling function can be treated as an injective constructor in ProVerif at the protocol level (p. 12).

We should also explore Tamarin's export to ProVerif.