日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

スマートコントラクト検証器 Helmholtz のためのエラー原因提示手法
小野 雄登

西田 雄気

古瀬 淳

末永 幸平

五十嵐 淳

Helmholtz はブロックチェーンプロトコル Tezos のスマートコントラクト記述言語 Michelson のための静的な検証器である．Helmholtz はユーザーの定める仕様が記述された注釈が挿入された Michelson プログラムが与えられると，プログラムが仕様を満たすことを保証するための検証条件を生成し，それを SMT ソルバの Z3 によって検証する．現在の実装においては，検証が失敗したときにその原因がユーザーに伝わりにくいという問題点がある．本研究では，この問題を解決するためのエラー原因提示手法を提案する．Helmholtz は検証が失敗した時に，検証条件が成り立たないような変数束縛であるモデルを内部的に Z3 から得る．本研究では，このモデルのうち，検証失敗の原因に関連する要素のみを得るモデル極小化アルゴリズムを提案する．いくつかのプログラムに対してこのアルゴリズ
ムを適用し，出力されたモデルがエラーの原因として適切な説明を含むことを確認した．
Helmholtz is a static veriﬁer for Michelson, the programming language for writing smart contracts fora blockchain protocol Tezos. Given a Michelson program annotated with a user-deﬁned speciﬁcation,
Helmholtz generates veriﬁcation conditions to ensure that the program meets the speciﬁcation, which isthen veriﬁed by the Z3 SMT solver. However, it is diﬃcult for users to know the cause of the failure when
Helmholtz fails to verify a program. To solve this problem, we propose a method of presenting the cause of
the error. When a veriﬁcation fails, Z3 outputs a model, a set of variable bindings which does not satisfy
the veriﬁcation condition. We propose a model minimalization algorithm to obtain only those elements ofthe model that are relevant to the cause of the veriﬁcation failure. We applied this algorithm to several
programs and conﬁrmed that the output models contain appropriate explanations for the causes of errors.

行されるスマートコントラクトの記述言語 Michelson

1 はじめにのための，型システムを用いたの静的な検証器であスマートコントラクトは，ブロックチェーン上で実る．Michelson の型システムを改良した篩型システム

行されるプログラムのことで，これをベースに多くの上で設計されていて，ユーザーの定める仕様を記述し仮想通貨が実装され，取引における契約の締結や履行た注釈が挿入された Michelson プログラムを入力との自動化のために利用されている．スマートコント

して受け取ると，Michelson の型システムに基づいたラクトは扱う金額が大きく，また一度ブロックチェー

型検査を行うとともに，仕様に基づいた検証条件をンにデプロイされると修正することができないため，

型検査中に生成する．検証条件は SMT ソルバである

静的な検証が必須であり，その手法の需要が高まってZ3 へ入力され，仕様が満たされているかどうかが検いる．

証される．Helmholtz を用いて，口座への送金や電子

スマートコントラクトを静的かつ形式的に検証する手法の事例として Helmholtz がある．Helmholtz は
ブロックチェーンプラットフォームの Tezos 上で実署名のチェックなど，実用的な Michelson のプログラ
ムを検証できることが確認されている．
一方で，正しく型付けられていないプログラムや，
注釈に記述された仕様が誤っているプログラムを入Yuto Ono, Yuki Nishida, Kohei Suenaga, Atsushi
Igarashi, 京 都 大 学 大 学 院 情 報 学 研 究 科, Graduate
School of Informatics, Kyoto University.
Jun Furuse, ダイラムダ株式会社, DaiLambda, Inc.

力として受け取り，検証に失敗した際に，エラーメッ
セージとして返す情報が不十分であるという課題がある．Helmholtz が検証に失敗すると，図 1 に示す

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

2


1
2
3
4
5
6
7

 原因の説明としてエラーメッセージに用いることがで=========== solver results ===========
Finding counter - example for ab - postcondition ofContractAnnot at line 0 , characters -1 - -1
unsat
Finding counter - example for postcondition ofContractAnnot at line 0 , characters -1 - -1sat=========== final result ===========
UNVERIFIED



図1

きると考えられる．本研究では，検証条件から Z3 によって得られるモデルから，検証失敗の原因として関係のある情報のみを含んだモデルを求めるアルゴリ
ズムを考案した．また，いくつかの検証が失敗するプHelmholtz の検証失敗時の出力の例

ログラムに対して，考案したアルゴリズムを適用することで，検証失敗の原因として妥当なモデルが得られることを確かめた．
本論文は以下のように構成されている．2 章では，ような出力が返されるが，この出力にはそれぞれの仕本研究に関連する背景知識について述べる．3 章で様が成り立っているかどうか，という情報しか含まれは，本研究で提案する，Helmholtz の検証におけるエておらず，エラーメッセージとしては不十分である．

ラー原因提示手法について述べる．4 章では，考案しMichelson は静的に型付けされたスタックベースの言たアルゴリズムについて，いくつかプログラムに対す語でありながら，リスト，マップ，高階関数などの高る適用例を示す．5 章では，本研究の関連研究についレベルで複雑なデータ構造をサポートしている分，読て論ずる．6 章では，本研究の結論と今後の課題につみ書きが難しい側面があり，また Tezos のスマートいて述べる．

コントラクトの記述のための言語であるという専門性から，ユーザーが検証失敗の原因を推測すること

2 背景知識は難しいと考えられる．よって，検証が失敗した際の2. 1 Tezos と Michelson

エラーメッセージとして，その原因をユーザーにとっTezos はブロックチェーンを技術基盤とし，その取て理解可能な形で示す必要性がある．

引にスマートコントラクトを用いる仮想通貨の 1 つ

本研究では，この問題を解決するために，Helmholtz

である．Bitcoin や Ethereum といった仮想通貨が先の検証失敗時に出力するためのエラー原因の提示手法

立って流通されるようになった中，Tezos はそれらのを提案する．検証失敗の原因となる情報として，Z3ブロックチェーンの弱点を解消することを目的としてのモデル出力機能によって得られるモデルを活用す開発された [1]．

る手法を提案する．Z3 のモデル出力機能を用いると，Michelson は，Tezos のスマートコントラクトを記入力された検証条件が sat であった場合に，その検証述するために用いられるプログラミング言語である．

条件を満たすような変数束縛であるモデルを得ることができる．†1 Helmholtz の検証においては，仕様が

この言語はスタックベースで，高レベルのデータ型と満たされない場合に sat となるような検証条件を生成いる [5]．

プリミティブ，および厳密な静的型チェックを備えてするため，検証が失敗した際に仕様を満たさないよう

Michelson の文法のうち，本論文で扱う部分を図 2

なモデルを得ることができる．Z3 によって生成されに示す．T はスタックの要素の型を表す．T には整数のるモデルは，検証条件中で宣言されている全ての変数

型 int，自然数の型 nat，Boolean の型 bool，文字列に対する変数束縛からなるので，検証失敗の原因としの型 string，Unit の型 unit，ペアの型 pair T T ，て関係のない情報も含まれている．よって，そのようオプションの型 option，リストの型 list T ，マッ

な関係のない情報を取り除いたモデルを，検証失敗の

プの型 map T T ，アドレスの型 address，コントラ†1 数理論理学における用語法とは異なり，SMT ソルバの文脈においては「モデル」という言葉を，与えられた制約を充足可能にする変数に対する値の割り当て（すなわち付値）の意味で用いる．本論文においても「モデル」をこの意味で用いることに注意されたい．

クトを表す型 contract，送金などのブロックチェー
ン上の操作を表す型 operation がある．V はスタッ
クの要素の値を表す．V には整数の i，自然数の n，Boolean の True，False，文字列の s，Unit の Unit，

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

T

::=

V

::=

3

int | nat | bool | string | unit | pair T T |option T | list T | map T T | address | contract T | operationi | n | True | False | s | Unit | (V1 , V2 ) |Some V | None | [] | V :: V | {Elt V V ; ...} | Contract V | Transfer V i Vn::=[0 − 9] +i::=n | −ns::=”[a − z] + ”

IS

::=

{I1 ; ... ; In }

I

::=

...

S

::=

E | V ▷S
図2

Michelson の文法

ペアの (V1 , V2 )，オプションを表す Some V ，None，り，それが出力される．

空リストを表す []，Cons を表す V :: V ，マップを

図 3 に示したプログラムは，boomerang と呼ばれ表す { Elt V V ; ...}，コントラクトを表す Contract

る Michelson プログラムの例である．boomerang がV ，送金操作を表す Transfer V i V がある．n は自呼び出されると，取引が始まった実行の起点のアカウ

然数，i は整数，s は文字列である．IS はコードに記

