JPYC.wf_transfer

名称・種別

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

型シグネチャ

lean

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

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

解説

何を述べているか。 送金は健全性不変条件 WF を壊しません。整合した状態から始めた transfer の結果は、再び整合しています。

直感。 transfer が変えるのは残高だけ。WF が見るフラグ・バージョンには触れないので、WF.of_flags_eq によって整合性が保たれます。証明は transfer_eq_ok で _transfer に還元し、_transfer_wf を適用するだけです。

なぜ安全性に効くか。 「正規の操作だけを続ける限り、フラグが壊れた値（2 など）にならない」を送金についても担保します。ブロックリスト判定などフラグに依存する全ロジックの前提が、送金後も成り立ち続けます。

図解

Lean ソースコード

lean

theorem wf_transfer {s s' : State} {ctx : CallContext} {dst : Address} {value : U256}
    (hwf : WF s) (h : transfer s ctx dst value = .ok s') : WF s' :=
  _transfer_wf hwf (transfer_eq_ok h)

JPYC.wf_transfer ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.wf_transfer

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存