どうやって確かめているか

帳簿の意味を決めるのは参照インタプリタで、chobo run がそれです。chobo が作るほかのもの、つまり SQL と十二のクライアントは、本物のデータベースで同じシナリオを流して、参照インタプリタと突き合わせます。検査と人が読むページが帳簿について言うことも、参照インタプリタで流して見つけたことです。

どのクライアントでも、意味は一つ

テストは、すべての例とテスト用の帳簿からシナリオを作り（手で書いたものを含めて 468 本、そのうち 38 本は呼び出し元が同時に来るもの）、一つずつをすべてのクライアントで流します。

操作が返すもの、終わりの残高、仮押さえの状態が、どれも参照インタプリタと同じでなければなりません。呼び出し元が同時に来るシナリオでは、参照インタプリタが出す、とりうる結果のどれかと同じでなければなりません。together の呼び出し元は、それぞれ別の接続（TigerBeetle では別のクライアント）から、同じ瞬間に送ります。どのクライアントも、chobo run --show が言うものを、フィールドまで（MySQL の系統では SQL 文の一字まで）そのとおりに送らなければなりません。だから四つの言語は、同じ呼び出しをし、同じ ID を作ります。まとめて送る形では、エラーのために走らなかった文もリクエストに入るので、比べるのは結果だけです。

データベースは本物です。ソケットでだけ受け付ける PostgreSQL のクラスタ、--development で立てた TigerBeetle のレプリカ一つ、MySQL のサーバー、Vitess の試験用のサーバー（vttestserver）二つは、テストのために立てて、終わったら捨てます。Vitess の一つはキースペースをシャード一つに置き、もう一つはテーブルをテナントで二つのシャードに分けて、シャードをまたぐトランザクションを誤りにします。テナントのシャードの外に出る呼び出しがあれば、そこで落ちます。TiDB は、マシンで動いているクラスタに、テストが自分のデータベースを作って使い、終わったら消します。最後に、PostgreSQL では、どの勘定の残高も entries の合計になっていることを、MySQL、TiDB、Vitess では、どの勘定の行も、足し込んだ記録の合計になっていることを確かめます。シナリオはそれぞれ自分のテナントで流すので、全部を同時に流せます。テストの仮押さえは、帳簿に何と書いてあっても 3 秒で切れるようにしてあり、ランナーは期限が来るのを実際に待ちます。遅いマシンでは、参照インタプリタの時計では期限の前に来るはずのステップが、期限のあとになってしまうことがあります。そのせいで食い違ったシナリオは、ほかの遅れたシナリオと一緒にもう一度流し、また遅れて食い違ったときだけ失敗にします。

データベースごとの確かめ

• PostgreSQL：四つのセッションが、同じ勘定のあいだを逆の向きに百回ずつ動かしても、デッドロックが起きないこと。REPEATABLE READ で、四つの呼び出し元が一つの勘定に 50 回ずつ入れ、どのクライアントも失敗したシリアライズをリトライして、200 回の呼び出しが全部済むこと。関数を通らない UPDATE を、CHECK 制約が止めること。境界を書き換えた行では、呼び出しが CB001 で止まること。expire() が言うとおりのものを戻し、どの残高も勘定の entries の合計になっていること。chobo_id が作る ID が、ほかの出力先と同じであること。
• TigerBeetle：上限を変えた帳簿を同じテナントで呼ぶと、その境界のために最初に流す振替で失敗すること。無い仮押さえの確定が、何も送らずに no_such_hold を返し、そのあと同じキーで仮押さえを作って確定できること。どちらも四つの言語で確かめます。
• MySQL、TiDB、Vitess（シャード二つ）：TypeScript のクライアントを通して、英語の帳簿と、テーブルの名前が日本語になる日本語の帳簿で確かめます。四つの呼び出し元が、同じ勘定のあいだを逆の向きに百回ずつ動かしても、デッドロックも呼び直しも起きないこと。クライアントを通らない UPDATE を CHECK 制約が止めること（TiDB では tidb_enable_check_constraint を ON にして作ったテーブルで。OFF で作ったテーブルに制約が無いことも確かめます）。境界を書き換えた行では、呼び出しが CB001 で止まること。expire() が言うとおりのものを戻し、境界の無い勘定の記録を勘定の行に足し込むこと。最後の 100 個を八つの呼び出し元が 50 回ずつ取りに来て、ちょうど 100 回が通ること（一つずつ送る形とまとめて送る形の両方で）。呼ぶ側のトランザクションの中にある接続を渡すと、呼び出しがそのコミットとロールバックに従うこと。TypeScript、Python、Go のどれでも、トランザクションの中にいない接続では呼び出しが自分のトランザクションになり、呼ぶ側が始めたトランザクションや autocommit を切った接続では、作った勘定の行も含めてロールバックで消え、その行を次の呼び出しが作り直すこと。Rust では、トランザクションの中にいないプールの接続では呼び出しが自分のトランザクションになり、sqlx の Transaction の中では、呼ぶ側の行と一緒にロールバックで消えること。まとめて送ると、結果は同じでリクエストが減ること。大文字と小文字、末尾の空白、濁点だけが違うキーが別の呼び出しになり、大文字と小文字だけが違うテナントが別の残高になること。sql_mode が ANSI_QUOTES でも NO_BACKSLASH_ESCAPES でも、引用符とバックスラッシュの入ったキーが通ること（Vitess はこの二つを設定させないので、そのままの設定で流します）。
• TigerBeetle の一つのリクエストに入らない帳簿（E060）、PostgreSQL には長すぎる名前の帳簿（E061）、MySQL が名前を持てない帳簿（E062）、Rust のターゲットでは Rust が名前にできない字を持つ帳簿（E063）が、ビルドされないこと。

