JPYCv2 形式検証

外観

JPYC.checkAllowlist_bind_cap ​

名称・種別 ​

  • 名称: JPYC.checkAllowlist_bind_cap
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:73-81
  • 概要: 上限超の額で checkAllowlist が通れば当該口座は許可登録済み、という補題（V2 cap 分岐）。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {α : Type} {s : JPYC.State} {acc : JPYC.Address} {value : JPYC.U256} {f : Unit → Except JPYC.Error α} {b : α}, Eq (Except.instMonad.bind (JPYC.checkAllowlist s acc value) f) (Except.ok b) → GT.gt value JPYC.allowlistLimitAmount → Eq (s.allowlisted acc) 1

checkAllowlist s acc value のあとに処理が続く形が成功し、かつ value が上限 allowlistLimitAmount を超えるなら、acc は許可リスト登録済み（allowlisted[acc] = 1）である、という補題です。

和訳 docstring ​

上限超の値で checkAllowlist が成功するなら、そのアカウントは許可リスト登録済み（V2 checkAllowlist の上限枝）。

解説 ​

何を述べているか。 checkAllowlist は「金額が上限を超えるときだけ、送り手の許可リスト登録を要求する」ガードです。その合成が成功し、しかも金額が上限超なら、require の枝が通ったということなので allowlisted[acc] = 1 が確定します。

直感。 「10 万トークン超を動かせたのなら、その人は必ず許可リストに載っていた」という、上限突破の前提条件を取り出します。証明は上限超の枝（if_pos）に入って req_bind_eq_ok で条件を抜き出すだけです。

なぜ安全性に効くか。 許可リスト・キャップ（transfer_above_cap_allowlisted / transferFrom_above_cap_allowlisted / mint_above_cap_allowlisted）の中核です。大口取引を「登録済みアカウントのみ」に閉じ込める性質を、これが下支えします。

図解 ​

Lean ソースコード ​

lean
/-- `checkAllowlist` succeeding for an above-cap value forces the account to be
allowlisted (the cap branch of the V2 `checkAllowlist` modifier). -/
theorem checkAllowlist_bind_cap {α : Type} {s : State} {acc : Address} {value : U256}
    {f : Unit → Except Error α} {b : α}
    (h : (checkAllowlist s acc value >>= f) = .ok b) (hcap : value > allowlistLimitAmount) :
    s.allowlisted acc = 1 := by
  unfold checkAllowlist at h
  rw [if_pos hcap] at h
  exact (req_bind_eq_ok h).1

依存 ​