JPYC.transferOwnership

名称・種別

• 名称: JPYC.transferOwnership
• 種別: def
• モジュール: JpycFormalVerification.AccessControl
• ソース: JpycFormalVerification/AccessControl.lean:104-109
• 概要: transferOwnership(newOwner)：owner のみが所有権を移転できる関数。
• 仕様: 対象外

型シグネチャ

JPYC.State → JPYC.CallContext → JPYC.Address → Except JPYC.Error JPYC.State

State・CallContext・新オーナー newOwner を受け取り、オーナーだけが、ゼロアドレス以外への所有権移転を行える関数です。

和訳 docstring

オーナーを newOwner に変更する（v1/Ownable.sol:57-60）。

解説

何を述べているか。 ERC の Ownable.transferOwnership です。現オーナーの呼び出し（onlyOwner）を要求し、さらに newOwner がゼロアドレスでないことを要求してから、オーナーを newOwner に書き換えます。

直感。 所有権という最上位の権限を、現オーナーが指定する別アドレスへ引き渡します。newOwner ≠ address(0) の検査により、誤って「持ち主のいない」状態にすることを防ぎます。

なぜ安全性に効くか。 JPYC 版 Ownable は renounceOwnership（所有権の放棄）を 削除 しているため、所有権がゼロアドレスに落ちる経路はそもそも存在しません。この関数でも newOwner ≠ 0 を課すので、オーナーは常に有効なアドレスに保たれます（transferOwnership_sets_owner）。権限は現オーナーに限られます（transferOwnership_auth）。

図解

Lean ソースコード

/-- `transferOwnership(newOwner)` — `v1/Ownable.sol:57-60`. -/
def transferOwnership (s : State) (ctx : CallContext) (newOwner : Address) :
    Except Error State := do
  onlyOwner s ctx
  req (newOwner ≠ Address.zero) .newOwnerZero
  pure (_transferOwnership s newOwner)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v1/Ownable.sol:57-60

function transferOwnership(address newOwner) public virtual onlyOwner {
    require(newOwner != address(0), "Ownable: new owner is the zero address");
    _transferOwnership(newOwner);
}

依存

• JPYC.Address
• JPYC.Address.zero
• JPYC.CallContext
• JPYC.Error
• JPYC.State
• JPYC.onlyOwner
• JPYC.req