JPYC.setBalance_blocklisted

名称・種別

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

型シグネチャ

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

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

解説

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

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

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

図解

Lean ソースコード

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

依存

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