class Comparse.BytesLike (Bytes : Type) : Type

• length : Bytes → Nat
• empty : Bytes
• empty_length : length empty = 0
• recognizeEmpty : Bytes → Bool
• recognizeEmpty_correct (b : Bytes) : recognizeEmpty b = true ↔ b = empty
• concat : Bytes → Bytes → Bytes
• concat_length (b1 b2 : Bytes) : length (concat b1 b2) = length b1 + length b2
• split : Bytes → Nat → Option (Bytes × Bytes)
• split_length (b : Bytes) (i : Nat) : match split b i with | none => True | some (b1, b2) => length b1 = i ∧ i + length b2 = length b
• split_concat (b1 b2 : Bytes) : split (concat b1 b2) (length b1) = some (b1, b2)
• concat_split (b : Bytes) (i : Nat) : match split b i with | none => True | some (b1, b2) => concat b1 b2 = b
• toByteArray (b : Bytes) : Option ByteArray
• fromByteArray (b : ByteArray) : Bytes
• fromByteArray_length (b : ByteArray) : length (fromByteArray b) = b.size
• to_from_ByteArray (b : ByteArray) : toByteArray (fromByteArray b) = some b
• from_to_ByteArray (b : Bytes) : match toByteArray b with | none => True | some res => fromByteArray res = b

structure Comparse.NonExtensibleMessageFormat (Bytes : Type) [BytesLike Bytes] (a : Type) : Type

• parse : Bytes → Option (a × Bytes)
• serialize : a → List Bytes
• parse_wf (buf : Bytes) : match self.parse buf with | none => True | some (fst, suffix) => BytesLike.length suffix ≤ BytesLike.length buf

structure Comparse.ExtensibleMessageFormat (Bytes : Type) [BytesLike Bytes] (a : Type) : Type

• parse : Bytes → Option a
• serialize : a → Bytes

def Comparse.concatPrefixes {Bytes : Type} [BytesLike Bytes] (prefixes : List Bytes) (suffix : Bytes) : Bytes

Equations

• Comparse.concatPrefixes prefixes suffix = List.foldr Comparse.BytesLike.concat suffix prefixes

class Comparse.NonExtensibleMessageFormat.IsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) : Prop

• parse_serialize_inv (x : a) (suffix : Bytes) : mf.parse (concatPrefixes (mf.serialize x) suffix) = some (x, suffix)

class Comparse.NonExtensibleMessageFormat.HasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) : Prop

• serialize_parse_inv (buf : Bytes) : match mf.parse buf with | none => True | some (x, suffix) => buf = concatPrefixes (mf.serialize x) suffix

class Comparse.NonExtensibleMessageFormat.ParseConsumes {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) : Prop

• parse_consumes (buf : Bytes) : match mf.parse buf with | none => True | some (fst, suffix) => BytesLike.length suffix < BytesLike.length buf

class Comparse.ExtensibleMessageFormat.IsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) : Prop

• parse_serialize_inv (x : a) : mf.parse (mf.serialize x) = some x

class Comparse.ExtensibleMessageFormat.HasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) : Prop

• serialize_parse_inv (buf : Bytes) : match mf.parse buf with | none => True | some x => buf = mf.serialize x

class Comparse.BytesCompatiblePred {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) : Prop

• pred_empty : pred BytesLike.empty
• pred_concat (lhs rhs : Bytes) : pred lhs → pred rhs → pred (BytesLike.concat lhs rhs)
• pred_split (buf : Bytes) (i : Nat) : pred buf → match BytesLike.split buf i with | none => True | some (lhs, rhs) => pred lhs ∧ pred rhs
• pred_fromByteArray (b : ByteArray) : pred (BytesLike.fromByteArray b)

def Comparse.ExtensibleMessageFormat.wf {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (pred : Bytes → Prop) (x : a) : Prop

Equations

• mf.wf pred x = pred (mf.serialize x)

def Comparse.NonExtensibleMessageFormat.wf {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) (pred : Bytes → Prop) (x : a) : Prop

Equations

• mf.wf pred x = ∀ (b : Bytes), b ∈ mf.serialize x → pred b

theorem Comparse.ExtensibleMessageFormat.wf_eq {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (pred : Bytes → Prop) (x : a) : mf.wf pred x = pred (mf.serialize x)