JPYCv2 形式検証

外観

JPYC.decreaseAllowance_revert_noop ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ {s : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {decrement : JPYC.U256} {e : JPYC.Error}, Eq (JPYC.decreaseAllowance s ctx spender decrement) (Except.error e) → Eq (s.afterCall (JPYC.decreaseAllowance s ctx spender decrement)) s

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

解説 ​

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

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

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

図解 ​

Lean ソースコード ​

lean
theorem decreaseAllowance_revert_noop {s : State} {ctx : CallContext} {spender : Address}
    {decrement : U256} {e : Error} (h : decreaseAllowance s ctx spender decrement = .error e) :
    s.afterCall (decreaseAllowance s ctx spender decrement) = s := by simp [h]

依存 ​