JPYCv2 形式検証

外観

JPYC.transferFrom_guards ​

名称・種別 ​

  • 名称: JPYC.transferFrom_guards
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:706-715
  • 概要: 成功した transferFrom のガード事実をまとめた補題。
  • 仕様: 対象外

型シグネチャ ​

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.paused Bool.false) (And (Eq (s.blocklisted ctx.sender) 0) (And (Eq (s.blocklisted frm) 0) (And (Eq (s.blocklisted dst) 0) (GT.gt value JPYC.allowlistLimitAmount → Eq (s.allowlisted frm) 1))))

transferFrom の成功が含意するガード事実（停止中でない・支払い者と送金元と受取人は未ブロック・上限超なら送金元は許可リスト登録済み）をまとめて取り出す補題です。

解説 ​

何を述べているか。 transferFrom が成功したなら、s.paused = false、s.blocklisted sender = 0、s.blocklisted frm = 0、s.blocklisted dst = 0、そして「value > allowlistLimitAmount ならば s.allowlisted frm = 1」が成り立ちます。

直感。 第三者送金が満たすべき条件を 1 本にまとめたものです。transfer と違い、ブロック検査は 3 者（msg.sender・frm・dst）に及びます。

なぜ安全性に効くか。 transferFrom_not_blocklisted と transferFrom_above_cap_allowlisted を、この 1 本から導きます。

図解 ​

Lean ソースコード ​

lean
theorem transferFrom_guards {s s' : State} {ctx : CallContext} {frm dst : Address} {value : U256}
    (h : transferFrom s ctx frm dst value = .ok s') :
    s.paused = false ∧ s.blocklisted ctx.sender = 0 ∧ s.blocklisted frm = 0 ∧
      s.blocklisted dst = 0 ∧ (value > allowlistLimitAmount → s.allowlisted frm = 1) := by
  unfold transferFrom whenNotPaused notBlocklisted at h
  obtain ⟨hp, h⟩ := req_bind_eq_ok h
  obtain ⟨hb0, h⟩ := req_bind_eq_ok h
  obtain ⟨hb1, h⟩ := req_bind_eq_ok h
  obtain ⟨hb2, h⟩ := req_bind_eq_ok h
  exact ⟨hp, hb0, hb1, hb2, fun hc => checkAllowlist_bind_cap h hc⟩

依存 ​