JPYC.updatePauser

名称・種別

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

型シグネチャ

lean

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

State・CallContext・新権限者 newPauser を受け取り、オーナーだけが一時停止権限者を交代させる関数です。

和訳 docstring

一時停止権限者を newPauser に交代する（v1/Pausable.sol:94-101）。

解説

何を述べているか。 Pausable.updatePauser です。onlyOwner を要求し、newPauser ≠ address(0) を確かめてから、pauser を newPauser に書き換えます。

直感。 「非常停止ボタンを誰が押せるか」という役割を、オーナーが付け替えます。ゼロアドレス指定を弾くことで、止められない（解除もできない）状態を防ぎます。

なぜ安全性に効くか。 ロールの交代はオーナー権限（最上位）でのみ可能、という階層を作ります。これにより pauser の鍵が漏れても、オーナーが安全なアドレスへ差し替えられます。権限は updatePauser_auth が保証します。

図解

Lean ソースコード

lean

/-- `updatePauser(newPauser)` — `v1/Pausable.sol:94-101`. -/
def updatePauser (s : State) (ctx : CallContext) (newPauser : Address) :
    Except Error State := do
  onlyOwner s ctx
  req (newPauser ≠ Address.zero) .pausableNewPauserZero
  pure (s.setPauser newPauser)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v1/Pausable.sol:94-101

solidity

function updatePauser(address _newPauser) external onlyOwner {
    require(
        _newPauser != address(0),
        "Pausable: new pauser is the zero address"
    );
    pauser = _newPauser;
    emit PauserChanged(pauser);
}

JPYC.updatePauser ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​