A message reads back as written

decode_encode: every message this client writes, read back, is the message it wrote.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF : Field → Prop

A field this client writes and reads back.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field.version n) = (n < 2 ^ 64)
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field.hash b) = (b.size < 2 ^ 64)
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field.msgType n) = (n < 2 ^ 64)
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field.text s) = (s.utf8ByteSize < 2 ^ 64)
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field.other key raw) = False
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field.acks b) = (b.size < 2 ^ 64)
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field.numbers b) = (b.size < 2 ^ 64)
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.FieldWF (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field.introducedAt b) = (b.size < 2 ^ 64)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.bytes_size (b : ByteArray) : b.data.toList.length = b.size

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readByteArray_bytes (b : ByteArray) (rest : List UInt8) (hb : b.size < 2 ^ 64) : readByteArray (Cbor.bytes b.data.toList ++ rest) = some (b, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.nullable_some {α : Type} (read : List UInt8 → Option (α × List UInt8)) (l : List UInt8) (a : α) (rest : List UInt8) (h : read l = some (a, rest)) (hn : Cbor.isNull l = false) : nullable read l = some (some a, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.isNull_cons (x : ℕ) (r : List UInt8) (hx : x < 246) : Cbor.isNull (x.toUInt8 :: r) = false

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.isNull_header (m n : ℕ) (rest : List UInt8) (hm : m < 7) : Cbor.isNull (Cbor.header m n ++ rest) = false

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.byteArray_eta (b : ByteArray) : { data := b.data.toList.toArray } = b

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readIntro_encodeIntro (i : Introduction) (rest : List UInt8) (hn : 1 ≤ i.name.length ∧ i.name.length ≤ maxNameChars ∧ i.readCap.size = readCapSize ∧ i.name.utf8ByteSize < 2 ^ 64) : readIntro (encodeIntro i ++ rest) = some (i, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readField_encodeField (f : Field) (hf : FieldWF f) (rest : List UInt8) : readField (encodeField f ++ rest) = some (some f, rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readFields_flatMap (fs : List Field) (acc : Acc) (rest : List UInt8) : (∀ f ∈ fs, FieldWF f) → readFields fs.length acc (List.flatMap encodeField fs ++ rest) = some (List.foldl Acc.add acc fs, rest)

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.WF (g : Gcm) : Prop

A message this client writes and reads back as it was.

• version : g.version ≤ currentVersion
• hash : g.membershipHash.size = hashSize
• msgType : g.msgType ≤ MsgType.control
• text (s : String) : s ∈ g.text → s.utf8ByteSize < 2 ^ 64
• intro (i : Introduction) : i ∈ g.introduction → 1 ≤ i.name.length ∧ i.name.length ≤ maxNameChars ∧ i.readCap.size = readCapSize ∧ i.name.utf8ByteSize < 2 ^ 64
• other : g.other = []
• acks (b : ByteArray) : b ∈ g.acks → b.size < 2 ^ 64
• numbers (b : ByteArray) : b ∈ g.numbers → b.size < 2 ^ 64
• introducedAt (b : ByteArray) : b ∈ g.introducedAt → b.size < 2 ^ 64

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.fields_wf {g : Gcm} (h : WF g) (f : Field) : f ∈ fields g → FieldWF f

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.finish_fields {g : Gcm} (h : WF g) : (List.foldl Acc.add { } (fields g)).finish = some g

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.decode_encode {g : Gcm} (h : WF g) : decode (encode g) = some g

Decoding undoes encoding.