JPYCv2 形式検証

外観

JPYC.transfer_eq_ok ​

名称・種別 ​

  • 名称: JPYC.transfer_eq_ok
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:315-323
  • 概要: 成功した transfer は呼び出し元からの _transfer の成功に還元される、という補題。
  • 仕様: 対象外

型シグネチャ ​

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

transfer s ctx dst value が Except.ok s' で成功するなら、内部の _transfer s ctx.sender dst value も同じ s' で成功する、という還元定理です。

和訳 docstring ​

成功した transfer は、呼び出し元を送り手とする _transfer の成功に還元される。

解説 ​

何を述べているか。 外部関数 transfer の成功は、4 つのガードを通過した後の内部送金 _transfer（送り手 = ctx.sender）の成功にそのまま等しい、と示します。

直感。 ガード（whenNotPaused・notBlocklisted×2・checkAllowlist）は成功時には状態を変えない「素通り」なので、transfer の中身は _transfer に一致します。証明は req_bind_eq_ok でガードを 3 枚剥がし、最後に checkAllowlist_bind_eq_ok で allowlist 検査を吸収します。

なぜ安全性に効くか。 この 1 本があるおかげで、transfer についてのすべての性質（供給保存・フレーム性・自己送金など）を、_transfer について証明済みの補題を「持ち上げる」だけで導けます。外部関数とその本体をつなぐ要石です。

図解 ​

Lean ソースコード ​

lean
/-- A successful `transfer` reduces to a successful `_transfer` from the caller. -/
theorem transfer_eq_ok {s s' : State} {ctx : CallContext} {dst : Address} {value : U256}
    (h : transfer s ctx dst value = .ok s') :
    _transfer s ctx.sender dst value = .ok s' := by
  unfold transfer whenNotPaused notBlocklisted at h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  exact checkAllowlist_bind_eq_ok h

依存 ​