JPYC.setPermitNonce_blocklisted
名称・種別
- 名称:
JPYC.setPermitNonce_blocklisted - 種別: theorem
- モジュール:
JpycFormalVerification.SignaturesTheorems - ソース:
JpycFormalVerification/SignaturesTheorems.lean:55-56 - 概要: setPermitNonce は blocklisted を変えない、という frame 補題。
- 仕様: 対象外
型シグネチャ
lean
∀ (s : JPYC.State) (o : JPYC.Address) (v : JPYC.U256), Eq (s.setPermitNonce o v).blocklisted s.blocklisted(s.setPermitNonce …).blocklisted は元の s.blocklisted に等しい、という @[simp] 等式です。
解説
何を述べているか。 permit nonce の更新を施しても、ブロックリスト・フラグ（blocklisted）は 変わらない ことを示します。定義から rfl で従います。
直感。 State.setPermitNonce は対象のマッピングだけを書き換える操作なので、それ以外のフィールドには一切触れません。
なぜ安全性に効くか。 @[simp] 補題として、permit / EIP-3009 各操作の証明で「この更新はブロックリスト・フラグを保つ」を自動適用します。供給保存（総供給・残高総和）や WF 保存の論証は、こうした 1 行補題の積み重ねで機械化されています。
図解
Lean ソースコード
lean
@[simp] theorem setPermitNonce_blocklisted (s : State) (o : Address) (v : U256) :
(s.setPermitNonce o v).blocklisted = s.blocklisted := rfl