Fixed-width packed words

A fixed tuple of bounded words stores an initial segment of a bit stream. Reading a field constrains its entire value, including all bits outside the specified width.

Main definitions

• Cslib.BitString.packRadix: bounded fields in a common radix.
• Cslib.BitString.packWords: split a bit stream into a fixed tuple of words.
• Cslib.BitString.readPackedBit: read one bit of a fixed tuple of words by its address.
• Cslib.BitString.readPackedField: read a bounded-width field across word boundaries.

Main results

• Cslib.BitString.packRadix_field: exact radix-field decoding.
• Cslib.BitString.readPackedField_packWords: exact field decoding.
• Cslib.BitString.readPackedField_fields: decoding fixed-width consecutive fields.

def Cslib.BitString.packWords (f : ℕ → Bool) (h B : ℕ) (r : Fin B) : ℕ

Pack a bit stream into B words of h bits each.

theorem Cslib.BitString.packWords_lt (f : ℕ → Bool) (h B : ℕ) (r : Fin B) : packWords f h B r < 2 ^ h

Each packed word is below 2 ^ h.

def Cslib.BitString.readPackedBit {B : ℕ} (h : ℕ) (w : Fin B → ℕ) (a : ℕ) : Bool

Read one bit of a fixed tuple; unused addresses are false.

def Cslib.BitString.readPackedField {B : ℕ} (h : ℕ) (w : Fin B → ℕ) (a s : ℕ) : ℕ

Decode exactly s bits starting at address a, with every higher bit zero.

theorem Cslib.BitString.readPackedField_lt {B : ℕ} (h : ℕ) (w : Fin B → ℕ) (a s : ℕ) : readPackedField h w a s < 2 ^ s

A field of width s is below 2 ^ s.

theorem Cslib.BitString.readPackedField_testBit {B : ℕ} (h : ℕ) (w : Fin B → ℕ) (a s b : ℕ) : (readPackedField h w a s).testBit b = true ↔ b < s ∧ ∃ (r : Fin B) (t : Fin h), ↑r * h + ↑t = a + b ∧ (w r).testBit ↑t = true

Bit b of the field of width s at address a is set exactly when b < s and the packed bit at address a + b, bit t of word r with r * h + t = a + b, is set.

theorem Cslib.BitString.readPackedBit_packWords (f : ℕ → Bool) {h B a : ℕ} (ha : a < B * h) : readPackedBit h (packWords f h B) a = f a

Every bit below the total capacity is recovered from the packed tuple.

theorem Cslib.BitString.readPackedField_packWords (f : ℕ → Bool) {h B a s z : ℕ} (ha : a + s ≤ B * h) (hz : z < 2 ^ s) (hf : ∀ b < s, f (a + b) = z.testBit b) : readPackedField h (packWords f h B) a s = z

A fitting field is recovered exactly, including high zero bits.

theorem Cslib.BitString.readPackedField_fields (v : ℕ → ℕ) {h B q s : ℕ} (hs : 0 < s) (ha : q * s + s ≤ B * h) (hv : v q < 2 ^ s) : readPackedField h (packWords (fun (a : ℕ) => (v (a / s)).testBit (a % s)) h B) (q * s) s = v q

Consecutive fixed-width fields can be packed and decoded without overlap.

def Cslib.BitString.packRadix (base n : ℕ) (f : ℕ → ℕ) : ℕ

Pack n radix-base fields, least significant field first.

theorem Cslib.BitString.packRadix_lt {base n : ℕ} (f : ℕ → ℕ) (hf : ∀ i < n, f i < base) : packRadix base n f < base ^ n

Bounded fields fit the total radix capacity, including the empty tuple.

theorem Cslib.BitString.packRadix_field {base n i : ℕ} (hb : 0 < base) (f : ℕ → ℕ) (hf : ∀ j < n, f j < base) (hi : i < n) : packRadix base n f / base ^ i % base = f i

Reading a radix field recovers its entire value, with no contributions from other fields.