クロスドメイン状態保存のための機械化されたファンクタタワー

原文

A Mechanized Functor Tower for Cross-Domain State Preservation — jay-oraclizer (2026-07-21)

この投稿では、クロスドメイン状態の再利用可能な検証基盤に、2つの機械検証された結果を追加します。同期ドメイン間の状態保存マッピングは、恒等写像と合成の下で閉じられており、合成は結合的であるという、すべて機械化された定理として示されています。そして、結合幅は層状のファンクタタワーを形成し、結合されたチェーンを忘却することは自然変換となります。この機械化は、任意のステートマシンに対する汎用的なIsabelle/HOLロケールのセットであるため、その法則は、ブリッジ、ロールアップのイグジット、共有シーケンサー、許可型決済レッグなど、ロケールの義務を果たす任意のドメインで直接再利用可能です。前回のトピックでは、アトミックなクロスドメイン状態同期の安全性と活性を機械化された証明で示しました（アトミックなクロスドメイン状態同期のための機械化された証明）。ここでは、保存マッピングの合成を機械化し、結合幅によってそれらを層状化します。

これが埋めるギャップは実用的なものです。デプロイされたシステムは、ブリッジされ、ミラーリングされ、因果的に結合され、アトミックにバインドされた、様々な強度の状態を保持していますが、今日、その強度はプロトコルがチェックできるものではなく、散文の中に存在しています。製品の解釈では、中心となる定理のペアは、宣言された強度を両面からの受け入れ基準に変えます。有効な状態の場合、資産の宣言された要件以上での処理はモデル化された保存保証を伴い、それ以下では明示的な反例が一般的な保証を排除します。全体を通して、証明されたもの、設計上の解釈であるもの、確立されていないものの間の線は明確に保たれています。

1. 前回の投稿で確立されたこと

以前の投稿では、クロスドメイン資産のステートマシンモデルを固定し、バインド・検証・コミット同期サイクルについて2つのことを証明しました。1つは安全性で、ドメイン間の資産ごとの双方向の保存関係です。もう1つは活性で、ビザンチン合意仮定と明示された公平性仮定の下での、モデルレベルでの決定論的かつ飢餓のない選択です。また、2つのマーカーを残しました。保存マッピングの直接合成は延期され、未解決の問いとして、同期強度の異質性をどのように扱うべきかが問われました。前者は以下で正式に解決され、後者は幅でインデックス付けされた結果として明確化され、運用上の同期強度への洗練は明示的に残されています。1つの語彙の引き継ぎが重要です。すべての遷移は、どの規制アクションがどのアセットに適用されたかという操作ペアによってインデックス付けされます。以前の投稿では、アセットがいくつのドメインに触れるかには依存しませんでしたが、それがこの投稿が追加する次元です。

2. 保存マッピングは圏を形成する

2つのステートマシン間の保存マッピングは、状態に関する関数とアクションに関する関数のペアであり、以前に証明された保存義務に従います。3つの定理により、これらのマッピングに圏の構造が与えられます。

theorem preservation_id:
  assumes "state_machine states actions transition terminal"
  shows "state_preservation states actions transition terminal
                             states actions transition terminal id id"

恒等写像は、任意の整形式マシンをそれ自身にマッピングします。合成は成分ごとにかつ結合的であり、preservation_compose および preservation_assoc として機械化されています。これらを合わせることで、リンクごとの推論が許可されます。ロールアップレッグ、ベースレイヤー、および許可型決済レッグのチェーンにおいて、ロールアップから決済へのマッピングは新たな証明なしに提供され、その義務はリンクから継承され、ホップのグループ化は保証に無関係です。エンドツーエンドの主張はリンクごとの義務に分解されるため、エンドツーエンドのプロパティが失敗した場合、少なくとも1つのリンク義務または合成前提が失敗しています。どれが失敗したかは、分解が整理する診断であり、実行するものではありません。

以前の投稿で、法則が形式的な証明を伴えば、エントリはファンクタのステータスを獲得すると述べましたが、これがその証明です。

