Skip to content

Commit eaacc6f

Browse files
fgdoraisfgdorais
committed
feat: add basic byte order support
1 parent bde4e24 commit eaacc6f

2 files changed

Lines changed: 150 additions & 0 deletions

File tree

‎Batteries.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ public import Batteries.Data.BinaryHeap
2727
public import Batteries.Data.BinomialHeap
2828
public import Batteries.Data.BitVec
2929
public import Batteries.Data.ByteArray
30+
public import Batteries.Data.ByteOrder
3031
public import Batteries.Data.ByteSlice
3132
public import Batteries.Data.Char
3233
public import Batteries.Data.DList

‎Batteries/Data/ByteOrder.lean‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
/-
2+
Copyright (c) 2026 François G. Dorais. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: François G. Dorais
5+
-/
6+
7+
module
8+
9+
/-! # Byte Order
10+
11+
Basic utilities to handle byte order for scalar types.
12+
-/
13+
14+
set_option linter.missingDocs false in
15+
/-- Byte ordering for scalar types.
16+
17+
* `platform`: byte ordering of the host platform
18+
* `bigEndian`: scalar types are stored most significant byte first
19+
* `littleEndian`: scalar types are stored least significant byte first
20+
21+
The host platform is expected to be either big endian or little endian. There are rare platforms
22+
that are mixed endian; these platforms are not well supported.
23+
-/
24+
public inductive System.ByteOrder
25+
| public platform
26+
| public bigEndian
27+
| public littleEndian
28+
deriving Inhabited, DecidableEq, Repr
29+
attribute [inherit_doc System.ByteOrder] System.ByteOrder.platform
30+
attribute [inherit_doc System.ByteOrder] System.ByteOrder.bigEndian
31+
attribute [inherit_doc System.ByteOrder] System.ByteOrder.littleEndian
32+
33+
/-- Determine the byte order of the host platform.
34+
35+
The host platform is expected to be `bigEndian` or `littleEndian`. In the rare
36+
event that the platform is mixed endian, `System.byteOrder.platform` is returned.
37+
-/
38+
public def System.Platform.byteOrder : System.ByteOrder :=
39+
if ntohl 0x01020304 = 0x01020304 then
40+
.bigEndian
41+
else if ntohl 0x01020304 = 0x04030201 then
42+
.littleEndian
43+
else
44+
.platform
45+
where
46+
/-- The C function `ntohl` converts a `UInt32` in network byte order (big endian) to a
47+
`UInt32` in host byte order. -/
48+
@[extern "ntohl"] ntohl : UInt32 → UInt32 := id
49+
50+
/-- Swap the bytes of a `UInt16` scalar. -/
51+
@[expose, inline]
52+
public def UInt16.byteswap (x : UInt16) : UInt16 :=
53+
x <<< 8 ||| x >>> 8
54+
55+
/-- Swap the bytes of a `UInt32` scalar. -/
56+
@[expose, inline]
57+
public def UInt32.byteswap (x : UInt32) : UInt32 :=
58+
let x := x <<< 16 ||| x >>> 16
59+
(x &&& 0xFF00FF00) >>> 8 ||| (x <<< 8 &&& 0xFF00FF00)
60+
61+
/-- Swap the byte of a `UInt64` scalar. -/
62+
@[expose, inline]
63+
public def UInt64.byteswap (x : UInt64) : UInt64 :=
64+
let x := x <<< 32 ||| x >>> 32
65+
let x := (x &&& 0xFFFF0000FFFF0000) >>> 16 ||| (x <<< 16 &&& 0xFFFF0000FFFF0000)
66+
(x &&& 0xFF00FF00FF00FF00) >>> 8 ||| (x <<< 8 &&& 0xFF00FF00FF00FF00)
67+
68+
/-- Convert to `endian` byte ordering. -/
69+
@[expose, inline]
70+
public def UInt16.toByteOrder (x : UInt16) (endian : System.ByteOrder) : UInt16 :=
71+
if endian = System.Platform.byteOrder then x else x.byteswap
72+
73+
/-- Convert to `endian` byte ordering. -/
74+
@[expose, inline]
75+
public def UInt32.toByteOrder (x : UInt32) (endian : System.ByteOrder) : UInt32 :=
76+
if endian = System.Platform.byteOrder then x else x.byteswap
77+
78+
/-- Convert to `endian` byte ordering. -/
79+
@[expose, inline]
80+
public def UInt64.toByteOrder (x : UInt64) (endian : System.ByteOrder) : UInt64 :=
81+
if endian = System.Platform.byteOrder then x else x.byteswap
82+
83+
/-- Convert a byte array of size 2 into a `UInt16` scalar in platform byte order. -/
84+
@[expose, extern c inline "(uint16_t*)lean_sarray_cptr(#1)[0]"]
85+
public def UInt16.ofByteArray (b : @& ByteArray) (h : b.size = 2) : UInt16 :=
86+
if System.Platform.byteOrder = .littleEndian then
87+
b[1].toUInt16 <<< 8 ||| b[0].toUInt16
88+
else -- default to big endian even if platform is mixed endian
89+
b[0].toUInt16 <<< 8 ||| b[1].toUInt16
90+
91+
/-- Convert a `UInt16` scalar into a byte array in platform byte order. -/
92+
@[expose, extern c inline "lean_alloc_sarray(1, 2, 2);\n(uint16_t*)lean_sarray_cptr(#1)[0] = #2"]
93+
public def UInt16.toByteArray (x : UInt16) : ByteArray :=
94+
if System.Platform.byteOrder = .littleEndian then
95+
.mk #[x.toUInt8, (x >>> 8).toUInt8]
96+
else -- default to big endian even if platform is mixed endian
97+
.mk #[(x >>> 8).toUInt8, x.toUInt8]
98+
99+
@[simp, grind =]
100+
public theorem UInt16.size_toByteArray (x : UInt16) : x.toByteArray.size = 2 := by
101+
cases _ : System.Platform.byteOrder <;> (simp only [toByteArray, *]; rfl)
102+
103+
/-- Convert a byte array of size 4 into a `UInt32` scalar in platform byte order. -/
104+
@[expose, extern c inline "(uint32_t*)lean_sarray_cptr(#1)[0]"]
105+
public def UInt32.ofByteArray (b : @& ByteArray) (h : b.size = 4) : UInt32 :=
106+
if System.Platform.byteOrder = .littleEndian then
107+
((b[3].toUInt32 <<< 8 ||| b[2].toUInt32) <<< 8 ||| b[1].toUInt32) <<< 8 ||| b[0].toUInt32
108+
else -- default to big endian even if platform is mixed endian
109+
((b[0].toUInt32 <<< 8 ||| b[1].toUInt32) <<< 8 ||| b[2].toUInt32) <<< 8 ||| b[3].toUInt32
110+
111+
/-- Convert a `UInt32` scalar into a byte array in platform byte order. -/
112+
@[expose, extern c inline "lean_alloc_sarray(1, 4, 4);\n(uint32_t*)lean_sarray_cptr(#1)[0] = #2"]
113+
public def UInt32.toByteArray (x : UInt32) : ByteArray :=
114+
if System.Platform.byteOrder = .littleEndian then
115+
.mk #[x.toUInt8, (x >>> 8).toUInt8, (x >>> 16).toUInt8, (x >>> 24).toUInt8]
116+
else -- default to big endian even if platform is mixed endian
117+
.mk #[(x >>> 24).toUInt8, (x >>> 16).toUInt8, (x >>> 8).toUInt8, x.toUInt8]
118+
119+
@[simp, grind =]
120+
public theorem UInt32.size_toByteArray (x : UInt32) : x.toByteArray.size = 4 := by
121+
cases _ : System.Platform.byteOrder <;> (simp only [toByteArray, *]; rfl)
122+
123+
/-- Convert a byte array of size 8 into a `UInt64` scalar in platform byte order. -/
124+
@[expose, extern c inline "(uint64_t*)lean_sarray_cptr(#1)[0]"]
125+
public def UInt64.ofByteArray (b : @& ByteArray) (h : b.size = 8) : UInt64 :=
126+
if System.Platform.byteOrder = .littleEndian then
127+
((((((b[7].toUInt64 <<< 8 ||| b[6].toUInt64) <<< 8
128+
||| b[5].toUInt64) <<< 8 ||| b[4].toUInt64) <<< 8
129+
||| b[3].toUInt64) <<< 8 ||| b[2].toUInt64) <<< 8
130+
||| b[1].toUInt64) <<< 8 ||| b[0].toUInt64
131+
else -- default to big endian even if platform is mixed endian
132+
((((((b[0].toUInt64 <<< 8 ||| b[1].toUInt64) <<< 8
133+
||| b[2].toUInt64) <<< 8 ||| b[3].toUInt64) <<< 8
134+
||| b[4].toUInt64) <<< 8 ||| b[5].toUInt64) <<< 8
135+
||| b[6].toUInt64) <<< 8 ||| b[7].toUInt64
136+
137+
/-- Convert a `UInt64` scalar into a byte array in platform byte order. -/
138+
@[expose, extern c inline "lean_alloc_sarray(1, 8, 8);\n(uint64_t*)lean_sarray_cptr(#1)[0] = #2"]
139+
public def UInt64.toByteArray (x : UInt64) : ByteArray :=
140+
if System.Platform.byteOrder = .littleEndian then
141+
.mk #[x.toUInt8, (x >>> 8).toUInt8, (x >>> 16).toUInt8, (x >>> 24).toUInt8,
142+
(x >>> 32).toUInt8, (x >>> 40).toUInt8, (x >>> 48).toUInt8, (x >>> 56).toUInt8]
143+
else -- default to big endian even if platform is mixed endian
144+
.mk #[(x >>> 56).toUInt8, (x >>> 48).toUInt8, (x >>> 56).toUInt8, (x >>> 32).toUInt8,
145+
(x >>> 24).toUInt8, (x >>> 16).toUInt8, (x >>> 8).toUInt8, x.toUInt8]
146+
147+
@[simp, grind =]
148+
public theorem UInt64.size_toByteArray (x : UInt64) : x.toByteArray.size = 8 := by
149+
cases _ : System.Platform.byteOrder <;> (simp only [toByteArray, *]; rfl)

0 commit comments

Comments
 (0)