Definition binaryExpOctets (b : binaryExp) : list octet :=
  match b with
  | U32 x    => octets32BE (Z.of_N x)
  | U64 x    => octets64BE (Z.of_N x)
  | UTF8 s   =>
    let text := stringUTF8Bytes s in
    let size := octets32BE (Z.of_nat (List.length text)) in
      size ++ text
  | Pad x    => repeat zero8 (N.to_nat x)
  | Octets o => o
  end.
