JPYCv2 形式検証

外観

JPYC.upgradeToAndCall_wf ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {impl : JPYC.Address}, JPYC.WF s → Eq (JPYC.upgradeToAndCall s ctx impl) (Except.ok s') → JPYC.WF s'

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

解説 ​

何を述べているか。 事前状態が WF を満たし、upgradeToAndCall が成功すれば、結果も WF を満たします。upgradeToAndCall_ok より s' = s（モデル状態は不変）なので、WF s がそのまま WF s' になります。

直感。 「状態が何も変わらないなら、健全性も当然そのまま」。

なぜ安全性に効くか。 アップグレード認可の経路が状態を壊さないことを、形式的に確認します（モデル化された範囲において）。

図解 ​

Lean ソースコード ​

lean
theorem upgradeToAndCall_wf {s s' : State} {ctx : CallContext} {impl : Address}
    (hwf : WF s) (h : upgradeToAndCall s ctx impl = .ok s') : WF s' := by
  rw [(upgradeToAndCall_ok h).2]; exact hwf

依存 ​