JPYCv2 形式検証

外観

JPYC.pause ​

名称・種別 ​

  • 名称: JPYC.pause
  • 種別: def
  • モジュール: JpycFormalVerification.AccessControl
  • ソース: JpycFormalVerification/AccessControl.lean:113-116
  • 概要: pause()：コントラクト全体を一時停止する関数（pauser 限定）。
  • 仕様: 対象外

型シグネチャ ​

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

State と CallContext を受け取り、一時停止権限者だけがコントラクトを停止状態にする関数です。

和訳 docstring ​

コントラクトを停止状態にする（v1/Pausable.sol:78-81）。

解説 ​

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

直感。 緊急時に送金・承認・ミントなどの主要操作を一括で止める「非常停止ボタン」です。押せるのは pauser だけです。

なぜ安全性に効くか。 paused = true の間は whenNotPaused を持つ全関数が revert します（*_paused 群）。停止を pauser に限定することで、攻撃検知時に資金移動を確実に凍結できます。権限は pause_auth、効果は pause_sets_paused が保証します。

図解 ​

Lean ソースコード ​

lean
/-- `pause()` — `v1/Pausable.sol:78-81`. -/
def pause (s : State) (ctx : CallContext) : Except Error State := do
  onlyPauser s ctx
  pure (s.setPaused true)

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/Pausable.sol:78-81

solidity
function pause() external onlyPauser {
    paused = true;
    emit Pause();
}

依存 ​