From da9a536ffda2e035f19cdcc61a5a21378a632753 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Thu, 19 Jun 2025 10:08:04 +0100 Subject: [PATCH] feat: BitVec.msb_sdiv (#8178) This PR provides a compact formula for the MSB of the sdiv. Most of the work in the PR involves handling the corner cases of division overflowing (e.g. `intMin / -1 = intMin`) --------- Co-authored-by: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Bitblast.lean | 82 ++++++++++++++++++++++++++++++ src/Init/Data/BitVec/Lemmas.lean | 10 ++++ 2 files changed, 92 insertions(+) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 5b9b7eae62..535815a96e 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1662,6 +1662,88 @@ theorem toInt_sdiv (a b : BitVec w) : (a.sdiv b).toInt = (a.toInt.tdiv b.toInt). · rw [← toInt_bmod_cancel] rw [BitVec.toInt_sdiv_of_ne_or_ne _ _ (by simpa only [Decidable.not_and_iff_not_or_not] using h)] +private theorem neg_udiv_eq_intMin_iff_eq_intMin_eq_one_of_msb_eq_true + {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = false) : + -x / y = intMin w ↔ (x = intMin w ∧ y = 1#w) := by + constructor + · intros h + rcases w with _ | w; decide +revert + have : (-x / y).msb = true := by simp [h, msb_intMin] + rw [msb_udiv] at this + simp only [bool_to_prop] at this + obtain ⟨hx, hy⟩ := this + simp only [beq_iff_eq] at hy + subst hy + simp only [udiv_one, zero_lt_succ, neg_eq_intMin] at h + simp [h] + · rintro ⟨hx, hy⟩ + subst hx hy + simp + +/-- +the most significant bit of the signed division `x.sdiv y` can be computed +by the following cases: +(1) x nonneg, y nonneg: never neg. +(2) x nonneg, y neg: neg when result nonzero. + We know that y is nonzero since it is negative, so we only check `|x| ≥ |y|`. +(3) x neg, y nonneg: neg when result nonzero. + We check that `y ≠ 0` and `|x| ≥ |y|`. +(4) x neg, y neg: neg when `x = intMin, `y = -1`, since `intMin / -1 = intMin`. + +The proof strategy is to perform a case analysis on the sign of `x` and `y`, +followed by unfolding the `sdiv` into `udiv`. +-/ +theorem msb_sdiv_eq_decide {x y : BitVec w} : + (x.sdiv y).msb = (decide (0 < w) && + (!x.msb && y.msb && decide (-y ≤ x)) || + (x.msb && !y.msb && decide (y ≤ -x) && !decide (y = 0#w)) || + (x.msb && y.msb && decide (x = intMin w) && decide (y = -1#w))) + := by + rcases w; decide +revert + case succ w => + simp only [decide_true, ne_eq, decide_and, decide_not, Bool.true_and, + sdiv_eq, udiv_eq] + rcases hxmsb : x.msb <;> rcases hymsb : y.msb + · simp [hxmsb, hymsb, msb_udiv_eq_false_of, Bool.not_false, Bool.and_false, Bool.false_and, + Bool.and_true, Bool.or_self, Bool.and_self] + · simp only [hxmsb, hymsb, msb_neg, msb_udiv_eq_false_of, bne_false, Bool.not_false, + Bool.and_self, ne_zero_of_msb_true, decide_false, Bool.and_true, Bool.true_and, Bool.not_true, + Bool.false_and, Bool.or_false, bool_to_prop] + have : x / -y ≠ intMin (w + 1) := by + intros h + have : (x / -y).msb = (intMin (w + 1)).msb := by simp only [h] + simp only [msb_udiv, msb_intMin, show 0 < w + 1 by omega, decide_true, and_eq_true, beq_iff_eq] at this + obtain ⟨hcontra, _⟩ := this + simp only [hcontra, true_eq_false] at hxmsb + simp [this, hymsb, udiv_ne_zero_iff_ne_zero_and_le] + · simp only [hxmsb, hymsb, Bool.not_true, Bool.and_self, Bool.false_and, Bool.not_false, + Bool.true_and, Bool.false_or, Bool.and_false, Bool.or_false] + by_cases hx₁ : x = 0#(w + 1) + · simp [hx₁, neg_zero, zero_udiv, msb_zero, le_zero_iff, Bool.and_not_self] + · by_cases hy₁ : y = 0#(w + 1) + · simp [hy₁, udiv_zero, neg_zero, msb_zero, decide_true, Bool.not_true, Bool.and_false] + · simp only [hy₁, decide_false, Bool.not_false, Bool.and_true] + by_cases hxy₁ : (- x / y) = 0#(w + 1) + · simp only [hxy₁, neg_zero, msb_zero, false_eq_decide_iff, BitVec.not_le, + decide_eq_true_eq, BitVec.not_le] + simp only [udiv_eq_zero_iff_eq_zero_or_lt, hy₁, _root_.false_or] at hxy₁ + bv_omega + · simp only [udiv_eq_zero_iff_eq_zero_or_lt, _root_.not_or, BitVec.not_lt, + hy₁, not_false_eq_true, _root_.true_and] at hxy₁ + simp only [hxy₁, decide_true, msb_neg, bne_iff_ne, ne_eq, + bool_to_prop, + bne_iff_ne, ne_eq, udiv_eq_zero_iff_eq_zero_or_lt, hy₁, _root_.false_or, + BitVec.not_lt, hxy₁, _root_.true_and, decide_not, not_eq_eq_eq_not, not_eq_not, + msb_udiv, msb_neg] + simp only [hx₁, not_false_eq_true, _root_.true_and, decide_not, hxmsb, not_eq_eq_eq_not, + Bool.not_true, decide_eq_false_iff_not, Decidable.not_not, beq_iff_eq] + rw [neg_udiv_eq_intMin_iff_eq_intMin_eq_one_of_msb_eq_true hxmsb hymsb] + · simp only [msb_udiv, msb_neg, hxmsb, bne_true, Bool.not_and, Bool.not_true, Bool.and_true, + Bool.false_and, Bool.and_false, hymsb, ne_zero_of_msb_true, decide_false, Bool.not_false, + Bool.or_self, Bool.and_self, Bool.true_and, Bool.false_or] + simp only [bool_to_prop] + simp [BitVec.ne_zero_of_msb_true (x := x) hxmsb, neg_eq_iff_eq_neg] + theorem msb_umod_eq_false_of_left {x : BitVec w} (hx : x.msb = false) (y : BitVec w) : (x % y).msb = false := by rw [msb_eq_false_iff_two_mul_lt] at hx ⊢ rw [toNat_umod] diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index c1a8a54c4e..93ab0f3c80 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -4119,6 +4119,16 @@ theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) : (x / y).toInt = x.toNat / y.toNat := by simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h] +/-- Unsigned division is zero if and only if either the denominator is zero, +or the numerator is unsigned less than the denominator -/ +theorem udiv_eq_zero_iff_eq_zero_or_lt {x y : BitVec w} : + x / y = 0#w ↔ (y = 0#w ∨ x < y) := by + simp [toNat_eq, toNat_udiv, toNat_ofNat, Nat.zero_mod, Nat.div_eq_zero_iff, BitVec.lt_def] + +theorem udiv_ne_zero_iff_ne_zero_and_le {x y : BitVec w} : + ¬ (x / y = 0#w) ↔ (y ≠ 0#w ∧ y ≤ x) := by + simp only [ne_eq, udiv_eq_zero_iff_eq_zero_or_lt, _root_.not_or, BitVec.not_lt] + /-! ### umod -/ theorem umod_def {x y : BitVec n} :