JPYC.MAX_U256_toNat

名称・種別

• 名称: JPYC.MAX_U256_toNat
• 種別: theorem
• モジュール: JpycFormalVerification.Word
• ソース: JpycFormalVerification/Word.lean:32-33
• 概要: MAX_U256 を自然数に直すと 2^256 − 1 になる、という補題。
• 仕様: 対象外

型シグネチャ

Eq (BitVec.toNat JPYC.MAX_U256) (instHSub.hSub (instHPow.hPow 2 256) 1)

命題「MAX_U256.toNat = 2^256 - 1」を主張する定理です。BitVec.toNat で自然数に直すと、ちょうど最大値になります。

解説

何を述べているか。 MAX_U256 を自然数に変換すると 2^256 - 1 になる、という事実です。

直感。「全ビットが 1 なら最大値」という当たり前のことを、Lean に明示的に伝えます。@[simp] 属性が付いているので、他の証明の中で自動的に書き換えに使われる補助定理です。

なぜ安全性に効くか。 算術補題や無限承認の証明で、ビット表現（BitVec）と数値表現（Nat）を橋渡しする小さな道具になります。

図解

Lean ソースコード

@[simp] theorem MAX_U256_toNat : MAX_U256.toNat = 2 ^ 256 - 1 := by
  simp [MAX_U256]

依存

• JPYC.MAX_U256