JPYCv2 形式検証

外観

JPYC.transfer_revert_noop ​

名称・種別 ​

  • 名称: JPYC.transfer_revert_noop
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:523-525
  • 概要: transfer が revert した場合、状態は一切変化しない、という定理。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s : JPYC.State} {ctx : JPYC.CallContext} {dst : JPYC.Address} {value : JPYC.U256} {e : JPYC.Error}, Eq (JPYC.transfer s ctx dst value) (Except.error e) → Eq (s.afterCall (JPYC.transfer s ctx dst value)) s

transfer が Except.error e で revert したとき、afterCall で観測される状態は元の s のまま、という定理です。

解説 ​

何を述べているか。 no-op on revert の具体化です。transfer が失敗した場合、s.afterCall (transfer …) = s。すなわち失敗した呼び出しは状態に何も残しません。

直感。 失敗の結果は Except.error e なので、afterCall は元の状態 s を返します（afterCall_error を simp で適用するだけ）。

なぜ安全性に効くか。 EVM のロールバック ―「revert したトランザクションは状態を変えない」― を transfer について保証します。攻撃者が失敗する呼び出しを使って状態を中途半端に汚す、という攻撃が成立しないことの証です。

図解 ​

Lean ソースコード ​

lean
theorem transfer_revert_noop {s : State} {ctx : CallContext} {dst : Address}
    {value : U256} {e : Error} (h : transfer s ctx dst value = .error e) :
    s.afterCall (transfer s ctx dst value) = s := by simp [h]

依存 ​