JPYCv2 形式検証

外観

JPYC.Error.revertMessage ​

名称・種別 ​

  • 名称: JPYC.Error.revertMessage
  • 種別: def
  • モジュール: JpycFormalVerification.Error
  • ソース: JpycFormalVerification/Error.lean:78-126
  • 概要: 各 Error をオンチェーンの revert 理由文字列に 1:1 で対応づける関数。
  • 仕様: 対象

型シグネチャ ​

lean
JPYC.Error → String

Error → String：失敗理由（Error）を受け取り、オンチェーンで実際に返る 理由文字列 を返す全域関数です。

和訳 docstring ​

各エラーに対応する、正確なオンチェーン revert 理由文字列。

理由文字列なしで revert する require（Solidity の Panic や素の require(cond)）は空文字列 "" に対応し、理由データを返さない EVM の挙動と一致する。

解説 ​

何を述べているか。 Error の各値を、実際にチェーン上で返る文字列（例:「Pausable: paused」）へ写す対応表です。

直感。 モデルの失敗が「現実にどう見えるか」を結びつけます。理由文字列を持たない失敗（算術 Panic や initializeV2WrongVersion の require(initializedVersion == 1)）は空文字列 "" になります。

なぜ安全性に効くか。 モデルの revert と実コントラクトの revert を 文字列レベルで照合 でき、モデルが忠実である（fidelity）ことの強い証拠になります。監査者は理由文字列から「どの require か」を逆引きでき、Lean とソースの対応を確認できます。

図解 ​

Lean ソースコード ​

lean
/-- The exact on-chain revert reason string for each error.

A reverting `require` with no reason string (Solidity `Panic` or a bare
`require(cond)`) maps to the empty string `""`, matching the EVM behavior of
returning no reason data. -/
def Error.revertMessage : Error → String
  | .arithmeticOverflow             => ""  -- Panic(0x11)
  | .arithmeticUnderflow            => ""  -- Panic(0x11)
  | .notOwner                       => "Ownable: caller is not the owner"
  | .newOwnerZero                   => "Ownable: new owner is the zero address"
  | .paused                         => "Pausable: paused"
  | .notPauser                      => "Pausable: caller is not the pauser"
  | .pausableNewPauserZero          => "Pausable: new pauser is the zero address"
  | .notBlocklister                 => "Blocklistable: caller is not the blocklister"
  | .accountBlocklisted             => "Blocklistable: account is blocklisted"
  | .blocklistableNewBlocklisterZero => "Blocklistable: new blocklister is the zero address"
  | .notRescuer                     => "Rescuable: caller is not the rescuer"
  | .rescuableNewRescuerZero        => "Rescuable: new rescuer is the zero address"
  | .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"
  | .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"
  | .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)
  | .permitExpired                  => "EIP2612: permit is expired"
  | .eip2612InvalidSignature        => "EIP2612: invalid signature"
  | .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"

依存 ​