The Acks field of a group chat message

Acknowledged members are named by roster index, as a list of index bytes or a bitmap, whichever is shorter, followed by one v-byte value each in ascending index order. See "Rosters" in the group chat spec. Bytes are natural numbers here, each < 256.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.rosterMax : ℕ

Roster indexes are one byte.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.maxNaming : ℕ

The longest naming: a bitmap reaching roster index 255.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.maxNaming = 32

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.width (i : ℕ) : ℕ

Bytes a bitmap needs to reach roster index i.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.byteBits (idx : List ℕ) (j : ℕ) : Finset ℕ

The bits of byte j of the bitmap for idx, counted from the least significant: index i is bit 7 - i % 8 of byte i / 8.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.byteBits idx j = (List.map (fun (i : ℕ) => 7 - i % 8) (List.filter (fun (i : ℕ) => decide (i / 8 = j)) idx)).toFinset

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.bitmapByte (idx : List ℕ) (j : ℕ) : ℕ

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.bitmapByte idx j = ∑ k ∈ Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.byteBits idx j, 2 ^ k

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.bitmap (idx : List ℕ) (w : ℕ) : List ℕ

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.nameMembers (idx : List ℕ) : List ℕ

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.AckCodec.bitSet (naming : List ℕ) (i : ℕ) : Bool

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.setBits (naming : List ℕ) : List ℕ

The roster indexes a bitmap marks, in ascending order.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.setBits naming = List.filter (Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.bitSet naming) (List.range (naming.length * 8))

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.listShortest (naming : List ℕ) : Bool

Whether a list naming is no longer than the bitmap for the same members.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.readMembers (strict : Bool) (naming : List ℕ) (count : ℕ) : Option (List ℕ)

What precedes count values. strict also refuses a list where the bitmap is shorter, which the spec does not ask for.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.chunks (v : ℕ) : List ℕ → ℕ → List (List ℕ)

The n values of v bytes that follow the naming.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.encodeUncounted (acks : List (ℕ × List ℕ)) : List ℕ

The field for acks, pairs of roster index and value in ascending order of index.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.decodeUncounted (strict : Bool) (v : ℕ) (field : List ℕ) : Option (List (ℕ × List ℕ))

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

Equations

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

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.WF (v : ℕ) (acks : List (ℕ × List ℕ)) : Prop

What a sender may encode: ascending roster indexes, each one byte, each value v bytes.

• sorted : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (List.map Prod.fst acks)
• lt (a : ℕ × List ℕ) : a ∈ acks → a.1 < rosterMax
• size (a : ℕ × List ℕ) : a ∈ acks → a.2.length = v

Lemmas

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.testBit_bitmapByte (idx : List ℕ) (j k : ℕ) : (bitmapByte idx j).testBit k = true ↔ k ∈ byteBits idx j

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.mem_byteBits {idx : List ℕ} {i : ℕ} : 7 - i % 8 ∈ byteBits idx (i / 8) ↔ i ∈ idx

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.bitSet_bitmap {idx : List ℕ} {w i : ℕ} (hi : i < w * 8) : bitSet (bitmap idx w) i = true ↔ i ∈ idx

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.filter_range_eq {l : List ℕ} {n : ℕ} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) l) (hl : ∀ x ∈ l, x < n) (p : ℕ → Bool) (hp : ∀ x < n, p x = true ↔ x ∈ l) : List.filter p (List.range n) = l

The members of a strictly ascending list below n, read off 0..n-1 in order, are the list.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.setBits_bitmap {idx : List ℕ} {w : ℕ} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) idx) (hl : ∀ x ∈ idx, x < w * 8) : setBits (bitmap idx w) = idx

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.bitmapByte_ne_zero {idx : List ℕ} {i : ℕ} (h : i ∈ idx) : bitmapByte idx (i / 8) ≠ 0

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.length_flatten_uniform {v : ℕ} {vals : List (List ℕ)} : (∀ a ∈ vals, a.length = v) → vals.flatten.length = vals.length * v

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.chunks_flatten {v : ℕ} {vals : List (List ℕ)} : (∀ a ∈ vals, a.length = v) → chunks v vals.flatten vals.length = vals

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.flatten_chunks {v n : ℕ} {l : List ℕ} : l.length = n * v → (chunks v l n).flatten = l

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.chunks_length_mem {v n : ℕ} {l : List ℕ} : l.length = n * v → ∀ c ∈ chunks v l n, c.length = v

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.length_chunks {v n : ℕ} {l : List ℕ} : (chunks v l n).length = n

