JPYCv2 形式検証

外観

JPYC.transfer_self ​

名称・種別 ​

  • 名称: JPYC.transfer_self
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:342-344
  • 概要: from == to の transfer は全残高を変えない（自己送金の安全性）、という定理。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {value : JPYC.U256}, Eq (JPYC.transfer s ctx ctx.sender value) (Except.ok s') → Eq s'.balances s.balances

dst が呼び出し元 ctx.sender と等しい（自己送金）とき、transfer が成功するなら全アカウントの残高が変わらない、という定理です。

解説 ​

何を述べているか。 自分自身への送金は、成功しても残高分布をまったく変えません。s'.balances = s.balances（マッピング全体が一致）。

直感。 送金は「引いてから足す」の 2 段。送り手 = 受け手なら、引いた直後の残高から足し戻すので、ちょうど元に戻ります（transferResult の構造）。checked 演算の往復 sub?→add? がぴったり相殺します。

なぜ安全性に効くか。 「自己送金で残高が壊れる」類のバグ（二重計上・消失）が無いことを保証します。from == to という境界ケースを明示的に安全だと確定する、堅牢性の証です。

図解 ​

Lean ソースコード ​

lean
theorem transfer_self {s s' : State} {ctx : CallContext} {value : U256}
    (h : transfer s ctx ctx.sender value = .ok s') : s'.balances = s.balances :=
  _transfer_self (transfer_eq_ok h)

依存 ​