JPYC.upgradeTo_ok
名称・種別
- 名称:
JPYC.upgradeTo_ok - 種別: theorem
- モジュール:
JpycFormalVerification.UpgradeabilityTheorems - ソース:
JpycFormalVerification/UpgradeabilityTheorems.lean:255-262 - 概要: 成功した upgradeTo は owner が認可し、モデル状態を変えない（slot 書き込みは対象外）。
- 仕様: 対象
型シグネチャ
lean
∀ {s s' : JPYC.State} {ctx : JPYC.CallContext} {impl : JPYC.Address}, Eq (JPYC.upgradeTo s ctx impl) (Except.ok s') → And (Eq s.owner ctx.sender) (Eq s' s)upgradeTo の成功は、オーナーによる認可であり、かつモデル状態が変わらない（s' = s）ことを取り出す前向き特徴づけ補題です。
和訳 docstring
成功した upgradeTo はオーナー認可であり、モデル状態は変わらない（実装スロット書き込みはスコープ外）。
解説
何を述べているか。 upgradeTo が成功したなら s.owner = ctx.sender（オーナー認可）かつ s' = s（モデル状態は不変）です。authorizeUpgrade（= onlyOwner）を剝がし、続く pure s から結果状態を確定します。
直感。 「アップグレードが通った ⇒ オーナーが呼んだ。そしてモデルの状態は何も変わっていない」。実装スロットの書き込みはスコープ外なので、観測できる状態変化はありません。
なぜ安全性に効くか。 upgradeTo の認可（upgradeTo_auth）と不変条件保存（upgradeTo_wf / upgradeTo_conserves）が、この 1 本から導けます。状態不変なので WF・供給保存は自明です。
図解
Lean ソースコード
lean
/-- A successful `upgradeTo` was authorized by the owner and leaves the modeled
state unchanged (the implementation-slot write is out of scope; see the model
header). -/
theorem upgradeTo_ok {s s' : State} {ctx : CallContext} {impl : Address}
(h : upgradeTo s ctx impl = .ok s') : s.owner = ctx.sender ∧ s' = s := by
unfold upgradeTo authorizeUpgrade onlyOwner at h
obtain ⟨h1, h⟩ := req_bind_eq_ok h
exact ⟨h1, pure_ok h⟩