val aes256_free: aes256_key ->
  ST unit aes256_free_pre aes256_free_post
val aes256_free: aes256_key ->
  ST unit aes256_free_pre aes256_free_post
let aes256_free pk =
  let k = !*pk in
  if AES256_HACL? k then
    let AES256_HACL w sbox = k in
    B.free w;
    B.free 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 (aes256_free)";
  B.free pk
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

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

let aes128_compute k plain cipher =
  let k = !*k in
  if AES128_VALE? k then
    let AES128_VALE w sbox = k in
    Vale.aes128_encrypt_one_block cipher plain w sbox
  else if AES128_HACL? k then
    let AES128_HACL w sbox = k in
    Hacl.aes128_cipher cipher plain 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_compute)"

let aes128_free pk =
  let k = !*pk in
  if AES128_VALE? k then
    let AES128_VALE w sbox = k in
    B.free w;
    B.free sbox
  else if AES128_HACL? k then
    let AES128_HACL w sbox = k in
    B.free w;
    B.free 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_free)";
  B.free pk

[@CAbstractStruct]
noeq type aes256_key_s =
  | AES256_OPENSSL: st:Dyn.dyn -> aes256_key_s
  | AES256_BCRYPT: st:Dyn.dyn -> aes256_key_s
  | AES256_HACL: w:uint8_p -> sbox:uint8_p -> aes256_key_s

let aes256_create k =
  let st =
    if hacl () then
      let w    = B.malloc HS.root 0uy 240ul in
      let sbox = B.malloc HS.root 0uy 256ul in
      Hacl.aes256_mk_sbox sbox;
      Hacl.aes256_keyExpansion k w sbox;
      AES256_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 (aes256_create)"
  in
  B.malloc HS.root st 1ul

let aes256_compute k plain cipher =
  let k = !*k in
  if AES256_HACL? k then
    let AES256_HACL w sbox = k in
    Hacl.aes256_cipher cipher plain 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 (aes256_compute)"
/
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
pk: MiTLS.EverCrypt.aes256_key -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.EverCrypt.aes256_key LowStar.Monotonic.Buffer.free MiTLS.EverCrypt.aes256_key_s LowStar.Buffer.trivial_preorder Prims.unit MiTLS.EverCrypt.uu___is_AES256_HACL EverCrypt.Helpers.uint8_p EverCrypt.Helpers.uint8_t Prims.bool LowStar.Failure.failwith LowStar.BufferOps.op_Bang_Star
let aes256_free pk =
  
let k = !*pk in
if AES256_HACL? k
then
  let AES256_HACL w sbox = k in
  B.free w;
  B.free sbox
else LowStar.Failure.failwith "ERROR: inconsistent configuration (aes256_free)";
B.free pk