ントへ受け取った通貨を送金し返す．なお，各命令後述される命令列で，命令 I のシーケンスである．命のスタックの状態を/*，*/で囲われたコメントで示

令 I は，数が非常に多いので，詳細は [5] を参照され

している．

たい．

以下，プログラムの内容を説明する．

S はスタックを表す．空のスタックを E で表し，スMichelson プログラムのコードは，プログラムに対タックに積まれた要素は ▷ で区切る．空のスタックをして与えられる引数である parameter と，ブロック

表す E は，要素の積まれたスタックを表すときは省チェーン上に保存されているストレージの値である

略する．例えば，V1 ▷ V2 は V1 ▷ V2 ▷ E を省略した形

storage の型宣言から始まる．1,2 行目は parameterである．

と storage の型が unit であることを宣言している．

Michelson のプログラムは，プログラムに対して与3 行目以降はプログラムの本体である code である．

えられるパラメータと，ブロックチェーン上に保存さcode には一連の命令が記述されていて，この命令れているストレージのペアを受け取り，このプログラ

が初期スタックに対して順に実行されていく．以下，

ムの終了後に実行される操作を表す operation list

code の内容について行番号ごとに説明する．

型の値と，プログラムの実行中に更新されブロック• プログラム開始時のスタックは，parameter とチェーン上に保存されるストレージのペアを返す純粋storage の値のペアである (param, st) が空のな関数である．プログラムのコードは，順番に実行さスタックに積まれた状態で始まる．

れる命令列 IS で記述される．各命令は，スタックを• 5 行目の CDR は，スタックのトップのペアを取入力として受け取り，そのスタックの内容を書き換えり出して，ペアの第 2 要素をスタックに積む．

て出力する．プログラムの初期スタックは，引数とし• 6 行目の NIL T はリストの型が T であるようなて与えられたパラメータとストレージのペアが一番

空リスト [] をスタックに積む．

上に積まれた状態のもので，その初期スタックに対し• 7 行目は SOURCE は現在実行中の取引の起点となて順番に命令が適用され，最後に操作のリストとストるアカウントのアドレス src をスタックに積む．

レージのペアが一番上に積まれた状態のスタックが残• 8 行目の CONTRACT T は スタックトップから ad-日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

4


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16



{
parameter unit ;storage unit ;code{ CDR ;NIL operation ;SOURCE ;CONTRACT unit ;ASSERT_SOME ;AMOUNT ;UNIT ;TR AN SFER_ T OKE NS ;CONS ;
PAIR ;
}

/*
/*
/*
/*
/*
/*
/*
/*
/*
/*
/*

( param , st ) */st */[] ▷ st */src ▷ [] ▷ st */Some ( Contract src ) ▷ [] ▷ st */( Contract src ) ▷ [] ▷ st */amount ▷ ( Contract src ) ▷ [] ▷ st */Unit ▷ amount ▷ ( Contract src ) ▷ [] ▷ st */( Transfer Unit amount ( Contract src ) ) ▷ [] ▷ st */[ Transfer Unit amount ( Contract src ) ] ▷ st */([ Transfer Unit amount ( Contract src ) ] , st ) */

}




図3

boomerang.tz

dress 型の値 addr を取り出し，(1) addr にコン

vcontr) は，vtz 分の量の通貨を，アカウント

トラクトが関連づけられていてかつ (2) 関連づけ

vcontr へ，引数 varg とともに送る，という操られたコントラクトの引数の型が T であるかを検作を表している．これをプログラムの返り値の操査する．型検査に成功すれば，Some (Contract

作のリストに含めておくと，プログラムの実行終addr) が積まれるが，失敗すれば None が積まれ了後に vcontr への送金が実行される．

る．Contract コンストラクタは，あるアドレス• 13 行目の CONS はスタックが v1 ▷ v2 ▷ s の形

に対して型検査されたコントラクトを表す値をの場合，v1 と v2 を取り出し，それらを Cons し構築する．Tezos において取引の起点となり得る

たリスト v1 :: v2 をスタックに積む．

アカウントは人の操作するアカウントだけであ• 14 行目の PAIR はスタックのトップの要素と 2

り，Michelson 上でこれは unit 型を引数として番目の要素を取り出し，それらのペアをスタック受け取るコントラクトとして扱われるため，このに積む．

場合の型検査は常に成功し，オプションの Some(Contract src) がスタックへ積まれる．

プログラムの終了時のスタックは，このプログラム
終了後に続いて行われる操作のリストと，ブロック• 9 行目の ASSERT SOME は，スタックトップの op-

チェーンに保存されるストレージの値 storage’ のペtion 型の値を取り出し，それが Some v であれば

アのみが積まれている状態でなければならない．このv をスタックに積み，None であれば例外を発生とき，プログラム実行前のストレージの値 storage

させる．

と，プログラム実行後のストレージの値 storage’ の• 10 行目の AMOUNT はこのプログラムが呼び出された際に関連づけられたアカウントへ送金された通貨の量 amount をスタックに積む．

• 11 行目の UNIT は unit 型の値 Unit をスタックに積む．

