JPYC.updateAllowlister

名称・種別

名称: JPYC.updateAllowlister
種別: def
モジュール: JpycFormalVerification.AccessControl
ソース: JpycFormalVerification/AccessControl.lean:225-230
概要: updateAllowlister(newAllowlister)：allowlister ロールを付け替える関数（owner 限定）。
仕様: 対象外

型シグネチャ

lean

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

State・CallContext・新管理者 newAllowlister を受け取り、オーナーだけが許可リスト管理者を交代させる関数です。

和訳 docstring

許可リスト管理者を newAllowlister に交代する（v2/FiatTokenV2.sol:634-641）。

解説

何を述べているか。 FiatTokenV2.updateAllowlister です。onlyOwner を要求し、newAllowlister ≠ address(0) を確かめてから、allowlister を書き換えます。

直感。 「誰を許可リストに載せられるか」という権限者を、オーナーが付け替えます。

なぜ安全性に効くか。 ロール交代をオーナー権限に限定する階層構造の一部です。権限は updateAllowlister_auth が保証します。

図解

Lean ソースコード

lean

/-- `updateAllowlister(newAllowlister)` — `v2/FiatTokenV2.sol:634-641`. -/
def updateAllowlister (s : State) (ctx : CallContext) (newAllowlister : Address) :
    Except Error State := do
  onlyOwner s ctx
  req (newAllowlister ≠ Address.zero) .newAllowlisterZero
  pure (s.setAllowlister newAllowlister)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:634-641

solidity

function updateAllowlister(address _newAllowlister) external onlyOwner {
    require(
        _newAllowlister != address(0),
        "FiatToken: new allowlister is the zero address"
    );
    allowlister = _newAllowlister;
    emit AllowlisterChanged(allowlister);
}

JPYC.updateAllowlister ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​