JPYC.SigOracle

名称・種別

名称: JPYC.SigOracle
種別: structure
モジュール: JpycFormalVerification.Signatures
ソース: JpycFormalVerification/Signatures.lean:53-63
概要: keccak256/ECDSA 復元を信頼するオラクルとして抽象化した署名プリミティブ一式。
仕様: 対象外

型シグネチャ

lean

Type

署名まわりの暗号プリミティブを束ねた 信頼できるオラクル（structure） です。フィールドは 2 つ ―― ドメインセパレータを作る makeDomainSeparator と、署名から署名者を復元する recoverSigner です。

和訳 docstring

署名検証の暗号プリミティブ（makeDomainSeparator と recoverSigner）を抽象化した信頼オラクル。keccak256 / ECDSA 復元はモデル化せず、全定理はこのオラクルについて全称化される。

解説

何を述べているか。 permit（EIP-2612）や EIP-3009 の各操作は電子署名を検証します。その検証には keccak256 ハッシュと ecrecover（ECDSA 署名からアドレスを復元する関数）が必要ですが、それらの内部実装の正しさはこのプロジェクトの検証対象外 です（入門の §3.8・「証明しないこと」を参照）。そこで makeDomainSeparator : String → String → U256 → Bytes32 と recoverSigner : Bytes32 → SignedMessage → U8 → Bytes32 → Bytes32 → Address の 2 つを抽象的なオラクルとして切り出します。

直感。 「署名検証はブラックボックスに任せる」という設計です。重要なのは、これ以降の すべての定義・定理が variable (O : SigOracle) の下で書かれている点です。つまり安全性の主張は「どんなオラクル O であっても成り立つ」という形になります。

なぜ安全性に効くか。 「署名検証が具体的に何を返そうと、nonce の単調増加・authorization の一回限り性・有効期限チェックといった性質は崩れない」ことを、オラクルを全称化することで明示します。これによりモデルは 公理（axiom）を一切増やさずに、しかも実行可能（Tests.lean では具体的なモックオラクルを与える）なまま保たれます。chainId を makeDomainSeparator に明示的に渡しているのは、address(this) がスコープ外だからです。

図解

Lean ソースコード

lean

/-- The trusted cryptographic primitives, abstracted as a signature oracle (see
the file header). `makeDomainSeparator` is `EIP712.makeDomainSeparator`
(`util/EIP712.sol:40-60`); `recoverSigner` is `EIP712.recover` ∘
`ECRecover.recover` (`util/EIP712.sol:71-86`, `util/ECRecover.sol:48-79`).
`chainId` is passed to `makeDomainSeparator` explicitly because `address(this)`
is out of scope; keccak256 / ECDSA recovery are not modeled. -/
structure SigOracle where
  /-- `EIP712.makeDomainSeparator(name, version)` (the `chainId` is threaded in). -/
  makeDomainSeparator : String → String → U256 → Bytes32
  /-- `EIP712.recover(domainSeparator, v, r, s, abi.encode(message))`. -/
  recoverSigner : Bytes32 → SignedMessage → U8 → Bytes32 → Bytes32 → Address

対応 Solidity ソースコード

reference/JPYCv2/contracts/util/EIP712.sol:40-60, reference/JPYCv2/contracts/util/EIP712.sol:71-86, reference/JPYCv2/contracts/util/ECRecover.sol:48-79

solidity

// util/EIP712.sol:40-60 — makeDomainSeparator
function makeDomainSeparator(string memory name, string memory version)
    internal view returns (bytes32)
{
    uint256 chainId;
    assembly { chainId := chainid() }
    return keccak256(abi.encode(
        0x8b73c3c69bb8fe3d512ecc4cf759cc79239f7b179b0ffacaa9a75d522b39400f,
        keccak256(bytes(name)), keccak256(bytes(version)),
        chainId, address(this)));
}

// util/EIP712.sol:71-86 — recover (∘ ECRecover.recover, util/ECRecover.sol:48-79)
function recover(
    bytes32 domainSeparator, uint8 v, bytes32 r, bytes32 s,
    bytes memory typeHashAndData
) internal pure returns (address) {
    bytes32 digest = keccak256(abi.encodePacked(
        "\x19\x01", domainSeparator, keccak256(typeHashAndData)));
    return ECRecover.recover(digest, v, r, s);
}

依存

（なし）

JPYC.SigOracle ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​