Decoding undoes encoding

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.width_le {i : ℕ} (h : i < rosterMax) : width i ≤ maxNaming

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.decodeUncounted_encodeUncounted (strict : Bool) {v : ℕ} (hv : maxNaming < v) {acks : List (ℕ × List ℕ)} (h : WF v acks) : decodeUncounted strict v (encodeUncounted acks) = some acks

Decoding undoes encoding, under either parser, whenever a value is longer than the longest naming.

Only then: a value of 32 bytes or fewer is misread

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.decodeUncounted_encodeUncounted_iff (strict : Bool) (v : ℕ) : (∀ (acks : List (ℕ × List ℕ)), WF v acks → decodeUncounted strict v (encodeUncounted acks) = some acks) ↔ maxNaming < v

Without a count, decoding undoes encoding for every acknowledgement set exactly when values exceed 32 bytes.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.le_of_getLast? {l : List ℕ} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) l) {last : ℕ} (h : l.getLast? = some last) {x : ℕ} (hx : x ∈ l) : x ≤ last

A strictly ascending list's last element is at least every element.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.mem_setBits {naming : List ℕ} {i : ℕ} : i ∈ setBits naming ↔ i < naming.length * 8 ∧ bitSet naming i = true

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.setBits_pairwise (naming : List ℕ) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (setBits naming)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.lt_eight_of_testBit {b k : ℕ} (hb : b < 256) (h : b.testBit k = true) : k < 8

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.nameMembers_setBits {naming : List ℕ} (hbytes : ∀ b ∈ naming, b < 256) (hne : naming ≠ []) (hlast : naming.getLast? ≠ some 0) (hcount : naming.length < (setBits naming).length) : nameMembers (setBits naming) = naming

Under the strict parser, a well-formed bitmap is the bitmap of the members it marks.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.encodeUncounted_decodeUncounted {v : ℕ} {field : List ℕ} {acks : List (ℕ × List ℕ)} (hbytes : ∀ b ∈ field, b < 256) (h : decodeUncounted true v field = some acks) : WF v acks ∧ encodeUncounted acks = field

Under the strict parser, a field that decodes is the encoding of its well-formed result.

The spec's parser is malleable; a strict one is not

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.spec_decodeUncounted_malleable : have field := [0, 1, 2] ++ List.replicate 99 0; ∃ (acks : List (ℕ × List ℕ)), decodeUncounted false 33 field = some acks ∧ encodeUncounted acks ≠ field ∧ decodeUncounted false 33 (encodeUncounted acks) = some acks

The members 0, 1 and 2, named by a list where the bitmap 0xe0 is shorter, with three 33-byte values: the spec's parser accepts it, but encodeUncounted would write the bitmap.

Counted field

Values shorter than the longest naming need an explicit count, so the field begins with the count less one; an empty field acknowledges no one.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.encode (acks : List (ℕ × List ℕ)) : List ℕ

The field for acks: the count less one, the naming, then the values.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.encode acks = if acks = [] then [] else (acks.length - 1) :: Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.encodeUncounted acks

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.decode (strict : Bool) (v : ℕ) : List ℕ → Option (List (ℕ × List ℕ))

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

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.decode strict v [] = some []

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.readMembers_nameMembers (strict : Bool) {idx : List ℕ} (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) idx) (hlt : ∀ x ∈ idx, x < rosterMax) : readMembers strict (nameMembers idx) idx.length = some idx

