JPYCv2 形式検証

外観

JPYC.initializeV2_requires_v1 ​

名称・種別 ​

  • 名称: JPYC.initializeV2_requires_v1
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:196-199
  • 概要: initializeV2 は version 1 からのみ成功する（二重実行ガード・順方向）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext}, Eq (JPYC.initializeV2 O s ctx) (Except.ok s') → Eq s.initializedVersion 1

initializeV2 の成功は、呼び出し前が 版数 1 だったことを含意する、という二重実行ガード（前向き）の定理です。

和訳 docstring ​

二重実行ガード（前向き）。 initializeV2 は版数 1 からのみ成功する。

解説 ​

何を述べているか。 initializeV2 が成功したなら s.initializedVersion = 1 です。initializeV2_ok の第 1 成分を取り出します。

直感。 「V2 初期化が通った ⇒ ちょうど V1 まで初期化済みだった」。版数 0（未初期化）でも 2（V2 済み）でも弾かれます。

なぜ安全性に効くか。 V1 → V2 の順序を強制します。V1 初期化を飛ばして V2 だけ走らせる、といった不正な初期化順序を防ぎます。

図解 ​

Lean ソースコード ​

lean
/-- **Double-execution guard (forward).** `initializeV2` succeeds only from
version `1`. -/
theorem initializeV2_requires_v1 {O : SigOracle} {s s' : State} {ctx : CallContext}
    (h : initializeV2 O s ctx = .ok s') : s.initializedVersion = 1 := (initializeV2_ok h).1

依存 ​