val aes128_create: key:uint8_p ->
  ST aes128_key aes128_create_pre aes128_create_post
val aes128_create: key:uint8_p ->
  ST aes128_key aes128_create_pre aes128_create_post
let aes128_create k =
  let st =
    if vale_and_aesni () then
      let w    = B.malloc HS.root 0uy 176ul in
      let sbox = B.malloc HS.root 0uy 256ul in
      Vale.aes128_key_expansion_sbox k w sbox;
      AES128_VALE w sbox
    else if hacl () then
      let w    = B.malloc HS.root 0uy 176ul in
      let sbox = B.malloc HS.root 0uy 256ul in
      Hacl.aes128_mk_sbox sbox;
      Hacl.aes128_keyExpansion k w sbox;
      AES128_HACL w sbox
  //  else if openssl () then
  //    OpenSSL.aes128_gcm_encrypt key iv ad adlen plaintext len cipher tag
  //  else if bcrypt () then
  //    BCrypt.aes128_gcm_encrypt key iv ad adlen plaintext len cipher tag
    else
      LowStar.Failure.failwith "ERROR: inconsistent configuration (aes128_create)"
  in
  B.malloc HS.root st 1ul
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 ()

let random_sample len out =
  OpenSSL.random_sample len out

let random_cleanup () =
  ()

/// AES128-ECB

[@CAbstractStruct]
noeq type aes128_key_s =
  | AES128_OPENSSL: st:Dyn.dyn -> aes128_key_s
  | AES128_BCRYPT: st:Dyn.dyn -> aes128_key_s
  | AES128_VALE: w:uint8_p -> sbox:uint8_p -> aes128_key_s
  | AES128_HACL: w:uint8_p -> sbox:uint8_p -> aes128_key_s
/
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
key: EverCrypt.Helpers.uint8_p -> FStar.HyperStack.ST.ST MiTLS.EverCrypt.aes128_key
EverCrypt.Helpers.uint8_p LowStar.Buffer.malloc MiTLS.EverCrypt.aes128_key_s FStar.Monotonic.HyperHeap.root FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.trivial_preorder Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length FStar.UInt32.v Prims.b2t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf LowStar.Monotonic.Buffer.freeable MiTLS.EverCrypt.AES128_VALE Prims.unit MiTLS.EverCrypt.Vale.aes128_key_expansion_sbox EverCrypt.Helpers.uint8_t FStar.UInt32.uint_to_t FStar.UInt32.t FStar.UInt8.__uint_to_t Prims.bool MiTLS.EverCrypt.AES128_HACL MiTLS.EverCrypt.Hacl.aes128_keyExpansion MiTLS.EverCrypt.Hacl.aes128_mk_sbox LowStar.Failure.failwith MiTLS.EverCrypt.hacl MiTLS.EverCrypt.vale_and_aesni MiTLS.EverCrypt.aes128_key
let aes128_create k =
  
let st =
  if vale_and_aesni ()
  then
    let w = B.malloc HS.root 0uy 176ul in
    let sbox = B.malloc HS.root 0uy 256ul in
    Vale.aes128_key_expansion_sbox k w sbox;
    AES128_VALE w sbox
  else
    if hacl ()
    then
      let w = B.malloc HS.root 0uy 176ul in
      let sbox = B.malloc HS.root 0uy 256ul in
      Hacl.aes128_mk_sbox sbox;
      Hacl.aes128_keyExpansion k w sbox;
      AES128_HACL w sbox
    else LowStar.Failure.failwith "ERROR: inconsistent configuration (aes128_create)"
in
B.malloc HS.root st 1ul