JPYCv2 形式検証

外観

JPYC.authorizationState ​

名称・種別 ​

  • 名称: JPYC.authorizationState
  • 種別: def
  • モジュール: JpycFormalVerification.Signatures
  • ソース: JpycFormalVerification/Signatures.lean:85-87
  • 概要: authorizationState(authorizer,nonce)：認可の使用済み状態を返す読み取り専用ビュー。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.Bytes32 → Bool

State・認可者 authorizer・nonce を受け取り、その authorization が使用済み（またはキャンセル済み）かを Bool で返す読み取り専用関数です。

和訳 docstring ​

authorizationState(authorizer, nonce) ― その authorization が使用済み/キャンセル済みかを返す（v1/EIP3009.sol:80-86）。

解説 ​

何を述べているか。 authorizationState(authorizer, nonce)（v1/EIP3009.sol:80-86）の写しです。authorizationStates[authorizer][nonce] == 1 を判定して返します。

直感。 状態を 読むだけ の関数です。返り値は、その (認可者, nonce) のマスが 1（使用済み／キャンセル済み）なら true、0（未使用）なら false です。クライアントは送信前にこれで「この authorization はまだ使えるか」を確認できます。

なぜ安全性に効くか。 EIP-3009 の一回限り性の「観測点」です。各操作が成功すると対応するマスが 1 になる（transferWithAuthorization_marks_used など）ため、この view で true を返す authorization はもう二度と通りません。

図解 ​

Lean ソースコード ​

lean
/-- `authorizationState(authorizer, nonce)` — `v1/EIP3009.sol:80-86`. -/
def authorizationState (s : State) (authorizer : Address) (nonce : Bytes32) : Bool :=
  s.authorizationStates authorizer nonce == 1

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/EIP3009.sol:80-86

solidity
function authorizationState(address authorizer, bytes32 nonce)
    external
    view
    returns (bool)
{
    return _authorizationStates[authorizer][nonce] == 1;
}

依存 ​