JPYCv2 形式検証

外観

JPYC.initializeV2_wf ​

名称・種別 ​

  • 名称: JPYC.initializeV2_wf
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:228-233
  • 概要: initializeV2 は健全性不変条件 WF を保つ、という定理。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext}, JPYC.WF s → Eq (JPYC.initializeV2 O s ctx) (Except.ok s') → JPYC.WF s'

initializeV2 が成功するなら、結果状態も WF を満たす、という不変条件保存の定理です。

和訳 docstring ​

WF 保存。 initializeV2 はフラグマップに触れず、ラッチを範囲内（2 ≤ 2）に保つ。

解説 ​

何を述べているか。 事前状態 s が WF を満たし、initializeV2 が成功して s' になったとき、s' もまた WF を満たします。

直感。 initializeV2 はフラグマップ（ブロック・許可リスト・authorization 台帳）に一切触れず、版数を 2 にするだけです。2 ≤ 2 なので版数の範囲条件も保たれ、フラグの 0/1 性は元のまま引き継がれます。

なぜ安全性に効くか。 アップグレード初期化が状態の健全性を壊さないことを保証します。

図解 ​

Lean ソースコード ​

lean
/-- **WF preservation.** `initializeV2` leaves every flag map untouched and the
latch at `2 ≤ 2`. -/
theorem initializeV2_wf {O : SigOracle} {s s' : State} {ctx : CallContext}
    (hwf : WF s) (h : initializeV2 O s ctx = .ok s') : WF s' := by
  obtain ⟨_, rfl⟩ := initializeV2_ok h
  exact wf_of_flags_eq_version_valid hwf rfl rfl rfl (by show (2 : U8).toNat ≤ 2; decide)

依存 ​