JPYC.SignedMessage

名称・種別

• 名称: JPYC.SignedMessage
• 種別: inductive
• モジュール: JpycFormalVerification.Signatures
• ソース: JpycFormalVerification/Signatures.lean:40-51
• 概要: FiatTokenV2 が使う *_TYPEHASH ごとに 1 コンストラクタを持つ EIP-712 型付きメッセージ。
• 仕様: 対象外

型シグネチャ

Type

EIP-712 の型付きメッセージを表す 直和型（inductive） です。FiatTokenV2 が使う 4 つの *_TYPEHASH（permit / transferWithAuthorization / receiveWithAuthorization / cancelAuthorization）に 1 対 1 対応する 4 つのコンストラクタを持ちます。

和訳 docstring

FiatTokenV2 が使う各 *_TYPEHASH に 1 コンストラクタずつ対応する、EIP-712 の型付きメッセージ。

解説

何を述べているか。 Ethereum の署名対象は「型ハッシュ（TYPEHASH）＋各フィールド」を abi.encode したバイト列です。本モデルでは、それを不透明な bytes のままにせず、メッセージ種別ごとに 1 コンストラクタ（引数はその abi.encode の引数列そのまま）として表現します。permit owner spender value nonce deadline、transferWithAuthorization frm dst value validAfter validBefore nonce など、署名された各フィールドが型レベルで見えるようになります。

直感。 「この署名は “誰が・誰に・いくら・どの nonce で” という、どのメッセージに対するものか」を、構造化したデータとして保持します。recoverSigner オラクル（SigOracle）は、この SignedMessage と署名 (v, r, s) を受け取り、復元した署名者アドレスを返します。

なぜ安全性に効くか。 フィールドを型で明示することで、「ある操作の署名」と「別の操作の署名」が決して取り違えられないことが、定義の段階で保証されます。たとえば transferWithAuthorization_signed_by_from は「transferWithAuthorization 構成子のメッセージ」に対する署名を要求するので、permit 用の署名で送金を通す、といったクロスプロトコルのリプレイが型レベルで排除されます。

図解

Lean ソースコード

/-- An EIP-712 typed message, one constructor per `*_TYPEHASH` used by
`FiatTokenV2`. -/
inductive SignedMessage where
  /-- `PERMIT_TYPEHASH` — `v1/EIP2612.sol:46-48`. -/
  | permit (owner spender : Address) (value nonce deadline : U256)
  /-- `TRANSFER_WITH_AUTHORIZATION_TYPEHASH` — `v1/EIP3009.sol:49-51`. -/
  | transferWithAuthorization (frm dst : Address) (value validAfter validBefore : U256) (nonce : Bytes32)
  /-- `RECEIVE_WITH_AUTHORIZATION_TYPEHASH` — `v1/EIP3009.sol:53-55`. -/
  | receiveWithAuthorization (frm dst : Address) (value validAfter validBefore : U256) (nonce : Bytes32)
  /-- `CANCEL_AUTHORIZATION_TYPEHASH` — `v1/EIP3009.sol:57-59`. -/
  | cancelAuthorization (authorizer : Address) (nonce : Bytes32)
  deriving DecidableEq, Repr

依存

（なし）