Fixpoint binarySize (b : binaryExp) : nat :=
  match b with
  | BiU32 _     => 4
  | BiU64 _     => 8
  | BiBytes s   => 4 + asMultipleOf4 (length s)
  | BiUTF8 s    => 4 + asMultipleOf4 (length s)
  | BiArray f   => 4 + fold_right plus 0 (map binarySize f)
  | BiReserve s => asMultipleOf4 s
  | BiRecord f  => fold_right plus 0 (map (binarySize ∘ snd) f)
  end.
