JPYCv2 形式検証

外観

JPYC.initializeV1_revert_noop ​

名称・種別 ​

  • 名称: JPYC.initializeV1_revert_noop
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:324-330
  • 概要: initializeV1 が revert した場合、状態は一切変化しない、という定理。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s : JPYC.State} {ctx : JPYC.CallContext} {self : JPYC.Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : JPYC.U8} {newMinterAdmin newPauser newBlocklister newRescuer newOwner : JPYC.Address} {e : JPYC.Error}, Eq (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) (Except.error e) → Eq (s.afterCall (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner)) s

initializeV1 が revert したとき、観測される状態（afterCall）は呼び出し前の状態に等しい、という「revert すれば状態は変わらない」定理です。

解説 ​

何を述べているか。 initializeV1 が Except.error e を返したとき、s.afterCall (initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) = s です。afterCall は「成功なら新状態、失敗なら元の状態」を返す観測関数なので、失敗時は定義から元の状態 s に簡約されます（simp [h]）。

直感。 EVM のトランザクション・ロールバックを模したものです。「途中で revert したら、何もなかったことになる」。

なぜ安全性に効くか。 no-op on revert は、失敗した呼び出しが副作用を残さないという基本的な安全性です。ガードに弾かれた初期化・アップグレードが、状態を中途半端に書き換えて残さないことを保証します。initializeV1 についてこれを個別に確認しています。

図解 ​

Lean ソースコード ​

lean
theorem initializeV1_revert_noop {O : SigOracle} {s : State} {ctx : CallContext} {self : Address}
    {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : U8}
    {newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address} {e : Error}
    (h : initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
      newMinterAdmin newPauser newBlocklister newRescuer newOwner = .error e) :
    s.afterCall (initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
      newMinterAdmin newPauser newBlocklister newRescuer newOwner) = s := by simp [h]

依存 ​