JPYCv2 形式検証

外観

JPYC.transfer_guards ​

名称・種別 ​

  • 名称: JPYC.transfer_guards
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:696-704
  • 概要: 成功した 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.paused Bool.false) (And (Eq (s.blocklisted ctx.sender) 0) (And (Eq (s.blocklisted dst) 0) (GT.gt value JPYC.allowlistLimitAmount → Eq (s.allowlisted ctx.sender) 1)))

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

解説 ​

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

直感。 送金が満たすべきアクセス制御条件を 1 本にまとめた「成功 ⇒ 前提一式」です。req_bind_eq_ok でガードを剝がし、条件付き含意は checkAllowlist_bind_cap で得ます。

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

図解 ​

Lean ソースコード ​

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

依存 ​