JPYCv2 形式検証

外観

JPYC.initializeResult ​

名称・種別 ​

  • 名称: JPYC.initializeResult
  • 種別: def
  • モジュール: JpycFormalVerification.Upgradeability
  • ソース: JpycFormalVerification/Upgradeability.lean:59-83
  • 概要: initialize の直線的代入ブロック。各書き込みは別フィールドなので同時更新としてモデル化。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.SigOracle → JPYC.State → JPYC.CallContext → JPYC.Address → String → String → String → JPYC.U8 → JPYC.Address → JPYC.Address → JPYC.Address → JPYC.Address → JPYC.Address → JPYC.State

initialize（V1）の 代入ブロック を 1 つにまとめた純関数です。各種名称・ロール・自己ブロックリスト・ドメインセパレータ・版数 1 を、状態 s にまとめて書き込んだ新しい State を返します。署名オラクル O の下で定義されます。

和訳 docstring ​

initialize の代入ブロック（v1/FiatTokenV1.sol:120-134）。各代入は相異なるフィールドを書くので 1 つの同時レコード更新と等価。_transferOwnership（v1/Ownable.sol:66-70）が owner := newOwner、blocklisted[address(this)] = 1 は self を使う。

解説 ​

何を述べているか。 initialize 本体の直線的な代入列（v1/FiatTokenV1.sol:120-134）をモデル化したものです。書き込み先はすべて 相異なるフィールド（name/symbol/各ロール/blocklisted[self]/domainSeparator/chainId/version/initializedVersion …）なので、Solidity の逐次代入は「同時のレコード更新」1 つと等価にモデル化できます。各フィールドにソース行番号が注釈されています。_transferOwnership(newOwner) は owner := newOwner の書き込みに、blocklisted[address(this)] = 1 は self を address(this) として使う書き込みに当たります。

直感。 「初期化が一括で行う “状態のセットアップ” そのもの」です。これを initializeV1 のガード群（版数チェック＋5 つのゼロアドレス検査）の 後ろ に置くことで、関数全体が「ガードを全部通ったらこの状態を作る」という形に分解できます。

なぜ安全性に効くか。 効果定理（initializeV1_sets_owner・initializeV1_blocklists_self など）と不変条件保存（initializeV1_wf・initializeV1_conserves）を、この純関数の形に対して機械的に示せます。残高・総供給には触れないので供給保存は自明、フラグは blocklisted[self] = 1 のみなので WF も保たれます。

図解 ​

Lean ソースコード ​

lean
/-- The straight-line assignment block of `initialize`
(`v1/FiatTokenV1.sol:120-134`). Every write targets a *distinct* field, so the
sequential Solidity assignments are equivalently modeled as one simultaneous
record update; each field carries its source line. `_transferOwnership(newOwner)`
(`v1/Ownable.sol:66-70`) is the `owner := newOwner` write, and
`blocklisted[address(this)] = 1` uses `self` for `address(this)`. -/
def initializeResult (s : State) (ctx : CallContext) (self : Address)
    (tokenName tokenSymbol tokenCurrency : String) (tokenDecimals : U8)
    (newMinterAdmin newPauser newBlocklister newRescuer newOwner : Address) : State :=
  { s with
    name := tokenName                                                       -- :120
    symbol := tokenSymbol                                                   -- :121
    currency := tokenCurrency                                               -- :122
    decimals := tokenDecimals                                               -- :123
    minterAdmin := newMinterAdmin                                           -- :124
    pauser := newPauser                                                     -- :125
    blocklister := newBlocklister                                           -- :126
    rescuer := newRescuer                                                   -- :127
    owner := newOwner                                                       -- :128 (_transferOwnership)
    blocklisted := Function.update s.blocklisted self 1                     -- :129
    domainSeparator := O.makeDomainSeparator tokenName "1" ctx.blockChainId -- :130 (DOMAIN_SEPARATOR)
    chainId := ctx.blockChainId                                            -- :131 (CHAIN_ID)
    domainName := tokenName                                                 -- :132 (NAME)
    version := "1"                                                          -- :133 (VERSION)
    initializedVersion := 1 }                                              -- :134

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/FiatTokenV1.sol:120-134, reference/JPYCv2/contracts/v1/Ownable.sol:66-70

solidity
// v1/FiatTokenV1.sol:120-134 (the straight-line assignment block of initialize)
name = tokenName;
symbol = tokenSymbol;
currency = tokenCurrency;
decimals = tokenDecimals;
minterAdmin = newMinterAdmin;
pauser = newPauser;
blocklister = newBlocklister;
rescuer = newRescuer;
_transferOwnership(newOwner);                                  // v1/Ownable.sol:66-70
blocklisted[address(this)] = 1;
DOMAIN_SEPARATOR = EIP712.makeDomainSeparator(tokenName, "1");
CHAIN_ID = block.chainid;
NAME = tokenName;
VERSION = "1";
initializedVersion = 1;

依存 ​