Polynomial Bit-Length Bounds for Encoded Group Elements

From the polynomial-time certificates for order, generator, and smul on a PrimeOrderGroupFamily, together with generator surjectivity smul_generator_surjective, every encoded group element F.encode d x has bit-length bounded by a fixed polynomial in the description length (F.encDesc d).length.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.exists_length_encode_le: uniform polynomial bound on (F.encode d x).length in terms of (F.encDesc d).length.

theorem Cslib.Crypto.PrimeOrderGroupFamily.exists_length_encode_le (F : PrimeOrderGroupFamily) : ∃ (c : ℕ) (k : ℕ), ∀ (d : F.Desc) (x : F.Carrier d), (F.encode d x).length ≤ c * ((F.encDesc d).length + 1) ^ k

Every encoded group element F.encode d x has bit-length polynomially bounded in (F.encDesc d).length.