JPYC.sub?_toNat

名称・種別

• 名称: JPYC.sub?_toNat
• 種別: theorem
• モジュール: JpycFormalVerification.Word
• ソース: JpycFormalVerification/Word.lean:72-78
• 概要: 成功した sub? は自然数減算と一致する、という補題。
• 仕様: 対象

型シグネチャ

∀ {a b r : JPYC.U256}, Eq (JPYC.sub? a b) (Except.ok r) → Eq (BitVec.toNat r) (instHSub.hSub (BitVec.toNat a) (BitVec.toNat b))

「sub? a b = .ok r ならば r.toNat = a.toNat - b.toNat」という定理です。成功時には、結果の自然数値が自然数の差に一致します。

和訳 docstring

成功した sub? は（切り捨てだが、ここでは正確な）自然数の減算と一致する。

解説

何を述べているか。 減算が成功したなら、結果の自然数値は自然数の差に一致する、という主張です。

直感。 b ≤ a が成り立つので、自然数の切り捨て減算（負にならないよう 0 で止まる引き算）も、ここでは正確な引き算と同じ結果になります。

なぜ安全性に効くか。 供給保存や残高計算で、ビット表現と自然数表現を橋渡しします。証明は sub?_eq_ok と BitVec.toNat_sub、omega を使います。

図解

Lean ソースコード

/-- A successful `sub?` agrees with (truncated, but here exact) natural-number
subtraction. -/
theorem sub?_toNat {a b r : U256} (h : sub? a b = .ok r) :
    r.toNat = a.toNat - b.toNat := by
  obtain ⟨rfl, hle⟩ := sub?_eq_ok h
  have ha : a.toNat < 2 ^ 256 := a.isLt
  rw [BitVec.toNat_sub]; omega

依存

• JPYC.Error
• JPYC.U256
• JPYC.sub?
• JPYC.sub?_eq_ok