JPYCv2 形式検証

外観

JPYC.increaseAllowance_revert_noop ​

名称・種別 ​

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

型シグネチャ ​

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

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

解説 ​

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

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

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

図解 ​

Lean ソースコード ​

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

依存 ​