JPYC.initializeV1_sets_minterAdmin

名称・種別

名称: JPYC.initializeV1_sets_minterAdmin
種別: theorem
モジュール: JpycFormalVerification.UpgradeabilityTheorems
ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:148-154
概要: 成功した initializeV1 は minterAdmin を指定値に設定する（効果）。
仕様: 対象

型シグネチャ

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'.minterAdmin newMinterAdmin

initializeV1 の成功は、minterAdmin をnewMinterAdminに設定する、という効果定理です。

解説

何を述べているか。 initializeV1 が成功した結果状態では s'.minterAdmin = newMinterAdmin です。initializeV1_ok が与える s' = initializeResult … の該当する代入から、rfl で従います。

直感。 「初期化で渡したミンター管理者が、ちゃんとその役職に就く」を確認します。

なぜ安全性に効くか。 各ロールが初期化時に指定どおりのアドレスへ設定されることを保証します。しかも initializeV1 はこれらが ゼロアドレスでない ことを要求するので、重要権限が「誰も持たない」状態で始まる事故を防ぎます。

図解

Lean ソースコード

lean

theorem initializeV1_sets_minterAdmin {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'.minterAdmin = newMinterAdmin := by
  obtain ⟨_, _, _, _, _, _, rfl⟩ := initializeV1_ok h; rfl

JPYC.initializeV1_sets_minterAdmin ​

名称・種別 ​

型シグネチャ ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.initializeV1_sets_minterAdmin

名称・種別

型シグネチャ

解説

図解

Lean ソースコード

依存