JPYCv2 形式検証

外観

JPYC.whenNotPaused ​

名称・種別 ​

  • 名称: JPYC.whenNotPaused
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:46-49
  • 概要: whenNotPaused 修飾子。paused なら Pausable: paused で revert するガード。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → Except JPYC.Error Unit

State を受け取り、paused が false なら Except.ok ()、停止中なら Pausable: paused で revert します。

和訳 docstring ​

whenNotPaused ― require(!paused, "Pausable: paused")。停止中はあらゆる被ガード関数を revert させる。対応 Solidity: v1/Pausable.sol:62-65。

解説 ​

何を述べているか。 Solidity の whenNotPaused modifier、すなわち require(!paused, "Pausable: paused") をモデル化したガードです。req を使い、条件 s.paused = false を検査します。

直感。 コントラクトが一時停止中なら、このガードを持つ関数（送金・承認など）はすべて即座に revert します。非常ブレーキが踏まれている間は何も動かさない、という仕組みです。

なぜ安全性に効くか。 transfer / transferFrom / approve / increaseAllowance / decreaseAllowance の先頭に置かれます。インシデント時に管理者が pause を立てれば、これらの価値移動・承認操作が一括で止まる――その「止まる」ことを各関数の *_paused 定理（Phase 2）で保証する起点になります。

図解 ​

Lean ソースコード ​

lean
/-- `whenNotPaused` — `require(!paused, "Pausable: paused")`.
Source: `v1/Pausable.sol:62-65`. -/
def whenNotPaused (s : State) : Except Error Unit :=
  req (s.paused = false) .paused

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/Pausable.sol:62-65

solidity
modifier whenNotPaused() {
    require(!paused, "Pausable: paused");
    _;
}

依存 ​