static byte[] intArrayToBytes_bigEndian(int[] a) {
  byte[] b = new byte[a.length*4];
  for (int i = 0; i < a.length; i++)
    intToBytes_inArray_bigEndian(a[i], b, i*4);
  ret b;
}