JPYCv2 形式検証

外観

JPYC.transferWithAuthorization ​

名称・種別 ​

  • 名称: JPYC.transferWithAuthorization
  • 種別: def
  • モジュール: JpycFormalVerification.Signatures
  • ソース: JpycFormalVerification/Signatures.lean:171-179
  • 概要: transferWithAuthorization(...)：署名認可で第三者が送金を実行する EIP-3009 関数。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.SigOracle → JPYC.State → JPYC.CallContext → JPYC.Address → JPYC.Address → JPYC.U256 → JPYC.U256 → JPYC.U256 → JPYC.Bytes32 → JPYC.U8 → JPYC.Bytes32 → JPYC.Bytes32 → Except JPYC.Error JPYC.State

EIP-3009 の transferWithAuthorization 関数です。署名された認可に基づき、from から to へ value を送金します。署名オラクル O の下で定義されます。

和訳 docstring ​

transferWithAuthorization(...) ― 署名された認可に基づく送金（v2/FiatTokenV2.sol:445-473）。

解説 ​

何を述べているか。 transferWithAuthorization(...)（v2/FiatTokenV2.sol:445-473）の写しです。先頭で whenNotPaused・notBlocklisted（from/to）・checkAllowlist を通し、内部 _transferWithAuthorization に委譲します。内部処理は (1) requireValidAuthorization（有効ウィンドウ＋未使用）、(2) 署名が from を復元するか検証、(3) authorization を使用済みにマーク（setAuthorizationState from nonce 1）、(4) _transfer で実際に送金、という順です。

直感。 「from がオフチェーンで署名した送金指示を、第三者がチェーンに持ち込んで実行する」操作です。permit と似ていますが、こちらは承認ではなく 送金そのもの を署名で動かします。使用済みマークが署名検証の後・送金の前に置かれます。

なぜ安全性に効くか。 各 authorization は (from, nonce) で識別され、一度使うと 1 になるので二度は通りません（transferWithAuthorization_no_replay）。有効期間（_within_window）・署名者（_signed_by_from）・供給保存（_conserves）も定理化されています。なお transferWithAuthorization には受取人チェックが ない（誰でも実行できる）点が、次の receiveWithAuthorization との違いです。

図解 ​

Lean ソースコード ​

lean
/-- `transferWithAuthorization(…)` — `v2/FiatTokenV2.sol:445-473`. -/
def transferWithAuthorization (s : State) (ctx : CallContext) (frm dst : Address)
    (value validAfter validBefore : U256) (nonce : Bytes32) (v : U8) (r sig : Bytes32) :
    Except Error State := do
  whenNotPaused s
  notBlocklisted s frm
  notBlocklisted s dst
  checkAllowlist s frm value
  _transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:445-473

solidity
function transferWithAuthorization(
    address from, address to, uint256 value,
    uint256 validAfter, uint256 validBefore, bytes32 nonce,
    uint8 v, bytes32 r, bytes32 s
)
    external
    whenNotPaused
    notBlocklisted(from)
    notBlocklisted(to)
    checkAllowlist(from, value)
{
    _transferWithAuthorization(
        from, to, value, validAfter, validBefore, nonce, v, r, s);
}

依存 ​