JPYCv2 形式検証

外観

JPYC.Bytes32 ​

名称・種別 ​

  • 名称: JPYC.Bytes32
  • 種別: abbrev
  • モジュール: JpycFormalVerification.Word
  • ソース: JpycFormalVerification/Word.lean:24-26
  • 概要: Solidity の bytes32 を表す語型。U256 と同一だが可読性のため別名で保持。
  • 仕様: 対象外

型シグネチャ ​

lean
Type

Type。BitVec 256 の別名（abbrev）で、語幅は U256 と同一です。

和訳 docstring ​

Solidity の bytes32（例: EIP-3009 の nonce、EIP-712 のドメインセパレータ）。語幅は U256 と同一だが、可読性のため別名として維持している。

解説 ​

何を述べているか。 32 バイト = 256 ビットのバイト列の型です。

直感。 ハッシュ値や署名の nonce（使い捨て番号）、EIP-712 のドメインセパレータなどに使います。中身は U256 と同じ BitVec 256 ですが、「これは数値ではなくバイト列だ」という意図を名前で示しています。

なぜ安全性に効くか。 数値とバイト列を名前で区別することで、署名まわりのフィールド（domainSeparator や authorizationStates のキー）が「計算する数」ではなく「識別子」であることを読み手に伝え、誤用を防ぎます。

図解 ​

Lean ソースコード ​

lean
/-- A Solidity `bytes32` (e.g. EIP-3009 nonces, the EIP-712 domain separator).
Word-identical to `U256`; kept as a distinct alias for readability. -/
abbrev Bytes32 : Type := BitVec 256

依存 ​

（なし）