static byte[] toASCII(S s) {
  ret s.getBytes(StandardCharsets.US_ASCII);
}