code: private static void mult(int[] src, int srcLen, int value, int[] dst) {
          long val = value & LONG_MASK;
          long carry = 0;
          for (int i = 0; i < srcLen; i++) {
              long product = (src[i] & LONG_MASK) * val + carry;
              dst[i] = (int) product;
              carry = product >>> 32;
          }
          dst[srcLen] = (int) carry;
      }
docs: /*@
  @ requires src.length >= srcLen && dst.length >= srcLen + 1;
  @ assignable dst[0 .. srcLen];
  @ ensures AP(dst, srcLen + 1) == \old(AP(src, srcLen) * UNSIGNED(value));
  @