JPYC.initializeV1

名称・種別

名称: JPYC.initializeV1
種別: def
モジュール: JpycFormalVerification.Upgradeability
ソース: JpycFormalVerification/Upgradeability.lean:85-104
概要: initialize(...)（Lean キーワード回避で改名）：未初期化からのみ実行できる一回限りの初期化関数。
仕様: 対象外

型シグネチャ

lean

JPYC.SigOracle → JPYC.State → JPYC.CallContext → JPYC.Address → String → String → String → JPYC.U8 → JPYC.Address → JPYC.Address → JPYC.Address → JPYC.Address → JPYC.Address → Except JPYC.Error JPYC.State

FiatTokenV1 の initialize 関数です（initialize は Lean の予約語なので initializeV1 と改名）。版数ラッチと 5 つのゼロアドレス検査を通したのち、初期化済み状態（版数 1）を作ります。署名オラクル O の下で定義されます。

和訳 docstring

initialize(...)（v1/FiatTokenV1.sol:84-135、initialize は Lean 予約語のため改名）。先頭の require(initializedVersion == 0) が二重実行ガード、続く 5 つの非ゼロアドレス検査の後に代入ブロックが走りラッチが 1 になる。ロール修飾子はなく誰でも呼べるが、未初期化状態からのみ ―― 安全性は一回限りガードであって呼び出し元ではない。

解説

何を述べているか。 initialize(...)（v1/FiatTokenV1.sol:84-135）の写しです。先頭の require(initializedVersion == 0, …) が 二重実行ガード（alreadyInitialized）で、続いて 5 つの非ゼロアドレス検査（minterAdmin/pauser/blocklister/rescuer/owner）がソース順に並びます。すべて通ると代入ブロック（initializeResult）が走り、ラッチが 1 になります。

直感。 「コントラクトの最初のセットアップ」です。注意すべきは、initialize は public で ロール modifier を持たない こと ―― つまり誰でも呼べます。ただし呼べるのは 未初期化状態（版数 0）からだけ です。したがって安全性の眼目は「誰が呼ぶか」ではなく「一度しか実行できない」という一回限り性にあります。UUPS プロキシでは、実装コントラクトの初期化が攻撃者に奪われない設計が重要で、ここではそれをラッチで表現しています。

なぜ安全性に効くか。 initializeV1_requires_uninitialized（成功 ⇒ 版数 0 だった）・initializeV1_sets_version（成功後は版数 1）・initializeV1_not_reinitializable（二度目は必ず revert）として、再初期化の不可能性が証明されています。さらに 5 つのゼロアドレス検査により、重要ロールが「宙に浮いた（誰も持たない）」状態で始まることを防ぎます。

図解

Lean ソースコード

lean

/-- `initialize(...)` — `v1/FiatTokenV1.sol:84-135` (named `initializeV1` here, as
`initialize` is a Lean keyword). The leading `require(initializedVersion == 0, …)`
is the double-execution guard; the five non-zero-address checks (`minterAdmin`,
`pauser`, `blocklister`, `rescuer`, `owner`) follow in source order, then the
assignment block (`initializeResult`) runs and the latch becomes `1`. `initialize`
is `public` with no role modifier: anyone may call it, but only from the
uninitialized state — so the safety property is the one-shot guard, not who calls
it. -/
def initializeV1 (s : State) (ctx : CallContext) (self : Address)
    (tokenName tokenSymbol tokenCurrency : String) (tokenDecimals : U8)
    (newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address) :
    Except Error State := do
  req (s.initializedVersion = 0) .alreadyInitialized
  req (newMinterAdmin ≠ Address.zero) .newMinterAdminZero
  req (newPauser ≠ Address.zero) .initNewPauserZero
  req (newBlocklister ≠ Address.zero) .initNewBlocklisterZero
  req (newRescuer ≠ Address.zero) .initNewRescuerZero
  req (newOwner ≠ Address.zero) .initNewOwnerZero
  pure (initializeResult O s ctx self tokenName tokenSymbol tokenCurrency tokenDecimals
    newMinterAdmin newPauser newBlocklister newRescuer newOwner)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v1/FiatTokenV1.sol:84-135

solidity

function initialize(
    string memory tokenName,
    string memory tokenSymbol,
    string memory tokenCurrency,
    uint8 tokenDecimals,
    address newMinterAdmin,
    address newPauser,
    address newBlocklister,
    address newRescuer,
    address newOwner
) public {
    require(
        initializedVersion == 0,
        "FiatToken: contract is already initialized"
    );
    require(newMinterAdmin != address(0), "FiatToken: new minterAdmin is the zero address");
    require(newPauser != address(0), "FiatToken: new pauser is the zero address");
    require(newBlocklister != address(0), "FiatToken: new blocklister is the zero address");
    require(newRescuer != address(0), "FiatToken: new rescuer is the zero address");
    require(newOwner != address(0), "FiatToken: new owner is the zero address");

    name = tokenName;
    symbol = tokenSymbol;
    currency = tokenCurrency;
    decimals = tokenDecimals;
    minterAdmin = newMinterAdmin;
    pauser = newPauser;
    blocklister = newBlocklister;
    rescuer = newRescuer;
    _transferOwnership(newOwner);
    blocklisted[address(this)] = 1;
    DOMAIN_SEPARATOR = EIP712.makeDomainSeparator(tokenName, "1");
    CHAIN_ID = block.chainid;
    NAME = tokenName;
    VERSION = "1";
    initializedVersion = 1;
}

JPYC.initializeV1 ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​