Fixed-width byte codecs

ByteCodec F is a fixed-width byte encoding of F with a decoder that succeeds on every encoding. Its single law, ofBytes?_toBytes, makes toBytes injective, and from it the protocol-facing classes follow for free: HasSize F UInt8, Serialize F ByteArray with Serialize.IsInjective, DeserializeOption, and Serde, together with the same for Vector UInt8 (width F).

The encoding is a property of the value, not of the carrier: two carriers of the same field must give the same bytes for the same element. Scalar fields derive their codec from CanonicalNat (ByteCodec.ofCanonicalNat, in CompPoly.Data.Bytes.CanonicalNat); composite types such as extensions and degree-bounded polynomials concatenate the codecs of their parts.

class CompPoly.ByteCodec (F : Type u) : Type u

A fixed-width byte encoding of F whose decoder recovers every encoded element.

• width : ℕ

  The number of bytes of every encoding.

• toBytes : F → Vector UInt8 (width F)

  Encode an element.

• ofBytes? : Vector UInt8 (width F) → Option F

  Decode width bytes, failing on strings that encode no element.

• ofBytes?_toBytes (x : F) : ofBytes? (toBytes x) = some x

theorem CompPoly.ByteCodec.toBytes_injective {F : Type u} [ByteCodec F] : Function.Injective toBytes

@[simp]

theorem CompPoly.ByteCodec.toBytes_inj {F : Type u} [ByteCodec F] {x y : F} : toBytes x = toBytes y ↔ x = y

def CompPoly.ByteCodec.toByteArray {F : Type u} [ByteCodec F] (x : F) : ByteArray

The encoding as a ByteArray of size width F.

@[simp]

theorem CompPoly.ByteCodec.data_toByteArray {F : Type u} [ByteCodec F] (x : F) : (toByteArray x).data = (toBytes x).toArray

@[simp]

theorem CompPoly.ByteCodec.size_toByteArray {F : Type u} [ByteCodec F] (x : F) : (toByteArray x).size = width F

theorem CompPoly.ByteCodec.toByteArray_injective {F : Type u} [ByteCodec F] : Function.Injective toByteArray

def CompPoly.ByteCodec.ofByteArray? {F : Type u} [ByteCodec F] (b : ByteArray) : Option F

Decode a ByteArray, failing unless it has size width F and encodes an element.

@[simp]

theorem CompPoly.ByteCodec.ofByteArray?_toByteArray {F : Type u} [ByteCodec F] (x : F) : ofByteArray? (toByteArray x) = some x

Derived protocol interfaces

@[instance_reducible]

instance CompPoly.ByteCodec.instHasSizeUInt8 {F : Type u} [ByteCodec F] : HasSize F UInt8

@[instance_reducible]

instance CompPoly.ByteCodec.instSerializeByteArray {F : Type u} [ByteCodec F] : Serialize F ByteArray

instance CompPoly.ByteCodec.instIsInjectiveByteArray {F : Type u} [ByteCodec F] : Serialize.IsInjective F ByteArray

@[instance_reducible]

instance CompPoly.ByteCodec.instDeserializeOptionByteArray {F : Type u} [ByteCodec F] : DeserializeOption F ByteArray

@[instance_reducible]

instance CompPoly.ByteCodec.instSerdeByteArray {F : Type u} [ByteCodec F] : Serde F ByteArray

@[instance_reducible]

instance CompPoly.ByteCodec.instSerializeVectorUInt8Width {F : Type u} [ByteCodec F] : Serialize F (Vector UInt8 (width F))

instance CompPoly.ByteCodec.instIsInjectiveVectorUInt8Width {F : Type u} [ByteCodec F] : Serialize.IsInjective F (Vector UInt8 (width F))

@[instance_reducible]

instance CompPoly.ByteCodec.instDeserializeOptionVectorUInt8Width {F : Type u} [ByteCodec F] : DeserializeOption F (Vector UInt8 (width F))

@[instance_reducible]

instance CompPoly.ByteCodec.instSerdeVectorUInt8Width {F : Type u} [ByteCodec F] : Serde F (Vector UInt8 (width F))

@[simp]

theorem CompPoly.ByteCodec.serialize_eq_toByteArray {F : Type u} [ByteCodec F] (x : F) : serialize x = toByteArray x

@[simp]

theorem CompPoly.ByteCodec.serialize_eq_toBytes {F : Type u} [ByteCodec F] (x : F) : serialize x = toBytes x

@[simp]

theorem CompPoly.ByteCodec.deserialize_byteArray_eq {F : Type u} [ByteCodec F] (b : ByteArray) : DeserializeOption.deserialize b = ofByteArray? b

@[simp]

theorem CompPoly.ByteCodec.deserialize_vector_eq {F : Type u} [ByteCodec F] (v : Vector UInt8 (width F)) : DeserializeOption.deserialize v = ofBytes? v

theorem CompPoly.ByteCodec.deserialize_serialize {F : Type u} [ByteCodec F] (x : F) : DeserializeOption.deserialize (serialize x) = some x