コンテンツにスキップ

rulec

ルールを書く。証明する。コードにする。

業務ルールのための小さな言語です。運賃表、クーポンの規約、返品の可否、軽減税率やただし書のついた税額表。条件は表に書き、そのまわりに計算、本則に優先する特例、ただし書、ほかの規則の準用、件数の決まらない明細の並び、状態が移っていく手続きの一歩を書きます。

小さいのはわざとです。再帰も状態も持たず、セルは自分の列しか見ません。だから rulec は、宣言した範囲のどの入力にも答えがちょうど一つ決まることを証明できます。テストでサンプリングするのではなく、一つ残らず調べて示します。証明できたルールだけが、12 の言語のふつうの関数になります。ランタイムも依存もありません。

書く作業はエージェントに任せられます。エージェントが返してくるのはコードではなく、人が読めるルールです。検査に落ちたところは、それを起こす入力つきで戻ってきます。人にしか決められないことは、質問として人に届きます。

ブラウザで試す インストール ルール(.rule)を書く エージェント向け GitHub

表を書く。rulec は一行を入力の組み合わせの一区画にして並べ、隙間も重なりも無いことを計算で証明する。抜けがあれば、それを起こす入力（あて先 = 遠隔地, 重量 = 2001g）が返ってきて、行を足してもう一度。運賃がいくらかだけは人が決める。証明できた表からだけ、依存ゼロの Python・TypeScript・JavaScript・Rust・Ruby・PHP・Go・Swift・Java・SQL・Wasm・NumPy が出る 表を書く。rulec は一行を入力の組み合わせの一区画にして並べ、隙間も重なりも無いことを計算で証明する。抜けがあれば、それを起こす入力（あて先 = 遠隔地, 重量 = 2001g）が返ってきて、行を足してもう一度。運賃がいくらかだけは人が決める。証明できた表からだけ、依存ゼロの Python・TypeScript・JavaScript・Rust・Ruby・PHP・Go・Swift・Java・SQL・Wasm・NumPy が出る

rulec がやること

table 運賃表(fee_table)
policy unique
| あて先 | 重量       | -> 運賃(fee) : money[円, incl_tax] |
| 近畿圏 | <=2kg      | 800円                              |
| 近畿圏 | >2kg <=5kg | 1000円                             |
| 近畿圏 | >5kg       | 1300円                             |
| 遠隔地 | <=2kg      | 1200円                             |
| 遠隔地 | >5kg       | 2000円                             |

表を土台にするから、証明できます

条件は表に書きます。セルは自分の列の値しか見ないので、一行は入力の組み合わせの中の一つの区画になり、区画どうしに隙間や重なりがあるかを計算で厳密に決められます。同じ表を、業務の担当者は仕様として読んで確かめ、生成したコードでは一行が一つの分岐になります。この表は上の図の運賃表で、一行足りません。

エラー[E101]: 完全性の欠落: どの行にも当てはまらない入力があります
  --> 運賃.rule:18 表 運賃表
   |
18 | table 運賃表(fee_table)
   |       ^^^^^^ 起こりうる入力を網羅していません
   |
 当てはまらない例: あて先 = 遠隔地, 重量 = 2001g

抜けと重なりは、走らせる前に落ちます

サンプリングではなく、宣言した範囲を全部調べます。足りない行は、そこをすり抜ける入力つきで返ってくるので、直すのは一行です。運賃がいくらかだけは、人が決めます。

エラー[E103]: この列は length[cm] ですが `1200円` が書かれています
  --> サイズ.rule:26 表 サイズ判定
   |
26 | | <=1200円 | S60                          |
   |   ^^^^^^^^
   |
 `1200円` は length[cm] の単位ではありません。

エラー[E104]: 丸めていない値が出力に到達します
  --> 割引.rule:21
   |
21 |   割引額(discount) : money[円,incl_tax]
   |                      ^^^^^^^^^^^^^^^^^^ 丸めの宣言がありません
   |
 例: 計算値が 0.12円 になる入力があります。down(1円) なら 0円、
     half_up(1円) なら 0円、up(10円) なら 10円 と、丸め方で最大 10円 動きます。

単位と税区分は型です。丸めは宣言しないと通りません

