JPYCv2 形式検証

外観

JPYC.burn_guards ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {amount : JPYC.U256}, Eq (JPYC.burn s ctx amount) (Except.ok s') → And (Eq s.paused Bool.false) (And (Eq (s.minters ctx.sender) Bool.true) (Eq (s.blocklisted ctx.sender) 0))

burn の成功が含意するガード事実（停止中でない・呼び出し元はミンター・呼び出し元は未ブロック）をまとめて取り出す補題です。

解説 ​

何を述べているか。 burn が成功したなら、s.paused = false、s.minters sender = true、s.blocklisted sender = 0 がすべて成り立ちます。req_bind_eq_ok で先頭 3 ガードを剝がして得ます。

直感。 「焼却が通った ⇒ 停止中でなく、呼び出し元はミンターで、ブロックされていない」という前提一式です。burn は受取人がいないので、ブロック検査は呼び出し元だけです。

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

図解 ​

Lean ソースコード ​

lean
theorem burn_guards {s s' : State} {ctx : CallContext} {amount : U256}
    (h : burn s ctx amount = .ok s') :
    s.paused = false ∧ s.minters ctx.sender = true ∧ s.blocklisted ctx.sender = 0 := by
  unfold burn whenNotPaused onlyMinters notBlocklisted at h
  obtain ⟨hp, h⟩ := req_bind_eq_ok h
  obtain ⟨hm, h⟩ := req_bind_eq_ok h
  obtain ⟨hb, h⟩ := req_bind_eq_ok h
  exact ⟨hp, hm, hb⟩

依存 ​