JPYCv2 形式検証

外観

JPYC.permit ​

名称・種別 ​

  • 名称: JPYC.permit
  • 種別: def
  • モジュール: JpycFormalVerification.Signatures
  • ソース: JpycFormalVerification/Signatures.lean:118-125
  • 概要: permit(owner,spender,value,deadline,v,r,s)：署名で承認を設定する EIP-2612 関数。
  • 仕様: 対象外

型シグネチャ ​

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

EIP-2612 の permit 関数です。署名でオフチェーン承認を行い、allowed[owner][spender] を value に設定します。署名オラクル O の下で定義されます。

和訳 docstring ​

permit(owner, spender, value, deadline, v, r, s) ― 署名による承認（v2/FiatTokenV2.sol:548-564）。

解説 ​

何を述べているか。 permit(owner, spender, value, deadline, v, r, s)（v2/FiatTokenV2.sol:548-564）の写しです。先頭で 4 つの modifier ガード ―― whenNotPaused（停止中でない）・notBlocklisted を owner/spender に・checkAllowlist（上限超なら owner が許可リスト登録済み）―― を順に通し、内部 _permit に委譲します。_permit は (1) deadline ≥ block.timestamp（期限内）を確認、(2) 現在の nonce を読み、checked add? で +1 して書き込み（post-increment）、(3) その状態でドメインセパレータを作り、署名が owner を復元するか検証、(4) _approve で許可額を設定、という流れです。

直感。 「ガス代を払う人（spender など）と、承認する人（owner）を分離できる承認」です。owner はオフチェーンで署名するだけで、誰かがそれをチェーンに持ち込めます。nonce のインクリメントが署名検証より前に行われる点が重要で、これにより不正な署名でも nonce 書き込みは試みられますが、署名検証で失敗すれば revert され、その書き込みごと巻き戻されます（permit_revert_noop）。

なぜ安全性に効くか。 EIP-2612 の安全性の核心は リプレイ防止 です。各署名は特定の nonce に紐づき、成功時に nonce が 1 増えるので（permit_nonce_increments）、同じ署名は二度と通りません。また期限（permit_not_expired）・署名者（permit_signed_by_owner）・効果（permit_sets_allowance）がそれぞれ定理化されています。

図解 ​

Lean ソースコード ​

lean
/-- `permit(owner, spender, value, deadline, v, r, s)` — `v2/FiatTokenV2.sol:548-564`. -/
def permit (s : State) (ctx : CallContext) (owner spender : Address)
    (value deadline : U256) (v : U8) (r sig : Bytes32) : Except Error State := do
  whenNotPaused s
  notBlocklisted s owner
  notBlocklisted s spender
  checkAllowlist s owner value
  _permit O s ctx owner spender value deadline v r sig

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:548-564

solidity
function permit(
    address owner,
    address spender,
    uint256 value,
    uint256 deadline,
    uint8 v,
    bytes32 r,
    bytes32 s
)
    external
    whenNotPaused
    notBlocklisted(owner)
    notBlocklisted(spender)
    checkAllowlist(owner, value)
{
    _permit(owner, spender, value, deadline, v, r, s);
}

依存 ​