let uint8_t = UInt8.t
let uint8_t =
UInt8.t
EverCrypt.Helpers.fsti.checked
prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked C.String.fsti.checked
EverCrypt.Helpers.fsti
FStar.UInt8.t
module EverCrypt.Helpers

module B = LowStar.Buffer

open FStar.HyperStack.ST

/// Small helpers
inline_for_extraction noextract
let (!$) = C.String.((!$))

/// For the time being, we do not write any specifications and just try to reach
/// agreement on calling conventions. A series of convenient type abbreviations
/// follows.

effect Stack_ (a: Type) = Stack a (fun _ -> True) (fun _ _ _ -> True)
val uint8_t : Prims.eqtype
Prims.eqtype