JPYC.State.afterCall

名称・種別

• 名称: JPYC.State.afterCall
• 種別: def
• モジュール: JpycFormalVerification.ERC20Theorems
• ソース: JpycFormalVerification/ERC20Theorems.lean:112-116
• 概要: 呼び出し結果を EVM ロールバック付きで観測する関数：revert 時は前状態を保つ。
• 仕様: 対象

型シグネチャ

JPYC.State → Except JPYC.Error JPYC.State → JPYC.State

State と呼び出し結果 Except Error State を受け取り、成功なら新状態 s'、revert なら元の状態 s を返します。

和訳 docstring

呼び出し結果を EVM ロールバック付きで観測する ― revert 時は呼び出し前の状態を保つ。

解説

何を述べているか。 EVM のロールバック意味論をモデル化した関数です。呼び出しの結果が .ok s'（成功）ならその新状態を、.error _（revert）なら呼び出し前の状態 s をそのまま「観測される状態」として返します。

直感。 Ethereum では、トランザクションが revert すると途中の状態変更がすべて巻き戻されます。afterCall はこの「失敗したら無かったことになる」を 1 行で表現します。

なぜ安全性に効くか。 no-op on revert を厳密に述べるための仕組みです。各関数の *_revert_noop は「revert したら afterCall で観測される状態 = 元の状態」を主張し、その根拠が afterCall_error です。

図解

Lean ソースコード

/-- Observe a call result with EVM rollback: keep the pre-state on revert. -/
def State.afterCall (s : State) (r : Except Error State) : State :=
  match r with
  | .ok s' => s'
  | .error _ => s

依存

• JPYC.Error
• JPYC.State