JPYCv2 形式検証

外観

JPYC.increaseAllowance_conserves ​

名称・種別 ​

  • 名称: JPYC.increaseAllowance_conserves
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:575-582
  • 概要: increaseAllowance は供給保存不変条件 SupplyConserved を保つ、という定理。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {spender : JPYC.Address} {increment : JPYC.U256}, JPYC.SupplyConserved s → Eq (JPYC.increaseAllowance s ctx spender increment) (Except.ok s') → JPYC.SupplyConserved s'

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

和訳 docstring ​

increaseAllowance の 供給保存（allowed だけを書き換える）。

解説 ​

何を述べているか。 許可額の増額は供給保存を保ちます。許可枠を書き換えるだけで、残高にも総供給にも触れないからです。

直感。 increaseAllowance_eq_ok で _increaseAllowance に還元すると、本体は _approve による allowed の更新だけ。残高マッピングも totalSupply も不変なので、_approve_conserves をそのまま持ち上げれば totalSupply = 全残高の合計 の両辺が保たれます。

なぜ安全性に効くか。 approve_conserves と対称に、「許可額を増やしても帳簿の合計は動かない」を確定します。許可枠（使ってよい枠）と実残高（実際のお金）が独立であることの、供給面からの裏付けです。

図解 ​

Lean ソースコード ​

lean
/-- **Supply conservation** for `increaseAllowance` (it rewrites only `allowed`). -/
theorem increaseAllowance_conserves {s s' : State} {ctx : CallContext} {spender : Address}
    {increment : U256} (hc : SupplyConserved s)
    (h : increaseAllowance s ctx spender increment = .ok s') : SupplyConserved s' := by
  have h := increaseAllowance_eq_ok h
  unfold _increaseAllowance at h
  obtain ⟨_, _, h⟩ := bind_eq_ok h
  exact _approve_conserves hc h

依存 ​