let buffer_of_literal_post (s: ascii_string) (h0: HS.mem) (b: IB.ibuffer UInt8.t) (h1: HS.mem) =
  IB.frameOf b == HS.root /\ // is this really useful?
  IB.recallable b /\ (
  // An inlined version of alloc_post_mem_common, without the unused_in
  // condition, which would contradict the Stack annotation
  let s = u8s_of_ascii_string s in
  IB.live h1 b /\
  Map.domain (HS.get_hmap h1) `Set.equal` Map.domain (HS.get_hmap h0) /\
  HS.get_tip h1 == HS.get_tip h0 /\
  B.(modifies loc_none h0 h1) /\
  B.as_seq h1 b == s)
let buffer_of_literal_post (s: ascii_string) (h0: HS.mem) (b: IB.ibuffer UInt8.t) (h1: HS.mem) =
IB.frameOf b == HS.root /\ IB.recallable b /\
(let s = u8s_of_ascii_string s in
  IB.live h1 b /\ (Map.domain (HS.get_hmap h1)) `Set.equal` (Map.domain (HS.get_hmap h0)) /\
  HS.get_tip h1 == HS.get_tip h0 /\ B.(modifies loc_none h0 h1) /\ B.as_seq h1 b == s)
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_string FStar.Monotonic.HyperStack.mem LowStar.ImmutableBuffer.ibuffer FStar.UInt8.t Prims.l_and Prims.eq2 FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf LowStar.ImmutableBuffer.immutable_preorder FStar.Monotonic.HyperHeap.root LowStar.Monotonic.Buffer.recallable LowStar.Monotonic.Buffer.live FStar.Set.equal FStar.Map.domain FStar.Monotonic.Heap.heap FStar.Monotonic.HyperStack.get_hmap FStar.Monotonic.HyperStack.get_tip LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq Prims.b2t Prims.op_Equality Prims.nat FStar.Seq.Base.length FStar.List.Tot.Base.length FStar.String.char FStar.String.list_of_string LowStar.Literal.u8s_of_ascii_string Prims.logical
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)

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

/// This means that if a string literal only contains ASCII, then we can easily
/// reflect its contents in terms of uint8's, without having to talk about the utf8
/// encoding.
/// TODO: lemma: S.index (u8s_of_string s) i = String.index s i
///   (cannot be proven right now because we don't know much about String.index)
///   (is this even what we want? should we do everything in terms of list_of_string?)
let u8s_of_ascii_string (s: ascii_string):
  ss:Seq.seq UInt8.t { Seq.length ss = List.Tot.length (String.list_of_string s) }
=
  let cs = List.Tot.map u8_of_ascii_char (ascii_chars_of_ascii_string s) in
  Seq.seq_of_list cs
val buffer_of_literal_post : s: LowStar.Literal.ascii_string ->
    h0: FStar.Monotonic.HyperStack.mem ->
    b: LowStar.ImmutableBuffer.ibuffer FStar.UInt8.t ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.logical

    s: LowStar.Literal.ascii_string ->
    h0: FStar.Monotonic.HyperStack.mem ->
    b: LowStar.ImmutableBuffer.ibuffer FStar.UInt8.t ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.logical