JPYCv2 形式検証

外観

JPYC.transfer_le ​

名称・種別 ​

  • 名称: JPYC.transfer_le
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:346-349
  • 概要: 成功した transfer は呼び出し元の残高を桁借りしない（value ≤ 残高）、という定理。
  • 仕様: 対象

型シグネチャ ​

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

transfer が成功するなら、送金額 value は呼び出し元の残高 s.balances ctx.sender 以下である、という定理です。

和訳 docstring ​

成功した transfer は、呼び出し元の残高をアンダーフローさせない。

解説 ​

何を述べているか。 送金が成功した以上、その額は送り手の残高を超えていなかった、と逆向きに保証します（value ≤ balance）。

直感。 _transfer 内の require(value ≤ balance) を通過しなければ成功しません。成功という結果から、この前提が満たされていたことを取り出します。

なぜ安全性に効くか。 「残高以上は送れない」= アンダーフロー（残高が負に回り込む）が起きないことの保証です。checked な sub? と合わせ、残高が不正な巨大値に化けることを二重に防ぎます。

図解 ​

Lean ソースコード ​

lean
/-- A successful `transfer` cannot underflow the caller's balance. -/
theorem transfer_le {s s' : State} {ctx : CallContext} {dst : Address} {value : U256}
    (h : transfer s ctx dst value = .ok s') : value ≤ s.balances ctx.sender :=
  _transfer_le (transfer_eq_ok h)

依存 ​