JPYCv2 形式検証

外観

JPYC.State.setInitializedVersion ​

名称・種別 ​

  • 名称: JPYC.State.setInitializedVersion
  • 種別: def
  • モジュール: JpycFormalVerification.Upgradeability
  • ソース: JpycFormalVerification/Upgradeability.lean:42-44
  • 概要: initializedVersion を v に書き換える更新関数（0=未初期化, 1=V1, 2=V2）。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.U8 → JPYC.State

Stateと版数 v（U8）を受け取り、初期化バージョン initializedVersion だけを v に差し替えた新しい State を返す純関数です。

和訳 docstring ​

initializedVersion = v（0 = 未初期化, 1 = V1, 2 = V2）。

解説 ​

何を述べているか。 Solidity の代入 initializedVersion = v をモデル化した補助関数です。状態 s のうち initializedVersion フィールドだけを v に置き換え、残りはそのまま引き継ぎます（レコード更新 { s with … }）。版数の意味は 0 = 未初期化、1 = V1、2 = V2 です。

直感。 「初期化ラッチ（一方向の掛け金）の目盛りを書き換える」操作です。残高・ロール・各種フラグには一切触れません。

なぜ安全性に効くか。 この 1 フィールドが、初期化の 一回限り性 を司る掛け金です（0 → 1 → 2 と単調に進む）。更新を 1 フィールドに閉じ込めることで、WF の「initializedVersion ∈ {0,1,2}」条件や、各 initialize*_sets_version の効果定理が機械的に示せます。

図解 ​

Lean ソースコード ​

lean
/-- `initializedVersion = v` (0 = uninitialized, 1 = V1, 2 = V2). -/
def State.setInitializedVersion (s : State) (v : U8) : State :=
  { s with initializedVersion := v }

依存 ​