JPYCv2 形式検証

外観

JPYC.requireUnusedAuthorization ​

名称・種別 ​

  • 名称: JPYC.requireUnusedAuthorization
  • 種別: def
  • モジュール: JpycFormalVerification.Signatures
  • ソース: JpycFormalVerification/Signatures.lean:129-132
  • 概要: _requireUnusedAuthorization：認可が未使用であることを要求するガード。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.Bytes32 → Except JPYC.Error Unit

State・認可者 authorizer・nonce を受け取り、その authorization が 未使用 であることを要求するガードです。成功なら () を、使用済みなら revert を返します。

和訳 docstring ​

_requireUnusedAuthorization(authorizer, nonce) ― authorization が未使用であることを要求するガード（v1/EIP3009.sol:213-221）。

解説 ​

何を述べているか。 _requireUnusedAuthorization(authorizer, nonce)（v1/EIP3009.sol:213-221）の写しです。authorizationStates[authorizer][nonce] = 0（未使用）を req で要求し、1（使用済み／キャンセル済み）なら EIP3009: authorization is used or canceled で revert します。

直感。 「この引換券はまだ使われていないか？」を確かめる関所です。使用済みなら門前払いです。

なぜ安全性に効くか。 EIP-3009 の 一回限り性 の入口です。transfer/receive/cancel のいずれもこのガードを通るので、一度 1 になった authorization は二度と通れません。これが transferWithAuthorization_no_replay などのリプレイ防止に直結します。

図解 ​

Lean ソースコード ​

lean
/-- `_requireUnusedAuthorization(authorizer, nonce)` — `v1/EIP3009.sol:213-221`. -/
def requireUnusedAuthorization (s : State) (authorizer : Address) (nonce : Bytes32) :
    Except Error Unit :=
  req (s.authorizationStates authorizer nonce = 0) .authorizationUsedOrCanceled

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/EIP3009.sol:213-221

solidity
function _requireUnusedAuthorization(address authorizer, bytes32 nonce)
    private
    view
{
    require(
        _authorizationStates[authorizer][nonce] == 0,
        "EIP3009: authorization is used or canceled"
    );
}

依存 ​