JPYC.initializeV1_wf
名称・種別
- 名称:
JPYC.initializeV1_wf - 種別: theorem
- モジュール:
JpycFormalVerification.UpgradeabilityTheorems - ソース:
JpycFormalVerification/UpgradeabilityTheorems.lean:110-123 - 概要: initializeV1 は健全性不変条件 WF を保つ、という定理。
- 仕様: 対象
型シグネチャ
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}, JPYC.WF s → Eq (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) (Except.ok s') → JPYC.WF s'initializeV1 が成功するなら、結果状態も WF を満たす、という不変条件保存の定理です。
和訳 docstring
WF 保存。 initializeV1 はフラグを 0/1 に保ち（blocklisted[self] = 1 のみ）、ラッチを範囲内（1 ≤ 2）に保つ。
解説
何を述べているか。 事前状態 s が WF を満たし、initializeV1 が成功して s' になったとき、s' もまた WF を満たします。
直感。 initializeV1 がフラグに対して行う唯一の書き込みは blocklisted[self] = 1 です。1 は 0/1 の範囲内なので（更新点は 1、それ以外は元の WF）、ブロックリストの 0/1 性は崩れません。許可リスト・authorization 台帳は不変、版数は 1 ≤ 2 で範囲内です。
なぜ安全性に効くか。 初期化直後から状態が健全（フラグが壊れていない）であることを保証します。これが以降のすべての操作の WF 前提の出発点になります。
図解
Lean ソースコード
lean
/-- **WF preservation.** `initializeV1` keeps the flag maps 0/1-valued (it only
sets `blocklisted[self] = 1`) and the latch in range (`1 ≤ 2`). -/
theorem initializeV1_wf {O : SigOracle} {s s' : State} {ctx : CallContext} {self : Address}
{tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : U8}
{newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address}
(hwf : WF s)
(h : initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
newMinterAdmin newPauser newBlocklister newRescuer newOwner = .ok s') : WF s' := by
obtain ⟨_, _, _, _, _, _, rfl⟩ := initializeV1_ok h
exact {
blocklistedBinary := binaryFlag_update hwf.blocklistedBinary self (Or.inr rfl)
allowlistedBinary := hwf.allowlistedBinary
authStateBinary := hwf.authStateBinary
initializedVersionValid := by show (1 : U8).toNat ≤ 2; decide }