合成は異種検証を生き残ります。認証されたインターフェース層は、Merkle形式のコミットメントスキームの下でドメイン状態を交換し、ハッシュインターフェース、状態抽出、マージ操作、および部分ビューに対するブラインディング関係を関連付ける明示的な義務を負います。これらの義務の下で、2つの認証された状態をマージすると、両方の入力を洗練する有効な状態が生成され、有効な状態のブラインドビューは有効なままです。つまり、状態の一部のみを公開するドメイン（一般的なエンタープライズ台帳の姿勢）でも、健全に構成されます。ドメインの独立性は別途チェックされます。これは、規制ドメインとはまったく関係なく、トレース準拠モデルではなく古典的なプロトコルから借用した語彙であるTCPにインスパイアされたエンドポイントライフサイクルに対して同じ義務を果たすことによって行われます。

3. 規制状態遷移ダイナミクス

そのインデックス内の操作は抽象的なラベルではありません。機械化されたインスタンスは、5つの状態、7つのアクション空間、35の構文ペアのうち12の有効な遷移を持つ規制アクションを実行します。一部の遷移は可逆的であり、1つの状態は終端（補題 confiscated_terminal）であり、エスカレーションは方向性があり、escalation_preservation は別の定理ではなく、異種アクションロケール解釈です。この疎性が内容です。すでに没収されたものの差し押さえは法的に無意味であり、モデルはランタイムの慣習に任せるのではなく、遷移関係でそれを拒否します。したがって、保存は具体的なことを意味します。遷移が持つ法的効果はドメイン間の通過後も存続し、凍結された資産は単に制限された状態で反対側に到着するわけではありません。

2つの役割は明確に区別されます。このインスタンスは、1つの具体的なステートマシンの内部一貫性を検証します。法的に異なるアクションが識別可能に表現され続けるという規範的要件は、現在レビュー中のERC-8319（議論）という情報提供ERCの提案に記録されている公開事項です。この機械化はその提案を実装するものではなく、その提案はいかなる特定のステートマシンも義務付けていません。これは、このインスタンスを動機付ける公開分類体系としてのみ引用されています。

obj_step :: "(reg_action × asset_id) ⇒ global_state ⇒ global_state option"

遷移はアクションと安定した資産識別子によってのみインデックス付けされます。次のセクションではその事実に基づいています。

4. ファンクタのタワーとしての同期度

すべてのアセットが同じ強度を必要とするわけではありません。製品の解釈では、スペクトルは単一チェーンの存在から、最終的な調整、因果的一貫性、そして上記の規制アクションの対象となるものを含む最強クラスの完全なアトミックなバインディングまで広がります。機械化は、そのスペクトルの下にある構造を層状化するものであり、運用上の意味そのものではありません。この区別は、続くすべての主張を限定します。

状態空間はチェーン幅によって段階付けされます。各 k について、キャリアは、ハブチェーン0にアンカーされたチェーン 0..k で資産保有がサポートされているグローバル状態を保持し、レベルごとに1つのファンクタを提供します。

definition deg_carrier :: "nat ⇒ global_state set" where
  "deg_carrier k = {gs. ∀c aid. asset_exists gs c aid ⟶ c ≤ k}"

definition F :: "nat ⇒ gobj" where
  "F k = ⟨ obj_states = deg_carrier k, obj_step = deg_step k ⟩"

このインデックスは**結合幅**を形式化します。つまり、アセットの状態がいくつのチェーンにまたがるかを示します。そのレベルを運用階層（観測、因果的実行、アトミックなバインディング、ロールバックセマンティクス）として解釈するには、幅からそれらのセマンティクスへの個別の洗練が必要であり、その洗練はここでは確立されていません。確立されているのは、運用階層がその上に位置する構造です。

隣接するレベル間では、degree_forget (Suc k) は最上位チェーンの保有を削除し、中心となる定理は、このマッピングが自然であるということです。つまり、忘却はすべての規制遷移と可換です。

theorem degree_natural_transformation:
  "natural_transformation (F (Suc k)) (F k) (degree_forget (Suc k))"

${\eta }_{k+1}\circ F_{k+1}(\alpha )=F_k(\alpha )\circ {\eta }_{k+1}$

すべての操作 α = (reg_action, asset_id) について、η マップの合成は再び自然であるため、任意の下位レベルへの射影は、1ステップでも複数ステップでも正当です。

