structure Serializer : Type

• bytes : ByteArray
• curByte : UInt8
• bitMask : UInt8

def instDecidableEqSerializer.decEq (x✝ x✝¹ : Serializer) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqSerializer.decEq { bytes := a, curByte := a_1, bitMask := a_2 } { bytes := b, curByte := b_1, bitMask := b_2 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ if h : a_2 = b_2 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqSerializer : DecidableEq Serializer

Equations

• instDecidableEqSerializer = instDecidableEqSerializer.decEq

@[reducible, inline]

abbrev Serializer.Ser (α : Type) : Type

Equations

• Serializer.Ser = StateM Serializer

def Serializer.empty : Serializer

Equations

• Serializer.empty = { bytes := ∅, curByte := 0, bitMask := 1 }

@[instance_reducible]

instance Serializer.instEmptyCollection : EmptyCollection Serializer

Equations

• Serializer.instEmptyCollection = { emptyCollection := Serializer.empty }

theorem Serializer.empty_def : ∅ = empty

def Serializer.flush' : Ser Unit

Equations

• Serializer.flush' = modify fun (s : Serializer) => { bytes := s.bytes.push s.curByte, curByte := 0, bitMask := 1 }

def Serializer.flush : Ser Unit

Equations

• Serializer.flush = do let __do_lift ← get bif __do_lift.bitMask != 0 then pure () else Serializer.flush'

def Serializer.finish : Ser Unit

Equations

• Serializer.finish = do let __do_lift ← get bif __do_lift.bitMask == 1 then pure () else Serializer.flush'

def Serializer.writeBit' (b : Bit) : Ser Unit

Equations

• Serializer.writeBit' b = modify fun (s : Serializer) => { bytes := s.bytes, curByte := match b with | Bit.B₀ => s.curByte | Bit.B₁ => s.curByte ||| s.bitMask, bitMask := s.bitMask <<< 1 }

def Serializer.writeBit (b : Bit) : Ser Unit

Equations

• Serializer.writeBit b = do Serializer.writeBit' b Serializer.flush

def Serializer.writeBits (bs : List Bit) : Ser Unit

Equations

• Serializer.writeBits bs = bs.forM Serializer.writeBit

def Serializer.getOutput : Ser ByteArray

Equations

• Serializer.getOutput = do Serializer.finish gets fun (x : Serializer) => x.bytes

def Serializer.ofBits (bs : List Bit) : Serializer

Equations

• Serializer.ofBits bs = (StateT.run (Serializer.writeBits bs) ∅).2

@[simp]

theorem Serializer.writeBits_nil : writeBits [] = pure ()

@[simp]

theorem Serializer.finish_empty : StateT.run finish ∅ = ((), ∅)

@[simp]

theorem Serializer.getOutput_empty : StateT.run getOutput ∅ = (∅, ∅)

@[simp]

theorem Serializer.ofBits_nil : ofBits [] = ∅

@[simp]

theorem Serializer.flush_empty : StateT.run flush ∅ = ((), ∅)

@[simp]

theorem Serializer.writeBits_cons {b : Bit} {bs : List Bit} : writeBits (b :: bs) = do writeBit b writeBits bs

@[simp]

theorem Serializer.writeBits_append {bs₁ bs₂ : List Bit} : writeBits (bs₁ ++ bs₂) = do writeBits bs₁ writeBits bs₂

@[simp]

theorem Serializer.flush_flush' {s : Serializer} : StateT.run flush (StateT.run flush' s).2 = StateT.run flush' s

@[simp]

theorem Serializer.flush_flush {s : Serializer} : StateT.run flush (StateT.run flush s).2 = StateT.run flush s

@[simp]

theorem Serializer.finish_finish {s : Serializer} : StateT.run finish (StateT.run finish s).2 = StateT.run finish s

@[simp]

theorem Serializer.flush_ofBits {bs : List Bit} : StateT.run flush (ofBits bs) = ((), ofBits bs)

@[simp]

theorem Serializer.bytes_empty : ∅.bytes = ∅

@[simp]

theorem Serializer.ofBits_append {bs₁ bs₂ : List Bit} : ofBits (bs₁ ++ bs₂) = (StateT.run (writeBits bs₂) (ofBits bs₁)).2

@[simp]

theorem Serializer.bitMask_empty : ∅.bitMask = 1

theorem Serializer.writeBit_eq_of_lt {s : Serializer} {b : Bit} (n : ℕ) (h₁ : s.bitMask = 1 <<< UInt8.ofNat n) (h₂ : n ≤ 6) : StateT.run (writeBit b) s = ((), { bytes := s.bytes, curByte := s.curByte ||| UInt8.ofBit b <<< UInt8.ofNat n, bitMask := 1 <<< UInt8.ofNat (n + 1) })

theorem Serializer.writeBits_eq_of_lt {s : Serializer} {bs : List Bit} (n : ℕ) (h₁ : s.bitMask = 1 <<< UInt8.ofNat n) (h₂ : n + bs.length ≤ 7) : StateT.run (writeBits bs) s = ((), { bytes := s.bytes, curByte := s.curByte ||| UInt8.ofBits bs <<< UInt8.ofNat n, bitMask := 1 <<< UInt8.ofNat (n + bs.length) })

theorem Serializer.fst_getOutput_ofBits_aux₁ {bs : List Bit} (h : bs ≠ []) (h₁ : bs.length < 8) : (StateT.run getOutput (ofBits bs)).1 = ByteArray.ofBits bs