• 12 行目の TRANFER TOKENS は，スタックが varg
▷ vtz ▷ vcontr ▷ tl の 形 を し て い る 場 合 ，varg, vtz, vcontr を ス タック か ら 取 り 出 して (Transfer varg vtz vcontr) を tl の上に積む．operation 型の値 (Transfer varg vtz

型が一致している必要がある．

Michelson には静的型検査が備えられている．それぞれの命令には，命令の実行前と実行後のスタックの状態を型で表した型付け規則が存在する．命令を実行する前にスタックの状態が型付け規則に則った形でな
い場合，命令は失敗する．これを防ぐために，プログ
ラム実行前に静的な型検査が行われる．

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

5


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19



{
parameter unit ;storage unit ;<< ContractAnnot { _ | True } - >{ ( ops , _ ) | match ops with [ Transfer < unit > Unit tz ( Contract addr ) ]- > addr = source && tz = amount | _ - > False } &{ _ | False } >>code { CDR ;NIL operation ;SOURCE ;CONTRACT unit ;ASSERT_SOME ;AMOUNT ;UNIT ;
TRAN S FER_ TOK E NS ;CONS ;
PAIR ;
}
}




図4

boomerang.tz（注釈付き）

2. 2 Helmholtz
Helmholtz は ，Nishida ら に よって 開 発 さ れ た
Michelson の静的型検証ツールである [4]．Helmholtz

した以下のような記法によって与えている．

{(param,st) | pre} ->{(ops,st’) | post} & {exc | abpost}

は，Michelson の単純型システムを拡張した篩型シ

こ こ で ，param, st, ops, st’, exc は 変 数 ，

ステムに基づいた型検査アルゴリズムを実装していpre, post, abpost は条件式を表す．この仕様は，る．具体的には，Helmholtz は，篩型の形式で表現さ(1) プログラムの引数を param，プログラム実行前のれたユーザーの定める仕様が記述された注釈付きのストレージを st として，プログラムが性質 pre を満Michelson プログラムを入力として受け取ると，上述たす状態で呼び出されたならば，(2) プログラムの実の篩型システムに基づいて設計された制約生成アル行が正常終了した時，返り値の operation list 型

ゴリズムに基づき型検査を行う．その際にプログラムの値を ops, 更新後のストレージを st’ として，性質が注釈された仕様に対して型付け可能であることを

post を満たし，(3) プログラムが例外を発生して終保証するための検証条件が生成され，その検証条件

了した場合，その時のスタックのトップの要素を excの成否が SMT ソルバ Z3 [2] によってチェックされる．

として，性質 abpost を満たす，ということを意味し検証条件が成り立てば，プログラムが篩型システムている．(1) を Precondition，(2) を Postcondition，によって型付け可能であるため，篩型システムの健全(3) を Ab-Postcondition と呼ぶ．

性からプログラムが仕様を満たすことが保証される．

条件式には，AMOUNT によって呼び出される通貨量

本論文では Helmholtz が用いている篩型システムとを表す amount や，SOURCE によって呼び出されるア型検査アルゴリズムについては詳述しない．詳細はドレスを表す source など，事前に環境内に定義されHelmholtz に関する論文 [4] を参照されたい．

た変数を用いることができる．また，条件式に用いな

図 4 に示したプログラムは，Helmholtz に入力として与えられるプログラムの一例で，仕様を記述した
注釈を boomerang.tz に挿入したものである．

4–7 行目の ContractAnnot とラベル付けされた注
釈は，Michelson プログラムの仕様を，篩型を参考とい変数をと書くことができる．

以下，図 4 中の ContractAnnot の注釈に記述された仕様について説明する．

• Precondition は {| True} となっていて，いかなる引数とストレージに対しても条件式が成り立つ．つまり，プログラムが正常に動作するために引数とストレージに対して要求される条件

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

6


1
2
3
4





( declare - fun a () Bool )( declare - fun b () Bool )( assert (= ( not ( and a b ) ) ( or ( not a ) ( not b ) ) ) )( check - sat )



図5



1
2
3
4
5
6

sample1.smt2

( declare - const a Int )( declare - const b Int )( assert (= (+ a b ) 20) )( assert (= (+ a (* 2 b ) ) 10) )( check - sat )( get - model )



図6



sample2.smt2がないことを表している．

• Postcondition は { (ops,) | match ops

with [Transfer<unit> Unit tz (Contractaddr)] -> addr = source && tz = amount |-> False } と なって い る ．条 件 式 に は リ
ス ト ops に 対 す る match 文 が 記 述 さ れていて，[Transfer<unit> Unit tz (Contractaddr)] という形であった場合は，addr と source

1
2
3
4
5
6
7



sat
(
( define - fun b () Int( - 10) )( define - fun a () Int
30)
)



図7



sample2.smt2 の出力結果が等しく，かつ tz と amount が等しい，という条件が記述されている．この条件は，12 行目の型の変数 a, b について，a ∧ b ≡ a ∨ b が充足可能でTRANSFER TOKENS によって積まれた送金操作があるかどうかを判定する．その結果，充足可能である

返り値の ops のただ 1 つの要素であり，それにため，sat という出力を返す．

含まれている引数が，7 行目の SOURCE や 10 行

Z3 には，制約集合を充足するような変数束縛（変数

目の AMOUNT によって積まれた値と一致している

への値の割り当て）を出力する機能が存在する．図 6

ことを確認している．また，2 つ目のパターンに示す sample2.smt2 は，Int 型の変数 a, b についマッチは，ops がそれ以外の形にはなり得ないとての連立方程式が制約集合として与えられ，充足可能いう条件を表している．

性を判定した後，6 行目に get-model が呼び出され• Ab-Postcondition は {| False} となっていており，直前の check-sat による判定が sat であって，いかなる例外に対しても条件式が成り立たた場合，制約集合を満たすような変数束縛が出力されない．つまり，例外が発生しないことを表してる．つまり，制約集合 C に対して get-model によっいる．

て得られる変数束縛 M は C を充足する（M |= C と以上のように，ContractAnnot にはプログラムが記述する）．実際の Z3 による出力は図 7 のようにな

期待通りの挙動を行うための条件が記述される．注釈

る．3–4 行目の (define-fun b () Int (-10)) は，には Assert, LoopInv など，ContractAnnot 以外に

変数 b が Int 型の-10 という値に束縛されているこも様々な用途のものがあるが，本論文では扱わないたとを表す．b の右隣の () は引数の型で，変数が関数め割愛する．

に束縛される場合は引数の型が () の中に記述される．
以降，get-model によって得られる変数束縛をモ

2. 3 Z3 とモデル出力機能

デル，その出力機能をモデル出力機能と呼ぶ．

Z3 は，Microsoft Research が開発した SMT ソル
バである [2]．制約集合を SMT-LIB 形式で記述した

2. 4 Helmholtz における Z3 を用いた検証

ファイルを Z3 に入力として与えることで，その充足

Helmholtz は注釈が加えられた Michelson プログ

可能性を判定することができる．

ラムが与えられると，上述した篩型システムに基づい

図 5 に示す sample1.smt2 は，SMT-LIB ファイルて型検査を行う．その際にプログラムが型付け可能での例で，これが Z3 に入力として与えられると，Bool

あるための検証条件が生成される．Z3 を用いてこの

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

7


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32



...
( assert( and ( or (= 0 amount ) ( > amount 0) )( or (= amount 9 2 2 3 3 7 2 0 3 6 8 5 4 7 7 5 8 0 7 ) ( > 9 2 2 3 3 7 2 0 3 6 8 5 4 7 7 5 8 07 amount ) )(= ( unpack_opt ! unit ( pack ! unit unit_l14_c10 -14 _0024 ) )(( as some ( Option Unit ) ) unit_l14_c10 -14 _0024 ) )( or (= 0 amount_l13_c10 -16 _0023 ) ( > amount_l13_c10 -16 _0023 0) )...
(= source_l10_c10 -16 _0013 source )(= v0021 ( as seq . empty ( Seq Operation ) ) )(= v0022 ( second pa ram_stor_0010 ) ) (= param_stor_0010 v0004 )(=( contra ct_ ty_op t(( as mk - pair ( Pair String String ) ) ( first self_addr ) "% default ") )(( as some ( Option String ) ) " unit ") )
( not
( ite
( and ( < 0 ( seq . len ( first v0029 ) ) )( is - transferToke ns ( seq . nth ( first v0029 ) 0) )( is - some
( unpack_opt ! unit ( transferData ( seq . nth ( first v0029 ) 0) ) ) )(= 0( seq . len( seq . extract ( first v0029 ) 1 ( - ( seq . len ( first v0029 ) ) 1) ) ) ) )( and(= ( ex tra ctCo n tra ct ( transferContract ( seq . nth ( first v0029 ) 0) ) )source ) (= ( transferMutez ( seq . nth ( first v0029 ) 0) ) amount ) )false ) ) ) )( echo" Finding counter - example for postcondition of ContractAnnot at line 0 , characters -1 - -1")
( check - sat )
...



図8

boomerang.tz の検証時に生成される，Postcondition に対する検証条件

検証条件の成否を検査することで，プログラムの検証

令で SMT ソルバに制約 C が充足可能であるかどを行う．

うかを検査するよう指示する．2 行目以降に記述さ生成される検証条件について，より詳しく説明すれている assert 命令の引数が Helmholtz によっる．検証条件は SMT-LIB 形式と呼ばれる，SMT ソて生成された検証条件である．Helmholtz によっ

ルバに対する命令を記述するプログラムとして生成さて生成される検証条件は，∃⃗
x.Ax ∧Constr ∧¬Spe

れる．図 8 は，図 4 の boomerang.tz を Helmholtzという形をしている．ここで ⃗x は Ax と Constr

で検証した時に生成される検証条件を表現した SMT-と Spe に自由に出現するすべての変数の列でLIB 形式のプログラムの一部であり，具体的にはある．

boomerang.tz が実行終了時に Postcondition の条件– Ax はある種の型の値が満たすべき公理でを満たすことを保証する検証条件に該当するコード

ある．3–4 行目が該当する部分で，アカウン

である．以下ではこのコードについて説明を加える．

トに送金された通貨を表現する変数 amount• 1 行目より前の図 8 では省略した部分にはの値が非負の一定範囲に収まることを表現

declare-fun や declare-const を用いた変数するための制約が記述されている．

宣言が含まれている．検証条件中における変数– Constr は，Helmholtz の制約生成アルゴ

は，プログラム中の各行におけるスタック上の各

リズムによって生成された条件で，Precon-

要素を表現する用途や，型検査時に課される制約

dition が成り立つ状態からプログラムの実を表現するための一時変数としての用途に使用行を開始した場合にプログラム終了時にされている．

成り立つ条件である．これらの条件は篩型• SMT-LIB 形式においては，(assert C) という命システムに基づいて計算されており，5–15

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

8

行目までが Constr に相当する条件である（一部を省略している）．Constr は各命令の挙動を表現する制約の論理積になっている．例えば，コード中の 9 行目の CDR に対応する制約は 11 行目の (= v0022 (second

param stor 0010)) である．これは命令実
行前のスタックのトップの値にあたる変数である param stor 0010 の第 2 要素と，命令

1
2
3
4
5
6
7



=========== solver results ===========
Finding counter - example for ab - postcondition ofContractAnnot at line 0 , characters -1 - -1
unsat
Finding counter - example for postcondition ofContractAnnot at line 0 , characters -1 - -1
unsat=========== final result ===========
VERIFIED

図9

boomerang.tz の検証結果

実行後にスタックに積まれた値にあたる変数である v0022 が等しいことを意味する制約である．†2は Postcondition に対する検証条件で，4 行目のメッ– ¬Spe は，Postcondition を満たすための制条件の Z3 による検証結果が示されており，成功した

約 Spe の否定である．16–28 行目がこれに場合には unsat が出力される．各検証条件の検証結相当する．

果が全て unsat であることが確認されるとプログラ

セージに対応している．3,5 行目にはそれぞれの検証

Helmholtz はプログラム終了時に成り立つ条件

ムの検証は成功したとみなされ，6–7 行目の final

Ax ∧ Constr が常に Postcondtion を含意する

result に VERIFIED と出力される．

こと，すなわち ∀⃗x.Ax ∧ Constr ⇒ Spe が成り立つことを検証する．この条件は，その否定

3 エラー原因提示手法∃⃗x.Ax ∧ Constr ∧ ¬Spe が成り立たないことと3. 1 エラーの原因としてのモデル等価であるため，SMT ソルバで検証するため

現在の Helmholtz は，検証に失敗した際にその原には Ax ∧ Constr ∧ ¬Spe が充足不能であるこ因を出力しないため，失敗の原因を理解するのが困難とを検査すればよい．したがって，生成されたであるという問題がある．例えば，図 10 に示すプロ

SMT-LIB のコードでは assert の引数としてグラム boomerang neg.tz を Helmholtz に入力する

Ax ∧ Constr ∧ ¬Spe を与え，その充足可能性と検証に失敗するが，その際の Helmholtz の出力はを命令 check-sat によって検査し，その結果が

図 11 に示す通りであり，検証が失敗したこと以上の充足不能を意味する unsat であれば検証が成功

情報は出力されない．

する．

boomerang neg.tz に対してどのような情報が出力

図 9 は，図 4 の boomerang.tz を入力として検証されると検証失敗の原因を特定するために有用であるを行なった時に得られる出力結果である．1–5 行目

かを考えるために，このコードをより詳しく見てみよの solver results には，各検証条件の検証結果がう．boomerang neg.tz は図 4 の boomerang.tz の仕示されている．boomerang.tz に含まれている注釈の様のうち 6 行目の addr = sourceを addr = sender

ContractAnnot に対しては，2 つの検証条件が生成さに書き換えて得られている．仕様における senderは，れている．1 つ目は Ab-Postcondition に対する検証

取引全体の起点となったアドレスを表す sourceと条件で，2 行目のメッセージに対応している．2 つ目は異なり，このスマートコントラクトに直前に送金したアカウントのアドレスを表す．したがって，一†2 本研究では Helmholtz の実装を改善し，できるだけ変数名にその値がプログラム中のどの命令によって生成された値であるかを表現する情報を与えている．例
えば 9 行目の source l10 c10-16 0013 は，コード中の 10 行目の 10–16 文字目にある SOURCE の実行後に生成される変数である．
（0013 は Helmholtz によって変数名に順に割り当てられる数字である．
）

般には senderと sourceは異なる．boomerang.tz とboomerang neg.tz はプログラム本体は共通である
ため，どちらにおいても実際にはプログラム終了時
点では addr = sourceが成り立っている．したがって boomerang neg.tz では addr = sourceが addr =日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

9


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19



{
parameter unit ;storage unit ;<< ContractAnnot { _ | True } - >{ ( ops , _ ) | match ops with [ Transfer < unit > Unit tz ( Contract addr ) ]- > addr = sender && tz = amount | _ - > False } &{ _ | False } >>code { CDR ;NIL operation ;SOURCE ;CONTRACT unit ;ASSERT_SOME ;AMOUNT ;UNIT ;
TRAN S FER_ TOK E NS ;CONS ;
PAIR ;
}
}




図 10

boomerang neg.tz


1
2
3
4
5
6
7

 それぞれ違うアドレスの値が割り当てられており，先=========== solver results ===========
Finding counter - example for ab - postcondition ofContractAnnot at line 0 , characters -1 - -1
unsat
Finding counter - example for postcondition ofContractAnnot at line 0 , characters -1 - -1sat=========== final result ===========
UNVERIFIED



図 11

述した検証が失敗する原因を説明するための情報が含まれていると言える．
一方で， Z3 が返すモデルには宣言された全ての変数に対する変数束縛が含まれるため，検証が失敗する

boomerang neg.tz の検証結果

原因とは関連性のない情報が多く含まれている．例えば，図 12 のモデルでは，source と sender 以外の変数束縛は関連性のない情報といえる．検証が失敗する
原因の説明として，モデルの情報をエラーメッセージ

senderを含意しないために検証が失敗する．このこに用いるために，元のモデルから関連性のない情報をとから，senderと sourceが異なる場合に検証が失敗

取り除き，関連性のある情報だけを残したモデルを得することを示唆する情報が得られれば，検証が失敗しる手続きを与える．この操作をモデルを極小化する，た原因を理解するのに有用であると考えられる．

と呼び，そのアルゴリズムをモデル極小化アルゴリズ

2. 3 節で言及したように，Z3 による充足可能性のムと呼ぶ．

判定の結果が sat である場合，モデル出力機能を用いて，制約集合を満たす変数束縛を得ることができ

3. 2 モデルを極小化する手順

る．図 12 は，図 10 の boomerang neg.tz を検証しHelmholtz がプログラムの検証に失敗し，生成された際に Postcondition に対する検証条件から得られた検証条件のうち，いずれかの検証結果が sat となっるモデルである．生成された検証条件のコード中のたとする．その検証条件を Ax ∧ Constr ∧ ¬Spe とお(check-sat) の直後に (get-model) を挿入するこ

くと，M |= Ax ∧ Constr ∧ ¬Spe が成り立つようなとでモデルを取得することができる．検証条件中にモデル M をモデル出力機能から得ることができるの宣言された変数に対する変数束縛情報が並んでいるで，このモデル M を極小化する手順を Algorithm 1

が，そのうちの 29–30 行目，および 31–32 行目には，に示す．

source および sender に対する変数束縛情報がある

以下，詳しく説明する．

（mk-pair s1 s2 は，その変数に対応したアドレスを• 1 行目では，与えられたモデル M を等式制約の表す値である）．これを見ると，source と sender に形に変換している．例えば，図 12 の 2–3 行目

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

10


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49



(
( define - fun v0021 () ( Seq Operation )( as seq . empty ( Seq Operation ) ) )( define - fun v0004 () ( Pair Unit Unit )( mk - pair unit unit ) )( define - fun v0022 () Unit
unit )( define - fun transfer_tokens_l15_c10 -25 _0025 () Operation( transferTo kens " t " 39 ( contract ( mk - pair " i " "% default ") ) ) )( define - fun self_addr () ( Pair String String )( mk - pair " n " "% default ") )( define - fun source_l10_c10 -16 _0013 () ( Pair String String )( mk - pair " i " "% default ") )( define - fun v0020 () Contract( contract ( mk - pair " i " "% default ") ) )( define - fun v0029 () ( Pair ( Seq Operation ) Unit )( let (( a !1 ( seq . unit ( transferTokens " t " 39 ( contract ( mk - pair " i " "% default ") ) ) ) ) )( mk - pair a !1 unit ) ) )( define - fun unit_l14_c10 -14 _0024 () Unit
unit )( define - fun amount_l13_c10 -16 _0023 () Int39)( define - fun contract_l11_c10 -23 _0014 () ( Option Contract )( some ( contract ( mk - pair " i " "% default ") ) ) )( define - fun p ara m_sto r_0 010 () ( Pair Unit Unit )( mk - pair unit unit ) )( define - fun cons_l16_c10 -14 _0026 () ( Seq Operation )( seq . unit ( trans ferTokens " t " 39 ( contract ( mk - pair " i " "% default ") ) ) ) )( define - fun source () ( Pair String String )( mk - pair " i " "% default ") )( define - fun sender () ( Pair String String )( mk - pair " u " "% default ") )( define - fun amount () Int39)( define - fun balance () Int40)( define - fun unpack_opt ! unit (( x !0 String ) ) ( Option Unit )( some unit ) )( define - fun seq . nth_u (( x !0 ( Seq Operation ) ) ( x !1 Int ) ) Operation( setDelegate ( as none ( Option String ) ) ) )( define - fun c ont ract_ ty_ opt (( x !0 ( Pair String String ) ) ) ( Option String )( ite (= x !0 ( mk - pair " i " "% default ") )( some " unit ")( ite (= x !0 ( mk - pair " n " "% default ") )( some " unit ")( some " unit ") ) ) )( define - fun pack ! unit (( x !0 Unit ) ) String" t ")
)




図 12

boomerang neg.tz の Postcondition に対するモデルの v0021 に関する束縛は，制約 (= v0021 (asC から取り除かれる．どのようにして xi = vi がseq.empty (Seq Operation))) に変換される．

検証失敗に関係のない要素であるかどうかを判得られた C について，∀⃗
x.C ⇒ Ax ∧ Constr ∧定するかは後述する．

¬Spe が成り立つことに注意されたい．
• 2 行目から始まるループでは，連言の形をした• 8 行目で，最終的に得られた C をモデルの形に変換し，極小化されたモデルとして返す．

C 中の制約を順番にチェックし，それぞれが検証
失敗に関係のない要素であるかどうかを検査し3. 3 検証失敗原因への関連性を判定する方法ている．もし xi = vi が検証失敗に関係のない要

図 1 の 4 行目で，等式 xi = vi が検証失敗に関連の素であると判定されたならば，それは 5 行目でない要素であるかを判定する方法について説明する．

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

11(seq.nth (first v0029) 0))) sender) （仕様中Algorithm 1 モデル極小化アルゴリズム
Input: 検 証 条 件 Ax ∧ Constr ∧ ¬Spe と M |=の addr = sender に対応する制約）を満たすような変数束縛が存在し，その場合は ¬Spe が成り立たな

