JPYC.transferFrom_self
名称・種別
- 名称:
JPYC.transferFrom_self - 種別: theorem
- モジュール:
JpycFormalVerification.ERC20Theorems - ソース:
JpycFormalVerification/ERC20Theorems.lean:645-652 - 概要: from == to の transferFrom は全残高を変えない（自己送金の安全性）、という定理。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {frm : JPYC.Address} {value : JPYC.U256}, Eq (JPYC.transferFrom s ctx frm frm value) (Except.ok s') → Eq s'.balances s.balances支払者 frm と受取人が等しい（自己送金）とき、transferFrom が成功するなら全アカウントの残高が変わらない、という定理です。
和訳 docstring
自己送金。 from == to のとき、成功した transferFrom はすべての残高を変えない（許可額ステップは残高を動かさず、引いた分は足し戻されて元に戻る）。
解説
何を述べているか。 同一アドレスへの第三者送金は、成功しても残高分布をまったく変えません（s'.balances = s.balances）。transfer_self の transferFrom 版です。
直感。 transferFrom_eq_ok で許可額ステップ s₁ と内部送金 _transfer s₁ frm frm value に分解します。許可額ステップは残高を動かさず（transferFrom_step_balances）、内部送金は「引いてから足す」の 2 段で、送り手 = 受け手なら引いた直後の値から足し戻すのでちょうど元に戻ります（checked な sub?→add? の相殺）。
なぜ安全性に効くか。 「自己送金で残高が壊れる」類のバグ（二重計上・消失）が、代理送金 transferFrom の経路でも起きないことを保証します。from == to という境界ケースを明示的に安全だと確定する、堅牢性の証です。
図解
Lean ソースコード
lean
/-- **Self-transfer.** When `from == to`, a successful `transferFrom` leaves every
balance unchanged (the allowance step does not move balances; the debit is
restored by the credit). -/
theorem transferFrom_self {s s' : State} {ctx : CallContext} {frm : Address} {value : U256}
(h : transferFrom s ctx frm frm value = .ok s') : s'.balances = s.balances := by
obtain ⟨s₁, hstep, htrans⟩ := transferFrom_eq_ok h
obtain ⟨hbal, _, _⟩ := transferFrom_step_balances hstep
rw [_transfer_self htrans, hbal]