JPYCv2 形式検証

外観

JPYC.transferWithAuthorization_guards ​

名称・種別 ​

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

型シグネチャ ​

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

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

解説 ​

何を述べているか。 transferWithAuthorization が成功したなら、s.paused = false、送金元（from）・受取人（to）がいずれも未ブロック（blocklisted … = 0）、そして「金額が上限 allowlistLimitAmount を超えるなら s.allowlisted frm = 1」がすべて成り立ちます。

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

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

図解 ​

Lean ソースコード ​

lean
theorem transferWithAuthorization_guards {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32}
    (h : transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s') :
    s.paused = false ∧ s.blocklisted frm = 0 ∧ s.blocklisted dst = 0 ∧
      (value > allowlistLimitAmount → s.allowlisted frm = 1) := by
  unfold transferWithAuthorization 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⟩

依存 ​