JPYC.setBalance_initializedVersion

名称・種別

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

型シグネチャ

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

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

解説

何を述べているか。 残高を更新しても、初期化バージョン（initializedVersion）は 変わらない ことを示します。

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

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

図解

Lean ソースコード

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

依存

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