何を証明するか

rulec check がこのツールの中心です。生成もベクタも再生も、全部その下流にあり、検査を通らない規則からは何も生成されません。

$ rulec check rules/ --lang ja
note rules/ゆうパック運賃.rule: 隠れ 21 対（階段 21、同じ答え 0、要確認 0）
ok rules/ゆうパック運賃.rule

note の行にある「隠れ」は、先に書いた行が後ろの行を隠しているという意味です（シャドーイング）。policy first の表ではふつうの姿なので、件数だけ出ます。

exit code は 0（注記だけ）、1（エラーあり）、2（引数の誤りか読めないファイル）。出力が空に見えるかどうかではなく、exit code を読んでください。

七つの検査

constraint を書いた規則では、完全性の言う「どの入力」がその分だけ狭くなります — 起きないと宣言した組み合わせに行は要求されず、そのかわり生成コードがその組み合わせを入口で受け付けません。fold のある規則では、表が出しうる判定に行き先があるかを、表の完全性と同じ検査が見ます（E024）。

import proto で列挙の値の集合を .proto と対応づけた規則では、完全性の検査が一つのファイルの中で閉じません。rulec check が毎回そのファイルを読み、集合がずれていれば E032、そろっていて行も default も無い値があれば E033 で止まります。列挙に値を足すのはワイヤの上では互換な変更なので、契約の側のツールでは止まりません。その値が - の行に吸われて黙って既定の額で通るのを、ここで捕まえます。

入力が呼び出し側のオブジェクトのどこから来るかを書いた規則（shape と from）も、同じように契約に縛られます。パスは毎回の rulec check でたどられ、契約に無いパスは E121（どこまで届いたか、そこに何のフィールドがあったかを言います）、型が入力と合わなければ E120、どの入力も射影していない契約は W122 です。どれも表の検査は動かしません——射影から出てくるのはただのスカラーの入力です——止めているのは、アプリケーションと規則のあいだをつなぐコードが、黙って古くなることのほうです。書き方はルール(.rule)を書くに、契約と並べた例は例で見るにあります。

契約は、そこからどんな値が来るかも言っています。それも入力の宣言と突き合わせます。.proto のフィールドに付いた Protovalidate の規則や、JSON Schema の minimum・maxItems・enum・required を、入力の range、列挙の値、count の範囲と比べて、契約は通すのに入力が受け付けない値があれば E122 です。API 自身が受け付けたリクエストを、生成コードが入口でエラーにすることになるからです。fix.text は契約に足す注釈そのものです。契約が通さない値でしか当たらない行は W123 です。proto3 で注釈の無い数のフィールドは、入れ忘れると 0 として届くので、いちばん多く引っかかるのはそこです。required の無いメッセージのフィールドは省略でき、そのとき Protovalidate は中を何も検証しません。中の値はそれ自身の規則にかかわらず既定値として届くので、既定値を受け付けない入力も E122 です。

契約は、フィールドどうしの関係も言っています。.proto のメッセージに付けた this.declared_jpy <= this.cover_jpy のような CEL の式、oneof、JSON Schema の allOf・anyOf・oneOf・not・if/then です。これも読みます。同じ契約から読む二つの入力のあいだの constraint を契約が守っていなければ E123 です。契約の検証を通るリクエストのなかに制約を破るものがあり、生成コードがそれを入口でエラーにすることになるからです。例にはそのリクエストを出し、.proto なら、約束させる (buf.validate.message).cel が fix.text です。契約が通さない組み合わせでしか当たらない行、たとえば契約が速達を 5kg までに限っているのに 5kg を超える速達を求める行は W124 です。条件のうち読めない部分（剰余や文字列の関数）は真として扱うので、どちらも見逃すことはありません。契約が、これらの値について規則の求めることを全部守っているときは、rulec certificate がその理由を場合ごとに書き出し、二つの再検査器がそれを確かめます。Lean のほうは定理 included_sound の上で確かめます（どうやって確かめているか）。

本則の表と、overrides でそれに優先する特例の表のように、同じ出力を定める表が二つ以上ある規則があります（文で書く clause も同じ仲間です）。そこでは、上の三つの検査がそれらをまとめた一つの集合に対して走ります。完全性は表を合わせて見ます。行の重なりは、どちらが優先するか書いてあれば通り、無ければ E105 で止まります。優先する表の行に丸ごと覆われて出番の無い行は E102、優先すると書いたのに交わる行が一つも無ければ W117 です。人が読む資料は、どの表がどの表の例外なのかを一文で書きます。

