The Acks field, in bytes

The executable codec for the Acks field, following katzenqt's ack_codec.py: the count less one, the members named as a list or a bitmap, whichever is shorter, then each one's Idx64, little-endian. Each definition follows its namesake in Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec, whose theorems AckBytesProofs carries over to this one. Reading is not strict: like katzenqt, it accepts a list where the bitmap would have been shorter.

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

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.maxNaming : Nat

The longest naming: a bitmap reaching roster index 255.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.maxNaming = 32

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.idxSize : Nat

Bytes in a value: an Idx64.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.idxSize = 8

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.width (i : Nat) : Nat

Bytes a bitmap needs to reach roster index i.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.width i = i / 8 + 1

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.marks (idx : List Nat) (j k : Nat) : Bool

Whether bit k of byte j marks a member of idx: index i is bit 7 - i % 8 of byte i / 8.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.marks idx j k = idx.any fun (i : Nat) => decide (i / 8 = j) && decide (7 - i % 8 = k)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.bitmapByte (idx : List Nat) (j : Nat) : Nat

Byte j of the bitmap for idx.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.bitmap (idx : List Nat) (w : Nat) : List Nat

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.bitmap idx w = List.map (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.bitmapByte idx) (List.range w)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.nameMembers (idx : List Nat) : List Nat

Ascending roster indexes as a list or a bitmap, whichever is shorter.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.bitSet (naming : List Nat) (i : Nat) : Bool

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.bitSet naming i = (naming.getD (i / 8) 0).testBit (7 - i % 8)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.setBits (naming : List Nat) : List Nat

The roster indexes a bitmap marks, in ascending order.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.ascending : List Nat → Bool

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.ascending x✝ = true

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.readMembers (naming : List Nat) (count : Nat) : Option (List Nat)

What precedes count values.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.chunks (v : Nat) : List Nat → Nat → List (List Nat)

The n values of v bytes that follow the naming.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.chunks v x✝ 0 = []
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.chunks v x✝ n.succ = List.take v x✝ :: Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.chunks v (List.drop v x✝) n

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.le : Nat → Nat → List Nat

The k bytes of n, least significant first.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.le 0 x✝ = []
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.le k.succ x✝ = x✝ % 256 :: Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.le k (x✝ / 256)

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.fromLE (l : List Nat) : Nat

The number little-endian bytes spell.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.fromLE l = List.foldr (fun (b n : Nat) => b + 256 * n) 0 l

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.encodeUncounted (acks : List (Nat × List Nat)) : List Nat

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.encodeValues (acks : List (Nat × List Nat)) : List Nat

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decodeValues (v : Nat) : List Nat → Option (List (Nat × List Nat))

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decodeValues v [] = some []

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.encodeNat (acks : List (Nat × Nat)) : List Nat

The field for acks, pairs of roster index and Idx64 in ascending order of index, as numbers below 256.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decodeNat (field : List Nat) : Option (List (Nat × Nat))

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.encode (acks : List (Nat × Nat)) : ByteArray

The field for acks; empty when there is nothing to acknowledge.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decode (field : ByteArray) : Option (List (Nat × Nat))

The acknowledgements a field carries, or none when it is malformed.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decode field = Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes.decodeNat (List.map UInt8.toNat field.data.toList)