JPYCv2 形式検証

外観

JPYC.initializeV2 ​

名称・種別 ​

  • 名称: JPYC.initializeV2
  • 種別: def
  • モジュール: JpycFormalVerification.Upgradeability
  • ソース: JpycFormalVerification/Upgradeability.lean:106-116
  • 概要: initializeV2()：version 1 からのみ実行でき、ラッチを 2 に上げる V2 初期化関数。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.SigOracle → JPYC.State → JPYC.CallContext → Except JPYC.Error JPYC.State

FiatTokenV2 の initializeV2 関数です。版数 1 からのみ実行でき、ラッチを 2 に進めつつ VERSION と V2 用ドメインセパレータを更新します。署名オラクル O の下で定義されます。

和訳 docstring ​

initializeV2()（v2/FiatTokenV2.sol:75-80）。素の require(initializedVersion == 1) で守られ、ラッチを 2 に進め VERSION = "2" を設定し V2 ドメインセパレータを再計算する。

解説 ​

何を述べているか。 initializeV2()（v2/FiatTokenV2.sol:75-80）の写しです。require(initializedVersion == 1)（理由文字列のない素の require）で守られ、ラッチを 2 に進め、VERSION = "2" に設定し、保存済みのトークン name から V2 用のドメインセパレータを再計算します。3 つの書き込みは相異なるフィールドを対象とし、ドメインセパレータは name（ここでは未変更）を読むので、順序は結果に影響しません。

直感。 「V1 から V2 へのアップグレード時に 1 回だけ走る、追加のセットアップ」です。V1 初期化（版数 0 → 1）の 後にしか 実行できず、それ自体も 1 回限りです（版数 1 → 2）。

なぜ安全性に効くか。 initializeV2_requires_v1（成功 ⇒ 版数 1 だった）・initializeV2_sets_version（成功後は版数 2）・initializeV2_not_reinitializable（二度目は revert）として、V2 初期化も一回限りであることが証明されています。さらに initializeV2_locks_initializeV1 により、V2 まで進んだ後は V1 初期化も恒久的にロックされます。

図解 ​

Lean ソースコード ​

lean
/-- `initializeV2()` — `v2/FiatTokenV2.sol:75-80`. Guarded by
`require(initializedVersion == 1)` (a bare `require`, no reason string); promotes
the latch to `2`, sets `VERSION = "2"`, and recomputes the V2 domain separator
from the stored token `name`. The three writes target distinct fields and the
domain separator reads `name` (untouched here), so order is immaterial. -/
def initializeV2 (s : State) (ctx : CallContext) : Except Error State := do
  req (s.initializedVersion = 1) .initializeV2WrongVersion
  pure { s with
    initializedVersion := 2                                              -- :77
    version := "2"                                                       -- :78
    domainSeparator := O.makeDomainSeparator s.name "2" ctx.blockChainId } -- :79

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:75-80

solidity
function initializeV2() public {
    require(initializedVersion == 1);
    initializedVersion = 2;
    VERSION = "2";
    DOMAIN_SEPARATOR = EIP712.makeDomainSeparator(name, "2");
}

依存 ​