source で文書を宣言し、@出典 第91条 のように引用している規則では、引用した箇所のコピーが規則の隣にあり、そのハッシュが規則に書いてあるとおりであることを check が確かめます。ハッシュが書いてなければ E037 です。コピーがハッシュと違えば E038 で、その箇所を引用している表・節・行を名指しします。コピーが無ければ E039、引用していない箇所のハッシュが残っていれば W119 です。check は通信しません。コピーを取るのは rulec source fetch、ハッシュを書くのは rulec source pin、法令の出典なら、後の改正で条文の本文が変わるか（XML の属性だけの違いは数えません）を政府の法令データベース（e-Gov 法令検索）に問い合わせるのは rulec source outdated です。

文書から引くのは表です。料金表や社内規程のような文書は、@出典 表1 と書くとその表が文書から取り出されて隣に置かれ、以後はそのコピーに縛られます（Excel はシート、Word は文書の中の表、Markdown と CSV はそのまま。PDF やスキャンは --via で抽出器を渡します）。ここでもう一つの検査が効きます。

• E116 — その行が書いた金額が、引いた出典のコピーのどこにも出てきません。表の中だけを見る検査では絶対に出ない誤り、つまり転記の誤りがここで止まります。1100円 を 1000円 と書いても、刻みには載っていて、抜けも重なりもないからです。行の語（関東）と同じ見出しがコピーにあれば、その見出しの行と列の中で探すので、コピーのどこかにはある隣の行の金額を転記してしまったときにも止まります。
• W120 — コピーが数だけのセルで言っている値を、どの行も使っていません。行を一本転記し忘れたときに出ます。落ちた行の入力は残った行のどれかに当てはまってしまうので、完全性の検査には出ません。
• E119 — 境界の値が、コピーの言っているのと反対の側に入っています。コピーが「60cmまで」なのに <60cm と書いた、という誤りです。これもほかの検査には出ません。60 という数は使っているので W120 は黙り、境界を分け合う二つの行を両方動かせば抜けも重なりもできず、答えが変わるのはちょうど 60cm の一点だけです。

閾値は転記するときに書き換わる（1,949,000円まで は <=1949000円 になる）ので、文字としては比べられません。それでも一つだけ書き換えを生き延びるものがあって、それが境界の値そのものがどちらに入るかです。「60cm以下」と「60cmを超え」はどちらも 60cm を小さいほうに入れると言っていて、<=60cm と >60cm も同じことを言います。だから規則がどちらの端から書いていてもコピーと突き合わせられます。読むのは数のとなりの語（「60cm以下」「Under 18」「Not over $11,925」）と、フィールドの見出しの語（「円以上」「円未満」——日本の料額表の普通の形）です。コピーがどちらとも言っていない境界（18 to 20、60〜80）には何も言いません。境界になる数を挙げるだけでは、その数がどちらに入るかは決まらないからです。人が読む資料には、転記元の表がそのまま引用され、確かめたことの一覧に二行増えます——この表の金額はコピーに出てくる値であること、境界はコピーが書いている側と同じであること。

ほかの規則を準用する規則（apply）では、check が四つを確かめます。元の規則のハッシュが書いてあるとおりか（E040）。元の規則の入力を全部読み替えたか（E041）。型が合うか（E042）。この規則が渡す値が元の規則の範囲と制約に収まるか（E043。はみ出す値を一つ例に挙げます）。準用できない規則（自身が apply を持つ、並びを順に見ていく、check を通らない）は E044 です。元の規則の表と節はこの規則の中に展開して一緒に検査します。この規則の範囲では当たらない行は黙って通し、表の全行が当たらないときだけ W118 を出します。

ステートマシンの一歩になっている規則（machine）では、呼び出しのあらゆる並びで何が起きうるかも確かめます。final の状態から案件を動かす呼び出しは E124、たどり着けるのに終われない状態は E125、after の状態を通ったあとに never の状態に着く並びは E126、一つの案件で once のセルに当てはまる答えが二回ある並びは E127 です。どれにも付く具体的な例は、始まりの状態からの呼び出しの並びで、主張を崩す最短のものです。一回ずつが、規則の受け付ける入力です。どの並びでも着かない状態は W125、そういう状態でしか当たらない行は W126 です。何回かの呼び出しにわたる例 scenario は、例と同じように実行します。

すべての診断は業務の言葉で一行目を書き、そのエラーを実際に起こす具体的な入力を必ず付け、ヒントは書き換えたあとの形まで示します。

「証明した」と「型が合っている」は別のこと

