let aes128_key = B.pointer aes128_key_s
let aes128_key =
B.pointer aes128_key_s
EverCrypt.fsti.checked
prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked EverCrypt.Specs.fsti.checked EverCrypt.Poly1305.fsti.checked EverCrypt.HMAC.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.Hash.fsti.checked EverCrypt.DRBG.fsti.checked EverCrypt.Curve25519.fsti.checked EverCrypt.Cipher.fsti.checked
EverCrypt.fsti
LowStar.Buffer.pointer EverCrypt.aes128_key_s
module EverCrypt

open FStar.HyperStack.ST
open EverCrypt.Helpers
open EverCrypt.Specs

module B = LowStar.Buffer

/// The EverCrypt verified cryptographic library
/// --------------------------------------------
///
/// This top-level module brings into scope all the components of EverCrypt.

include EverCrypt.Hash
include EverCrypt.HMAC
include EverCrypt.HKDF
include EverCrypt.DRBG
include EverCrypt.Poly1305
include EverCrypt.Curve25519
include EverCrypt.Cipher

/// Legacy, deprecated
/// ------------------
///
/// Unverified, legacy wrappers calling into old HACL* code. Clients should
/// abandon these in favor of the verified, properly-specified modules above.

/// Random sampling

val random_init: unit ->
  ST uint32_t random_init_pre random_init_post

val random_sample: len:uint32_t -> out:uint8_p ->
  ST unit random_sample_pre random_sample_post

val random_cleanup: unit ->
  ST unit random_cleanup_pre random_cleanup_post

/// AES block function

[@CAbstractStruct]
val aes128_key_s: Type0
val aes128_key : Type0
Type0