EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
321 stars 49 forks source link

Add parser support for memory restriction annotations (and checking) on module definition #419

Open fdupress opened 1 year ago

fdupress commented 1 year ago

We'd like to be able to write the following, given some module type T and external module M.

module M' : T {-M} = {
  ...
}.

(similarly with general restriction expressions)