Polynomial-time padded XOR

A bounded bitwise map runs over the larger operand length. Two runtime bit reads and Boolean connectives implement each output XOR.

theorem Complexity.BitPolynomial.Internal.addEval_mem_FP : addEval ∈ FP