val va_wp_Gcm_blocks128
      (alg: algorithm)
      (in_b out_b: buffer128)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b hkeys_b: buffer128)
      (h_LE: quad32)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_Gcm_blocks128 (alg:algorithm) (in_b:buffer128) (out_b:buffer128) (key:(seq nat32))
  (round_keys:(seq quad32)) (keys_b:buffer128) (hkeys_b:buffer128) (h_LE:quad32) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (sse_enabled /\ Vale.X64.Decls.buffers_disjoint128 keys_b out_b /\
    Vale.X64.Decls.buffers_disjoint128 hkeys_b out_b /\ (Vale.X64.Decls.buffers_disjoint128 in_b
    out_b \/ in_b == out_b) /\ Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 1 va_s0)
    (va_get_reg64 rRax va_s0) in_b (va_get_reg64 rRdx va_s0) (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validDstAddrs128 (va_get_mem_heaplet 1 va_s0) (va_get_reg64 rRdi va_s0) out_b
    (va_get_reg64 rRdx va_s0) (va_get_mem_layout va_s0) Secret /\ va_get_reg64 rRax va_s0 + 16
    `op_Multiply` va_get_reg64 rRdx va_s0 < pow2_64 /\ va_get_reg64 rRdi va_s0 + 16 `op_Multiply`
    va_get_reg64 rRdx va_s0 < pow2_64 /\ l_and (Vale.X64.Decls.buffer_length
    #Vale.X64.Memory.vuint128 in_b == Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 out_b)
    (Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 in_b < pow2_32) /\ va_get_reg64 rRdx
    va_s0 == Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 in_b /\ va_get_xmm 9 va_s0 ==
    Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051 /\
    va_get_reg64 rRdx va_s0 < pow2_32 /\ aes_reqs alg key round_keys keys_b (va_get_reg64 rR8
    va_s0) (va_get_mem_heaplet 0 va_s0) (va_get_mem_layout va_s0) /\ pclmulqdq_enabled /\
    Vale.AES.GHash.hkeys_reqs_priv (Vale.X64.Decls.s128 (va_get_mem_heaplet 0 va_s0) hkeys_b)
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) /\ Vale.X64.Decls.validSrcAddrs128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rR9 va_s0 - 32) hkeys_b 8 (va_get_mem_layout va_s0)
    Secret) /\ (forall (va_x_mem:vale_heap) (va_x_rbx:nat64) (va_x_rdi:nat64) (va_x_r11:nat64)
    (va_x_r10:nat64) (va_x_rdx:nat64) (va_x_r12:nat64) (va_x_xmm0:quad32) (va_x_xmm1:quad32)
    (va_x_xmm2:quad32) (va_x_xmm3:quad32) (va_x_xmm4:quad32) (va_x_xmm5:quad32) (va_x_xmm6:quad32)
    (va_x_xmm7:quad32) (va_x_xmm8:quad32) (va_x_xmm11:quad32) (va_x_xmm10:quad32)
    (va_x_heap1:vale_heap) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl
    (va_upd_mem_heaplet 1 va_x_heap1 (va_upd_xmm 10 va_x_xmm10 (va_upd_xmm 11 va_x_xmm11
    (va_upd_xmm 8 va_x_xmm8 (va_upd_xmm 7 va_x_xmm7 (va_upd_xmm 6 va_x_xmm6 (va_upd_xmm 5 va_x_xmm5
    (va_upd_xmm 4 va_x_xmm4 (va_upd_xmm 3 va_x_xmm3 (va_upd_xmm 2 va_x_xmm2 (va_upd_xmm 1 va_x_xmm1
    (va_upd_xmm 0 va_x_xmm0 (va_upd_reg64 rR12 va_x_r12 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64
    rR10 va_x_r10 (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rRdi va_x_rdi (va_upd_reg64 rRbx
    va_x_rbx (va_upd_mem va_x_mem va_s0))))))))))))))))))) in va_get_ok va_sM /\
    (Vale.X64.Decls.modifies_buffer128 out_b (va_get_mem_heaplet 1 va_s0) (va_get_mem_heaplet 1
    va_sM) /\ Vale.AES.GCTR.gctr_partial alg (va_get_reg64 rRdx va_s0) (Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) in_b) (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_sM) out_b) key
    (va_get_xmm 11 va_s0) /\ va_get_xmm 11 va_sM == Vale.AES.GCTR.inc32lite (va_get_xmm 11 va_s0)
    (va_get_reg64 rRdx va_s0) /\ (va_get_reg64 rRdx va_s0 == 0 ==> l_and (va_get_xmm 8 va_sM ==
    va_get_xmm 8 va_s0) (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_sM) out_b ==
    Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) out_b)) /\ (va_get_reg64 rRdx va_s0 > 0 ==>
    l_and (va_get_reg64 rRdx va_s0 <= FStar.Seq.Base.length #Vale.X64.Decls.quad32
    (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) in_b) ==> FStar.Seq.Base.length
    #Vale.X64.Decls.quad32 (FStar.Seq.Base.slice #Vale.X64.Decls.quad32 (Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) in_b) 0 (va_get_reg64 rRdx va_s0)) > 0)
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_sM) == Vale.AES.GHash.ghash_incremental
    h_LE (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_s0)) (Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) in_b)))) ==> va_k va_sM (())))
val va_wp_Gcm_blocks128
      (alg: algorithm)
      (in_b out_b: buffer128)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b hkeys_b: buffer128)
      (h_LE: quad32)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_Gcm_blocks128
      (alg: algorithm)
      (in_b out_b: buffer128)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b hkeys_b: buffer128)
      (h_LE: quad32)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0 =
