val dh_compute:
  st: dh_state ->
  public: uint8_p ->
  public_len: uint32_t ->
  out: uint8_p ->
  ST uint32_t
  (requires fun h0 -> False)
  (ensures fun h0 _ h1 -> True)
let dh_compute st public public_len out =
  let s = !*st in
  if DH_OPENSSL? s then
    OpenSSL.dh_compute (DH_OPENSSL?.st s) public public_len out
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (dh_compute)"
val dh_compute:
  st: dh_state ->
  public: uint8_p ->
  public_len: uint32_t ->
  out: uint8_p ->
  ST uint32_t
  (requires fun h0 -> False)
  (ensures fun h0 _ h1 -> True)
let dh_compute st public public_len out =
let s = !*st in
if DH_OPENSSL? s
then OpenSSL.dh_compute (DH_OPENSSL?.st s) public public_len out
else LowStar.Failure.failwith "ERROR: inconsistent configuration (dh_compute)"
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
EverCrypt.dh_state EverCrypt.Helpers.uint8_p EverCrypt.Helpers.uint32_t EverCrypt.uu___is_DH_OPENSSL EverCrypt.OpenSSL.dh_compute EverCrypt.__proj__DH_OPENSSL__item__st Prims.bool LowStar.Failure.failwith EverCrypt.dh_state_s LowStar.BufferOps.op_Bang_Star LowStar.Buffer.trivial_preorder
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
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)"

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

/// AES128-GCM

#set-options "--admit_smt_queries true"

// TODO move to ValeGlue
private inline_for_extraction
let vale_aes128_gcm_encrypt xkey (iv:uint8_p) (ad:uint8_p) (adlen:uint32_t)
                            (plaintext:uint8_p) (len:uint32_t) (cipher:uint8_p) (tag:uint8_p) =
  push_frame ();
  let open EverCrypt.Vale in
  let iv'        = B.alloca 0uy 16ul in
  let plaintext' = B.alloca 0uy U32.(((len +^ 15ul) /^ 16ul) *^ 16ul) in
  let cipher'    = B.alloca 0uy U32.(((len +^ 15ul) /^ 16ul) *^ 16ul) in
  let ad'        = B.alloca 0uy U32.(((adlen +^ 15ul) /^ 16ul) *^ 16ul) in
  blit iv 0ul iv' 0ul 12ul;
  blit plaintext 0ul plaintext' 0ul len;
  blit ad 0ul ad' 0ul adlen;
  let b = B.alloca ({
    plain = plaintext';
    plain_len = FStar.Int.Cast.Full.uint32_to_uint64 len;
    aad = ad';
    aad_len = FStar.Int.Cast.Full.uint32_to_uint64 adlen;
    iv = iv';
    expanded_key = xkey;
    cipher = cipher';
    tag = tag
  }) 1ul in
  Vale.old_gcm128_encrypt b;
  blit cipher' 0ul cipher 0ul len;
  pop_frame ()

private inline_for_extraction
let vale_aes128_gcm_decrypt xkey (iv:uint8_p) (ad:uint8_p) (adlen:uint32_t)
                            (plaintext:uint8_p) (len:uint32_t) (cipher:uint8_p) (tag:uint8_p) =
  push_frame ();
  let open EverCrypt.Vale in
  let iv'        = B.alloca 0uy 16ul in
  let plaintext' = B.alloca 0uy U32.(((len +^ 15ul) /^ 16ul) *^ 16ul) in
  let cipher'    = B.alloca 0uy U32.(((len +^ 15ul) /^ 16ul) *^ 16ul) in
  let ad'        = B.alloca 0uy U32.(((adlen +^ 15ul) /^ 16ul) *^ 16ul) in
  blit iv 0ul iv' 0ul 12ul;
  blit cipher 0ul cipher' 0ul len;
  blit ad 0ul ad' 0ul adlen;
  let b = B.alloca ({
    plain = cipher';
    plain_len = FStar.Int.Cast.Full.uint32_to_uint64 len;
    aad = ad';
    aad_len = FStar.Int.Cast.Full.uint32_to_uint64 adlen;
    iv = iv';
    expanded_key = xkey;
    cipher = plaintext';
    tag = tag
  }) 1ul in
  let ret = Vale.old_gcm128_decrypt b in
  blit plaintext' 0ul plaintext 0ul len;
  pop_frame ();
  if ret = 0ul then 1ul else 0ul

