JPYCv2 形式検証

外観

JPYC.receiveWithAuthorization_payee ​

名称・種別 ​

  • 名称: JPYC.receiveWithAuthorization_payee
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:432-440
  • 概要: receiveWithAuthorization の成功は payee が呼び出し元（to == msg.sender）であることを含意する（フロントラン防止）。
  • 仕様: 対象

型シグネチャ ​

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.receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s') → Eq dst ctx.sender

receiveWithAuthorization の成功は、受取人が呼び出し元自身（to == msg.sender）だったことを含意する、という フロントランニング対策 の定理です。

和訳 docstring ​

受取人チェック。 成功した receiveWithAuthorization は to == msg.sender を含意する（transferWithAuthorization が意図的に持たないフロントラン対策ガード）。

解説 ​

何を述べているか。 receiveWithAuthorization が成功したなら dst = ctx.sender、すなわち「受取人＝この関数を呼んだ人」です。内部 _receiveWithAuthorization 先頭の require(to == msg.sender) の通過条件を取り出します。

直感。 「自分宛ての署名付き送金は、自分自身でしか実行できない」。transferWithAuthorization は誰でも実行できるため、攻撃者が他人の署名を先回りして別の文脈（別のトランザクション順序など）で実行する余地がありますが、receiveWithAuthorization は実行者を受取人に固定してそれを封じます。

なぜ安全性に効くか。 これが EIP-3009 の receive 系が transfer 系に 追加 している唯一のガードであり、フロントランニング攻撃への対策です。transferWithAuthorization は設計上この保証を持たない（誰でも持ち込める）ことと対になっています。

図解 ​

Lean ソースコード ​

lean
/-- **Payee check.** A successful `receiveWithAuthorization` implies the payee is
the caller (`to == msg.sender`) — the front-running guard that
`transferWithAuthorization` deliberately omits. -/
theorem receiveWithAuthorization_payee {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32}
    (h : receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s') :
    dst = ctx.sender :=
  (_receiveWithAuthorization_ok (receiveWithAuthorization_eq_ok h)).1

依存 ​