let decrypt_opt_stdcall_st (a: algorithm { a = AES_128 \/ a = AES_256 }) =
  key:Ghost.erased (Seq.seq nat32) ->
  iv:Ghost.erased supported_iv_LE ->
  cipher_b:uint8_p ->
  cipher_len:uint64 ->
  auth_b:uint8_p ->
  auth_len:uint64 ->
  iv_b:uint8_p ->
  out_b:uint8_p ->
  tag_b:uint8_p ->
  keys_b:uint8_p ->
  hkeys_b:uint8_p ->
  scratch_b:uint8_p ->

  Stack UInt64.t
    (requires fun h0 ->
      B.disjoint tag_b out_b /\ B.disjoint tag_b hkeys_b /\
      B.disjoint tag_b cipher_b /\ B.disjoint tag_b auth_b /\
      B.disjoint tag_b iv_b /\ disjoint_or_eq tag_b keys_b /\

      B.disjoint iv_b keys_b /\ B.disjoint iv_b out_b /\
      B.disjoint iv_b cipher_b /\ B.disjoint iv_b hkeys_b /\
      B.disjoint iv_b auth_b /\

      B.disjoint out_b keys_b /\ B.disjoint out_b hkeys_b /\
      B.disjoint out_b auth_b /\ disjoint_or_eq out_b cipher_b /\

      B.disjoint cipher_b keys_b /\ B.disjoint cipher_b hkeys_b /\
      B.disjoint cipher_b auth_b /\

      disjoint_or_eq keys_b hkeys_b /\
      B.disjoint keys_b auth_b /\ B.disjoint hkeys_b auth_b /\

      B.disjoint cipher_b scratch_b /\ B.disjoint auth_b scratch_b /\
      B.disjoint iv_b scratch_b /\ B.disjoint out_b scratch_b /\
      B.disjoint tag_b scratch_b /\ B.disjoint keys_b scratch_b /\
      B.disjoint hkeys_b scratch_b /\

      B.live h0 auth_b /\ B.live h0 keys_b /\
      B.live h0 iv_b /\ B.live h0 hkeys_b /\
      B.live h0 out_b /\ B.live h0 cipher_b /\
      B.live h0 tag_b /\ B.live h0 scratch_b /\

      B.length auth_b = UInt64.v auth_len /\
      B.length iv_b = 16 /\
      B.length cipher_b = UInt64.v cipher_len /\
      B.length out_b = B.length cipher_b /\
      B.length hkeys_b = 128 /\
      B.length tag_b == 16 /\
      B.length keys_b = Vale.Wrapper.X64.AES.key_offset a /\
      B.length scratch_b = 176 /\

      aesni_enabled /\ pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ movbe_enabled /\
      is_aes_key_LE a (Ghost.reveal key) /\
      (Seq.equal (B.as_seq h0 keys_b)
        (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (key_to_round_keys_LE a (Ghost.reveal key))))) /\

      hkeys_reqs_pub (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 hkeys_b)))
        (reverse_bytes_quad32 (aes_encrypt_LE a (Ghost.reveal key) (Mkfour 0 0 0 0))) /\

      (le_bytes_to_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 iv_b)) ==
        compute_iv_BE (aes_encrypt_LE a (Ghost.reveal key) (Mkfour 0 0 0 0)) (Ghost.reveal iv))
    )
    (ensures fun h0 c h1 ->
      B.modifies (B.loc_union (B.loc_buffer scratch_b)
                 (B.loc_union (B.loc_buffer iv_b)
                 (B.loc_buffer out_b))) h0 h1 /\

      (let cipher = seq_uint8_to_seq_nat8 (B.as_seq h0 cipher_b) in
       let auth = seq_uint8_to_seq_nat8 (B.as_seq h0 auth_b) in
       let expected_tag = seq_uint8_to_seq_nat8 (B.as_seq h0 tag_b) in
       let plain, result = gcm_decrypt_LE a (seq_nat32_to_seq_nat8_LE (Ghost.reveal key)) (Ghost.reveal iv) cipher auth expected_tag in
       Seq.equal (seq_uint8_to_seq_nat8 (B.as_seq h1 out_b)) plain /\
       (UInt64.v c = 0) == result)
  )