let aes128_gcm_encrypt key iv ad adlen plaintext len cipher tag =
  if vale_and_aesni () then begin
    push_frame ();
    let expanded = B.alloca 0uy 176ul in
    Vale.old_aes128_key_expansion key expanded;
    vale_aes128_gcm_encrypt expanded iv ad adlen plaintext len cipher tag;
    pop_frame ()
  end
  else if openssl () then
    OpenSSL.aes128_gcm_encrypt key iv ad adlen plaintext len cipher tag
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (aes128_gcm_encrypt)"

let aes128_gcm_decrypt key iv ad adlen plaintext len cipher tag =
  if vale_and_aesni () then
   begin
    push_frame ();
    let expanded = B.alloca 0uy 176ul in
    Vale.old_aes128_key_expansion key expanded;
    let r = vale_aes128_gcm_decrypt expanded iv ad adlen plaintext len cipher tag in
    pop_frame ();
    r
   end
  else if openssl () then
    OpenSSL.aes128_gcm_decrypt key iv ad adlen plaintext len cipher tag
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (aes128_gcm_decrypt)"

/// AES256-GCM

// TODO move to ValeGlue
private inline_for_extraction
let vale_aes256_gcm_encrypt xkey (iv:uint8_p) (ad:uint8_p) (adlen:uint32_t)
                            (plaintext:uint8_p) (len:uint32_t) (cipher:uint8_p) (tag:uint8_p) =
  push_frame ();
  let open EverCrypt.Vale in
  let iv'        = B.alloca 0uy 16ul in
  let plaintext' = B.alloca 0uy U32.(((len +^ 15ul) /^ 16ul) *^ 16ul) in
  let cipher'    = B.alloca 0uy U32.(((len +^ 15ul) /^ 16ul) *^ 16ul) in
  let ad'        = B.alloca 0uy U32.(((adlen +^ 15ul) /^ 16ul) *^ 16ul) in
  blit iv 0ul iv' 0ul 12ul;
  blit plaintext 0ul plaintext' 0ul len;
  blit ad 0ul ad' 0ul adlen;
  let b = B.alloca ({
    plain = plaintext';
    plain_len = FStar.Int.Cast.Full.uint32_to_uint64 len;
    aad = ad';
    aad_len = FStar.Int.Cast.Full.uint32_to_uint64 adlen;
    iv = iv';
    expanded_key = xkey;
    cipher = cipher';
    tag = tag
  }) 1ul in
  Vale.old_gcm256_encrypt b;
  blit cipher' 0ul cipher 0ul len;
  pop_frame ()

private inline_for_extraction
let vale_aes256_gcm_decrypt xkey (iv:uint8_p) (ad:uint8_p) (adlen:uint32_t)
                            (plaintext:uint8_p) (len:uint32_t) (cipher:uint8_p) (tag:uint8_p) =
  push_frame ();
  let open EverCrypt.Vale in
  let iv'        = B.alloca 0uy 16ul in
  let plaintext' = B.alloca 0uy U32.(((len +^ 15ul) /^ 16ul) *^ 16ul) in
  let cipher'    = B.alloca 0uy U32.(((len +^ 15ul) /^ 16ul) *^ 16ul) in
  let ad'        = B.alloca 0uy U32.(((adlen +^ 15ul) /^ 16ul) *^ 16ul) in
  blit iv 0ul iv' 0ul 12ul;
  blit cipher 0ul cipher' 0ul len;
  blit ad 0ul ad' 0ul adlen;
  let b = B.alloca ({
    plain = cipher';
    plain_len = FStar.Int.Cast.Full.uint32_to_uint64 len;
    aad = ad';
    aad_len = FStar.Int.Cast.Full.uint32_to_uint64 adlen;
    iv = iv';
    expanded_key = xkey;
    cipher = plaintext';
    tag = tag
  }) 1ul in
  let ret = Vale.old_gcm256_decrypt b in
  blit plaintext' 0ul plaintext 0ul len;
  pop_frame ();
  if ret = 0ul then 1ul else 0ul