型が合っていることが言うのは、値がその形をしていることです。列挙のどれかである、整数である、単位が揃っている。型のついた値を返す API やモデルが増えたので、この二つは混ざりやすくなりました。形が正しいことは、答えが正しいことを何も言いません。

rulec check が証明するのは形ではなく表の性質です。宣言した範囲のどの入力にも当てはまる行がある。二つの行が同時に当てはまらない。どの行にも出番がある。単位が混ざらない。途中の値が int64 に収まる。この五つを、しらみつぶしに調べて示します — 標本を取るのではありません。

なぜ全部を調べ切れるのか。 セルに書けるのは自分の列への条件だけだからです（<=2000g は重量の列、遠隔地 はあて先の列）。だから一行は列ごとの条件のかけ算、つまり入力の組み合わせの中の一区画になり、数値の列も表に出てくる境目でだけ切れば足ります。宣言した範囲は有限個の区画に落ちるので、あとはその全部を見るだけで検査は必ず終わります。セルの書き方を狭くしてあるのは、この形を保つためです。完全性については、調べ切れなかったときに黙って通すことはありません — 予算を超えれば E109 で止まります。

そのうえで、証明していないことが四つあります。

1. 表が現実と合っているか。 証明しているのは「書かれた表について」です。転記元の文書を @出典 表1 で引いていれば、金額がコピーと食い違うところまでは落とせます（E116・W120）が、それでも言えるのは「引いた出典のコピーと合っているか」までです。引用が無ければ、料金表を誤って転記しても全部通ります
2. 生成コードが表と同じ答えを返すか。 これはテストです。境界から作ったケースを参照評価器と全言語に流し、バイト単位で比べています。強い証拠ですが、同値の証明ではありません
3. W114 の対。 重なるかを決められなかった行の組は、実行時のガードに移ります。つまり「重なりが無いこと」は、いつでも証明できるわけではありません。証明できなかった対は必ず名指しします
4. 検査器そのものが正しいか。 上の五つを出しているのは rulec の実装で、その実装の正しさを証明したわけではありません。根拠は、わざと壊した規則 109 本（tests/mutants/）が狙ったとおりの診断を出すこと、公開されている規約や法令から転記したものを含む規則集が、毎コミット通ること、参照評価器と 12 言語の答えが一致すること。証拠であって、証明ではありません

Rust については、生成したものをもう一つのツールが読みます。gen が Kani の証明ハーネスを書き、宣言した範囲のすべての入力について、どの表も素通りしないこと、3 のガードが当たらないこと、i64 があふれないこと、unique の表の行が範囲をちょうど一度ずつ覆うことを確かめます。上の検査器とは、コードを一行も共有していません。一致すれば、無関係な二つのツールが同じことを言ったことになります。食い違えば、どちらかが誤っていて、それを示す入力が出てきます（生成する）。

証拠は渡せる形で出て、その検査が主張を含意することは Lean で確かめてあります。 rulec certificate は、五つの証明が寄りかかっているものをそのまま書き出します — 入力の空間を敷き詰める木、unique の行の対ごとに座標の交わらない軸、行ごとの到達する点とその裏にある値、計算する値ごとの区間と型。あわせて、どのセルがファイルのどこにあるか（行・バイト位置・長さ）と、そこに何が書かれているかも出します。これを読み直すプログラムが二つあります。ひとつは tools/recheck.py、依存ゼロの一ファイル。もうひとつは proofs/ が作るプログラムで、表の意味と、検査と、「検査が通れば主張が成り立つ」という定理を Lean 4 で書いたものです。lake build が定理を確かめ、そのプログラムは定理が対象にしている検査そのものを走らせます。これで 4 が「信じてください」と言っている相手は、42,000 行の Rust から、健全性を証明した数百行の検査に移ります。ただし移るだけで、消えはしません。ツールが正しい証明書を出すかどうかはいまも証拠ですし、証明書に書かれた宣言範囲・型・制約はその証明書自身の言い分です。証明せずに名指しするだけのものも五つあり、どちらのプログラムも最後にそれを並べて終わります（形式）。

この四つを隣に置いたまま「証明」と言う、というのがこのツールの決めです。

診断の読み方

エラー[E101]: 完全性の欠落: どの行にも当てはまらない入力があります
  --> rules/ゆうパック運賃.rule:34 表 運賃表
   |
