JPYCv2 形式検証

外観

JPYC.approve_conserves ​

名称・種別 ​

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

型シグネチャ ​

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

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

解説 ​

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

直感。 approve は allowed のみ更新。残高マッピングも totalSupply も不変（setAllowance_balances・setAllowance_totalSupply）なので、totalSupply = 全残高の合計 の両辺がそのまま保たれます。

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

図解 ​

Lean ソースコード ​

lean
theorem approve_conserves {s s' : State} {ctx : CallContext} {spender : Address} {value : U256}
    (hc : SupplyConserved s) (h : approve s ctx spender value = .ok s') : SupplyConserved s' :=
  _approve_conserves hc (approve_eq_ok h)

依存 ​