From 623f6266a62bd92516331ec8d88ccb49f2cafddc Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Fri, 25 Oct 2024 14:17:33 -0700 Subject: [PATCH] feat: BitVec.toNat (BitVec.signExtend) This PR adds toNat theorems for BitVec.signExtend. Sign extending to a larger bitwidth depends on the msb. If the msb is false, then the result equals the original value. If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the sign extension. ```lean theorem toNat_signExtend (x : BitVec w) {v : Nat} : (x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0 ``` Co-authored-by: Siddharth Bhat Co-authored-by: Harun Khan --- src/Init/Data/BitVec/Lemmas.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 5c931f353c4f..d7d78ee9bc0d 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1622,14 +1622,16 @@ theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by /-- Sign extending to a larger bitwidth depends on the msb. If the msb is false, then the result equals the original value. If the msb is true, then we add a value of `(2^v - 2^w)`, which arises from the sign extension. -/ -theorem toNat_signExtend_of_le (x : BitVec w) {v : Nat} (hv : w ≤ v) : +private theorem toNat_signExtend_of_le (x : BitVec w) {v : Nat} (hv : w ≤ v) : (x.signExtend v).toNat = x.toNat + if x.msb then 2^v - 2^w else 0 := by apply Nat.eq_of_testBit_eq intro i have ⟨k, hk⟩ := Nat.exists_eq_add_of_le hv rw [hk, testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one, Nat.add_comm (x.toNat)] by_cases hx : x.msb - · simp [hx, Nat.testBit_mul_pow_two_add _ x.isLt, testBit_toNat] + · simp only [hx, Bool.if_true_right, ↓reduceIte, + Nat.testBit_mul_pow_two_add _ x.isLt, + testBit_toNat, Nat.testBit_two_pow_sub_one] -- Case analysis on i being in the intervals [0..w), [w..w + k), [w+k..∞) have hi : i < w ∨ (w ≤ i ∧ i < w + k) ∨ w + k ≤ i := by omega rcases hi with hi | hi | hi @@ -1637,7 +1639,8 @@ theorem toNat_signExtend_of_le (x : BitVec w) {v : Nat} (hv : w ≤ v) : · simp [hi]; omega · simp [hi, show ¬ (i < w + k) by omega, show ¬ (i < w) by omega] omega - · simp [hx, Nat.testBit_mul_pow_two_add _ x.isLt, testBit_toNat] + · simp only [hx, Bool.if_false_right, + Bool.false_eq_true, ↓reduceIte, Nat.zero_add, testBit_toNat] have hi : i < w ∨ (w ≤ i ∧ i < w + k) ∨ w + k ≤ i := by omega rcases hi with hi | hi | hi · simp [hi]; omega