JPYC.transferFrom_conserves

名称・種別

名称: JPYC.transferFrom_conserves
種別: theorem
モジュール: JpycFormalVerification.ERC20Theorems
ソース: JpycFormalVerification/ERC20Theorems.lean:398-408
概要: 承認ステップが残高を保つので、transferFrom の保存は _transfer の保存に還元される、という定理。
仕様: 対象

型シグネチャ

lean

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

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

解説

何を述べているか。 第三者送金も供給保存を保ちます。totalSupply = 全残高の合計 が transferFrom の前後で崩れません。

直感。 transferFrom_eq_ok で中間状態 s₁ と _transfer に分解。transferFrom_step_balances より s₁ は s と同じ供給状況なので SupplyConserved s₁ が言え、あとは _transfer_conserves を適用します。

なぜ安全性に効くか。 allowance を介した送金でもお金が湧かず消えないことを保証します。transfer だけでなく transferFrom 経由でも供給の総量保存が破れない、という網羅性が監査品質に効きます。

図解

Lean ソースコード

lean

/-- The allowance step preserves balances, so `transferFrom` conservation reduces
to `_transfer` conservation. -/
theorem transferFrom_conserves {s s' : State} {ctx : CallContext} {frm dst : Address}
    {value : U256} (hc : SupplyConserved s) (h : transferFrom s ctx frm dst value = .ok s') :
    SupplyConserved s' := by
  obtain ⟨s₁, hstep, htrans⟩ := transferFrom_eq_ok h
  obtain ⟨hbal, hsup, _⟩ := transferFrom_step_balances hstep
  have hc₁ : SupplyConserved s₁ := by
    unfold SupplyConserved State.totalBalances at hc ⊢
    rw [hbal, hsup]; exact hc
  exact _transfer_conserves hc₁ htrans

JPYC.transferFrom_conserves ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.transferFrom_conserves

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存