JPYC.receiveWithAuthorization_paused

名称・種別

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

型シグネチャ

lean

∀ {O : JPYC.SigOracle} {s : JPYC.State} {ctx : JPYC.CallContext} {frm dst : JPYC.Address} {value validAfter validBefore : JPYC.U256} {nonce : JPYC.Bytes32} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq s.paused Bool.true → Eq (JPYC.receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.error JPYC.Error.paused)

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

解説

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

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

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

図解

Lean ソースコード

lean

theorem receiveWithAuthorization_paused {O : SigOracle} {s : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32} (h : s.paused = true) :
    receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .error .paused := by
  unfold receiveWithAuthorization; rw [whenNotPaused_paused h]; rfl

JPYC.receiveWithAuthorization_paused ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.receiveWithAuthorization_paused

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存