モダナイゼーションの検証

English: Modernisation verification

モダナイゼーションの変更は、「意図したことだけを行い、それ以外は変わらない」という根拠があって初めて信頼できます。 Kurahi Industrialはこれを実行によって確認します。元のプログラム（ベースライン）と変更後のプログラム（候補）を凍結したスナップショットからコンパイルし、同じ入力で実行し、出力を決定的なルールで比較します。判定に言語モデルは関与しません。

2026年11月1日時点の状況：R1の範囲（KIMS-010、013、014、015、017）。次のIndustrialリリースに向けたブランチにあります。

示すこと、示さないこと

判定が示すこと	示さないこと
使用したソーススナップショット（全ファイルのSHA-256）、コンパイラ、フラグ、フィクスチャ、比較器、制限	フィクスチャが通らない入力に対して候補が正しいこと
各側がそのフィクスチャで出力・書き込み・終了コードとして返したもの、および出力の差異	業務ルールが完全に復元されたこと、説明が正しいこと
すべての差異が承認済みの変更仕様でカバーされていること（PASS）、またはカバーされていない差異（FAIL）	本番プラットフォーム（z/OS、EBCDIC、CICS、Db2、VSAM、JCLのリスタート）での動作
署名後に記録が改ざんされていないこと（`kurahi evidence verify`）	性能、並行性、本番相当の負荷での動作

署名付きエビデンスは「何が実行されたか」の改ざん検知可能な記録です。テストしたフィクスチャを超えて意味的な正しさを証明するものではありません。FORTRANのフィクスチャがその例です。単精度化という回帰は、あるローンの返済額は変えますが別のローンでは変えません。2つ目のローンを含まないフィクスチャであれば、PASSと報告されていました。

対応言語とツールチェーン

言語	ツールチェーン	実行
COBOL	GnuCOBOL `cobc -x`（3.1.2で確認）	あり。方言（`-std=`）とフラグは記録され、スナップショットとポリシーの識別子に含まれます。コピーブックのフォルダは `-I` で渡します。
FORTRAN	`gfortran`（13.3で確認）	あり。全ソースを1回で、`program` ユニットを先頭にコンパイルします。
PL/I	なし	実行なし。解析は動作します（`modernise_inventory kind pli`）。実行は `NOT_RUN_COMPILER_UNAVAILABLE` と報告します。

GnuCOBOLはIBM Enterprise COBOLではありません。方言オプションで差は縮まりますが、なくなりません（EBCDIC、 COMP のバイト順、コンパイラ固有の切り捨て）。GnuCOBOLでのPASSはGnuCOBOLについての根拠です。

実行の流れ

ランナーの契約は prepare → execute_baseline → execute_candidate → compare → report です。

スナップショット。 両フォルダをプロジェクトのデータ領域にコンテンツアドレスで凍結します。各ファイルの SHA-256、サイズ、観測した文字コード（ascii、utf-8、unknown-8bit、binary）と改行（lf、crlf、 cr、mixed）、さらにツールチェーンの識別情報（コンパイラのパス、バージョン行、バイナリのSHA-256、方言、フラグ）を記録します。スナップショットIDはこのマニフェストのSHA-256なので、同じ内容なら同じID、どんな変更でも新しいIDになります。オブジェクトは一度だけ書き込まれ、上書きされません。シンボリックリンクはたどらず、 output/ と隠しフォルダは対象外です。
準備。 両スナップショットを再ハッシュし、言語とコンパイラを決定し、フィクスチャを読み込んでダイジェストを取ります。ビルドはライブのフォルダではなく、常にスナップショットストアから行います。
実行。 各側を専用のスクラッチフォルダでコンパイルし、フィクスチャのケースごとに実行します（ベースラインは再現性を確認するため既定で2回）。終了コード、標準出力、標準エラー、プログラムが作成・変更したすべてのファイルを取得します。
比較。 ベースラインの出力は、ケースのゴールデン出力と一致し、実行間でも一致しなければなりません。そのうえで各出力を比較器で比較します。
報告。 判定、所見、ダイジェスト、制限を署名付きエビデンスとして封印します。

フィクスチャ

フィクスチャフォルダには、ケースごとに1つのサブフォルダを置きます。

