val openssl: Prims.unit -> Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1)
let openssl (): Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1) =
  true
val openssl: Prims.unit -> Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1)
let openssl () : Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1) =
true
EverCrypt.fst.checked
prims.fst.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.Vale.fsti.checked EverCrypt.OpenSSL.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.Hacl.fsti.checked EverCrypt.AutoConfig2.fsti.checked
EverCrypt.fst
Prims.unit Prims.bool FStar.Monotonic.HyperStack.mem Prims.l_True LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none
module EverCrypt

module B = LowStar.Buffer

module Hacl = EverCrypt.Hacl
module OpenSSL = EverCrypt.OpenSSL
module Vale = 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
val openssl: Prims.unit -> Stack bool (fun _ -> True) (fun h0 _ h1 -> B.modifies B.loc_none h0 h1)
_: Prims.unit -> FStar.HyperStack.ST.Stack Prims.bool