Scillaの形式的検証
概要
ScillaからCoqにトランスパイルし、Coqにより形式的検証を行う
現状はマニュアルだが、いずれ自動でやれるようになる
CoqでZilliqaコントラクトの形式的なセマンティックがある
コントラクトによる状態遷移
環境である各種データ構造
※まだ未完成
セマンティックを用い、関数の性質を証明する
コントラクトの、メッセージ通信なしの部分のみをGallinaでモデル化
メッセージをやりとりして状態遷移するセマンティックはcoqのrelationを使ってエンコード
(これは、LipsやScala上で実行するDSLを実装するのと同じ方法: "shallow encoding")
yamarkz.icon < Coq is 定理証明機 Coq Zilliqaコントラクトのセマンティック
paperとGitHubの最新のコードとは少し書き方や命名が異なる
厳密にはScillaから変換されたGallinaでのコントラクトのセマンティック
「Scillaのセマンティック」ではない
VM, インタプリタレベルではない
trace-based semantic
ステートに関するデータ型
code: State(Ocaml)
Section State.
Definition value := nat.
Definition address := nat.
Definition tag := nat.
Definition payload := (seq (nat * seq nat)).
(* Message with a payload *)
(* MessageはZilliqaのコントラクト間のやりとり *)
Record message := Msg {
val : value;
sender : address;
to : address;
method : tag;
body : payload
}.
(* Augmented state of a contract *)
Record cstate (T : Type) := CState {
my_id : address;
balance : value;
state : T
}.
(* Global blockchain state *)
Record bstate := BState {
block_num : nat;
(* Anything else? *)
(* ↑まだここは詳細が実装されていない *)
}.
End State.
プロトコルレベルのデータ型
transtion はZilliqaにおいてcontract-specificな変化
Contractはオートマトンとしてモデル化されているので状態遷移(transition)
code: Protocol(Ocaml)
Section Protocol.
Section Transitions.
(* State type *)
Variable S: Type.
(* A response from a transition *)
Definition resp_type := (address * value * tag * payload)%type.
Definition msg_bal (rt : resp_type) : value := rt.1.1.2.
(* Transitions are functions *)
Definition trans_fun_type :=
address -> value -> S -> message -> bstate -> (S * option message).
(* Contract transition in the spirit of I/O automata *)
Record ctransition :=
CTrans {
(* Unique tag of a transition in the protocol *)
ttag : tag;
(* Funcion (bstate, state, msg) :-> (state', option msg') *)
tfun : trans_fun_type;
}.
Definition idle_fun : trans_fun_type := fun _ _ s _ _ => (s, None).
Definition idle := CTrans 0 idle_fun.
End Transitions.
Record Protocol (S : Type) :=
CProt {
(*Account id *)
acc : address;
(* Initial balance *)
init_bal : nat;
(* Initial state of a protocol *)
init_state : S;
(* Protocol comes with a set of transitions *)
transitions : seq (ctransition S);
(* All transitions have unique tags *)
_ : uniq (map (@ttag _) transitions)
}.
Definition tags {S : Type} (p : Protocol S) :=
map (@ttag _) (transitions p).
End Protocol.
コントラクトのセマンティック定義
code: Semantic 一部略(Ocaml)
Variables (S : Type) (p : Protocol S).
(* Blockchain schedules *)
(* コントラクトとその環境(他のコントラクト、ブロックチェーンのステート)同士の任意のやりとりを表せる *)
Definition schedule := seq (bstate * message).
Record step :=
Step {
pre : cstate S;
post : cstate S;
out : option message
}.
Definition trace := seq step.
Definition apply_prot id bal s m bc : (S * option message) :=
let n := seq.find (fun t => ttag t == method m) (transitions p) in
let tr := nth (idle S) (transitions p) n in
let f := tfun tr in
f id bal s m bc.
Definition step_prot pre bc m : step :=
let: CState id bal s := pre in
let: (s', out) := apply_prot id bal s m bc in
let: bal' := if out is Some m' then (bal + val m) - val m' else bal in
let: post := CState id bal' s' in
Step pre post out.
(* Map a schedule into a trace *)
Fixpoint execute (pre : cstate S) (sc: schedule) : trace :=
if sc is (bc, m) :: sc'
then let stp := step_prot pre bc m in
stp :: execute (post stp) sc'
Definition state0 := CState (acc p) (init_bal p) (init_state p).
(* Execute from the initial contract state, if schedule is empty, repeat the initial state *)
Definition execute0 sc :=
if sc is _ :: _
then execute state0 sc
プロパティ
Safety proparty
述語Iは、cstateを受け取り命題を返す関数型、IのSafetyを示す
「initial stateから実行したtraceに含まれるような任意のschedule, pre, post, outに関して、preとpostの両方がIを満たす」
code: Sementic(Ocaml)
Definition safe (I : cstate S → Prop) : Prop :=
(* For any schedule sc, pre/post states and out... *)
forall sc pre post out,
(* such that the triple Step (pre, post, out) is in the trace obtained via sc *)
Step pre post out \in execute0 sc →
(* both pre and post satisfy I *)
I pre ∧ I post.
※ \in→∈
具体例
「あるコントラクトの残高が常に正」「残高はconrtibutorの合計」「常にコントラクトにロックされない」
実用的には、以下の(帰納的な)補題を利用する
「Iが、(a)初期状態で成立し、かつ、(b)任意の事前状態preで成立し、かつ、任意のブロックチェーンの状態bcで任意のメッセージmにより遷移した事後状態で成立する」時、Iのsafetyが示される 証明 GitHub code: Semantic(Ocaml)
Lemma safe_ind (I : cstate S → Prop) :
(* (a) *)
I state0 →
(* (b) *)
(∀ pre bc m, (method m ∈ tags p) → I pre → I (post (step_prot pre bc m))) →
(* (conclusion) *)
safe I.
Coqで導入できる他の証明規則であっても良い
Temporal properties
時相論理の推論規則や演算は、高階論理演算子を定義することでcoqにエンコードできる
paperでは、まだどんなconnectiveのセットを導入するか決めている段階と書いてあった
since_as_long
「コントラクトが
code: Semantic(Ocaml)
Definition reachable (st st' : cstate S) sc :=
st' = post (last (Step st st None) (execute st sc)).
(* q holds since p, as long as schedule bits satisfy r. *)
Definition since_as_long (p : cstate S → Prop)
(q : cstate S → cstate S → Prop)
(r : bstate * message → Prop) :=
∀ sc st st',
(* (i) st satisfies p *)
p st →
(* (ii) st' is reachable from st via sc *)
reachable st st' sc →
(* (iii) any element b of sc satisfies r *)
(∀ b, b ∈ sc → r b) →
(* (conclusion) q holds over st and st' *)
q st st'.
具体例: クラウドファンディング
プロパティ
「クラウドセールが成功しない限り、コントラクトは出資を全て保持している」
code: Crowdfunding(Ocaml)
Definition balance_backed (st: cstate crowdState) : Prop :=
(* If the campaign not funded... *)
~~ (funded (state st)) ->
(* the contract has enough funds to reimburse everyone. *)
sumn (map snd (backers (state st))) <= balance st.
Lemma sufficient_funds_safe : safe crowd_prot balance_backed.
~~ → ¬
fundedはbool型のステート変数
「claimがない全ての」
code: Crowdfunding(Ocaml)
(* Contribution of backer b is d is recorded in the backers *)
Definition donated b (d : value) st :=
(* b doesn't claim its funding back *)
Definition no_claims_from b (q : bstate * message) := sender q.2 != b.
Lemma donation_preserved (b : address) (d : value):
since_as_long crowd_prot (donated b d)
(fun _ s' => donated b d s') (no_claims_from b).
「資金が十分集まらなかった場合、寄付した人は資金を引き出せる」
https://gyazo.com/5476061bca272fa7c011aedd6b9c177d