The Numbers and IntroducedAt encodings round trip

See "Numbers and IntroducedAt wire format" in the group chat spec.

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.consecutive (first : ℕ) (ps : List ByteArray) : Numbers

Members at consecutive indexes from first, each named by its prefix.

Equations

• Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.consecutive first ps = List.map (fun (x : ByteArray × ℕ) => match x with | (p, n) => (first + n, some p)) ps.zipIdx

def Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.NumbersWF (ns : Numbers) : Prop

What the Numbers encoding can carry.

Equations

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

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.toUInt8_toNat {k : ℕ} (h : k < 256) : k.toUInt8.toNat = k

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.prefixes_flatMap (ps : List ByteArray) : (∀ p ∈ ps, p.size = prefixSize) → prefixes ps.length (List.flatMap (fun (x : ByteArray) => x.data.toList) ps) = List.map (fun (x : ByteArray) => x.data.toList) ps

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.data_toList_injective : Function.Injective fun (p : ByteArray) => p.data.toList

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.encodeNumbers_some (k : ℕ) (p : ByteArray) (rest : Numbers) : encodeNumbers ((k, some p) :: rest) = k.toUInt8 :: List.flatMap (fun (x : Option ByteArray) => match x with | some p => p.data.toList | none => []) (some p :: List.map (fun (x : ℕ × Option ByteArray) => x.2) rest)

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.decodeNumbers_encodeNumbers {ns : Numbers} (h : NumbersWF ns) : decodeNumbers (encodeNumbers ns) = ns

theorem Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.decodeIntroducedAt_encodeIntroducedAt {r : IntroRef} (hi : r.introducer < 256) (hs : ByteArray.size r.index = indexSize) : decodeIntroducedAt (encodeIntroducedAt r) = some r