JPYCv2 形式検証

外観

JPYC.transferFrom_above_cap_allowlisted ​

名称・種別 ​

  • 名称: JPYC.transferFrom_above_cap_allowlisted
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:749-754
  • 概要: 上限超の transferFrom 成功は payer(from) が許可登録済みであることを含意する。
  • 仕様: 対象

型シグネチャ ​

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') → GT.gt value JPYC.allowlistLimitAmount → Eq (s.allowlisted frm) 1

transferFrom で allowlistLimitAmount（上限額）を超える額が成功したなら、送金元（from）は許可リスト登録済み（allowlisted frm = 1）だった、という許可リスト・キャップの定理です。

和訳 docstring ​

allowlistLimitAmount を超える transferFrom の成功は、送金元（from）が許可リスト登録済みだったことを含意する。

解説 ​

何を述べているか。 transferFrom が成功し、かつ金額が上限 allowlistLimitAmount を超えるなら、allowlisted frm = 1、すなわち送金元（from）が許可リストに載っていたことが導けます。*_guards の条件付き含意に「上限超」という仮定を当てて得ます（おおもとは checkAllowlist_bind_cap）。

直感。 checkAllowlist ガードの対偶です。「大口（10 万トークン超）が通った ⇒ その人は登録済みだった」。逆に言えば、未登録なら上限超の取引は必ず失敗します。

なぜ安全性に効くか。 JPYC 固有の 送金上限つき許可リスト の中心的保証です。大口の資金移動を「事前に審査・登録されたアカウントだけ」に限定し、未知のアドレスによる大量送金を防ぎます。

図解 ​

Lean ソースコード ​

lean
/-- A successful `transferFrom` of more than `allowlistLimitAmount` implies the
payer (`from`) was allowlisted. -/
theorem transferFrom_above_cap_allowlisted {s s' : State} {ctx : CallContext} {frm dst : Address}
    {value : U256} (h : transferFrom s ctx frm dst value = .ok s')
    (hcap : value > allowlistLimitAmount) : s.allowlisted frm = 1 :=
  (transferFrom_guards h).2.2.2.2 hcap

依存 ​