JPYCv2 形式検証

外観

JPYC.setAuthorizationState_blocklisted ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ (s : JPYC.State) (a : JPYC.Address) (n : JPYC.Bytes32) (v : JPYC.U256), Eq (s.setAuthorizationState a n v).blocklisted s.blocklisted

(s.setAuthorizationState …).blocklisted は元の s.blocklisted に等しい、という @[simp] 等式です。

解説 ​

何を述べているか。 authorization 台帳の更新を施しても、ブロックリスト・フラグ（blocklisted）は 変わらない ことを示します。定義から rfl で従います。

直感。 State.setAuthorizationState は対象のマッピングだけを書き換える操作なので、それ以外のフィールドには一切触れません。

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

図解 ​

Lean ソースコード ​

lean
@[simp] theorem setAuthorizationState_blocklisted (s : State) (a : Address) (n : Bytes32) (v : U256) :
    (s.setAuthorizationState a n v).blocklisted = s.blocklisted := rfl

依存 ​