JPYC.transfer_paused

名称・種別

名称: JPYC.transfer_paused
種別: theorem
モジュール: JpycFormalVerification.AccessControlTheorems
ソース: JpycFormalVerification/AccessControlTheorems.lean:663-665
概要: paused 状態では transfer は Pausable: paused で revert する、という定理。
仕様: 対象

型シグネチャ

lean

∀ {s : JPYC.State} {ctx : JPYC.CallContext} {dst : JPYC.Address} {value : JPYC.U256}, Eq s.paused Bool.true → Eq (JPYC.transfer s ctx dst value) (Except.error JPYC.Error.paused)

コントラクトが停止中なら、transfer は本体に入る前に Pausable: paused で revert する、という停止定理です。

解説

何を述べているか。 s.paused = true のとき transfer s ctx dst value = .error .paused です。transfer の先頭ガードが whenNotPaused なので、whenNotPaused_paused で書き換えれば即座に revert が出ます。

直感。 「非常停止中は、この操作は一切実行されない」。状態も当然変わりません。

なぜ安全性に効くか。 緊急停止が 実効的 であること ―― 停止フラグを立てれば、資金や権限を動かす操作が確実に止まること ―― の個別保証です。whenNotPaused を持つ全関数についてこの形が揃い、停止の網羅性を示します。

図解

Lean ソースコード

lean

theorem transfer_paused {s : State} {ctx : CallContext} {dst : Address} {value : U256}
    (h : s.paused = true) : transfer s ctx dst value = .error .paused := by
  unfold transfer; rw [whenNotPaused_paused h]; rfl

JPYC.transfer_paused ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.transfer_paused

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存