val u8_of_ascii_char (c: ascii_char) : x: UInt8.t{UInt8.v x = Char.int_of_char c}
let u8_of_ascii_char (c: ascii_char): x:UInt8.t{ UInt8.v x = Char.int_of_char c } =
  let x32 = Char.u32_of_char c in
  assert_norm (pow2 24 * pow2 8 = pow2 32);
  Math.Lemmas.modulo_modulo_lemma (UInt32.v x32) (pow2 24) (pow2 8);
  Int.Cast.Full.uint32_to_uint8 x32
val u8_of_ascii_char (c: ascii_char) : x: UInt8.t{UInt8.v x = Char.int_of_char c}
let u8_of_ascii_char (c: ascii_char) : x: UInt8.t{UInt8.v x = Char.int_of_char c} =
let x32 = Char.u32_of_char c in
assert_norm (pow2 24 * pow2 8 = pow2 32);
Math.Lemmas.modulo_modulo_lemma (UInt32.v x32) (pow2 24) (pow2 8);
Int.Cast.Full.uint32_to_uint8 x32
LowStar.Literal.fsti.checked
prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.String.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.Int.Cast.Full.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Char.fsti.checked
LowStar.Literal.fsti
LowStar.Literal.ascii_char FStar.Int.Cast.uint32_to_uint8 Prims.unit FStar.Math.Lemmas.modulo_modulo_lemma FStar.UInt32.v Prims.pow2 FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int FStar.Mul.op_Star FStar.Char.char_code FStar.Char.u32_of_char FStar.UInt8.t Prims.l_or FStar.UInt.size FStar.UInt8.n Prims.op_GreaterThanOrEqual FStar.UInt8.v FStar.Char.int_of_char
module LowStar.Literal

module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

open FStar.Mul

/// This module enables clients to make use of string literals in Low* as
/// shorthand syntax for immutable, always-live uint8 buffers. See
/// LowStar.printf for writing and printing string literals.

/// .. note::
///
///    This module supersedes ``C.String``.

/// As a reminder, the F* compiler enforces that string literals are UTF-8
/// encoded, and list_of_string returns the corresponding sequence of Unicode
/// scalar values (see https://erratique.ch/software/uucp/doc/Uucp.html#uminimal) for an excellent
/// crash course on Unicode.

/// When compiling with KaRaMeL, string literals are printed as series of bytes,
/// where non-alphanumeric characters are hex-encoded. For instance, if after reading
/// the C standard, the user writes ``let x = "🤮"``, then KaRaMeL will generate
/// ``const char *x = "\xf0\x9f\xa4\xae"``.

/// String literals as buffers
/// --------------------------

/// Therefore, in order to talk about the interpretation of a string literal as
/// a series of bytes, we need to define the serialization of Unicode scalar values
/// (as returned by ``String.list_of_string``) into bytes. This is a commendable and
/// noble goal, but instead, we choose to restrict ourselves to the ASCII subset of
/// UTF-8, where the byte encoding of a scalar value is the identity.
let is_ascii_char (c: Char.char) = UInt32.lt (Char.u32_of_char c) 0x80ul

let ascii_char = c:Char.char{is_ascii_char c}

let is_ascii_string (s: string) =
  List.Tot.for_all is_ascii_char (String.list_of_string s)

let ascii_string = s:string{is_ascii_string s}

let for_all_tail #a p (l: list a { Cons? l }): Lemma
  (requires (List.Tot.for_all p l))
  (ensures (List.Tot.for_all p (List.Tot.tl l)))
=
  ()

let ascii_chars_of_ascii_string (s: ascii_string):
  l:list ascii_char { List.Tot.length l = String.length s }
= List.Tot.list_refb #(Char.char) #_ (String.list_of_string s)
val u8_of_ascii_char (c: ascii_char) : x: UInt8.t{UInt8.v x = Char.int_of_char c}
c: LowStar.Literal.ascii_char -> x: FStar.UInt8.t{FStar.UInt8.v x = FStar.Char.int_of_char c}