max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add UInt64 unpackings

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-07-22 12:56:08 -07:00 • committed by Sebastian Ullrich
parent b3d9e90695
commit 776a0c71aa
3 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/Init/Data/ByteArray/Basic.lean
View file

@ -85,3 +85,27 @@ def List.toByteArray (bs : List UInt8) : ByteArray :=
loop bs ByteArray.empty
instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
assert! bs.size == 8
(bs.get! 0).toUInt64 <<< 0x38 |||
(bs.get! 1).toUInt64 <<< 0x30 |||
(bs.get! 2).toUInt64 <<< 0x28 |||
(bs.get! 3).toUInt64 <<< 0x20 |||
(bs.get! 4).toUInt64 <<< 0x18 |||
(bs.get! 5).toUInt64 <<< 0x10 |||
(bs.get! 6).toUInt64 <<< 0x8 |||
(bs.get! 7).toUInt64
/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
assert! bs.size == 8
(bs.get! 7).toUInt64 <<< 0x38 |||
(bs.get! 6).toUInt64 <<< 0x30 |||
(bs.get! 5).toUInt64 <<< 0x28 |||
(bs.get! 4).toUInt64 <<< 0x20 |||
(bs.get! 3).toUInt64 <<< 0x18 |||
(bs.get! 2).toUInt64 <<< 0x10 |||
(bs.get! 1).toUInt64 <<< 0x8 |||
(bs.get! 0).toUInt64

3
tests/lean/bytearray.lean
View file

@ -15,3 +15,6 @@ IO.println (bs.extract 1 3);
pure ()
#eval tst
#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64LE! == 0x1122334455667788
#eval [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88].toByteArray.toUInt64BE! == 0x8877665544332211

2
tests/lean/bytearray.lean.expected.out
View file

@ -5,3 +5,5 @@
4
[1, 20, 3, 4, 1, 20, 3, 4]
[20, 3]
true
true