34 | table 運賃表(fee_table)
   |       ^^^^^^ 起こりうる入力を網羅していません
   |
 当てはまらない例: あて先 = 山梨県, サイズ = S60
 ヒント: この入力に当てはまる行を足してください。
 足す行の形: `| 山梨県 | S60 | 820円 |`。出力の値は表の一行目からコピーした仮の値で、正しい値とは限りません。…

考えるべきはそれを起こす入力です。あて先 = 山梨県, サイズ = S60 は「たとえば」の話ではありません — 検査器が実際に組み立てた入力そのものであり、答えを知っている人にそのまま渡せる一文です。

件数が多いとき: --terse

$ rulec check rules/ --terse --lang ja
エラー[E101]: 完全性の欠落: どの行にも当てはまらない入力があります
  --> rules/ゆうパック運賃.rule:34 表 運賃表
  その入力: あて先 = 山梨県, サイズ = S60
…
details: rulec explain <code>

見出し・位置・その入力の三行。残りをどう見るかは、検査の最後に一度だけ出ます。

プログラムが読むとき: --format json

同じ指摘をデータで。文面も残りますが、下流が文を解析する必要はありません。

$ rulec check rules/ゆうパック運賃.rule --format json | jq -c 'select(.code=="E101") | {table:.where.table, witness:.witness.inputs, fix:.fix}'
{"table":"運賃表","witness":{"あて先":"山梨県","サイズ":"S60"},"fix":{"kind":"add_row","text":"| 山梨県 | S60 | 820円 |"}}

where がどの表のどの行か、witness が「どの入力にどの値を入れたか」（数値は決めた単位の整数）、rows が関わっている行の全部、fix がそのまま貼れる書き換え後の形です。witness と fix は --lang で変わりません — 変わるのは名前が文面だと言っているフィールドだけです。形式の定義は 形式 にあります。

コードを引く

どのコードにも項目があります。いつ出るか、どう直すか（書き換え後の形まで）、走る最小の再現、関係するコード。

$ rulec explain E101 --lang ja
エラー[E101]: 完全性の欠落: どの行にも当てはまらない入力があります

いつ出るか
  行を全部合わせても、宣言した範囲の入力を覆いきれていないとき。…

直し方
  それを起こす入力に当てはまる行を足してください。…

最小の再現
  rule t(t) v1

  enum k(k) = a(a) | b(b) | c(c)
  …

関係するコード: E102 E105 W111

rulec explain --all --format markdown が一覧の全部で、このサイトの 診断コード はその出力そのものです。載っている再現は全部テストが走らせているので、「文章は立派だが実はもう嘘」という古び方をしません。

新しく出たものだけ

$ rulec check rules/ --diff-base origin/main

基準にしたリビジョンに既にあった指摘は伏せられ、伏せた件数が出ます。同じ指摘かどうかは行番号ではなくセルを揃えた形で見るので、行を一つ挿しただけで全部が新規に見えることはありません。

これで、CI の警告が使いものになります。意図してそうしている policy first の隠れを何年も抱えたままの表があっても、この変更が持ち込んだ一件が埋もれません。

証明できないとき

そう言います。近似して通すことはしません。

• E109 — 検査の予算を超えたので完全性を証明できなかった。表を分けるか --budget を上げてください。何も仮定しません。
• W114 — unique の表の二行が重なるかもしれないが、それを起こす入力を組み立てられず、「起こりえない」ことも示せなかった。警告を出し、生成コードにガードが入ります — 万一その条件に当てはまる入力が来たとき、黙って先の行を選ばずエラーを返します。このガードが動いたなら、その重なりは本当にあったということです。入力を共有する二つの導出と、真偽の定義の中の閾値は、ここには落ちてきません。変数を一つずつ消していく方法で決まるからです。残るのは、その方法が有理数の上で解いているために決まらない形——値が整数であることだけが妨げている対です。

koyomi の日付がとる日の上で

日付の入力は、範囲を koyomi のファイルの日付からとれます。pay_day : date range from koyomi "payment_terms.cal" date payment と書きます。koyomi は自分の入力の範囲のすべてで日付を計算するので、とる日が正確にわかり、七つの検査はその日の上だけで行います。支払日と支払日のあいだの日には行が要りません。どの行も取らない支払日があれば、その日を例にした E101 になり、支払日を一つも取らない行は E102 になります。生成コードはほかの日を入口で受け付けず、証明書には日の並びと koyomi のファイルの SHA-256 が入ります。日の集合は ritsu を通して koyomi から受け取るので、ritsu rulec check か ritsu check で確かめます。koyomi をつないでいない rulec は、すべての日で確かめ直すことはせず、確かめられないと言います（E129）。くわしくはリファレンスにあります。

