JPYC.configureMinter_paused
名称・種別
- 名称:
JPYC.configureMinter_paused - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:684-686 - 概要: paused 状態では configureMinter は Pausable: paused で revert する、という定理。
- 仕様: 対象
型シグネチャ
lean
∀ {s : JPYC.State} {ctx : JPYC.CallContext} {minter : JPYC.Address} {amount : JPYC.U256}, Eq s.paused Bool.true → Eq (JPYC.configureMinter s ctx minter amount) (Except.error JPYC.Error.paused)コントラクトが停止中なら、configureMinter は本体に入る前に Pausable: paused で revert する、という停止定理です。
解説
何を述べているか。 s.paused = true のとき configureMinter s ctx minter amount = .error .paused です。configureMinter の先頭ガードが whenNotPaused なので、whenNotPaused_paused で書き換えれば即座に revert が出ます。
直感。 「非常停止中は、この操作は一切実行されない」。状態も当然変わりません。
なぜ安全性に効くか。 緊急停止が 実効的 であること ―― 停止フラグを立てれば、資金や権限を動かす操作が確実に止まること ―― の個別保証です。whenNotPaused を持つ全関数についてこの形が揃い、停止の網羅性を示します。
図解
Lean ソースコード
lean
theorem configureMinter_paused {s : State} {ctx : CallContext} {minter : Address} {amount : U256}
(h : s.paused = true) : configureMinter s ctx minter amount = .error .paused := by
unfold configureMinter; rw [whenNotPaused_paused h]; rfl