Skip to content

Commit 489177e

Browse files
f64uf64u
committed
feat: add ByteArray conversions for BitVec
1 parent 09bca7a commit 489177e

File tree

2 files changed

+228
-4
lines changed

2 files changed

+228
-4
lines changed

‎src/Init/Data/BitVec/Conversions.lean‎

Lines changed: 79 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,17 @@ Authors: Fady Adal
66
module
77

88
prelude
9-
public import Init.Data.BitVec.Basic
10-
public import Init.Data.BitVec.Folds
11-
public import Init.Data.List.Basic
129
public import Init.Data.Array.Basic
1310
public import Init.Data.Array.Lemmas
1411
public import Init.Data.Array.OfFn
12+
public import Init.Data.BitVec.Basic
13+
public import Init.Data.BitVec.Folds
14+
public import Init.Data.BitVec.Lemmas
15+
public import Init.Data.ByteArray.Basic
1516
public import Init.Data.Function
17+
public import Init.Data.List.Basic
1618
public import Init.Data.Vector.Basic
1719
public import Init.Data.Vector.Lemmas
18-
public import Init.Data.BitVec.Lemmas
1920

2021
public section
2122

@@ -665,4 +666,78 @@ theorem toVector_concat (x : BitVec w) (b : Bool) :
665666
theorem toList_toVectorLE (x : BitVec w) : x.toVectorLE.toList = x.toListLE := by
666667
simp [Vector.toList, toVectorLE]
667668

669+
/-! ## ByteArray conversions -/
670+
671+
/--
672+
Convert a bitvector to a byte array (little-endian).
673+
674+
The byte at index 0 contains bits 0-7 (the least significant byte).
675+
If the width is not a multiple of 8, the most significant bits of the last byte are zero-padded.
676+
677+
Examples:
678+
* `(0x1234#16).toBytesLE.data = #[0x34, 0x12]`
679+
* `(0xAB#8).toBytesLE.data = #[0xAB]`
680+
* `(0b101#3).toBytesLE.data = #[0b00000101]`
681+
-/
682+
def toBytesLE (x : BitVec w) : ByteArray :=
683+
let numBytes := (w + 7) / 8
684+
ByteArray.mk <| Array.ofFn fun (i : Fin numBytes) =>
685+
((x >>> (i.val * 8)).toNat &&& 0xFF).toUInt8
686+
687+
/--
688+
Convert a bitvector to a byte array (big-endian).
689+
690+
The byte at index 0 contains the most significant 8 bits.
691+
If the width is not a multiple of 8, the most significant bits of the first byte are zero-padded.
692+
693+
Examples:
694+
* `(0x1234#16).toBytesBE.data = #[0x12, 0x34]`
695+
* `(0xAB#8).toBytesBE.data = #[0xAB]`
696+
* `(0b101#3).toBytesBE.data = #[0b00000101]`
697+
-/
698+
def toBytesBE (x : BitVec w) : ByteArray :=
699+
let numBytes := (w + 7) / 8
700+
let xn := x.toNat
701+
ByteArray.mk <| Array.ofFn fun (i : Fin numBytes) =>
702+
let shift := (numBytes - 1 - i) * 8
703+
UInt8.ofNat ((xn >>> shift) &&& 0xFF)
704+
705+
@[local simp]
706+
theorem size_toBytesLE (x : BitVec w) : x.toBytesLE.size = (w + 7) / 8 := by
707+
simp [toBytesLE, ByteArray.size]
708+
709+
@[local simp]
710+
theorem size_toBytesBE (x : BitVec w) : x.toBytesBE.size = (w + 7) / 8 := by
711+
simp [toBytesBE, ByteArray.size]
712+
713+
/--
714+
Build a bitvector from a byte array (little-endian).
715+
716+
The byte at index 0 becomes bits 0-7 (the least significant byte).
717+
718+
Examples:
719+
* `ofBytesLE (ByteArray.mk #[0x34, 0x12]) = 0x1234#16`
720+
* `ofBytesLE (ByteArray.mk #[0xAB]) = 0xAB#8`
721+
* `ofBytesLE (ByteArray.mk #[0xFF, 0x0F]) = 0xFFF#16`
722+
-/
723+
def ofBytesLE (bytes : ByteArray) : BitVec (bytes.size * 8) :=
724+
let w := bytes.size * 8
725+
(List.range bytes.size).foldl (init := (0 : BitVec w)) fun acc i =>
726+
acc ||| (BitVec.ofNat w bytes[i]!.toNat <<< (i * 8))
727+
728+
/--
729+
Build a bitvector from a byte array (big-endian).
730+
731+
The byte at index 0 becomes the most significant 8 bits.
732+
733+
Examples:
734+
* `ofBytesBE (ByteArray.mk #[0x12, 0x34]) = 0x1234#16`
735+
* `ofBytesBE (ByteArray.mk #[0xAB]) = 0xAB#8`
736+
* `ofBytesBE (ByteArray.mk #[0x0F, 0xFF]) = 0xFFF#16`
737+
-/
738+
def ofBytesBE (bytes : ByteArray) : BitVec (bytes.size * 8) :=
739+
let w := bytes.size * 8
740+
(List.range bytes.size).foldl (init := (0 : BitVec w)) fun acc i =>
741+
acc ||| (BitVec.ofNat w bytes[i]!.toNat <<< (w - i * 8 - 8))
742+
668743
end BitVec

