JPYCv2 形式検証

外観

JPYC.nonces ​

名称・種別 ​

  • 名称: JPYC.nonces
  • 種別: def
  • モジュール: JpycFormalVerification.Signatures
  • ソース: JpycFormalVerification/Signatures.lean:82-83
  • 概要: nonces(owner)：EIP-2612 の現在 nonce を返す読み取り専用ビュー。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.U256

Stateと所有者アドレス owner を受け取り、その所有者の現在の permit nonce（U256）を返す読み取り専用関数です。

和訳 docstring ​

nonces(owner) ― 所有者の現在の permit nonce を返す（v1/EIP2612.sol:57-59）。

解説 ​

何を述べているか。 nonces(owner)（v1/EIP2612.sol:57-59）の写しです。状態 s の permitNonces owner をそのまま返します。

直感。 状態を 読むだけ の関数（Solidity の view）で、書き込みは一切しません。返り値は「その所有者が次に使うべき permit の連番」です。署名を作るクライアントは、まずこの値を読んでメッセージに埋め込みます。

なぜ安全性に効くか。 これ自体は状態を変えませんが、permit のリプレイ防止の「観測点」を定義します。署名は特定の nonce に紐づくので、permit_nonce_increments により消費済みの nonce は二度と一致せず、同じ署名を使い回せません。

図解 ​

Lean ソースコード ​

lean
/-- `nonces(owner)` — `v1/EIP2612.sol:57-59`. -/
def nonces (s : State) (owner : Address) : U256 := s.permitNonces owner

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/EIP2612.sol:57-59

solidity
function nonces(address owner) external view returns (uint256) {
    return _permitNonces[owner];
}

依存 ​