JPYCv2 形式検証

外観

JPYC.domainSeparatorV4 ​

名称・種別 ​

  • 名称: JPYC.domainSeparatorV4
  • 種別: def
  • モジュール: JpycFormalVerification.Signatures
  • ソース: JpycFormalVerification/Signatures.lean:93-98
  • 概要: _domainSeparatorV4()：chainid 一致ならキャッシュ値、不一致ならオラクルで再計算するドメイン区切り子。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.SigOracle → JPYC.State → JPYC.CallContext → JPYC.Bytes32

StateとCallContextを受け取り、EIP-712 の ドメインセパレータ（Bytes32）を返す関数です。署名オラクル O の下で定義されます。

和訳 docstring ​

_domainSeparatorV4() ― block.chainid がキャッシュ時と一致すれば保存済みドメインセパレータ、違えばオラクルで再計算して返す（v1/EIP712Domain.sol:53-59）。

解説 ​

何を述べているか。 _domainSeparatorV4()（v1/EIP712Domain.sol:53-59）の写しです。現在の block.chainid（CallContext の blockChainId）が、コントラクトに保存された chainId と一致すれば、キャッシュ済みの domainSeparator をそのまま返します。一致しなければ（チェーンが分岐＝ハードフォークした場合など）、オラクルの makeDomainSeparator で 再計算します。

直感。 ドメインセパレータは「この署名はどのコントラクト・どのチェーン向けか」を縛る指紋です。通常はキャッシュを返して計算を節約し、チェーン ID が変わったときだけ作り直します。

なぜ安全性に効くか。 署名の有効範囲を「正しいチェーン」に限定する仕組みです。チェーンが分岐しても、再計算により別チェーンへのリプレイを防ぎます。署名検証（recoverSigner）はこのドメインセパレータを入力に取るため、ここが正しく分岐することが各 *_signed_by_* 定理の前提になります。

図解 ​

Lean ソースコード ​

lean
/-- `_domainSeparatorV4()` — returns the cached `DOMAIN_SEPARATOR` when the
current `block.chainid` matches the stored `CHAIN_ID`, else recomputes it via the
oracle. Source: `v1/EIP712Domain.sol:53-59`. -/
def domainSeparatorV4 (s : State) (ctx : CallContext) : Bytes32 :=
  if ctx.blockChainId = s.chainId then s.domainSeparator
  else O.makeDomainSeparator s.domainName s.version ctx.blockChainId

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v1/EIP712Domain.sol:53-59

solidity
function _domainSeparatorV4() public view returns (bytes32) {
    if(block.chainid == CHAIN_ID) {
        return DOMAIN_SEPARATOR;
    } else {
        return EIP712.makeDomainSeparator(NAME, VERSION);
    }
}

依存 ​