let decrypt_opt_stdcall_st (a: algorithm{a = AES_128 \/ a = AES_256}) =

    key: Ghost.erased (Seq.seq nat32) ->
    iv: Ghost.erased supported_iv_LE ->
    cipher_b: uint8_p ->
    cipher_len: uint64 ->
    auth_b: uint8_p ->
    auth_len: uint64 ->
    iv_b: uint8_p ->
    out_b: uint8_p ->
    tag_b: uint8_p ->
    keys_b: uint8_p ->
    hkeys_b: uint8_p ->
    scratch_b: uint8_p
  -> Stack UInt64.t
      (requires
        fun h0 ->
          B.disjoint tag_b out_b /\ B.disjoint tag_b hkeys_b /\ B.disjoint tag_b cipher_b /\
          B.disjoint tag_b auth_b /\ B.disjoint tag_b iv_b /\ disjoint_or_eq tag_b keys_b /\
          B.disjoint iv_b keys_b /\ B.disjoint iv_b out_b /\ B.disjoint iv_b cipher_b /\
          B.disjoint iv_b hkeys_b /\ B.disjoint iv_b auth_b /\ B.disjoint out_b keys_b /\
          B.disjoint out_b hkeys_b /\ B.disjoint out_b auth_b /\ disjoint_or_eq out_b cipher_b /\
          B.disjoint cipher_b keys_b /\ B.disjoint cipher_b hkeys_b /\ B.disjoint cipher_b auth_b /\
          disjoint_or_eq keys_b hkeys_b /\ B.disjoint keys_b auth_b /\ B.disjoint hkeys_b auth_b /\
          B.disjoint cipher_b scratch_b /\ B.disjoint auth_b scratch_b /\ B.disjoint iv_b scratch_b /\
          B.disjoint out_b scratch_b /\ B.disjoint tag_b scratch_b /\ B.disjoint keys_b scratch_b /\
          B.disjoint hkeys_b scratch_b /\ B.live h0 auth_b /\ B.live h0 keys_b /\ B.live h0 iv_b /\
          B.live h0 hkeys_b /\ B.live h0 out_b /\ B.live h0 cipher_b /\ B.live h0 tag_b /\
          B.live h0 scratch_b /\ B.length auth_b = UInt64.v auth_len /\ B.length iv_b = 16 /\
          B.length cipher_b = UInt64.v cipher_len /\ B.length out_b = B.length cipher_b /\
          B.length hkeys_b = 128 /\ B.length tag_b == 16 /\
          B.length keys_b = Vale.Wrapper.X64.AES.key_offset a /\ B.length scratch_b = 176 /\
          aesni_enabled /\ pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ movbe_enabled /\
          is_aes_key_LE a (Ghost.reveal key) /\
          (Seq.equal (B.as_seq h0 keys_b)
              (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (key_to_round_keys_LE a
                          (Ghost.reveal key))))) /\
          hkeys_reqs_pub (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 hkeys_b)))
            (reverse_bytes_quad32 (aes_encrypt_LE a (Ghost.reveal key) (Mkfour 0 0 0 0))) /\
          (le_bytes_to_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 iv_b)) ==
            compute_iv_BE (aes_encrypt_LE a (Ghost.reveal key) (Mkfour 0 0 0 0)) (Ghost.reveal iv)))
      (ensures
        fun h0 c h1 ->
          B.modifies (B.loc_union (B.loc_buffer scratch_b)
                (B.loc_union (B.loc_buffer iv_b) (B.loc_buffer out_b)))
            h0
            h1 /\
          (let cipher = seq_uint8_to_seq_nat8 (B.as_seq h0 cipher_b) in
            let auth = seq_uint8_to_seq_nat8 (B.as_seq h0 auth_b) in
            let expected_tag = seq_uint8_to_seq_nat8 (B.as_seq h0 tag_b) in
            let plain, result =
              gcm_decrypt_LE a
                (seq_nat32_to_seq_nat8_LE (Ghost.reveal key))
                (Ghost.reveal iv)
                cipher
                auth
                expected_tag
            in
            Seq.equal (seq_uint8_to_seq_nat8 (B.as_seq h1 out_b)) plain /\
            (UInt64.v c = 0) == result))