値は単位を持ち、金額なら通貨と、税込か税抜かも持ちます。だから円と g は足せず、税込の額を税抜の列に書くこともできません。途中の値がどれも int64 に収まることも証明します。数値の出力には端数の決め方の宣言が要り、書き忘れには丸め方で円がいくら動くかを見せてから訊きます。黙って寄せることはしません。

table サイズ判定(size_of)
policy first
| 三辺合計 | -> サイズ(size) : サイズ区分 |
| <=60cm   | S60                          |
| <=80cm   | S80                          |
| <=100cm  | S100                         |
…

table 運賃表(fee_table)
policy unique
| あて先 | サイズ | -> 運賃(fee) : money[円, incl_tax] |
| 都内   | S60    | 820円                              |
| 都内   | S80    | 1130円                             |
| 都内   | S100   | 1450円                             |
…

表を重ねて書けます

セルが自分の列しか見ないぶん、表は何段でも重ねられます。ゆうパックなら、三辺の合計からサイズを決める表と、あて先とサイズから運賃を決める表の二段です。前の表が決めたサイズを、次の表はそのまま列として読みます。どの段も同じように検査され、前の表が決して出さない値を後の表の行に書けば、その行は当たらない行として落ちます。答えには、どの段のどの行で決まったかが段ごとに付きます。

table 運賃表(fee_table)
policy unique
| あて先      | サイズ | -> 基本運賃(base) : money[円] |
| 遠隔地      | S60    | 1150円                        |
| 遠隔地      | S80    | 1400円                        |
| not: 遠隔地 | S60    | 820円                         |
| not: 遠隔地 | S80    | 1050円                        |

clause 通常(regular) -> 送料
  when always
  then 基本運賃

clause 無料(free) -> 送料
  when 注文金額 >=3900円 and 会員 true
  then 0円
  overrides 通常

特例やただし書も、まとめて検査します

ルールは一枚の表で終わりません。運賃表で基本運賃を決め、ふだんはそれが送料になる。ただし、会員が 3,900 円以上注文したときは無料。このただし書は clause で文のまま書き、overrides で本則に優先させます。検査は、本則と特例をひとまとまりとして読みます。どの入力もどこかに当てはまらなければならず、二つが当てはまるところでは、どちらが勝つかを overrides が言っていなければ落ちます。

machine 注文(order) over 遷移
  carry   状態 -> 次の状態
  held    支払額
  initial 受付
  final   配達済, 取消
  never   出荷済 after 取消
  once    返金額 >0円

エラー[E126]: 取消 のあとに 出荷済 に着く手順があります
  --> 注文の状態.rule:37 ステートマシン 注文
   |
37 |   never   出荷済 after 取消
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^
   |
 手順（受付 から）:
   1. 受付 のとき 出来事 = 取消依頼, 支払額 = 0円 → 取消（表 遷移 行2）
   2. 取消 のとき 出来事 = 入金, 支払額 = 0円 → 入金済（表 遷移 行10）
   3. 入金済 のとき 出来事 = 出荷, 支払額 = 0円 → 出荷済（表 遷移 行4）

ステートマシンも書けます。呼び出しの並びまで検査します

注文は入金され、出荷され、配達されるか、取り消されます。こうした手続きの一歩ぶんの規則は、状態とイベントのふつうの表に、machine の節を足して書きます。どの出力が次の呼び出しの状態になるか、案件がどこで始まりどこで終わるか、何が起きてはいけないか（ここでは、取り消した注文が出荷されること）を言う節です。生成する関数は何も覚えず、状態は呼び出す側が持ちます。rulec check は案件がたどれる呼び出しの並びをすべて調べ、崩れた主張を崩す最短の並びで返します。ここで返ってきたのは、取消のあとに届いた入金が注文を入金済に戻してしまう欠陥で、表を一行ずつ読んでも見えません。

$ rulec certificate 運賃.rule > cert.json
$ proofs/.lake/build/bin/rulec-recheck --rule 運賃.rule cert.json
運賃 (0.22.1), re-checked against the Lean proofs
  運賃表: 6 rows — complete, 6 rows reached, no two rows meet, 1 axes tiled
    12 boxes read back from the cells they were written as
  the digest is 運賃.rule's, and 12 cells are read back out of it
OK: every claim this program states was proved, by the theorems of RulecCert.

$ rulec test generated/ --proofs --lang ja
…
ok    fee (Rust, proof) ハーネス 2 本

証明を、rulec の外でもう一度確かめます

