Writing encodings in polynomial time

A polynomial-time construction that hands its result to a DataEncode consumer, such as a verifier reading a list of query positions, has to write the DataEncode.bitstringEncode of that result. This module shows that writing the encoding of a bit list, and of a number, is polynomial-time.

A bit list is encoded as the encodings of its bits between two brackets, and writing that is a fold over the list (encodeList_mem_FP). A number is encoded as its minimal binary expansion Nat.bits, so writing a polynomial-time number's encoding is writing its expansion (bits_mem_FP) and then encoding that list (natEncode_mem_FP). No width has to be supplied.

Main results

• encodeList_mem_FP — writing the encoding of a bit list is polynomial-time
• natEncode_mem_FP — writing the encoding of a polynomial-time number is polynomial-time

theorem Complexity.encodeList_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => DataEncode.bitstringEncode (a z)) ∈ FP

Writing the encoding of a bit list is polynomial-time. If a ∈ FP, then so is z ↦ DataEncode.bitstringEncode (a z).

theorem Complexity.natEncode_mem_FP {n : List Bool → ℕ} (hn : UnaryFn n) : (fun (z : List Bool) => DataEncode.bitstringEncode (n z)) ∈ FP

Writing the encoding of a polynomial-time number is polynomial-time. If n is a polynomial-time number, then z ↦ DataEncode.bitstringEncode (n z) is in FP: a number is encoded as its minimal binary expansion.