JPYC.updateBlocklister

名称・種別

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

型シグネチャ

lean

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

State・CallContext・新管理者 newBlocklister を受け取り、オーナーだけがブロックリスト管理者を交代させる関数です。

和訳 docstring

ブロックリスト管理者を newBlocklister に交代する（v1/Blocklistable.sol:100-107）。

解説

何を述べているか。 Blocklistable.updateBlocklister です。onlyOwner を要求し、newBlocklister ≠ address(0) を確かめてから、blocklister を書き換えます。

直感。 「誰を凍結できるか」という権限者を、オーナーが付け替えます。

なぜ安全性に効くか。 ロール交代をオーナー権限に限定する階層構造の一部です。ゼロアドレス禁止により、凍結機能が無効化される事故を防ぎます。権限は updateBlocklister_auth が保証します。

図解

Lean ソースコード

lean

/-- `updateBlocklister(newBlocklister)` — `v1/Blocklistable.sol:100-107`. -/
def updateBlocklister (s : State) (ctx : CallContext) (newBlocklister : Address) :
    Except Error State := do
  onlyOwner s ctx
  req (newBlocklister ≠ Address.zero) .blocklistableNewBlocklisterZero
  pure (s.setBlocklister newBlocklister)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v1/Blocklistable.sol:100-107

solidity

function updateBlocklister(address _newBlocklister) external onlyOwner {
    require(
        _newBlocklister != address(0),
        "Blocklistable: new blocklister is the zero address"
    );
    blocklister = _newBlocklister;
    emit BlocklisterChanged(blocklister);
}

JPYC.updateBlocklister ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​