JPYCv2 形式検証

外観

JPYC.mint_guards ​

名称・種別 ​

  • 名称: JPYC.mint_guards
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:421-432
  • 概要: 成功した mint のガード事実（minter であること・非ブロックリスト・上限超は許可登録）をまとめた補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {dst : JPYC.Address} {amount : JPYC.U256}, Eq (JPYC.mint s ctx dst amount) (Except.ok s') → And (Eq s.paused Bool.false) (And (Eq (s.minters ctx.sender) Bool.true) (And (Eq (s.blocklisted ctx.sender) 0) (And (Eq (s.blocklisted dst) 0) (GT.gt amount JPYC.allowlistLimitAmount → Eq (s.allowlisted ctx.sender) 1))))

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

和訳 docstring ​

mint 成功が含意するガード事実（呼び出し元はミンター、両者ともブロックされていない、上限超のミントは呼び出し元の許可リスト登録を要する）。

解説 ​

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

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

なぜ安全性に効くか。 mint_auth・mint_not_blocklisted・mint_above_cap_allowlisted を、この 1 本から枝分かれで導きます。発行が満たすべきアクセス制御条件を一望できます。

図解 ​

Lean ソースコード ​

lean
/-- The guard facts of a successful `mint` (caller is a minter; neither party
blocklisted; above-cap mints require an allowlisted caller). -/
theorem mint_guards {s s' : State} {ctx : CallContext} {dst : Address} {amount : U256}
    (h : mint s ctx dst amount = .ok s') :
    s.paused = false ∧ s.minters ctx.sender = true ∧ s.blocklisted ctx.sender = 0 ∧
      s.blocklisted dst = 0 ∧ (amount > allowlistLimitAmount → s.allowlisted ctx.sender = 1) := by
  unfold mint whenNotPaused onlyMinters notBlocklisted at h
  obtain ⟨hp, h⟩ := req_bind_eq_ok h
  obtain ⟨hm, h⟩ := req_bind_eq_ok h
  obtain ⟨hb1, h⟩ := req_bind_eq_ok h
  obtain ⟨hb2, h⟩ := req_bind_eq_ok h
  exact ⟨hp, hm, hb1, hb2, fun hc => checkAllowlist_bind_cap h hc⟩

依存 ​