JPYC.add?_eq_ok

名称・種別

• 名称: JPYC.add?_eq_ok
• 種別: theorem
• モジュール: JpycFormalVerification.Word
• ソース: JpycFormalVerification/Word.lean:50-52
• 概要: add? が成功したなら結果は通常の和であり桁あふれしていない、という補題。
• 仕様: 対象

型シグネチャ

∀ {a b r : JPYC.U256}, Eq (JPYC.add? a b) (Except.ok r) → And (Eq r (instHAdd.hAdd a b)) (instLTNat.lt (instHAdd.hAdd (BitVec.toNat a) (BitVec.toNat b)) (instHPow.hPow 2 256))

「add? a b = .ok r ならば、r = a + b かつ 和は 256 ビットに収まる」という定理です。成功という結果から、その内訳を取り出します。

解説

何を述べているか。 add? が成功したとき、その結果 r が和に等しく、かつオーバーフローしていなかったことを取り出す 除去（elimination）補題 です。

直感。「成功した」という事実から、逆に「条件が満たされていた／結果が何だったか」を読み出します。証明では add? を展開して if を場合分け（split）するだけです。

なぜ安全性に効くか。 多くの上位証明が「add? が成功した」という仮定から「和が収まっていた・結果は和だ」を引き出すのに使う、中心的な補題です。add?_toNat もこれを経由します。

図解

Lean ソースコード

theorem add?_eq_ok {a b r : U256} (h : add? a b = .ok r) :
    r = a + b ∧ a.toNat + b.toNat < 2 ^ 256 := by
  unfold add? at h; split at h <;> simp_all

依存

• JPYC.Error
• JPYC.U256
• JPYC.add?