JPYC.setAllowance_totalSupply

名称: JPYC.setAllowance_totalSupply
種別: theorem
モジュール: JpycFormalVerification.ERC20Theorems
ソース: JpycFormalVerification/ERC20Theorems.lean:90-91
概要: setAllowance は totalSupply を変えない、という frame 補題。
仕様: 対象外

名称・種別

lean

∀ (s : JPYC.State) (o sp : JPYC.Address) (v : JPYC.U256), Eq (s.setAllowance o sp v).totalSupply s.totalSupply

(s.setAllowance o sp v).totalSupply は元の s.totalSupply に等しい、という等式です。

何を述べているか。 許可額を更新しても、総供給量（totalSupply）は 変わらない ことを示します。

直感。 State.setAllowance は allowed マッピングの 1 マスだけを書き換える操作なので、他のフィールドには触れません（rfl）。

なぜ安全性に効くか。 @[simp] 補題として、approve 系・transferFrom の許可額消費の証明で「許可額更新は総供給量を保つ」を自動適用します。これにより、承認操作が残高・供給・WF を壊さないことが機械的に示せます。

lean

@[simp] theorem setAllowance_totalSupply (s : State) (o sp : Address) (v : U256) :
    (s.setAllowance o sp v).totalSupply = s.totalSupply := rfl