From 67d5319a0a8af3d5435660ac9d7c3510f51ca416 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 20 Sep 2024 10:53:19 -0500 Subject: [PATCH] feat: BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning These theorems are useful when one wants to simplify the goal state, under knowledge that the bitvector operations don't overflow. This can produce much smaller goal states that eventually allows `bv_omega` to quickly close the goal. A problem is that these theorems are *not* in `simp` normal form, since e.g. `(x + y).toNat` is normalized to `(x.toNat + y.toNat) % 2^w`. It's not immediately clear to me what should be done. --- src/Init/Data/BitVec/Lemmas.lean | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 54355070f1f3..6aa78159c076 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2113,6 +2113,11 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := /-! ### Non-overflow theorems -/ +/-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow. -/ +theorem toNat_add_of_lt {w} {x y : BitVec w} (h : x.toNat + y.toNat < 2^w) : + (x + y).toNat = x.toNat + y.toNat := by + rw [BitVec.toNat_add, Nat.mod_eq_of_lt h] + /-- If `y ≤ x`, then the subtraction `(x - y)` does not overflow. Thus, `(x - y).toNat = x.toNat - y.toNat` @@ -2126,6 +2131,24 @@ theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) : · have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)] +/-- +If `y > x`, then the subtraction `(x - y)` *does* overflow, and the result is the wraparound. +Thus, `(x - y).toNat = 2^w - (y.toNat - x.toNat)`. +-/ +theorem toNat_sub_of_lt {x y : BitVec w} (h : x < y) : + (x - y).toNat = 2^w - (y.toNat - x.toNat) := by + simp only [toNat_sub] + rw [Nat.mod_eq_of_lt (by bv_omega)] + bv_omega + +/-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow. +Thus, `(x * y).toNat = x.toNat * y.toNat`. +-/ +theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) : + (x * y).toNat = x.toNat * y.toNat := by + rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h] + + /-! ### Deprecations -/ set_option linter.missingDocs false