(va_get_ok va_s0 /\
  (sse_enabled /\ Vale.X64.Decls.buffers_disjoint128 keys_b out_b /\
    Vale.X64.Decls.buffers_disjoint128 hkeys_b out_b /\
    (Vale.X64.Decls.buffers_disjoint128 in_b out_b \/ in_b == out_b) /\
    Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 1 va_s0)
      (va_get_reg64 rRax va_s0)
      in_b
      (va_get_reg64 rRdx va_s0)
      (va_get_mem_layout va_s0)
      Secret /\
    Vale.X64.Decls.validDstAddrs128 (va_get_mem_heaplet 1 va_s0)
      (va_get_reg64 rRdi va_s0)
      out_b
      (va_get_reg64 rRdx va_s0)
      (va_get_mem_layout va_s0)
      Secret /\ va_get_reg64 rRax va_s0 + 16 `op_Multiply` (va_get_reg64 rRdx va_s0) < pow2_64 /\
    va_get_reg64 rRdi va_s0 + 16 `op_Multiply` (va_get_reg64 rRdx va_s0) < pow2_64 /\
    l_and (Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 in_b ==
        Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 out_b)
      (Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 in_b < pow2_32) /\
    va_get_reg64 rRdx va_s0 == Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 in_b /\
    va_get_xmm 9 va_s0 ==
    Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051 /\
    va_get_reg64 rRdx va_s0 < pow2_32 /\
    aes_reqs alg
      key
      round_keys
      keys_b
      (va_get_reg64 rR8 va_s0)
      (va_get_mem_heaplet 0 va_s0)
      (va_get_mem_layout va_s0) /\ pclmulqdq_enabled /\
    Vale.AES.GHash.hkeys_reqs_priv (Vale.X64.Decls.s128 (va_get_mem_heaplet 0 va_s0) hkeys_b)
      (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) /\
    Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0)
      (va_get_reg64 rR9 va_s0 - 32)
      hkeys_b
      8
      (va_get_mem_layout va_s0)
      Secret) /\
  (forall (va_x_mem: vale_heap) (va_x_rbx: nat64) (va_x_rdi: nat64) (va_x_r11: nat64)
      (va_x_r10: nat64) (va_x_rdx: nat64) (va_x_r12: nat64) (va_x_xmm0: quad32) (va_x_xmm1: quad32)
      (va_x_xmm2: quad32) (va_x_xmm3: quad32) (va_x_xmm4: quad32) (va_x_xmm5: quad32)
      (va_x_xmm6: quad32) (va_x_xmm7: quad32) (va_x_xmm8: quad32) (va_x_xmm11: quad32)
      (va_x_xmm10: quad32) (va_x_heap1: vale_heap) (va_x_efl: Vale.X64.Flags.t).
      let va_sM =
        va_upd_flags va_x_efl
          (va_upd_mem_heaplet 1
              va_x_heap1
              (va_upd_xmm 10
                  va_x_xmm10
                  (va_upd_xmm 11
                      va_x_xmm11
                      (va_upd_xmm 8
                          va_x_xmm8
                          (va_upd_xmm 7
                              va_x_xmm7
                              (va_upd_xmm 6
                                  va_x_xmm6
                                  (va_upd_xmm 5
                                      va_x_xmm5
                                      (va_upd_xmm 4
                                          va_x_xmm4
                                          (va_upd_xmm 3
                                              va_x_xmm3
                                              (va_upd_xmm 2
                                                  va_x_xmm2
                                                  (va_upd_xmm 1
                                                      va_x_xmm1
                                                      (va_upd_xmm 0
                                                          va_x_xmm0
                                                          (va_upd_reg64 rR12
                                                              va_x_r12
                                                              (va_upd_reg64 rRdx
                                                                  va_x_rdx
                                                                  (va_upd_reg64 rR10
                                                                      va_x_r10
                                                                      (va_upd_reg64 rR11
                                                                          va_x_r11
                                                                          (va_upd_reg64 rRdi
                                                                              va_x_rdi
                                                                              (va_upd_reg64 rRbx
                                                                                  va_x_rbx
                                                                                  (va_upd_mem va_x_mem
                                                                                      va_s0)))))))))
                                              ))))))))))
      in
      va_get_ok va_sM /\
      (Vale.X64.Decls.modifies_buffer128 out_b
          (va_get_mem_heaplet 1 va_s0)
          (va_get_mem_heaplet 1 va_sM) /\
        Vale.AES.GCTR.gctr_partial alg
          (va_get_reg64 rRdx va_s0)
          (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) in_b)
          (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_sM) out_b)
          key
          (va_get_xmm 11 va_s0) /\
        va_get_xmm 11 va_sM ==
        Vale.AES.GCTR.inc32lite (va_get_xmm 11 va_s0) (va_get_reg64 rRdx va_s0) /\
        (va_get_reg64 rRdx va_s0 == 0 ==>
          l_and (va_get_xmm 8 va_sM == va_get_xmm 8 va_s0)
            (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_sM) out_b ==
              Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) out_b)) /\
        (va_get_reg64 rRdx va_s0 > 0 ==>
          l_and (va_get_reg64 rRdx va_s0 <=
              FStar.Seq.Base.length #Vale.X64.Decls.quad32
                (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) in_b) ==>
              FStar.Seq.Base.length #Vale.X64.Decls.quad32
                (FStar.Seq.Base.slice #Vale.X64.Decls.quad32
                    (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) in_b)
                    0
                    (va_get_reg64 rRdx va_s0)) >
              0)
            (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_sM) ==
              Vale.AES.GHash.ghash_incremental h_LE
                (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_s0))
                (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) in_b)))) ==>
      va_k va_sM (())))