let aes256_gcm_encrypt key iv ad adlen plaintext len cipher tag =
  if vale_and_aesni () then begin
    push_frame ();
    let expanded = B.alloca 0uy 240ul in
    Vale.old_aes256_key_expansion key expanded;
    vale_aes256_gcm_encrypt expanded iv ad adlen plaintext len cipher tag;
    pop_frame ()
  end
  else if openssl () then
    OpenSSL.aes256_gcm_encrypt key iv ad adlen plaintext len cipher tag
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (aes256_gcm_encrypt)"

let aes256_gcm_decrypt key iv ad adlen plaintext len cipher tag =
  if vale_and_aesni () then begin
    push_frame ();
    let expanded = B.alloca 0uy 240ul in
    Vale.old_aes256_key_expansion key expanded;
    let r = vale_aes256_gcm_decrypt expanded iv ad adlen plaintext len cipher tag in
    pop_frame ();
    r
  end
  else if openssl () then
    OpenSSL.aes256_gcm_decrypt key iv ad adlen plaintext len cipher tag
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (aes256_gcm_decrypt)"


/// AEAD

[@CAbstractStruct]
private noeq type _aead_state =
  | AEAD_OPENSSL: st:Dyn.dyn -> _aead_state
  | AEAD_BCRYPT: st:Dyn.dyn -> _aead_state
  | AEAD_AES128_GCM_VALE: xkey:uint8_p -> _aead_state
  | AEAD_AES256_GCM_VALE: xkey:uint8_p -> _aead_state
  | AEAD_CHACHA20_POLY1305_HACL: k:uint8_p -> _aead_state

let aead_state_s = _aead_state

let aead_create alg k =
  let st: aead_state_s =
    match alg with
    | AES128_GCM ->
      if vale_and_aesni () then
        let xk = B.malloc HS.root 0uy 176ul in
        Vale.old_aes128_key_expansion k xk;
        AEAD_AES128_GCM_VALE xk
      else if openssl () then
        AEAD_OPENSSL (OpenSSL.aead_create OpenSSL.AES128_GCM k)
      else
        LowStar.Failure.failwith "ERROR: inconsistent configuration (aead_create/AES128_GCM)"
    | AES256_GCM ->
      if vale_and_aesni () then
        let xk = B.malloc HS.root 0uy 240ul in
        Vale.old_aes256_key_expansion k xk;
        AEAD_AES256_GCM_VALE xk
      else if openssl () then
        AEAD_OPENSSL (OpenSSL.aead_create OpenSSL.AES256_GCM k)
      else
        LowStar.Failure.failwith "ERROR: inconsistent configuration (aead_create/AES256_GCM)"
    | CHACHA20_POLY1305 ->
      if hacl () then
        let k0 = B.malloc HS.root 0uy 32ul in
        blit k 0ul k0 0ul 32ul;
        AEAD_CHACHA20_POLY1305_HACL k0
      else if openssl () then
        AEAD_OPENSSL (OpenSSL.aead_create OpenSSL.CHACHA20_POLY1305 k)
      else
        LowStar.Failure.failwith "ERROR: inconsistent configuration (aead_create/CHACHA20_POLY1305)"
  in
  B.malloc HS.root st 1ul

