Serialization and deserialization classes

Simple type classes for serializing a type into another type, most often ByteArray or a fixed-length Vector of units, and for deserializing back, with or without failure.

These declarations are ported verbatim from ArkLib (ArkLib/Data/Classes/Serde.lean) so that CompPoly can supply instances for its field and polynomial types directly. The statistical-closeness class Deserialize.CloseToUniform stays in ArkLib, where the probability theory it needs already lives; CompPoly proves the counting facts behind it in Nat terms.

class Serialize (α : Type u) (β : Type v) : Type (max u v)

Type class for types that can be serialized to another type (most often ByteArray or String).

• serialize : α → β

class Serialize.IsInjective (α : Type u) (β : Type v) [inst : Serialize α β] : Prop

Type class for injective serialization.

• serialize_inj : Function.Injective serialize

class Deserialize (α : Type u) (β : Type v) : Type (max u v)

Type class for types that can be deserialized from another type (most often ByteArray or String), which never fails.

• deserialize : β → α

class DeserializeOption (α : Type u) (β : Type v) : Type (max u v)

Type class for types that can be deserialized from another type (most often ByteArray or String), returning an Option if the deserialization fails.

• deserialize : β → Option α

class Serde (α : Type u) (β : Type v) extends Serialize α β, DeserializeOption α β : Type (max u v)

Type class for types that can be serialized and deserialized (with potential failure) to/from another type (most often ByteArray or String).

• serialize : α → β
• deserialize : β → Option α