JPYC.approve_eq_ok
名称・種別
- 名称:
JPYC.approve_eq_ok - 種別: theorem
- モジュール:
JpycFormalVerification.ERC20Theorems - ソース:
JpycFormalVerification/ERC20Theorems.lean:454-462 - 概要: 成功した approve は呼び出し元からの _approve に還元される、という補題。
- 仕様: 対象外
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {value : JPYC.U256}, Eq (JPYC.approve s ctx spender value) (Except.ok s') → Eq (JPYC._approve s ctx.sender spender value) (Except.ok s')approve が成功するなら、内部の _approve s ctx.sender spender value も同じ結果で成功する、という還元定理です。
和訳 docstring
成功した approve は、呼び出し元を所有者とする _approve の成功に還元される。
解説
何を述べているか。 外部関数 approve の成功は、ガードを通過した後の内部関数 _approve（所有者 = ctx.sender）の成功に等しいと示します。
直感。 transfer_eq_ok と同じ構造です。whenNotPaused・notBlocklisted×2 を req_bind_eq_ok で剥がし、checkAllowlist を checkAllowlist_bind_eq_ok で吸収すると _approve が残ります。
なぜ安全性に効くか。 approve の性質（許可額設定・WF・供給保存）を、_approve の補題を持ち上げて導くための要石です。外部入口と内部本体をつなぎます。
図解
Lean ソースコード
lean
/-- A successful `approve` reduces to `_approve` from the caller. -/
theorem approve_eq_ok {s s' : State} {ctx : CallContext} {spender : Address} {value : U256}
(h : approve s ctx spender value = .ok s') :
_approve s ctx.sender spender value = .ok s' := by
unfold approve 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
exact checkAllowlist_bind_eq_ok h