JPYCv2 形式検証

外観

JPYC.transfer_totalSupply ​

名称・種別 ​

  • 名称: JPYC.transfer_totalSupply
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:333-335
  • 概要: 成功した transfer は totalSupply を変えない、という定理。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {dst : JPYC.Address} {value : JPYC.U256}, Eq (JPYC.transfer s ctx dst value) (Except.ok s') → Eq s'.totalSupply s.totalSupply

transfer が成功するなら、結果状態の総供給量 s'.totalSupply は元の s.totalSupply に等しい、という定理です。

解説 ​

何を述べているか。 送金は総供給量をまったく変えません。送り手と受け手の残高は動きますが、totalSupply フィールドには触れません。

直感。 transfer は残高マッピングだけを書き換え、総供給フィールドは読みも書きもしません。setBalance_totalSupply（残高更新は総供給を保つ）から従います。

なぜ安全性に効くか。 「送金で総発行量が変わってはならない」という ERC20 の基本契約です。mint/burn だけが総供給を動かしてよく、transfer は動かしてはいけない――その境界を明示します。

図解 ​

Lean ソースコード ​

lean
theorem transfer_totalSupply {s s' : State} {ctx : CallContext} {dst : Address} {value : U256}
    (h : transfer s ctx dst value = .ok s') : s'.totalSupply = s.totalSupply :=
  _transfer_totalSupply (transfer_eq_ok h)

依存 ​