operators taking in modules and memories

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs

MIT License

320 stars 49 forks source link

operators taking in modules and memories #609

Open alleystoughton opened 2 months ago

alleystoughton commented 2 months ago

We had some discussion of this on Zulip a year ago, but I don't see an issue, so creating one. It would be super-useful to be able to define operators taking in modules and memories, as in:

op adv (Adv : ADV) &m : real =
  `|Pr[GRF(PRF, Adv2RFA(Adv)).main() @ &m : res] -
    Pr[GRF(TRF, Adv2RFA(Adv)).main() @ &m : res]|.