rulec certificate が証明の根拠を出し、rulec とコードを共有しない二つのプログラムがそれを確かめ直します。依存の無い Python のファイル一つと、Lean 4 で書いた検査です。Lean の側では、検査が通れば主張が成り立つことを定理として証明しています。生成した Rust はモデル検査器の Kani にかけ、宣言した範囲のすべての入力について、どの表でも当てはまる行が見つかること、オーバーフローしないことを確かめます。

source 機構 = file "sources/nenkin/R08ryougaku.xlsx" sha256:462a199ad4f3b69c
  表1 sha256:09a23ce9620373c4

table 等級(grade)  @機構 表1  # 保険料額表の 1〜32 等級をそのまま転記した
policy unique
| 報酬月額             | -> 標準報酬月額(std) : money[円] |
| <93000円             | 88000円                          |
| >=93000円 <101000円  | 98000円                          |
| >=101000円 <107000円 | 104000円                         |
…

出典を引用して、コピーを固定します

日本年金機構の保険料額表（Excel のブック）を source で宣言し、表を @機構 表1 と引用します。コピーは rulec source fetch が規則の隣に保存し、rulec source pin がハッシュで固定します。以後、行はそのコピーと突き合わされるので、金額を一桁間違えたら落ちます。コピーにあるのにどの行も使っていない値は W120 として出るので、同じ打ち間違いを反対側からも見つけられます。法令なら条文を @法 別表第一 と引用して、e-Gov 法令検索の条文のコピーに固定でき、改正されれば読み直す行が名指しされます。

人が読むページ。左の入力欄に例 2（東京都、1999g、12000円、プラチナ）が入り、送料 = 400円 と、生成コードがログに書く一行が出ている。右では、基本送料の行 3（遠隔地以外、2000g 以下）と 負担判定の行 2（プラチナ）に色が付いている 人が読むページ。左の入力欄に例 2（東京都、1999g、12000円、プラチナ）が入り、送料 = 400円 と、生成コードがログに書く一行が出ている。右では、基本送料の行 3（遠隔地以外、2000g 以下）と 負担判定の行 2（プラチナ）に色が付いている

人が読むページが出ます

rulec doc --format html が、ルールを一枚のページにします。読む人が自分の件を入れると、当てはまった行に色が付き、答えが出ます。動いているのは生成した JavaScript そのものなので、ページがコードと違うことを言うことはありません。転記元の表と規則の表を並べた、人が読む資料も、顧客向けの案内も、同じルールから出ます。

if dest in _近畿圏 and size == SizeClass.S60:    # 行1
    fee = 990
elif dest in _近畿圏 and size == SizeClass.S80:  # 行2
    fee = 1210
...
else:
    raise AssertionError("到達不能: 完全性は rulec が静的に検査済み")

12 の言語に、依存ゼロで出ます

Python・TypeScript・JavaScript・Rust・Ruby・PHP・Go・Swift・Java・SQL・Wasm、それに列をまとめて計算する NumPy。行と分岐が一対一で、ランタイムも設定ファイルもありません。関数の隣には _traced が出て、答えと一緒にどの表のどの行で決まったかを返します。ログにも、問い合わせへの返事にも使えます。

生成できる言語は 12、診断は 112 種類。規則 87 本（うち 34 本は、公開されている規約や法令などからの転記）を、毎コミットで検査し、生成し、実行しています。依存ゼロ、ランタイム無し、バイナリは 1 本、検査はオフライン。

手元にあるものから始める

三つとも、いま動いているものは変えません。

手元にあるもの 最初の一手 コマンド
Excel か、公開されている規約か、法令 .rule に転記して検査にかけます。Excel ならブックをそのまま読んで下書きが起こせて、推定した箇所には印が付きます。法令や文書は引用して、コピーを取っておきます。データも、いま動いている実装も要りません rulec import xlsx のあと rulec check（何を証明するか）
いま動いている実装 .rule に書き起こし、いまのコードを短いアダプタで包みます。verify が、ルールの境界から作ったケースを両方に流して、食い違うところを「どの行に当てはまったか」ごとにまとめて返します。動いているコードには触りません rulec verify（突き合わせと再生）
過去の記録 ルールを記録に当てて再生します。改定なら、何件がいくら動くかが入れる前に出ます。そもそもどの入力が動くかは、記録が無くても二つの版だけで出ます rulec fixtures lint のあと rulec replay か rulec diff（突き合わせと再生）