‎tests/lean/run/bitvec_bytearray.lean‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
/-
2+
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Fady Adal
5+
6+
Tests for BitVec ByteArray conversion operations.
7+
-/
8+
9+
open BitVec
10+
11+
/-! ## Basic conversions (standard widths) -/
12+
13+
-- 16-bit conversions
14+
#guard (0x1234#16).toBytesLE.data = #[0x34, 0x12]
15+
#guard (0x1234#16).toBytesBE.data = #[0x12, 0x34]
16+
17+
-- 8-bit conversions
18+
#guard (0xAB#8).toBytesLE.data = #[0xAB]
19+
#guard (0xAB#8).toBytesBE.data = #[0xAB]
20+
21+
-- 32-bit conversions
22+
#guard (0xDEADBEEF#32).toBytesLE.data = #[0xEF, 0xBE, 0xAD, 0xDE]
23+
#guard (0xDEADBEEF#32).toBytesBE.data = #[0xDE, 0xAD, 0xBE, 0xEF]
24+
25+
-- 64-bit conversions
26+
#guard (0x0123456789ABCDEF#64).toBytesLE.data = #[0xEF, 0xCD, 0xAB, 0x89, 0x67, 0x45, 0x23, 0x01]
27+
#guard (0x0123456789ABCDEF#64).toBytesBE.data = #[0x01, 0x23, 0x45, 0x67, 0x89, 0xAB, 0xCD, 0xEF]
28+
29+
/-! ## Non-multiple-of-8 widths -/
30+
31+
-- 3-bit value (pads to 1 byte)
32+
#guard (0b101#3).toBytesLE.data = #[0b00000101]
33+
#guard (0b101#3).toBytesBE.data = #[0b00000101]
34+
#guard (0b101#3).toBytesLE.size = 1
35+
#guard (0b101#3).toBytesBE.size = 1
36+
37+
-- 12-bit value (pads to 2 bytes)
38+
#guard (0xABC#12).toBytesLE.data = #[0xBC, 0x0A]
39+
#guard (0xABC#12).toBytesBE.data = #[0x0A, 0xBC]
40+
#guard (0xABC#12).toBytesLE.size = 2
41+
#guard (0xABC#12).toBytesBE.size = 2
42+
43+
-- 20-bit value (pads to 3 bytes)
44+
#guard (0x12345#20).toBytesLE.data = #[0x45, 0x23, 0x01]
45+
#guard (0x12345#20).toBytesBE.data = #[0x01, 0x23, 0x45]
46+
#guard (0x12345#20).toBytesLE.size = 3
47+
#guard (0x12345#20).toBytesBE.size = 3
48+
49+
/-! ## Edge cases -/
50+
51+
-- Empty bitvector (width 0)
52+
#guard (0#0).toBytesLE.size = 0
53+
#guard (0#0).toBytesBE.size = 0
54+
55+
-- Single bit
56+
#guard (0b1#1).toBytesLE.data = #[0x01]
57+
#guard (0b0#1).toBytesLE.data = #[0x00]
58+
#guard (0b1#1).toBytesLE.size = 1
59+
#guard (0b0#1).toBytesLE.size = 1
60+
61+
-- All zeros
62+
#guard (0x0000#16).toBytesLE.data = #[0x00, 0x00]
63+
#guard (0x0000#16).toBytesBE.data = #[0x00, 0x00]
64+
65+
-- All ones
66+
#guard (0xFFFF#16).toBytesLE.data = #[0xFF, 0xFF]
67+
#guard (0xFFFF#16).toBytesBE.data = #[0xFF, 0xFF]
68+
69+
/-! ## Size properties -/
70+
71+
#guard (0x12345678#32).toBytesLE.size = 4
72+
#guard (0x12345678#32).toBytesBE.size = 4
73+
#guard (0x123456#24).toBytesLE.size = 3
74+
#guard (0x123456#24).toBytesBE.size = 3
75+
#guard (0x12345#20).toBytesLE.size = 3 -- rounds up from 2.5 bytes
76+
77+
/-! ## Round trips (LE) -/
78+
79+
#guard ofBytesLE (ByteArray.mk #[0x34, 0x12]) = 0x1234#16
80+
#guard ofBytesLE (ByteArray.mk #[0xAB]) = 0xAB#8
81+
#guard ofBytesLE (ByteArray.mk #[0xEF, 0xBE, 0xAD, 0xDE]) = 0xDEADBEEF#32
82+
83+
#guard ofBytesLE (0x1234#16).toBytesLE = 0x1234#16
84+
#guard ofBytesLE (0xDEADBEEF#32).toBytesLE = 0xDEADBEEF#32
85+
#guard ofBytesLE (0xAB#8).toBytesLE = 0xAB#8
86+
87+
-- Non-multiple-of-8 round trips
88+
#guard ofBytesLE (0xABC#12).toBytesLE = 0xABC#16
89+
#guard ofBytesLE (0x12345#20).toBytesLE = 0x12345#24
90+
#guard ofBytesLE (0b101#3).toBytesLE = 0b101#8
91+
92+
/-! ## Round trips (BE) -/
93+
94+
#guard ofBytesBE (ByteArray.mk #[0x12, 0x34]) = 0x1234#16
95+
#guard ofBytesBE (ByteArray.mk #[0xAB]) = 0xAB#8
96+
#guard ofBytesBE (ByteArray.mk #[0xDE, 0xAD, 0xBE, 0xEF]) = 0xDEADBEEF#32
97+
98+
#guard ofBytesBE (0x1234#16).toBytesBE = 0x1234#16
99+
#guard ofBytesBE (0xDEADBEEF#32).toBytesBE = 0xDEADBEEF#32
100+
#guard ofBytesBE (0xAB#8).toBytesBE = 0xAB#8
101+
102+
-- Non-multiple-of-8 round trips
103+
#guard ofBytesBE (0xABC#12).toBytesBE = 0xABC#16
104+
#guard ofBytesBE (0x12345#20).toBytesBE = 0x12345#24
105+
#guard ofBytesBE (0b101#3).toBytesBE = 0b101#8
106+
107+
/-! ## Endianness differences -/
108+
109+
-- Single byte: LE and BE are the same
110+
#guard (0xFF#8).toBytesLE = (0xFF#8).toBytesBE
111+
#guard (0xAB#8).toBytesLE = (0xAB#8).toBytesBE
112+
113+
-- Multi-byte: LE and BE are different (unless palindrome)
114+
#guard (0x00FF#16).toBytesLE.data != (0x00FF#16).toBytesBE.data
115+
#guard (0x1234#16).toBytesLE.data != (0x1234#16).toBytesBE.data
116+
117+
118+
/-! ## Empty ByteArray handling -/
119+
120+
#guard ofBytesLE ByteArray.empty = 0#0
121+
122+
/-! ## Integration with other BitVec operations -/
123+
124+
-- Bitwise operations preserve round-trip
125+
#guard let x := 0b11001100#8
126+
let y := 0b10101010#8
127+
ofBytesLE ((x &&& y).toBytesLE) = x &&& y
128+
129+
#guard let x := 0x1234#16
130+
let y := 0x5678#16
131+
ofBytesLE ((x ||| y).toBytesLE) = x ||| y
132+
133+
-- Concatenation and ByteArray conversions
134+
#guard let x := 0xAB#8
135+
let y := 0xCD#8
136+
(x ++ y).toBytesLE.data = #[0xCD, 0xAB]
137+
138+
#guard let x := 0xAB#8
139+
let y := 0xCD#8
140+
(x ++ y).toBytesBE.data = #[0xAB, 0xCD]
141+
142+
/-! ## Large bitvectors -/
143+
144+
-- Size checks for large widths
145+
#guard let x := allOnes 256
146+
x.toBytesLE.size = 32
147+
148+
#guard let x := allOnes 256
149+
x.toBytesBE.size = 32

0 commit comments

Comments
 (0)