search

cryspen / bertie

Bertie TLS 1.3 Implementation
Apache License 2.0
112 stars 3 forks source link

[Feature request] Gate extractions to F* and ProVerif behind a single feature `hax` #109

Open jschneider-bensch opened 7 months ago

jschneider-bensch commented 7 months ago

102 and #107 both introduce features to gate extraction to ProVerif and F*, respectively. Both features are justified by an optional dependency on hax-lib-macros and nothing else. This suggests unifying the features into a single hax feature that guards any hax extraction specific code and dependencies.

This should also clean up redundancies in the hax driver.

franziskuskiefer commented 7 months ago

hax itself sets the hax config that could be re-used for anything hax related.