JPYC.burn_conserves

名称・種別

名称: JPYC.burn_conserves
種別: theorem
モジュール: JpycFormalVerification.AccessControlTheorems
ソース: JpycFormalVerification/AccessControlTheorems.lean:571-577
概要: burn は供給保存不変条件 SupplyConserved を保つ、という定理。
仕様: 対象

型シグネチャ

lean

∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {amount : JPYC.U256}, JPYC.SupplyConserved s → Eq (JPYC.burn s ctx amount) (Except.ok s') → JPYC.SupplyConserved s'

burn が成功するなら、結果状態も SupplyConserved（総供給 = 残高総和）を満たす、という供給保存の定理です。

和訳 docstring

供給保存。 burn は SupplyConserved を保つ。

解説

何を述べているか。 事前状態 s が SupplyConserved（totalSupply = Σ balances）を満たし、burn が成功して s' になったとき、s' もまた供給保存を満たします。

直感。 burn は総供給と呼び出し元残高をともに amount 減らします（burn_totalSupply / burn_totalBalances）。総供給も残高総和も動かないので、両者が等しいという関係はそのまま保たれます。

なぜ安全性に効くか。 「帳簿が常に釣り合っている（発行総量＝全員の残高合計）」という会計上の健全性を、各操作が壊さないことを保証します。mint/burn のように総供給を動かす操作では残高総和も同じだけ動くので、等式が保たれます。

図解

Lean ソースコード

lean

/-- **Supply conservation.** `burn` preserves `SupplyConserved`. -/
theorem burn_conserves {s s' : State} {ctx : CallContext} {amount : U256}
    (hc : SupplyConserved s) (h : burn s ctx amount = .ok s') : SupplyConserved s' := by
  unfold SupplyConserved
  have ht := burn_totalSupply h
  have hb := burn_totalBalances h
  unfold SupplyConserved at hc; omega

JPYC.burn_conserves ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.burn_conserves

名称・種別

型シグネチャ

和訳 docstring

解説

図解

Lean ソースコード

依存