JPYCv2 形式検証

外観

JPYC.initializeV2_conserves ​

名称・種別 ​

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

型シグネチャ ​

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

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

和訳 docstring ​

供給保存。 initializeV2 は残高にも totalSupply にも触れない。

解説 ​

何を述べているか。 事前状態が SupplyConserved を満たし、initializeV2 が成功すれば、結果も供給保存を満たします。initializeV2 は残高にも総供給にも触れないので、仮定 hc をそのまま使えます。

直感。 V2 初期化はメタデータ（版数・ドメインセパレータ）を更新するだけで、お金は一切動かしません。

なぜ安全性に効くか。 アップグレード初期化がトークンを発行・焼却しないこと（供給の帳簿に中立）を保証します。

図解 ​

Lean ソースコード ​

lean
/-- **Supply conservation.** `initializeV2` touches neither balances nor
`totalSupply`. -/
theorem initializeV2_conserves {O : SigOracle} {s s' : State} {ctx : CallContext}
    (hc : SupplyConserved s) (h : initializeV2 O s ctx = .ok s') : SupplyConserved s' := by
  obtain ⟨_, rfl⟩ := initializeV2_ok h
  exact hc

依存 ​