JPYCv2 形式検証

外観

JPYC.transfer_conserves ​

名称・種別 ​

  • 名称: JPYC.transfer_conserves
  • 種別: theorem
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:329-331
  • 概要: transfer は供給保存不変条件 SupplyConserved を保つ、という定理。
  • 仕様: 対象

型シグネチャ ​

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

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

解説 ​

何を述べているか。 送金は供給保存不変条件 SupplyConserved を保ちます。totalSupply = 全残高の合計 という等式が、送金の前後で崩れません。

直感。 送金は「送り手から引いた額を、受け手にそのまま足す」だけ。全体の合計は変わらないので、合計と一致していた totalSupply も一致したままです（sum_double_update_nat が支える）。

なぜ安全性に効くか。 ステーブルコインの根幹「お金が勝手に増減しない」を送金について保証します。transfer_eq_ok で _transfer に還元し、_transfer_conserves を適用します。

図解 ​

Lean ソースコード ​

lean
theorem transfer_conserves {s s' : State} {ctx : CallContext} {dst : Address} {value : U256}
    (hc : SupplyConserved s) (h : transfer s ctx dst value = .ok s') : SupplyConserved s' :=
  _transfer_conserves hc (transfer_eq_ok h)

依存 ​