JPYC.owner

名称・種別

• 名称: JPYC.owner
• 種別: def
• モジュール: JpycFormalVerification.AccessControl
• ソース: JpycFormalVerification/AccessControl.lean:234-235
• 概要: owner()：現在の所有者アドレスを返す読み取り専用ビュー。
• 仕様: 対象外

型シグネチャ

JPYC.State → JPYC.Address

State を受け取り、現在のオーナーアドレスを返す読み取り専用関数です。

和訳 docstring

現在のオーナーを返す（v1/Ownable.sol:41-43）。

解説

何を述べているか。 Ownable.owner です。状態 s の owner フィールドをそのまま返します。

直感。 状態を 読むだけ の関数（Solidity の view）で、書き込みは一切しません。返り値は現オーナーのアドレスです。

なぜ安全性に効くか。 これ自体は状態を変えないので安全性の主役ではありませんが、ガードや他の証明が参照する「観測値」を定義します。たとえばブロック判定・許可リスト判定・ミンター判定は、対応するフラグマッピングをこの形で読み出します。

図解

Lean ソースコード

/-- `owner()` — `v1/Ownable.sol:41-43`. -/
def owner (s : State) : Address := s.owner

対応 Solidity ソースコード

reference/JPYCv2/contracts/v1/Ownable.sol:41-43

function owner() public view virtual returns (address) {
    return _owner;
}

依存

• JPYC.Address
• JPYC.State