JPYC.WF_setBlocklisted

名称・種別

• 名称: JPYC.WF_setBlocklisted
• 種別: theorem
• モジュール: JpycFormalVerification.AccessControlTheorems
• ソース: JpycFormalVerification/AccessControlTheorems.lean:89-94
• 概要: 0/1 を書く限り setBlocklisted は WF を保つ、という補題。
• 仕様: 対象外

型シグネチャ

∀ {s : JPYC.State}, JPYC.WF s → ∀ (a : JPYC.Address) {v : JPYC.U256}, Or (Eq v 0) (Eq v 1) → JPYC.WF (s.setBlocklisted a v)

事前状態が WF を満たし、ブロックリスト・フラグ（blocklisted）に 0 または 1 を書き込むなら、書き込み後も WF が保たれる、という補題です。

解説

何を述べているか。 State.setBlocklisted はブロックリスト・フラグの 1 点に値 v を書き込みます。v が 0 か 1 のいずれかなら、フラグマップが 0/1 値のままであるという WF の条件は崩れません。残りの WF 条件（他フラグ・initializedVersion）は触れていないのでそのまま保たれます。

直感。 「フラグには 0 か 1 しか書かない」というモデルの約束を、WF 保存の形で確認します。証明は共通補助 binaryFlag_update に委ね、更新点は v ∈ {0,1}、それ以外は元の WF を使います。

なぜ安全性に効くか。 blocklist_wf / unBlocklist_wf / allowlist_wf / unAllowlist_wf の土台です。ブロック・許可リスト操作が WF を壊さないことを保証し、フラグに依存する判定ロジックの前提を守ります。

図解

Lean ソースコード

theorem WF_setBlocklisted {s : State} (hwf : WF s) (a : Address) {v : U256}
    (hv : v = 0 ∨ v = 1) : WF (s.setBlocklisted a v) where
  blocklistedBinary := binaryFlag_update hwf.blocklistedBinary a hv
  allowlistedBinary := hwf.allowlistedBinary
  authStateBinary := hwf.authStateBinary
  initializedVersionValid := hwf.initializedVersionValid

依存

• JPYC.Address
• JPYC.State
• JPYC.State.setBlocklisted
• JPYC.U256
• JPYC.WF