JPYC.wf_approve

名称・種別

名称: JPYC.wf_approve
種別: theorem
モジュール: JpycFormalVerification.ERC20Theorems
ソース: JpycFormalVerification/ERC20Theorems.lean:476-478
概要: approve は健全性不変条件 WF を保つ、という定理。
仕様: 対象

型シグネチャ

lean

∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {value : JPYC.U256}, JPYC.WF s → Eq (JPYC.approve s ctx spender value) (Except.ok s') → JPYC.WF s'

s が WF を満たし approve が成功するなら、結果 s' も WF を満たす、という定理です。

解説

何を述べているか。 承認操作は健全性不変条件 WF を壊しません。

直感。 approve が変えるのは許可額（allowed）だけ。フラグ・バージョンに触れないので WF.of_flags_eq で WF が保たれます。approve_eq_ok で _approve に還元してから _approve_wf を適用します。

なぜ安全性に効くか。 承認後もフラグが 0/1 を保ち、権限・ブロックリスト判定が破綻しません。状態を変える全操作が WF を保存する、という網羅性の一部です。

図解

Lean ソースコード

lean

theorem wf_approve {s s' : State} {ctx : CallContext} {spender : Address} {value : U256}
    (hwf : WF s) (h : approve s ctx spender value = .ok s') : WF s' :=
  _approve_wf hwf (approve_eq_ok h)

JPYC.wf_approve ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.wf_approve

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存