diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 83fc4ef748..2e011aa386 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1385,6 +1385,7 @@ gen_injective_theorems% Except
 gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
+gen_injective_theorems% BitVec
 
 theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
   fun x => Nat.noConfusion x id
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index fc0812eee9..d676503692 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -7,7 +7,7 @@ prelude
 import Init.WFTactics
 import Init.Data.Nat.Basic
 import Init.Data.Fin.Basic
-import Init.Data.UInt.Basic
+import Init.Data.UInt.BasicAux
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 432db5296a..3d4b311d12 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -8,12 +8,13 @@ import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 import Init.Data.Int.Bitwise
+import Init.Data.BitVec.BasicAux
 
 /-!
-We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
-(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
-with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
-representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
+We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over
+others for its relative efficiency (Lean has special support for `Nat`),  and the fact that bitwise
+operations on `Fin` are already defined. Some other possible representations are `List Bool`,
+`{ l : List Bool // l.length = w }`, `Fin w → Bool`.
 
 We define many of the bitvector operations from the
 [`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
@@ -22,60 +23,12 @@ of SMT-LIBv2.
 
 set_option linter.missingDocs true
 
-/--
-A bitvector of the specified width.
-
-This is represented as the underlying `Nat` number in both the runtime
-and the kernel, inheriting all the special support for `Nat`.
--/
-structure BitVec (w : Nat) where
-  /-- Construct a `BitVec w` from a number less than `2^w`.
-  O(1), because we use `Fin` as the internal representation of a bitvector. -/
-  ofFin ::
-  /-- Interpret a bitvector as a number less than `2^w`.
-  O(1), because we use `Fin` as the internal representation of a bitvector. -/
-  toFin : Fin (2^w)
-
-/--
-Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
--/
--- We manually derive the `DecidableEq` instances for `BitVec` because
--- we want to have builtin support for bit-vector literals, and we
--- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
-def BitVec.decEq (x y : BitVec n) : Decidable (x = y) :=
-  match x, y with
-  | ⟨n⟩, ⟨m⟩ =>
-    if h : n = m then
-      isTrue (h ▸ rfl)
-    else
-      isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h))
-
-instance : DecidableEq (BitVec n) := BitVec.decEq
-
 namespace BitVec
 
 section Nat
 
-/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
-@[match_pattern]
-protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2^n) : BitVec n where
-  toFin := ⟨i, p⟩
-
-/-- The `BitVec` with value `i mod 2^n`. -/
-@[match_pattern]
-protected def ofNat (n : Nat) (i : Nat) : BitVec n where
-  toFin := Fin.ofNat' (2^n) i
-
-instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
-/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
-(zero-cost) wrapper around a `Nat`. -/
-protected def toNat (x : BitVec n) : Nat := x.toFin.val
-
-/-- Return the bound in terms of toNat. -/
-theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
-
 @[deprecated isLt (since := "2024-03-12")]
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
 
@@ -238,22 +191,6 @@ end repr_toString
 
 section arithmetic
 
-/--
-Addition for bit vectors. This can be interpreted as either signed or unsigned addition
-modulo `2^n`.
-
-SMT-Lib name: `bvadd`.
--/
-protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
-instance : Add (BitVec n) := ⟨BitVec.add⟩
-
-/--
-Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
-modulo `2^n`.
--/
-protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
-instance : Sub (BitVec n) := ⟨BitVec.sub⟩
-
 /--
 Negation for bit vectors. This can be interpreted as either signed or unsigned negation
 modulo `2^n`.
@@ -387,10 +324,6 @@ SMT-Lib name: `bvult`.
 -/
 protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat
 
-instance : LT (BitVec n) where lt := (·.toNat < ·.toNat)
-instance (x y : BitVec n) : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.toNat < y.toNat))
-
 /--
 Unsigned less-than-or-equal-to for bit vectors.
 
@@ -398,10 +331,6 @@ SMT-Lib name: `bvule`.
 -/
 protected def ule (x y : BitVec n) : Bool := x.toNat ≤ y.toNat
 
-instance : LE (BitVec n) where le := (·.toNat ≤ ·.toNat)
-instance (x y : BitVec n) : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.toNat ≤ y.toNat))
-
 /--
 Signed less-than for bit vectors.
 
diff --git a/src/Init/Data/BitVec/BasicAux.lean b/src/Init/Data/BitVec/BasicAux.lean
new file mode 100644
index 0000000000..6e6eccc157
--- /dev/null
+++ b/src/Init/Data/BitVec/BasicAux.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed
+-/
+prelude
+import Init.Data.Fin.Basic
+
+set_option linter.missingDocs true
+
+/-!
+This module exists to provide the very basic `BitVec` definitions required for
+`Init.Data.UInt.BasicAux`.
+-/
+
+namespace BitVec
+
+section Nat
+
+/-- The `BitVec` with value `i mod 2^n`. -/
+@[match_pattern]
+protected def ofNat (n : Nat) (i : Nat) : BitVec n where
+  toFin := Fin.ofNat' (2^n) i
+
+instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
+
+/-- Return the bound in terms of toNat. -/
+theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
+
+end Nat
+
+section arithmetic
+
+/--
+Addition for bit vectors. This can be interpreted as either signed or unsigned addition
+modulo `2^n`.
+
+SMT-Lib name: `bvadd`.
+-/
+protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
+instance : Add (BitVec n) := ⟨BitVec.add⟩
+
+/--
+Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
+modulo `2^n`.
+-/
+protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
+instance : Sub (BitVec n) := ⟨BitVec.sub⟩
+
+end arithmetic
+
+end BitVec
diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean
index 930141907a..93f997f9ef 100644
--- a/src/Init/Data/Char/Basic.lean
+++ b/src/Init/Data/Char/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Data.UInt.Basic
+import Init.Data.UInt.BasicAux
 
 /-- Determines if the given integer is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).
 
@@ -42,8 +42,10 @@ theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
 
 theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
   match h with
-  | Or.inl h        => Or.inl h
-  | Or.inr ⟨h₁, h₂⟩ => Or.inr ⟨h₁, h₂⟩
+  | Or.inl h =>
+    Or.inl (UInt32.ofNat'_lt_of_lt _ (by decide) h)
+  | Or.inr ⟨h₁, h₂⟩ =>
+    Or.inr ⟨UInt32.lt_ofNat'_of_lt _ (by decide) h₁, UInt32.ofNat'_lt_of_lt _ (by decide) h₂⟩
 
 theorem isValidChar_zero : isValidChar 0 :=
   Or.inl (by decide)
@@ -57,7 +59,7 @@ theorem isValidChar_zero : isValidChar 0 :=
   c.val.toUInt8
 
 /-- The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other. -/
-def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.1.2 (by decide))⟩
+def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.toBitVec.isLt (by decide))⟩
 
 instance : Inhabited Char where
   default := 'A'
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index b0f40b7e07..cc2aa0c9e5 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -796,6 +796,8 @@ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
   | zero => cases h
   | succ n => simp [Nat.pow_succ]
 
+protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+
 instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
   ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pos_pow_of_pos m (pos_of_neZero _))⟩
 
diff --git a/src/Init/Data/Nat/Power2.lean b/src/Init/Data/Nat/Power2.lean
index 287e4dfdbf..46b1b29599 100644
--- a/src/Init/Data/Nat/Power2.lean
+++ b/src/Init/Data/Nat/Power2.lean
@@ -8,8 +8,6 @@ import Init.Data.Nat.Linear
 
 namespace Nat
 
-protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
-
 theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
   have : power * 2 = power + power := by simp_arith
   rw [this, Nat.sub_add_eq]
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index c1f7e522df..9b363da289 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -7,7 +7,7 @@ prelude
 import Init.Data.Format.Basic
 import Init.Data.Int.Basic
 import Init.Data.Nat.Div
-import Init.Data.UInt.Basic
+import Init.Data.UInt.BasicAux
 import Init.Control.Id
 open Sum Subtype Nat
 
diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index 696482fb17..406639dbd0 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.ByteArray
+import Init.Data.UInt.Lemmas
 
 namespace String
 
@@ -20,14 +21,14 @@ def toNat! (s : String) : Nat :=
 def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
   let c ← a[i]?
   if c &&& 0x80 == 0 then
-    some ⟨c.toUInt32, .inl (Nat.lt_trans c.1.2 (by decide))⟩
+    some ⟨c.toUInt32, .inl (Nat.lt_trans c.toBitVec.isLt (by decide))⟩
   else if c &&& 0xe0 == 0xc0 then
     let c1 ← a[i+1]?
     guard (c1 &&& 0xc0 == 0x80)
     let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32
     guard (0x80 ≤ r)
     -- TODO: Prove h from the definition of r once we have the necessary lemmas
-    if h : r < 0xd800 then some ⟨r, .inl h⟩ else none
+    if h : r < 0xd800 then some ⟨r, .inl (UInt32.toNat_lt_of_lt (by decide) h)⟩ else none
   else if c &&& 0xf0 == 0xe0 then
     let c1 ← a[i+1]?
     let c2 ← a[i+2]?
@@ -38,7 +39,14 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
       (c2 &&& 0x3f).toUInt32
     guard (0x800 ≤ r)
     -- TODO: Prove `r < 0x110000` from the definition of r once we have the necessary lemmas
-    if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then some ⟨r, h⟩ else none
+    if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then
+      have :=
+        match h with
+        | .inl h => Or.inl (UInt32.toNat_lt_of_lt (by decide) h)
+        | .inr h => Or.inr ⟨UInt32.lt_toNat_of_lt (by decide) h.left, UInt32.toNat_lt_of_lt (by decide) h.right⟩
+      some ⟨r, this⟩
+    else
+      none
   else if c &&& 0xf8 == 0xf0 then
     let c1 ← a[i+1]?
     let c2 ← a[i+2]?
@@ -50,7 +58,7 @@ def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
       ((c2 &&& 0x3f).toUInt32 <<< 6) |||
       (c3 &&& 0x3f).toUInt32
     if h : 0x10000 ≤ r ∧ r < 0x110000 then
-      some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) h.1, h.2⟩⟩
+      some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) (UInt32.le_toNat_of_le (by decide) h.left), UInt32.toNat_lt_of_lt (by decide) h.right⟩⟩
     else none
   else
     none
diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean
index 97cb28c8f3..06b3d85ff0 100644
--- a/src/Init/Data/ToString/Basic.lean
+++ b/src/Init/Data/ToString/Basic.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.String.Basic
-import Init.Data.UInt.Basic
+import Init.Data.UInt.BasicAux
 import Init.Data.Nat.Div
 import Init.Data.Repr
 import Init.Data.Int.Basic
diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean
index 1eb20a30e7..ed99636dba 100644
--- a/src/Init/Data/UInt.lean
+++ b/src/Init/Data/UInt.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
+import Init.Data.UInt.BasicAux
 import Init.Data.UInt.Basic
 import Init.Data.UInt.Log2
 import Init.Data.UInt.Lemmas
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index 99ab03cf11..c0e94d9639 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -4,52 +4,50 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.Fin.Basic
+import Init.Data.UInt.BasicAux
+import Init.Data.BitVec.Basic
 
 open Nat
 
-@[extern "lean_uint8_of_nat"]
-def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨Fin.ofNat n⟩
-abbrev Nat.toUInt8 := UInt8.ofNat
-@[extern "lean_uint8_to_nat"]
-def UInt8.toNat (n : UInt8) : Nat := n.val.val
 @[extern "lean_uint8_add"]
-def UInt8.add (a b : UInt8) : UInt8 := ⟨a.val + b.val⟩
+def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint8_sub"]
-def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.val - b.val⟩
+def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.toBitVec - b.toBitVec⟩
 @[extern "lean_uint8_mul"]
-def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.val * b.val⟩
+def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_uint8_div"]
-def UInt8.div (a b : UInt8) : UInt8 := ⟨a.val / b.val⟩
+def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint8_mod"]
-def UInt8.mod (a b : UInt8) : UInt8 := ⟨a.val % b.val⟩
-@[extern "lean_uint8_modn"]
+def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+@[extern "lean_uint8_modn", deprecated UInt8.mod (since := "2024-09-23")]
 def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint8_land"]
-def UInt8.land (a b : UInt8) : UInt8 := ⟨Fin.land a.val b.val⟩
+def UInt8.land (a b : UInt8) : UInt8 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint8_lor"]
-def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
+def UInt8.lor (a b : UInt8) : UInt8 := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_uint8_xor"]
-def UInt8.xor (a b : UInt8) : UInt8 := ⟨Fin.xor a.val b.val⟩
+def UInt8.xor (a b : UInt8) : UInt8 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_uint8_shift_left"]
-def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.val <<< (modn b 8).val⟩
+def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.toBitVec <<< (mod b 8).toBitVec⟩
 @[extern "lean_uint8_shift_right"]
-def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
-def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
-def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
+def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.toBitVec >>> (mod b 8).toBitVec⟩
+def UInt8.lt (a b : UInt8) : Prop := a.toBitVec < b.toBitVec
+def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
 
-instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
 instance : Mod UInt8       := ⟨UInt8.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod UInt8 Nat UInt8 := ⟨UInt8.modn⟩
+
 instance : Div UInt8       := ⟨UInt8.div⟩
 instance : LT UInt8        := ⟨UInt8.lt⟩
 instance : LE UInt8        := ⟨UInt8.le⟩
 
 @[extern "lean_uint8_complement"]
-def UInt8.complement (a:UInt8) : UInt8 := 0-(a+1)
+def UInt8.complement (a : UInt8) : UInt8 := ⟨~~~a.toBitVec⟩
 
 instance : Complement UInt8 := ⟨UInt8.complement⟩
 instance : AndOp UInt8     := ⟨UInt8.land⟩
@@ -58,69 +56,58 @@ instance : Xor UInt8       := ⟨UInt8.xor⟩
 instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
+  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint8_dec_le"]
 def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
+  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
 instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
 instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
 instance : Max UInt8 := maxOfLe
 instance : Min UInt8 := minOfLe
 
-@[extern "lean_uint16_of_nat"]
-def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
-abbrev Nat.toUInt16 := UInt16.ofNat
-@[extern "lean_uint16_to_nat"]
-def UInt16.toNat (n : UInt16) : Nat := n.val.val
 @[extern "lean_uint16_add"]
-def UInt16.add (a b : UInt16) : UInt16 := ⟨a.val + b.val⟩
+def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint16_sub"]
-def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.val - b.val⟩
+def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.toBitVec - b.toBitVec⟩
 @[extern "lean_uint16_mul"]
-def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.val * b.val⟩
+def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_uint16_div"]
-def UInt16.div (a b : UInt16) : UInt16 := ⟨a.val / b.val⟩
+def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint16_mod"]
-def UInt16.mod (a b : UInt16) : UInt16 := ⟨a.val % b.val⟩
-@[extern "lean_uint16_modn"]
+def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+@[extern "lean_uint16_modn", deprecated UInt16.mod (since := "2024-09-23")]
 def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint16_land"]
-def UInt16.land (a b : UInt16) : UInt16 := ⟨Fin.land a.val b.val⟩
+def UInt16.land (a b : UInt16) : UInt16 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint16_lor"]
-def UInt16.lor (a b : UInt16) : UInt16 := ⟨Fin.lor a.val b.val⟩
+def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_uint16_xor"]
-def UInt16.xor (a b : UInt16) : UInt16 := ⟨Fin.xor a.val b.val⟩
+def UInt16.xor (a b : UInt16) : UInt16 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_uint16_shift_left"]
-def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.val <<< (modn b 16).val⟩
-@[extern "lean_uint16_to_uint8"]
-def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint8_to_uint16"]
-def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.toBitVec <<< (mod b 16).toBitVec⟩
 @[extern "lean_uint16_shift_right"]
-def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
-def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
-def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
+def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.toBitVec >>> (mod b 16).toBitVec⟩
+def UInt16.lt (a b : UInt16) : Prop := a.toBitVec < b.toBitVec
+def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
 
-instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
 instance : Mod UInt16       := ⟨UInt16.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod UInt16 Nat UInt16 := ⟨UInt16.modn⟩
+
 instance : Div UInt16       := ⟨UInt16.div⟩
 instance : LT UInt16        := ⟨UInt16.lt⟩
 instance : LE UInt16        := ⟨UInt16.le⟩
 
 @[extern "lean_uint16_complement"]
-def UInt16.complement (a:UInt16) : UInt16 := 0-(a+1)
+def UInt16.complement (a : UInt16) : UInt16 := ⟨~~~a.toBitVec⟩
 
 instance : Complement UInt16 := ⟨UInt16.complement⟩
 instance : AndOp UInt16     := ⟨UInt16.land⟩
@@ -132,74 +119,53 @@ instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
+  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_le"]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
+  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
 instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
 instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
 instance : Max UInt16 := maxOfLe
 instance : Min UInt16 := minOfLe
 
-@[extern "lean_uint32_of_nat"]
-def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
-@[extern "lean_uint32_of_nat"]
-def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩
-/--
-Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
--/
-def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
-  if h : n < UInt32.size then
-    UInt32.ofNat' n h
-  else
-    UInt32.ofNat' (UInt32.size - 1) (by decide)
-abbrev Nat.toUInt32 := UInt32.ofNat
 @[extern "lean_uint32_add"]
-def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩
+def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint32_sub"]
-def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.val - b.val⟩
+def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.toBitVec - b.toBitVec⟩
 @[extern "lean_uint32_mul"]
-def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.val * b.val⟩
+def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_uint32_div"]
-def UInt32.div (a b : UInt32) : UInt32 := ⟨a.val / b.val⟩
+def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint32_mod"]
-def UInt32.mod (a b : UInt32) : UInt32 := ⟨a.val % b.val⟩
-@[extern "lean_uint32_modn"]
+def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+@[extern "lean_uint32_modn", deprecated UInt32.mod (since := "2024-09-23")]
 def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint32_land"]
-def UInt32.land (a b : UInt32) : UInt32 := ⟨Fin.land a.val b.val⟩
+def UInt32.land (a b : UInt32) : UInt32 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint32_lor"]
-def UInt32.lor (a b : UInt32) : UInt32 := ⟨Fin.lor a.val b.val⟩
+def UInt32.lor (a b : UInt32) : UInt32 := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_uint32_xor"]
-def UInt32.xor (a b : UInt32) : UInt32 := ⟨Fin.xor a.val b.val⟩
+def UInt32.xor (a b : UInt32) : UInt32 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_uint32_shift_left"]
-def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.val <<< (modn b 32).val⟩
+def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.toBitVec <<< (mod b 32).toBitVec⟩
 @[extern "lean_uint32_shift_right"]
-def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.val >>> (modn b 32).val⟩
-@[extern "lean_uint32_to_uint8"]
-def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint32_to_uint16"]
-def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
-@[extern "lean_uint8_to_uint32"]
-def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
-@[extern "lean_uint16_to_uint32"]
-def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (mod b 32).toBitVec⟩
 
-instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
 instance : Mod UInt32       := ⟨UInt32.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
+
 instance : Div UInt32       := ⟨UInt32.div⟩
 
 @[extern "lean_uint32_complement"]
-def UInt32.complement (a:UInt32) : UInt32 := 0-(a+1)
+def UInt32.complement (a : UInt32) : UInt32 := ⟨~~~a.toBitVec⟩
 
 instance : Complement UInt32 := ⟨UInt32.complement⟩
 instance : AndOp UInt32     := ⟨UInt32.land⟩
@@ -208,60 +174,45 @@ instance : Xor UInt32       := ⟨UInt32.xor⟩
 instance : ShiftLeft UInt32  := ⟨UInt32.shiftLeft⟩
 instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 
-@[extern "lean_uint64_of_nat"]
-def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
-abbrev Nat.toUInt64 := UInt64.ofNat
-@[extern "lean_uint64_to_nat"]
-def UInt64.toNat (n : UInt64) : Nat := n.val.val
 @[extern "lean_uint64_add"]
-def UInt64.add (a b : UInt64) : UInt64 := ⟨a.val + b.val⟩
+def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint64_sub"]
-def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.val - b.val⟩
+def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.toBitVec - b.toBitVec⟩
 @[extern "lean_uint64_mul"]
-def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.val * b.val⟩
+def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_uint64_div"]
-def UInt64.div (a b : UInt64) : UInt64 := ⟨a.val / b.val⟩
+def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 @[extern "lean_uint64_mod"]
-def UInt64.mod (a b : UInt64) : UInt64 := ⟨a.val % b.val⟩
-@[extern "lean_uint64_modn"]
+def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+@[extern "lean_uint64_modn", deprecated UInt64.mod (since := "2024-09-23")]
 def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨Fin.modn a.val n⟩
 @[extern "lean_uint64_land"]
-def UInt64.land (a b : UInt64) : UInt64 := ⟨Fin.land a.val b.val⟩
+def UInt64.land (a b : UInt64) : UInt64 := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_uint64_lor"]
-def UInt64.lor (a b : UInt64) : UInt64 := ⟨Fin.lor a.val b.val⟩
+def UInt64.lor (a b : UInt64) : UInt64 := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_uint64_xor"]
-def UInt64.xor (a b : UInt64) : UInt64 := ⟨Fin.xor a.val b.val⟩
+def UInt64.xor (a b : UInt64) : UInt64 := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_uint64_shift_left"]
-def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.val <<< (modn b 64).val⟩
+def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.toBitVec <<< (mod b 64).toBitVec⟩
 @[extern "lean_uint64_shift_right"]
-def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.val >>> (modn b 64).val⟩
-def UInt64.lt (a b : UInt64) : Prop := a.val < b.val
-def UInt64.le (a b : UInt64) : Prop := a.val ≤ b.val
-@[extern "lean_uint64_to_uint8"]
-def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
-@[extern "lean_uint64_to_uint16"]
-def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
-@[extern "lean_uint64_to_uint32"]
-def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
-@[extern "lean_uint8_to_uint64"]
-def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
-@[extern "lean_uint16_to_uint64"]
-def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
-@[extern "lean_uint32_to_uint64"]
-def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨a.val, Nat.lt_trans a.1.2 (by decide)⟩
+def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.toBitVec >>> (mod b 64).toBitVec⟩
+def UInt64.lt (a b : UInt64) : Prop := a.toBitVec < b.toBitVec
+def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
 
-instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
 instance : Mod UInt64       := ⟨UInt64.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod UInt64 Nat UInt64 := ⟨UInt64.modn⟩
+
 instance : Div UInt64       := ⟨UInt64.div⟩
 instance : LT UInt64        := ⟨UInt64.lt⟩
 instance : LE UInt64        := ⟨UInt64.le⟩
 
 @[extern "lean_uint64_complement"]
-def UInt64.complement (a:UInt64) : UInt64 := 0-(a+1)
+def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
 
 instance : Complement UInt64 := ⟨UInt64.complement⟩
 instance : AndOp UInt64     := ⟨UInt64.land⟩
@@ -273,79 +224,52 @@ instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩
 @[extern "lean_bool_to_uint64"]
 def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint64_dec_lt"]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
+  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint64_dec_le"]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
+  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
 instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
 instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 
--- This instance would interfere with the global instance `NeZero (n + 1)`,
--- so we only enable it locally.
-@[local instance]
-private def instNeZeroUSizeSize : NeZero USize.size := ⟨add_one_ne_zero _⟩
-
-@[deprecated (since := "2024-09-16")]
-theorem usize_size_gt_zero : USize.size > 0 :=
-  Nat.zero_lt_succ ..
-
-@[extern "lean_usize_of_nat"]
-def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat'  _ n⟩
-abbrev Nat.toUSize := USize.ofNat
-@[extern "lean_usize_to_nat"]
-def USize.toNat (n : USize) : Nat := n.val.val
-@[extern "lean_usize_add"]
-def USize.add (a b : USize) : USize := ⟨a.val + b.val⟩
-@[extern "lean_usize_sub"]
-def USize.sub (a b : USize) : USize := ⟨a.val - b.val⟩
 @[extern "lean_usize_mul"]
-def USize.mul (a b : USize) : USize := ⟨a.val * b.val⟩
+def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
 @[extern "lean_usize_div"]
-def USize.div (a b : USize) : USize := ⟨a.val / b.val⟩
+def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
 @[extern "lean_usize_mod"]
-def USize.mod (a b : USize) : USize := ⟨a.val % b.val⟩
-@[extern "lean_usize_modn"]
+def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
+@[extern "lean_usize_modn", deprecated USize.mod (since := "2024-09-23")]
 def USize.modn (a : USize) (n : @& Nat) : USize := ⟨Fin.modn a.val n⟩
 @[extern "lean_usize_land"]
-def USize.land (a b : USize) : USize := ⟨Fin.land a.val b.val⟩
+def USize.land (a b : USize) : USize := ⟨a.toBitVec &&& b.toBitVec⟩
 @[extern "lean_usize_lor"]
-def USize.lor (a b : USize) : USize := ⟨Fin.lor a.val b.val⟩
+def USize.lor (a b : USize) : USize := ⟨a.toBitVec ||| b.toBitVec⟩
 @[extern "lean_usize_xor"]
-def USize.xor (a b : USize) : USize := ⟨Fin.xor a.val b.val⟩
+def USize.xor (a b : USize) : USize := ⟨a.toBitVec ^^^ b.toBitVec⟩
 @[extern "lean_usize_shift_left"]
-def USize.shiftLeft (a b : USize) : USize := ⟨a.val <<< (modn b System.Platform.numBits).val⟩
+def USize.shiftLeft (a b : USize) : USize := ⟨a.toBitVec <<< (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
 @[extern "lean_usize_shift_right"]
-def USize.shiftRight (a b : USize) : USize := ⟨a.val >>> (modn b System.Platform.numBits).val⟩
+def USize.shiftRight (a b : USize) : USize := ⟨a.toBitVec >>> (mod b (USize.ofNat System.Platform.numBits)).toBitVec⟩
 @[extern "lean_uint32_to_usize"]
-def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.val a.1.2
+def UInt32.toUSize (a : UInt32) : USize := USize.ofNat32 a.toBitVec.toNat a.toBitVec.isLt
 @[extern "lean_usize_to_uint32"]
 def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 
-def USize.lt (a b : USize) : Prop := a.val < b.val
-def USize.le (a b : USize) : Prop := a.val ≤ b.val
-
-instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
-instance : Add USize       := ⟨USize.add⟩
-instance : Sub USize       := ⟨USize.sub⟩
 instance : Mul USize       := ⟨USize.mul⟩
 instance : Mod USize       := ⟨USize.mod⟩
+
+set_option linter.deprecated false in
 instance : HMod USize Nat USize := ⟨USize.modn⟩
+
 instance : Div USize       := ⟨USize.div⟩
-instance : LT USize        := ⟨USize.lt⟩
-instance : LE USize        := ⟨USize.le⟩
 
 @[extern "lean_usize_complement"]
-def USize.complement (a:USize) : USize := 0-(a+1)
+def USize.complement (a : USize) : USize := ⟨~~~a.toBitVec⟩
 
 instance : Complement USize := ⟨USize.complement⟩
 instance : AndOp USize      := ⟨USize.land⟩
@@ -354,19 +278,5 @@ instance : Xor USize        := ⟨USize.xor⟩
 instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
-set_option bootstrap.genMatcherCode false in
-@[extern "lean_usize_dec_lt"]
-def USize.decLt (a b : USize) : Decidable (a < b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
-
-set_option bootstrap.genMatcherCode false in
-@[extern "lean_usize_dec_le"]
-def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
-
-instance (a b : USize) : Decidable (a < b) := USize.decLt a b
-instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
 instance : Max USize := maxOfLe
 instance : Min USize := minOfLe
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
new file mode 100644
index 0000000000..b751f6f3d9
--- /dev/null
+++ b/src/Init/Data/UInt/BasicAux.lean
@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Fin.Basic
+import Init.Data.BitVec.BasicAux
+
+/-!
+This module exists to provide the very basic `UInt8` etc. definitions required for
+`Init.Data.Char.Basic` and `Init.Data.Array.Basic`. These are very important as they are used in
+meta code that is then (transitively) used in `Init.Data.UInt.Basic` and `Init.Data.BitVec.Basic`.
+This file thus breaks the import cycle that would be created by this dependency.
+-/
+
+open Nat
+
+def UInt8.val (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
+@[extern "lean_uint8_of_nat"]
+def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩
+abbrev Nat.toUInt8 := UInt8.ofNat
+@[extern "lean_uint8_to_nat"]
+def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
+
+instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
+
+def UInt16.val (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
+@[extern "lean_uint16_of_nat"]
+def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨BitVec.ofNat 16 n⟩
+abbrev Nat.toUInt16 := UInt16.ofNat
+@[extern "lean_uint16_to_nat"]
+def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat
+@[extern "lean_uint16_to_uint8"]
+def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint8_to_uint16"]
+def UInt8.toUInt16 (a : UInt8) : UInt16 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+
+instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
+
+def UInt32.val (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
+@[extern "lean_uint32_of_nat"]
+def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩
+@[extern "lean_uint32_of_nat"]
+def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨BitVec.ofNatLt n h⟩
+/--
+Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
+-/
+def UInt32.ofNatTruncate (n : Nat) : UInt32 :=
+  if h : n < UInt32.size then
+    UInt32.ofNat' n h
+  else
+    UInt32.ofNat' (UInt32.size - 1) (by decide)
+abbrev Nat.toUInt32 := UInt32.ofNat
+@[extern "lean_uint32_to_uint8"]
+def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint32_to_uint16"]
+def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
+@[extern "lean_uint8_to_uint32"]
+def UInt8.toUInt32 (a : UInt8) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+@[extern "lean_uint16_to_uint32"]
+def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+
+instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
+
+theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
+     n < m → UInt32.ofNat' n h1 < UInt32.ofNat m := by
+  simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
+    Nat.mod_eq_of_lt h2, imp_self]
+
+theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
+     m < n → UInt32.ofNat m < UInt32.ofNat' n h1  := by
+  simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLt, ofNat, BitVec.ofNat, Fin.ofNat',
+    Nat.mod_eq_of_lt h2, imp_self]
+
+def UInt64.val (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
+@[extern "lean_uint64_of_nat"]
+def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨BitVec.ofNat 64 n⟩
+abbrev Nat.toUInt64 := UInt64.ofNat
+@[extern "lean_uint64_to_nat"]
+def UInt64.toNat (n : UInt64) : Nat := n.toBitVec.toNat
+@[extern "lean_uint64_to_uint8"]
+def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
+@[extern "lean_uint64_to_uint16"]
+def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
+@[extern "lean_uint64_to_uint32"]
+def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
+@[extern "lean_uint8_to_uint64"]
+def UInt8.toUInt64 (a : UInt8) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+@[extern "lean_uint16_to_uint64"]
+def UInt16.toUInt64 (a : UInt16) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+@[extern "lean_uint32_to_uint64"]
+def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBitVec.isLt (by decide)⟩⟩
+
+instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
+
+theorem usize_size_gt_zero : USize.size > 0 := by
+  cases usize_size_eq with
+  | inl h => rw [h]; decide
+  | inr h => rw [h]; decide
+
+def USize.val (x : USize) : Fin USize.size := x.toBitVec.toFin
+@[extern "lean_usize_of_nat"]
+def USize.ofNat (n : @& Nat) : USize := ⟨BitVec.ofNat _ n⟩
+abbrev Nat.toUSize := USize.ofNat
+@[extern "lean_usize_to_nat"]
+def USize.toNat (n : USize) : Nat := n.toBitVec.toNat
+@[extern "lean_usize_add"]
+def USize.add (a b : USize) : USize := ⟨a.toBitVec + b.toBitVec⟩
+@[extern "lean_usize_sub"]
+def USize.sub (a b : USize) : USize := ⟨a.toBitVec - b.toBitVec⟩
+
+def USize.lt (a b : USize) : Prop := a.toBitVec < b.toBitVec
+def USize.le (a b : USize) : Prop := a.toBitVec ≤ b.toBitVec
+
+instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
+
+instance : Add USize       := ⟨USize.add⟩
+instance : Sub USize       := ⟨USize.sub⟩
+instance : LT USize        := ⟨USize.lt⟩
+instance : LE USize        := ⟨USize.le⟩
+
+@[extern "lean_usize_dec_lt"]
+def USize.decLt (a b : USize) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
+
+@[extern "lean_usize_dec_le"]
+def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
+  inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
+
+instance (a b : USize) : Decidable (a < b) := USize.decLt a b
+instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean
index 4c3a04571a..b9282fcf4f 100644
--- a/src/Init/Data/UInt/Bitwise.lean
+++ b/src/Init/Data/UInt/Bitwise.lean
@@ -6,13 +6,14 @@ Authors: Markus Himmel
 prelude
 import Init.Data.UInt.Basic
 import Init.Data.Fin.Bitwise
+import Init.Data.BitVec.Lemmas
 
 set_option hygiene false in
 macro "declare_bitwise_uint_theorems" typeName:ident : command =>
 `(
 namespace $typeName
 
-@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
+@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
 
 end $typeName
 )
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index 3500dc24cd..ff376e15cc 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.UInt.Basic
 import Init.Data.Fin.Lemmas
+import Init.Data.BitVec.Lemmas
+import Init.Data.BitVec.Bitblast
 
 set_option hygiene false in
 macro "declare_uint_theorems" typeName:ident : command =>
@@ -17,48 +19,100 @@ instance : Inhabited $typeName where
 
 theorem zero_def : (0 : $typeName) = ⟨0⟩ := rfl
 theorem one_def : (1 : $typeName) = ⟨1⟩ := rfl
-theorem sub_def (a b : $typeName) : a - b = ⟨a.val - b.val⟩ := rfl
-theorem mul_def (a b : $typeName) : a * b = ⟨a.val * b.val⟩ := rfl
-theorem mod_def (a b : $typeName) : a % b = ⟨a.val % b.val⟩ := rfl
-theorem add_def (a b : $typeName) : a + b = ⟨a.val + b.val⟩ := rfl
+theorem sub_def (a b : $typeName) : a - b = ⟨a.toBitVec - b.toBitVec⟩ := rfl
+theorem mul_def (a b : $typeName) : a * b = ⟨a.toBitVec * b.toBitVec⟩ := rfl
+theorem mod_def (a b : $typeName) : a % b = ⟨a.toBitVec % b.toBitVec⟩ := rfl
+theorem add_def (a b : $typeName) : a + b = ⟨a.toBitVec + b.toBitVec⟩ := rfl
 
-@[simp] theorem mk_val_eq : ∀ (a : $typeName), mk a.val = a
+@[simp] theorem mk_toBitVec_eq : ∀ (a : $typeName), mk a.toBitVec = a
   | ⟨_, _⟩ => rfl
-theorem val_eq_of_lt {a : Nat} : a < size → ((ofNat a).val : Nat) = a :=
-  Nat.mod_eq_of_lt
-theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
-  rw [toNat, val_eq_of_lt h]
 
-theorem le_def {a b : $typeName} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
-theorem lt_def {a b : $typeName} : a < b ↔ a.1 < b.1 := .rfl
-theorem lt_iff_val_lt_val {a b : $typeName} : a < b ↔ a.val < b.val := .rfl
-@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := Fin.not_le
-@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := Fin.not_lt
+theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
+  Nat.mod_eq_of_lt
+
+theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
+  rw [toNat, toBitVec_eq_of_lt h]
+
+theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
+
+theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
+
+@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := by simp [le_def, lt_def]
+
+@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := by simp [le_def, lt_def]
+
 @[simp] protected theorem le_refl (a : $typeName) : a ≤ a := by simp [le_def]
+
 @[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
-protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := Fin.le_trans
-protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := Fin.lt_trans
-protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := Fin.le_total a.1 b.1
-protected theorem lt_asymm {a b : $typeName} (h : a < b) : ¬ b < a := Fin.lt_asymm h
-protected theorem val_eq_of_eq {a b : $typeName} (h : a = b) : a.val = b.val := h ▸ rfl
-protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by cases a; cases b; simp at h; simp [h]
-open $typeName (val_eq_of_eq) in
-protected theorem ne_of_val_ne {a b : $typeName} (h : a.val ≠ b.val) : a ≠ b := fun h' => absurd (val_eq_of_eq h') h
-open $typeName (ne_of_val_ne) in
-protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := ne_of_val_ne (Fin.ne_of_lt h)
+
+protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
+
+protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_trans
+
+protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
+
+protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
+
+protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl
+
+protected theorem eq_of_toBitVec_eq {a b : $typeName} (h : a.toBitVec = b.toBitVec) : a = b := by
+  cases a; cases b; simp_all
+
+open $typeName (eq_of_toBitVec_eq) in
+protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
+  rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
+
+open $typeName (toBitVec_eq_of_eq) in
+protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b :=
+  fun h' => absurd (toBitVec_eq_of_eq h') h
+
+open $typeName (ne_of_toBitVec_ne) in
+protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := by
+  apply ne_of_toBitVec_ne
+  apply BitVec.ne_of_lt
+  simpa [lt_def] using h
 
 @[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
-@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
-@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
-@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
-@[simp] protected theorem toNat_modn (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
-protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m
-  | ⟨u⟩, h => Fin.modn_lt u h
-open $typeName (modn_lt) in
-protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
+
+@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := BitVec.toNat_umod ..
+
+@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := BitVec.toNat_udiv  ..
+
+@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := BitVec.toNat_sub_of_le
+
+protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt
+
+open $typeName (toNat_mod toNat_lt_size) in
+protected theorem toNat_mod_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % ofNat m) < m := by
+  intro u h1
+  by_cases h2 : m < size
+  · rw [toNat_mod, toNat_ofNat_of_lt h2]
+    apply Nat.mod_lt _ h1
+  · apply Nat.lt_of_lt_of_le
+    · apply toNat_lt_size
+    · simpa using h2
+
+open $typeName (toNat_mod_lt) in
+set_option linter.deprecated false in
+@[deprecated toNat_mod_lt (since := "2024-09-24")]
+protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m := by
+  intro u
+  simp only [(· % ·)]
+  simp only [gt_iff_lt, toNat, modn, Fin.modn_val, BitVec.natCast_eq_ofNat, BitVec.toNat_ofNat,
+    Nat.reducePow]
+  rw [Nat.mod_eq_of_lt]
+  · apply Nat.mod_lt
+  · apply Nat.lt_of_le_of_lt
+    · apply Nat.mod_le
+    · apply Fin.is_lt
+
+protected theorem mod_lt (a : $typeName) {b : $typeName} : 0 < b → a % b < b := by
+  simp only [lt_def, mod_def]
+  apply BitVec.umod_lt
+
 protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
-protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.1.2
+
 @[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
 
 end $typeName
@@ -70,27 +124,34 @@ declare_uint_theorems UInt32
 declare_uint_theorems UInt64
 declare_uint_theorems USize
 
+theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
+  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
+theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by
+  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
+theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by
+  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
+theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
+  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev UInt8.modn_toNat := @UInt8.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev UInt16.modn_toNat := @UInt16.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev UInt32.modn_toNat := @UInt32.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev UInt64.modn_toNat := @UInt64.toNat_modn
 
 @[deprecated (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero
 @[deprecated (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div
 @[deprecated (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod
-@[deprecated (since := "2024-06-23")] protected abbrev USize.modn_toNat := @USize.toNat_modn
diff --git a/src/Init/Data/UInt/Log2.lean b/src/Init/Data/UInt/Log2.lean
index 3e6bb6e18f..f34c711122 100644
--- a/src/Init/Data/UInt/Log2.lean
+++ b/src/Init/Data/UInt/Log2.lean
@@ -7,16 +7,16 @@ prelude
 import Init.Data.Fin.Log2
 
 @[extern "lean_uint8_log2"]
-def UInt8.log2 (a : UInt8) : UInt8 := ⟨Fin.log2 a.val⟩
+def UInt8.log2 (a : UInt8) : UInt8 := ⟨⟨Fin.log2 a.val⟩⟩
 
 @[extern "lean_uint16_log2"]
-def UInt16.log2 (a : UInt16) : UInt16 := ⟨Fin.log2 a.val⟩
+def UInt16.log2 (a : UInt16) : UInt16 := ⟨⟨Fin.log2 a.val⟩⟩
 
 @[extern "lean_uint32_log2"]
-def UInt32.log2 (a : UInt32) : UInt32 := ⟨Fin.log2 a.val⟩
+def UInt32.log2 (a : UInt32) : UInt32 := ⟨⟨Fin.log2 a.val⟩⟩
 
 @[extern "lean_uint64_log2"]
-def UInt64.log2 (a : UInt64) : UInt64 := ⟨Fin.log2 a.val⟩
+def UInt64.log2 (a : UInt64) : UInt64 := ⟨⟨Fin.log2 a.val⟩⟩
 
 @[extern "lean_usize_log2"]
-def USize.log2 (a : USize) : USize := ⟨Fin.log2 a.val⟩
+def USize.log2 (a : USize) : USize := ⟨⟨Fin.log2 a.val⟩⟩
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index ab04ea8ba8..28cd71a307 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1866,6 +1866,52 @@ instance {n} : LE (Fin n) where
 instance Fin.decLt {n} (a b : Fin n) : Decidable (LT.lt a b) := Nat.decLt ..
 instance Fin.decLe {n} (a b : Fin n) : Decidable (LE.le a b) := Nat.decLe ..
 
+/--
+A bitvector of the specified width.
+
+This is represented as the underlying `Nat` number in both the runtime
+and the kernel, inheriting all the special support for `Nat`.
+-/
+structure BitVec (w : Nat) where
+  /-- Construct a `BitVec w` from a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  ofFin ::
+  /-- Interpret a bitvector as a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  toFin : Fin (hPow 2 w)
+
+/--
+Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
+-/
+-- We manually derive the `DecidableEq` instances for `BitVec` because
+-- we want to have builtin support for bit-vector literals, and we
+-- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
+def BitVec.decEq (x y : BitVec n) : Decidable (Eq x y) :=
+  match x, y with
+  | ⟨n⟩, ⟨m⟩ =>
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h)))
+
+instance : DecidableEq (BitVec n) := BitVec.decEq
+
+/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
+@[match_pattern]
+protected def BitVec.ofNatLt {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
+  toFin := ⟨i, p⟩
+
+/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
+(zero-cost) wrapper around a `Nat`. -/
+protected def BitVec.toNat (x : BitVec n) : Nat := x.toFin.val
+
+instance : LT (BitVec n) where lt := (LT.lt ·.toNat ·.toNat)
+instance (x y : BitVec n) : Decidable (LT.lt x y) :=
+  inferInstanceAs (Decidable (LT.lt x.toNat y.toNat))
+
+instance : LE (BitVec n) where le := (LE.le ·.toNat ·.toNat)
+instance (x y : BitVec n) : Decidable (LE.le x y) :=
+  inferInstanceAs (Decidable (LE.le x.toNat y.toNat))
+
 /-- The size of type `UInt8`, that is, `2^8 = 256`. -/
 abbrev UInt8.size : Nat := 256
 
@@ -1874,12 +1920,12 @@ The type of unsigned 8-bit integers. This type has special support in the
 compiler to make it actually 8 bits rather than wrapping a `Nat`.
 -/
 structure UInt8 where
-  /-- Unpack a `UInt8` as a `Nat` less than `2^8`.
+  /-- Unpack a `UInt8` as a `BitVec 8`.
   This function is overridden with a native implementation. -/
-  val : Fin UInt8.size
+  toBitVec : BitVec 8
 
 attribute [extern "lean_uint8_of_nat_mk"] UInt8.mk
-attribute [extern "lean_uint8_to_nat"] UInt8.val
+attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec
 
 /--
 Pack a `Nat` less than `2^8` into a `UInt8`.
@@ -1887,7 +1933,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint8_of_nat"]
 def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
-  val := { val := n, isLt := h }
+  toBitVec := BitVec.ofNatLt n h
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1898,7 +1944,9 @@ This function is overridden with a native implementation.
 def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt8 := UInt8.decEq
 
@@ -1913,12 +1961,12 @@ The type of unsigned 16-bit integers. This type has special support in the
 compiler to make it actually 16 bits rather than wrapping a `Nat`.
 -/
 structure UInt16 where
-  /-- Unpack a `UInt16` as a `Nat` less than `2^16`.
+  /-- Unpack a `UInt16` as a `BitVec 16`.
   This function is overridden with a native implementation. -/
-  val : Fin UInt16.size
+  toBitVec : BitVec 16
 
 attribute [extern "lean_uint16_of_nat_mk"] UInt16.mk
-attribute [extern "lean_uint16_to_nat"] UInt16.val
+attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec
 
 /--
 Pack a `Nat` less than `2^16` into a `UInt16`.
@@ -1926,7 +1974,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint16_of_nat"]
 def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
-  val := { val := n, isLt := h }
+  toBitVec := BitVec.ofNatLt n h
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1937,7 +1985,9 @@ This function is overridden with a native implementation.
 def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt16 := UInt16.decEq
 
@@ -1952,12 +2002,12 @@ The type of unsigned 32-bit integers. This type has special support in the
 compiler to make it actually 32 bits rather than wrapping a `Nat`.
 -/
 structure UInt32 where
-  /-- Unpack a `UInt32` as a `Nat` less than `2^32`.
+  /-- Unpack a `UInt32` as a `BitVec 32.
   This function is overridden with a native implementation. -/
-  val : Fin UInt32.size
+  toBitVec : BitVec 32
 
 attribute [extern "lean_uint32_of_nat_mk"] UInt32.mk
-attribute [extern "lean_uint32_to_nat"] UInt32.val
+attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec
 
 /--
 Pack a `Nat` less than `2^32` into a `UInt32`.
@@ -1965,14 +2015,14 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
-  val := { val := n, isLt := h }
+  toBitVec := BitVec.ofNatLt n h
 
 /--
 Unpack a `UInt32` as a `Nat`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_to_nat"]
-def UInt32.toNat (n : UInt32) : Nat := n.val.val
+def UInt32.toNat (n : UInt32) : Nat := n.toBitVec.toNat
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1991,30 +2041,26 @@ instance : Inhabited UInt32 where
   default := UInt32.ofNatCore 0 (by decide)
 
 instance : LT UInt32 where
-  lt a b := LT.lt a.val b.val
+  lt a b := LT.lt a.toBitVec b.toBitVec
 
 instance : LE UInt32 where
-  le a b := LE.le a.val b.val
+  le a b := LE.le a.toBitVec b.toBitVec
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides less-equal on `UInt32`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_dec_lt"]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LT.lt n m))
+  inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides less-than on `UInt32`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_dec_le"]
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LE.le n m))
+  inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 
 instance (a b : UInt32) : Decidable (LT.lt a b) := UInt32.decLt a b
 instance (a b : UInt32) : Decidable (LE.le a b) := UInt32.decLe a b
@@ -2028,12 +2074,12 @@ The type of unsigned 64-bit integers. This type has special support in the
 compiler to make it actually 64 bits rather than wrapping a `Nat`.
 -/
 structure UInt64 where
-  /-- Unpack a `UInt64` as a `Nat` less than `2^64`.
+  /-- Unpack a `UInt64` as a `BitVec 64`.
   This function is overridden with a native implementation. -/
-  val : Fin UInt64.size
+  toBitVec: BitVec 64
 
 attribute [extern "lean_uint64_of_nat_mk"] UInt64.mk
-attribute [extern "lean_uint64_to_nat"] UInt64.val
+attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec
 
 /--
 Pack a `Nat` less than `2^64` into a `UInt64`.
@@ -2041,7 +2087,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint64_of_nat"]
 def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
-  val := { val := n, isLt := h }
+  toBitVec := BitVec.ofNatLt n h
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -2052,36 +2098,20 @@ This function is overridden with a native implementation.
 def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq UInt64 := UInt64.decEq
 
 instance : Inhabited UInt64 where
   default := UInt64.ofNatCore 0 (by decide)
 
-/--
-The size of type `USize`, that is, `2^System.Platform.numBits`, which may
-be either `2^32` or `2^64` depending on the platform's architecture.
-
-Remark: we define `USize.size` using `(2^numBits - 1) + 1` to ensure the
-Lean unifier can solve constraints such as `?m + 1 = USize.size`. Recall that
-`numBits` does not reduce to a numeral in the Lean kernel since it is platform
-specific. Without this trick, the following definition would be rejected by the
-Lean type checker.
-```
-def one: Fin USize.size := 1
-```
-Because Lean would fail to synthesize instance `OfNat (Fin USize.size) 1`.
-Recall that the `OfNat` instance for `Fin` is
-```
-instance : OfNat (Fin (n+1)) i where
-  ofNat := Fin.ofNat i
-```
--/
-abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
+/-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
+abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
 
 theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
-  show Or (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 4294967296) (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 18446744073709551616) from
+  show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
   match System.Platform.numBits, System.Platform.numBits_eq with
   | _, Or.inl rfl => Or.inl (by decide)
   | _, Or.inr rfl => Or.inr (by decide)
@@ -2094,21 +2124,20 @@ For example, if running on a 32-bit machine, USize is equivalent to UInt32.
 Or on a 64-bit machine, UInt64.
 -/
 structure USize where
-  /-- Unpack a `USize` as a `Nat` less than `USize.size`.
+  /-- Unpack a `USize` as a `BitVec System.Platform.numBits`.
   This function is overridden with a native implementation. -/
-  val : Fin USize.size
+  toBitVec : BitVec System.Platform.numBits
 
 attribute [extern "lean_usize_of_nat_mk"] USize.mk
-attribute [extern "lean_usize_to_nat"] USize.val
+attribute [extern "lean_usize_to_nat"] USize.toBitVec
 
 /--
 Pack a `Nat` less than `USize.size` into a `USize`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_of_nat"]
-def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize := {
-  val := { val := n, isLt := h }
-}
+def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize where
+  toBitVec := BitVec.ofNatLt n h
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -2119,7 +2148,9 @@ This function is overridden with a native implementation.
 def USize.decEq (a b : USize) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h =>isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq n m)
+      (fun h => isTrue (h ▸ rfl))
+      (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq USize := USize.decEq
 
@@ -2135,12 +2166,12 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_of_nat"]
 def USize.ofNat32 (n : @& Nat) (h : LT.lt n 4294967296) : USize where
-  val := {
-    val  := n
-    isLt := match USize.size, usize_size_eq with
+  toBitVec :=
+    BitVec.ofNatLt n (
+      match System.Platform.numBits, System.Platform.numBits_eq with
       | _, Or.inl rfl => h
       | _, Or.inr rfl => Nat.lt_trans h (by decide)
-  }
+    )
 
 /--
 A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and
@@ -2175,7 +2206,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_of_nat"]
 def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
-  { val := ⟨{ val := n, isLt := isValidChar_UInt32 h }⟩, valid := h }
+  { val := ⟨BitVec.ofNatLt n (isValidChar_UInt32 h)⟩, valid := h }
 
 /--
 Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scalar value,
@@ -2185,7 +2216,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal
 def Char.ofNat (n : Nat) : Char :=
   dite (n.isValidChar)
     (fun h => Char.ofNatAux n h)
-    (fun _ => { val := ⟨{ val := 0, isLt := by decide }⟩, valid := Or.inl (by decide) })
+    (fun _ => { val := ⟨BitVec.ofNatLt 0 (by decide)⟩, valid := Or.inl (by decide) })
 
 theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -3445,15 +3476,13 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_to_uint64"]
 def USize.toUInt64 (u : USize) : UInt64 where
-  val := {
-    val  := u.val.val
-    isLt :=
-      let ⟨n, h⟩ := u
-      show LT.lt n _ from
-      match USize.size, usize_size_eq, h with
-      | _, Or.inl rfl, h => Nat.lt_trans h (by decide)
-      | _, Or.inr rfl, h => h
-  }
+  toBitVec := BitVec.ofNatLt u.toBitVec.toNat (
+        let ⟨⟨n, h⟩⟩ := u
+        show LT.lt n _ from
+        match System.Platform.numBits, System.Platform.numBits_eq, h with
+        | _, Or.inl rfl, h => Nat.lt_trans h (by decide)
+        | _, Or.inr rfl, h => h
+      )
 
 /-- An opaque hash mixing operation, used to implement hashing for tuples. -/
 @[extern "lean_uint64_mix_hash"]
diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean
index 9c59cf6c17..209967f59d 100644
--- a/src/Init/SizeOf.lean
+++ b/src/Init/SizeOf.lean
@@ -67,6 +67,7 @@ deriving instance SizeOf for PLift
 deriving instance SizeOf for ULift
 deriving instance SizeOf for Decidable
 deriving instance SizeOf for Fin
+deriving instance SizeOf for BitVec
 deriving instance SizeOf for UInt8
 deriving instance SizeOf for UInt16
 deriving instance SizeOf for UInt32
diff --git a/src/Init/SizeOfLemmas.lean b/src/Init/SizeOfLemmas.lean
index dd75ee0b67..ce0d077d3f 100644
--- a/src/Init/SizeOfLemmas.lean
+++ b/src/Init/SizeOfLemmas.lean
@@ -11,22 +11,25 @@ import Init.Data.Nat.Linear
 @[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
   cases a; simp_arith
 
-@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [UInt8.toNat]
+@[simp] protected theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
+  cases a; simp_arith
 
-@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [UInt16.toNat]
+@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [UInt8.toNat, BitVec.toNat]
 
-@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [UInt32.toNat]
+@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [UInt16.toNat, BitVec.toNat]
 
-@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [UInt64.toNat]
+@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [UInt32.toNat, BitVec.toNat]
 
-@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
-  cases a; simp_arith [USize.toNat]
+@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [UInt64.toNat, BitVec.toNat]
 
-@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
+@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3 := by
+  cases a; simp_arith [USize.toNat, BitVec.toNat]
+
+@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4 := by
   cases a; simp_arith [Char.toNat]
 
 @[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
diff --git a/src/Lean/Data/PersistentArray.lean b/src/Lean/Data/PersistentArray.lean
index 579a61ecfd..427d17fc38 100644
--- a/src/Lean/Data/PersistentArray.lean
+++ b/src/Lean/Data/PersistentArray.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Data.Array.Basic
 import Init.NotationExtra
 import Init.Data.ToString.Macro
+import Init.Data.UInt.Basic
 
 universe u v w
 
diff --git a/src/Lean/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean
index 6d3dc49ad4..16cd8b4c59 100644
--- a/src/Lean/Data/PersistentHashMap.lean
+++ b/src/Lean/Data/PersistentHashMap.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.BasicAux
 import Init.Data.ToString.Macro
+import Init.Data.UInt.Basic
 
 namespace Lean
 universe u v w w'
diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean
index 6e0ee722dd..9d29b18f4c 100644
--- a/src/Lean/ToExpr.lean
+++ b/src/Lean/ToExpr.lean
@@ -59,35 +59,35 @@ instance : ToExpr (BitVec n) where
 instance : ToExpr UInt8 where
   toTypeExpr := mkConst ``UInt8
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt8) r
       (.app (.const ``UInt8.instOfNat []) r)
 
 instance : ToExpr UInt16 where
   toTypeExpr := mkConst ``UInt16
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt16) r
       (.app (.const ``UInt16.instOfNat []) r)
 
 instance : ToExpr UInt32 where
   toTypeExpr := mkConst ``UInt32
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt32) r
       (.app (.const ``UInt32.instOfNat []) r)
 
 instance : ToExpr UInt64 where
   toTypeExpr := mkConst ``UInt64
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``UInt64) r
       (.app (.const ``UInt64.instOfNat []) r)
 
 instance : ToExpr USize where
   toTypeExpr := mkConst ``USize
   toExpr a :=
-    let r := mkRawNatLit a.val
+    let r := mkRawNatLit a.toNat
     mkApp3 (.const ``OfNat.ofNat [0]) (mkConst ``USize) r
       (.app (.const ``USize.instOfNat []) r)
 
diff --git a/src/Std/Data/DHashMap/Internal/Index.lean b/src/Std/Data/DHashMap/Internal/Index.lean
index a6afa47b56..60e14072e7 100644
--- a/src/Std/Data/DHashMap/Internal/Index.lean
+++ b/src/Std/Data/DHashMap/Internal/Index.lean
@@ -54,9 +54,9 @@ cf. https://github.com/leanprover/lean4/issues/4157
         · exact Nat.one_pos
         · exact Nat.lt_of_le_of_lt h h'
       · exact h'
-      · rw [USize.le_def, Fin.le_def]
+      · rw [USize.le_def, BitVec.le_def]
         change _ ≤ (_ % _)
-        rw [Nat.mod_eq_of_lt h', USize.ofNat, Fin.val_ofNat', Nat.mod_eq_of_lt]
+        rw [Nat.mod_eq_of_lt h', USize.ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
         · exact h
         · exact Nat.lt_of_le_of_lt h h'
     · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩
diff --git a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
index 762aa169d6..c6e33b4c8d 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
@@ -81,8 +81,7 @@ attribute [bv_normalize] BitVec.testBit_toNat
 @[bv_normalize]
 theorem BitVec.lt_ult (x y : BitVec w) : (x < y) = (BitVec.ult x y = true) := by
   rw [BitVec.ult]
-  rw [LT.lt]
-  rw [BitVec.instLT]
+  simp only [(· < ·)]
   simp
 
 attribute [bv_normalize] BitVec.natCast_eq_ofNat
diff --git a/src/lake/Lake/Util/Compare.lean b/src/lake/Lake/Util/Compare.lean
index 8afc6d89ce..8dec7bb511 100644
--- a/src/lake/Lake/Util/Compare.lean
+++ b/src/lake/Lake/Util/Compare.lean
@@ -64,7 +64,7 @@ instance : LawfulCmpEq Nat compare where
 
 instance : LawfulCmpEq UInt64 compare where
   eq_of_cmp h := eq_of_compareOfLessAndEq h
-  cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
+  cmp_rfl := compareOfLessAndEq_rfl <| UInt64.lt_irrefl _
 
 instance : LawfulCmpEq String compare where
   eq_of_cmp := eq_of_compareOfLessAndEq
diff --git a/tests/lean/run/4465.lean b/tests/lean/run/4465.lean
index ca890dbe65..94591e5dad 100644
--- a/tests/lean/run/4465.lean
+++ b/tests/lean/run/4465.lean
@@ -1,9 +1,9 @@
-/-- info: { val := { val := ⟨0, ⋯⟩ }, valid := ⋯ } -/
+/-- info: { val := { toBitVec := { toFin := ⟨0, ⋯⟩ } }, valid := ⋯ } -/
 #guard_msgs in
 #reduce Char.ofNat (nat_lit 0)
 
 /--
-info: { val := { val := ⟨0, isValidChar_UInt32 (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ },
+info: { val := { toBitVec := { toFin := ⟨0, isValidChar_UInt32 (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ } },
   valid := Or.inl (Nat.le_of_ble_eq_true rfl) }
 -/
 #guard_msgs in
diff --git a/tests/lean/sizeof.lean.expected.out b/tests/lean/sizeof.lean.expected.out
index 52020debae..59217b3878 100644
--- a/tests/lean/sizeof.lean.expected.out
+++ b/tests/lean/sizeof.lean.expected.out
@@ -1,10 +1,10 @@
 10
 6
 7
-12
-100
-553
-308
-310
+13
+101
+558
+311
+313
 11
 InfTree.node.sizeOf_spec.{u} {α : Type u} [SizeOf α] (children : Nat → InfTree α) : sizeOf (InfTree.node children) = 1
diff --git a/tests/lean/uintCtors.lean b/tests/lean/uintCtors.lean
index dc4ddf7407..64104bfebf 100644
--- a/tests/lean/uintCtors.lean
+++ b/tests/lean/uintCtors.lean
@@ -1,34 +1,34 @@
 def UInt32.ofNatCore' (n : Nat) (h : n < UInt32.size) : UInt32 := {
-  val := { val := n, isLt := h }
+  toBitVec := ⟨{ val := n, isLt := h }⟩
 }
 
 #eval UInt32.ofNatCore' 10 (by decide)
 
 def UInt64.ofNatCore' (n : Nat) (h : n < UInt64.size) : UInt64 := {
-  val := { val := n, isLt := h }
+  toBitVec := ⟨{ val := n, isLt := h }⟩
 }
 
 #eval UInt64.ofNatCore' 3 (by decide)
 
-#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt8 }
+#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt8 }
 #eval (3 : UInt8).val
-#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt16 }
+#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt16 }
 #eval (3 : UInt16).val
-#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt32 }
+#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt32 }
 #eval (3 : UInt32).val
-#eval toString $ { val := { val := 3, isLt := (by decide) } : UInt64 }
+#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt64 }
 #eval (3 : UInt64).val
-#eval toString $ { val := { val := 3, isLt := (match USize.size, usize_size_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
+#eval toString $ { toBitVec := ⟨{ val := 3, isLt := (match System.Platform.numBits, System.Platform.numBits_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) }⟩ : USize }
 #eval (3 : USize).val
 
 
-#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt8 }
+#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt8 }
 #eval (4 : UInt8).val
-#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt16 }
+#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt16 }
 #eval (4 : UInt16).val
-#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt32 }
+#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt32 }
 #eval (4 : UInt32).val
-#eval toString $ { val := { val := 4, isLt := (by decide) } : UInt64 }
+#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt64 }
 #eval (4 : UInt64).val
-#eval toString $ { val := { val := 4, isLt := (match USize.size, usize_size_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
+#eval toString $ { toBitVec := ⟨{ val := 4, isLt := (match System.Platform.numBits, System.Platform.numBits_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) }⟩ : USize }
 #eval (4 : USize).val