JPYC.Error

名称・種別

• 名称: JPYC.Error
• 種別: inductive
• モジュール: JpycFormalVerification.Error
• ソース: JpycFormalVerification/Error.lean:17-76
• 概要: FiatTokenV2 と基底コントラクトの全 revert 理由を列挙した型。同一の理由文字列は単一コンストラクタを共有する。
• 仕様: 対象外

型シグネチャ

Type

Type ＝ 取りうる失敗理由を列挙する 列挙型（inductive） を定義します。各コンストラクタが 1 つの revert 理由に対応します。

和訳 docstring

FiatTokenV2 とその基底コントラクトの revert 理由。

下のグループ化コメントは、由来となる reference/JPYCv2/contracts 内の Solidity ファイルを示す。異なる 2 つの関数が 同じ 理由文字列で revert する場合は、1 つのコンストラクタを共有する。

解説

何を述べているか。 revert（巻き戻し）が起こりうるときの「失敗理由」を、ひとつの列挙型に網羅的に集めたものです（primer §3.3）。

直感。 各 external 関数の型は … → Except Error State です。失敗したときに返る Except.error e の e が、まさにこの Error 型の値です。理由文字列を持たない算術 Panic(0x11) は、専用の arithmeticOverflow / arithmeticUnderflow コンストラクタで表します。

なぜ安全性に効くか。 失敗の集合を 有限かつ網羅的 に固定することで、「どの require がどの失敗に対応するか」がソースと 1 対 1 で追跡できます。さらに Error.revertMessage を通じて、各失敗をオンチェーンの理由文字列まで照合できます。

図解

Lean ソースコード

/-- Revert reasons of `FiatTokenV2` and its base contracts.

The grouping comments below cite the originating Solidity file inside
`reference/JPYCv2/contracts`. Where two different functions revert with the
*same* reason string, they share a single constructor. -/
inductive Error where
  -- Solidity 0.8 checked arithmetic — `Panic(0x11)` (no reason string).
  | arithmeticOverflow
  | arithmeticUnderflow
  -- v1/Ownable.sol
  | notOwner                       -- "Ownable: caller is not the owner"
  | newOwnerZero                   -- "Ownable: new owner is the zero address"
  -- v1/Pausable.sol
  | paused                         -- "Pausable: paused"
  | notPauser                      -- "Pausable: caller is not the pauser"
  | pausableNewPauserZero          -- "Pausable: new pauser is the zero address"
  -- v1/Blocklistable.sol
  | notBlocklister                 -- "Blocklistable: caller is not the blocklister"
  | accountBlocklisted             -- "Blocklistable: account is blocklisted"
  | blocklistableNewBlocklisterZero -- "Blocklistable: new blocklister is the zero address"
  -- v1/Rescuable.sol
  | notRescuer                     -- "Rescuable: caller is not the rescuer"
  | rescuableNewRescuerZero        -- "Rescuable: new rescuer is the zero address"
  -- v1/FiatTokenV1.sol + v2/FiatTokenV2.sol — minting / ERC20
  | notMinter                      -- "FiatToken: caller is not a minter"
  | mintToZero                     -- "FiatToken: mint to the zero address"
  | mintAmountNotPositive          -- "FiatToken: mint amount not greater than 0"
  | mintExceedsMinterAllowance     -- "FiatToken: mint amount exceeds minterAllowance"
  | notMinterAdmin                 -- "FiatToken: caller is not the minterAdmin"
  | approveFromZero                -- "FiatToken: approve from the zero address"
  | approveToZero                  -- "FiatToken: approve to the zero address"
  | transferExceedsAllowance       -- "FiatToken: transfer amount exceeds allowance"
  | transferFromZero               -- "FiatToken: transfer from the zero address"
  | transferToZero                 -- "FiatToken: transfer to the zero address"
  | transferExceedsBalance         -- "FiatToken: transfer amount exceeds balance"
  | burnAmountNotPositive          -- "FiatToken: burn amount not greater than 0"
  | burnExceedsBalance             -- "FiatToken: burn amount exceeds balance"
  | decreasedAllowanceBelowZero    -- "FiatToken: decreased allowance below zero"
  | newMinterAdminZero             -- "FiatToken: new minterAdmin is the zero address"
  -- v1/FiatTokenV1.sol — initialize (FiatToken-prefixed zero-address checks)
  | alreadyInitialized             -- "FiatToken: contract is already initialized"
  | initNewPauserZero              -- "FiatToken: new pauser is the zero address"
  | initNewBlocklisterZero         -- "FiatToken: new blocklister is the zero address"
  | initNewRescuerZero             -- "FiatToken: new rescuer is the zero address"
  | initNewOwnerZero               -- "FiatToken: new owner is the zero address"
  -- v2/FiatTokenV2.sol — allowlist (V2-only) + initializeV2
  | notAllowlister                 -- "FiatToken: caller is not the allowlister"
  | accountNotAllowlisted          -- "FiatToken: account is not allowlisted"
  | newAllowlisterZero             -- "FiatToken: new allowlister is the zero address"
  | initializeV2WrongVersion       -- `require(initializedVersion == 1)` (no reason string)
  -- v1/EIP2612.sol
  | permitExpired                  -- "EIP2612: permit is expired"
  | eip2612InvalidSignature        -- "EIP2612: invalid signature"
  -- v1/EIP3009.sol
  | callerMustBePayee              -- "EIP3009: caller must be the payee"
  | eip3009InvalidSignature        -- "EIP3009: invalid signature"
  | authorizationUsedOrCanceled    -- "EIP3009: authorization is used or canceled"
  | authorizationNotYetValid       -- "EIP3009: authorization is not yet valid"
  | authorizationExpired           -- "EIP3009: authorization is expired"
  deriving DecidableEq, Repr, Inhabited

依存

（なし）