Bit-prefix projection of bit strings as an additive homomorphism

When M ≤ q, taking the first M bits of a q-bit word v : BitString q agrees with Cslib.BitString.zeroExtend (d' := M) v, forms a surjective additive group homomorphism Cslib.BitString.restrictBitsAddHom hM : BitString q →+ BitString M, and reduces the unsigned integer value Cslib.BitString.equivFin q v modulo 2 ^ M (Cslib.BitString.val_equivFin_restrictBitsAddHom).

Placing these declarations in a dedicated topic module avoids expanding the public interface of the widely imported Complexity/Foundations/Data/BitString/Basic.lean.

Main definitions

• Cslib.BitString.restrictBitsAddHom: projecting BitString q to its first M ≤ q bits as an additive group homomorphism BitString q →+ BitString M.

Main results

• Cslib.BitString.restrictBitsAddHom_eq_zeroExtend: restrictBitsAddHom hM v agrees with zeroExtend (d' := M) v.
• Cslib.BitString.restrictBitsAddHom_zeroExtend, Cslib.BitString.restrictBitsAddHom_surjective: zeroExtend is a right inverse to restrictBitsAddHom hM, which is therefore surjective.
• Cslib.BitString.val_equivFin_restrictBitsAddHom: the unsigned value of restrictBitsAddHom hM v is (equivFin q v).val % 2 ^ M.

def Cslib.BitString.restrictBitsAddHom {q M : ℕ} (hM : M ≤ q) : BitString q →+ BitString M

Projecting a q-bit string to its first M ≤ q bits as an additive group homomorphism.

theorem Cslib.BitString.restrictBitsAddHom_eq_zeroExtend {q M : ℕ} (hM : M ≤ q) (v : BitString q) : (restrictBitsAddHom hM) v = v.zeroExtend

When M ≤ q, restrictBitsAddHom hM v agrees pointwise with zeroExtend (d' := M) v.

@[simp]

theorem Cslib.BitString.restrictBitsAddHom_zeroExtend {q M : ℕ} (hM : M ≤ q) (w : BitString M) : (restrictBitsAddHom hM) w.zeroExtend = w

Zero-extending an M-bit string to q ≥ M bits is a right inverse to restrictBitsAddHom hM.

theorem Cslib.BitString.restrictBitsAddHom_surjective {q M : ℕ} (hM : M ≤ q) : Function.Surjective ⇑(restrictBitsAddHom hM)

restrictBitsAddHom hM is surjective whenever M ≤ q.

theorem Cslib.BitString.val_equivFin_restrictBitsAddHom {q M : ℕ} (hM : M ≤ q) (v : BitString q) : ↑((equivFin M) ((restrictBitsAddHom hM) v)) = ↑((equivFin q) v) % 2 ^ M

Taking the first M ≤ q bits of v : BitString q corresponds to taking its unsigned integer value modulo 2 ^ M.

theorem Cslib.BitString.val_equivFin_zeroExtend_of_le {q M : ℕ} (hM : M ≤ q) (v : BitString q) : ↑((equivFin M) v.zeroExtend) = ↑((equivFin q) v) % 2 ^ M

Taking the M-bit prefix of v : BitString q via zeroExtend when M ≤ q reduces its unsigned integer value modulo 2 ^ M.