Vale.Wrapper.X64.GCMdecryptOpt.fsti.checked
Vale.X64.CPU_Features_s.fst.checked Vale.Wrapper.X64.AES.fsti.checked Vale.Interop.Base.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.OptPublic.fsti.checked Vale.AES.GHash_s.fst.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.GCM_s.fst.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Vale.Wrapper.X64.GCMdecryptOpt.fsti
Vale.AES.AES_common_s.algorithm Prims.l_or Prims.b2t Prims.op_Equality Vale.AES.AES_common_s.AES_128 Vale.AES.AES_common_s.AES_256 FStar.Ghost.erased FStar.Seq.Base.seq Vale.Def.Types_s.nat32 Vale.AES.GCM_s.supported_iv_LE Vale.Wrapper.X64.GCMdecryptOpt.uint8_p Vale.Wrapper.X64.GCMdecryptOpt.uint64 FStar.UInt64.t FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.disjoint FStar.UInt8.t LowStar.Buffer.trivial_preorder Vale.Wrapper.X64.GCMdecryptOpt.disjoint_or_eq LowStar.Monotonic.Buffer.live Prims.int Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt64.n LowStar.Monotonic.Buffer.length FStar.UInt64.v Prims.nat Prims.eq2 Vale.Wrapper.X64.AES.key_offset Vale.X64.CPU_Features_s.aesni_enabled Vale.X64.CPU_Features_s.pclmulqdq_enabled Vale.X64.CPU_Features_s.avx_enabled Vale.X64.CPU_Features_s.sse_enabled Vale.X64.CPU_Features_s.movbe_enabled Vale.AES.AES_s.is_aes_key_LE FStar.Ghost.reveal FStar.Seq.Base.equal LowStar.Monotonic.Buffer.as_seq Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 Vale.Def.Types_s.le_seq_quad32_to_bytes Vale.AES.AES_s.key_to_round_keys_LE Vale.AES.OptPublic.hkeys_reqs_pub Vale.Def.Types_s.le_bytes_to_seq_quad32 Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 Vale.Def.Types_s.reverse_bytes_quad32 Vale.AES.AES_s.aes_encrypt_LE Vale.Def.Words_s.Mkfour Vale.Def.Types_s.quad32 Vale.Def.Types_s.le_bytes_to_quad32 Vale.AES.GCM_s.compute_iv_BE LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union LowStar.Monotonic.Buffer.loc_buffer Vale.Def.Types_s.nat8 Prims.bool Vale.Def.Words_s.nat8 Prims.logical FStar.Pervasives.Native.tuple2 Vale.AES.GCM_s.gcm_decrypt_LE Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE
module Vale.Wrapper.X64.GCMdecryptOpt

open Vale.X64.CPU_Features_s
open FStar.HyperStack.ST
module B = LowStar.Buffer
module HS = FStar.HyperStack
module DV = LowStar.BufferView.Down
module UV = LowStar.BufferView.Up
open Vale.AsLowStar.MemoryHelpers
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Types_s
open Vale.AES.GCM_helpers
open Vale.AES.AES_s
open Vale.AES.GCM_s
open Vale.AES.GHash_s
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.Interop.Base
open Vale.Arch.Types
open Vale.AES.OptPublic

let uint8_p = B.buffer UInt8.t
let uint64 = UInt64.t

let disjoint_or_eq (b1 b2:uint8_p) = B.disjoint b1 b2 \/ b1 == b2

let length_aux (b:uint8_p) : Lemma
  (requires B.length b = 176)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db

let length_aux2 (b:uint8_p) : Lemma
  (requires B.length b = 240)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db

let length_aux3 (b:uint8_p) (n:nat) : Lemma
  (requires B.length b = 16 * n)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db;
    FStar.Math.Lemmas.cancel_mul_mod n 16

let length_aux4 (b:uint8_p) : Lemma
  (requires B.length b = 16)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db

let length_aux5 (b:uint8_p) : Lemma
  (requires B.length b = 128)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db

#set-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0"

inline_for_extraction noextract
val decrypt_opt_stdcall_st : a:
      Vale.AES.AES_common_s.algorithm
        {a = Vale.AES.AES_common_s.AES_128 \/ a = Vale.AES.AES_common_s.AES_256}
  -> Type0

    a:
      Vale.AES.AES_common_s.algorithm
        {a = Vale.AES.AES_common_s.AES_128 \/ a = Vale.AES.AES_common_s.AES_256}
  -> Type0