JPYC.wf_increaseAllowance
名称・種別
- 名称:
JPYC.wf_increaseAllowance - 種別: theorem
- モジュール:
JpycFormalVerification.ERC20Theorems - ソース:
JpycFormalVerification/ERC20Theorems.lean:492-503 - 概要: increaseAllowance は健全性不変条件 WF を保つ、という定理。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {increment : JPYC.U256}, JPYC.WF s → Eq (JPYC.increaseAllowance s ctx spender increment) (Except.ok s') → JPYC.WF s's が WF を満たし increaseAllowance が成功するなら、結果 s' も WF を満たす、という定理です。
解説
何を述べているか。 許可額の積み増し操作 increaseAllowance は WF を保ちます。
直感。 ガードを req_bind_eq_ok で剥がし、checked 加算 add? を bind_eq_ok で、checkAllowlist を吸収し、最後は _approve（= 許可額の書き込み）に到達。許可額しか変えないので _approve_wf で WF が保たれます。
なぜ安全性に効くか。 積み増し後もフラグ・バージョンが健全なまま。checked 加算によりオーバーフローでの破綻も排除されており、許可額更新の全経路で整合性が保たれます。
図解
Lean ソースコード
lean
/-- **WF preservation** for `increaseAllowance`. -/
theorem wf_increaseAllowance {s s' : State} {ctx : CallContext} {spender : Address}
{increment : U256} (hwf : WF s) (h : increaseAllowance s ctx spender increment = .ok s') :
WF s' := by
unfold increaseAllowance _increaseAllowance whenNotPaused notBlocklisted at h
obtain ⟨_, h⟩ := req_bind_eq_ok h
obtain ⟨_, h⟩ := req_bind_eq_ok h
obtain ⟨_, h⟩ := req_bind_eq_ok h
obtain ⟨_, _, h⟩ := bind_eq_ok h
have h := checkAllowlist_bind_eq_ok h
obtain ⟨_, _, h⟩ := bind_eq_ok h
exact _approve_wf hwf h