JPYCv2 形式検証

外観

JPYC.mint_frame ​

名称・種別 ​

  • 名称: JPYC.mint_frame
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:468-474
  • 概要: mint は受取人以外の残高を変えない、という frame 定理。
  • 仕様: 対象

型シグネチャ ​

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

mint は、受取人 dst 以外のすべてのアドレスの残高を変えない、というフレーム定理です。

和訳 docstring ​

フレーム。 mint は受取人以外のすべての残高を変えない。

解説 ​

何を述べているか。 mint が成功したとき、dst と異なる任意のアドレス a について s'.balances a = s.balances a です。mint_eq の結果状態に対し、balances を触る更新は setBalance dst nb だけなので、a ≠ dst では Function.update_of_ne で元の値に戻ります。

直感。 「お金を刷っても、受取人以外の財布には一切手を触れない」。総供給と許可量の更新は balances を変えないことに注意します。

なぜ安全性に効くか。 フレーム性 は「無関係なアカウントが巻き込まれない」という基本的な安全性です。発行が局所的（受取人 1 人だけに作用）であることを保証し、第三者の残高が勝手に動く可能性を排除します。

図解 ​

Lean ソースコード ​

lean
/-- **Frame.** `mint` leaves every balance other than the recipient's unchanged. -/
theorem mint_frame {s s' : State} {ctx : CallContext} {dst : Address} {amount : U256}
    (h : mint s ctx dst amount = .ok s') {a : Address} (ha : a ≠ dst) :
    s'.balances a = s.balances a := by
  obtain ⟨ns, nb, nma, _, _, _, rfl⟩ := mint_eq h
  simp only [setMinterAllowed_balances, setBalance_balances, setTotalSupply_balances]
  rw [Function.update_of_ne ha]

依存 ​