JPYCv2 形式検証

外観

JPYC.burn_eq ​

名称・種別 ​

  • 名称: JPYC.burn_eq
  • 種別: theorem
  • モジュール: JpycFormalVerification.AccessControlTheorems
  • ソース: JpycFormalVerification/AccessControlTheorems.lean:481-495
  • 概要: 成功した burn の算術的書き込みと結果状態を順方向に特徴づける補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {amount : JPYC.U256}, Eq (JPYC.burn s ctx amount) (Except.ok s') → Exists fun ns => Exists fun nb => And (Eq (JPYC.sub? s.totalSupply amount) (Except.ok ns)) (And (Eq (JPYC.sub? (s.balances ctx.sender) amount) (Except.ok nb)) (Eq s' ((s.setTotalSupply ns).setBalance ctx.sender nb)))

burn s ctx amount が成功したという仮定から、2 つの checked 減算（総供給・残高）が成功したことと、結果状態の形を取り出す前向き特徴づけ補題です。

解説 ​

何を述べているか。 burn が成功したとき、sub? totalSupply amount と sub? balances[sender] amount がともに成功して値 ns/nb を返し、結果 s' が「総供給を ns、balances[sender] を nb に更新した状態」に等しいことを取り出します。

直感。 停止・ミンター・ブロックの 3 ガードと正値・残高検査を剝がし、残る「2 つの減算」を露出させます。証明手順は mint_eq と同型です。

なぜ安全性に効くか。 burn の効果・不変条件定理（burn_totalSupply・burn_balance・burn_frame・burn_conserves・burn_wf）の出発点です。

図解 ​

Lean ソースコード ​

lean
theorem burn_eq {s s' : State} {ctx : CallContext} {amount : U256}
    (h : burn s ctx amount = .ok s') :
    ∃ ns nb,
      sub? s.totalSupply amount = .ok ns ∧
      sub? (s.balances ctx.sender) amount = .ok nb ∧
      s' = (s.setTotalSupply ns).setBalance ctx.sender nb := by
  unfold burn whenNotPaused onlyMinters notBlocklisted at h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨_, h⟩ := req_bind_eq_ok h
  obtain ⟨ns, hns, h⟩ := bind_eq_ok h
  obtain ⟨nb, hnb, h⟩ := bind_eq_ok h
  exact ⟨ns, nb, hns, hnb, pure_ok h⟩

依存 ​