JPYCv2 形式検証

外観

JPYC.initializeV1_requires_uninitialized ​

名称・種別 ​

  • 名称: JPYC.initializeV1_requires_uninitialized
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:63-70
  • 概要: initializeV1 は未初期化状態（version 0）からのみ成功する（二重実行ガード・順方向）。
  • 仕様: 対象

型シグネチャ ​

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') → Eq s.initializedVersion 0

initializeV1 の成功は、呼び出し前が 未初期化（initializedVersion = 0）だったことを含意する、という二重実行ガード（前向き）の定理です。

和訳 docstring ​

二重実行ガード（前向き）。 initializeV1 は未初期化状態（initializedVersion = 0）からのみ成功する。

解説 ​

何を述べているか。 initializeV1 が成功したなら s.initializedVersion = 0 です。initializeV1_ok の第 1 成分を取り出すだけです。

直感。 「初期化が通った ⇒ まだ初期化されていなかった」。すでに初期化済み（版数 ≠ 0）なら、先頭ガードで弾かれます。

なぜ安全性に効くか。 再初期化の不可能性の 前提側 です。対になる initializeV1_sets_version（成功後は版数 1）と組み合わさり、initializeV1_not_reinitializable を導きます。

図解 ​

Lean ソースコード ​

lean
/-- **Double-execution guard (forward).** `initializeV1` succeeds only from the
uninitialized state (`initializedVersion = 0`). -/
theorem initializeV1_requires_uninitialized {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 := (initializeV1_ok h).1

依存 ​