JPYCv2 形式検証

外観

JPYC.transferWithAuthorization_conserves ​

名称・種別 ​

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

型シグネチャ ​

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}, JPYC.SupplyConserved s → Eq (JPYC.transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s') → JPYC.SupplyConserved s'

transferWithAuthorization が成功するなら、結果状態も SupplyConserved を満たす、という供給保存の定理です。

和訳 docstring ​

transferWithAuthorization の 供給保存。

解説 ​

何を述べているか。 事前状態が SupplyConserved を満たし、transferWithAuthorization が成功して s' になれば、s' も供給保存を満たします。送金は内部で Phase 1 の _transfer を使うため、その供給保存補題（_transfer_conserves）を再利用します。

直感。 送金は「from の残高が減り、to の残高が同じだけ増える」ので、残高総和は不変。総供給も動かないので、等式は保たれます。

なぜ安全性に効くか。 署名つき送金でも「お金が湧いたり消えたりしない」という会計健全性が崩れないことを保証します。

図解 ​

Lean ソースコード ​

lean
/-- **Supply conservation** for `transferWithAuthorization`. -/
theorem transferWithAuthorization_conserves {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32} (hc : SupplyConserved s)
    (h : transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s') :
    SupplyConserved s' := by
  obtain ⟨_, _, _, _, htr⟩ := _transferWithAuthorization_ok (transferWithAuthorization_eq_ok h)
  refine _transfer_conserves ?_ htr
  exact supplyConserved_of_balances_totalSupply_eq hc rfl rfl

依存 ​