JPYCv2 形式検証

外観

JPYC.burn_frame ​

名称・種別 ​

  • 名称: JPYC.burn_frame
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:553-559
  • 概要: burn は呼び出し元以外の残高を変えない、という frame 定理。
  • 仕様: 対象

型シグネチャ ​

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

burn は、呼び出し元 sender 以外のすべてのアドレスの残高を変えない、というフレーム定理です。

和訳 docstring ​

フレーム。 burn は呼び出し元以外のすべての残高を変えない。

解説 ​

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

直感。 「お金を焼いても、焼いた本人以外の財布には触れない」。

なぜ安全性に効くか。 フレーム性 の保証です。焼却が局所的（呼び出し元 1 人だけに作用）であり、第三者の残高が巻き込まれないことを示します。

図解 ​

Lean ソースコード ​

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

依存 ​