JPYC.add?_toNat

名称・種別

• 名称: JPYC.add?_toNat
• 種別: theorem
• モジュール: JpycFormalVerification.Word
• ソース: JpycFormalVerification/Word.lean:54-58
• 概要: 成功した add? は自然数加算と一致する（ラップアラウンドしない）、という補題。
• 仕様: 対象

型シグネチャ

∀ {a b r : JPYC.U256}, Eq (JPYC.add? a b) (Except.ok r) → Eq (BitVec.toNat r) (instHAdd.hAdd (BitVec.toNat a) (BitVec.toNat b))

「add? a b = .ok r ならば r.toNat = a.toNat + b.toNat」という定理です。成功時には、ビット演算の結果と自然数の和が一致します。

和訳 docstring

成功した add? は自然数の加算と一致する（ラップアラウンドなし）。

解説

何を述べているか。 加算が成功したなら、結果を自然数に直したものは元の自然数和に 完全一致 する（途中で 2^256 を法とした丸めが起きない）、という主張です。

直感。「あふれていない」のだから、ビット演算の結果は普通の足し算と同じになる、ということです。

なぜ安全性に効くか。 残高合計などを自然数で扱う供給保存の証明で、ビットの世界と自然数の世界を安全に行き来するための橋です。証明は add?_eq_ok を使い、BitVec.toNat_add と omega で締めます。

図解

Lean ソースコード

/-- A successful `add?` agrees with natural-number addition (no wraparound). -/
theorem add?_toNat {a b r : U256} (h : add? a b = .ok r) :
    r.toNat = a.toNat + b.toNat := by
  obtain ⟨rfl, hlt⟩ := add?_eq_ok h
  rw [BitVec.toNat_add]; omega

依存

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