RFC: act: storage case

[d-xo]

I often find myself writing storage conditions like this:

storage

    foo |-> Foo => #if Bar and Baz #then NewFoo #else Foo #fi

This can get pretty messy, especially if the condition must be repeated multiple times. I therefore propose a little bit of sugar:

storage case Bar and Baz

    foo |-> Foo => NewFoo

Would produce the following K statement in the storage cell:

[#Contract.foo <- (Foo => #if (Bar andBool Baz) #then NewFoo #else Foo #fi)]

I think this could be implemented fairly easily and would help readability in complex specs.

Note that this limited syntax does not support cases where the #else block is not a no-op, or writing to the storage location in multiple storage case blocks. I would be very happy to come up with syntax that can cleanly handle the above situations.

[MrChico]

I would be very happy to come up with syntax that can cleanly handle the above situations.

I present to you ethereum/act#5:

A more systematic way is to not just add the casing to storage blocks, but as an optional parent block to the two post condition cells (return and storage). This effectively allows the case syntax to play the rôle of if headers, but in a way which reduces duplication. Compare for example a spec for transfer in act 1 (introduction):

behaviour transfer-diff of Token
interface transfer(address To, uint Value)

for all

    FromBal : uint256
    ToBal   : uint256

storage

    #Token.balances[CALLER_ID] |-> FromBal => FromBal - Value
    #Token.balances[To]        |-> ToBal => ToBal + Value

returns 1

iff in range uint256

    FromBal - Value
    ToBal + Value

iff

    VCallValue == 0

if
    CALLER_ID =/= To

behaviour transfer-same of Token
interface transfer(address To, uint Value)

for all

    FromBal : uint256
    ToBal   : uint256

storage

    #Token.balances[CALLER_ID] |-> FromBal => FromBal

returns 1

iff in range uint256

    FromBal - Value

iff

    VCallValue == 0

if
    CALLER_ID == To

with act 2 (confrontation):

behaviour transfer of Token
interface transfer(uint256 value, address to)

iff

   CALLVALUE == 0
   value <= balanceOf[CALLER]
   CALLER =/= to => balanceOf[to] + value < 2^256

case CALLER =/= to:

   storage

     balanceOf[CALLER] => balanceOf[CALLER] - value
     balanceOf[to]     => balanceOf[to] + value

   returns 1

case CALLER == to:

   returns 1

[d-xo]

nice!

Some questions:

• Would each case block compile to a different spec?
• Would there be any requirement for exhaustiveness or exclusivity between case blocks?
• If no to the above, what happens if multiple cases overlap (e.g. case CALLER < 10 and case CALLER == 0)

[asymmetric]

IIUC these would just be compiled to requires with the semantics of if, so there would be no intrinsic check on exhaustiveness (same as there isn't one now) nor overlap, and they would compile to two different specs (because you can't have contradicting clauses in the side-conditions)