JPYCv2 形式検証

外観

JPYC.transferFrom_not_blocklisted ​

名称・種別 ​

  • 名称: JPYC.transferFrom_not_blocklisted
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:724-729
  • 概要: transferFrom の成功は spender・payer・payee がいずれも非ブロックリストであることを含意する。
  • 仕様: 対象

型シグネチャ ​

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

transferFrom の成功は、支払い者・送金元・受取人のいずれもブロックリストに載っていなかったことを含意する、という定理です。

和訳 docstring ​

transferFrom の成功は、支払い者・送金元・受取人のいずれもブロックされていなかったことを含意する。

解説 ​

何を述べているか。 transferFrom が成功したなら s.blocklisted sender = 0、s.blocklisted frm = 0、s.blocklisted dst = 0 の 3 つが成り立ちます。transferFrom_guards から取り出します。

直感。 第三者送金では関与者が 3 人（実行する msg.sender・資金の出どころ frm・受取人 dst）。そのいずれか 1 人でもブロックされていれば、送金は失敗します。

なぜ安全性に効くか。 凍結アカウントが、代理人を立てても・代理人として動いても取引に関われないことを保証します。ブロックリストの抜け穴を塞ぐ性質です。

図解 ​

Lean ソースコード ​

lean
/-- A successful `transferFrom` implies the spender, payer, and payee were all
not blocklisted. -/
theorem transferFrom_not_blocklisted {s s' : State} {ctx : CallContext} {frm dst : Address}
    {value : U256} (h : transferFrom s ctx frm dst value = .ok s') :
    s.blocklisted ctx.sender = 0 ∧ s.blocklisted frm = 0 ∧ s.blocklisted dst = 0 :=
  ⟨(transferFrom_guards h).2.1, (transferFrom_guards h).2.2.1, (transferFrom_guards h).2.2.2.1⟩

依存 ​