search

easyuc / EasyUC

Experiments with Universal Composability in EasyCrypt
30 stars 1 forks source link

Use uc_dsl_interpreter_hints in simplify_function #18

Closed 01tomislav closed 11 months ago

01tomislav commented 11 months ago

Low priority, but if we can make our simplification procedure run

rewrite uc_dsl_interpreter_hints

we can avoid a lot of SMT calls involving envport goals.