技術的概要：認知ワークフロー実行器のための認証済み純粋性

1. 課題：認知ワークフローにおける純粋性のギャップ

認知ワークフローシステム（AI 推論、ツールの使用、推論を調整する）は、高リスクドメインにおいてますます運用されています。先行研究（McCann [2026e]）は、ガバナンス完全性、出所完全性、および管理されていない効果の不可能性を保証する 3 層ガバナンスアーキテクチャを確立しました。しかし、これらの安全性定理は、実行器モジュールが I/O 効果を実行できず、宣言的指示のみを返すことを要求する重要な前提、すなわち純粋モジュール制約に依存していました。

以前の実装では、この制約は BEAM 仮想マシン（Erlang/OTP）上での静的モジュールインポートグラフ分析によって強制されていました。慣習に基づくガバナンスよりも強力ですが、このメカニズムは敵対的な回避に対しては不十分です。BEAM の動的機能により、静的分析では確実に防止できない 5 つの明確な回避クラスが存在します：

1. 動的ディスパッチ： :erlang.apply/3 を使用して、静的インポートなしで任意の関数を呼び出す。
2. コード評価：Code.eval_string/1 を使用して、実行時に任意のコードを実行する。
3. ネイティブ実装関数（NIFs）：制限のないシステムアクセスを持つ共有ライブラリをロードする。
4. ポート： :erlang.open_port/2 を通じて外部プロセスを生成する。
5. 動的モジュールロード： :code.load_binary/3 を通じて実行時に任意のバイトコードをロードする。

ライス（Rice）の定理により、「I/O 効果がない」という非自明な意味論的性質を、すべての可能なプログラムに対して決定する静的分析は存在しません。健全な過大評価（overapproximation）は、正当な慣習的な Elixir コードの大部分を拒否することになります。これにより純粋性のギャップが生じます：形式的モデルは純粋性を仮定しますが、強制メカニズム（静的分析）は、意図的な敵対者に対して構造的にそれを保証できません。

2. 手法：検出から構造的防止へ

本論文は、純粋モジュール制約を分析によって強制される慣習から、実行環境によって強制される構造的機能境界へと変換する認証済み純粋性アーキテクチャを提案します。この手法は、4 つの中核メカニズムに依存します：

A. 制限されたコンパイルターゲット（WebAssembly）

実行器は、制限された**WebAssembly（WASM）**ターゲットにコンパイルされます。WASM の機能モデルを活用して、上記の 5 つの BEAM 回避クラスを構造的に排除します：

• 動的ディスパッチなし：WASM には、実行時の文字列/アトム名で関数呼び出しを解決する命令が存在しません。呼び出しは、関数テーブル内の静的インデックスに制限されます。
• コード評価なし：WASM は事前にコンパイルされたバイトコードを実行します。実行時に新しいコードを生成またはロードするメカニズムは存在しません。
• NIFs/ポートなし：WASM モジュールは、ホストのファイルシステム、共有ライブラリ、またはプロセス生成へのアクセスがないサンドボックス化された VM 内で実行されます。
• 動的ロードなし：モジュールのインスタンス化はホストによって完全に制御されます。モジュールは他のモジュールをロードできません。

B. ホスト関数ホワイトリスト（$W$）

WASM モジュールは、インポートセクションで明示的に宣言された関数のみ呼び出すことができます。これらのインポートは、有限で列挙された**ホワイトリスト（$W$）**に制限されます：

• $W_{data}$：純粋なデータ操作（メモリ管理、文字列操作、算術、JSON シリアライズ、コンテキスト読み取り）。
• $W_{dir}$：指示コンストラクタ（意図された効果を表すデータ構造を構築する関数、例：directive_http_request。ただし、それらを実行するものではありません）。
• 除外：効果機能を与える WASI（WebAssembly System Interface）インポートは明示的に除外されます。

C. 純粋性証明書

純粋性証明書は、実行器バイナリをその純粋性分類に結びつける暗号学的証明アーティファクトです。

• 構造：実行器バイナリの SHA-256 ハッシュ、純粋性証明（インポートリスト＋分類）のハッシュ、およびこれらのハッシュに対するEd25519 署名を含みます。
• 完全性：SHA-256 の衝突耐性と Ed25519 の不可偽性により、証明書は変更されたアーティファクトに転送できません。

D. 実行時検証ゲート

