search

EasyCrypt / easycrypt

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

Remove the "nosmt" mechanism #575

Closed strub closed 4 months ago

alleystoughton commented 4 months ago

Is there a new mechanism that replaces nosmt for operators? I was the one that implemented nosmt for operators. It's crucial for some of my work.

I thought maybe you changed the semantics of [opaque] to subsume this, but I just checked and you didn't. Using abstract operators and adding axioms to give their meanings is a bad replacement for nosmt for operators.

I find it completely natural to give concrete definitions of operators but to want to hide those definitions from the solvers.

strub commented 4 months ago

The nosmt keyword is going to disappear. This is pure technical debt, it has a lot of ad-hoc variations that have been introduced for specific projets & it has not been used consistently for the last 10 years.

IMO, this is orthogonal to having opaque operators to SMT (but even here, the implementation was intricated).

alleystoughton commented 4 months ago

With lemmas and axioms, one can select whether to use them in smt(...). But with concrete operators, this is not possible. Making [opaque] also apply to smt would be one solution. For my needs that would be perfect.

strub commented 4 months ago

Discussion is now in #576