EthereumのActを使う(Hevm編)

この文書は株式会社 [proof ninja](https://proof-ninja.co.jp/) の助成を受けたものです．

Actについての前回の記事は[こちら](https://qiita.com/mrkbc/items/23d1e254277de4dfcf57)．

今回はAct言語で書かれた仕様とSolidityによる実装の同値性を示す，Act Hevmを使ってみる．

[Act BookのHevmの章](https://ethereum.github.io/act/hevm.html)を参考にしたのだが，記述が古い箇所があるらしく，そのままでは動かなかった．
これからこのQiitaに書く内容もすぐ古くなるかもしれない．
この記事ではActのgithub上の現在の[最新版](https://github.com/ethereum/act/commit/a15d717336e086a563773204d3504231dcacf736)のもとでの結果を書いている．

# 簡単な例

まず，サンプルSolidityプログラムとして
```
contract Simple {
    uint val;

    function set(uint x) external payable returns (uint) {
        require(x > 100);
        val = x;
        return x;
    }
}
```
を考える．これに対応するActファイルは以下．

```
constructor of Simple
interface constructor()

iff
  CALLVALUE == 0

creates
  uint val := 0

behaviour set of Simple
interface set(uint x)

iff
  x > 100

storage
  val => x

returns x

```
このコード内の
```
iff
  CALLVALUE == 0
```
の部分は現在のActBookには書いていないのだが，githubのissueを投げたら必要だと[言われた](https://github.com/ethereum/act/issues/158)．Solidityには明示的に書いていない事前条件に当たるようだ．

また，
```
creates
  uint val := 0
```
の部分はSolidityプログラム内でSimpleコントラクトに変数 `val` が作られていることに対応する．

`behaviour set of Simple` 以下がSolidityプログラム内のset関数の実装に対応する．

Solidityプログラムの `require(x > 100);` がActの
```
iff
  x > 100
```
に対応し，Solidityの `val = x;` がActの
```
storage
  val => x
```
に対応するようだ．

これらのSolidityとActが実際に同値であることをチェックするために `act hevm` コマンドを使う．
上記のActコードをsimple.act，Solidityコードをsimple.solというファイルに保存して
```
act hevm --spec simple.act --sol simple.sol --contract Simple
```
を実行すると，以下の結果が得られた．
```
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
No discrepancies found
Checking if constructor input spaces are the same.
No discrepancies found
Checking behavior set of Act
Checking if behaviour is matched by EVM
Found 1 total pairs of endstates
Asking the SMT solver for 1 pairs
Reuse of previous queries was Useful in 0 cases
No discrepancies found
Checking if the input spaces are the same
No discrepancies found
Checking if the ABI of the contract matches the specification
No discrepancies found
```

細かいことはわからないが，No discrepancies(差異)と言っていることから同値性が言えているのだと思う．
実際，コードを書きかえて，たとえばActの `x > 100` を `x < 100` にしたりすると以下が得られた．
```
(略)
Checking if the input spaces are the same
Not equivalent.

-----

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

Storage:
  Addr 0xb4c79daB8f259C7Aee6E5b2Aa729821864227e84: [(0x0,0x0)]



-----

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

Storage:
  Addr 0xb4c79daB8f259C7Aee6E5b2Aa729821864227e84: [(0x0,0x0)]
```
同値でないというメッセージ(Not equivalent.)と，反例らしきものを提示してくれた．
読み方に自信はないがset関数の引数 x として0x0はActでは許される(iffの条件を x < 100 に変えたので)が，Solidity/EVMでは require(x > 100) に弾かれる，ということを言っていると思う．

# 累乗の例
[前回の記事](https://qiita.com/mrkbc/items/23d1e254277de4dfcf57)で書いたActコードをすこし変更したものと，それに対応するSolidityを自分で書いてHevmを試してみた．Actコードは以下．
```
constructor of Exponent
interface constructor(uint _b, uint _e)

iff
    CALLVALUE == 0
    _e > 0

creates

    uint b := _b
    uint e := _e
    uint r := _b

behaviour exp of Exponent
interface exp()

iff

    e > 1

iff in range uint

    r * b
    e - 1

storage

    r => r * b
    e => e - 1
    b
```
これに対応するSolidityコードは以下．
```
contract Exponent {
  uint b;
  uint e;
  uint r;
  constructor(uint _b, uint _e) {
    require(_e > 0);
    b = _b;
    e = _e;
    r = _b;
  }

  function exp() public {
    require(e > 1);
    r = r * b;
    e = e - 1;
  }

}
```
これで先ほどと同様act hevmを走らせてみたが，以下の結果になった．
```
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
No discrepancies found
Checking if constructor input spaces are the same.
No discrepancies found
Checking behavior exp of Act
Checking if behaviour is matched by EVM
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 the input spaces are the same
No discrepancies found
But timeout(s) occurred
```
exp関数のinput spaceをチェックするのにタイムアウトが起きたらしい．expには引数がないのでなんでこうなったんだろう．expの引数に適当にダミー変数を加えてみたりしてみたけど結果は同じだった．
少なくとも他の同値性(expの振舞いなど)はちゃんと示されたらしいが．