Vale.AES.X64.GCMdecryptOpt.fst.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.Stack.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsVector.fsti.checked Vale.X64.InsStack.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.InsAes.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Poly1305.Math.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Lib.Meta.fsti.checked Vale.Lib.Basic.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.AES.X64.GHash.fsti.checked Vale.AES.X64.GF128_Mul.fsti.checked Vale.AES.X64.GCTR.fsti.checked Vale.AES.X64.GCMencryptOpt.fsti.checked Vale.AES.X64.AESopt2.fsti.checked Vale.AES.X64.AESopt.fsti.checked Vale.AES.X64.AESGCM.fsti.checked Vale.AES.X64.AES.fsti.checked Vale.AES.OptPublic.fsti.checked Vale.AES.GHash_s.fst.checked Vale.AES.GHash.fsti.checked Vale.AES.GF128_s.fsti.checked Vale.AES.GF128.fsti.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.GCM.fsti.checked Vale.AES.AES_s.fst.checked Vale.AES.AES_common_s.fst.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.X64.GCMdecryptOpt.fst
Vale.AES.AES_common_s.algorithm Vale.X64.Memory.buffer128 FStar.Seq.Base.seq Vale.X64.Memory.nat32 Vale.X64.Decls.quad32 Vale.X64.Decls.va_state Prims.unit Prims.l_and Prims.b2t Vale.X64.Decls.va_get_ok Vale.X64.CPU_Features_s.sse_enabled Vale.X64.Decls.buffers_disjoint128 Prims.l_or Prims.eq2 Vale.X64.Decls.validSrcAddrs128 Vale.X64.Decls.va_get_mem_heaplet Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRax Vale.X64.Machine_s.rRdx Vale.X64.Decls.va_get_mem_layout Vale.Arch.HeapTypes_s.Secret Vale.X64.Decls.validDstAddrs128 Vale.X64.Machine_s.rRdi Prims.op_LessThan Prims.op_Addition Prims.op_Multiply Vale.X64.Machine_s.pow2_64 Prims.nat Vale.X64.Decls.buffer_length Vale.X64.Memory.vuint128 Vale.X64.Machine_s.pow2_32 Vale.Def.Words_s.four Vale.Def.Types_s.nat32 Vale.X64.Decls.va_get_xmm Vale.Def.Words_s.Mkfour Vale.AES.X64.GCMencryptOpt.aes_reqs Vale.X64.Machine_s.rR8 Vale.X64.CPU_Features_s.pclmulqdq_enabled Vale.AES.GHash.hkeys_reqs_priv Vale.X64.Decls.s128 Vale.Def.Types_s.reverse_bytes_quad32 Prims.op_Subtraction Vale.X64.Machine_s.rR9 Prims.l_Forall Vale.X64.InsBasic.vale_heap Vale.X64.Memory.nat64 Vale.X64.Flags.t Prims.l_imp Vale.X64.Decls.modifies_buffer128 Vale.AES.GCTR.gctr_partial Vale.Def.Types_s.quad32 Vale.AES.GCTR.inc32lite Prims.int Prims.op_GreaterThan Prims.op_LessThanOrEqual FStar.Seq.Base.length FStar.Seq.Base.slice Vale.AES.GHash.ghash_incremental Vale.X64.State.vale_state Vale.X64.Decls.va_upd_flags Vale.X64.Decls.va_upd_mem_heaplet Vale.X64.Decls.va_upd_xmm Vale.X64.Decls.va_upd_reg64 Vale.X64.Machine_s.rR12 Vale.X64.Machine_s.rR10 Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rRbx Vale.X64.Decls.va_upd_mem
module Vale.AES.X64.GCMdecryptOpt
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open FStar.Seq
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.AES.AES_s
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.AES.GCM
open Vale.AES.GHash_s
open Vale.AES.GHash
open Vale.AES.GCM_s
open Vale.AES.X64.AES
open Vale.AES.GF128_s
open Vale.AES.GF128
open Vale.Poly1305.Math
open Vale.AES.GCM_helpers
open Vale.AES.X64.GHash
open Vale.AES.X64.GCTR
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsVector
open Vale.X64.InsStack
open Vale.X64.InsAes
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.AES.X64.GF128_Mul
open Vale.X64.Stack
open Vale.X64.CPU_Features_s
open Vale.Math.Poly2.Bits_s
open Vale.AES.X64.AESopt
open Vale.AES.X64.AESGCM
open Vale.AES.X64.AESopt2
open Vale.Lib.Meta
open Vale.AES.X64.GCMencryptOpt
open Vale.AES.OptPublic
open Vale.Lib.Basic
#reset-options "--z3rlimit 20 --max_ifuel 0"
//-- Gcm_extra_bytes

val va_code_Gcm_extra_bytes : alg:algorithm -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Gcm_extra_bytes alg =
  (va_Block (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 5) (va_op_xmm_xmm 0)
    (va_op_reg_opr64_reg64 rRax) 0 Secret) (va_CCons (va_code_Mov128 (va_op_xmm_xmm 10)
    (va_op_xmm_xmm 0)) (va_CCons (va_code_Ghash_extra_bytes ()) (va_CCons (va_code_Mov128
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 11)) (va_CCons (va_code_Pshufb (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 9)) (va_CCons (va_code_AESEncryptBlock alg) (va_CCons (va_code_Pxor
    (va_op_xmm_xmm 10) (va_op_xmm_xmm 0)) (va_CCons (va_code_Store128_buffer
    (va_op_heaplet_mem_heaplet 5) (va_op_reg_opr64_reg64 rRax) (va_op_xmm_xmm 10) 0 Secret)
    (va_CNil ()))))))))))

