JPYC.wf_empty

名称・種別

名称: JPYC.wf_empty
種別: theorem
モジュール: JpycFormalVerification.State
ソース: JpycFormalVerification/State.lean:162-166
概要: 初期状態 State.empty が WF を満たす、という定理（WF の充足可能性）。
仕様: 対象

型シグネチャ

lean

JPYC.WF JPYC.State.empty

命題「WF State.empty」を主張する定理です。すなわち 初期状態 State.empty は健全性条件 WF を満たす こと（primer §5 の記号読み下し）。

解説

何を述べているか。 まっさらな初期状態 State.empty が、整合性の前提 WF のすべての条項を満たす、という証明です。

直感。 空状態では全フラグが 0、initializedVersion = 0 なので、4 つの条項はいずれも自明に成立します（フラグ条項は left; rfl、バージョン条項は decide で判定）。

なぜ安全性に効くか。 WF が 充足可能 であること（条件を満たす状態が現に存在すること）を保証する証人です。これが「あらゆる操作が WF を保つ」という連鎖の出発点になります。

図解

Lean ソースコード

lean

theorem wf_empty : WF State.empty where
  blocklistedBinary := by intro a; left; rfl
  allowlistedBinary := by intro a; left; rfl
  authStateBinary := by intro a n; left; rfl
  initializedVersionValid := by decide

JPYC.wf_empty ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.wf_empty

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存