JPYC.SupplyConserved

名称・種別

• 名称: JPYC.SupplyConserved
• 種別: def
• モジュール: JpycFormalVerification.State
• ソース: JpycFormalVerification/State.lean:155-158
• 概要: totalSupply が全残高の総和に等しいという、中心となる監査不変条件。
• 仕様: 対象

型シグネチャ

JPYC.State → Prop

State → Prop：状態について「totalSupply.toNat = totalBalances」が成り立つという 命題 です。

和訳 docstring

供給保存不変条件：totalSupply が全残高の総和に等しい。これは中心的な監査特性であり、Phase 1 / 2 が transfer / transferFrom / mint / burn による保存を証明する。

解説

何を述べているか。「帳簿上の総供給量 totalSupply」と「実際に配られている残高の合計 totalBalances」が一致する、という命題です（primer §3.7）。

直感。 二重帳簿の整合性です。総供給という一方の数字と、各人の残高を足し合わせたもう一方の数字が、常にぴったり合っていることを要求します。

なぜ安全性に効くか。 このプロジェクトの 中心的な安全性 です。transfer 系は総供給を変えず、mint は両辺を +amount、burn は両辺を −amount しますが、いずれの場合もこの等式が崩れないこと（*_conserves）が証明されています。つまり、お金が勝手に増えたり消えたりしません。

図解

Lean ソースコード

/-- Supply-conservation invariant: `totalSupply` equals the sum of all balances.
This is the central audit property; Phase 1/2 prove it is preserved by
`transfer` / `transferFrom` / `mint` / `burn`. -/
def SupplyConserved (s : State) : Prop := s.totalSupply.toNat = s.totalBalances

依存

• JPYC.State
• JPYC.State.totalBalances