val va_codegen_success_Gcm_extra_bytes : alg:algorithm -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Gcm_extra_bytes alg =
  (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 5) (va_op_xmm_xmm 0)
    (va_op_reg_opr64_reg64 rRax) 0 Secret) (va_pbool_and (va_codegen_success_Mov128 (va_op_xmm_xmm
    10) (va_op_xmm_xmm 0)) (va_pbool_and (va_codegen_success_Ghash_extra_bytes ()) (va_pbool_and
    (va_codegen_success_Mov128 (va_op_xmm_xmm 0) (va_op_xmm_xmm 11)) (va_pbool_and
    (va_codegen_success_Pshufb (va_op_xmm_xmm 0) (va_op_xmm_xmm 9)) (va_pbool_and
    (va_codegen_success_AESEncryptBlock alg) (va_pbool_and (va_codegen_success_Pxor (va_op_xmm_xmm
    10) (va_op_xmm_xmm 0)) (va_pbool_and (va_codegen_success_Store128_buffer
    (va_op_heaplet_mem_heaplet 5) (va_op_reg_opr64_reg64 rRax) (va_op_xmm_xmm 10) 0 Secret)
    (va_ttrue ())))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Gcm_extra_bytes (va_mods:va_mods_t) (alg:algorithm) (inout_b:buffer128) (key:(seq
  nat32)) (round_keys:(seq quad32)) (keys_b:buffer128) (hkeys_b:buffer128) (total_bytes:nat)
  (old_hash:quad32) (completed_quads:(seq quad32)) (h_LE:quad32) : (va_quickCode unit
  (va_code_Gcm_extra_bytes alg)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let (len:(va_int_range
    1 1)) = 1 in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 188 column 19 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 5) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64
    rRax) 0 Secret inout_b 0) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 189 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 10) (va_op_xmm_xmm 0)) (fun (va_s:va_state) _ -> let
    (hash_input:quad32) = va_get_xmm 0 va_s in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 193 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Ghash_extra_bytes hkeys_b total_bytes old_hash h_LE completed_quads) (fun
    (va_s:va_state) _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 194 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (FStar.Seq.Base.equal #Vale.X64.Decls.quad32 (Vale.X64.Decls.s128 (va_get_mem_heaplet 5 va_s)
    inout_b) (FStar.Seq.Base.create #quad32 1 hash_input)) (let (snap:(FStar.Seq.Base.seq
    Vale.X64.Decls.quad32)) = Vale.X64.Decls.s128 (va_get_mem_heaplet 5 va_s) inout_b in va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 198 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 0) (va_op_xmm_xmm 11)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 199 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Pshufb (va_op_xmm_xmm 0) (va_op_xmm_xmm 9)) (fun (va_s:va_state) _ -> va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 200 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_AESEncryptBlock alg (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 11 va_s)) key
    round_keys keys_b) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 201 column 26 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_s.aes_encrypt_LE_reveal ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 204 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Pxor (va_op_xmm_xmm 10) (va_op_xmm_xmm 0)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 205 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Store128_buffer (va_op_heaplet_mem_heaplet 5) (va_op_reg_opr64_reg64 rRax)
    (va_op_xmm_xmm 10) 0 Secret inout_b 0) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 207 column 24 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (fun (_:unit) -> Vale.AES.GCTR.gctr_partial_reveal ()) (va_QEmpty (()))))))))))))))


