JPYCv2 形式検証

外観

JPYC.U8 ​

名称・種別 ​

  • 名称: JPYC.U8
  • 種別: abbrev
  • モジュール: JpycFormalVerification.Word
  • ソース: JpycFormalVerification/Word.lean:21-22
  • 概要: Solidity の uint8 を表す語型（BitVec 8）。decimals や initializedVersion 用。
  • 仕様: 対象外

型シグネチャ ​

lean
Type

Type。BitVec 8 の別名（abbrev）です。

和訳 docstring ​

Solidity の uint8（例: decimals, initializedVersion）。

解説 ​

何を述べているか。 8 ビットの符号なし整数の型です。

直感。 decimals（小数桁数）や initializedVersion（初期化バージョン）のような小さな値に使います。initializedVersion は WF によって 0 / 1 / 2 のみを取ります。

なぜ安全性に効くか。 値域が小さいフィールドを適切な幅で表すことで、モデルが Solidity の型と忠実に対応します。

図解 ​

Lean ソースコード ​

lean
/-- A Solidity `uint8` (e.g. `decimals`, `initializedVersion`). -/
abbrev U8 : Type := BitVec 8

依存 ​

（なし）