JPYC.wf_transferFrom

名称・種別

名称: JPYC.wf_transferFrom
種別: theorem
モジュール: JpycFormalVerification.ERC20Theorems
ソース: JpycFormalVerification/ERC20Theorems.lean:417-422
概要: transferFrom は健全性不変条件 WF を保つ、という定理。
仕様: 対象

型シグネチャ

lean

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

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

解説

何を述べているか。 第三者送金は健全性不変条件 WF を保ちます。許可額・残高は変わってもフラグ・バージョンには触れないからです。

直感。 transferFrom_eq_ok で分解し、transferFrom_step_balances の WF s → WF s₁ で中間状態の整合性を得て、_transfer_wf で最終状態へ繋ぎます。

なぜ安全性に効くか。 transferFrom 後もフラグが 0/1 を保ち、ブロックリスト・許可リスト判定が意味を持ち続けます。価値移動のすべての経路で WF が保存される、という一貫性を保証します。

図解

Lean ソースコード

lean

/-- **WF preservation** for `transferFrom`. -/
theorem wf_transferFrom {s s' : State} {ctx : CallContext} {frm dst : Address} {value : U256}
    (hwf : WF s) (h : transferFrom s ctx frm dst value = .ok s') : WF s' := by
  obtain ⟨s₁, hstep, htrans⟩ := transferFrom_eq_ok h
  obtain ⟨_, _, hwfimp⟩ := transferFrom_step_balances hstep
  exact _transfer_wf (hwfimp hwf) htrans

JPYC.wf_transferFrom ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.wf_transferFrom

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存