fixtures/
  week-01/
    stdin          任意：標準入力
    args           任意：1行に1つの引数
    files/         実行フォルダに置く入力ファイル
    golden/        ベースラインが正確に再現すべき出力（stdout、exit、PAYOUT.DAT など）

比較器と変更仕様

変更仕様がない場合、すべての出力をバイト単位で比較し、差異はすべて回帰とみなします。変更仕様（JSON）では出力ごとの比較器と、承認済みの意図した差異を宣言します。

比較器	用途
`exact`（既定）	バイト
`text`	レコード（行）。CRLFとLFは同じ区切り。`trimTrailing` は任意
`fields`	レコードごとの固定位置フィールド（行、またはバイナリファイルでは `recordLength`）：`text`、`decimal`（表示形式：符号の前置・後置、小数点または暗黙の `scale`、CR/DB）、`packed`（COMP-3）。`tolerance` は明示的に指定し、既定は `0`。`signedZero: "equal"` としない限り `-0` と `+0` は異なるものとします。宣言したフィールド以外のバイトは完全一致で比較します。

意図した差異の項目は対象の出力を指定し、フィクスチャ、フィールド、レコードキー（keyField）、レコード番号で絞り込めます。候補が出力すべき正確な expected 出力も指定できます。各差異は次のように分類されます。

EQUIVALENT：比較器のもとで差異なし。
INTENDED_CHANGE：意図した差異の項目でカバーされ、expected があればそれと一致する。
REGRESSION：それ以外の差異。カバーされたフィールドの変更でも、承認済みの期待出力にならない場合を含みます。

変更仕様（期待出力のダイジェストを含む）はレポートと承認スコープにハッシュとして含まれるため、許容誤差や意図した差異は変更と一緒に承認されます。

判定

判定	条件
`PASS`	両側がビルドでき、すべてのフィクスチャが実行され、ベースラインが安定し、すべての差異が承認済みの意図した変更である
`FAIL`	回帰がある、または候補がビルドできない
`INCONCLUSIVE`	ベースラインがビルドできない、再現しない、ゴールデン出力と一致しない。出力が上限に達した。意図した変更がどのフィクスチャでも実行されなかった
`NOT_RUN_COMPILER_UNAVAILABLE`	その言語のコンパイラがない（この環境のPL/Iは常にこれ）
`NOT_RUN_NO_FIXTURES`	フィクスチャのケースがない
`TIMEOUT`	コンパイルまたは実行が時間制限を超えた
`CANCELLED`	実行が中断された（プロセスグループを終了）

コンパイラなし、フィクスチャなし、タイムアウト、キャンセルがPASSと報告されることはなく、いずれの場合も署名付きエビデンスを生成します。

分離のレベル

誤解のないよう、そのまま記載します。

コンパイルと実行は毎回、OSの一時ディレクトリ配下の新しいスクラッチフォルダで行い、終了後に削除します。
環境変数は固定の最小限です：LC_ALL=C、TZ=UTC。何も継承しません（コンパイル時のみツールチェーンへの PATH を渡します）。
実時間のタイムアウト（既定60秒）と出力の上限（既定でストリームまたはファイルごとに4 MiB）。タイムアウト、上限超過、キャンセル時はプロセスグループ全体を終了します。
prlimit がある場合：実行時にCPU秒、ファイルサイズ、オープンファイル数を制限します。
非特権ユーザー名前空間が使える場合（unshare -rn）：実行は空のネットワーク名前空間で行われ、ネットワークに到達できません。使えない場合、レポートには network NOT isolated と記載されます。
コンテナや仮想マシンではありません。プログラムは同じOSユーザーとして動作し、そのユーザーが読めるものは読めます。この方法で実行するのは信頼できるソースまたは合成ソースに限るか、Kurahi自体をコンテナで動かしてください。

各レポートには、実際に適用された分離レベルが記録されます。

変更ケースと承認

変更ケースは、ベースラインのスナップショット、候補のスナップショット、変更仕様、検証ポリシー、フィクスチャのダイジェスト、テスト実行を承認に結び付けます。KIMS仕様の状態遷移（DRAFT → SNAPSHOT_FROZEN → … → TEST_REVIEW → APPROVAL_PENDING → APPROVED_FOR_HANDOFF → EXPORTED、および BLOCKED、FAILED、 CANCELLED、REJECTED、RECONCILIATION_REQUIRED）に従い、それ以外の遷移は拒否します。