let aead_encrypt pkey iv ad adlen plaintext len cipher tag =
  let k = !*pkey in
  if AEAD_AES128_GCM_VALE? k then
    let xk = AEAD_AES128_GCM_VALE?.xkey k in
    vale_aes128_gcm_encrypt xk iv ad adlen plaintext len cipher tag
  else if AEAD_AES256_GCM_VALE? k then
    let xk = AEAD_AES256_GCM_VALE?.xkey k in
    vale_aes256_gcm_encrypt xk iv ad adlen plaintext len cipher tag
  else if AEAD_CHACHA20_POLY1305_HACL? k then
    let key = AEAD_CHACHA20_POLY1305_HACL?.k k in
    Hacl.Chacha20Poly1305_32.aead_encrypt key iv adlen ad len plaintext cipher tag
  else if AEAD_OPENSSL? k then
    let key = AEAD_OPENSSL?.st k in
    OpenSSL.aead_encrypt key iv ad adlen plaintext len cipher tag
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (aead_encrypt)"

let aead_decrypt pkey iv ad adlen plaintext len cipher tag =
  let k = !*pkey in
  if AEAD_AES128_GCM_VALE? k then
    let xk = AEAD_AES128_GCM_VALE?.xkey k in
    vale_aes128_gcm_decrypt xk iv ad adlen plaintext len cipher tag
  else if AEAD_AES256_GCM_VALE? k then
    let xk = AEAD_AES256_GCM_VALE?.xkey k in
    vale_aes256_gcm_decrypt xk iv ad adlen plaintext len cipher tag
  else if AEAD_CHACHA20_POLY1305_HACL? k then
    let key = AEAD_CHACHA20_POLY1305_HACL?.k k in
    let r = Hacl.Chacha20Poly1305_32.aead_decrypt key iv adlen ad len plaintext cipher tag in
    U32.(1ul -^ r)
  else if AEAD_OPENSSL? k then
    let key = AEAD_OPENSSL?.st k in
    OpenSSL.aead_decrypt key iv ad adlen plaintext len cipher tag
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (aead_decrypt)"

let aead_free pk =
  let k = !*pk in
  if AEAD_AES128_GCM_VALE? k then
    let AEAD_AES128_GCM_VALE xk = k in
    B.free xk
  else if AEAD_AES256_GCM_VALE? k then
    let AEAD_AES256_GCM_VALE xk = k in
    B.free xk
  else if AEAD_CHACHA20_POLY1305_HACL? k then
    let AEAD_CHACHA20_POLY1305_HACL key = k in
    B.free key
  else if AEAD_OPENSSL? k then
    OpenSSL.aead_free (AEAD_OPENSSL?.st k)
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (aead_free)";
  B.free pk

/// DH

[@CAbstractStruct]
private noeq type _dh_state =
  | DH_OPENSSL: st:Dyn.dyn -> _dh_state
  | DH_DUMMY // Necessary placeholder or discriminators are not defined

let dh_state_s = _dh_state

let dh_load_group dh_p dh_p_len dh_g dh_g_len dh_q dh_q_len =
  let st: dh_state_s =
    if openssl () then
      DH_OPENSSL (OpenSSL.dh_load_group dh_p dh_p_len dh_g dh_g_len dh_q dh_q_len)
    else
      LowStar.Failure.failwith "ERROR: inconsistent configuration (dh_load_group)"
  in
  B.malloc HS.root st 1ul

let dh_free_group st =
  let s : _dh_state = !*st in
  if DH_OPENSSL? s then
    OpenSSL.dh_free_group (DH_OPENSSL?.st s)
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (dh_free_group)";
  B.free st

let dh_keygen st public =
  let s = !*st in
  if DH_OPENSSL? s then
    OpenSSL.dh_keygen (DH_OPENSSL?.st s) public
  else
    LowStar.Failure.failwith "ERROR: inconsistent configuration (dh_keygen)"
val dh_compute:
  st: dh_state ->
  public: uint8_p ->
  public_len: uint32_t ->
  out: uint8_p ->
  ST uint32_t
  (requires fun h0 -> False)
  (ensures fun h0 _ h1 -> True)

    st: EverCrypt.dh_state ->
    public: EverCrypt.Helpers.uint8_p ->
    public_len: EverCrypt.Helpers.uint32_t ->
    out: EverCrypt.Helpers.uint8_p
  -> FStar.HyperStack.ST.ST EverCrypt.Helpers.uint32_t