この文書は株式会社 proof ninja の助成を受けたものです．
Actについての前回の記事はこちら．
今回はAct言語で書かれた仕様とSolidityによる実装の同値性を示す，Act Hevmを使ってみる．
Act BookのHevmの章を参考にしたのだが，記述が古い箇所があるらしく，そのままでは動かなかった．
これからこのQiitaに書く内容もすぐ古くなるかもしれない．
この記事ではActのgithub上の現在の最新版のもとでの結果を書いている．
簡単な例
まず，サンプル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を投げたら必要だと言われた．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) に弾かれる，ということを言っていると思う．
累乗の例
前回の記事で書いた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の振舞いなど)はちゃんと示されたらしいが．