JPYC.permit_nonce_increments
名称・種別
- 名称:
JPYC.permit_nonce_increments - 種別: theorem
- モジュール:
JpycFormalVerification.SignaturesTheorems - ソース:
JpycFormalVerification/SignaturesTheorems.lean:174-187 - 概要: 成功した permit は owner の nonce をちょうど 1 増やす、という定理（再生防止）。
- 仕様: 対象
型シグネチャ
lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {owner spender : JPYC.Address} {value deadline : JPYC.U256} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.permit O s ctx owner spender value deadline v r sig) (Except.ok s') → Eq (BitVec.toNat (s'.permitNonces owner)) (instHAdd.hAdd (BitVec.toNat (s.permitNonces owner)) 1)permit の成功は、所有者の nonce を（自然数換算で）ちょうど 1 増やす、という リプレイ防止 の中核定理です。
和訳 docstring
nonce 単調増加（リプレイ防止）。 成功した permit は所有者の nonce をちょうど 1 増やす（消費した nonce は二度と現れない）。
解説
何を述べているか。 permit が成功すると (s'.permitNonces owner).toNat = (s.permitNonces owner).toNat + 1 です。_permit は現在の nonce を読み、checked add? で +1 して書き込みます。add? が成功した時点であふれは起きていないので（add?_toNat）、ℕ 上の素直な +1 になります。後続の _approve は nonce に触れません（setAllowance_permitNonces）。
直感。 「承認を 1 回使うと、次の連番に進む」。署名は特定の nonce に紐づくので、消費された nonce は二度と現れません。
なぜ安全性に効くか。 EIP-2612 の リプレイ防止 そのものです。同じ署名（同じ nonce 向け）を再送しても、nonce が既に進んでいるため署名検証で別メッセージ扱いとなり、通りません。
図解
Lean ソースコード
lean
/-- **Nonce monotonicity (replay protection).** A successful `permit` increments
the owner's nonce by exactly one (so the signed nonce is consumed and can never
recur). -/
theorem permit_nonce_increments {O : SigOracle} {s s' : State} {ctx : CallContext}
{owner spender : Address} {value deadline : U256} {v : U8} {r sig : Bytes32}
(h : permit O s ctx owner spender value deadline v r sig = .ok s') :
(s'.permitNonces owner).toNat = (s.permitNonces owner).toNat + 1 := by
obtain ⟨_, _, nextNonce, hadd, happ⟩ := _permit_ok (permit_eq_ok h)
obtain ⟨_, _, rfl⟩ := _approve_ok happ
have hn : (((s.setPermitNonce owner nextNonce).setAllowance owner spender value).permitNonces owner)
= nextNonce := by simp
rw [hn]
have := add?_toNat hadd
simpa using this