JPYCv2 形式検証

外観

JPYC.State.setAuthorizationState ​

名称・種別 ​

  • 名称: JPYC.State.setAuthorizationState
  • 種別: def
  • モジュール: JpycFormalVerification.Signatures
  • ソース: JpycFormalVerification/Signatures.lean:74-78
  • 概要: _authorizationStates[authorizer][nonce] を v に書き換える純粋な状態更新関数。
  • 仕様: 対象外

型シグネチャ ​

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

State・認可者アドレス authorizer・nonce・新しい値 v を受け取り、EIP-3009 の authorization 台帳 authorizationStates のうち (authorizer, nonce) の 1 マスだけを v に差し替えた新しい State を返す純関数です。

和訳 docstring ​

_authorizationStates[authorizer][nonce] = v（EIP-3009 authorization 台帳の該当マスを更新する）。

解説 ​

何を述べているか。 Solidity の二重マッピング代入 _authorizationStates[authorizer][nonce] = v をモデル化したものです。authorizationStates は「アドレス → (Bytes32 → U256)」の入れ子の全域関数で、authorizer の行を取り出してその nonce の 1 点を Function.update で書き換え、それを外側の Function.update で戻します。他の認可者・他の nonce・他のフィールドはそのまま残ります。

直感。 「authorization の使用済み台帳の、特定の (人, 連番) のマスだけを塗る」操作です。v = 1 で「使用済み／キャンセル済み」を表します。

なぜ安全性に効くか。 EIP-3009 の各操作は、署名検証の前にこのマスを 1 にします（使用済みマーク）。更新を 1 マスに限定することで、setAuthorizationState_self（書いた値が読める）と WF_setAuthorizationState（0/1 を保つ）が証明でき、それが authorization の 一回限り性（transferWithAuthorization_marks_used ほか）の土台になります。

図解 ​

Lean ソースコード ​

lean
/-- `_authorizationStates[authorizer][nonce] = v`. -/
def State.setAuthorizationState (s : State) (authorizer : Address) (nonce : Bytes32)
    (v : U256) : State :=
  { s with authorizationStates :=
      Function.update s.authorizationStates authorizer (Function.update (s.authorizationStates authorizer) nonce v) }

依存 ​