val va_lemma_Gcm_extra_bytes : va_b0:va_code -> va_s0:va_state -> alg:algorithm ->
  inout_b:buffer128 -> key:(seq nat32) -> round_keys:(seq quad32) -> keys_b:buffer128 ->
  hkeys_b:buffer128 -> total_bytes:nat -> old_hash:quad32 -> completed_quads:(seq quad32) ->
  h_LE:quad32
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Gcm_extra_bytes alg) va_s0 /\ va_get_ok va_s0 /\ (let
    (len:(va_int_range 1 1)) = 1 in sse_enabled /\ Vale.X64.Decls.buffers_disjoint128 keys_b
    inout_b /\ Vale.X64.Decls.buffers_disjoint128 hkeys_b inout_b /\
    Vale.X64.Decls.validDstAddrs128 (va_get_mem_heaplet 5 va_s0) (va_get_reg64 rRax va_s0) inout_b
    len (va_get_mem_layout va_s0) Secret /\ len == Vale.X64.Decls.buffer_length
    #Vale.X64.Memory.vuint128 inout_b /\ va_get_xmm 9 va_s0 == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051 /\ aes_reqs alg key round_keys
    keys_b (va_get_reg64 rR8 va_s0) (va_get_mem_heaplet 0 va_s0) (va_get_mem_layout va_s0) /\
    pclmulqdq_enabled /\ Vale.AES.GHash.hkeys_reqs_priv (Vale.X64.Decls.s128 (va_get_mem_heaplet 0
    va_s0) hkeys_b) (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) /\ Vale.X64.Decls.validSrcAddrs128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rR9 va_s0 - 32) hkeys_b 8 (va_get_mem_layout va_s0)
    Secret /\ va_get_xmm 8 va_s0 == Vale.Def.Types_s.reverse_bytes_quad32
    (Vale.AES.GHash.ghash_incremental0 h_LE old_hash completed_quads) /\ FStar.Seq.Base.length
    #quad32 completed_quads == total_bytes `op_Division` 16 /\ total_bytes < 16 `op_Multiply`
    FStar.Seq.Base.length #quad32 completed_quads + 16 /\ va_get_reg64 rR10 va_s0 == total_bytes
    `op_Modulus` 16 /\ total_bytes `op_Modulus` 16 =!= 0 /\ (0 < total_bytes /\ total_bytes < 16
    `op_Multiply` Vale.AES.GCM_helpers.bytes_to_quad_size total_bytes) /\ 16 `op_Multiply`
    (Vale.AES.GCM_helpers.bytes_to_quad_size total_bytes - 1) < total_bytes)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (len:(va_int_range 1 1)) = 1 in Vale.X64.Decls.modifies_buffer128 inout_b
    (va_get_mem_heaplet 5 va_s0) (va_get_mem_heaplet 5 va_sM) /\ Vale.AES.GCTR.gctr_partial alg len
    (Vale.X64.Decls.s128 (va_get_mem_heaplet 5 va_s0) inout_b) (Vale.X64.Decls.s128
    (va_get_mem_heaplet 5 va_sM) inout_b) key (va_get_xmm 11 va_s0) /\ (let raw_quads =
    FStar.Seq.Base.append #quad32 completed_quads (Vale.X64.Decls.s128 (va_get_mem_heaplet 5 va_s0)
    inout_b) in let input_bytes = FStar.Seq.Base.slice #Vale.Def.Types_s.nat8
    (Vale.Def.Types_s.le_seq_quad32_to_bytes raw_quads) 0 total_bytes in let padded_bytes =
    Vale.AES.GCTR_s.pad_to_128_bits input_bytes in let input_quads =
    Vale.Def.Types_s.le_bytes_to_seq_quad32 padded_bytes in l_and (FStar.Seq.Base.length
    #Vale.Def.Types_s.quad32 input_quads > 0) (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8
    va_sM) == Vale.AES.GHash.ghash_incremental h_LE old_hash input_quads))) /\ va_state_eq va_sM
    (va_update_flags va_sM (va_update_mem_heaplet 5 va_sM (va_update_xmm 10 va_sM (va_update_xmm 8
    va_sM (va_update_xmm 7 va_sM (va_update_xmm 6 va_sM (va_update_xmm 5 va_sM (va_update_xmm 4
    va_sM (va_update_xmm 3 va_sM (va_update_xmm 2 va_sM (va_update_xmm 1 va_sM (va_update_xmm 0
    va_sM (va_update_reg64 rR11 va_sM (va_update_reg64 rRcx va_sM (va_update_ok va_sM
    (va_update_mem va_sM va_s0))))))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Gcm_extra_bytes va_b0 va_s0 alg inout_b key round_keys keys_b hkeys_b total_bytes
  old_hash completed_quads h_LE =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 5; va_Mod_xmm 10; va_Mod_xmm 8;
    va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm
    1; va_Mod_xmm 0; va_Mod_reg64 rR11; va_Mod_reg64 rRcx; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Gcm_extra_bytes va_mods alg inout_b key round_keys keys_b hkeys_b
    total_bytes old_hash completed_quads h_LE in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Gcm_extra_bytes alg) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 121 column 1 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_get_ok va_sM) /\ (let (len:(va_int_range 1 1)) = 1 in label va_range1
    "***** POSTCONDITION NOT MET AT line 174 column 55 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (Vale.X64.Decls.modifies_buffer128 inout_b (va_get_mem_heaplet 5 va_s0) (va_get_mem_heaplet 5
    va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 177 column 95 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (Vale.AES.GCTR.gctr_partial alg len (Vale.X64.Decls.s128 (va_get_mem_heaplet 5 va_s0) inout_b)
    (Vale.X64.Decls.s128 (va_get_mem_heaplet 5 va_sM) inout_b) key (va_get_xmm 11 va_s0)) /\ label
    va_range1
    "***** POSTCONDITION NOT MET AT line 180 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (let raw_quads = FStar.Seq.Base.append #quad32 completed_quads (Vale.X64.Decls.s128
    (va_get_mem_heaplet 5 va_s0) inout_b) in label va_range1
    "***** POSTCONDITION NOT MET AT line 181 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (let input_bytes = FStar.Seq.Base.slice #Vale.Def.Types_s.nat8
    (Vale.Def.Types_s.le_seq_quad32_to_bytes raw_quads) 0 total_bytes in label va_range1
    "***** POSTCONDITION NOT MET AT line 182 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (let padded_bytes = Vale.AES.GCTR_s.pad_to_128_bits input_bytes in label va_range1
    "***** POSTCONDITION NOT MET AT line 183 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (let input_quads = Vale.Def.Types_s.le_bytes_to_seq_quad32 padded_bytes in label va_range1
    "***** POSTCONDITION NOT MET AT line 186 column 59 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (l_and (FStar.Seq.Base.length #Vale.Def.Types_s.quad32 input_quads > 0)
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_sM) == Vale.AES.GHash.ghash_incremental
    h_LE old_hash input_quads)))))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 5; va_Mod_xmm 10; va_Mod_xmm 8; va_Mod_xmm
    7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1;
    va_Mod_xmm 0; va_Mod_reg64 rR11; va_Mod_reg64 rRcx; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Gcm_extra_bytes (alg:algorithm) (inout_b:buffer128) (key:(seq nat32)) (round_keys:(seq
  quad32)) (keys_b:buffer128) (hkeys_b:buffer128) (total_bytes:nat) (old_hash:quad32)
  (completed_quads:(seq quad32)) (h_LE:quad32) (va_s0:va_state) (va_k:(va_state -> unit -> Type0))
  : Type0 =
  (va_get_ok va_s0 /\ (let (len:(va_int_range 1 1)) = 1 in sse_enabled /\
    Vale.X64.Decls.buffers_disjoint128 keys_b inout_b /\ Vale.X64.Decls.buffers_disjoint128 hkeys_b
    inout_b /\ Vale.X64.Decls.validDstAddrs128 (va_get_mem_heaplet 5 va_s0) (va_get_reg64 rRax
    va_s0) inout_b len (va_get_mem_layout va_s0) Secret /\ len == Vale.X64.Decls.buffer_length
    #Vale.X64.Memory.vuint128 inout_b /\ va_get_xmm 9 va_s0 == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051 /\ aes_reqs alg key round_keys
    keys_b (va_get_reg64 rR8 va_s0) (va_get_mem_heaplet 0 va_s0) (va_get_mem_layout va_s0) /\
    pclmulqdq_enabled /\ Vale.AES.GHash.hkeys_reqs_priv (Vale.X64.Decls.s128 (va_get_mem_heaplet 0
    va_s0) hkeys_b) (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) /\ Vale.X64.Decls.validSrcAddrs128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rR9 va_s0 - 32) hkeys_b 8 (va_get_mem_layout va_s0)
    Secret /\ va_get_xmm 8 va_s0 == Vale.Def.Types_s.reverse_bytes_quad32
    (Vale.AES.GHash.ghash_incremental0 h_LE old_hash completed_quads) /\ FStar.Seq.Base.length
    #quad32 completed_quads == total_bytes `op_Division` 16 /\ total_bytes < 16 `op_Multiply`
    FStar.Seq.Base.length #quad32 completed_quads + 16 /\ va_get_reg64 rR10 va_s0 == total_bytes
    `op_Modulus` 16 /\ total_bytes `op_Modulus` 16 =!= 0 /\ (0 < total_bytes /\ total_bytes < 16
    `op_Multiply` Vale.AES.GCM_helpers.bytes_to_quad_size total_bytes) /\ 16 `op_Multiply`
    (Vale.AES.GCM_helpers.bytes_to_quad_size total_bytes - 1) < total_bytes) /\ (forall
    (va_x_mem:vale_heap) (va_x_rcx:nat64) (va_x_r11:nat64) (va_x_xmm0:quad32) (va_x_xmm1:quad32)
    (va_x_xmm2:quad32) (va_x_xmm3:quad32) (va_x_xmm4:quad32) (va_x_xmm5:quad32) (va_x_xmm6:quad32)
    (va_x_xmm7:quad32) (va_x_xmm8:quad32) (va_x_xmm10:quad32) (va_x_heap5:vale_heap)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_mem_heaplet 5
    va_x_heap5 (va_upd_xmm 10 va_x_xmm10 (va_upd_xmm 8 va_x_xmm8 (va_upd_xmm 7 va_x_xmm7
    (va_upd_xmm 6 va_x_xmm6 (va_upd_xmm 5 va_x_xmm5 (va_upd_xmm 4 va_x_xmm4 (va_upd_xmm 3 va_x_xmm3
    (va_upd_xmm 2 va_x_xmm2 (va_upd_xmm 1 va_x_xmm1 (va_upd_xmm 0 va_x_xmm0 (va_upd_reg64 rR11
    va_x_r11 (va_upd_reg64 rRcx va_x_rcx (va_upd_mem va_x_mem va_s0)))))))))))))) in va_get_ok
    va_sM /\ (let (len:(va_int_range 1 1)) = 1 in Vale.X64.Decls.modifies_buffer128 inout_b
    (va_get_mem_heaplet 5 va_s0) (va_get_mem_heaplet 5 va_sM) /\ Vale.AES.GCTR.gctr_partial alg len
    (Vale.X64.Decls.s128 (va_get_mem_heaplet 5 va_s0) inout_b) (Vale.X64.Decls.s128
    (va_get_mem_heaplet 5 va_sM) inout_b) key (va_get_xmm 11 va_s0) /\ (let raw_quads =
    FStar.Seq.Base.append #quad32 completed_quads (Vale.X64.Decls.s128 (va_get_mem_heaplet 5 va_s0)
    inout_b) in let input_bytes = FStar.Seq.Base.slice #Vale.Def.Types_s.nat8
    (Vale.Def.Types_s.le_seq_quad32_to_bytes raw_quads) 0 total_bytes in let padded_bytes =
    Vale.AES.GCTR_s.pad_to_128_bits input_bytes in let input_quads =
    Vale.Def.Types_s.le_bytes_to_seq_quad32 padded_bytes in l_and (FStar.Seq.Base.length
    #Vale.Def.Types_s.quad32 input_quads > 0) (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8
    va_sM) == Vale.AES.GHash.ghash_incremental h_LE old_hash input_quads))) ==> va_k va_sM (())))


