JPYC.decreaseAllowance_conserves
名称・種別
- 名称:
JPYC.decreaseAllowance_conserves - 種別: theorem
- モジュール:
JpycFormalVerification.ERC20Theorems - ソース:
JpycFormalVerification/ERC20Theorems.lean:612-620 - 概要: decreaseAllowance は供給保存不変条件 SupplyConserved を保つ、という定理。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {decrement : JPYC.U256}, JPYC.SupplyConserved s → Eq (JPYC.decreaseAllowance s ctx spender decrement) (Except.ok s') → JPYC.SupplyConserved s's が SupplyConserved を満たし decreaseAllowance が成功するなら、結果 s' も SupplyConserved を満たす、という定理です。
和訳 docstring
decreaseAllowance の 供給保存。
解説
何を述べているか。 許可額の減額は供給保存を保ちます。許可枠を書き換えるだけで、残高にも総供給にも触れないからです。
直感。 decreaseAllowance_eq_ok で _decreaseAllowance に還元すると、本体は _approve による allowed の更新だけ。残高マッピングも totalSupply も不変なので、_approve_conserves をそのまま持ち上げれば供給保存が保たれます。
なぜ安全性に効くか。 increaseAllowance_conserves と対称に、「許可額を減らしても帳簿の合計は動かない」を確定します。許可枠と実残高が独立であることの、供給面からの裏付けです。
図解
Lean ソースコード
lean
/-- **Supply conservation** for `decreaseAllowance`. -/
theorem decreaseAllowance_conserves {s s' : State} {ctx : CallContext} {spender : Address}
{decrement : U256} (hc : SupplyConserved s)
(h : decreaseAllowance s ctx spender decrement = .ok s') : SupplyConserved s' := by
have h := decreaseAllowance_eq_ok h
unfold _decreaseAllowance at h
obtain ⟨_, h⟩ := req_bind_eq_ok h
obtain ⟨_, _, h⟩ := bind_eq_ok h
exact _approve_conserves hc h