承認には有効な PASS の実行が必要です。承認者は承認者ロールを持ち、ケースの所有者や承認の依頼者であってはなりません。
承認には、ベースライン、候補、変更仕様、ポリシー、フィクスチャ、テスト実行レポートにわたるスコープハッシュが保存されます。新しい候補、変更仕様、ポリシー、フィクスチャのいずれかで承認とテスト実行は無効になり、ケースは CHANGE_PROPOSED に戻ります。
引き渡し時に承認を再確認します：有効であること、期限切れでないこと、スコープハッシュが現在のケースと一致すること、スナップショットが無傷であること、ライブの候補フォルダが凍結時から変わっていないこと。古くなった承認は無効化され、引き渡しは拒否されます。
R1の最上位の状態は APPROVED_FOR_HANDOFF です。EXPORTED は引き渡しマニフェスト（deployed: false）を書き出すだけで、Kurahiはデプロイしません。デプロイには独自の承認とエビデンスが必要です。

承認、却下、無効化、終端への遷移、引き渡しはそれぞれ、ケース配下に署名付きエビデンスとして封印されます。

使い方

Industrialプロジェクトのエージェントツールとして（コンパイルしたプログラムを実行するため、実行 Act モードのみ。パスはプロジェクトフォルダ内に限ります）：

modernise_verify baseline=src/v1 candidate=src/v2 fixtures=tests/payroll change_spec=specs/CHG-001.json

コマンドラインから：

kurahi legacy verify \
  --baseline test/fixtures/modernisation/cobol-payroll/baseline \
  --candidate test/fixtures/modernisation/cobol-payroll/candidate-threshold \
  --fixtures test/fixtures/modernisation/cobol-payroll/fixtures \
  --change-spec test/fixtures/modernisation/cobol-payroll/change-spec-chg001.json

オプション：--entry、--dialect、--flag、--timeout、--project <id>（そのプロジェクトのデータ領域に保存）または --data <dir>、--json。終了コードが0になるのはPASSのときだけです。

スナップショット、実行、ケースはプロジェクトのデータ領域（<KOLO_HOME>/projects/<id>/modernisation/）に保存され、ソースフォルダには書き込みません。

エビデンスのオフライン検証

各実行ディレクトリは標準のエビデンスバンドルです：events.jsonl（ハッシュチェーン）、manifest.json （Ed25519署名、全ファイルのSHA-256）、report.json、REPORT.md、2つのスナップショットマニフェスト、変更仕様、取得した出力（1 MiBを超える出力はバンドルにコピーせず、SHA-256を report.json に記録し、省略をイベントに記載します）。

kurahi evidence verify <run-dir> --trust-key <keyId>

--trust-key なしでは、バンドルが内部的に一貫し、記載された鍵で署名されていることを確認します。--trust-key ありでは、さらにその鍵が信頼する鍵であることを要求するため、編集して別の鍵で再署名したバンドルは失敗します。取得した出力、レポート、マニフェストのいずれを改変しても検証は失敗します。

合成フィクスチャ

test/fixtures/modernisation/ には、Kurahiのために作成した合成プログラム（MIT）があります。

cobol-payroll：コピーブック、COMP-3パック10進数、ROUNDED、符号付き調整額、88レベルを含む給与計算。2つのケース（week-01、ゼロと負のゼロを扱う edge-zero）とゴールデン出力。candidate-threshold（CHG-001：残業の閾値を40.0時間から45.0時間へ。change-spec-chg001.json と期待出力つき）と candidate-regression（CHG-001に加え、税計算から ROUNDED を削除）。
fortran-loan：外部の返済額関数を持つローン償還。candidate-equivalent（リファクタリング）と candidate-regression（割引係数を単精度で計算）。
pli-payroll：%INCLUDE を含むPL/I。解析と NOT_RUN_COMPILER_UNAVAILABLE の確認用。

これらのフィクスチャを実際のツールチェーンで実行した結果：CHG-001 → PASS（意図した出力3件、同等7件）。回帰候補 → FAIL（レコードE00001の税額179.56 → 179.55）。FORTRANのリファクタリング → PASS。FORTRANの回帰 → loan-b のみでFAIL。 PL/I → NOT_RUN_COMPILER_UNAVAILABLE。