refactor: redefine unsigned fixed width integers in terms of BitVec

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

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

src/Init/Data/BitVec/Basic.lean

@@ -8,6 +8,7 @@ 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
@@ -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,21 +324,13 @@ 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.
 
 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.
 

src/Init/Data/BitVec/BasicAux.lean

@@ -0,0 +1,47 @@
+/-
+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
+
+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

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'

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 _))⟩
 

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]

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
 

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

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

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