ERC20 transfer test

[virgil-serbanuta]

No description provided.

[sskeirik]

Looks good! Thanks!

I wanted to leave a comment on a possible future twist on this approach (no need to try and implement this now): if we can't get strictness added to alternate cells, there is an alternate approach that might make the code a bit cleaner.

Essentially, the idea is to have operators like:

syntax KItem ::= seqExp(List)
               | seqVal(List)

which is used to do all seq-strict style heating and cooling. Then the other operators desugar into it. For one argument operators, we have:

rule <k> (.K => seqExp(ListItem(Expr))) ~> #setOutput(Expr)
rule <k> seqVal(Expr) ~> #setOutput(_) => ... </k>

For many argument operators, we have:

rule (.K => seqExp(ListItem(E1) ListItem(E2) ListItem(E3) ListItem(E4)) ~> #log(E1, E2, E3, E4) </k>
rule seqVal(V1, V2, V3, V4) ~> #log(...) => ... </k>

Then, you only need to implement this strategy once.