JPYCv2 形式検証

外観

JPYC.afterCall_error ​

名称・種別 ​

  • 名称: JPYC.afterCall_error
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:118-120
  • 概要: revert した呼び出しは観測される状態を変えない、という補題。
  • 仕様: 対象

型シグネチャ ​

lean
∀ (s : JPYC.State) (e : JPYC.Error), Eq (s.afterCall (Except.error e)) s

任意の状態 s と理由 e について、s.afterCall (Except.error e) は s に等しい、という等式です。

和訳 docstring ​

revert した呼び出しは、観測される状態を変えない。

解説 ​

何を述べているか。 revert（Except.error e）を afterCall で観測すると、状態は元の s のまま、という形式的な「revert は無操作」保証です。

直感。 失敗した呼び出しは、状態に何の痕跡も残しません。afterCall の定義の .error 枝そのものなので rfl で従います。

なぜ安全性に効くか。 すべての *_revert_noop 定理（transfer_revert_noop ほか）がこの補題に帰着します。@[simp] 指定されており、「失敗 ⇒ 状態不変」を証明全体で自動的に使えます。攻撃者が失敗トランザクションで状態を汚すことはできない、という保証の核です。

図解 ​

Lean ソースコード ​

lean
/-- A reverting call leaves the observed state unchanged. -/
@[simp] theorem afterCall_error (s : State) (e : Error) :
    s.afterCall (.error e) = s := rfl

依存 ​