JPYC.add?_of_lt
名称・種別
- 名称:
JPYC.add?_of_lt - 種別: theorem
- モジュール:
JpycFormalVerification.Word - ソース:
JpycFormalVerification/Word.lean:47-48 - 概要: 和が 2^256 未満なら add? は成功して通常の和を返す、という補題。
- 仕様: 対象
型シグネチャ
lean
∀ {a b : JPYC.U256}, instLTNat.lt (instHAdd.hAdd (BitVec.toNat a) (BitVec.toNat b)) (instHPow.hPow 2 256) → Eq (JPYC.add? a b) (Except.ok (instHAdd.hAdd a b))「和が 256 ビットに収まる（a.toNat + b.toNat < 2^256）ならば、add? a b = .ok (a + b)」という定理です。前提 → 結論の形をしています。
解説
何を述べているか。 あふれない前提のもとでは add? は必ず成功して和を返す、という 導入（introduction）補題 です。
直感。 add? の定義の if 条件が真なら then の枝（成功）に入る、という当たり前の事実を定理にしたものです。
なぜ安全性に効くか。 上限が分かっているときに「加算が成功する」ことを示す道具で、round-trip 補題 sub?_add?_cancel などの部品として使われます。
図解
Lean ソースコード
lean
theorem add?_of_lt {a b : U256} (h : a.toNat + b.toNat < 2 ^ 256) :
add? a b = .ok (a + b) := by simp [add?, h]