Bits.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1/-!
2# Format: bits, bytes and numbers
3
4Heap-free, pointer-free vocabulary for the data format of `docs/spec/format/README.md`
5(RFC 1950, 1951, 1952). Everything here is total and structurally recursive.
6
7The reader functions return `none` when the input is too short. A reader that
8succeeds returns the value and the bits that are left.
9-/
10
11namespace ZlibF.Spec
12
13/-- The 8 bits of a byte, least significant bit first.
14RFC 1951, 3.1.1 and `F-bit-order`: data elements are packed starting at the
15least significant bit of each byte. -/
16def byteBits (b : UInt8) : List Bool :=
17  (List.range 8).map fun i => b.toNat.testBit i
18
19/-- The bit sequence of a byte sequence, first bit first (`F-bit-order`). -/
20def bytesToBits (bs : List UInt8) : List Bool :=
21  bs.flatMap byteBits
22
23/-- `readBits n inp` reads an `n`-bit number packed least significant bit first
24(RFC 1951, 3.1.1; `F-bit-order`: lengths, extra bits, `HLIT`, `LEN`, ...).
25It is NOT used for Huffman codes, which are packed most significant bit first. -/
26def readBits : Nat → List Bool → Option (Nat × List Bool)
27  | 0, inp => some (0, inp)
28  | _ + 1, [] => none
29  | n + 1, b :: r =>
30    match readBits n r with
31    | none => none
32    | some (v, r') => some ((if b then 1 else 0) + 2 * v, r')
33
34/-- `readBytes n inp` reads `n` whole bytes (8 bits each, least significant bit
35first), as the body of a stored block (RFC 1951, 3.2.4). -/
36def readBytes : Nat → List Bool → Option (List UInt8 × List Bool)
37  | 0, inp => some ([], inp)
38  | n + 1, inp =>
39    match readBits 8 inp with
40    | none => none
41    | some (v, r) =>
42      match readBytes n r with
43      | none => none
44      | some (bs, r') => some (v.toUInt8 :: bs, r')
45
46/-- `readNats w n inp` reads `n` numbers of `w` bits each (least significant bit first). -/
47def readNats (w : Nat) : Nat → List Bool → Option (List Nat × List Bool)
48  | 0, inp => some ([], inp)
49  | n + 1, inp =>
50    match readBits w inp with
51    | none => none
52    | some (v, r) =>
53      match readNats w n r with
54      | none => none
55      | some (vs, r') => some (v :: vs, r')
56
57/-- The `len`-bit representation of `v`, MOST significant bit first. This is the
58order in which the bits of a Huffman code are read from the stream
59(RFC 1951, 3.1.1; `F-bit-order`). -/
60def natToBitsMSB (len v : Nat) : List Bool :=
61  (List.range len).map fun i => v.testBit (len - 1 - i)
62
63/-- Big-endian 4 bytes (zlib trailer and dictionary id, RFC 1950, 2.2). -/
64def be32 (n : Nat) : List UInt8 :=
65  [(n / 2 ^ 24 % 256).toUInt8, (n / 2 ^ 16 % 256).toUInt8, (n / 2 ^ 8 % 256).toUInt8, (n % 256).toUInt8]
66
67/-- Little-endian 4 bytes (gzip trailer, RFC 1952, 2.3.1). -/
68def le32 (n : Nat) : List UInt8 :=
69  [(n % 256).toUInt8, (n / 2 ^ 8 % 256).toUInt8, (n / 2 ^ 16 % 256).toUInt8, (n / 2 ^ 24 % 256).toUInt8]
70
71/-- Little-endian 2 bytes (gzip `XLEN` and header CRC, RFC 1952, 2.3.1). -/
72def le16 (n : Nat) : List UInt8 :=
73  [(n % 256).toUInt8, (n / 2 ^ 8 % 256).toUInt8]
74
75end ZlibF.Spec