JPYC.permit_paused

名称・種別

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

型シグネチャ

lean

∀ {O : JPYC.SigOracle} {s : JPYC.State} {ctx : JPYC.CallContext} {owner spender : JPYC.Address} {value deadline : JPYC.U256} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq s.paused Bool.true → Eq (JPYC.permit O s ctx owner spender value deadline v r sig) (Except.error JPYC.Error.paused)

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

解説

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

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

なぜ安全性に効くか。 緊急停止が 実効的 であること ―― 停止フラグを立てれば、署名を使った送金・承認・キャンセルまで含めて確実に止まること ―― の個別保証です。署名系 4 関数すべてについてこの形が揃い、停止の網羅性を示します。

図解

Lean ソースコード

lean

theorem permit_paused {O : SigOracle} {s : State} {ctx : CallContext} {owner spender : Address}
    {value deadline : U256} {v : U8} {r sig : Bytes32} (h : s.paused = true) :
    permit O s ctx owner spender value deadline v r sig = .error .paused := by
  unfold permit; rw [whenNotPaused_paused h]; rfl

JPYC.permit_paused ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.permit_paused

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存