Ax ∧ Constr ∧ ¬Spe であるようなモデル M :=い．source と sender が異なる値である，という追{x1 7→ v1 , . . . , xn 7→ vn }加の条件を満たしている場合に初めて ¬Spe が成り立Output: 極小化されたモデル M∧
1: C ← i∈{1,...,n} xi = vi′

2: for i = 1 to n do

ち，Ax ∧ Constr ∧ ¬Spe が sat となる．
このようなケースの場合，Ax ∧ Constr が成り立っているという前提の上で，¬Spe が成り立つ原

3:

C ′ ← C\ {xi = vi }因となる要素を残すことによって，検証失敗の原因

4:

if xi = vi が検証失敗に関連がない thenとして関係のある情報のみを含んだモデルになる

5:
6:C ← C′
end ifと考えられるため，M |= Ax ∧ Constr ⇒ ¬Spe が成り立つように M を極小化すればよい．よって，

7: end for「∀⃗x.C ′ ⇒ (Ax ∧ Constr ⇒ ¬Spe) が成り立つ」場

8: M ′ ← C の各等式制約を変数束縛に変換したもの

合に，等式制約 xi = vi が検証失敗に関係のない

9: return M ′制約であると判定する．これを確かめるためには，

C ′ ∧ Ax ∧ Constr ∧ Spe が unsat であるかどうかを Z3 によって判定すればよい．このケースでは，
検証条件 Ax ∧ Constr ∧ ¬Spe が sat であった場合，