人に見せる

$ rulec doc rules/ゆうパック運賃.rule --lang ja > 運賃.md

.rule は既にほぼ markdown なので、書いてあることをそのまま繰り返しても価値がありません。doc の仕事は、検査器が知っているのに文字には出ていない事実を添えることです — 6 値のグループとその「以外」の 41 値が本当に 47 を覆っていること、どの行がどの行を隠しているか、どの丸めが根拠なしの仮置きか。

rulec doc が出すのはこういう資料です（抜粋）。

## グループ

グループは列挙の一部に名前を付けたものです。表のセルに書かれた一語が、下の値をまとめて指しています。

- **近畿圏**（6 値）— 滋賀県、京都府、大阪府、兵庫県、奈良県、和歌山県
- **中国四国**（9 値）— 鳥取県、島根県、岡山県、広島県、山口県、徳島県、香川県、愛媛県、高知県
- **沖縄**（1 値）— 沖縄県
…

この 6 グループは 都道府県 の 47 値を過不足なく分割しています（この資料が宣言から数えました）。

## 表 運賃表（policy unique）

| 列 | 出どころ |
|---|---|
| あて先 | 入力 |
| サイズ | 表 サイズ判定 の出力 |
| → 運賃 | この規則の出力 |
…

表の行や table 行に # 出典: 日本郵便 基本運賃表（東京） と書いておけば、その言葉もこの資料に出ます。読む人の仕事が「表全体をもう一度読む」から「この行とあのセルを見比べる」に変わります。

自分の件を入れて試せるページ

$ rulec doc rules/送料.rule --lang ja --format html > 送料.html

--format html にすると、同じ資料が一枚の画面になります。左が入力欄、真ん中にカードが並びます。カード一枚が、値を一つ決めているもの——表ひとつ、derive ひとつ、define ひとつ——で、その表そのものがカードの中に入っています。読む人が自分の件を入れると、当てはまった行がその表の中で色づき、カードにはその行番号が、答えのカードには結果が出ます。生成コードがログに書く一行も、そのまま左に出ます。「例」のボタンは、規則に書いてある検証済みの例をそのまま入れます。ページは、読む人のブラウザの設定に合わせて、明るい配色でも暗い配色でも出ます。

カードを選ぶと、下にもう一枚ペインが開きます。その表の列がどこから来るのかと、rulec check がその表について確かめたことです。選んだカードだけが色を持ち、ほかはモノクロのままなので、いま読んでいるのがどれかを見失いません。

ページの中で動くのは生成した JavaScript そのもので、コードが言わないことをページが言うことはありません。入れた件も選んだカードも URL に残るので（?dest=東京都&weight=1999&…#t-基本送料）、「この件のこの表を見てください」がリンク一つで送れます。

してはいけないことが一つあります。検査器の出力に無い文章は書きません。 どの行もかならず、もとの表か検査の結果にたどれます。出どころも、「rulec check が確かめました」と「この資料が宣言から数えました」で必ず書き分けます。コミットはしません — CI がその場で作って PR に貼ります。古い資料がいまの正しい姿に見えてしまうことが、この設計でいちばん避けたい危険だからです。

診断コードの一覧 生成して呼ぶ

顧客に見せる

$ rulec doc rules/ゆうパック運賃.rule --lang ja --audience customer > 運賃の案内.md

同じ規則を、ヘルプセンターに載せる案内の形で出します。別名や宣言範囲、診断コードは出しません。代わりに、条件の境目の両側で答えがどう変わるかを例として添えます。例は境界両側のベクタから取るので、<=60cm の行が 61cm にどう効くかを、読む人も、検索して読むモデルも、自分で考えずにすみます。

## 境目の例

条件の境目をまたぐと、答えがどう変わるかの例です。

- 三辺合計が 60cm のとき 運賃 1410円、61cm のとき 運賃 1710円（あて先: 北海道、重量: 1g）
- 三辺合計が 80cm のとき 運賃 1710円、81cm のとき 運賃 2020円（あて先: 北海道、重量: 1g）
…

境目の例

条件の境目の両側で、答えがどう変わるかです。

• 三辺合計 が 60cm なら 運賃 1410円、61cm なら 運賃 1710円（あて先 北海道、重量 1g）
• 三辺合計 が 80cm なら 運賃 1710円、81cm なら 運賃 2020円（あて先 北海道、重量 1g） … ```

このページは一つの層です。どうやって確かめているかに、層の全体と、 それぞれがどこで止まるかをまとめてあります。