JPYCv2 形式検証

外観

JPYC.transfer_not_blocklisted ​

名称・種別 ​

  • 名称: JPYC.transfer_not_blocklisted
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:717-722
  • 概要: transfer の成功は送り手・受け手の誰もブロックリストされていないことを含意する。
  • 仕様: 対象

型シグネチャ ​

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

transfer の成功は、送り手も受取人もブロックリストに載っていなかったことを含意する、というブロックリスト相互作用の定理です。

和訳 docstring ​

transfer の成功は、送り手も受取人もブロックされていなかったことを含意する。

解説 ​

何を述べているか。 transfer が成功したなら s.blocklisted sender = 0 ∧ s.blocklisted dst = 0 です。transfer_guards の該当成分を取り出します。

直感。 notBlocklisted ガードの対偶です。「送金が通った ⇒ どちらもブロックされていなかった」。逆に言えば、どちらかがブロック済みなら送金は必ず失敗します。

なぜ安全性に効くか。 ブロックリストの意味 ―― 凍結アカウントは 送れも受け取れもしない ―― を、送金について厳密に保証します。制裁・不正対応の実効性の根拠です。

図解 ​

Lean ソースコード ​

lean
/-- A successful `transfer` implies neither the sender nor the recipient was
blocklisted. -/
theorem transfer_not_blocklisted {s s' : State} {ctx : CallContext} {dst : Address} {value : U256}
    (h : transfer s ctx dst value = .ok s') :
    s.blocklisted ctx.sender = 0 ∧ s.blocklisted dst = 0 :=
  ⟨(transfer_guards h).2.1, (transfer_guards h).2.2.1⟩

依存 ​