JPYCv2 形式検証

外観

JPYC.burn_not_blocklisted ​

名称・種別 ​

  • 名称: JPYC.burn_not_blocklisted
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:737-739
  • 概要: burn の成功は呼び出し元が非ブロックリストであることを含意する。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {amount : JPYC.U256}, Eq (JPYC.burn s ctx amount) (Except.ok s') → Eq (s.blocklisted ctx.sender) 0

burn の成功は、呼び出し元がブロックリストに載っていなかったことを含意する、という定理です。

和訳 docstring ​

burn の成功は、呼び出し元がブロックされていなかったことを含意する。

解説 ​

何を述べているか。 burn が成功したなら s.blocklisted sender = 0 です。burn_guards から取り出します。

直感。 「ブロックされたミンターは焼却もできない」。burn は自分のトークンを焼くだけなので、関与者は呼び出し元 1 人です。

なぜ安全性に効くか。 凍結中のアカウントは残高を動かす一切の操作（送金・受領・焼却）から排除される、という一貫性を保ちます。

図解 ​

Lean ソースコード ​

lean
/-- A successful `burn` implies the caller was not blocklisted. -/
theorem burn_not_blocklisted {s s' : State} {ctx : CallContext} {amount : U256}
    (h : burn s ctx amount = .ok s') : s.blocklisted ctx.sender = 0 := (burn_guards h).2.2

依存 ​