JPYCv2 形式検証

外観

JPYC.permit_signed_by_owner ​

名称・種別 ​

  • 名称: JPYC.permit_signed_by_owner
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:209-216
  • 概要: 成功した permit は owner の EIP-712 署名で認可されている、という定理（権限）。
  • 仕様: 対象

型シグネチャ ​

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 (O.recoverSigner (JPYC.domainSeparatorV4 O s ctx) (JPYC.SignedMessage.permit owner spender value (s.permitNonces owner) deadline) v r sig) owner

permit の成功は、署名が owner を復元したこと（正しい署名者による認可）を含意する、という認可定理です。

和訳 docstring ​

認可。 成功した permit は、消費した nonce を含む EIP-712 Permit メッセージに対する所有者の署名で認可されている。

解説 ​

何を述べているか。 permit が成功したなら、O.recoverSigner (domainSeparatorV4 O s ctx) (.permit owner spender value (s.permitNonces owner) deadline) v r s = owner、すなわち提示された署名 (v, r, s) が確かに owner のものだったことが導けます。内部処理の署名検査ガードの通過条件を取り出します。

直感。 「この操作が通った ⇒ 正規の署名者が署名していた」。SigOracle の recoverSigner が何を返すかに関わらず、復元結果が owner と一致したことが成功の必要条件です。

なぜ安全性に効くか。 署名操作の 認可 の核心です。署名者本人の意思なしに、その人の資産や承認を動かすことはできません。オラクルを全称化しているので、この保証は「どんな復元関数でも」成り立ちます。

図解 ​

Lean ソースコード ​

lean
/-- **Authorization.** A successful `permit` was authorized by the owner's
signature over the EIP-712 `Permit` message (with the consumed nonce). -/
theorem permit_signed_by_owner {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') :
    O.recoverSigner (domainSeparatorV4 O s ctx)
      (.permit owner spender value (s.permitNonces owner) deadline) v r sig = owner :=
  (_permit_ok (permit_eq_ok h)).2.1

依存 ​