JPYC.setAllowance_authorizationStates
名称・種別
- 名称:
JPYC.setAllowance_authorizationStates - 種別: theorem
- モジュール:
JpycFormalVerification.ERC20Theorems - ソース:
JpycFormalVerification/ERC20Theorems.lean:96-97 - 概要: setAllowance は authorizationStates を変えない、という frame 補題。
- 仕様: 対象外
型シグネチャ
lean
∀ (s : JPYC.State) (o sp : JPYC.Address) (v : JPYC.U256), Eq (s.setAllowance o sp v).authorizationStates s.authorizationStates(s.setAllowance o sp v).authorizationStates は元の s.authorizationStates に等しい、という等式です。
解説
何を述べているか。 許可額を更新しても、署名使用済みフラグ（authorizationStates）は 変わらない ことを示します。
直感。 State.setAllowance は allowed マッピングの 1 マスだけを書き換える操作なので、他のフィールドには触れません（rfl）。
なぜ安全性に効くか。 @[simp] 補題として、approve 系・transferFrom の許可額消費の証明で「許可額更新は署名使用済みフラグを保つ」を自動適用します。これにより、承認操作が残高・供給・WF を壊さないことが機械的に示せます。
図解
Lean ソースコード
lean
@[simp] theorem setAllowance_authorizationStates (s : State) (o sp : Address) (v : U256) :
(s.setAllowance o sp v).authorizationStates = s.authorizationStates := rfl