Definition binaryExpImage2D
  (i : imageInfo)
  (m : mipMapList)
: binaryExp :=
  let imageDataStart := mipMapOffset (mipMapFirst m) in
  let encMips        := binaryExpMipMaps m in
  let encMipsSize    := binarySize encMips in
  let encMipsPad     := imageDataStart - encMipsSize in
  let imageSize      := mipMapImageDataSizeTotal m in
  let imageSize16    := asMultipleOf16 imageSize in
    BiRecord [
      ("mipMaps", encMips);
      ("mipPad",  BiReserve encMipsPad);
      ("mipData", BiReserve imageSize16)
    ].