生成するコード

生成した TypeScript は、erasableSyntaxOnly と noUnusedLocals を付けた tsc --strict を通ります。Python は py_compile を通り、ritsu のテストが mypy --strict にもかけます。Go は gofmt と go vet を通ります。Rust は、エディション 2021 と 2024 の両方で、clippy の lint も含めて警告なしで組め、単位の型を受け取る ritsu のパッケージの中でも組めます。頭に書くクレートの版はテストが固定した版で、E063 が名前から外す字は、chobo の名前に書けるどの字についても、rustc が外す字と同じです。テストは Node.js 23.11、Python 3.13、Go 1.26、Rust 1.94 で、PostgreSQL 18.0、TigerBeetle 0.17.9、MySQL 8.4.11、TiDB 8.5.8、Vitess 24.0.5 を相手に走ります。

診断

tests/fixtures のテスト用の帳簿の診断は、どれも英語と日本語の golden ファイルと比べます。どのコードにも、chobo explain が出す専用の帳簿があり、テストは、その帳簿がそのコードを出すことを確かめます。日本語の名前のテスト用の帳簿には、どれも英語の版があり、二つは同じコードを出して、同じようにエラーで止まるか通るかしなければなりません。診断と報告が挙げる操作の列は、言う前に参照インタプリタで流してあります。並ぶのは、操作の列が実際に届いた理由だけです。

人が読むページ

chobo doc が例とテスト用の帳簿について書くページは、golden ファイルです。ページが見せるどのステップにも、そのステップのあとに参照インタプリタが残した残高が載ります。Mermaid の図は、どれも Mermaid 11 と Mermaid 12 で描けることを確かめます。HTML のページは Chrome で開き、ステップを進めたときに、ページのデータどおりの残高が出て、そのステップが呼んだ振替が光ることを確かめます。このサイトに置いた例のページも、chobo doc のいまの出力と一字も違いません。

Lean の証明

参照インタプリタを Lean 4 のモデルとして書き直してあり（ritsu の proofs/ の ChoboModel）、定理はそのモデルについてのものです。

• 通った呼び出しも、時間が過ぎることも、勘定を、境界が禁じる向きに越えさせません。だから、境界の中にある勘定は、何を呼んでも境界の中にとどまります。
• 拒否された呼び出しは、残高も仮押さえも変えません。移動は全部行われるか、一つも行われないかです。
• 同じ do や hold をもう一度呼ぶと、done_before を返して何も変えません。だから、リトライで二度動くことはありません。

モデルは、例とテスト用の帳簿の、どのシナリオでも参照インタプリタと並べて走らせます。二つは、ステップごと、勘定ごと、仮押さえごとに、同じ結果でなければなりません。どの証明も、sorry にも独自の公理にも頼っていません。

文書

README、リファレンス、エージェントのスキル、このサイトのページは、テストがツールと突き合わせています。載せた診断はどれも golden ファイルにあり、帳簿の行はどれも実在する帳簿の行です。出力つきで載せた chobo のコマンドは、どれもいまその出力を出し、相対リンクはどれも行き先があり、書いた数は実際の数です。上の 468 本のシナリオと 32 種類のコードもそうです。

テストを動かす

$ cargo test -p chobo

ritsu のリポジトリでこれを走らせると、次のうち見つかったものを使います。

• PostgreSQL（PATH にあるものか CHOBO_PG_BIN）
• TigerBeetle（crates/chobo/tools/tigerbeetle/fetch.sh か CHOBO_TIGERBEETLE）
• MySQL（crates/chobo/tools/mysql/fetch.sh か RITSU_MYSQL_BIN）
• TiDB のクラスタ（RITSU_TIDB に host:port）
• Node.js と Python と、crates/chobo/tools/runner に書いた依存
• Go
• Rust と clippy と、crates/chobo/tools/runner/rust のクレート（cargo が取ってきます）
• Chrome（CHOBO_CHROME）
• Mermaid（npm ci --prefix crates/chobo/tools/mermaid）

見つからないものは、それぞれ SKIP: の行を出して飛ばします。