JPYC.sub?_add?_cancel

名称・種別

• 名称: JPYC.sub?_add?_cancel
• 種別: theorem
• モジュール: JpycFormalVerification.Word
• ソース: JpycFormalVerification/Word.lean:96-102
• 概要: a−b が c で成功するなら c+b は a に戻る、という往復補題。
• 仕様: 対象

型シグネチャ

∀ {a b c : JPYC.U256}, Eq (JPYC.sub? a b) (Except.ok c) → Eq (JPYC.add? c b) (Except.ok a)

「a - b が結果 c として成功するなら、c + b は成功して a を返す」という定理です。引いてから足せば元に戻る。

和訳 docstring

a - b が結果 c で成功するなら、c + b は成功して a を返す。

解説

何を述べているか。 add?_sub?_cancel の逆向きの round-trip 相殺 です。

直感。 引けたのなら、同じ量を足して元に戻せ、しかもその足し算はあふれません（元の a に戻るだけだから）。

なぜ安全性に効くか。 残高を引いてから別口で戻す・合算する局面の保存性に使います。証明は sub?_eq_ok と add?_of_lt、BitVec.sub_add_cancel を組み合わせます。

図解

Lean ソースコード

/-- If `a - b` succeeds with result `c`, then `c + b` succeeds and returns `a`. -/
theorem sub?_add?_cancel {a b c : U256} (h : sub? a b = .ok c) :
    add? c b = .ok a := by
  obtain ⟨rfl, hle⟩ := sub?_eq_ok h
  have ha : a.toNat < 2 ^ 256 := a.isLt
  have hlt : (a - b).toNat + b.toNat < 2 ^ 256 := by rw [BitVec.toNat_sub]; omega
  rw [add?_of_lt hlt, BitVec.sub_add_cancel]

依存

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