JPYCv2 形式検証

外観

JPYC.transfer_frame ​

名称・種別 ​

  • 名称: JPYC.transfer_frame
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:337-340
  • 概要: transfer は from・to 以外の口座残高を変えない、という frame 定理。
  • 仕様: 対象

型シグネチャ ​

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

transfer が成功したとき、送り手 ctx.sender でも受取人 dst でもない任意のアカウント a の残高は変わらない、という定理です。

解説 ​

何を述べているか。 フレーム性の言明です。送金は当事者 2 人の残高しか動かさず、それ以外のアカウント a（a ≠ sender かつ a ≠ dst）の残高は一切影響を受けません。

直感。 送金は balances の 2 点だけを Function.update します。3 点目以降には update_of_ne（更新点と違う鍵は不変）が働き、残高は据え置きです。

なぜ安全性に効くか。 「他人の取引が、自分の残高を勝手に変えない」という分離保証です。意図しない副作用がないこと、つまり送金の影響範囲が当事者に限定されることを数学的に確定します。

図解 ​

Lean ソースコード ​

lean
theorem transfer_frame {s s' : State} {ctx : CallContext} {dst : Address} {value : U256}
    (h : transfer s ctx dst value = .ok s') {a : Address}
    (ha1 : a ≠ ctx.sender) (ha2 : a ≠ dst) : s'.balances a = s.balances a :=
  _transfer_frame (transfer_eq_ok h) ha1 ha2

依存 ​