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