JPYCv2 形式検証

外観

JPYC.U256 ​

名称・種別 ​

  • 名称: JPYC.U256
  • 種別: abbrev
  • モジュール: JpycFormalVerification.Word
  • ソース: JpycFormalVerification/Word.lean:18-19
  • 概要: Solidity の uint256 を表す語型（BitVec 256）。
  • 仕様: 対象外

型シグネチャ ​

lean
Type

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

和訳 docstring ​

Solidity の uint256。

解説 ​

何を述べているか。 256 ビットの符号なし整数の型です（primer §3.2）。

直感。 残高・許可額・供給量など「お金の量」はすべてこの型で表します。固定長なので桁あふれ（オーバーフロー）が起こりえます。だからこそ加減算は checked 演算 add? / sub? を通します。

なぜ安全性に効くか。 モデル全体の数値の土台です。BitVec なので等価判定・有限性が付随し、Σ balances の表現や各種算術補題の基盤になります。

図解 ​

Lean ソースコード ​

lean
/-- A Solidity `uint256`. -/
abbrev U256 : Type := BitVec 256

依存 ​

（なし）