val random_sample: len:uint32_t -> out:uint8_p ->
  ST unit random_sample_pre random_sample_post
val random_sample: len:uint32_t -> out:uint8_p ->
  ST unit random_sample_pre random_sample_post
let random_sample len out =
  OpenSSL.random_sample len out
module MiTLS.EverCrypt
open MiTLS

module B = LowStar.Buffer

module Hacl = MiTLS.EverCrypt.Hacl
module OpenSSL = MiTLS.EverCrypt.OpenSSL
module Vale = MiTLS.EverCrypt.Vale

module AC = EverCrypt.AutoConfig2
module U32 = FStar.UInt32
module HS = FStar.HyperStack

open EverCrypt.Helpers
open LowStar.BufferOps

inline_for_extraction
let vale (): Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1) =
  true

inline_for_extraction
let vale_and_aesni (): Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1) =
  AC.has_aesni ()

inline_for_extraction
let hacl (): Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1) =
  true

inline_for_extraction
let openssl (): Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1) =
  true

inline_for_extraction
let bcrypt (): Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1) =
  false

/// Random sampling

let random_init () =
  OpenSSL.random_init ()
/
prims.fst.checked MiTLS.EverCrypt.Vale.fsti.checked MiTLS.EverCrypt.OpenSSL.fsti.checked MiTLS.EverCrypt.Hacl.fsti.checked LowStar.Failure.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Hacl.Chacha20Poly1305_32.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.Full.fst.checked FStar.HyperStack.fst.checked FStar.Dyn.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.AutoConfig2.fsti.checked
MiTLS.EverCrypt.fst
len: EverCrypt.Helpers.uint32_t -> out: EverCrypt.Helpers.uint8_p
  -> FStar.HyperStack.ST.ST Prims.unit
EverCrypt.Helpers.uint32_t EverCrypt.Helpers.uint8_p MiTLS.EverCrypt.OpenSSL.random_sample Prims.unit
let random_sample len out =
  
OpenSSL.random_sample len out