EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
316 stars 48 forks source link

Error requiring theory that clones FinType #298

Open mbbarbosa opened 1 year ago

mbbarbosa commented 1 year ago

Can be seen in examples/quantum/FDH_quantum.ec in branch deploy-quantum-upgrade.

In external theory T_QROM [: line 1 (0) to line 213 (18)]:

cannot process [activate] outside a proof script

strub commented 1 year ago

I pushed a temporary hack in deploy-quantum-upgrade. A proper fix would require much more work :/