M ′ |= Ax ∧ Constr ⇒ ¬Spe となるような M ′ を M

以下の 2 つのケースが考えられる．

から得ることができる．

ケース 1 ∀⃗
x.Ax ∧ Constr ⇒ ¬Spe が成り立たないケース．つまり，プログラムが実行された際に，変数が何らかの条件を満たしている場合にのみ仕様が成り立たない，というケース．

3. 3. 2 ケース 2: ∀⃗x.Ax ∧ Constr ⇒ ¬Spe が成り立つ場合
このケースに該当する例として，図 14 に示した

ケース 2 ∀⃗
x.Ax ∧ Constr ⇒ ¬Spe が成り立つ

プログラム empty map.tz が挙げられる．これはス

ケース．つまり，プログラムが実行されれば，変トレージを空のマップで更新するプログラムである

数がいかなる値であっても仕様が成り立たない，が，4–6 行目の注釈 ContractAnnot に記述されたというケース．

仕様は，更新後のストレージに格納されているマッ

この 2 つのケースで，等式制約が検証失敗の原因

プのキー"hoge"に対応する要素が 0 であるというへの関連性がないかを判定する方法を変える必要が条件を課しており，そのマップは空であるはずなのある．以下ではそれぞれのケースについて説明する．

で，Postcondition に対する検証結果が sat となり，

Helmholtz による検証は失敗する．図 15 は，その検3. 3. 1 ケース 1: ∀⃗x.Ax ∧ Constr ⇒ ¬Spe が成り立たない場合

証時に Postcondition に対して生成される検証条件である．3–14 行目が Ax ∧ Constr に，15 行目が ¬Spe

こ の ケ ー ス に 該 当 す る 例 と し て ，??節 で 示に該当する制約であるが，プログラムの最終スタッ

し た ，図 10 の boomerang neg.tz が 挙 げ ら れ る ．

クを表す変数である v0015 の第 2 要素が空マップで

図 13 は ，そ の 検 証 時 に Postcondition に 対 し てあるという条件が Ax ∧ Constr に含まれている一方

生 成 さ れ る 検 証 条 件 で あ る ．3–15 行 目 が Ax ∧で，Spe が Postcondition を満たすための制約である

Constr ，16–28 行 目 が ¬Spe に 該 当 す る 制 約 で あため，∀⃗
x.Ax ∧ Constr ⇒ ¬Spe が成り立つ．よって，るが，∃⃗x.Ax ∧ Constr となる ⃗x について，26–27

Ax ∧ Constr を満たすような変数束縛は必ず ¬Spe を

