JPYCv2 形式検証

外観

JPYC.initializeV2_ok ​

名称・種別 ​

  • 名称: JPYC.initializeV2_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:183-190
  • 概要: 成功した initializeV2 を順方向に特徴づける補助補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext}, Eq (JPYC.initializeV2 O s ctx) (Except.ok s') → And (Eq s.initializedVersion 1) (Eq s' { name := s.name, symbol := s.symbol, currency := s.currency, decimals := s.decimals, totalSupply := s.totalSupply, initializedVersion := 2, balances := s.balances, allowed := s.allowed, minters := s.minters, minterAllowed := s.minterAllowed, allowlisted := s.allowlisted, owner := s.owner, pauser := s.pauser, blocklister := s.blocklister, rescuer := s.rescuer, minterAdmin := s.minterAdmin, allowlister := s.allowlister, paused := s.paused, blocklisted := s.blocklisted, domainSeparator := O.makeDomainSeparator s.name "2" ctx.blockChainId, chainId := s.chainId, domainName := s.domainName, version := "2", permitNonces := s.permitNonces, authorizationStates := s.authorizationStates })

initializeV2 が成功したという仮定から、版数 1 だったことと結果状態の形を取り出す前向き特徴づけ補題です。

解説 ​

何を述べているか。 initializeV2 が Except.ok s' で成功したとき、s.initializedVersion = 1 であり、s' が「版数 2・VERSION = "2"・ドメインセパレータ再計算」を施した状態に等しいことを取り出します。証明は req_bind_eq_ok でガードを剝がし、pure_ok で pure の成功値を取り出します。

直感。 「成功した」という結果から「版数 1 だった」「状態がどうなったか」を逆算する分解です。V2 初期化の後続定理は、この 1 本から枝分かれします。

なぜ安全性に効くか。 initializeV2 の 仕様の核 です。一回限り性（*_requires_v1 / *_sets_version）と不変条件（*_wf / *_conserves）が、ここから短く導けます。

図解 ​

Lean ソースコード ​

lean
theorem initializeV2_ok {O : SigOracle} {s s' : State} {ctx : CallContext}
    (h : initializeV2 O s ctx = .ok s') :
    s.initializedVersion = 1 ∧ s' = { s with
      initializedVersion := 2, version := "2",
      domainSeparator := O.makeDomainSeparator s.name "2" ctx.blockChainId } := by
  unfold initializeV2 at h
  obtain ⟨h1, h⟩ := req_bind_eq_ok h
  exact ⟨h1, pure_ok h⟩

依存 ​