JPYC.add?_sub?_cancel
名称・種別
- 名称:
JPYC.add?_sub?_cancel - 種別: theorem
- モジュール:
JpycFormalVerification.Word - ソース:
JpycFormalVerification/Word.lean:90-98 - 概要: a+b が c で成功するなら c−b は a に戻る、という往復（借方→貸方）補題。
- 仕様: 対象
型シグネチャ
lean
∀ {a b c : JPYC.U256}, Eq (JPYC.add? a b) (Except.ok c) → Eq (JPYC.sub? c b) (Except.ok a)「a + b が結果 c として成功するなら、c - b は成功して a を返す」という定理です。足してから引けば元に戻る。
和訳 docstring
a + b が結果 c で成功するなら、c - b は成功して a を返す。API の完全性のために用意したもので、実際に下流（_transfer_self）で使われるのは双対の sub?_add?_cancel のほう。この向きは下流では使われていない。
解説
何を述べているか。 checked 加算と減算の round-trip（往復）相殺 です。
直感。 あふれずに足せたのなら、同じ量を引けば確実に元の値に戻る、ということです。
なぜ安全性に効くか。 checked 加減算の往復が成り立つことは、供給保存（足した分はちゃんと引いて回収できる）を扱う基盤です。証明は add?_eq_ok と sub?_of_le、BitVec.add_sub_cancel を組み合わせます。なお実際に下流（_transfer_self の証明内）で使われるのは双対の sub?_add?_cancel のほうで、この add?_sub?_cancel 自体は API 完全性（往復の両向きを揃える）のために置いてあり、現状の証明では直接は使われていません。
図解
Lean ソースコード
lean
/-- If `a + b` succeeds with result `c`, then `c - b` succeeds and returns `a`.
Provided for API completeness — the dual `sub?_add?_cancel` is the direction
actually used downstream (in `_transfer_self`); this one has no downstream use. -/
theorem add?_sub?_cancel {a b c : U256} (h : add? a b = .ok c) :
sub? c b = .ok a := by
obtain ⟨rfl, hlt⟩ := add?_eq_ok h
have hb : b.toNat < 2 ^ 256 := b.isLt
have hle : b.toNat ≤ (a + b).toNat := by rw [BitVec.toNat_add]; omega
rw [sub?_of_le hle, BitVec.add_sub_cancel]