val va_wpProof_Gcm_extra_bytes : alg:algorithm -> inout_b:buffer128 -> key:(seq nat32) ->
  round_keys:(seq quad32) -> keys_b:buffer128 -> hkeys_b:buffer128 -> total_bytes:nat ->
  old_hash:quad32 -> completed_quads:(seq quad32) -> h_LE:quad32 -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Gcm_extra_bytes alg inout_b key round_keys keys_b hkeys_b
    total_bytes old_hash completed_quads h_LE va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Gcm_extra_bytes alg) ([va_Mod_flags;
    va_Mod_mem_heaplet 5; va_Mod_xmm 10; va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5;
    va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_xmm 0; va_Mod_reg64 rR11;
    va_Mod_reg64 rRcx; va_Mod_mem]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Gcm_extra_bytes alg inout_b key round_keys keys_b hkeys_b total_bytes old_hash
  completed_quads h_LE va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Gcm_extra_bytes (va_code_Gcm_extra_bytes alg) va_s0 alg inout_b key
    round_keys keys_b hkeys_b total_bytes old_hash completed_quads h_LE in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_mem_heaplet 5 va_sM (va_update_xmm 10
    va_sM (va_update_xmm 8 va_sM (va_update_xmm 7 va_sM (va_update_xmm 6 va_sM (va_update_xmm 5
    va_sM (va_update_xmm 4 va_sM (va_update_xmm 3 va_sM (va_update_xmm 2 va_sM (va_update_xmm 1
    va_sM (va_update_xmm 0 va_sM (va_update_reg64 rR11 va_sM (va_update_reg64 rRcx va_sM
    (va_update_ok va_sM (va_update_mem va_sM va_s0)))))))))))))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 5; va_Mod_xmm 10; va_Mod_xmm 8; va_Mod_xmm
    7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1;
    va_Mod_xmm 0; va_Mod_reg64 rR11; va_Mod_reg64 rRcx; va_Mod_mem]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Gcm_extra_bytes (alg:algorithm) (inout_b:buffer128) (key:(seq nat32)) (round_keys:(seq
  quad32)) (keys_b:buffer128) (hkeys_b:buffer128) (total_bytes:nat) (old_hash:quad32)
  (completed_quads:(seq quad32)) (h_LE:quad32) : (va_quickCode unit (va_code_Gcm_extra_bytes alg)) =
  (va_QProc (va_code_Gcm_extra_bytes alg) ([va_Mod_flags; va_Mod_mem_heaplet 5; va_Mod_xmm 10;
    va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm
    2; va_Mod_xmm 1; va_Mod_xmm 0; va_Mod_reg64 rR11; va_Mod_reg64 rRcx; va_Mod_mem])
    (va_wp_Gcm_extra_bytes alg inout_b key round_keys keys_b hkeys_b total_bytes old_hash
    completed_quads h_LE) (va_wpProof_Gcm_extra_bytes alg inout_b key round_keys keys_b hkeys_b
    total_bytes old_hash completed_quads h_LE))
//--
//-- Gcm_blocks128

val va_code_Gcm_blocks128 : alg:algorithm -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Gcm_blocks128 alg =
  (va_Block (va_CCons (va_code_Mov64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRdi))
    (va_CCons (va_code_Mov64 (va_op_dst_opr64_reg64 rR12) (va_op_opr64_reg64 rRdx)) (va_CCons
    (va_code_Mov64 (va_op_dst_opr64_reg64 rRdi) (va_op_opr64_reg64 rRax)) (va_CCons
    (va_code_Ghash_buffer ()) (va_CCons (va_code_Mov64 (va_op_dst_opr64_reg64 rRdi)
    (va_op_opr64_reg64 rRbx)) (va_CCons (va_code_Mov64 (va_op_dst_opr64_reg64 rRdx)
    (va_op_opr64_reg64 rR12)) (va_CCons (va_code_Gctr_blocks128 alg) (va_CNil ())))))))))

