RFC: act: all of

[d-xo]

I often find myself having to expand large calculations in the iff in range blocks.

For example a spec of sub(mul(add(a, b), c), d) would need the following:

iff in range uint256

    A + B
    (A + B) * C
    ((A + B) * C)  - D

I therefore propose the following sugar:

iff in range uint256

    all of : ((A + B) * C) - D

Which would be exactly equivalent to the first example above. This would remove a common source of duplication in my specs.

I'm not 100% sure how to implement this. I think we would have to do some non trivial parsing of the RHS of the expression to determine which arithmetic operations we would need to add. I think we would also have to move the expansion of the macros in the where block earlier in the build process, or the all of machinery will not expand things correctly.

[livnev]

Hm, I see where you are coming from (certainly I found listing all of these to be very tiresome in the past), but this could be a source of problematic indirection.

[d-xo]

this could be a source of problematic indirection.

Agree. Especially when combined with the macros in the new where block.

I do however find that complex specs are currently excessively verbose in a way that makes them harder to think about (often I cannot fit all of a large spec on a large monitor, even when flipped vertically 😮), so perhaps there are some trade offs to be made.