JPYC.whenNotPaused_paused

名称・種別

• 名称: JPYC.whenNotPaused_paused
• 種別: theorem
• モジュール: JpycFormalVerification.AccessControlTheorems
• ソース: JpycFormalVerification/AccessControlTheorems.lean:658-661
• 概要: paused 状態では whenNotPaused は revert する、という補題。
• 仕様: 対象

型シグネチャ

∀ {s : JPYC.State}, Eq s.paused Bool.true → Eq (JPYC.whenNotPaused s) (Except.error JPYC.Error.paused)

コントラクトが停止中（paused = true）なら、whenNotPaused ガードは Pausable: paused で revert する、という補題です。

和訳 docstring

whenNotPaused of a paused contract reverts.（停止中コントラクトの whenNotPaused は revert する。）

解説

何を述べているか。 s.paused = true のとき whenNotPaused s = .error .paused です。whenNotPaused は req (!paused) .paused なので、paused が真なら条件 !paused は偽となり、if_neg で .error .paused に倒れます。

直感。 「停止スイッチが入っていれば、この関所は必ず閉じている」。

なぜ安全性に効くか。 これ 1 本が、停止系のすべての定理（transfer_paused・mint_paused など）の共通の土台です。各関数の先頭ガードが whenNotPaused であることと合わせ、「停止中はその関数が必ず revert する」を一律に導きます。

図解

Lean ソースコード

/-- `whenNotPaused` of a paused contract reverts. -/
theorem whenNotPaused_paused {s : State} (h : s.paused = true) :
    whenNotPaused s = .error .paused := by
  unfold whenNotPaused req; rw [if_neg (by rw [h]; decide)]; rfl

依存

• JPYC.Error
• JPYC.State
• JPYC.req
• JPYC.whenNotPaused