The CBOR a group chat message uses

Definite-length unsigned integers, byte strings, text strings and maps, as Python's cbor2 writes them: each header in its shortest form. Reading also skips any other well-formed item, so that a field this client does not interpret can be passed over or kept as it came. Every function here is total, so what is proved of it holds of what runs.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.be : Nat → Nat → List UInt8

n as k bytes, most significant first.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.be 0 x✝ = []
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.be k.succ x✝ = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.be k (x✝ / 256) ++ [(x✝ % 256).toUInt8]

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.fromBE (l : List UInt8) : Nat

The number big-endian bytes spell.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.fromBE l = List.foldl (fun (n : Nat) (b : UInt8) => n * 256 + b.toNat) 0 l

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.header (major n : Nat) : List UInt8

The header of an item of major type major with argument n, in its shortest form.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readHeader : List UInt8 → Option (Nat × Nat × List UInt8)

An item's major type, its argument, and what follows the header. Indefinite lengths and the reserved additional information values are refused.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.uint (n : Nat) : List UInt8

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.uint n = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.header 0 n

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.bytes (b : List UInt8) : List UInt8

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.bytes b = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.header 2 b.length ++ b

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.text (s : String) : List UInt8

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.text s = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.header 3 s.utf8ByteSize ++ s.toByteArray.data.toList

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.null : List UInt8

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.null = [246]

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readUInt (l : List UInt8) : Option (Nat × List UInt8)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readString (major : Nat) (l : List UInt8) : Option (List UInt8 × List UInt8)

A string's contents: of major type major, n bytes.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readBytes : List UInt8 → Option (List UInt8 × List UInt8)

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readBytes = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readString 2

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readText (l : List UInt8) : Option (String × List UInt8)

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.isNull (l : List UInt8) : Bool

Whether the next item is null.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.isNull l = (l.head? == some 246)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.skipItems : Nat → Nat → List UInt8 → Option (List UInt8)

Pass over count well-formed items. fuel bounds the items visited; one per byte of input is always enough, since every item takes at least one byte.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.skipItems x✝¹ 0 x✝ = some x✝
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.skipItems 0 n.succ x✝ = none

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Cbor.readRaw (l : List UInt8) : Option (List UInt8 × List UInt8)

The next item as it came, and what follows it.

Equations

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