JPYCv2 形式検証

外観

JPYC.cancelAuthorization_signed_by_authorizer ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {authorizer : JPYC.Address} {nonce : JPYC.Bytes32} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.cancelAuthorization O s ctx authorizer nonce v r sig) (Except.ok s') → Eq (O.recoverSigner (JPYC.domainSeparatorV4 O s ctx) (JPYC.SignedMessage.cancelAuthorization authorizer nonce) v r sig) authorizer

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

和訳 docstring ​

認可。 成功した cancelAuthorization は authorizer の署名で認可されている。

解説 ​

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

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

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

図解 ​

Lean ソースコード ​

lean
/-- **Authorization.** A successful `cancelAuthorization` was signed by the authorizer. -/
theorem cancelAuthorization_signed_by_authorizer {O : SigOracle} {s s' : State} {ctx : CallContext}
    {authorizer : Address} {nonce : Bytes32} {v : U8} {r sig : Bytes32}
    (h : cancelAuthorization O s ctx authorizer nonce v r sig = .ok s') :
    O.recoverSigner (domainSeparatorV4 O s ctx)
      (.cancelAuthorization authorizer nonce) v r sig = authorizer :=
  (_cancelAuthorization_ok (cancelAuthorization_eq_ok h)).2.1

依存 ​