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