JPYC.sub?_eq_ok

名称・種別

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

型シグネチャ

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

「sub? a b = .ok r ならば、r = a - b かつ b ≤ a」という定理です。成功という結果から内訳を取り出します。

解説

何を述べているか。 sub? が成功したとき、結果 r が差に等しく、かつ b ≤ a（引けた）であったことを取り出す 除去補題 です。

直感。「成功した」事実から逆に「引けた・結果は差」を読み出します。証明は sub? を展開して場合分けするだけです。

なぜ安全性に効くか。「残高から value を引けた」という仮定から「value ≤ 残高」を導く、アンダーフロー無し（No underflow） 性の中核部品です。sub?_toNat もこれを経由します。

図解

Lean ソースコード

theorem sub?_eq_ok {a b r : U256} (h : sub? a b = .ok r) :
    r = a - b ∧ b.toNat ≤ a.toNat := by
  unfold sub? at h; split at h <;> simp_all

依存

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