JPYCv2 形式検証

外観

JPYC.upgradeTo_conserves ​

名称・種別 ​

  • 名称: JPYC.upgradeTo_conserves
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:287-289
  • 概要: upgradeTo は供給保存不変条件 SupplyConserved を保つ、という定理。
  • 仕様: 対象

型シグネチャ ​

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

upgradeTo が成功するなら、結果状態も SupplyConserved を満たす、という供給保存の定理です。

解説 ​

何を述べているか。 事前状態が SupplyConserved を満たし、upgradeTo が成功すれば、結果も供給保存を満たします。upgradeTo_ok より s' = s なので、hc がそのまま結論になります。

直感。 「状態が変わらないなら、供給の帳簿も当然そのまま」。

なぜ安全性に効くか。 アップグレード認可がトークンの総量・残高に影響しないことを保証します（モデル化された範囲において）。

図解 ​

Lean ソースコード ​

lean
theorem upgradeTo_conserves {s s' : State} {ctx : CallContext} {impl : Address}
    (hc : SupplyConserved s) (h : upgradeTo s ctx impl = .ok s') : SupplyConserved s' := by
  rw [(upgradeTo_ok h).2]; exact hc

依存 ​