search

DavePearce / DevmProofGen

Dafny Evm Proof Generator (experimental)
1 stars 1 forks source link

Use set notation for `st.Operands()` #66

Closed DavePearce closed 1 year ago

DavePearce commented 1 year ago

Currently, we have things like this:

    requires st'.Operands() >= 8 && st'.Operands() <= 10
    requires st'.Operands() == 8 ==> ...
    requires st'.Operands() != 9
    requires st'.Operands() == 10 ==> ...

Which we could presumably rewrite as something like this:

        requires st'.Operands() in {8,9,10}
    requires st'.Operands() == 8 ==> ...
    requires st'.Operands() == 10 ==> ...

In case that we really have a contiguous region, then we could just use >= and <=.