JPYC.MAX_U256

名称・種別

• 名称: JPYC.MAX_U256
• 種別: def
• モジュール: JpycFormalVerification.Word
• ソース: JpycFormalVerification/Word.lean:28-30
• 概要: type(uint256).max = 2^256 − 1。transferFrom の無限承認分岐で使う定数。
• 仕様: 対象外

型シグネチャ

JPYC.U256

型 U256 の 定数 で、全ビットが 1、すなわち 2^256 - 1 です。

和訳 docstring

type(uint256).max、すなわち 2^256 - 1。transferFrom の無限承認（infinite-approval）分岐で使う。

解説

何を述べているか。 uint256 の最大値です。BitVec.allOnes 256（全ビット 1）として定義します。

直感。 ERC20 の慣習では「許可額（allowance）が最大値なら無限承認」とみなし、transferFrom のたびにその許可額を減らしません（毎回減らすと使い切ってしまうため）。

なぜ安全性に効くか。 無限承認かどうかの判定基準です。Phase 1 の transferFrom_allowance 定理で「許可額が MAX_U256 のときはそれを変えない」ことを保証するための境界値になります。

図解

Lean ソースコード

/-- `type(uint256).max`, i.e. `2^256 - 1`. Used by the infinite-approval branch
of `transferFrom`. -/
def MAX_U256 : U256 := BitVec.allOnes 256

依存

• JPYC.U256