JPYCv2 形式検証

外観

JPYC.permit_guards ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {owner spender : JPYC.Address} {value deadline : JPYC.U256} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.permit O s ctx owner spender value deadline v r sig) (Except.ok s') → And (Eq s.paused Bool.false) (And (Eq (s.blocklisted owner) 0) (And (Eq (s.blocklisted spender) 0) (GT.gt value JPYC.allowlistLimitAmount → Eq (s.allowlisted owner) 1)))

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

解説 ​

何を述べているか。 permit が成功したなら、s.paused = false、送り手（owner）・支出者（spender）がいずれも未ブロック（blocklisted … = 0）、そして「金額が上限 allowlistLimitAmount を超えるなら s.allowlisted owner = 1」がすべて成り立ちます。

直感。 多重 modifier を 1 本にまとめた「成功 ⇒ 前提条件一式」です。req_bind_eq_ok でガードを順に剝がし、最後の条件付き含意は checkAllowlist_bind_cap で得ます。

なぜ安全性に効くか。 停止・ブロックリスト・許可リストの各相互作用定理（*_paused / *_not_blocklisted / *_above_cap_allowlisted）を、この 1 本から枝分かれで導きます。署名操作が満たすべきアクセス制御条件を一望できます。

図解 ​

Lean ソースコード ​

lean
theorem permit_guards {O : SigOracle} {s s' : State} {ctx : CallContext} {owner spender : Address}
    {value deadline : U256} {v : U8} {r sig : Bytes32}
    (h : permit O s ctx owner spender value deadline v r sig = .ok s') :
    s.paused = false ∧ s.blocklisted owner = 0 ∧ s.blocklisted spender = 0 ∧
      (value > allowlistLimitAmount → s.allowlisted owner = 1) := by
  unfold permit 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⟩

依存 ​