モデルに関する短いトレースとして、チェーン 0..2 上のアセットと、それにインデックス付けされた凍結を考えます。幅2で凍結を適用し、その後チェーン2を忘却することは、最初に忘却してから幅1で適用することと同じ状態になります。したがって、より狭いコンテキストへの射影は、そのコンテキストが認識すべき規制履歴と矛盾しません。遅延、リトライ、メンバーシップ変更を伴うライブイグジットプロトコルは、この法則の候補アプリケーションであり、それだけです。特定のプロトコルがモデルを洗練すると主張するものではありません。

度合いはシステムではなく、アセットに付随します。階層は、コンテキストで固定され、エクスポート時に一般化される任意の割り当て asset_degree :: asset_id ⇒ nat に対してパラメトリックです。これは、以前のスレッドで収束した立場を形式化したものです。同期強度は宣言されるものであり、発見されるものではありません。 製品設計の解釈では、度合いは発行時に宣言されます。定理はいつ宣言されるかについては無知であり、サイクル間の静的な再割り当てをカバーし、ライブサイクル中の変更はモデルの範囲外とし、未解決の問いとして残しています。

製品の解釈では、以下の定理のペアは保守的な両面からの受け入れポリシーをサポートし、この投稿の2番目の見出しとなります。

theorem over_provisioning_guarantees:
  assumes deg: "asset_degree aid ≤ d" and val: "valid_state gs"
  shows "guarantees_preservation d gs aid"

theorem no_downward_safety:
  assumes "asset_degree aid > system_degree"
  shows "¬ (∀gs. guarantees_preservation system_degree gs aid)"

over_provisioning_guarantees は、システム機能が宣言された要件を満たすか超えた場合、有効な状態に対するモデル化された保存保証を確立します。no_downward_safety は、過少供給下ではすべての状態に対する無条件の保証が存続しない理由を示す明示的な反例を提供します。これらを合わせることで、包含関係

$S_3\supseteq S_2\supseteq S_1\supseteq S_0$

は、分類から強制可能な受け入れルールの基礎へと変わります。会場レベルでの受け入れと拒否は、定理の記述そのものではなく、このペアの設計上の結果です。包含表記は製品の解釈に属し、形式層は定理とそれが記述される幅インデックスを提供します。

レベル間の境界も明確にされており、1つの点に注意が必要です。lamport_hb はタイムスタンプ上の厳密な順序として定義されているため、定理が証明するのは、モデルのタイムスタンプ順序が厳密な半順序であるということです。この名前は、メッセージ因果関係の構築を主張することなく、ハプンドビフォーから借用されています。

theorem boundary_well_defined:
  "(causal_consistent_at aid d ⟷ (2 ≤ asset_degree aid ⟶ 2 ≤ d))
   ∧ (asset_degree aid ≤ d ⟶ causal_consistent_at aid d)
   ∧ (∀t1 t2. lamport_hb t1 t2 ⟶ ¬ lamport_hb t2 t1)
   ∧ (∀t. ¬ lamport_hb t t)
   ∧ (∀t1 t2 t3. lamport_hb t1 t2 ⟶ lamport_hb t2 t3 ⟶ lamport_hb t1 t3)"

5. 定理が述べることと述べないこと

スコープを述べることは結果の一部であり、以前のスレッドでのあるやり取り（投稿5）が、このセクションが単なる脚注以上の意味を持つ理由です。それは、度合いの圏論的扱いが個体化要件を継承するかどうかを問うものでした。ロットに対する集約をコリミットとして解釈すると、混在する残高はコリミットが必要とするまさにその図を消去します。

このタワーはロットに依存しませんが、個体化を免れるわけではありません。ロットごとの来歴は必要ありません。自然性の四角は、(reg_action, asset_id) とチェーン幅によって遷移をインデックス付けし、どの単位がどこから来たかを追跡することはありません。しかし、明確に定義された度合い割り当て asset_degree aid を持つ安定した資産レベル識別子を前提としています。したがって、異なる宣言された度合いの単位を1つの識別子の下で混在させることは、モデルの型付け境界の外にあり、反証されたケースではなく、表現されていないケースです。バケット化された識別子または保守的な集約度という2つの修正が見られますが、どちらも設計上の方向性であり、定理の結果ではありません。機械化はマルチアセット結合ルールを証明しておらず、コリミットの解釈は、その図とインデックスが命名され、表現がそのインデックスを保存する場合にのみ正当です。生の代替可能な残高はロットインデックスを消去するため、それらについてはその解釈は利用できません。