val va_codegen_success_Gcm_blocks128 : alg:algorithm -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Gcm_blocks128 alg =
  (va_pbool_and (va_codegen_success_Mov64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRdi))
    (va_pbool_and (va_codegen_success_Mov64 (va_op_dst_opr64_reg64 rR12) (va_op_opr64_reg64 rRdx))
    (va_pbool_and (va_codegen_success_Mov64 (va_op_dst_opr64_reg64 rRdi) (va_op_opr64_reg64 rRax))
    (va_pbool_and (va_codegen_success_Ghash_buffer ()) (va_pbool_and (va_codegen_success_Mov64
    (va_op_dst_opr64_reg64 rRdi) (va_op_opr64_reg64 rRbx)) (va_pbool_and (va_codegen_success_Mov64
    (va_op_dst_opr64_reg64 rRdx) (va_op_opr64_reg64 rR12)) (va_pbool_and
    (va_codegen_success_Gctr_blocks128 alg) (va_ttrue ()))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Gcm_blocks128 (va_mods:va_mods_t) (alg:algorithm) (in_b:buffer128) (out_b:buffer128)
  (key:(seq nat32)) (round_keys:(seq quad32)) (keys_b:buffer128) (hkeys_b:buffer128) (h_LE:quad32)
  : (va_quickCode unit (va_code_Gcm_blocks128 alg)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 274 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rRdi)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 275 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rR12) (va_op_opr64_reg64 rRdx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 276 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRdi) (va_op_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 277 column 17 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Ghash_buffer hkeys_b in_b h_LE (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8
    va_old_s))) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 278 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRdi) (va_op_opr64_reg64 rRbx)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 279 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Mov64 (va_op_dst_opr64_reg64 rRdx) (va_op_opr64_reg64 rR12)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 280 column 19 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_quick_Gctr_blocks128 alg in_b out_b key round_keys keys_b) (va_QEmpty (()))))))))))


