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

static byte toASCII(char c) {
  ret toASCII(str(new char[] {c}))[0];
}