Ascending roster indexes, named by nameMembers, read back as themselves.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.readMembers_strict_some {naming : List ℕ} {count : ℕ} {idx : List ℕ} (hbytes : ∀ b ∈ naming, b < 256) (h : readMembers true naming count = some idx) : idx.length = count ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) idx ∧ (∀ i ∈ idx, i < rosterMax) ∧ nameMembers idx = naming

What the strict parser reads before count values: count ascending roster indexes, named exactly as nameMembers names them.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.count_lt {v : ℕ} {acks : List (ℕ × List ℕ)} (h : WF v acks) : acks.length - 1 < rosterMax

A sender acknowledges at most rosterMax members, so the count less one fits in a byte.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.decode_encode (strict : Bool) (v : ℕ) {acks : List (ℕ × List ℕ)} (h : WF v acks) : decode strict v (encode acks) = some acks

Decoding undoes encoding, under either parser, for values of every size.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.encode_decode {v : ℕ} {field : List ℕ} {acks : List (ℕ × List ℕ)} (hbytes : ∀ b ∈ field, b < 256) (h : decode true v field = some acks) : WF v acks ∧ encode acks = field

Under the strict parser, a field that decodes is the encoding of its well-formed result.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.spec_decode_malleable : have field := [2, 0, 1, 2] ++ List.replicate 24 0; ∃ (acks : List (ℕ × List ℕ)), decode false 8 field = some acks ∧ encode acks ≠ field ∧ decode false 8 (encode acks) = some acks

The members 0, 1 and 2, named by a list where the bitmap 0xe0 is shorter, with three 8-byte values: the spec's parser accepts it, but encode would write the bitmap.

Values: Idx64, little-endian

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.le : ℕ → ℕ → List ℕ

The k bytes of n, least significant first.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.fromLE (l : List ℕ) : ℕ

The number little-endian bytes spell.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.fromLE_le (k n : ℕ) : n < 256 ^ k → fromLE (le k n) = n

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.le_fromLE (l : List ℕ) : (∀ b ∈ l, b < 256) → le l.length (fromLE l) = l

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.fromLE_lt (l : List ℕ) : (∀ b ∈ l, b < 256) → fromLE l < 256 ^ l.length

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.length_le (k n : ℕ) : (le k n).length = k

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.idxSize : ℕ

Bytes in a value: an Idx64.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.idxSize = 8

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.encodeIdx64 (acks : List (ℕ × ℕ)) : List ℕ

The field for acks, pairs of roster index and Idx64.

Equations

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

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.decodeIdx64 (strict : Bool) (field : List ℕ) : Option (List (ℕ × ℕ))

Equations

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

structure Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.WFIdx64 (acks : List (ℕ × ℕ)) : Prop

What a sender may encode: ascending roster indexes, each one byte, each value an Idx64.

• sorted : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (List.map Prod.fst acks)
• lt (a : ℕ × ℕ) : a ∈ acks → a.1 < rosterMax
• idx64 (a : ℕ × ℕ) : a ∈ acks → a.2 < 2 ^ 64

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.map_le_fromLE {acks : List (ℕ × ℕ)} (h : ∀ a ∈ acks, a.2 < 2 ^ 64) : List.map (fun (a : ℕ × List ℕ) => (a.1, fromLE a.2)) (List.map (fun (a : ℕ × ℕ) => (a.1, le idxSize a.2)) acks) = acks

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.decodeIdx64_encodeIdx64 (strict : Bool) {acks : List (ℕ × ℕ)} (h : WFIdx64 acks) : decodeIdx64 strict (encodeIdx64 acks) = some acks

Decoding undoes encoding for Idx64 values.

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec.encodeIdx64_decodeIdx64 {field : List ℕ} {acks : List (ℕ × ℕ)} (hbytes : ∀ b ∈ field, b < 256) (h : decodeIdx64 true field = some acks) : WFIdx64 acks ∧ encodeIdx64 acks = field

For Idx64 values, under the strict parser, a field that decodes is the encoding of its well-formed result.