JPYCv2 形式検証

外観

JPYC.mint_not_blocklisted ​

名称・種別 ​

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

型シグネチャ ​

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

mint の成功は、呼び出し元（ミンター）と受取人がブロックリストに載っていなかったことを含意する、という定理です。

和訳 docstring ​

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

解説 ​

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

直感。 「ブロックされたミンターは発行できず、ブロックされたアドレスは受け取れない」。

なぜ安全性に効くか。 凍結対象が発行の経路でトークンを得る抜け道を塞ぎます。ミンター自身が制裁対象になった場合も、発行が止まることを保証します。

図解 ​

Lean ソースコード ​

lean
/-- A successful `mint` implies the caller and recipient were not blocklisted. -/
theorem mint_not_blocklisted {s s' : State} {ctx : CallContext} {dst : Address} {amount : U256}
    (h : mint s ctx dst amount = .ok s') :
    s.blocklisted ctx.sender = 0 ∧ s.blocklisted dst = 0 :=
  ⟨(mint_guards h).2.2.1, (mint_guards h).2.2.2.1⟩

依存 ​