JPYC.initializeV1_conserves

名称・種別

名称: JPYC.initializeV1_conserves
種別: theorem
モジュール: JpycFormalVerification.UpgradeabilityTheorems
ソース: JpycFormalVerification/UpgradeabilityTheorems.lean:128-137
概要: initializeV1 は供給保存不変条件 SupplyConserved を保つ、という定理。
仕様: 対象

型シグネチャ

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.SupplyConserved s → Eq (JPYC.initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals newMinterAdmin newPauser newBlocklister newRescuer newOwner) (Except.ok s') → JPYC.SupplyConserved s'

initializeV1 が成功するなら、結果状態も SupplyConserved を満たす、という供給保存の定理です。

和訳 docstring

供給保存。 initializeV1 は残高にも totalSupply にも触れないので SupplyConserved を保つ。

解説

何を述べているか。 事前状態が SupplyConserved を満たし、initializeV1 が成功すれば、結果も供給保存を満たします。証明は、initializeResult が balances にも totalSupply にも触れないことから直ちに従います（仮定 hc をそのまま使う）。

直感。 初期化はメタデータとロールを設定するだけで、お金（残高・総供給）は一切動かしません。総供給は 0、残高総和も 0 のまま、等式は自明に成立します。

なぜ安全性に効くか。 「初期化はトークンを発行しない」という当たり前を保証します。セットアップ時点で供給の帳簿が壊れないことの裏付けです。

図解

Lean ソースコード

lean

/-- **Supply conservation.** `initializeV1` touches neither balances nor
`totalSupply`, so it preserves `SupplyConserved`. -/
theorem initializeV1_conserves {O : SigOracle} {s s' : State} {ctx : CallContext} {self : Address}
    {tokenName tokenSymbol tokenCurrency : String} {tokenDecimals : U8}
    {newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address}
    (hc : SupplyConserved s)
    (h : initializeV1 O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
      newMinterAdmin newPauser newBlocklister newRescuer newOwner = .ok s') : SupplyConserved s' := by
  obtain ⟨_, _, _, _, _, _, rfl⟩ := initializeV1_ok h
  exact hc

JPYC.initializeV1_conserves ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

依存 ​

JPYC.initializeV1_conserves

名称・種別

型シグネチャ

和訳 docstring

解説

図解

Lean ソースコード

依存