Reading back what is written

Each item written by Cbor reads back as itself, followed by whatever came after it.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.foldl_be_aux (k n acc : ℕ) : n < 256 ^ k → List.foldl (fun (n : ℕ) (b : UInt8) => n * 256 + b.toNat) acc (be k n) = acc * 256 ^ k + n

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.fromBE_be (k n : ℕ) (h : n < 256 ^ k) : fromBE (be k n) = n

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.length_be (k n : ℕ) : (be k n).length = k

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.toNat_byte {x : ℕ} (h : x < 256) : x.toUInt8.toNat = x

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readHeader_long (b k m n : ℕ) (rest : List UInt8) (hb : b = m * 32 + 24 + k) (hk : k < 4) (hm : m < 8) (hn : n < 256 ^ 2 ^ k) : readHeader (b.toUInt8 :: (be (2 ^ k) n ++ rest)) = some (m, n, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readHeader_header (m n : ℕ) (rest : List UInt8) (hm : m < 8) (hn : n < 2 ^ 64) : readHeader (header m n ++ rest) = some (m, n, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readUInt_uint (n : ℕ) (rest : List UInt8) (hn : n < 2 ^ 64) : readUInt (uint n ++ rest) = some (n, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readString_header (m : ℕ) (b rest : List UInt8) (hm : m < 8) (hb : b.length < 2 ^ 64) : readString m (header m b.length ++ b ++ rest) = some (b, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readBytes_bytes (b rest : List UInt8) (hb : b.length < 2 ^ 64) : readBytes (bytes b ++ rest) = some (b, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.fromUTF8_toByteArray (s : String) : String.fromUTF8? s.toByteArray = some s

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readText_text (s : String) (rest : List UInt8) (hs : s.utf8ByteSize < 2 ^ 64) : readText (text s ++ rest) = some (s, rest)