Lemma dataSectionSize : forall s,
  lengthN (binaryExpsNamedOctets (dataSection s)) mod 16 = 0.
Proof.
  (** Proof omitted for brevity. *)
Qed.
