let well_formed (s:Seq.seq C.char) =
  let l = Seq.length s in
  l <= FStar.UInt.max_int 32 /\
  l >= 1 /\
  Seq.index s (l - 1) = C.char_of_uint8 0uy /\
  zero_free s
let well_formed (s: Seq.seq C.char) =
let l = Seq.length s in
l <= FStar.UInt.max_int 32 /\ l >= 1 /\ Seq.index s (l - 1) = C.char_of_uint8 0uy /\ zero_free s
C.String.fsti.checked
prims.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.String.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked C.fst.checked
C.String.fsti
FStar.Seq.Base.seq C.char Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt.max_int Prims.op_GreaterThanOrEqual Prims.op_Equality FStar.Seq.Base.index Prims.op_Subtraction C.char_of_uint8 FStar.UInt8.__uint_to_t C.String.zero_free Prims.nat FStar.Seq.Base.length Prims.logical
module C.String

module U8 = FStar.UInt8
module U32 = FStar.UInt32

module B = LowStar.Buffer
module M = LowStar.Modifies

open FStar.HyperStack.ST

let zero_free (s: Seq.seq C.char) =
  forall (i: nat). {:pattern (Seq.index s i)}
    i < Seq.length s - 1 ==> Seq.index s i <> C.char_of_uint8 0uy
val well_formed : s: FStar.Seq.Base.seq C.char -> Prims.logical
s: FStar.Seq.Base.seq C.char -> Prims.logical