誰が書くか — 人とエージェントと rulec

いまはルールが Excel か、規約の PDF か、Wiki のページか、誰かの頭の中にあって、エンジニアが if の連なりに書き直しています。rulec はその書き直しをエージェントに任せ、エージェントが返してくるものを変えます。コードではなく、人が読めるルールです。

エージェントがルールを書き、rulec が証明して直し方を返し、決められないことだけを人が決める。出てくるのは証明済みのルールから生成したコードと、入れる前に分かる影響

エージェントがルールを書き、rulec が証明して直し方を返し、決められないことだけを人が決める。出てくるのは証明済みのルールから生成したコードと、入れる前に分かる影響

青はエージェントと rulec のあいだのループで、人は出てきません。エージェントがルールを渡し、rulec がおかしいところ（場所、直し方、それを起こす入力）を返し、エージェントが直してまた渡します。山吹色は人を通る回り道です。人が訊かれるのは出典から決められないことだけで、「山梨県あての S60 の運賃はいくらですか」のような質問に、金額や丸めの向きで答えます。コードは一行も見ません。人が読んで確かめるのは、ルールから出した資料と、自分の件を入れて試せるページです。

エージェント側の手順はエージェント向けにあります。エージェントスキルはリポジトリに入っていて（手順）、シェルの無い環境では rulec mcp が同じコマンドをツールとして出します（手順）。指摘は JSON で返り、診断コードと JSON の形は文面が良くなっても変わりません。

何が証明され、何がされないか

同じ計算が三つの欠陥を決める。抜け（E101）はどの行も覆っていない範囲、重なり（E105）は二つの行が同じ範囲を覆っていること、当てはまらない行（E102）は先の行がその行の範囲を先に全部取ること。表はどれも同じで、違うのは一箇所だけ 同じ計算が三つの欠陥を決める。抜け（E101）はどの行も覆っていない範囲、重なり（E105）は二つの行が同じ範囲を覆っていること、当てはまらない行（E102）は先の行がその行の範囲を先に全部取ること。表はどれも同じで、違うのは一箇所だけ

七つが、生成の前に片づきます。五つは静的に証明（どの入力もどれかの行に当たる、二つの行に当たる入力は無い、当たらない行は無い、単位は混ざらない、途中の値は int64 に収まる）、一つは宣言の要求（端数の決め方）、一つは実行（例が全部通る）。どれか一つでも示せなければ、何も生成しません。

証明していないことのほうが大事です。ルールが現実と合っているか、生成コードがルールと同じ答えを返すか（生成したどの言語でもバイト単位でテストしていますが、証明ではありません）、重なりの証明が届かなかった行の対、検査器そのものが正しいか。どこまで届いていてどこで止まるかは、何を証明するかと確かめ方にあります。

書けること、書けないこと

一件の取引を、そのままの値から一度で判定するルールです。答えは金額、可否、区分、順序のどれかです。運賃、割引、料率、適用の可否、区分、振り分け、法令の規定がこの形をしています。お金が出てこないルールも書けます。

この言語には親が二つあります。条件を表に書く形は決定表（DMN）から、本則と特例、ただし書は、法令を論理で書く試み（Catala）から来ています。持たないのは、再帰、状態、日付の計算、ネストしたオブジェクト、そして二つの列をまたぐセルです。これを持たないから、どの検査も必ず答えが出ます。セルは自分の列しか狭めないので、一行が一つの区画になり、区画どうしに隙間や重なりがあるかを計算で厳密に決められます。重量 × 10 > 注文金額 はセルに書けませんが、derive か define で名前を付ければ、一つの列になります。

自分のルールが入るかは、五つの問いと、DMN・ルールエンジン・Catala との違いと一緒に、自分のルールが入るかにまとめてあります。

次に読むもの

ページ 書いてあること
ルール(.rule)を書く 一つの表から、特例、ただし書、明細の並びまで
何を証明するか 七つの検査と、診断の読み方
生成して呼ぶ 12 の生成先と、ルールを MCP のツールやサービスとして出すこと
突き合わせと再生 いま動いているもの、過去の記録との突き合わせ
立場ごとの使い方 公開されたルール、手元のルール、新しいルール、API の契約
例で見る 運賃表、規約、法令から転記したルール
自分のルールが入るか 五つの問いと、似たもの