JPYCv2 形式検証

外観

JPYC.permit_nonce_frame ​

名称・種別 ​

  • 名称: JPYC.permit_nonce_frame
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:189-198
  • 概要: 成功した permit は owner 以外の nonce を変えない、という定理（nonce frame）。
  • 仕様: 対象

型シグネチャ ​

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') → ∀ {a : JPYC.Address}, Ne a owner → Eq (s'.permitNonces a) (s.permitNonces a)

permit の成功は、所有者以外のすべてのアドレスの nonce を変えない、というフレーム定理です。

和訳 docstring ​

nonce フレーム。 成功した permit は所有者以外の nonce を変えない。

解説 ​

何を述べているか。 permit が成功したとき、owner と異なる任意のアドレス a について s'.permitNonces a = s.permitNonces a です。nonce を触る更新は setPermitNonce owner _ だけなので、a ≠ owner では setPermitNonce_permitNonces_ne で元の値に戻ります（_approve も nonce に触れません）。

直感。 「ある人の承認を処理しても、他人の nonce は一切動かない」。

なぜ安全性に効くか。 フレーム性 の保証です。permit の効果が所有者 1 人に局所化され、無関係なアカウントの nonce が勝手に進む（＝その人の将来の署名が壊れる）ことを排除します。

図解 ​

Lean ソースコード ​

lean
/-- **Nonce frame.** A successful `permit` leaves every nonce other than the
owner's untouched. -/
theorem permit_nonce_frame {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') {a : Address}
    (ha : a ≠ owner) : s'.permitNonces a = s.permitNonces a := by
  obtain ⟨_, _, nextNonce, _, happ⟩ := _permit_ok (permit_eq_ok h)
  obtain ⟨_, _, rfl⟩ := _approve_ok happ
  rw [setAllowance_permitNonces]
  exact setPermitNonce_permitNonces_ne s owner a nextNonce ha

依存 ​