JPYCv2 形式検証

外観

JPYC.initializeV1_sets_version ​

名称・種別 ​

  • 名称: JPYC.initializeV1_sets_version
  • 種別: theorem
  • モジュール: JpycFormalVerification.UpgradeabilityTheorems
  • ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:72-80
  • 概要: 成功した initializeV1 はラッチを version 1 にする（効果）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {self : JPYC.Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : JPYC.U8} {newMinterAdmin newPauser newBlocklister newRescuer newOwner : JPYC.Address}, Eq (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) (Except.ok s') → Eq s'.initializedVersion 1

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

和訳 docstring ​

効果（ラッチ）。 成功した initializeV1 はラッチを版数 1 にする。

解説 ​

何を述べているか。 initializeV1 が成功した結果状態では s'.initializedVersion = 1 です。initializeV1_ok が与える s' = initializeResult … の最後の書き込み（initializedVersion := 1）から従います。

直感。 「V1 初期化が済んだら、掛け金が 0 から 1 に上がる」を確認します。

なぜ安全性に効くか。 ラッチが確実に進むことで、initializeV1_not_reinitializable（二度目は版数 ≠ 0 で弾かれる）と initializeV2_requires_v1（V2 は版数 1 からのみ）が意味を持ちます。0 → 1 → 2 の一方向ラッチの 1 段目です。

図解 ​

Lean ソースコード ​

lean
/-- **Effect (latch).** A successful `initializeV1` leaves the latch at version
`1`. -/
theorem initializeV1_sets_version {O : SigOracle} {s s' : State} {ctx : CallContext}
    {self : Address} {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : U8}
    {newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address}
    (h : initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
      newMinterAdmin newPauser newBlocklister newRescuer newOwner = .ok s') :
    s'.initializedVersion = 1 := by
  obtain ⟨_, _, _, _, _, _, rfl⟩ := initializeV1_ok h; rfl

依存 ​