JPYC.setBalance_allowlisted

名称・種別

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

型シグネチャ

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

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

解説

何を述べているか。 残高を更新しても、許可リスト・フラグ（allowlisted）は 変わらない ことを示します。

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

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

図解

Lean ソースコード

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

依存

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