Group chat messages on the wire

A box of a member's stream holds F followed by the CBOR map of one GroupChatMessage, as katzenqt's models.py writes it: its fields in declaration order, absent ones left out. A message too long for a box goes to a substream of C chunks ending in an F chunk, announced in the member's stream by an I chunk carrying the substream's read cap.

Gcm holds what this client reads of a message. The fields between introduction and acks (file_upload, who, reply_who, tally) are kept as their CBOR, unread; keys katzenqt does not know are dropped, as its decoder drops them.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.currentVersion : Nat

The newest message version this client reads; it writes no other.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.currentVersion = 3

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.hashSize : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.hashSize = 32

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readCapSize : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readCapSize = 136

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.maxNameChars : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.maxNameChars = 30

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.text : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.text = 0

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.introduction : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.introduction = 1

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.fileUpload : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.fileUpload = 2

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.who : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.who = 3

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.replyWho : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.replyWho = 4

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.control : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.MsgType.control = 10

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.otherKeys : List String

The fields this client keeps without reading, in the order they are written.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.otherKeys = ["file_upload", "who", "reply_who", "tally"]

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Gcm : Type

• version : Nat
• membershipHash : ByteArray
• msgType : Nat
• text : Option String
• introduction : Option Introduction
• other : List (String × List UInt8)
• acks : Option ByteArray
• numbers : Option ByteArray
• introducedAt : Option ByteArray

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instDecidableEqGcm : DecidableEq Gcm

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instDecidableEqGcm = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instDecidableEqGcm.decEq

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instDecidableEqGcm.decEq (x✝ x✝¹ : Gcm) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instInhabitedGcm : Inhabited Gcm

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instInhabitedGcm = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instInhabitedGcm.default }

Encoding

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Field : Type

• version (n : Nat) : Field
• hash (b : ByteArray) : Field
• msgType (n : Nat) : Field
• text (s : String) : Field
• intro (i : Introduction) : Field
• other (key : String) (raw : List UInt8) : Field
• acks (b : ByteArray) : Field
• numbers (b : ByteArray) : Field
• introducedAt (b : ByteArray) : Field

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.fields (g : Gcm) : List Field

A message's fields, in the order they are written.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.encodeIntro (i : Introduction) : List UInt8

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.encodeField : Field → List UInt8

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.encodeList (g : Gcm) : List UInt8

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.encode (g : Gcm) : ByteArray

The CBOR of g.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.encode g = { data := (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.encodeList g).toArray }

Decoding

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.introEntries : Nat → Option String × Option ByteArray → List UInt8 → Option ((Option String × Option ByteArray) × List UInt8)

An introduction map's entries: display_name and read_cap, in either order.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.introEntries 0 x✝¹ x✝ = some (x✝¹, x✝)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readIntro (l : List UInt8) : Option (Introduction × List UInt8)

An introduction katzenqt accepts: a name of 1 to 30 characters and a whole read cap.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.nullable {α : Type} (read : List UInt8 → Option (α × List UInt8)) (l : List UInt8) : Option (Option α × List UInt8)

Read a value that may be null, which counts as absent.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readByteArray (l : List UInt8) : Option (ByteArray × List UInt8)

Equations

• One or more equations did not get rendered due to their size.

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Acc : Type

What the fields read so far say.

• version : Option Nat
• hash : Option ByteArray
• msgType : Option Nat
• text : Option String
• introduction : Option Introduction
• other : List (String × List UInt8)
• acks : Option ByteArray
• numbers : Option ByteArray
• introducedAt : Option ByteArray

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readField (l : List UInt8) : Option (Option Field × List UInt8)

One map entry: a key this client reads and its value, or none for an entry it passes over.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Acc.add (a : Acc) : Field → Acc

Take in one field; a repeated key keeps its last value, as a Python dict does.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readFields : Nat → Acc → List UInt8 → Option (Acc × List UInt8)

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.readFields 0 x✝¹ x✝ = some (x✝¹, x✝)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.inferType (a : Acc) : Nat

The type of a message written before msg_type was, from the field it carries.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Acc.finish (a : Acc) : Option Gcm

A message from the fields read, when katzenqt would accept it.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.decodeList (l : List UInt8) : Option Gcm

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.decode (b : ByteArray) : Option Gcm

The message a CBOR map holds, or none when katzenqt would refuse it. What follows the map is ignored, as cbor2.loads ignores it.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.decode b = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.decodeList b.data.toList

Boxes

inductive Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.Chunk : Type

What a box of a stream holds.

• final (cbor : ByteArray) : Chunk

  The last or only chunk of a message.

• continued (part : ByteArray) : Chunk

  A chunk of a message that continues in the next box.

• indirection (total : Option Nat) (readCap : ByteArray) : Chunk

  Where a long message is: the substream's read cap, and how many chunks it holds when the writer said.

• unknown : Chunk

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instInhabitedChunk : Inhabited Chunk

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instInhabitedChunk = { default := Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.instInhabitedChunk.default }

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.frame (cbor : ByteArray) : ByteArray

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.frame cbor = { data := #['F'.toNat.toUInt8] } ++ cbor

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.unframe (box : ByteArray) : Chunk

Equations

• One or more equations did not get rendered due to their size.

Between a message and what a member reads of it

As katzenqt's GcmCodec: a content message's whole CBOR travels as its content; control messages and introductions are written afresh.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.sentinel : ByteArray

The hash a control message or an introduction carries in place of the membership hash.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.sentinel = { data := (List.replicate Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.hashSize 0).toArray }

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.isControl (g : Gcm) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.toMessage (cbor : ByteArray) : Option Message

What a member reads of a message's CBOR, or none when it is not a message.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.nonEmpty (b : ByteArray) : Option ByteArray

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.nonEmpty b = if b.size = 0 then none else some b

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.ofMessage (m : Message) : Option Gcm

The message whose CBOR a member's m is written as; none when its content is not a message.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.box (m : Message) : Option ByteArray

The box for a member's m.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm.textContent (membershipHash : ByteArray) (s : String) : ByteArray

A text message, as a member's content.

Equations

• One or more equations did not get rendered due to their size.