JPYCv2 形式検証

外観

JPYC.unpause ​

名称・種別 ​

  • 名称: JPYC.unpause
  • 種別: def
  • モジュール: JpycFormalVerification.AccessControl
  • ソース: JpycFormalVerification/AccessControl.lean:118-121
  • 概要: unpause()：一時停止を解除する関数（pauser 限定）。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.CallContext → Except JPYC.Error JPYC.State

State と CallContext を受け取り、一時停止権限者だけが停止を解除して通常状態に戻す関数です。

和訳 docstring ​

停止を解除して通常状態に戻す（v1/Pausable.sol:86-89）。

解説 ​

何を述べているか。 Pausable.unpause です。onlyPauser を通過した呼び出しだけが、paused フラグを false に戻します。

直感。 pause の対です。問題が解決したら、pauser が通常運転を再開します。

なぜ安全性に効くか。 停止・解除の両方を pauser に限定することで、運転状態の切り替えが単一の責任者に集約されます。権限は unpause_auth、効果は unpause_sets_unpaused が保証します。

図解 ​

Lean ソースコード ​

lean
/-- `unpause()` — `v1/Pausable.sol:86-89`. -/
def unpause (s : State) (ctx : CallContext) : Except Error State := do
  onlyPauser s ctx
  pure (s.setPaused false)

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/Pausable.sol:86-89

solidity
function unpause() external onlyPauser {
    paused = false;
    emit Unpause();
}

依存 ​