実行器がガバナンスパイプラインに入る前に、検証ゲートが以下の処理を実行します：

1. 署名検証：Ed25519 署名を検証します。
2. アーティファクト結合：バイナリハッシュが証明書と一致することを確認します。
3. 独立した証明導出：WASM バイナリのインポートセクションを de novo（改めて）解析し、現在のホワイトリストに対して主張された純粋性証明と一致することを確認します。
4. 分類検証：すべてのインポートが純粋として分類されていることを確認します。

このゲートを通過した実行器のみがインスタンス化されます。このゲートは構造的な前提条件として機能し、有効な純粋性証明書を持たない実行器が実行されないことを保証します。

3. 主要な貢献

1. 形式的脅威モデル：この文脈における 5 つの BEAM 回避クラスと静的分析の理論的限界（ライス定理）の厳密な特徴付け。
2. 構築による構造的純粋性：制限された WASM ターゲットへのコンパイルが、実行器のコード内容とは無関係に、純粋モジュール制約を構築によって満たすことの証明（定理 4.5）。
3. 回避の排除：制限された WASM 環境において、5 つの BEAM 回避クラスそれぞれが構造的に不可能であることを示す形式的証明（定理 5.5）。
4. 暗号学的アテステーション：ソースコードへのアクセスなしに実行器の純粋性を組織間間で携帯可能に検証可能にする、純粋性証明書と遠隔アテステーション記録の方式。
5. 信頼計算基盤（TCB）の定義：保証に必要な 5 つのコンポーネント（WASM ランタイム、ホスト関数、ホワイトリスト、検証ゲート、指示インタプリタ）の明示的な定義。信頼対象を無制限の実行器コードから、限定され監査可能なセットへ縮小。
6. 段階的信頼ティア：段階的な導入を可能にする、3 つのティア（検証済み純粋性、静的分析、実験的）をサポートする実装アーキテクチャ。

4. 結果と評価

このアーキテクチャは、Apple M シリーズプロセッサ上で Wasmtime JIT バックエンドを実行する、4 つの実装済み実行器（Rust ベース、WASM コンパイル）で評価されました。

• 検証レイテンシ：検証ゲートは、本番環境の実行器に対して39–42 µs（中央値）を要します。ハッシュベースのキャッシングにより、繰り返し呼び出しにおける償却コストはゼロに近づきます。
• 実行時オーバーヘッド：完全なプランサイクル（インスタンス化、実行、逆シリアライズ）は256–398 µsで完了します。これは 100 ms の HTTP リクエストに対して**<0.4%、典型的な 800 ms の LLM 呼び出しに対して<0.05%**のオーバーヘッドを表します。
• 決定性：同一の入力による 40 回の繰り返し呼び出しで、WASM 実行環境の決定性を確認し、ゼロの乖離が観測されました。
• 証明書サイズ：証明書はコンパクト（約 1.3 KB）であり、帯域幅の予算内に十分収まります。
• 正しさ：すべての実行器は期待される指示形状を生成し、システムは実行間でバイト同一の出力を維持しました。

5. 意義と主張

本論文は、ガバナンス保証の認識論的ステータスにおける根本的な転換を主張します：

• 検出から防止へ：従来のアプローチは、静的分析による既知の回避パターンの検出に依存していました。このアーキテクチャは、効果を生み出す機能を構造的に欠如させることで、回避を防止します。
• 既存定理の強化：McCann [2026e] の安全性定理（ガバナンス完全性、出所完全性、管理されていない効果の不存在）は形式的に同一のままです。しかし、それらの基礎的前提は、静的分析の限界ではなく、WASM 機能モデルと暗号学的プリミティブ（SHA-256、Ed25519）の数学的性質に基づいて機械的に解消されます。
• 携帯可能な信頼：ローカルの純粋性証明を携帯可能なアテステーション記録に変換することで、このアーキテクチャは組織間ガバナンスの構成を可能にし、組織 A が組織 B の実行器の純粋性をソースコードレビューなしに暗号学的に検証できるようにします。

本論文は、これは Rocq や Lean の意味での機械化された証明（これは併行論文で基礎ガバナンス論理に予約されています）ではなく、実行時に検証される構造的保証であると明示的に述べています。貢献は、信頼対象を「すべての実行器コード」から、小さく明示的に定義された**信頼計算基盤（TCB）**へ縮小することにあります。