JPYCv2 形式検証

外観

JPYC.initializeV1_ok ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {self : JPYC.Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : JPYC.U8} {newMinterAdmin newPauser newBlocklister newRescuer newOwner : JPYC.Address}, Eq (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) (Except.ok s') → And (Eq s.initializedVersion 0) (And (Ne newMinterAdmin JPYC.Address.zero) (And (Ne newPauser JPYC.Address.zero) (And (Ne newBlocklister JPYC.Address.zero) (And (Ne newRescuer JPYC.Address.zero) (And (Ne newOwner JPYC.Address.zero) (Eq s' (JPYC.initializeResult O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner)))))))

initializeV1 が成功したという仮定から、6 つのガード（版数 0 ＋ 5 つの非ゼロアドレス）の成立と、結果状態が initializeResult に等しいことを取り出す前向き特徴づけ補題です。

解説 ​

何を述べているか。 initializeV1 が Except.ok s' で成功したとき、s.initializedVersion = 0 と 5 つの ≠ Address.zero、そして s' = initializeResult … がすべて取り出せます。証明は先頭から req_bind_eq_ok でガードを 1 枚ずつ剝がし、最後に pure_ok で pure の成功値を取り出します。

直感。 「成功した」という結果だけから、「どの条件が満たされていたか」「状態がどう変わったか」を逆算する分解です。初期化に関する後続のすべての定理は、この 1 本から枝分かれします。

なぜ安全性に効くか。 これは initializeV1 の 仕様の核 です。一度証明しておけば、一回限り性（*_requires_* / *_sets_version）・効果（*_sets_owner ほか）・不変条件（*_wf / *_conserves）が短く導けます。

図解 ​

Lean ソースコード ​

lean
theorem initializeV1_ok {O : SigOracle} {s s' : State} {ctx : CallContext} {self : Address}
    {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : U8}
    {newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address}
    (h : initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
      newMinterAdmin newPauser newBlocklister newRescuer newOwner = .ok s') :
    s.initializedVersion = 0 ∧ newMinterAdmin ≠ Address.zero ∧ newPauser ≠ Address.zero ∧
      newBlocklister ≠ Address.zero ∧ newRescuer ≠ Address.zero ∧ newOwner ≠ Address.zero ∧
      s' = initializeResult O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
        newMinterAdmin newPauser newBlocklister newRescuer newOwner := by
  unfold initializeV1 at h
  obtain ⟨h0, h⟩ := req_bind_eq_ok h
  obtain ⟨h1, h⟩ := req_bind_eq_ok h
  obtain ⟨h2, h⟩ := req_bind_eq_ok h
  obtain ⟨h3, h⟩ := req_bind_eq_ok h
  obtain ⟨h4, h⟩ := req_bind_eq_ok h
  obtain ⟨h5, h⟩ := req_bind_eq_ok h
  exact ⟨h0, h1, h2, h3, h4, h5, pure_ok h⟩

依存 ​