Documentation

CompPoly.Data.Bytes.CanonicalNat

Byte codecs from canonical naturals #

A type with a CanonicalNat structure has a fixed-width byte codec: the little-endian bytes of toNat, bytesFor bound of them, decoded by ofNat?. This is ByteCodec.ofCanonicalNat, a definition rather than an instance so that a composite type may choose a different codec (an extension field concatenates its coefficients) while still having a canonical natural.

The same structure gives the total decoder used for challenges: ofBytesModOrder reads any number of bytes as an integer and reduces it modulo bound. Reading back an exact-width encoding this way recovers the element (ofBytesModOrder_toBytes); reading more bytes than the width is what makes the result close to uniform.

ZMod p receives both: instCanonicalNatZMod from CompPoly.Data.Classes.CanonicalNat and the derived ByteCodec (ZMod p) here, so every spec prime field in CompPoly.Fields serializes.

source
@[instance_reducible]
def CompPoly.ByteCodec.ofCanonicalNat (F : Type u) [CanonicalNat F] :
ByteCodec F

The fixed-width byte codec of a type with canonical naturals: bytesFor bound little-endian bytes of toNat, decoded by ofNat?.

Instances For
    source
    def CompPoly.CanonicalNat.ofBytesModOrder {F : Type u} [CanonicalNat F] {n : ℕ} (v : Vector UInt8 n) :
    F

    Read any byte string as a little-endian integer and reduce it modulo bound. Total, and close to uniform when the string is longer than bytesFor bound.

    Instances For
      source
      def CompPoly.CanonicalNat.ofByteArrayModOrder {F : Type u} [CanonicalNat F] (b : ByteArray) :
      F

      ofBytesModOrder on a ByteArray of any size.

      Instances For
        source
        @[instance_reducible]
        instance CompPoly.CanonicalNat.instDeserializeVectorUInt8 {F : Type u} [CanonicalNat F] {n : ℕ} :
        Deserialize F (Vector UInt8 n)
        source
        @[instance_reducible]
        instance CompPoly.CanonicalNat.instDeserializeByteArray {F : Type u} [CanonicalNat F] :
        Deserialize F ByteArray
        source
        @[simp]
        theorem CompPoly.CanonicalNat.deserialize_vector_eq {F : Type u} [CanonicalNat F] {n : ℕ} (v : Vector UInt8 n) :
        Deserialize.deserialize v = ofBytesModOrder v
        source
        @[simp]
        theorem CompPoly.CanonicalNat.deserialize_byteArray_eq {F : Type u} [CanonicalNat F] (b : ByteArray) :
        Deserialize.deserialize b = ofByteArrayModOrder b
        source
        theorem CompPoly.CanonicalNat.ofBytesModOrder_toVecLE_toNat {F : Type u} [CanonicalNat F] (x : F) :
        ofBytesModOrder (Bytes.toVecLE (Bytes.bytesFor (bound F)) (toNat x)) = x

        Reading back an exact-width little-endian encoding modulo the order recovers the element.

        source
        theorem CompPoly.CanonicalNat.ofByteArrayModOrder_toByteArrayLE_toNat {F : Type u} [CanonicalNat F] (x : F) :
        ofByteArrayModOrder (Bytes.toByteArrayLE (Bytes.bytesFor (bound F)) (toNat x)) = x
        source
        theorem CompPoly.ByteCodec.ofBytesModOrder_toBytes {F : Type u} [CanonicalNat F] (x : F) :
        CanonicalNat.ofBytesModOrder (toBytes x) = x

        Reading back the ofCanonicalNat encoding modulo the order recovers the element.

        ZMod #

        source
        @[instance_reducible]
        instance CompPoly.instByteCodecZMod (p : ℕ) [NeZero p] :
        ByteCodec (ZMod p)

        The little-endian residue codec of ZMod p, bytesFor p bytes wide.

        source
        @[simp]
        theorem CompPoly.ByteCodec.width_zmod (p : ℕ) [NeZero p] :
        width (ZMod p) = Bytes.bytesFor p
        source
        @[simp]
        theorem CompPoly.ByteCodec.toBytes_zmod {p : ℕ} [NeZero p] (x : ZMod p) :
        toBytes x = Bytes.toVecLE (Bytes.bytesFor p) x.val
        source
        @[simp]
        theorem CompPoly.ByteCodec.ofBytes?_zmod {p : ℕ} [NeZero p] (v : Vector UInt8 (Bytes.bytesFor p)) :
        ofBytes? v = CanonicalNat.ofNat? (Bytes.ofVecLE v)

        Round trips through the class interfaces #

        For a type whose codec is ByteCodec.ofCanonicalNat, the total decoder inverts the serializer at the codec's width. Together with ByteCodec.deserialize_serialize (the partial decoder) and the Serialize.IsInjective instances, this is the full round-trip story a protocol relies on.

        source
        theorem CompPoly.CanonicalNat.deserialize_serialize {F : Type u} [CanonicalNat F] [inst : ByteCodec F] (h : inst = ByteCodec.ofCanonicalNat F) (x : F) :
        Deserialize.deserialize (serialize x) = x

        The total decoder inverts the serializer at the codec's own width, whenever the codec is the one derived from canonical naturals.

        source
        theorem CompPoly.CanonicalNat.deserialize_serialize_byteArray {F : Type u} [CanonicalNat F] [inst : ByteCodec F] (h : inst = ByteCodec.ofCanonicalNat F) (x : F) :
        Deserialize.deserialize (serialize x) = x
        source
        theorem CompPoly.deserialize_serialize_zmod {p : ℕ} [NeZero p] (x : ZMod p) :
        Deserialize.deserialize (serialize x) = x

        ZMod p: the total decoder inverts the serializer.