JPYCv2 形式検証

外観

JPYC.initializeV2_sets_version ​

名称・種別 ​

  • 名称: JPYC.initializeV2_sets_version
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:201-204
  • 概要: 成功した initializeV2 はラッチを version 2 に上げる（効果）。
  • 仕様: 対象

型シグネチャ ​

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

initializeV2 の成功は、ラッチを版数 2 に進める、という効果（ラッチ）の定理です。

和訳 docstring ​

効果（ラッチ）。 成功した initializeV2 はラッチを版数 2 に進める。

解説 ​

何を述べているか。 initializeV2 が成功した結果状態では s'.initializedVersion = 2 です。initializeV2_ok の結果状態から rfl で従います。

直感。 「V2 初期化が済んだら、掛け金が 1 から 2 に上がる」を確認します。これがラッチの最終段です。

なぜ安全性に効くか。 ラッチが 2 に達することで、initializeV2_not_reinitializable（V2 再実行は 2 ≠ 1 で弾かれる）と initializeV2_locks_initializeV1（V1 も 2 ≠ 0 で弾かれる）が成立します。

図解 ​

Lean ソースコード ​

lean
/-- **Effect (latch).** A successful `initializeV2` promotes the latch to `2`. -/
theorem initializeV2_sets_version {O : SigOracle} {s s' : State} {ctx : CallContext}
    (h : initializeV2 O s ctx = .ok s') : s'.initializedVersion = 2 := by
  obtain ⟨_, rfl⟩ := initializeV2_ok h; rfl

依存 ​