EthereumのActを使う

この文書は株式会社 proof ninja の助成を受けたものです．

EthereumのEVMプログラムの仕様記述言語であるActを使ってみる．記述した仕様はSMTソルバに自動証明させたり，Coqコードに変換してCoqの中で自分で証明したりできるらしい．
Actの仕様とEVMでの実装の同値性はHevmというエンジンで自動証明するらしい．

インストール

ソースコードはここ．
https://github.com/ethereum/act

ビルドにはNixというパッケージマネージャを使うので，まずNixをインストール．

ActのReadmeには nix build でビルドすると書いてあるが，自分の環境では

$ nix build --extra-experimental-features nix-command --extra-experimental-features flakes

とする必要があった．

act/result/bin/ にバイナリが生成される．パスを通すなどしよう．

また，Coqコードを生成して使いたい場合にはActLibをインストールする必要がありそうなので，act/lib/ActLib.v もビルドする．act/lib/の下で

$ coqc -R . ActLib ActLib.v

としてビルドした．自分はOpamでインストールしたCoqを使っているので，~/.opam/バージョン/lib/coq/user-contrib/ の下に ActLib というディレクトリを作り，

cp ActLib.* ~/.opam/バージョン/lib/coq/user-contrib/ActLib

とした．

使ってみる

ActBookに書いてあることをやってみた．ここではCoqの部分のみを見ていく．

以下はActBookのサンプルActコードに自分で理解したなりのコメントを加えたもの．
非負整数 b, e に対して b の e 乗を計算する状態機械を定義しようとしている．

// Exponent というコントラクトを宣言する．
constructor of Exponent
// 二つの符号なし整数 _b, _e を引数に取ることにする．
interface constructor(uint _b, uint _e)

iff // コントラクトが生成されるための条件．ここでは _e が正という条件を課す．

    _e > 0

// Exponentの状態変数を定義する．
// ここでは b, e, r の3個で，初期値として _b, _e, _b を与える．
creates

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

// Exponentの状態遷移を定義する．
behaviour exp of Exponent
interface exp()

// 状態遷移が起こるための条件を書く．
// ここでは e > 1 であることと， r*b, e-1 が uintの範囲に収まっていることとする．
iff

    e > 1

iff in range uint

    r * b
    e - 1

// 状態遷移を定義する．ここでは，上の条件のもとで，(r, e, b) => (r*b, e-1, b) と定める．
storage

    r => r * b
    e => e - 1
    b

上のコードを Exponent.act として保存し，

act coq --file Exponent.act > Exponent.v

で以下のようなCoqコード Exponent.v が生成される．

(* --- GENERATED BY ACT --- *)

Require Import Coq.ZArith.ZArith.
Require Import ActLib.ActLib.
Require Coq.Strings.String.

Module Str := Coq.Strings.String.
Open Scope Z_scope.

Record State : Set := state
{ b : Z
; e : Z
; r : Z
}.

Definition exp0 (STATE : State)  :=
state (b STATE) (((e STATE) - 1)) (((r STATE) * (b STATE))).

Definition Exponent0 (_b : Z) (_e : Z) :=
state (_b) (_e) (_b).

Inductive reachable  : State -> State -> Prop :=
| Exponent0_base : forall (_b : Z) (_e : Z),
     (_e > 0)
  -> ((0 <= _b) /\ (_b <= (UINT_MAX 256)))
  -> ((0 <= _e) /\ (_e <= (UINT_MAX 256)))
  -> reachable (Exponent0 _b _e) (Exponent0 _b _e)

| exp0_step : forall (BASE STATE : State),
     reachable BASE STATE
  -> ((e STATE) > 1)
  -> ((0 <= ((r STATE) * (b STATE))) /\ (((r STATE) * (b STATE)) <= (UINT_MAX 256)))
  -> ((0 <= ((e STATE) - 1)) /\ (((e STATE) - 1) <= (UINT_MAX 256)))
  -> ((0 <= (r STATE)) /\ ((r STATE) <= (UINT_MAX 256)))
  -> ((0 <= (e STATE)) /\ ((e STATE) <= (UINT_MAX 256)))
  -> ((0 <= (b STATE)) /\ ((b STATE) <= (UINT_MAX 256)))
  -> reachable BASE (exp0 STATE )
.

状態 s から 状態 s' への状態遷移が可能であることを表す reachable s s' が帰納的述語として定義された．
ActBookでは，この状態機械が実際に累乗を計算していること

Theorem exp_correct : forall base s,
  reachable base s -> e s = 1 -> r s = (b base) ^ (e base).

を証明している．これは普通のCoqの証明なのでここでは触れない．

他にはCoqで証明している例が見つからなかったので，何か試したいところ．