Theorem serializedValueSizeCorrect : forall v t,
  valueHasType v t -> length (serializeValue v) = componentTypeSizeOctets t.
Proof.
  (** Proof omitted for brevity. *)
Qed.
