Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is zero #5616

Merged
merged 1 commit into from
Nov 10, 2024
Merged

feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is zero #5616

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 32 additions & 0 deletions src/Init/Data/BitVec/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -512,6 +512,31 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
subst h
simp

@[simp]
theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w]

/-! ### slt -/

/--
A bitvector, when interpreted as an integer, is less than zero iff
its most significant bit is true.
-/
theorem slt_zero_iff_msb_cond (x : BitVec w) : x.slt 0#w ↔ x.msb = true := by
have := toInt_eq_msb_cond x
constructor
· intros h
apply Classical.byContradiction
intros hmsb
simp only [Bool.not_eq_true] at hmsb
simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this
simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h
omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/
· intros h
simp only [h, ↓reduceIte] at this
simp [BitVec.slt, this]
omega

/-! ### setWidth, zeroExtend and truncate -/

@[simp]
Expand Down Expand Up @@ -2376,6 +2401,9 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
simp [smtUDiv]

@[simp]
theorem smtUDiv_zero {x : BitVec n} : x.smtUDiv 0#n = allOnes n := rfl

/-! ### sdiv -/

/-- Equation theorem for `sdiv` in terms of `udiv`. -/
Expand Down Expand Up @@ -2443,6 +2471,10 @@ theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
rw [BitVec.smtSDiv]
rcases x.msb <;> rcases y.msb <;> simp

@[simp]
theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n) := by
rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond x, hx, ← negOne_eq_allOnes]

/-! ### srem -/

theorem srem_eq (x y : BitVec w) : srem x y =
Expand Down
Loading