Group chat messages

Messages are modelled after CBOR decoding. See "Group chat message types" and "Numbers and IntroducedAt wire format" in the group chat spec.

@[reducible, inline]

abbrev Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Key : Type

A member's identity: the public key its read cap begins with.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Key = ByteArray

@[reducible, inline]

abbrev Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Index : Type

A box: its 104-byte MessageBoxIndex.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Index = ByteArray

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keySize : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keySize = 32

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.indexSize : Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.indexSize = 104

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.rosterMax : Nat

The most entries a roster holds: roster indexes are one byte.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.rosterMax = 256

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.prefixSize : Nat

How much of a member's key a Numbers field names it by.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.prefixSize = 8

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keyOf (readCap : ByteArray) : Key

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keyOf readCap = readCap.extract 0 Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keySize

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.prefixOf (key : Key) : ByteArray

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.prefixOf key = ByteArray.extract key 0 Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.prefixSize

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.startOf (readCap : ByteArray) : Index

The index a read cap starts at.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.startOf readCap = readCap.extract Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.keySize readCap.size

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.counter (index : Index) : Nat

The BACAP Idx64 of index: its first 8 bytes, little-endian.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.counter index = List.foldr (fun (b : UInt8) (n : Nat) => b.toNat + 256 * n) 0 (ByteArray.extract index 0 8).toList

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.bytesLt : List UInt8 → List UInt8 → Bool

Lexicographic order on bytes, a proper prefix first.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.bytesLt [] [] = false
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.bytesLt [] (head :: tail) = true
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.bytesLt (head :: tail) [] = false
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.bytesLt (a :: as) (b :: bs) = if a = b then Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.bytesLt as bs else decide (a < b)

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

An Introduction: its introducer's roster index in the sender's roster, and its box.

• introducer : Nat
• index : Index

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqIntroRef : DecidableEq IntroRef

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqIntroRef = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqIntroRef.decEq

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedIntroRef : Inhabited IntroRef

Equations

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

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

• name : String
• readCap : ByteArray

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqIntroduction : DecidableEq Introduction

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqIntroduction = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqIntroduction.decEq

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedIntroduction : Inhabited Introduction

Equations

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

@[reducible, inline]

abbrev Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Numbers : Type

Roster indexes assigned, consecutive, each with the key prefix of the member assigned it; none for the member the message's own Introduction introduces.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Numbers = List (Nat × Option ByteArray)

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

A message carries content or control, never both. acks pairs roster indexes, ascending, with the Idx64 of the box acknowledged.

• content : Option ByteArray
• introduction : Option Introduction
• numbers : Numbers
• introducedAt : Option IntroRef
• acks : List (Nat × Nat)

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqMessage : DecidableEq Message

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqMessage = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instDecidableEqMessage.decEq

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

Equations

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

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.instInhabitedMessage : Inhabited Message

Equations

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

Numbers and IntroducedAt

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.encodeNumbers : Numbers → List UInt8

The first index assigned, then the key prefix of each member, one per consecutive index; a lone byte for the member an Introduction introduces.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.encodeNumbers [(k, none)] = [k.toUInt8]
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.encodeNumbers [] = []

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.prefixes : Nat → List UInt8 → List (List UInt8)

Split a field into n prefixes.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.prefixes 0 x✝ = []

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.decodeNumbers (field : List UInt8) : Numbers

Empty when the field is malformed.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.decodeNumbers [k] = [(k.toNat, none)]
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.decodeNumbers [] = []

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.encodeIntroducedAt (r : IntroRef) : List UInt8

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.encodeIntroducedAt r = r.introducer.toUInt8 :: r.index.data.toList

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.decodeIntroducedAt : List UInt8 → Option IntroRef

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.decodeIntroducedAt [] = none