コストも目に見えて異なります。バケット化された識別子は、バケットが廃止されるまで代替可能性を破壊しますが、単一の集約度はすべての単位の宣言を支配しなければならないため、1つの高度単位が残高全体の義務を広げます。型付け境界は、これらのコストが明確になる場所です。

さらに2つの構造的仮定も同じ場所に属します。自然性の結果は単一ハブトポロジーに依存します。チェーン0はどのレベルでも忘れられず、許容性はそれにアンカーされるため、ここではマルチハブまたは変化するトポロジーについては何も述べていません。そして、アクション語彙は固定されています。四角は与えられた操作インデックスに対して可換であり、アクションセット自体の変更に対してではありません。

分業の概要は次のとおりです。

機械化で証明されたこと	設計上の解釈	確立されていないこと
保存マッピングの圏構造（恒等写像、合成、結合性）、degree_forget の自然性、over_provisioning_guarantees、no_downward_safety、boundary_well_defined、明示されたインターフェース義務の下での認証されたマージとブラインドビューの有効性	発行時に宣言され、チェック可能なインターフェースメタデータとしての度合い、会場レベルでの受け入れと拒否、自然性法則のアプリケーションとしてのイグジットプロトコル	幅から運用上の度合いセマンティクスへの洗練、マルチアセット結合ルール、ライブサイクル中の度合い変更、マルチハブ自然性、いかなる実装もモデルに準拠すること

したがって、スレッドの質問には正確な答えがあります。圏論的記述はロットごとの要件を継承するのではなく、操作インデックスがすでに持つ資産レベルの個体化を継承します。境界は定義に暗黙的に含まれていましたが、このやり取りにより定理のスコープとして明示的に述べられることになりました。

6. これがここで重要である理由

部分同期はロールアップエコシステムの通常の条件であり、段階付けされたモデルはその強度に型を与えます。インターフェース解釈は、定理そのものではなく定理に基づいて構築された設計上の解釈であり、直接的です。アセットはその度合いを宣言し、会場は処理できる度合いを宣伝します。そのレベル以下での受け入れは、有効状態の前提を満たす入力に対して over_provisioning_guarantees によって裏付けられ、それ以上での拒否は no_downward_safety が保守的に動機付けるものです。上位への移動は変換プロトコルであり、再ラベリングではありません。不一致はサイレントなダウングレードではなくなり、型付けされた拒否となります。認証されたインターフェースの結果は、コミットメントによって検証し、ブラインドビューを公開する相手方にも同じ規律を拡張します。これは、許可型台帳が公開チェーンと出会う一般的なパターンであり、インターフェース義務が果たされている場合に限ります。アトミックなバインディングは、離散的な更新周辺の抽出機会の構造も変化させますが、その問題は現在のスコープ外です。

7. 成果物

• 機械化: Cross_Domain_State_Preservation セッション、Isabelle/HOL、sorryなしビルド。Functor_Laws.thy、Composition.thy、Hierarchy.thy、External_Instance.thy を含む理論（コミット aafdcf327cce0dbfed4e9123dfe3f46ef786d028 のリポジトリ）。
• 論文: The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL, v3。

8. 未解決の問い

これらは活発に探求されている方向性であり、コミュニティの視点を得るためにここに投稿されています。

• 集約度。 異なる宣言された度合いを持つ単位が1つの表現を共有する場合、どの保守的な集約ルールが健全であり、表現力と代替可能性においてどのようなコストがかかるか？
• 動的昇格。 アセットの宣言された度合いが同期サイクル中に変更された場合、どの度合いがそのサイクルを支配し、遷移境界はどこに配置されるべきか？
• 単一ハブを超えて。 現在の自然性の結果はハブチェーン0を保存します。複数のハブや変化する結合トポロジーを越えて自然性を回復するには、どのような追加構造が必要か？
• 義務の境界。 どの法則が公開仕様に属し、どの法則が実装レベルの準拠またはコード検証によって果たされるべきであり、どの法則が設計ガイダンスとして残るべきか？

1投稿 - 1参加者

トピック全文を読む