JPYC.setTotalSupply_totalSupply

名称・種別

• 名称: JPYC.setTotalSupply_totalSupply
• 種別: theorem
• モジュール: JpycFormalVerification.AccessControlTheorems
• ソース: JpycFormalVerification/AccessControlTheorems.lean:41-42
• 概要: setTotalSupply 後の totalSupply は設定値になる、という補題。
• 仕様: 対象外

型シグネチャ

∀ (s : JPYC.State) (v : JPYC.U256), Eq (s.setTotalSupply v).totalSupply v

総供給量を設定した直後に同じ鍵で読み出すと、設定した値 v がそのまま返る、という @[simp] 等式です。

解説

何を述べているか。 (s.setTotalSupply v).totalSupply = v を示します。総供給量を設定で書いた値が、同じ鍵での読み出しでそのまま得られます（Function.update_self）。

直感。 「書いた値はそのまま読める」という当たり前を、機械が自動で使える形（@[simp]）で確認しています。

なぜ安全性に効くか。 効果系の定理（mint_totalSupply など）が「設定した値が実際に反映される」と結論づけるための核心の補題です。

図解

Lean ソースコード

@[simp] theorem setTotalSupply_totalSupply (s : State) (v : U256) :
    (s.setTotalSupply v).totalSupply = v := rfl

依存

• JPYC.State
• JPYC.State.setTotalSupply
• JPYC.U256