Simplify code using latest F* features

REPROSEC / dolev-yao-star-extrinsic

DY* with extrinsic proofs

https://reprosec.org/

Mozilla Public License 2.0

10 stars 0 forks source link

Open TWal opened 2 months ago

TWal commented 2 months ago

We could clean things using some new F* features:

simplify includes using FStarLang/FStar#3345
remove workarounds for FStarLang/FStar#3286 that has been fixed
in the attacker knowledge file, we can use move_requires_4 introduced in FStarLang/FStar#3449

(this issue is more a note for myself rather than to ask someone to do it!)

TWal commented 2 months ago