JPYCv2 形式検証

外観

JPYC.transferWithAuthorization_signed_by_from ​

名称・種別 ​

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

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {frm dst : JPYC.Address} {value validAfter validBefore : JPYC.U256} {nonce : JPYC.Bytes32} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s') → Eq (O.recoverSigner (JPYC.domainSeparatorV4 O s ctx) (JPYC.SignedMessage.transferWithAuthorization frm dst value validAfter validBefore nonce) v r sig) frm

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

和訳 docstring ​

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

解説 ​

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

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

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

図解 ​

Lean ソースコード ​

lean
/-- **Authorization.** A successful `transferWithAuthorization` was authorized by
`from`'s signature. -/
theorem transferWithAuthorization_signed_by_from {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32}
    (h : transferWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s') :
    O.recoverSigner (domainSeparatorV4 O s ctx)
      (.transferWithAuthorization frm dst value validAfter validBefore nonce) v r sig = frm :=
  (_transferWithAuthorization_ok (transferWithAuthorization_eq_ok h)).2.2.2.1

依存 ​