MysticIR Federation v0.8.5

MysticIR Federation v0.8.5 とは Overview

MysticIR Federation v0.8.5 では、見た目が異なる2つの「言語」が、代表的な失敗ケースにおいて同じ Core AST に正規化され、同じ CEK trace と error signature に到達することを確認しました。

これは「完全証明」ではなく、プロトタイプ・検証デモです。表面の記号が違っても、Core AST に変換された時点で区別がつかなくなり、そのまま同じ CEK machine を動き、同じ場所で同じエラーを起こします。

MysticIR Federation v0.8.5 では、異なる表面言語が同じ Core AST、同じ CEK trace、同じ error signature に到達することを代表ケースで確認しました。

下の2つは、同じ意味のプログラムです。片方は 💩 系の記号（ScatLang）、もう片方は 🌊 系の記号（SeaIR）で書かれています。

💩 ScatLang

x ← 💩×3 ⊛ 💩₀

🚽⇐ missing

⟳ 💩₀ ≠ 💩⁺(💩₀) {
  x ← 💩₀
}

💩₀ = ゼロ、💩×N = N、⊛ = mod、← = 代入

🌊 SeaIR

x ⚓ 🌊×3 ⚫ 🌊

🏝️ missing

🌀 🌊 ≠ 〰️🌊 {
  x ⚓ 🌊
}

🌊 = ゼロ、🌊×N = N、⚫ = mod、⚓ = 代入

記号は違いますが、パーサー層で正規化され、この代表ケースでは同じ Core AST が生成されます。その後の比較では、表面ラベルを除いた trace と error が一致します。

ScatLang と SeaIR の表面記号を、同じパーサー層で同じ Core AST に正規化します。その後は、この代表ケースでは同じ経路を通ります。

💩 ScatLang

表面パーサー

🌊 SeaIR

表面パーサー

Core AST

両者が同じ木構造に変換される

CEK Machine / Trace

同じ step 列、同じ continuation

Error Federation

同じ error signature（frontend ラベルを除く）

フロントエンドのラベル（💩ScatLang / 🌊SeaIR）は trace に残るので、表面の違いは証拠として残しつつ、地下では同一である、という状態が作れます。

以下は Python スクリプトを実行して得られた実際の結果です。今回用意した3つの代表ケースでは trace_equal・error_equal = true、surface_diff = true が確認されました。

ケース	error type	trace_equal	error_equal	surface_diff	steps（両者）
mod by zero 3 ⊛ 0 → ゼロ除算	ScatError	✓ true	✓ true	✓ true	12 == 12
unbound variable 未定義変数 missing を参照	ScatError	✓ true	✓ true	✓ true	2 == 2
step limit / infinite loop 0≠1 が永遠に true → step 40 で打ち切り	StepLimitError	✓ true	✓ true	✓ true	40 == 40

※ steps が一致するのは、今回の代表ケースで両表面記号が同じ Core AST に正規化され、CEK machine が同じ step 数で進んだためです。

✓ trace_equal

CEK machine が踏んだ「ステップ列の記録」を、フロントエンドのラベルを外して比べたとき、この代表ケースで ScatLang と SeaIR が一致したら true。
同じ実行経路として扱えることを示します。

✓ error_equal

エラーが起きた瞬間の「状態の指紋」を、フロントエンドラベルを外して比べたとき、両者が一致したら true。
同じ場所で転んだ証拠。

✓ surface_diff

フロントエンドのラベルを付けたまま比べると、💩ScatLang と 🌊SeaIR の違いが残って不一致になる = true。
表面の違いは記録に残る証拠。

3つがすべて true のとき、「表面は違う、地下配管は同じ」という Federation の主張が、そのケースで確認できた、ということになります。

MysticIR Federation v0.8.5 は「増やす」作業ではなく、発表に使える固定版に整えることを目的としたプロトタイプです。

3つの代表的な失敗ケース（ゼロ除算・未束縛変数・無限ループ）すべてで、ScatLang と SeaIR が同じ CEK trace・同じ error signature に到達することが確認できました。

🔧 実行コマンド: python mysticir_federation_v085.py — 同じフォルダに mysticir_v085_error_federation_report.json が生成されます。