From fbf47928076b41a8ade4d8a2492d2de9dc5e27a3 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Fri, 19 Dec 2025 10:17:37 +0100
Subject: [PATCH] feat: add BitVec.ofBitVecList

---
 src/Init/Data/BitVec/Basic.lean | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 1c7b99a9aba4..6e355783cd16 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -771,6 +771,34 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length
 | [] => 0#0
 | b :: bs => concat (ofBoolListLE bs) b
 
+/-- Converts a list of `BitVec`s into a single concatenated `BitVec`. -/
+def ofBitVecList {n : Nat} : (bvs : List (BitVec n)) → BitVec (n * bvs.length)
+| [] => 0#0
+| bv :: bvs => (bv ++ ofBitVecList bvs).cast (by simp; rw [Nat.mul_add]; omega)
+
+/-- Convert a `BitVec` into a list of `BitVec`. -/
+def toBitVecList {n : Nat} : (bv : BitVec (n * m)) → List (BitVec n) :=
+  let rec aux : (bv : BitVec (n * m)) → (acc : List (BitVec n)) → Nat → List (BitVec n)
+    | bv, acc, 0 => acc.reverse
+    | bv, acc, k + 1 =>
+      let part := bv.extractLsb' (k * n) n
+      aux bv (part :: acc) k
+  aux bv [] m
+
+/-- Converts an array of `BitVec`s into a single concatenated `BitVec`. -/
+def ofBitVecArray {n : Nat} : (bvs : Array (BitVec n)) → BitVec (n * bvs.size)
+| ⟨[]⟩ => 0#0
+| ⟨x :: xs⟩ => (x ++ ofBitVecArray ⟨xs⟩).cast (by simp; rw [Nat.mul_add]; omega)
+
+/-- Convert a `BitVec` into an array of `BitVec`. -/
+def toBitVecArray {n : Nat} : (bv : BitVec (n * m)) → Array (BitVec n) :=
+  let rec aux : (bv : BitVec (n * m)) → (acc : Array (BitVec n)) → Nat → Array (BitVec n)
+    | bv, acc, 0 => acc
+    | bv, acc, k + 1 =>
+      let part := bv.extractLsb' (k * n) n
+      aux bv (acc.push part) k
+  aux bv #[] m
+
 /-! ## Overflow -/
 
 /--