実験ノート：COBOLのモダナイゼーション with Opus4.6(その3):Proof Carryingな変換を試行
【注意】著者はCOBOLの言語仕様をしらない、これはあくまでClaude Codeの能力を測るためである。
前記事にて、COBOLを型安全なシステムでモダナイゼーションするやり方を試行した。
型安全性を謳う割には、あんまり、形式的なアプローチではないなということでちょっと工夫してみた。
Proof carryingな変換をClaude Code(on the web)にお願いした
前回までの成果物を、Githubに載せて、Claude Code on the webから以下の指示をだした。モデルはOpus4.6
この、cobolのモダナイゼーションのPOCを参考に、proof carryingすなわち、なんらかの制約や性質を元のCOBOLプログラムに対して定義して、これがモダナイゼーション後にも保たれるような、仕組みにしたい、
さすがに、初期立ち上げはコードを理解するところからスタートし、計画を立ててくれた。
コードベースを、「完全に理解した」、さすが、Opus4.6、そうそうプロパティを定義して、プロパティが成立することを確認する。最後にCirtifcateを作るってのは気づかなかったな。
そして、コードを生成し、テストを開始。一部失敗しているが
どうも、このFAILは、proof carryingの仕組みからして、正しい振る舞いだった模様。やったね！
というわけで完成。
事前に定義できる、プロパティ定義の種類は、８カテゴリ
まあ、なんか、形式的なプログラム検証の枠組みではおなじみの面々かな。
そして、デモ（ローン計算）でのプロパティは、
proof-carrying-modernization.md
最後に、proof-carrying-modernization.mdにサマリを作ってもらった。新たに作られたproperties.tsには、プロパティ定義のDSLも定義されているのか。
全体のシステム構成はこのようになっておる。うまいこと元のシステムにProof Carryingの仕組みが差し込まれている。
┌─────────────────────────────────────────────────────────────────┐
│ Proof-Carrying Flow │
│ │
│ ┌───────────────┐ ┌──────────────────┐ │
│ │ COBOL Source │ │ Property │ │
│ │ (AST) │ │ Definitions │ │
│ └───────┬───────┘ │ (13 properties) │ │
│ │ └────────┬─────────┘ │
│ v │ │
│ ┌───────────────────┐ │ │
│ │ Instrumented │ │ │
│ │ Interpreter │ │ │
│ │ (type-safe exec) │ │ │
│ └───────┬───────────┘ │ │
│ │ │ │
│ v v │
│ ┌───────────────┐ ┌──────────────────┐ │
│ │ Execution │────>│ Property │ │
│ │ Traces │ │ Verifier │ │
│ │ (186 events) │ │ │ │
│ └───────────────┘ └────────┬─────────┘ │
│ │ │
│ v │
│ ┌──────────────────┐ │
│ │ Proof Certificate │ │
│ │ (VALID/PARTIAL/ │ │
│ │ INVALID) │ │
│ └────────┬─────────┘ │
│ │ │
│ ┌─────────────────┼─────────────────┐ │
│ v v v │
│ ┌──────────────┐ ┌────────────┐ ┌──────────────┐ │
│ │ Code │ │ Cross │ │ Modernized │ │
│ │ Generation │ │ Verification│ │ Code │ │
│ │ (TypeScript) │ │ (多入力) │ │ Re-verify │ │
│ └──────────────┘ └────────────┘ └──────────────┘ │
└─────────────────────────────────────────────────────────────────┘実行例
main.tsがローン計算のテストプログラムであった。これにProof-Carryingのセクションが追加された
プロパティ定義
// ============================================================
// Proof-Carrying: ローン計算プログラムのプロパティ定義
// ============================================================
//
// これらのプロパティはビジネスルールや数学的性質を表現する。
// モダナイゼーション後もこれらが保持されることを保証する。
const loanCalcProperties: PropertySet = {
programId: 'LOAN-CALC',
version: '1.0.0',
createdAt: new Date().toISOString(),
properties: [
// --- ビジネスルール不変条件 ---
{
propertyType: 'data-invariant',
id: 'INV-01',
description: 'WS-TOTAL-INTEREST は常に 0 以上（利息はマイナスにならない）',
targetVar: 'WS-TOTAL-INTEREST',
condition: cmp('>=', varRef('WS-TOTAL-INTEREST'), lit(0)),
checkAt: 'every-assignment',
},
{
propertyType: 'data-invariant',
id: 'INV-02',
description: 'WS-BALANCE は常に 0 以上（残高はマイナスにならない）',
targetVar: 'WS-BALANCE',
condition: cmp('>=', varRef('WS-BALANCE'), lit(0)),
checkAt: 'every-assignment',
},propertiesが定義される。失敗したのはこいつか、
// --- 最終状態の検証 ---
{
propertyType: 'final-state',
id: 'FINAL-01',
description: 'プログラム終了時: WS-STATUS は "HIGH-INT" または "LOW-INT"',
targetVar: 'WS-STATUS',
expectedValue: 'HIGH-INT', // デフォルト入力ではHIGH-INT
},出力は、以下の様に１３個のプロパティが定義される、なるほど。
[data-invariant ] INV-01: WS-TOTAL-INTEREST は常に 0 以上（利息はマイナスにならない）
[data-invariant ] INV-02: WS-BALANCE は常に 0 以上（残高はマイナスにならない）
[data-invariant ] INV-03: WS-MONTHLY-RATE は 1 未満（月利が100%を超えることはない）
[precondition ] PRE-01: CALC-MONTHLY-RATE 呼出前: WS-ANNUAL-RATE > 0
[precondition ] PRE-02: CALC-PAYMENT 呼出前: WS-MONTHLY-RATE > 0
[postcondition ] POST-01: CALC-MONTHLY-RATE 実行後: WS-MONTHLY-RATE > 0
[postcondition ] POST-02: CALC-PAYMENT 実行後: WS-PAYMENT > 0
[relational ] REL-01: CALC-AMORTIZATION 後: WS-PRINCIPAL-AMT + WS-INTEREST-AMT ≈ WS-PAYMENT
[precision ] PREC-01: WS-MONTHLY-RATE は ROUNDED モードで計算されること
[precision ] PREC-02: WS-INTEREST-AMT は ROUNDED モードで計算されること
[loop-bound ] LOOP-01: CALC-AMORTIZATION ループは 12 回で終了する
[final-state ] FINAL-01: プログラム終了時: WS-STATUS は "HIGH-INT" または "LOW-INT"
[output-equivalence ] OUT-01: DISPLAY出力がモダナイゼーション前後で一致すること検証実行
検証実行は実にシンプル。
const verifier = new PropertyVerifier(
tracer.getEvents(),
result.variables,
result.displayOutput
);
const report = verifier.verify(loanCalcProperties);
結果は、
--- Verification Results ---
[PASS] INV-01: WS-TOTAL-INTEREST は常に 0 以上（利息はマイナスにならない）
Invariant held across 12 check points
[PASS] INV-02: WS-BALANCE は常に 0 以上（残高はマイナスにならない）
Invariant held across 13 check points
[PASS] INV-03: WS-MONTHLY-RATE は 1 未満（月利が100%を超えることはない）
Invariant held across 1 check points
[PASS] PRE-01: CALC-MONTHLY-RATE 呼出前: WS-ANNUAL-RATE > 0
Precondition held for 1 call(s) to "CALC-MONTHLY-RATE"
[PASS] PRE-02: CALC-PAYMENT 呼出前: WS-MONTHLY-RATE > 0
Precondition held for 1 call(s) to "CALC-PAYMENT"
[PASS] POST-01: CALC-MONTHLY-RATE 実行後: WS-MONTHLY-RATE > 0
Postcondition held for 1 return(s) from "CALC-MONTHLY-RATE"
[PASS] POST-02: CALC-PAYMENT 実行後: WS-PAYMENT > 0
Postcondition held for 1 return(s) from "CALC-PAYMENT"
[PASS] REL-01: CALC-AMORTIZATION 後: WS-PRINCIPAL-AMT + WS-INTEREST-AMT ≈ WS-PAYMENT
Relational property held across 12 check(s)
[PASS] PREC-01: WS-MONTHLY-RATE は ROUNDED モードで計算されること
Precision property held across 1 arithmetic operation(s)
[PASS] PREC-02: WS-INTEREST-AMT は ROUNDED モードで計算されること
Precision property held across 12 arithmetic operation(s)
[PASS] LOOP-01: CALC-AMORTIZATION ループは 12 回で終了する
Loop bounded: 12 iterations <= 12
[PASS] FINAL-01: プログラム終了時: WS-STATUS は "HIGH-INT" または "LOW-INT"
Final state matches expected value
[PASS] OUT-01: DISPLAY出力がモダナイゼーション前後で一致すること
Collected 14 output line(s) for cross-verification
Summary: 13/13 passed, 0 failed, 0 skippedCertificate生成
// ========================================
// Phase 5: Proof Certificate 生成
// ========================================
console.log('━━━ Phase 5: Generate Proof Certificate ━━━');
const stateMap = new Map<string, string>();
for (const [name, value] of result.variables) {
stateMap.set(name, formatCobolValue(value));
}
const certificate = new ProofCertificateBuilder(
loanCalcProgram.programId,
'TypeScript',
loanCalcProperties,
report
)こちらも結果（一部）は、こうなる。
--- Property Preservation ---
[PASS] INV-01: WS-TOTAL-INTEREST は常に 0 以上（利息はマイナスにならない）
Source: passed, Target: not-verified
Property holds in source (target not yet verified)
[PASS] INV-02: WS-BALANCE は常に 0 以上（残高はマイナスにならない）
Source: passed, Target: not-verified
Property holds in source (target not yet verified)
[PASS] INV-03: WS-MONTHLY-RATE は 1 未満（月利が100%を超えることはない）
Source: passed, Target: not-verified
Property holds in source (target not yet verified)
[PASS] PRE-01: CALC-MONTHLY-RATE 呼出前: WS-ANNUAL-RATE > 0
Source: passed, Target: not-verified
Property holds in source (target not yet verified)
[PASS] PRE-02: CALC-PAYMENT 呼出前: WS-MONTHLY-RATE > 0
Source: passed, Target: not-verified
Property holds in source (target not yet verified)
[PASS] POST-01: CALC-MONTHLY-RATE 実行後: WS-MONTHLY-RATE > 0
Source: passed, Target: not-verified
Property holds in source (target not yet verified)クロス検証（入力をふる）
いろいろ入力を変えて実行するのをクロス検証と言っている模様。
// ========================================
// Phase 6: クロス検証（異なる入力データ）
// ========================================
console.log('━━━ Phase 6: Cross-Verification with Multiple Inputs ━━━');
console.log('');
const testInputs: TestInput[] = [
{
name: 'Low Rate (1%)',
overrides: new Map<string, number | string>([
['WS-ANNUAL-RATE', 1.0],
['WS-PRINCIPAL', 50000],
]),
},
{
name: 'High Rate (8%)',
overrides: new Map<string, number | string>([
['WS-ANNUAL-RATE', 8.0],
['WS-PRINCIPAL', 200000],
]),
},
{
name: 'Small Loan',
overrides: new Map<string, number | string>([
['WS-ANNUAL-RATE', 5.0],
['WS-PRINCIPAL', 10000],
]),
},
];３パターンを試した結果がこちら、Low Rate (1%)と、Small Loan がそれぞれFAILしている。
================================================================
CROSS-VERIFICATION SUITE
================================================================
Program: LOAN-CALC
Test Cases: 4 (default + 3 additional)
All Valid: false
--- Default Input ---
Status: valid
Properties: 13/13 preserved
--- Test: Low Rate (1%) ---
Status: partial
Properties: 12/13 preserved
Failures:
[FAIL] FINAL-01: Final state mismatch
--- Test: High Rate (8%) ---
Status: valid
Properties: 13/13 preserved
--- Test: Small Loan ---
Status: partial
Properties: 12/13 preserved
Failures:
[FAIL] FINAL-01: Final state mismatch
サマリ
最後にサマリがでて、
================================================================
╔═══════════════════════════════════════════════════════════════╗
║ Proof-Carrying Modernization - Summary ║
╠═══════════════════════════════════════════════════════════════╣
║ ║
║ 1. Property Definition (プロパティ定義): ║
║ 13 properties defined across 8 categories ║
║ - Data Invariants, Pre/Post conditions ║
║ - Relational, Precision, Loop Bounds ║
║ - Final State, Output Equivalence ║
║ ║
║ 2. Source Verification (ソース検証): ║
║ 13/13 properties verified on original COBOL ║
║ ║
║ 3. Proof Certificate (証明書): ║
║ Status: VALID ║
║ Preservation Rate: 100.0% ║
║ ║
║ 4. Cross-Verification (クロス検証): ║
║ 3 additional test inputs verified ║
║ All Valid: false ║
║ ║
║ Proof-Carrying Flow: ║
║ COBOL Source ║
║ + Property Definitions ║
║ + Execution Traces ║
║ = Proof Certificate (properties verified) ║
║ | ║
║ v ║
║ Modernized Code ║
║ + Same Property Definitions (carried over) ║
║ + Re-verification against modernized execution ║
║ = Updated Certificate (preservation confirmed) ║
║ ║
╚═══════════════════════════════════════════════════════════════╝今後の発展性
summary.mdの最後に、今後の拡張ポイントが書いてあった。
プロパティの自動推論やLLM連携って面白そうだし、回帰テストってテストベクトルを自動生成する話で、これはこれで、形式化の延長線としては筋がいい気がする。
感想
筆者は、COBOLは知らないが、ここまでモダナイゼーションを試すことができた。何をするというよりも、どうやるかという視点でみると、対象がわからなくても、ある程度できるもんだ。
でも、事前条件とか事後条件とかをプロパティで定義して、これが変換後にも満たされることを証明するしくみだけど、実行トレース依存なので、「証明」とかそういうものにはなってないな。
そういう意味で、容易に想像できる範囲内での実現ってところか、最初のプロンプトからここまで作成したのはOpus4.6の底力なのか。でも、ちょっと、物足らない。
つづく、のか？
成果物をここに供養する。
