JPYCv2 形式検証

外観

JPYC.transferWithAuthorization_totalSupply ​

名称・種別 ​

  • 名称: JPYC.transferWithAuthorization_totalSupply
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:380-387
  • 概要: transferWithAuthorization は totalSupply を変えない、という定理。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {frm dst : JPYC.Address} {value validAfter validBefore : JPYC.U256} {nonce : JPYC.Bytes32} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s') → Eq s'.totalSupply s.totalSupply

transferWithAuthorization の成功は、総供給 totalSupply を変えない、という効果定理です。

和訳 docstring ​

効果（供給）。 transferWithAuthorization は totalSupply を変えない。

解説 ​

何を述べているか。 transferWithAuthorization が成功すると s'.totalSupply = s.totalSupply です。authorization のマーク（setAuthorizationState）は総供給に触れず、内部 _transfer も総供給を保つ（_transfer_totalSupply）ので、総供給は不変です。

直感。 「送金は所有者の付け替えであって、トークンの総量は変わらない」を確認します。

なぜ安全性に効くか。 供給保存（transferWithAuthorization_conserves）の片側です。署名つき送金が発行・焼却ではないこと（総量に中立）を明示します。

図解 ​

Lean ソースコード ​

lean
/-- **Supply (totalSupply).** `transferWithAuthorization` leaves `totalSupply` fixed. -/
theorem transferWithAuthorization_totalSupply {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32}
    (h : transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s') :
    s'.totalSupply = s.totalSupply := by
  obtain ⟨_, _, _, _, htr⟩ := _transferWithAuthorization_ok (transferWithAuthorization_eq_ok h)
  rw [_transfer_totalSupply htr]; rfl

依存 ​