JPYCv2 形式検証

外観

JPYC.initializeV2_wrong_version ​

名称・種別 ​

  • 名称: JPYC.initializeV2_wrong_version
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:206-211
  • 概要: version 1 以外からの initializeV2 は revert する（二重実行ガード・revert形）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s : JPYC.State} {ctx : JPYC.CallContext}, Ne s.initializedVersion 1 → Eq (JPYC.initializeV2 O s ctx) (Except.error JPYC.Error.initializeV2WrongVersion)

版数が 1 以外の状態からは、initializeV2 は initializeV2WrongVersion で revert する、という二重実行ガード（revert）の定理です。

和訳 docstring ​

二重実行ガード（revert）。 版数 1 以外からの initializeV2 は revert する（素の require(initializedVersion == 1)）。

解説 ​

何を述べているか。 s.initializedVersion ≠ 1 のとき、initializeV2 は Except.error .initializeV2WrongVersion を返します。素の require(initializedVersion == 1) の if を偽側（req_neg）に倒すだけです。

直感。 「版数が 1 でなければ、V2 初期化はちょうどこのエラーで弾かれる」。版数 0 でも 2 でも同じです。

なぜ安全性に効くか。 initializeV2_requires_v1 の対偶を、具体的なエラー名つきで固定します。Solidity 側が理由文字列のない素の require を使っていることに対応します。

図解 ​

Lean ソースコード ​

lean
/-- **Double-execution guard (revert).** From any version other than `1`,
`initializeV2` reverts (the bare `require(initializedVersion == 1)`). -/
theorem initializeV2_wrong_version {O : SigOracle} {s : State} {ctx : CallContext}
    (h : s.initializedVersion ≠ 1) :
    initializeV2 O s ctx = .error .initializeV2WrongVersion := by
  unfold initializeV2; rw [req_neg h]; rfl

依存 ​