見出し画像

実験ノート：COBOLのモダナイゼーション with Opus4.6(その5):Leanによる検証-リベンジ編-

ミトKeY(MeatKey)

2026年2月28日 23:07

前記事では、COBOLの変換に対してleanの証明をつけようとして、Claude Code on the webからLeanをインストールできず、なぜか、強制的にSMTソルバでの検証に回り道をした。

Leanファイルの生成

window環境にleanをインストールして、そこからこのモチーフとなるローン計算に関わる証明をすることにした。Claude Code on the webの前回の続きから、

Lean検証の部分を、別の環境で実施したいので、例題から .leanファイルを生成してほしい。あとlean検証のドキュメントを doc下に作成

出来上がったファイル群はこちら、

LonCalc.leanより、PICに関わるインバリアントがaxiomとして定義されている。

COBOLプログラムに基づくaxioms

LoanCalcProofs.leanより、MONTHRLY-RATEを計算した事後条件として、RATEが正であることのtheoremの例

POST-01 theorem

Verification Stack

検証のアーキテクチャは、COBOLからLean4のファイルを作成しこれを証明する。SMTソルバーとも関係するが、今回は省略。

LocalCalcProofs.leanというが証明したい定理らしい。lakeflle.leanは、プロジェクト全体のビルドに関わる

どうも個別のファイルを lake buildしてゆくらしい。

Foundation.leanの証明

このファイルは、「基盤型: FixedDecimal, BoundedString, PicSpec, loopIterate (終了性証明付き)」ということで、最後"loopIterate_bounded"を証明する。

LocalCalc.lean

「LOAN-CALC の形式化: ProgramState, initialState, 3つのセマンティクス関数, 7つの型制約公理」がかいてあるという。

LocalCalcProofs.lean

「13プロパティの定理と証明 (sorry なし): omega, simp, exact」

一部

証明に使うテクニック集

Omega tactic

ご存じ、simp

その他いろいろ、

Leanのインストール

Leanがインストールされてないから悪いんだろうと、いくつかやってみた

Lean4 Skills

Lean4 Skills for Claudeというのをまず入れてみた。

Claude のpluginみたいなので、Claude Desktopから、Readmeに書いてある手順で、インストール、Desktopなので、以下は、実際とは違うのに注意。

# Add marketplace
/plugin marketplace add cameronfreer/lean4-skills
# Install plugin
/plugin install lean4

Claude Desktopでは、ローカルフォルダを指定して、"+"からプラグインを追加する。

Claude DesktopのCodeの画面から、

「プラグインを管理」画面で、GitHubからマーケットプレースを追加を選び、先ほどの"cameronfreer/lean4-skills"を指定して、から当該プラグインをインストールするｌ

プラグインのインストール

VSCodeからleanをインストール

それから、Leanのホームページあるように、VSCodeのextentionをインストールして、そこから、Leanをインストールした。

Windows版なのに、動くんだろうか？

Claude Desktopから、Claude Codeをローカルで実行

GitHubからcloneしたものを、Leanの部分だけ、windowsのフォルダにコピーし、それをターゲットフォルダにして、ローカルにClaude Codeを実行。

このファイルは、lake用の設定である。内容を呼んで証明を進めてほしい。

windowsへのleanのインストールがうまくいっておらず、いったん中断してインストール。

windows環境にelan, leanをインストールしたので再開

Leanファイルを読みこみ、".lean"をキーにして、Lean4-skillが起動される。"lean4:prove"機能だ。

skill起動開始

Lean4:prove

そして、Leanを見つけることができた。

バージョンが確認できたということで、Leanは無事認識されたが、そのあとのコマンドが、bashのコマンドがことごとくエラーになる。windows環境だとうまくいかないのか。

うむ、なんか動いているようだ。エラーが出ているようである。

Buildした結果、４つの修正が必要というはなしに。

なんか、いろいろ修正して、buildして証明しようとしている、素晴らしい！

勝利宣言

そして、勝利宣言。

VSCodeでleanファイルを開けてみて確かめる。

loopIterate_bounded（loopIterateは高々fuel回実行される）は、証明されたようだ。

POST-01post01_monthly_rate_positiveexact✅ proven

なるほど。個別のtheoremは証明されている。

まとめ

COBOL変換に関して、propertyをLean化して証明を行った。この証明が変換後も保たれていれば、すなわちProof Carryingな言語変換ができたことになる。

今回は、やっとLean4をインストールし、そして、Lean4 Skillを使って、Claude Desktopから、leanをつかったproveをしながら、問題個所を修正するということができた、私はLean言語をよくしらないし、一行も修正してないことに着目。

これは最高のエンターテイメントだ。

成果物、すなわち、修正後のLeanファイルをここに供養する。

いいなと思ったら応援しよう！