From e13fb4764c2b11e49d4987f90b32fde974183ab1 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <jhendrix@whoisjoe.info>
Date: Thu, 19 Oct 2023 23:46:31 -0700
Subject: [PATCH] chore: Make signExtend use output number of bits. (#308)

---
 Std/Data/BitVec/Basic.lean |  3 +--
 test/bitvec.lean           | 12 ++++++++++--
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/Std/Data/BitVec/Basic.lean b/Std/Data/BitVec/Basic.lean
index bf14f4c821..0106473294 100644
--- a/Std/Data/BitVec/Basic.lean
+++ b/Std/Data/BitVec/Basic.lean
@@ -416,5 +416,4 @@ bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
 
 SMT-Lib name: `sign_extend`.
 -/
-def signExtend (i : Nat) (x : BitVec w) : BitVec (w+i) :=
-  Nat.add_comm .. ▸ (fill i x.msb ++ x)
+def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
diff --git a/test/bitvec.lean b/test/bitvec.lean
index 023f6453f2..57cb0595bf 100644
--- a/test/bitvec.lean
+++ b/test/bitvec.lean
@@ -8,11 +8,19 @@ open Std.BitVec
 #guard 3#5 * 7#5 = 0x15#5
 #guard 3#4 * 7#4 = 0x05#4
 
--- Division and mod/rem
+#guard zeroExtend  4 0x7f#8 = 0xf#4
+#guard zeroExtend 12 0x7f#8 = 0x07f#12
+#guard zeroExtend 12 0x80#8 = 0x080#12
+#guard zeroExtend 16 0xff#8 = 0x00ff#16
 
+#guard signExtend  4 0x7f#8 = 0xf#4
+#guard signExtend 12 0x7f#8 = 0x07f#12
+#guard signExtend 12 0x80#8 = 0xf80#12
+#guard signExtend 16 0xff#8 = 0xffff#16
 
-#guard 3#4 / 0 = 0
+-- Division and mod/rem
 
+#guard 3#4 / 0 = 0
 #guard 10#4 / 2 = 5
 
 #guard 8#4 % 0 = 8