JPYC.transferFrom_frame
名称・種別
- 名称:
JPYC.transferFrom_frame - 種別: theorem
- モジュール:
JpycFormalVerification.ERC20Theorems - ソース:
JpycFormalVerification/ERC20Theorems.lean:636-643 - 概要: transferFrom は from・to 以外の口座残高を変えない、という frame 定理。
- 仕様: 対象
型シグネチャ
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') → ∀ {a : JPYC.Address}, Ne a frm → Ne a dst → Eq (s'.balances a) (s.balances a)transferFrom が成功したとき、支払者 frm でも受取人 dst でもない任意のアカウント a の残高は変わらない、という定理です。
和訳 docstring
フレーム性。 成功した transferFrom は、支払者（frm）・受取人（dst）以外のすべての残高を変えない。
解説
何を述べているか。 フレーム性の言明です。第三者送金 transferFrom も当事者 2 人（frm・dst）の残高しか動かさず、それ以外のアカウント a（a ≠ frm かつ a ≠ dst）の残高は一切影響を受けません。transfer_frame の transferFrom 版です。
直感。 transferFrom_eq_ok で許可額ステップ s₁ と内部送金に分解します。許可額ステップは残高を動かさず（transferFrom_step_balances）、内部送金 _transfer は balances の 2 点だけを Function.update するので、3 点目以降は update_of_ne により据え置きです。
なぜ安全性に効くか。 「他人が代理で行う送金でも、無関係な第三者の残高を勝手に変えない」という分離保証です。意図しない副作用がなく、送金の影響範囲が当事者に限定されることを数学的に確定します。
図解
Lean ソースコード
lean
/-- **Frame.** A successful `transferFrom` leaves every balance other than the
payer's (`frm`) and payee's (`dst`) untouched. -/
theorem transferFrom_frame {s s' : State} {ctx : CallContext} {frm dst : Address} {value : U256}
(h : transferFrom s ctx frm dst value = .ok s') {a : Address}
(ha1 : a ≠ frm) (ha2 : a ≠ dst) : s'.balances a = s.balances a := by
obtain ⟨s₁, hstep, htrans⟩ := transferFrom_eq_ok h
obtain ⟨hbal, _, _⟩ := transferFrom_step_balances hstep
rw [_transfer_frame htrans ha1 ha2, hbal]