JPYC.transferFrom_le
名称・種別
- 名称:
JPYC.transferFrom_le - 種別: theorem
- モジュール:
JpycFormalVerification.ERC20Theorems - ソース:
JpycFormalVerification/ERC20Theorems.lean:628-634 - 概要: 成功した transferFrom は支払者の残高を桁借りしない（value ≤ 残高）、という定理。
- 仕様: 対象
型シグネチャ
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') → instLEBitVec.le value (s.balances frm)transferFrom が成功するなら、送金額 value は支払者 frm の残高 s.balances frm 以下である、という定理です。
和訳 docstring
アンダーフローなし。 成功した transferFrom は、支払者の残高をアンダーフローさせない（value ≤ balance from）。
解説
何を述べているか。 transfer_le の transferFrom 版です。送金が成功した以上、その額は支払者 frm の残高を超えていなかった、と逆向きに保証します（value ≤ balance from）。
直感。 transferFrom_eq_ok で許可額ステップ s₁ と内部送金 _transfer s₁ frm dst value に分解します。許可額ステップは残高に触れないので（transferFrom_step_balances が s₁.balances = s.balances を与える）、内部送金の require(value ≤ balance) から取り出した _transfer_le の不等式をそのまま s の残高に読み替えられます。
なぜ安全性に効くか。 「残高以上は送れない」= アンダーフロー（残高が負に回り込む）が起きないことの保証です。checked な sub? と合わせ、第三者送金 transferFrom でも残高が不正な巨大値に化けないことを確定します（checked 演算）。
図解
Lean ソースコード
lean
/-- **No underflow.** A successful `transferFrom` cannot underflow the payer's
balance: `value ≤ balance from`. -/
theorem transferFrom_le {s s' : State} {ctx : CallContext} {frm dst : Address} {value : U256}
(h : transferFrom s ctx frm dst value = .ok s') : value ≤ s.balances frm := by
obtain ⟨s₁, hstep, htrans⟩ := transferFrom_eq_ok h
obtain ⟨hbal, _, _⟩ := transferFrom_step_balances hstep
rw [← hbal]; exact _transfer_le htrans