JPYC.unpause_wf
名称・種別
- 名称:
JPYC.unpause_wf - 種別: theorem
- モジュール:
JpycFormalVerification.AccessControlTheorems - ソース:
JpycFormalVerification/AccessControlTheorems.lean:220-221 - 概要: unpause は健全性不変条件 WF を保つ、という定理。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext}, JPYC.WF s → Eq (JPYC.unpause s ctx) (Except.ok s') → JPYC.WF s'unpause が成功するなら、結果状態も WF を満たす、という不変条件保存の定理です。
解説
何を述べているか。 事前状態 s が WF を満たし、unpause が成功して s' になったとき、s' もまた WF を満たします。
直感。 WF はフラグ（blocklisted/allowlisted/authorizationStates）が 0/1 のみ、initializedVersion ∈ {0,1,2} を要求します。paused の切り替えはフラグ 4 種に触れないので、WF は保たれます（WF.of_flags_eq）。
なぜ安全性に効くか。 すべての操作が WF を保つので、「正規の操作を続ける限りフラグが壊れた値にならない」が帰納的に保証されます。フラグに依存する判定ロジック全体の前提が、操作後も成り立ち続けます。
図解
Lean ソースコード
lean
theorem unpause_wf {s s' : State} {ctx : CallContext} (hwf : WF s) (h : unpause s ctx = .ok s') : WF s' := by
obtain ⟨_, rfl⟩ := unpause_ok h; exact WF.of_flags_eq hwf rfl rfl rfl rfl