JPYCv2 形式検証

外観

JPYC.State ​

名称・種別 ​

  • 名称: JPYC.State
  • 種別: structure
  • モジュール: JpycFormalVerification.State
  • ソース: JpycFormalVerification/State.lean:41-101
  • 概要: FiatTokenV2 のストレージを継承チェーン全体にわたって写し取った状態構造体。
  • 仕様: 対象外

型シグネチャ ​

lean
Type

Type ＝ コントラクトのストレージ全体を写し取った 構造体 を定義します。残高・許可額・各種ロール・フラグ・署名管理情報など、多数のフィールドを持ちます。

和訳 docstring ​

FiatTokenV2 のストレージ。継承チェーン全体にわたる宣言を写したもの。フィールド順は論理的（EVM のスロット配置は対象外）。

解説 ​

何を述べているか。 コントラクトが保持する全データの「スナップショット型」です（primer §3.1）。

直感。 Solidity の mapping(address => uint256) のような「キーが無ければ 0」のマップは、Lean では全域関数（Address → U256 など）で表し、「未設定キーは残高 0」を表現します。ガス節約のため bool を uint256 で持つフィールド（blocklisted / allowlisted / authorizationStates）もそのまま写し、WF が「その値は 0 か 1 だけ」を記録します。すべての external 関数は State → … → Except Error State、すなわちこの型を入力に取り、新しい State を返します。

なぜ安全性に効くか。 検証対象の「世界」そのものです。EVM のスロット配置は抽象化する一方、各フィールドには対応する Solidity 宣言の file:line を注釈し、忠実性を担保しています。

図解 ​

Lean ソースコード ​

lean
/-- Storage of `FiatTokenV2`, mirroring the declarations across its inheritance
chain. Field order is logical (the EVM slot layout is out of scope). -/
structure State where
  -- Token metadata — `v2/FiatTokenV2.sol:49-55`, `v1/FiatTokenV1.sol:65-71`
  /-- `string public name`. -/
  name : String
  /-- `string public symbol`. -/
  symbol : String
  /-- `string public currency`. -/
  currency : String
  /-- `uint8 public decimals`. -/
  decimals : U8
  /-- `uint256 internal totalSupply_`. -/
  totalSupply : U256
  /-- `uint8 internal initializedVersion` (0 = uninitialized, 1 = V1, 2 = V2). -/
  initializedVersion : U8
  -- Core ERC20 maps — `v2/FiatTokenV2.sol:57-63`
  /-- `mapping(address => uint256) internal balances`. -/
  balances : Address → U256
  /-- `mapping(address => mapping(address => uint256)) internal allowed`
  (`allowed owner spender`). -/
  allowed : Address → Address → U256
  /-- `mapping(address => bool) internal minters`. -/
  minters : Address → Bool
  /-- `mapping(address => uint256) internal minterAllowed`. -/
  minterAllowed : Address → U256
  /-- `mapping(address => uint256) internal allowlisted` (V2; `1` = allowlisted). -/
  allowlisted : Address → U256
  -- Role addresses
  /-- `Ownable._owner` — `v1/Ownable.sol:27`. -/
  owner : Address
  /-- `Pausable.pauser` — `v1/Pausable.sol:56`. -/
  pauser : Address
  /-- `Blocklistable.blocklister` — `v1/Blocklistable.sol:43`. -/
  blocklister : Address
  /-- `Rescuable.rescuer` — `v1/Rescuable.sol:42`. -/
  rescuer : Address
  /-- `FiatTokenV2.minterAdmin` — `v2/FiatTokenV2.sol:53`. -/
  minterAdmin : Address
  /-- `FiatTokenV2.allowlister` — `v2/FiatTokenV2.sol:64`. -/
  allowlister : Address
  -- Pausable / Blocklistable state
  /-- `Pausable.paused` — `v1/Pausable.sol:57`. -/
  paused : Bool
  /-- `Blocklistable.blocklisted` — `v1/Blocklistable.sol:44` (`1` = blocklisted). -/
  blocklisted : Address → U256
  -- EIP-712 domain — `v1/EIP712Domain.sol:45-48`
  /-- `bytes32 internal DOMAIN_SEPARATOR`. -/
  domainSeparator : Bytes32
  /-- `uint256 internal CHAIN_ID`. -/
  chainId : U256
  /-- `string internal NAME`. -/
  domainName : String
  /-- `string internal VERSION`. -/
  version : String
  -- Signature bookkeeping
  /-- `EIP2612._permitNonces` — `v1/EIP2612.sol:50`. -/
  permitNonces : Address → U256
  /-- `EIP3009._authorizationStates` — `v1/EIP3009.sol:64`
  (`authorizationStates authorizer nonce`; `1` = used or canceled). -/
  authorizationStates : Address → Bytes32 → U256

依存 ​

（なし）