JPYCv2 形式検証

外観

JPYC.State.setPermitNonce ​

名称・種別 ​

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

型シグネチャ ​

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

State・所有者アドレス owner・新しい値 v を受け取り、permit 用 nonce マッピング permitNonces のうち owner の 1 点だけを v に差し替えた新しい State を返す純関数です。

和訳 docstring ​

_permitNonces[owner] = v（permit nonce マッピングの該当キーを更新する）。

解説 ​

何を述べているか。 Solidity のマッピング代入 _permitNonces[owner] = v をモデル化したものです。permitNonces は「アドレス → U256」の全域関数で、その owner の 1 点だけを Function.update で書き換え、他のキー・他のフィールドはそのまま残します。

直感。 「permit の連番台帳の、特定アドレスの行だけを書き換える」操作です。他人の nonce には一切影響しません。

なぜ安全性に効くか。 permit は成功のたびにこの関数で nonce を 1 進めます。更新を 1 点に限定することで、setPermitNonce_self（書いた値が読める）と setPermitNonce_permitNonces_ne（他人の nonce は不変）が証明でき、それが permit_nonce_increments と permit_nonce_frame のリプレイ防止につながります。

図解 ​

Lean ソースコード ​

lean
/-- `_permitNonces[owner] = v`. -/
def State.setPermitNonce (s : State) (owner : Address) (v : U256) : State :=
  { s with permitNonces := Function.update s.permitNonces owner v }

依存 ​