JPYC.wf_decreaseAllowance
名称・種別
- 名称:
JPYC.wf_decreaseAllowance - 種別: theorem
- モジュール:
JpycFormalVerification.ERC20Theorems - ソース:
JpycFormalVerification/ERC20Theorems.lean:505-515 - 概要: decreaseAllowance は健全性不変条件 WF を保つ、という定理。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {decrement : JPYC.U256}, JPYC.WF s → Eq (JPYC.decreaseAllowance s ctx spender decrement) (Except.ok s') → JPYC.WF s's が WF を満たし decreaseAllowance が成功するなら、結果 s' も WF を満たす、という定理です。
解説
何を述べているか。 許可額の減算操作 decreaseAllowance は WF を保ちます。
直感。 ガードと「減らしすぎ防止」require、checked 減算 sub? を順に剥がすと _approve（許可額の書き込み）に到達。許可額のみ変えるので _approve_wf で WF が保たれます（checkAllowlist を持たないぶん increaseAllowance より簡素）。
なぜ安全性に効くか。 減算後もフラグ・バージョンが健全なまま。許可額がアンダーフローしないことと合わせ、減らす方向の操作も状態を壊さないことを保証します。
図解
Lean ソースコード
lean
/-- **WF preservation** for `decreaseAllowance`. -/
theorem wf_decreaseAllowance {s s' : State} {ctx : CallContext} {spender : Address}
{decrement : U256} (hwf : WF s) (h : decreaseAllowance s ctx spender decrement = .ok s') :
WF s' := by
unfold decreaseAllowance _decreaseAllowance 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⟩ := req_bind_eq_ok h
obtain ⟨_, _, h⟩ := bind_eq_ok h
exact _approve_wf hwf h