val va_lemma_Gcm_blocks128 : va_b0:va_code -> va_s0:va_state -> alg:algorithm -> in_b:buffer128 ->
  out_b:buffer128 -> key:(seq nat32) -> round_keys:(seq quad32) -> keys_b:buffer128 ->
  hkeys_b:buffer128 -> h_LE:quad32
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Gcm_blocks128 alg) va_s0 /\ va_get_ok va_s0 /\
    (sse_enabled /\ Vale.X64.Decls.buffers_disjoint128 keys_b out_b /\
    Vale.X64.Decls.buffers_disjoint128 hkeys_b out_b /\ (Vale.X64.Decls.buffers_disjoint128 in_b
    out_b \/ in_b == out_b) /\ Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 1 va_s0)
    (va_get_reg64 rRax va_s0) in_b (va_get_reg64 rRdx va_s0) (va_get_mem_layout va_s0) Secret /\
    Vale.X64.Decls.validDstAddrs128 (va_get_mem_heaplet 1 va_s0) (va_get_reg64 rRdi va_s0) out_b
    (va_get_reg64 rRdx va_s0) (va_get_mem_layout va_s0) Secret /\ va_get_reg64 rRax va_s0 + 16
    `op_Multiply` va_get_reg64 rRdx va_s0 < pow2_64 /\ va_get_reg64 rRdi va_s0 + 16 `op_Multiply`
    va_get_reg64 rRdx va_s0 < pow2_64 /\ l_and (Vale.X64.Decls.buffer_length
    #Vale.X64.Memory.vuint128 in_b == Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 out_b)
    (Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 in_b < pow2_32) /\ va_get_reg64 rRdx
    va_s0 == Vale.X64.Decls.buffer_length #Vale.X64.Memory.vuint128 in_b /\ va_get_xmm 9 va_s0 ==
    Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051 /\
    va_get_reg64 rRdx va_s0 < pow2_32 /\ aes_reqs alg key round_keys keys_b (va_get_reg64 rR8
    va_s0) (va_get_mem_heaplet 0 va_s0) (va_get_mem_layout va_s0) /\ pclmulqdq_enabled /\
    Vale.AES.GHash.hkeys_reqs_priv (Vale.X64.Decls.s128 (va_get_mem_heaplet 0 va_s0) hkeys_b)
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) /\ Vale.X64.Decls.validSrcAddrs128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rR9 va_s0 - 32) hkeys_b 8 (va_get_mem_layout va_s0)
    Secret)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (Vale.X64.Decls.modifies_buffer128 out_b (va_get_mem_heaplet 1 va_s0) (va_get_mem_heaplet 1
    va_sM) /\ Vale.AES.GCTR.gctr_partial alg (va_get_reg64 rRdx va_s0) (Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) in_b) (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_sM) out_b) key
    (va_get_xmm 11 va_s0) /\ va_get_xmm 11 va_sM == Vale.AES.GCTR.inc32lite (va_get_xmm 11 va_s0)
    (va_get_reg64 rRdx va_s0) /\ (va_get_reg64 rRdx va_s0 == 0 ==> l_and (va_get_xmm 8 va_sM ==
    va_get_xmm 8 va_s0) (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_sM) out_b ==
    Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) out_b)) /\ (va_get_reg64 rRdx va_s0 > 0 ==>
    l_and (va_get_reg64 rRdx va_s0 <= FStar.Seq.Base.length #Vale.X64.Decls.quad32
    (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) in_b) ==> FStar.Seq.Base.length
    #Vale.X64.Decls.quad32 (FStar.Seq.Base.slice #Vale.X64.Decls.quad32 (Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) in_b) 0 (va_get_reg64 rRdx va_s0)) > 0)
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_sM) == Vale.AES.GHash.ghash_incremental
    h_LE (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_s0)) (Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) in_b)))) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_mem_heaplet 1 va_sM (va_update_xmm 10 va_sM (va_update_xmm 11 va_sM (va_update_xmm 8
    va_sM (va_update_xmm 7 va_sM (va_update_xmm 6 va_sM (va_update_xmm 5 va_sM (va_update_xmm 4
    va_sM (va_update_xmm 3 va_sM (va_update_xmm 2 va_sM (va_update_xmm 1 va_sM (va_update_xmm 0
    va_sM (va_update_reg64 rR12 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rR10 va_sM
    (va_update_reg64 rR11 va_sM (va_update_reg64 rRdi va_sM (va_update_reg64 rRbx va_sM
    (va_update_ok va_sM (va_update_mem va_sM va_s0)))))))))))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Gcm_blocks128 va_b0 va_s0 alg in_b out_b key round_keys keys_b hkeys_b h_LE =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_mem_heaplet 1; va_Mod_xmm 10; va_Mod_xmm 11;
    va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm
    2; va_Mod_xmm 1; va_Mod_xmm 0; va_Mod_reg64 rR12; va_Mod_reg64 rRdx; va_Mod_reg64 rR10;
    va_Mod_reg64 rR11; va_Mod_reg64 rRdi; va_Mod_reg64 rRbx; va_Mod_ok; va_Mod_mem] in
  let va_qc = va_qcode_Gcm_blocks128 va_mods alg in_b out_b key round_keys keys_b hkeys_b h_LE in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Gcm_blocks128 alg) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 210 column 1 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 255 column 53 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (Vale.X64.Decls.modifies_buffer128 out_b (va_get_mem_heaplet 1 va_s0) (va_get_mem_heaplet 1
    va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 261 column 95 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (Vale.AES.GCTR.gctr_partial alg (va_get_reg64 rRdx va_s0) (Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) in_b) (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_sM) out_b) key
    (va_get_xmm 11 va_s0)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 262 column 45 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_get_xmm 11 va_sM == Vale.AES.GCTR.inc32lite (va_get_xmm 11 va_s0) (va_get_reg64 rRdx
    va_s0)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 265 column 93 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_get_reg64 rRdx va_s0 == 0 ==> l_and (va_get_xmm 8 va_sM == va_get_xmm 8 va_s0)
    (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_sM) out_b == Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) out_b)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 267 column 131 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GCMdecryptOpt.vaf *****"
    (va_get_reg64 rRdx va_s0 > 0 ==> l_and (va_get_reg64 rRdx va_s0 <= FStar.Seq.Base.length
    #Vale.X64.Decls.quad32 (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) in_b) ==>
    FStar.Seq.Base.length #Vale.X64.Decls.quad32 (FStar.Seq.Base.slice #Vale.X64.Decls.quad32
    (Vale.X64.Decls.s128 (va_get_mem_heaplet 1 va_s0) in_b) 0 (va_get_reg64 rRdx va_s0)) > 0)
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_sM) == Vale.AES.GHash.ghash_incremental
    h_LE (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 8 va_s0)) (Vale.X64.Decls.s128
    (va_get_mem_heaplet 1 va_s0) in_b))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_mem_heaplet 1; va_Mod_xmm 10; va_Mod_xmm 11; va_Mod_xmm
    8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2;
    va_Mod_xmm 1; va_Mod_xmm 0; va_Mod_reg64 rR12; va_Mod_reg64 rRdx; va_Mod_reg64 rR10;
    va_Mod_reg64 rR11; va_Mod_reg64 rRdi; va_Mod_reg64 rRbx; va_Mod_ok; va_Mod_mem]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Gcm_blocks128 (alg:algorithm) (in_b:buffer128) (out_b:buffer128) (key:(seq nat32))
  (round_keys:(seq quad32)) (keys_b:buffer128) (hkeys_b:buffer128) (h_LE:quad32) (va_s0:va_state)
val va_wp_Gcm_blocks128
      (alg: algorithm)
      (in_b out_b: buffer128)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b hkeys_b: buffer128)
      (h_LE: quad32)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0

    alg: Vale.AES.AES_common_s.algorithm ->
    in_b: Vale.X64.Memory.buffer128 ->
    out_b: Vale.X64.Memory.buffer128 ->
    key: FStar.Seq.Base.seq Vale.X64.Memory.nat32 ->
    round_keys: FStar.Seq.Base.seq Vale.X64.Decls.quad32 ->
    keys_b: Vale.X64.Memory.buffer128 ->
    hkeys_b: Vale.X64.Memory.buffer128 ->
    h_LE: Vale.X64.Decls.quad32 ->
    va_s0: Vale.X64.Decls.va_state ->
    va_k: (_: Vale.X64.Decls.va_state -> _: Prims.unit -> Type0)
  -> Type0