行目の (= (extractContract (transferContract満たすため，Ax ∧ Constr ∧ ¬Spe が sat となる．

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

12


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32



...
( assert( and ( or (= 0 amount ) ( > amount 0) )( or (= amount 9 2 2 3 3 7 2 0 3 6 8 5 4 7 7 5 8 0 7 ) ( > 9 2 2 3 3 7 2 0 3 6 8 5 4 7 7 5 8 07 amount ) )(= ( unpack_opt ! unit ( pack ! unit unit_l14_c10 -14 _0024 ) )(( as some ( Option Unit ) ) unit_l14_c10 -14 _0024 ) )( or (= 0 amount_l13_c10 -16 _0023 ) ( > amount_l13_c10 -16 _0023 0) )...
(= source_l10_c10 -16 _0013 source )(= v0021 ( as seq . empty ( Seq Operation ) ) )(= v0022 ( second pa ram_stor_0010 ) ) (= param_stor_0010 v0004 )(=( contra ct_ ty_op t(( as mk - pair ( Pair String String ) ) ( first self_addr ) "% default ") )(( as some ( Option String ) ) " unit ") )
( not
( ite
( and ( < 0 ( seq . len ( first v0029 ) ) )( is - transferToke ns ( seq . nth ( first v0029 ) 0) )( is - some
( unpack_opt ! unit ( transferData ( seq . nth ( first v0029 ) 0) ) ) )(= 0( seq . len( seq . extract ( first v0029 ) 1 ( - ( seq . len ( first v0029 ) ) 1) ) ) ) )( and(= ( ex tra ctCo n tra ct ( transferContract ( seq . nth ( first v0029 ) 0) ) )sender ) (= ( transferMutez ( seq . nth ( first v0029 ) 0) ) amount ) )false ) ) ) )( echo" Finding counter - example for postcondition of ContractAnnot at line 0 , characters -1 - -1")
( check - sat )
...



図 13

boomerang neg.tz の検証時に生成される，Postcondition に対する検証条件

 が unsat であるかどうかを Z3 によって判定すればよ


1
2
3
4
5
6
7
8
9
10
11
12
13



い．このケースでは，M ′ |= Ax ∧ Constr となるよ{
parameter bool ;storage ( map string int ) ;<< ContractAnnot{ _ | True } - >{ _ , ret_map | find_opt " hoge " ret_map =Some 0 }& { _ | False } () >>code { DROP ;EMPTY_MAP string int ;NIL operation ;PAIR ;}}



うな M ′ を M から得ることができる．

3. 4 モデル極小化アルゴリズム
以上を踏まえて，設計したアルゴリズムを Algo-rithm 2 に示す．このアルゴリズムでは，まず検証条
件がケース 1 とケース 2 のどちらに該当するかを 2


図 14

empty map.tz

行目においてチェックする．その後 1 で示したアルゴリズムを実行するが，その際に各等式が検証失敗に関連のない要素であるかどうかの検査を，5 行目と 12 行目で，それぞれ上に述べた通りに行っている．

このようなケースの場合，Ax ∧ Constr が成り立つ
原因が ¬Spe が成り立つ原因，つまり検証が失敗する

SAT(P )(および UNSAT(P )) は，論理式 P が充足可能 (不能) であることを示している．

原因に等しいと考えられるため，M |= Ax ∧ Constrが成り立つように M を極小化すればよい．よって，′

4 アルゴリズムの適用例「∀⃗
x.C ⇒ Ax ∧ Constr が成り立つ」場合に，等式制

本章では，Helmholtz の検証が失敗するようない

約 xi = vi は検証失敗の原因に関連がないと判定す

くつかのプログラムについて，検証時に得られる検証′

る．これを確かめるためには，C ∧ ¬(Ax ∧ Constr )条件とモデルを入力として，3. 4 節のモデル極小化ア日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

13


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19



...
( assert( and(= v0015(( as mk - pair ( Pair ( Seq Operation ) ( Array String ( Option Int ) ) ) )nil_l10_c9 -22 _0012 empty_map_l9_c9 -29 _0011 ) )(= nil_l10_c9 -22 _0012 ( as seq . empty ( Seq Operation ) ) )(= empty_map_l9_c9 -29 _0011(( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) )(= pa ra m_s tor_ 0 010 v0004 )(=( contra ct_ ty_op t(( as mk - pair ( Pair String String ) ) ( first self_addr ) "% default ") )(( as some ( Option String ) ) " bool ") )( not (= ( select ( second v0015 ) " hoge ") (( as some ( Option Int ) ) 0) ) ) ) )( echo" Finding counter - example for postcondition of ContractAnnot at line 0 , characters -1 - -1")
( check - sat )
...



図 15

empty map.tz の検証時に生成される，Postcondition に対する検証条件

ルゴリズムを適用した結果を示す．なお，極小化アルぼ全ての変数に対する変数束縛が残っていて要素数がゴリズムを適用する前のモデルは特に言及しないた

多く，検証失敗の原因の説明としての粒度は粗いもの

め付録に示す．適宜参照されたい．

になっているが，source や sender などの関連性のない変数束縛情報は取り除かれ，関連性のある情報のみが残ったモデルを得ることに成功している．

4. 1 boomerang neg.tz
図 10 で示した boomerang neg.tz について，図 13に 示 し た Postcondition に 対 す る 検 証 条 件 Ax ∧4. 3 transfer.tz

Constr ∧ ¬Spe と，図 12 に示したモデル M を入力と

図 18 に示す transfer.tz は，パラメータとして受けして，モデル極小化アルゴリズムを適用すると，図 16

取ったアドレスについて，unit 型のコントラクトが′に示すようなモデル M が得られる．3. 2 節で述べた

関連づけられているならば，そのアドレスのアカウ

通りケース 1 に該当し，M ′ |= Ax ∧ Constr ⇒ ¬Spe

ントに対して送金するプログラムである．3–6 行目の′′となる M が出力されている．M には source と

注釈 ContractAnnot の Postcondition には，返り値sender が異なる値に束縛されているという情報のみの ops に含まれているアドレスがパラメータのものが残っており，¬Spe が成り立つ原因となる要素のみと一致するかどうかを確かめる，という仕様の記述がを含んだモデルに極小化することに成功している．

ある．しかし，match 文の 1 つ目のパターンが unit
型でなく int 型のコントラクトに対する送金操作と4. 2 empty map.tz

なっていて型が一致せず，2 つ目のパターンにマッチ

図 14 で示した empty map.tz について，図 15 に示するため，Postcondition に対する検証結果が sat とした Postcondition に対する検証条件 Ax ∧ Constr ∧なり，検証は失敗する．

¬Spe と，図 23 に示したモデル M を入力として，モ

図 19 に 示 す Postcondition に 対 す る 検 証 条 件

デル極小化アルゴリズムを適用すると，図 17 に示す

Ax ∧ Constr ∧ ¬Spe と，図 24 に示す Postcondi-

ようなモデル M ′ が得られる．3. 2 節で述べた通り

tion に対する検証時に得られるモデル M を入力とし′′ケース 2 に該当し，M |= Ax ∧ Constr となる M がて，モデル極小化アルゴリズムを適用すると，図 20

出力されている．ケース 1 と比べると，Ax ∧ Constrに示すようなモデル M ′ が得られる．このプログラムが成り立つように極小化する，という操作を行っていにアルゴリズムを適用する場合，プログラムが正常にるため，Ax ∧ Constr の等式制約に含まれているほ実行されれば必ず仕様が成り立たないにも関わらず日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

14

む値になるため，Spe に含まれる (unpack opt!int

Algorithm 2 モデル極小化アルゴリズム (完成版)(transferData (seq.nth (first v0025) 0))) は

Input: 検 証 条 件 Ax ∧ Constr ∧ ¬Spe と M |=None を返し，その場合 ¬Spe が sat となる．しかし，

Ax ∧ Constr ∧ ¬Spe であるようなモデル M :=仮に unpack opt!int に Some n（n は任意の整数値）{x1 7→ v1 , . . . , xn 7→ vn }を割り当てた場合，¬Spe が unsat となる．つまり，Output: 極小化されたモデル M∧
1: C ← i∈{1,...,n} xi = vi′

2: if SAT(Ax ∧ Constr ∧ Spe) thenfor i = 1 to n do

3:

C ′ ← C\ {xi = vi }4:′

if UNSAT(C ∧ Ax ∧ Constr ∧ Spe) then

5:

C←C

6:

M ′ には unpack opt!int の変数束縛のみが残っていて，None を表す値に束縛されていることから，¬Spe が成り立つ原因となる要素と言える．そのため，の変数は Helmholtz が検証条件を生成するために定義された補助的な変数であり，これをそのままエラー

9: elsefor i = 1 to n do

10:

ス 1 に該当するのである．

極小化することに成功していると言える．しかし，こend for8:∃⃗x.¬(Ax ∧ Constr ⇒ ¬Spe) が成り立つため，ケー

検証失敗に関連性のある情報のみを含んだモデルに′end if7:

プログラムを実際に実行した際は起こり得ないが，′C ← C\ {xi = vi }11:′

if UNSAT(C ∧ ¬(Ax ∧ Constr )) then

12:

C←C

13:

′

の原因として示したとしても，ユーザーにとってあまり直感的でないと考えられる．このような情報を，ユーザーにとってわかりやすい形で示すための手段を考えることは，今後の課題の 1 つである．

end if14:

end for15:

16: end if′

17: M ← C の各等式制約を変数束縛に変換したもの

4. 4 boomerang ab neg.tz
図 21 に 示 す boomerang ab neg.tz は ，図 4 のboomerang.tz の コ ー ド の ，11 行 目 の SOURCE を
SENDER に書き換えたものである．このプログラムのHelmholtz による検証において，Postcondition に対


1
2
3
4
5
6

 する検証結果は 3. 1 節で述べた boomerang neg.tz の(( define - fun source () ( Pair String String )( mk - pair " i " "% default ") )( define - fun sender () ( Pair String String )( mk - pair " u " "% default ") )
)


図 16

検証と同様の理由で sat となるが，Ab-Postcondition
に対する検証結果も sat となる．boomerang.tz においては，SOURCE によって積まれるアドレス source に 関連づけられたコントラクトの引数の型は必ず unit
極小化された boomerang neg.tz のモデルであるため，その後の CONTRACT unit による型検査は成功して Some (Contract source) が積まれるが，ケース 1 に該当する，という稀な結果になる．図 19

boomarang ab neg.tz においては，SENDER によっての 26 行目にある unpack opt!int という関数は，引積まれるアドレス sender に関連づけられたコント

数の Trasfer 値に含まれるコントラクトの型が int

ラクトの引数の型は必ずしも unit であるとは限らなであるかどうかを判定してオプション型を返す関数

いため，その後の CONTRACT unit による型検査に失で，注釈中の match 文の 1 つ目のパターンで int 型

敗して None が積まれる可能性があり，その場合はそのコントラクトであるかどうかを判定する部分に対の後の ASSERT SOME によって例外が発生する．Ab-応している．Ax ∧ Constr が成り立つ場合，この関Postcondition に記述された仕様 {数の引数に取られる値は unit 型のコントラクトを含かなる例外に対しても満たされないため，生成される| False} はい日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

15


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19



(
( define - fun p ara m_sto r_0 010 () ( Pair Bool ( Array String ( Option Int ) ) )( mk - pair false (( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) ) )( define - fun empty_map_l9_c9 -29 _0011 () ( Array String ( Option Int ) )(( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) )( define - fun nil_l10_c9 -22 _0012 () ( Seq Operation )( as seq . empty ( Seq Operation ) ) )( define - fun v0004 () ( Pair Bool ( Array String ( Option Int ) ) )( mk - pair false (( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) ) )( define - fun self_addr () ( Pair String String )( mk - pair " i " "% default ") )( define - fun v0015 () ( Pair ( Seq Operation ) ( Array String ( Option Int ) ) )( mk - pair ( as seq . empty ( Seq Operation ) )(( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) ) )( define - fun c ont ract_ ty_ opt (( x !0 ( Pair String String ) ) ) ( Option String )( ite (= x !0 ( mk - pair " i " "% default ") )( some " bool ")( some " unit ") ) )
)




図 17

極小化された empty map.tz のモデル


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

 仕様が満たされないので，ケース 2 に該当する．そ{ parameter address ;storage unit ;<< ContractAnnot{ ( addr , _ ) | True } - >{ ( ops , _ ) |match ops with[ Transfer < int > _ _ ( Contract addr ’) ] - >addr ’ = addr
| _ - > False } &{ err | err = Error Unit } >>code { CAR ; CONTRACT unit ;IF_NONE{ FAIL }{PUSH mutez 1; UNIT ;TRAN SFE R_TOK ENS ;NIL operation ;SWAP ; CONS ;UNIT ; SWAP ; PAIR ;
}
}
}



図 18

transfer.tzのため，残っている要素数が多く，検証失敗の原因の説明としての粒度は粗いものになっているが，検証失敗の原因に関連性のない情報は取り除かれ，関連性のある情報のみが残っており，Ab-Postcondition に対するモデルにおいてもアルゴリズムを適用できることが確認できる．

5 関連研究プログラムの形式検証が失敗した際に，その原因をプログラムスライスの形でユーザーに提示するための手法がいくつか提案されている．本論文における手

法では，Michelson が静的型のついたスタックマシン
言語であり，プログラムスライスが有用な情報となりにくい．これは，スタックマシン言語においてある命令を削除すると，その命令以降のスタックが変化する

検証条件 Ax ∧ Constr ∧ ¬Spe の検証結果は sat となため，プログラムとしてほぼ意味をなさなくなることる．
（この検証条件における Constr は Postcondition

が多いことによる．そのため，本論文においてはモデの場合と異なり，プログラムの実行時に例外が発生す

ルを失敗原因として提示する手法を提案した．

る条件となる制約である．
）

Haack らは，プログラムの型エラーの原因を提示

図 25 に示したモデル M は，この Ab-Postcondition

するための手法として，エラーの発生箇所を特定し，に対する検証結果から得られるもので，検証条件

それが含まれるプログラムのスライスを取得する手法

Ax ∧ Constr ∧ ¬Spe と M を入力としてモデル極小を提案した [3]．この手法では，Hindley-Milner 型推化アルゴリズムを適用すると，図 22 に示すようなモ論を拡張することでスライスの取得を行っている．具′デル M が得られる．Ab-Postcondition に記述され体的には，型推論の過程で生成される制約にプログラ

た仕様は {

ム中の場所を表す情報を関連付け，単一化の過程でそ| false} で，例外が発生すれば必ず

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

16


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35



...
( assert( and(= ( unpack_opt ! unit ( pack ! unit unit_l14_c26 -30 _0017 ) )(( as some ( Option Unit ) ) unit_l14_c26 -30 _0017 ) )( or (= 0 push_l14_c12 -24 _0016 ) ( > push_l14_c12 -24 _0016 0) )( or (= push_l14_c12 -24 _0016 9 2 2 3 3 7 2 0 3 6 8 5 4 7 7 5 8 0 7 )( > 9 2 2 3 3 7 2 0 3 6 8 5 4 7 7 58 0 7 push_l14_c12 -24 _0016 ) )...
(= contract_l10_c14 -27 _0012( ite(= ( co ntrac t_t y_opt car_l10_c9 -12 _0011 )(( as some ( Option String ) ) " unit ") )(( as some ( Option Contract ) )(( as contract Contract ) car_l10_c9 -12 _0011 ) )( as none ( Option Contract ) ) ) )(= car_l10_c9 -12 _0011 ( first param_stor_0010 ) ) (= param_stor_0010 v0004 )(=( contra ct_ ty_op t(( as mk - pair ( Pair String String ) ) ( first self_addr ) "% default ") )(( as some ( Option String ) ) " address ") )
( not
( ite
( and ( < 0 ( seq . len ( first v0025 ) ) )( is - transferToke ns ( seq . nth ( first v0025 ) 0) )( is - some ( unpack_opt ! int ( transferData ( seq . nth ( first v0025 ) 0) ) ) )(= 0( seq . len( seq . extract ( first v0025 ) 1 ( - ( seq . len ( first v0025 ) ) 1) ) ) ) )(= ( ex tract Con tract ( transferContract ( seq . nth ( first v0025 ) 0) ) )( first v0004 ) ) false ) ) ) )( echo" Finding counter - example for postcondition of ContractAnnot at line 0 , characters -1 - -1")
( check - sat )
...



図 19

transfer.tz の検証時に生成される，Postcondition に対する検証条件


1
2
3
4



(
( define - fun unpack_opt ! int (( x !0 String ) ) (Option Int )( as none ( Option Int ) ) )
)



1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16



極小化された transfer.tz のモデルの情報を追跡し，単一化が失敗した際にプログラム中の関連する場所を取り出せるようにしてある．また，得られた制約のうち充足不能な極小の集合を求める
ことで，スライスのサイズを抑える工夫をしている．
本論文における極小化アルゴリズムは Haack らの{parameter unit ;storage unit ;<< ContractAnnot { _ | True } - >{ ( ops , _ ) |match ops with[ Transfer < unit > Unit tz ( Contract addr ) ]- > addr = source && tz = amount| _ - > False } &{ _ | False } >>code { CDR ; NIL operation ; SENDER ;CONTRACT unit ; ASSERT_SOME ;AMOUNT ; UNIT ; TRANSFER_TOKENS ;CONS ; PAIR ;
}


図 20



}




図 21

boomerang ab neg.tz

研究に着想を得ている．一方で，Haack らの手法においては制約の具体的な構造はほとんど用いないのに対いる必要がある．また，上述した理由により，本論文

し，本論文のアルゴリズムにおいては，Algorithm 2ではプログラムスライスではなくモデルを失敗原因が検証条件の充足可能性に応じてモデル極小化の手として提示している．

法を切り替えるように，検証条件の具体的な性質を用

Ueno らは，型システムに基づいた命令形プログラ日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

17


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26



(
( define - fun self_addr () ( Pair String String )( mk - pair " i " "% default ") )( define - fun v0028 () Exception( error " t ") )( define - fun nil_l11_c16 -29 _0012 () ( Seq Operation )( as seq . empty ( Seq Operation ) ) )( define - fun contract_l12_c10 -23 _0014 () ( Option Contract )( as none ( Option Contract ) ) )( define - fun sender () ( Pair String String )( mk - pair " n " "% default ") )( define - fun sender_l11_c32 -38 _0013 () ( Pair String String )( mk - pair " n " "% default ") )( define - fun unpack_opt ! unit (( x !0 String ) ) ( Option Unit )( some unit ) )( define - fun c ont ract_ ty_ opt (( x !0 ( Pair String String ) ) ) ( Option String )( ite (= x !0 ( mk - pair " u " "% default ") )( some " unit ")( ite (= x !0 ( mk - pair " n " "% default ") )( as none ( Option String ) )( ite (= x !0 ( mk - pair " i " "% default ") )( some " unit ")( some " unit ") ) ) ) )( define - fun pack ! unit (( x !0 Unit ) ) String" t ")
)




図 22

モデル極小化アルゴリズムによって極小化された boomerang ab neg.tz のモデル

ム検証ツールである ConSORT [6] について，検証失検証条件の検証結果に対して，Z3 のモデル出力機能

敗時に有益なエラーメッセージを生成するための手法

によって，仕様を満たさないような変数束縛であるを提案した [7]．ConSORT による検証は，所有権制モデルを得ることができる．有用な説明を得るため

約による推論と，CHC (Constrained Horn Clauses)に，得られたモデルのうち検証失敗の原因に関連性により表現された制約の生成・解消という 2 つの段階のない情報を取り除き，関連性のある情報のみを含に分けられ，それぞれにおいて異なる理由で検証に失んだモデルを得るためのモデル極小化アルゴリズム

敗する可能性がある．そこで，前者において失敗したを提案した．提案したモデル極小化アルゴリズムを，際は，所有権制約に違反する最小のプログラムスライ

Helmholtz の検証が失敗するようないくつかのプロスを生成し，後者において失敗した際は，それまでのグラムに対して適用し，入力としたモデルを適切に極プログラムの実行シーケンスであるエラートレース

小化し，検証失敗に関連性のある情報のみを含んだモを生成する．これによって，それぞれの段階において

デルが得られることを確かめた．

検証に失敗した際に，ユーザーがエラーの原因を理解

本研究の今後の課題として以下の点が挙げられる．

するための有益な情報を生成することを可能として• 3. 2 節で述べたケース 2 に該当するプログラム

いる．本論文の手法では，プログラムスライスではなのモデルに対してアルゴリズムを適用した際に，く極小化されたモデルを出力している．

出力されるモデルの要素数を減らし，検証失敗の原因としてより妥当なものになるようにアルゴ

6 まとめと今後の課題

リズムを改良する．

本研究では，Tezos のスマートコントラクト記述言• モデル極小化アルゴリズムによって極小化され語である Michelson の形式検証器 Helmholtz を用いたモデルをエラーの原因の説明としてユーザーた検証が失敗した際に，その原因を提示する手法をに提示する際に，よりユーザーが理解しやすいよ提案した．提案手法によって，検証の失敗時に，注釈

うに見せ方を工夫する．例えば，スタックの状態に記述された仕様のうち満たされないものに対するを 1 命令毎に視覚化し，モデルに含まれている日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集18

変数がプログラム実行時のどのタイミングで出現しているのかよりわかりやすくする．
謝辞 本研究はテゾス財団の助成金を受けて行われた．

参 考 文 献[1] Allombert, V., Bourgoin, M., and Tesson, J.: Introduction to the Tezos Blockchain, 17th International Conference on High Performance Computing& Simulation, HPCS 2019, Dublin, Ireland, July
15-19, 2019, IEEE, 2019, pp. 1–10.
[2] de Moura, L. M. and Bjørner, N.: Z3: An Efﬁcient SMT Solver, Tools and Algorithms for theConstruction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Partof the Joint European Conferences on Theory andPractice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Ramakrishnan, C. R. and Rehof, J.(eds.), Lecture
Notes in Computer Science, Vol. 4963, Springer,
2008, pp. 337–340.
[3] Haack, C. and Wells, J. B.: Type error slicing in
implicitly typed higher-order languages, Sci. Comput. Program., Vol. 50, No. 1-3(2004), pp. 189–224.
[4] Nishida, Y., Saito, H., Chen, R., Kawata, A., Furuse, J., Suenaga, K., and Igarashi, A.: Helmholtz:
A Veriﬁer for Tezos Smart Contracts Based on Reﬁnement Types, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Partof the European Joint Conferences on Theory andPractice of Software, ETAPS 2021, Luxembourg
City, Luxembourg, March 27 - April 1, 2021,
Proceedings, Part II, Groote, J. F. and Larsen,
K. G.(eds.), Lecture Notes in Computer Science,Vol. 12652, Springer, 2021, pp. 262–280.
[5] TezosDeveloper: Michelson: the language ofSmart Contracts in Tezos, https://tezos.gitlab.
io/alpha/michelson.html. (Accessed on July 6th,2022).
[6] Toman, J., Siqi, R., Suenaga, K., Igarashi, A.,
and Kobayashi, N.: ConSORT: Context- and FlowSensitive Ownership Reﬁnement Types for Imperative Programs, Programming Languages and Systems - 29th European Symposium on Programming,
ESOP 2020, Held as Part of the European Joint
Conferences on Theory and Practice of Software,
ETAPS 2020, Dublin, Ireland, April 25-30, 2020,
Proceedings, Müller, P.(ed.), Lecture Notes in Computer Science, Vol. 12075, Springer, 2020, pp. 684–
714.
[7] Ueno, H., Toman, J., Kobayashi, N., andTsukada, T.: Counterexample generation for program veriﬁcation based on ownership reﬁnement
types, Proceedings of the 2021 ACM SIGPLAN
Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2021, Virtual Event,
Denmark, January 18-19, 2021, Lindley, S. andMogensen, T. Æ.(eds.), ACM, 2021, pp. 44–57.

A 極小化アルゴリズムを適用する前のモデル

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

19



(
( define - fun p ara m_sto r_0 010 () ( Pair Bool ( Array String ( Option Int ) ) )( mk - pair false (( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) ) )( define - fun empty_map_l9_c9 -29 _0011 () ( Array String ( Option Int ) )(( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) )( define - fun nil_l10_c9 -22 _0012 () ( Seq Operation )( as seq . empty ( Seq Operation ) ) )( define - fun source () ( Pair String String )( mk - pair " u " "% default ") )( define - fun v0004 () ( Pair Bool ( Array String ( Option Int ) ) )( mk - pair false (( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) ) )( define - fun sender () ( Pair String String )( mk - pair " n " "% default ") )( define - fun self_addr () ( Pair String String )( mk - pair " i " "% default ") )( define - fun amount () Int0)( define - fun balance () Int1)( define - fun v0015 () ( Pair ( Seq Operation ) ( Array String ( Option Int ) ) )( mk - pair ( as seq . empty ( Seq Operation ) )(( as const ( Array String ( Option Int ) ) ) ( as none ( Option Int ) ) ) ) )( define - fun c ont ract_ ty_ opt (( x !0 ( Pair String String ) ) ) ( Option String )( ite (= x !0 ( mk - pair " i " "% default ") )( some " bool ")( some " unit ") ) )
)




図 23

empty map.tz の Postcondition に対するモデル

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

20


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53



(
( define - fun nil_l16_c12 -25 _0019 () ( Seq Operation )( as seq . empty ( Seq Operation ) ) )( define - fun push_l14_c12 -24 _0016 () Int1)( define - fun v0004 () ( Pair ( Pair String String ) Unit )( mk - pair ( mk - pair " t " " it ") unit ) )( define - fun v0025 () ( Pair ( Seq Operation ) Unit )( let (( a !1 ( seq . unit ( transferTokens " nit " 1 ( contract ( mk - pair " t " " it ") ) ) ) ) )( mk - pair a !1 unit ) ) )( define - fun self_addr () ( Pair String String )( mk - pair " i " "% default ") )( define - fun transfer_tokens_l15_c12 -27 _0018 () Operation( transferTo kens " nit " 1 ( contract ( mk - pair " t " " it ") ) ) )( define - fun car_l10_c9 -12 _0011 () ( Pair String String )( mk - pair " t " " it ") )( define - fun contract_l10_c14 -27 _0012 () ( Option Contract )( some ( contract ( mk - pair " t " " it ") ) ) )( define - fun if_none_l11_c9 -12 _0013 () Contract( contract ( mk - pair " t " " it ") ) )( define - fun p ara m_sto r_0 010 () ( Pair ( Pair String String ) Unit )( mk - pair ( mk - pair " t " " it ") unit ) )( define - fun source () ( Pair String String )( mk - pair " u " "% default ") )( define - fun cons_l17_c18 -22 _0020 () ( Seq Operation )( seq . unit ( trans ferTokens " nit " 1 ( contract ( mk - pair " t " " it ") ) ) ) )( define - fun sender () ( Pair String String )( mk - pair " n " "% default ") )( define - fun amount () Int0)( define - fun balance () Int1)( define - fun unit_l18_c12 -16 _0021 () Unit
unit )( define - fun unit_l14_c26 -30 _0017 () Unit
unit )( define - fun unpack_opt ! unit (( x !0 String ) ) ( Option Unit )( some unit ) )( define - fun seq . nth_u (( x !0 ( Seq Operation ) ) ( x !1 Int ) ) Operation( setDelegate ( as none ( Option String ) ) ) )( define - fun unpack_opt ! int (( x !0 String ) ) ( Option Int )( as none ( Option Int ) ) )( define - fun c ont ract_ ty_ opt (( x !0 ( Pair String String ) ) ) ( Option String )( ite (= x !0 ( mk - pair " u " "% default ") )( some " unit ")( ite (= x !0 ( mk - pair " t " " it ") )( some " unit ")( ite (= x !0 ( mk - pair " i " "% default ") )( some " address ")( some " unit ") ) ) ) )( define - fun pack ! unit (( x !0 Unit ) ) String" nit ")
)




図 24

transfer.tz の Postcondition に対するモデル

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

21



(
( define - fun v0004 () ( Pair Unit Unit )( mk - pair unit unit ) )( define - fun unit_l12_c26 -37 _0016 () Unit
unit )( define - fun self_addr () ( Pair String String )( mk - pair " i " "% default ") )( define - fun v0028 () Exception( error " t ") )( define - fun contract_l12_c10 -23 _0014 () ( Option Contract )( as none ( Option Contract ) ) )( define - fun cdr_l11_c10 -13 _0011 () Unit
unit )( define - fun nil_l11_c16 -29 _0012 () ( Seq Operation )( as seq . empty ( Seq Operation ) ) )( define - fun p ara m_sto r_0 010 () ( Pair Unit Unit )( mk - pair unit unit ) )( define - fun source () ( Pair String String )( mk - pair " u " "% default ") )( define - fun sender () ( Pair String String )( mk - pair " n " "% default ") )( define - fun amount () Int0)( define - fun balance () Int1)( define - fun sender_l11_c32 -38 _0013 () ( Pair String String )( mk - pair " n " "% default ") )( define - fun unpack_opt ! unit (( x !0 String ) ) ( Option Unit )( some unit ) )( define - fun c ont ract_ ty_ opt (( x !0 ( Pair String String ) ) ) ( Option String )( ite (= x !0 ( mk - pair " u " "% default ") )( some " unit ")( ite (= x !0 ( mk - pair " n " "% default ") )( as none ( Option String ) )( ite (= x !0 ( mk - pair " i " "% default ") )( some " unit ")( some " unit ") ) ) ) )( define - fun pack ! unit (( x !0 Unit ) ) String" t ")
)




図 25

boomerang ab neg.tz の Ab-Postcondition に対するモデル