JPYC.setTotalSupply_balances
名称・種別
- 名称:
JPYC.setTotalSupply_balances - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:43-44 - 概要: setTotalSupply は balances を変えない、という frame 補題。
- 仕様: 対象外
型シグネチャ
lean
∀ (s : JPYC.State) (v : JPYC.U256), Eq (s.setTotalSupply v).balances s.balances(s.setTotalSupply …).balances は元の s.balances に等しい、という @[simp] 等式です。
解説
何を述べているか。 総供給量の更新を施しても、残高マッピング（balances）は 変わらない ことを示します。
直感。 State.setTotalSupply は対象フィールドだけを書き換える操作なので、それ以外には一切触れません。定義から rfl で従います。
なぜ安全性に効くか。 @[simp] 補題として、ミント・バーン・ロール操作の証明で「この更新は残高マッピングを保つ」を自動適用します。総供給不変や WF 保存（フラグ不変）の論証は、こうした 1 行補題の積み重ねで機械化されています。
図解
Lean ソースコード
lean
@[simp] theorem setTotalSupply_balances (s : State) (v : U256) :
(s.setTotalSupply v).balances = s.balances := rfl