ActBook: Hevm section seems outdated

[mir-ikbch]

I tried the example in Hevm section of ActBook.

The command in the book

act hevm --spec src/simple.act --soljson out/dapp.sol.json

did not work because --soljson option seems outdated and also it should have --contract option.
Then I tried

act hevm --spec xxx.act --sol xxx.sol --contract Simple

but I got the following:

Checking if constructor results are equivalent.
Found 1 total pairs of endstates
Asking the SMT solver for 1 pairs
Reuse of previous queries was Useful in 0 cases
Not equivalent.

-----

The following input results in different behaviours
Calldata:
  Any

Transaction Context:
  CallValue: 0x0

I thought this was because the second line of EVM should have been uint val = 0;, so I replaced it, but then I got

Checking if constructor results are equivalent.
Found 1 total pairs of endstates
Asking the SMT solver for 0 pairs
Reuse of previous queries was Useful in 0 cases
No discrepancies found
Checking if constructor input spaces are the same.
Not equivalent.

-----

The following inputs are accepted by Act but not EVM
Calldata:
  Any

Transaction Context:
  CallValue: 0x2

Now I have no idea why this is happening.

[zoep]

Thanks for opening the issue! Indeed, the recently rewrote the hevm equivalence checker and the documentation is out of date.

The reason why the example is failing is because, for the moment, the constructor code is executed with an abstract store, so there is no information the the value of val is 0.

This might change in the future, but for now if you want the example to succeed you add an explicit constructor:

    constructor () payable {
	val = 0;
    }

[zoep]

#159 should fixes this issue as it uses an empty initial store for constructors.

Note that the tests will still fail unless you add a precondition that callvalue is zero in the constructor:

interface constructor()

iff
  CALLVALUE == 0
  
creates
  uint val := 0