JPYCv2 形式検証

外観

JPYC.initializeV2_not_reinitializable ​

名称・種別 ​

  • 名称: JPYC.initializeV2_not_reinitializable
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:213-219
  • 概要: 一度成功後、2 回目の initializeV2 は常に revert する（ラッチが 2≠1）（再初期化不可）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext}, Eq (JPYC.initializeV2 O s ctx) (Except.ok s') → ∀ {ctx₂ : JPYC.CallContext}, Eq (JPYC.initializeV2 O s' ctx₂) (Except.error JPYC.Error.initializeV2WrongVersion)

initializeV2 が一度成功したら、二度目の initializeV2 は必ず revert する、という 再初期化不可能（V2） の定理です。

和訳 docstring ​

再初期化不可能（V2）。 成功した initializeV2 の後、二度目の initializeV2 は常に revert する（ラッチが 2 ≠ 1）。

解説 ​

何を述べているか。 initializeV2 が成功して s' になったあと、s' に対する二度目の initializeV2（別の文脈でもよい）は常に Except.error .initializeV2WrongVersion を返します。initializeV2_sets_version で s' の版数が 2 であることを使い、initializeV2_wrong_version を適用します（2 ≠ 1）。

直感。 「V2 初期化も、ただ一度だけ」。ラッチが 2 に上がれば二度と 1 には戻らないので、再実行は不可能です。

なぜ安全性に効くか。 V2 初期化の 一回限り性 です。アップグレード後の初期化を再実行して状態を上書きする、という攻撃を原理的に封じます。

図解 ​

Lean ソースコード ​

lean
/-- **Re-initialization impossible (V2).** After a successful `initializeV2`, a
second `initializeV2` always reverts (the latch is now `2 ≠ 1`). -/
theorem initializeV2_not_reinitializable {O : SigOracle} {s s' : State} {ctx : CallContext}
    (h : initializeV2 O s ctx = .ok s') {ctx₂ : CallContext} :
    initializeV2 O s' ctx₂ = .error .initializeV2WrongVersion := by
  apply initializeV2_wrong_version
  rw [initializeV2_sets_version h]; decide

依存 ​