どうやって確かめているか
rulec が「確かだ」と言うことは多くありません。そのかわり、一つずつに手数をかけています。このページはその見取り図です。層ごとに、何が言えて、どこから先は言えないのか、そして自分で走らせるならどのコマンドか。上の層を信じてくださいとは言いません。層ごとに別のプログラムで、いくつかは検査器とコードを一行も共有していません。
並びは走る順番そのままです。ある層で止まった規則は、次の層に進みません。
絵にすると、層の置きどころが見えます。縦に並ぶ四つは、どれも一つ上のものを書き表したものです。検査の層はたいていその継ぎ目にいて、上と下を突き合わせています。表からはもう一つ、証明書が出ます。五つの証明の中身をそのまま書き出した JSON で、7 の二つの再検査器はこれを読み直します。継ぎ目にいないのは二つだけで、表そのものを見る 1・2・3 と、ツールのほうを向いている 8 です。そしていちばん上の継ぎ目には、層が一つもありません。現実を読んで文書にしたのは人で、その読みを確かめる手立ては、このツールの中にありません。
| 何が決まるか | 走らせ方 | |
|---|---|---|
| 1. 五つの証明 | 宣言が許すすべての入力について、抜けも、重なりも、当てはまらない行も、単位の取り違えも、あふれも無い | rulec check |
| 2. 二つの宣言 | 丸めは推測せず書かせる。証明が届かなかった重なりは、一方を黙って選ばずにエラーにする実行時のガードになる | rulec check |
| 3. 例 | 人が手で書いた答えが、いまも合っている | rulec check |
| 4. ベクタ | 生成コードが参照評価器と同じ答えを返す。12 言語、一バイトも違わずに | rulec test |
| 5. 網羅の七基準 | そのベクタが、どの行にも、どの境目の対にも、隠れている対にも、計算した値を二通りに動かす対にも、丸めの同着にも、畳み込みの遷移にも、ステートマシンの遷移にも、実際に届いている | rulec coverage |
| 6. モデル検査器 | 生成した Rust を、宣言した範囲のすべての入力について、rulec とコードを共有しないツールが読む | rulec test --proofs |
| 7. 証明書 | 渡せる大きさの証拠を、rulec とコードを共有しない二つのプログラムが読み直す。片方は Lean の証明つき | rulec certificate |
| 8. リポジトリ自身のテスト | わざと壊した 109 本が狙いどおりの診断を出し、87 本の規則が毎コミット検査・生成・実行される | cargo test |
| 9. 出典 | 行が引いている文書と金額が食い違えば落ちる | rulec source fetch のあと rulec check |
1. 五つの証明
完全性（E101）・重なり（E105）・当てはまらない行（E102）・単位（E103）・int64（E108）は、宣言した入力空間の全体について決めます。サンプリングではありません。全体を見て有限で済むのは §6.2 の圧縮があるからです。列はそのセルが名指す境目で切られ、境目と境目のあいだは全部同じ振る舞いをするので、1018 通りの組み合わせが数百の区画になり、歩けるようになります。
ステートマシンの一歩になっている規則では、呼び出しのあらゆる並びについての主張も同じやり方で決めます。終わりの状態から出る呼び出しが無いこと（E124）、たどり着けるどの状態からも終われること（E125）、never と once の行が言うこと（E126・E127）です。状態は有限の列挙で、ほかの入力は表自身の境目で切られるので、呼び出しの並びは、有限のグラフをたどることに置き換わります。主張が崩れれば、崩す最短の呼び出しの並びが返ってきます。
届かないところ。 見ているのは「書かれた表」です。料金表を誤って転記した表は、五つとも通ります。そのための層が 9 で、それでも言えるのは「引いた出典のコピーと合っているか」までです。
2. 二つの宣言
丸めは推測しません。 数値の出力に round が無ければ E104 で、そのとき動く金額が診断に出ます。どちら向きに丸めるかは業務の判断なので、ツールが代わりに決めません。
決着しなかった重なりは、ガードになります。 二つの行に同時に当てはまる入力も、そんな入力が無いことの証明も組み立てられなかったとき、W114 がその対を名指しし、生成コードは一方を黙って選ぶかわりにエラーを返します。静的な答えが無い唯一の場所で、しかも隠れずに出力に現れます。
3. 例
examples は実行できる仕様です。rulec check のたびに全行が参照評価器を通り、合わない行は E107 として、当たった行つきで返ってきます。
これがあるのは、下の層が揃って同じ間違いをすることがあるからです。実際にありました。複数出力の丸めが参照評価器にも生成した全言語にも同時に無く、突き合わせは最後まで緑のままでした。それを捕まえられるのは、人が書いた期待値だけです。
4. ベクタと、12 言語
rulec gen はコードの隣にベクタ一式を書きます。規則の境目から組み立てた入力と、参照評価器が返す答えです。rulec test は生成した全言語をそれに通し、一バイトずつ比べます。「だいたい合っている」では通りません。比べるのは答えだけでなく、当たった行もです。
言語は 12 ですが、呼び出し方はそれより多くあります。モジュールそのもの、MCP サーバ、同じサーバの HTTP、WASI 向けにコンパイルした Rust のランナー、Wasm のコンポーネント、SQL の問い合わせ、同じ問い合わせを PostgreSQL の関数にしたもの。呼び方ごとに別の通しです。入力を受け付けない規則にはそのためのベクタもあり、受け付けてはいけないところで答えてしまえば落ちます。状態を持ち越す規則には呼び出しの並びもあり、各言語が自分の返した状態を次の呼び出しへ渡すので、その受け渡しも比べます。
届かないところ。 これはテストで、同値であることの証明ではありません。意地悪に作った一式なので証拠としては強いのですが、定理ではありません。
5. 網羅の七基準
走るベクタと、届くベクタは違います。rulec coverage は規則そのものから出てくる義務を並べ、そのどれが満たされたかを言います。どの行もどこかで勝つこと、どの境目の対にも両側の例があること、policy first で隠れている対が試されていること、計算した値（リテラルではなく名前を返す行や、define で計算する出力）が、入力を一つだけ変えた二つのベクタで、実装が返す値として二通りに動いていること、丸めの同着がちょうど半分にあたる点を踏んでいること、畳み込みの遷移が全部通ること、ステートマシンなら、案件がたどれる遷移の一つずつと、続けて起きうる二つずつを、始まりの状態から通すこと。義務はベクタからではなく規則から出します。空っぽの一式を見て「全部満たしている」と言う監査は何も言っていないからで、そうなっていないことをリポジトリのテストが見張っています。丸めの同着の義務が立たないのは、規則の計算からどの入力も届かないと示せる出力だけです。見つからなかっただけの同着は、義務として残り、欠けとして出ます。
6. モデル検査器
生成した Rust の隣に、gen は Kani の証明ハーネスを書きます（#[cfg(kani)] の下なので rustc は読みません）。宣言した範囲のすべての入力について、どの表も素通りしないこと、2 の実行時ガードが当たらないこと、i64 があふれないこと、unique の表の行が範囲をちょうど一度ずつ覆うことを確かめます。
モデル検査器と、表を証明した検査器は、コードを一行も共有していません。 走らせる値打ちはそこにあります。一致すれば、無関係な二つのツールが同じことを言ったことになります。食い違えば、どちらかが誤っていて、それを示す入力がそのまま出てきます。
届かないところ。 読むのは Rust だけです。それと、ハーネスがそもそも出ない規則が二種類あり、どちらもファイルに理由が書いてあります。string の入力があるもの（あらゆる文字列を一度には置けません）と、allocate で配分を出しているもの（変数で割る式が二つ入ると返ってきません）です。
7. 証明書と、二つの再検査器
rulec certificate は、五つの証明が寄りかかっているものを書き出します。入力空間を敷き詰める木と各区画を覆う行、行の対がどの軸で分かれるか、どの行にも届く点とその値、計算される値が必ず収まる区間と型。そして表のどのセルがファイルのどこにあるかを、バイト単位で。どの軸でも分かれない対や、どの行も覆わない区画を、導出の式と制約が組み合わさって締め出しているときは、それらを足し合わせると矛盾になる乗数を書き出します。再検査器がするのは、その足し算です。規則が入力を読む契約については、契約の条件を場合に開き、場合ごとに、規則の入口が求めること（宣言した範囲、二つの入力のあいだの constraint、列挙の値）を守る理由を書き出します。呼び出し側の検証を通ったリクエストは、規則が受け取る、ということです。ステートマシンについては、行に載せた主張を書き出します。案件がたどり着ける状態を全部含み、一回の呼び出しで閉じている状態の集合、never と once の行を読むための組、そしてその集合のどの状態からも終わりの状態に着く呼び出しの並びです。
それを読むプログラムが二つあり、どちらも rulec とコードを共有していません。
tools/recheck.py— 一ファイル、依存ゼロ。区画をもとのセルから組み直し、そのセルを.ruleの本文の、証明書が言うバイト位置から読み戻し、残りをその主張に突き合わせます。ミリ秒で終わります。proofs/— Lean 4 の開発です。表の意味と、証明書が通らなければならない検査と、「検査が通れば主張が成り立つ」という定理が、そこに全部書いてあり、Lean が確かめています。lake buildが作るプログラムが走らせるのはその検査関数そのものなので、出てくるのは一つの文書に定理を当てた結果です。sorryもaxiomも一つもなく、#print axiomsに出るのは Lean 自身が立っている三つだけです。
二つ目を書いているとき、そして書いたあとに偽造する側になって読み直したときに、三つのものが出てきました。完全性の検査そのものの欠陥が一つ。規則の constraint を破る入力を例として出してしまう欠陥が一つ。そして、偽った証明書が再検査をすり抜ける手口が十一。
届かないところ。 証明書は、digest で一つの本文に、セル単位ではそのバイト位置で縛られています。それ以外——宣言した範囲、型、グループ、制約、各値の式——は証明書自身の言い分で、その裏を取るには規則のパーサが要ります。rulec と同じ読み方をする検査器は、rulec から独立していません。 契約の読み——どの入力に値を渡し、どんな条件を置き、それがどう場合に開くか——も証明書の言い分です。証明書は digest で契約の本文に縛られていますが、CEL やスキーマを読む再検査器はありません。
8. リポジトリ自身のテスト
五つの証明は rulec の実装から出てきていて、その実装の正しさは証明していません。証明の代わりに置いてあるのは証拠です。これは意識して貯めています。
- わざと壊した規則 109 本。それぞれが狙った診断を出します。出るべきコードは固定してあるので、別のことを言い出した変異はテストが落とします。
- 規則 87 本（34 本は公開されている出典からの転記、53 本は言語の隅に届かせるために書いたもの）を、毎コミット、生成できるすべての言語で検査・生成・実行しています。
- 文書をツールに突き合わせています。 診断の台帳はコードから焼き直し、生成コードのページはツールの出力そのものに突き合わせ、このサイトの例はコーパスのファイルに突き合わせています。ずれた文書は、落ちるテストです。
- 出しうる診断は全部台帳にあります。 113 件、それぞれに最小の再現例が付いていて、毎コミット走らせて「いまもそのコードを出すか」を確かめています。
9. 転記元の文書
規則は、転記元の文書を引けます。政府の法令データベースにある法令（source 法 = law "342AC0000000023" asof 2026-04-01）か、隣に置いて digest で固定したファイルか。行・表・節・導出の行末に @法 別表第一 と書くと、rulec check が表の金額と、文書のコピーの金額を突き合わせます。コピーのどこにも出てこない金額（行の語と同じ見出しがコピーにあれば、その見出しの行と列に無い金額）は E116、コピーにあるのにどの行も使っていない値は W120——一桁の打ち間違いには、たいていこの二つが一緒に出ます。閾値も、比べられるただ一つのやり方で比べます。コピーの「60cm以下」は 60cm を小さいほうに入れ、<60cm は大きいほうに入れる——これが E119 です。
届かないところ。 言えるのはコピーと合っているかで、現実と合っているかではありません。引用の無い規則には、この層がまるごと効きません。
どこにも届いていないこと
ここを正直に書くのも仕事のうちです。
- 表が業務の意図どおりか。 上の層は全部「書かれた表」についてです。9 がそれを「引いた出典のコピーと合っている」まで狭めますが、行けるのはそこまでです。
- rulec 自身が正しいか。 6・7・8 が三方向から攻めています（無関係なモデル検査器、独立した二つの再検査器、わざと壊した規則）。どれも検査器の正しさの証明ではありません。証明してあるのはその次の段——証明書が検査を通ったなら、その証明書の主張が成り立つ、という部分です。
- W114 が決着させられなかった対。 名指ししたうえで、黙って選ばずに実行時のエラーにしています。
- 宣言していないこと。 証明は宣言した範囲についてです。入力の範囲を広げれば主張も広い空間についてのものになり、狭めれば、その外の入力を生成コードが入口で受け付けません。