The byte codec is the proved one

AckBytes computes what AckCodec defines, reading with the spec's (not strict) parser, so AckCodec's theorems hold of the codec a client runs.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.foldr_pow (l : List ℕ) : List.foldr (fun (k s : ℕ) => 2 ^ k + s) 0 l = (List.map (fun (x : ℕ) => 2 ^ x) l).sum

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.bitmapByte_eq (idx : List ℕ) (j : ℕ) : bitmapByte idx j = AckCodec.bitmapByte idx j

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.bitmap_eq (idx : List ℕ) (w : ℕ) : bitmap idx w = AckCodec.bitmap idx w

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.nameMembers_eq (idx : List ℕ) : nameMembers idx = AckCodec.nameMembers idx

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.ascending_iff (l : List ℕ) : ascending l = true ↔ List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) l

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.setBits_eq (naming : List ℕ) : setBits naming = AckCodec.setBits naming

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.readMembers_eq (naming : List ℕ) (count : ℕ) : readMembers naming count = AckCodec.readMembers false naming count

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.chunks_eq (v : ℕ) (l : List ℕ) (n : ℕ) : chunks v l n = AckCodec.chunks v l n

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.le_eq (k n : ℕ) : le k n = AckCodec.le k n

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.fromLE_eq (l : List ℕ) : fromLE l = AckCodec.fromLE l

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.encodeValues_eq (acks : List (ℕ × List ℕ)) : encodeValues acks = AckCodec.encode acks

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decodeValues_eq (v : ℕ) (field : List ℕ) : decodeValues v field = AckCodec.decode false v field

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.encodeNat_eq (acks : List (ℕ × ℕ)) : encodeNat acks = AckCodec.encodeIdx64 acks

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decodeNat_eq (field : List ℕ) : decodeNat field = AckCodec.decodeIdx64 false field

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decodeNat_encodeNat {acks : List (ℕ × ℕ)} (h : AckCodec.WFIdx64 acks) : decodeNat (encodeNat acks) = some acks

Decoding undoes encoding, for numbers.