#はじめに
証券システムにおける株式の売買成立を決定するアルゴリズムの1つに「板寄せアルゴリズム」があります。
本記事ではこのアルゴリズムが正しい仕様を満たしているかどうかを形式検証ツールの１つであるCoq/SSReflectを用いて形式検証していきます。
※私はフィンテックが独学であるため、専門用語の言い回しなどが稚拙な箇所があるかもしれません。あらかじめご了承ください。
この記事は「ある証券会社の証券用語の解説に仕様バグが存在することを形式検証によって発見した話」の続きです。
ソースコードはこちらです。
#問題設定
まず本記事で仮定する株式の売買と板寄せアルゴリズムの仕様について定義します。
まず、板寄せアルゴリズムの入出力を定義するために「注文」と「約定」を定義します。
##注文
注文とは、注文数×注文種別×**{売り,買い}×注文者情報**である。
注文数は自然数であり、注文種別は成行または指値であり、指値の場合は、全順序集合Priceの要素である価格を設定する。
実際の取引には他にも逆指値などがありますが、本記事ではシンプルに成行と指値のみを考えます。
##約定
-
[狭義] 約定とは注文のペアであり、任意の約定(注文1、注文2)に対し、注文1が売り注文かつ注文2が買い注文であり、それぞれの注文数と価格が等しいことである。
-
[広義] 約定とは注文のペアであり、任意の約定(注文1、注文2)に対し、注文1が売り注文かつ注文2が買い注文であり、それぞれの注文数が等しく、注文1の価格は注文2の価格に等しいかそれ以下であることである。
約定するということは、取引が成立するということです。
つまり、片方が売り注文、もう片方が買い注文であり、それぞれの注文数が等しく、[狭義]では2つの注文価格が一致すること、[広義]では売り注文の価格が買い注文の価格以下、すなわち証券所が損しないようになっていなければなりません。(ただし、基本的には成行注文の場合にも必ず価格がつくが、元々の注文が成行注文のみの場合、価格をつけようがないため、両者価格なしがありうることに注意)
基本的には[狭義]の定義を使いますが、のちに[広義]を使う例も紹介します。
##板寄せアルゴリズムの入出力
板寄せアルゴリズムの入出力は上で定義した注文と約定で定義されます。
入力：注文の列と任意で約定価格の初期値
出力：約定の列と約定価格、及び未約定注文の列
ここで任意入力としての約定価格の初期値を取っているのは、指値注文が存在しない場合の約定価格を設定するのに必要だからです。
基本的には、前営業日の終値を入れれば問題ないと思いますが、新規公開株など、前営業日の終値が存在しないものでも対応できるようになっています。
(実際の実装はどうなっているのか分からないので、間違っている可能性があります。fintechに詳しい方、教えていただけると幸いです。)
ただし、この入出力は以下で述べる仕様を満たさなければいけません。
#板寄せアルゴリズムの仕様
詳細は前回の記事をご覧ください。
これらの条件を全て満たすようなアルゴリズムを考えます。
#板寄せアルゴリズムの型
板寄せアルゴリズムを形式検証ツールの1つであるCoq/SSReflectで実装します。
##準備
板寄せアルゴリズムの型を定義するための準備をします。
Variable priceType : eqType.
Variable pricerel : rel priceType.
Variable otherdataType : eqType.
Variable timerel : rel otherdataType.
Definition orderType : Type
:= nat * option priceType * otherdataType.
Variable tobool : pred otherdataType.
Notation is_bid := (fun x : orderType => tobool x.2).
Notation share_of := (fun x : orderType => x.1.1).
Notation price_of := (fun x : orderType => x.1.2).
Notation otherdata_of := (fun x : orderType => x.2).
Notation orderbookType := (seq orderType * seq orderType:Type).
価格の型をpriceType : eqType、価格における全順序関係をpricerel : rel priceTypeとし、注文者情報の型をotherdataType : eqTypeとします。
また、(買い/売り)の情報は注文者情報の中に入れておき、それを取り出す関数toBool : pred otherdataTypeを定義します。
ここでは、toBool x = trueのときに売り注文、toBool x = falseのときに買い注文を表すことにします。
なぜ、(売り/買い)の情報をの値を独立にせずに注文者情報の型に含めたかというと、どちらも約定前の注文と約定後の注文とで値が変化しないためです。
例えば、100株の買い注文をしたとしてもその全てが約定するとは限らず、50株だけで約定するかもしれないので、注文数が変化する可能性があり、成行注文が約定すると価格もつくので価格も変化します。しかしながら、(売り/買い)を変えてはいけないので、それならば注文者情報otherdataTypeにまとめてしまってよいと考えられるからです。
さらに、注文の型orderType := nat * option priceType * otherdataTypeとし、
第一引数が注文数、第二引数が注文種別、第三引数が**(売り/買い)と注文者情報**を表しています。
特に、注文種別はoption priceType型であり、成行をNone、価格xの指値をSome xで表します。
また、「時間優先の原理」を保つための関係timerel : rel otherdataTypeを定義しています。これは証明において特に使用しませんが、実装の上では注文時間でもソートされていることも想定しています。
これらを用いて、板寄せアルゴリズムopentradeの型を以下に定義します。
Check opentrade.
(*
opentrade
: option priceType ->
seq orderType * seq orderType ->
option priceType * seq (orderType * orderType) * (seq orderType * seq orderType)
*)
第一引数が約定価格の初期値、第二引数が売り注文の列と売り注文の列を表しています。
返り値の１つ目が約定価格、２つ目が約定した注文、３つ目が未約定注文を表しています。
約定価格の初期値および約定価格は注文種別と同じoption priceTypeで表し、価格がつかないことを成行と同一視します。このように定義するとのちの計算が簡単になります。
これに対して、板寄せアルゴリズムの仕様を定義していきます。
#板寄せアルゴリズムの仕様の記述
上で定義した仕様をCoqで記述するのですが、その前にあるoption型に関する二項関係を定義します。
##準備
以下の関数を定義します。
Definition orel T (R:rel T) : rel (option T) :=
fun x y => match x, y with
| None, _ => true
| Some _, None => false
| Some a, Some b => R a b
end.
これは、型TとT上の二項関係Rに対し、新たに最小元Noneを追加した二項関係orel R : rel (option T)を表しています。
これを何に使うかというと、成行と指値を同じ関数で比較するのに使います。
実は成行はただの指値全体の集合に追加した最小元そのものだと考えることができます。具体的には、成行売り注文は無限小での指値、成行買い注文は無限大の指値だと考えると、板寄せアルゴリズムの処理する順番に一致します。（ただし、約定する価格に関しては別に考える必要があります）
また、本当に成行と指値を区別しなくてもいいのかどうかは、全体のアルゴリズムが仕様を満たすことを示すことによって間接的に示せます。言い換えれば、「仕様を満たす関数」であればその実装は問わないという考え方です。
今回定義する板寄せアルゴリズムは全ての仕様を満たすので、本記事の記事の実装では成行と指値を同一視します。
具体的に、成行と指値を同時に比較するような二項関係は以下のように定義します。
Definition opricerel (mode:bool) : rel (option priceType) :=
(orel (fun x y => if mode then pricerel x y else pricerel y x)).
注文種別上の順序opricerelは成行注文が最小元になるような価格における順序を表していていて、引数modeが売り注文であるかどうかを表す引数です。
具体的には、価格が実数の場合、成行注文は売り注文の場合は無限小の価格、買い注文の場合は無限大の価格を提示しているのと同じ扱いになります。(約定後の価格はもちろん無限小や無限大にならないようにしなければいけません。)
これを用いて、以下に板寄せアルゴリズムの仕様をCoq/SSReflectで実装していきます。
##仕様の記述
まず、そもそも板寄せアルゴリズムの返り値が約定の条件を満たしていることを保証するための命題を示します。
###返り値が約定であること
- 約定とは注文のペアであり、任意の約定(注文1、注文2)に対し、それぞれの注文数と価格が等しく、注文1が売り注文かつ注文2が買い注文である。
Variable (ple : rel priceType).
Hypothesis (ple_refl : reflexive ple).
(* ple x y := x == y or, opricerel x y *)
Definition ople : rel (option priceType) :=
fun x y => match x, y with
| None, None => true
| Some a, Some b => ple a b
| _, _ => false
end.
Definition contract_valid (contracts:seq (orderType * orderType)) :=
all (fun contract =>
[&& is_bid contract.1, ~~ is_bid contract.2,
share_of contract.1 == share_of contract.2 &
ople (price_of contract.1) (price_of contract.2)]) contracts.
contract_valid contractsが注文のペアの列contractsが全て約定であることを表した命題で、注文のペアcontractに対し、注文1がcontract.1、注文2がcontract.2を表します。
is_bid contract.1と~~ is_bid contract.2でそれぞれがちゃんと売り注文と買い注文であることを表し、その注文数share_ofが等しく、ople x y := x == yのとき、価格が等しいことを表しています。
ここで変数opleが==のとき、[狭義]の定義になり、opleがopricerelのとき、[広義]になります。
また、どちらも反射律を満たすためreflexive pleが仮定されています。
###条件1
- [条件1] **未約定(売り/買い)注文が存在するならば、**未約定(買い/売り)注文は全て指値である。
Definition traderesult_valid1
(result:
option priceType * seq (orderType * orderType) * orderbookType)
:=
let book := result.2 in
(book.2 <> [::] -> all (isSome \o price_of) book.1) /\
(book.1 <> [::] -> all (isSome \o price_of) book.2).
traderesult_valid1 resultが条件1を表した命題で、resultが板寄せアルゴリズムの返り値のとき、book := result.2が未約定注文を表しています。
このとき、book.1が未約定の売り注文であり、book.2が未約定の買い注文を表します。
また、isSome \o price_of : pred orderTypeが注文が指値注文であることを表す述語になっていて、例えば、(book.2 <> [::] -> all (isSome \o price_of) book.1)は
未約定売り注文が存在するならば未約定買い注文は全て指値であることを表しています。
###条件2
- [条件2] 約定値段が存在するならば、全ての指値の未約定(売り/買い)注文の価格は約定値段より(高い/低い)。
Definition traderesult_valid2
(result:
option priceType * seq (orderType * orderType) * orderbookType)
:=
let price := result.1.1 in
let book := result.2 in
all (fun x => price_of x ==> opricerel true price (price_of x)) book.1 &&
all (fun x => price_of x ==> opricerel false price (price_of x)) book.2.
traderesult_valid2 resultが条件2を表した命題で、resultが板寄せアルゴリズムの返り値のとき、price := result.1.1が約定価格、book := result.2が未約定注文を表しています。
fun x => price_of x ==> opricerel b price (price_of x)とありますが、
price_of xはisSome (price_of x)の省略であり、xが指値であることを仮定しています。
このときb = trueのとき、orel pricerel price (price_of x)つまりxの価格が約定価格より高いこと、b = falseのときはxの価格が約定価格より安いことを意味しています。
###条件3
- [条件3] **約定値段が存在するならば、**未約定の売り注文か買い注文のうちどちらか全ての指値価格は約定価格と異なる。
Definition traderesult_valid3
(result:
option priceType * seq (orderType * orderType) * orderbookType)
:=
let price := result.1.1 in
let book := result.2 in
price ->
all (fun x => price_of x != price) book.2 \/
all (fun x => price_of x != price) book.1.
traderesult_valid3 resultが条件3を表した命題で、条件2と同様に、resultが板寄せアルゴリズムの返り値のとき、price := result.1.1が約定価格、book := result.2が未約定注文を表しています。
このとき、未約定の売り注文book.1か買い注文book.2のどちらか全ての価格が約定価格priceと異なることを表しています。
###約定価格の存在性
- [約定価格の存在性] 約定価格が存在することは以下のどちらかが成り立つことと同値である。
- 約定価格の初期値が設定されていること。
- 指値注文が存在すること。
Lemma deals_price_isSomeP
(price:option priceType) (book:orderbookType) :
reflect
[\/ isSome price,
has (isSome \o price_of) book.1 |
has (isSome \o price_of) book.2]
(isSome (opentrade price book).1.1).
deals_price_isSomeP price bookが板寄せアルゴリズムの入力である、価格の初期値priceで注文がbookであったときの約定価格の存在性を示した補題で、reflectを用いて同値性を表しています。
具体的には、約定価格(opentrade price book).1.1が存在するisSomeことと
約定価格の初期値priceが存在するか、売り注文book.1か買い注文book.2の中に指値注文が存在するhas (isSome \o price_of)ことの同値性を表しています。
###約定の健全性
- [約定の健全性1] 任意の注文者情報に対し、その注文者情報を持つ(売り/買い)注文の注文数の合計と、その注文者情報を持つ約定した(売り/買い)注文及び未約定の(売り/買い)注文の注文数の合計が一致する。
Definition contract_valid1_def (usr:otherdataType) (mode:bool)
(book contracts rbook:seq orderType) :=
let order := head (0,None,usr) [seq x <- book | otherdata_of x == usr] in
let rorder :=
head (0,None,usr) [seq x <- rbook | otherdata_of x == usr] in
share_of order =
share_of rorder +
\sum_(x <- contracts | otherdata_of x == usr) share_of x.
Definition contract_valid1 (book:orderbookType)
(result:option priceType * seq (orderType * orderType)
* orderbookType) :=
forall usr : otherdataType,
let mode := tobool usr in
if mode
then contract_valid2_def
usr mode book.1 [seq x.1 | x <- result.1.2] result.2.1
else contract_valid2_def
usr mode book.2 [seq x.2 | x <- result.1.2] result.2.2.
contract_valid1 book resultが健全性1を表していて、
bookが約定前注文の列、resultが板寄せアルゴリズムの返り値であるとき、
任意の注文者情報usrに対し、それが売り注文tobool usr = trueであるか買い注文tobool usr = falseであるかで場合分けします。
それぞれの場合に対して、contract_valid1_defで定義される命題で具体的な条件を表します。
contract_valid1_def usr mode book contracts rbookの引数はそれぞれ、
usrが注文者情報、modeが(売り/買い)、bookが取引前の(売り/買い)注文の列、contrancsが約定した(売り/買い)注文、rbookが未約定の(売り/買い)注文の列を表します。
このとき、orderとrorderがそれぞれ注文者情報usrを含む取引前と未約定の注文で、存在しなければ(0,None,usr)となります。
同じ注文者情報の注文が複数ある場合がありますが、後に一意性を仮定するため、ここではhead関数を使って取り出しています。
このとき、取引前の注文数share_of orderが未約定の注文数share_of rorderと約定した注文数の合計\sum_(x <- contracts | otherdata_of x == usr) share_of xの和が等しいことを表しています。
- [約定の健全性2] 任意の注文者情報に対し、その注文者情報を持つ指値(売り/買い)注文が存在し、等しい注文者情報を持つ約定した(売り/買い)注文が存在する場合、その価格は元の注文の価格より(高い/安い)。
Definition contract_valid2_def (usr:otherdataType) (mode:bool)
(book contracts rbook:seq orderType) :=
let order := head (0,None,usr) [seq x <- book | otherdata_of x == usr] in
all (opricerel mode (price_of order) \o price_of)
[seq x <- contracts | otherdata_of x == usr].
Definition contract_valid2 (book:orderbookType)
(result:option priceType * seq (orderType * orderType)
* orderbookType) :=
forall usr : otherdataType,
let mode := tobool usr in
if mode
then contract_valid2_def
usr mode book.1 [seq x.1 | x <- result.1.2] result.2.1
else contract_valid2_def
usr mode book.2 [seq x.2 | x <- result.1.2] result.2.2.
contract_valid2が健全性2を表した命題で、記述の仕方は健全性1とほぼ同じで、売り注文と買い注文の場合でそれぞれcontract_valid2_defを使って定義し、contract_valid2_defの引数もcontract_valid1_defのときと同じです。
違うのは命題の中身で、約定した列のうち、注文者情報がusrのものに対して、全てopricerel mode (price_of other) \o price_ofであることを主張していて、
これは、mode = trueつまり売り注文の場合は元の注文orderの価格より高い価格で約定したこと、mode = falseつまり買い注文の場合は元の価格より安い価格で約定したことを表しています。
つまり損をしていないことを表しているということです。
#板寄せアルゴリズムの実装
板寄せアルゴリズムを実装していきます。
基本的には、こちらの楽天証券/現物取引 取引ルール/板寄せを参考に定義するのですが、このサイトでは細かい実装が見えてこないのと、Coqでは停止性が示せるような実装にする必要があるため、多少異なるものになります。
具体的に板寄せアルゴリズムopentradeの実装を見ていきます。
##実装の考え方
参考元のアルゴリズムでは、まず
売りと買いの注文が交錯した状態からまずは始値を仮定する
とあります。
しかし、これは取引実行関数が停止する条件と一致するので取引実行関数と分ける必要がなく、「取引実行関数において、先に再帰呼び出しして停止したときの返り値を取引価格として、その価格で約定する」というアルゴリズムにすれば取引と同時に計算できます。
また、次に
売り成行注文と買い成行注文を約定させる
500円より高い買いの指値注文と500円より低い売りの指値注文を約定させる
(500円は始値)
とあります。
しかしながら、売り成行注文は最小元の指値、買い成行注文は最大元の指値という扱いにすれば、成行と指値注文を区別する必要がありません。(ただし約定する価格にだけは注意する必要がある)
また、各約定における約定価格をいくらに設定すればいいのか詳細の記載がないため、いくつか考えられるパタンを考えてみます。
例えば、始値500円のとき497円の売り注文と501円の買い注文が約定した場合、
- 売り注文の価格(497円)または買い注文の価格(501円)に統一する。
- それぞれの注文の平均価格(499円)に統一する。
- 始値(500円)に統一する。
- それぞれ注文した元の価格のまま約定する。このとき4円差額が発生するが、これを証券会社の収益にする。(※ただし約定価格が異なるため、[広義]の約定になる)
などが考えられ、どのパタンも
- [約定の健全性2] 任意の注文者情報に対し、その注文者情報を持つ指値(売り/買い)注文が存在し、等しい注文者情報を持つ約定した(売り/買い)注文が存在する場合、その価格は元の注文の価格より(高い/安い)。
を満たします。
本記事では、注文の価格x y : priceTypeが約定したときの価格priceop x yを返す関数priceop:priceType -> priceType -> priceTypeを考え、
健全性2を満たす条件を探して仮定します。
最後に
約定値段の売りまたは買い注文のいずれかがすべて約定する状態にする
を満たすように停止条件を定義すれば完成です。
##満たすべき漸化式
板寄せアルゴリズムopentradeが満たすべき漸化式は以下になります。
Lemma opentrade_equation
(price:option priceType) (book:orderbookType) :
opentrade price book =
if book.1 is xa :: sa
then
if book.2 is xb :: sb
then
if check_price xa xb
then
if share_of xa == share_of xb
then
let result :=
opentrade (deal_price price xa xb) (sa, sb) in
(result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
else
if share_of xa > share_of xb
then
let result :=
opentrade
(deal_price price xa xb)
((share_of xa - share_of xb,
price_of xa, otherdata_of xa) :: sa, sb) in
(result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
else
let result :=
opentrade
(deal_price price xb xa)
(sa,
(share_of xb - share_of xa,
price_of xb, otherdata_of xb) :: sb) in
(result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
else
(price_of xa, [::], book)
else
(head_price price book.1, [::], book)
else
(head_price price book.2, [::], book).
Proof.
by case : book =>[[|xa sa][|xb sb]].
Qed.
ただし、
Definition oop (T:Type) (op:T -> T -> T) (x y:option T) : option T :=
match x,y with
| None, _ => y
| _, None => x
| Some x', Some y' => Some (op x' y')
end.
Definition check_price : rel orderType :=
fun x y =>
match price_of x, price_of y with
| Some x', Some y' => pricerel x' y'
| _, _ => true
end.
Variable (priceop:priceType -> priceType -> priceType).
Definition deal_price
(default:option priceType) (x y:orderType) : option priceType :=
let xy := oop priceop (price_of x) (price_of y) in
if isSome xy then xy else default.
まず、約定価格の初期値price、注文がbookで、特に売り注文の列がbook.1、買い注文の列がbook.1です。
このとき、book.1とbook.2が価格に対してソートされて、(売り/買い)注文の列の先頭要素が最も価格の(安い/高い)と仮定します。
それぞれ先頭要素xaとxbを取り出し、停止条件check_price xa xbを見て、もし売り注文の価格の方が買い注文より安かったら約定させます。
具体的には、注文数が少ない方に合わせてその注文数だけ約定して再帰します。(実際には、始値を計算するために再帰してから約定します)
このように定義すれば、板寄せアルゴリズムが定義できます。
しかしながら、停止性が自明ではなく、Coqではそのまま定義できません。
そこで、Coqでは以下のように定義します。
###停止性を示すための実装
上の漸化式における再帰呼び出しでは売り注文と買い注文の列の長さのどちらか一方が必ず短くなっています。言い換えれば、辞書式順序で引数の長さが短くなっていると言えます。
そこで、「Coq/SSReflectで辞書式順序で引数が構造的に小さくなる関数をFixpointで定義する」を応用して定義します。
Fixpoint opentrade_rec
(price:option priceType) (a:seq orderType) (b:seq orderType) :
option priceType * seq (orderType * orderType) * orderbookType :=
if a is xa :: sa
then
let fix recf (price:option priceType) (xa:orderType) (b:seq orderType) :
option priceType * seq (orderType * orderType) * orderbookType :=
if b is xb :: sb
then
if check_price xa xb
then
if share_of xa == share_of xb
then
let result :=
opentrade_rec (deal_price price xa xb) sa sb in
(result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
else
if share_of xa > share_of xb
then
let result :=
recf
(deal_price price xa xb)
(share_of xa - share_of xb,
price_of xa, otherdata_of xa) sb in
(result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
else
let result :=
opentrade_rec
(deal_price price xb xa) sa
((share_of xb - share_of xa,
price_of xb, otherdata_of xb) :: sb) in
(result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
else
(price_of xa, [::], (xa :: sa, b))
else
(head_price price (xa :: sa), [::], (xa :: sa, b))
in recf price xa b
else
(head_price price b, [::], (a, b)).
Definition opentrade (price:option priceType) (book:orderbookType)
:= opentrade_rec price book.1 book.2.
また、証明に使用するための帰納原理opentrade_indと漸化式を満たすことの補題opentrade_equation(既に上に記載しています)も証明します。
Lemma opentrade_ind
(P:option priceType -> seq orderType -> seq orderType -> Prop) :
(forall price b, P price [::] b) ->
(forall price xa sa, P price (xa :: sa) [::]) ->
(forall price xa sa xb sb,
check_price xa xb -> share_of xa == share_of xb ->
P (deal_price price xa xb) sa sb -> P price (xa :: sa) (xb :: sb)) ->
(forall price xa sa xb sb,
check_price xa xb -> share_of xa == share_of xb = false ->
share_of xa > share_of xb ->
P (deal_price price xa xb)
((share_of xa - share_of xb, price_of xa, otherdata_of xa) :: sa)
sb -> P price (xa :: sa) (xb :: sb)) ->
(forall price xa sa xb sb,
check_price xa xb -> share_of xa == share_of xb = false ->
share_of xa > share_of xb = false ->
share_of xa < share_of xb ->
P (deal_price price xb xa) sa
((share_of xb - share_of xa, price_of xb, otherdata_of xb) :: sb) ->
P price (xa :: sa) (xb :: sb)) ->
(forall price xa sa xb sb,
check_price xa xb = false ->
P price (xa :: sa) (xb :: sb)) ->
forall price a b, P price a b.
4つ目と5つ目の仮定にはshare_of xa == share_of xb = falseとshare_of xa > share_of xbなどが同時に存在し、冗長に見える部分があります。
しかしながら、帰納法を適用したときにopentrade_equationを使うと、if文の分岐条件にshare_of xa == share_of xbが登場するため、場合分けしなくてもそのまま代入できるように、あえてこのように記述しています。
#板寄せアルゴリズムの入力が満たすべき仮定
上記のアルゴリズムは任意の入力に対しては仕様を満たしません。
そこで、入力が満たすべき性質を記述します。
Definition seq_order_valid (mode:bool) : pred (seq orderType) :=
fun book => [&& sorted (orderrel mode) book,
uniq [seq otherdata_of order | order <- book] &
all (fun k => is_bid k == mode) book].
Definition orderbook_valid : pred orderbookType :=
fun book => seq_order_valid true book.1 && seq_order_valid false book.2.
ただし
Definition argrel (S T:Type) (f:S -> T) (R:rel T) : rel S :=
fun x y => R (f x) (f y).
Definition lexi : (T:eqType) (S:Type) (R:rel T) (S:rel S) : rel (T * S) :=
fun x y => (x.1 == y.1) && Q x.2 y.2 || strict R x.1 y.1.
Definition orderrel (mode:bool) : rel orderType :=
argrel (fun x => (price_of x, otherdata_of x))
(lexi (opricerel mode) timerel).
これが何を表しているかというと、
入力の(売り/買い)注文の列がちゃんと(売り/買い)注文のみからなる列であり、価格に対して(昇順/降順)にソートされていてかつ、注文者情報が全て異なっているということです。
(価格に対する順序は実際には(価格,注文時刻)に対する辞書式順序lexiで定義されています。)
価格のソートは板寄せアルゴリズムを成り立たせるための仮定であり、注文者情報の一意性は約定の健全性の証明に必要です。
これを仮定して、仕様を満たすことを証明していきます。
#仕様を満たすことを証明する
基本的には上で定義した帰納原理opentrade_indを使って示します。
具体的な証明はソースにありますが、長くなるので命題だけ示します。
###返り値が約定であること
Hypothesis (priceop_ple:
forall x y, pricerel x y -> ple (priceop x y) (priceop y x)).
Lemma opentrade_contract_valid (price:option priceType) (book:orderbookType):
orderbook_valid book -> contract_valid (opentrade price book).1.2.
priceopに関する仮定としてproceop_pleが必要です。この条件は上記の「約定価格を決定する関数」で紹介した全ての関数で満たします。
###条件1
Theorem opentrade_valid1 (price:option priceType) (book:orderbookType) :
orderbook_valid book -> traderesult_valid1 (opentrade price book).
Proof.
###条件2
Theorem opentrade_valid2 (price:option priceType) (book:orderbookType) :
orderbook_valid book -> traderesult_valid2 (opentrade price book).
###条件3
Theorem opentrade_valid3 (price:option priceType) (book:orderbookType) :
orderbook_valid book -> traderesult_valid3 (opentrade price book).
###約定価格の存在性
Lemma deals_price_isSomeP
(price:option priceType) (book:orderbookType) :
reflect
[\/ isSome price,
has (isSome \o price_of) book.1 |
has (isSome \o price_of) book.2]
(isSome (opentrade price book).1.1).
任意の入力に対し、板寄せアルゴリズムの返り値の約定価格がこれを満たすことを証明できます。
###約定の健全性1
Lemma opentrade_contract_valid1
(price:option priceType) (book:orderbookType) :
orderbook_valid book -> contract_valid1 book (opentrade price book).
###約定の健全性2
Hypothesis (pricerel_opl :
forall x y, pricerel x y -> pricerel x (priceop x y)).
Hypothesis (pricerel_opr :
forall x y, pricerel x y -> pricerel (priceop y x) y).
Lemma openorder_contract_valid2
(price:option priceType) (book:orderbookType) :
orderbook_valid book -> contract_valid2 book (opentrade price book).
priceopに関する仮定としてproceop_oplおよびpriceop_oprが必要です。この条件も上記の「約定価格を決定する関数」で紹介した全ての関数で満たします。
#まとめ
板寄せアルゴリズムをCoq/SSReflectで形式検証しました。
異なる指値価格の注文を約定させる関数によって、仕様を満たす複数の板寄せアルゴリズムが存在することも分かりました。