JPYCv2 形式検証

外観

JPYC.transferFrom_totalSupply ​

名称・種別 ​

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

型シグネチャ ​

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

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

解説 ​

何を述べているか。 第三者送金は総供給量を変えません。許可額の消費も残高の移動も、totalSupply フィールドには触れないからです。

直感。 許可額ステップは transferFrom_step_balances より総供給を保ち、残高移動 _transfer も _transfer_totalSupply より総供給を保ちます。2 段とも保つので、全体でも不変です。

なぜ安全性に効くか。 transfer と同様、「送金は発行量を変えない」という基本契約を transferFrom についても確定します。総供給を動かしてよいのは mint/burn だけ、という不変式の網羅的な裏付けです。

図解 ​

Lean ソースコード ​

lean
theorem transferFrom_totalSupply {s s' : State} {ctx : CallContext} {frm dst : Address}
    {value : U256} (h : transferFrom s ctx frm dst value = .ok s') :
    s'.totalSupply = s.totalSupply := by
  obtain ⟨s₁, hstep, htrans⟩ := transferFrom_eq_ok h
  obtain ⟨_, hsup, _⟩ := transferFrom_step_balances hstep
  rw [_transfer_totalSupply htrans, hsup]

依存 ​