JPYC.setBalance_totalSupply

名称・種別

• 名称: JPYC.setBalance_totalSupply
• 種別: theorem
• モジュール: JpycFormalVerification.ERC20Theorems
• ソース: JpycFormalVerification/ERC20Theorems.lean:75-76
• 概要: setBalance は totalSupply を変えない、という frame 補題。
• 仕様: 対象外

型シグネチャ

∀ (s : JPYC.State) (a : JPYC.Address) (v : JPYC.U256), Eq (s.setBalance a v).totalSupply s.totalSupply

(s.setBalance a v).totalSupply は元の s.totalSupply に等しい、という等式です。

解説

何を述べているか。 残高を更新しても、総供給量（totalSupply）は 変わらない ことを示します。

直感。 State.setBalance は balances の 1 点だけを書き換える操作なので、それ以外のフィールドには一切触れません。定義から rfl で従います。

なぜ安全性に効くか。 @[simp] 補題として、送金系の証明で「残高更新は総供給量を保つ」を自動適用します。totalSupply 不変や WF 保存（フラグ不変）の論証は、こうした 1 行補題の積み重ねで機械化されています。

図解

Lean ソースコード

@[simp] theorem setBalance_totalSupply (s : State) (a : Address) (v : U256) :
    (s.setBalance a v).totalSupply = s.totalSupply := rfl

依存

• JPYC.Address
• JPYC.State
• JPYC.State.setBalance
• JPYC.U256