JPYC.State.totalBalances

名称・種別

• 名称: JPYC.State.totalBalances
• 種別: def
• モジュール: JpycFormalVerification.State
• ソース: JpycFormalVerification/State.lean:150-153
• 概要: 全口座残高の自然数としての総和。アドレス空間が有限なので well-defined。
• 仕様: 対象外

型シグネチャ

JPYC.State → Nat

State → Nat：状態を受け取り、全アカウント残高の総和を 自然数（ℕ） で返します。

和訳 docstring

全アカウント残高の総和を自然数で返す（総和自体がオーバーフローしないように）。アドレス空間は有限（Fintype Address）なので、これは実際に計算されることはなくても well-defined な有限和になる。

解説

何を述べているか。 ∑ a : Address, (balances a).toNat、すなわち全アカウントの残高を足し合わせた合計です。

直感。 合計を U256 のまま取ると総和自体がオーバーフローしうるので、あふれない自然数 ℕ で測ります。アドレスは無限にありうるように見えますが、有限型なので有限和として確定します（instFintypeBitVec）。

なぜ安全性に効くか。 SupplyConserved の右辺そのものです。totalSupply と突き合わせて「お金が湧かない・消えない」を表現するための量で、値として計算はされず証明の中だけで使う「概念量」です。

図解

Lean ソースコード

/-- Sum of all account balances, as a natural number (so the sum cannot itself
overflow). The address space is finite (`Fintype Address`), so this is a
well-defined finite sum even though it is never computed. -/
def State.totalBalances (s : State) : ℕ := ∑ a : Address, (s.balances a).toNat

依存

• JPYC.Address
• JPYC.State
• JPYC.instFintypeBitVec