Documentation

CompPoly.Data.Bytes.Bias

Bias of the reduce-modulo-order decoder #

A challenge squeezed from a byte sponge is CanonicalNat.ofBytesModOrder: n bytes read as a little-endian integer and reduced modulo bound. Reducing the 256 ^ n strings modulo bound hits every residue 256 ^ n / bound or 256 ^ n / bound + 1 times, so the induced distribution on F is within bound / 256 ^ n of uniform in total variation. Sixteen bytes beyond the field's width make that below 2 ^ -128, which is the margin spongefish uses.

Everything here is counting; no probability theory is imported. ArkLib's Deserialize.CloseToUniform instance for ZMod p is derived from the last theorem by casting into its PMF distance.

source
def CompPoly.Bytes.equivFin (n : ℕ) :
Vector UInt8 n ≃ Fin (256 ^ n)

Little-endian byte strings of length n are the naturals below 256 ^ n.

Instances For
    source
    @[instance_reducible]
    instance CompPoly.Bytes.instFintypeVectorUInt8 (n : ℕ) :
    Fintype (Vector UInt8 n)

    n-byte strings are finite, through equivFin.

    source
    theorem CompPoly.Bytes.card_vector_uint8 (n : ℕ) :
    Fintype.card (Vector UInt8 n) = 256 ^ n
    source
    theorem CompPoly.CanonicalNat.ofNat_eq_iff {F : Type u_1} [CanonicalNat F] {m : ℕ} {x : F} :
    ofNat m = x ↔ m % bound F = toNat x
    source
    def CompPoly.CanonicalNat.fiberEquiv {F : Type u_1} [CanonicalNat F] (n : ℕ) (x : F) :
    { v : Vector UInt8 n // ofBytesModOrder v = x } ≃ { k : ℕ // k < 256 ^ n ∧ k ≡ toNat x [MOD bound F] }

    The n-byte strings decoding to x modulo the order, as the naturals below 256 ^ n congruent to toNat x.

    Instances For
      source
      @[instance_reducible]
      instance CompPoly.CanonicalNat.instFintypeFiber {F : Type u_1} [CanonicalNat F] [DecidableEq F] (n : ℕ) (x : F) :
      Fintype { v : Vector UInt8 n // ofBytesModOrder v = x }
      source
      theorem CompPoly.CanonicalNat.card_fiber_ofBytesModOrder {F : Type u_1} [CanonicalNat F] [DecidableEq F] (n : ℕ) (x : F) :
      Fintype.card { v : Vector UInt8 n // ofBytesModOrder v = x } = 256 ^ n / bound F + if toNat x < 256 ^ n % bound F then 1 else 0

      Exactly how many n-byte strings decode to x modulo the order: the quotient 256 ^ n / bound, plus one for the residues below the remainder.

      source
      theorem CompPoly.CanonicalNat.abs_card_fiber_div_sub_le {F : Type u_1} [CanonicalNat F] [DecidableEq F] (n : ℕ) (x : F) :
      |↑(Fintype.card { v : Vector UInt8 n // ofBytesModOrder v = x }) / 256 ^ n - 1 / ↑(bound F)| ≤ 1 / 256 ^ n

      Every fiber is within one of the ideal 256 ^ n / bound, so each residue's probability is within 1 / 256 ^ n of uniform.

      source
      theorem CompPoly.CanonicalNat.tv_ofBytesModOrder_le {F : Type u_1} [CanonicalNat F] [DecidableEq F] [Fintype F] (n : ℕ) :
      ∑ x : F, |↑(Fintype.card { v : Vector UInt8 n // ofBytesModOrder v = x }) / 256 ^ n - 1 / ↑(bound F)| ≤ ↑(bound F) / 256 ^ n

      The total-variation distance of ofBytesModOrder on n bytes from the uniform distribution on F is at most bound / 256 ^ n: sixteen bytes beyond the width give 2 ^ -128. Stated over ℚ; ArkLib derives its PMF form from it.