JPYCv2 形式検証

外観

JPYC.transferOwnership_sets_owner ​

名称・種別 ​

  • 名称: JPYC.transferOwnership_sets_owner
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:164-170
  • 概要: 成功した transferOwnership は所有者を newOwner に設定する（かつ非ゼロ＝所有権放棄不可）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {newOwner : JPYC.Address}, Eq (JPYC.transferOwnership s ctx newOwner) (Except.ok s') → And (Eq s'.owner newOwner) (Ne newOwner JPYC.Address.zero)

transferOwnership の成功は、オーナーを newOwner に設定し、しかも newOwner がゼロアドレスでないことを含意する、という効果定理です。

和訳 docstring ​

効果。 transferOwnership の成功はオーナーを newOwner に設定する（newOwner は決してゼロアドレスにならず、所有権は放棄できない）。

解説 ​

何を述べているか。 transferOwnership が成功すると s'.owner = newOwner であり、かつ newOwner ≠ address(0) です。transferOwnership_ok から両成分を取り出します。

直感。 「所有権はちゃんと新しい人に移り、しかも宙に浮かない」を 1 つの定理にまとめています。

なぜ安全性に効くか。 JPYC 版 Ownable は renounceOwnership を削除しており、ここでも newOwner ≠ 0 を課すので、オーナーが不在になる経路が存在しない ことが保証されます。最上位権限が常に有効なアドレスに保たれます。

図解 ​

Lean ソースコード ​

lean
/-- **Effect.** A successful `transferOwnership` sets the owner to `newOwner`
(and `newOwner` is never the zero address — ownership cannot be dropped). -/
theorem transferOwnership_sets_owner {s s' : State} {ctx : CallContext} {newOwner : Address}
    (h : transferOwnership s ctx newOwner = .ok s') :
    s'.owner = newOwner ∧ newOwner ≠ Address.zero := by
  obtain ⟨_, h2, rfl⟩ := transferOwnership_ok h
  exact ⟨rfl, h2⟩

依存 ​