val va_lemma_Ghash_register : va_b0:va_code -> va_s0:va_state -> hkeys_b:buffer128 -> h_LE:quad32
  -> y_prev:quad32
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Ghash_register ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in pclmulqdq_enabled
    /\ avx_enabled /\ sse_enabled /\ hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_layout va_s0) (va_get_reg64 rR9 va_s0 - 32) h /\ Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_s0) == prev)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in va_get_xmm 8 va_sM
    == Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE y_prev data))
    /\ va_state_eq 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_flags
    va_sM (va_update_ok va_sM va_s0))))))))))))))
let va_lemma_Ghash_register va_b0 va_s0 hkeys_b h_LE y_prev =
  let (va_mods:va_mods_t) = [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_flags;
    va_Mod_ok] in
  let va_qc = va_qcode_Ghash_register va_mods hkeys_b h_LE y_prev in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Ghash_register ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 729 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_ok va_sM) /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in label va_range1
    "***** POSTCONDITION NOT MET AT line 753 column 79 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_xmm 8 va_sM == Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental
    h_LE y_prev data)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([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_flags;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)
val va_lemma_Ghash_register : va_b0:va_code -> va_s0:va_state -> hkeys_b:buffer128 -> h_LE:quad32
  -> y_prev:quad32
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Ghash_register ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in pclmulqdq_enabled
    /\ avx_enabled /\ sse_enabled /\ hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_layout va_s0) (va_get_reg64 rR9 va_s0 - 32) h /\ Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_s0) == prev)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in va_get_xmm 8 va_sM
    == Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE y_prev data))
    /\ va_state_eq 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_flags
    va_sM (va_update_ok va_sM va_s0))))))))))))))
let va_lemma_Ghash_register va_b0 va_s0 hkeys_b h_LE y_prev =
let va_mods:va_mods_t =
  [
    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_flags; va_Mod_ok
  ]
in
let va_qc = va_qcode_Ghash_register va_mods hkeys_b h_LE y_prev in
let va_sM, va_fM, va_g =
  va_wp_sound_code_norm (va_code_Ghash_register ())
    va_qc
    va_s0
    (fun va_s0 va_sM va_g ->
        let () = va_g in
        label va_range1
          "***** POSTCONDITION NOT MET AT line 729 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
          (va_get_ok va_sM) /\
        (let h:Vale.Math.Poly2_s.poly =
            Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 h_LE)
          in
          let data:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32) =
            FStar.Seq.Base.create #Vale.Def.Types_s.quad32
              1
              (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0))
          in
          let prev:Vale.Math.Poly2_s.poly =
            Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev)
          in
          let pdata:(Prims.int -> Vale.AES.GHash.poly128) =
            Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
          in
          label va_range1
            "***** POSTCONDITION NOT MET AT line 753 column 79 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
            (va_get_xmm 8 va_sM ==
              Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE
                    y_prev
                    data))))
in
assert_norm (va_qc.mods == va_mods);
va_lemma_norm_mods ([
      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_flags; va_Mod_ok
    ])
  va_sM
  va_s0;
(va_sM, va_fM)
Vale.AES.X64.AESopt2.fst.checked
Vale.X64.State.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.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_s.fsti.checked Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Math.Poly2.Bits.fsti.checked Vale.Math.Poly2.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.AES.X64.PolyOps.fsti.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_helpers.fsti.checked Vale.AES.AES_s.fst.checked Vale.AES.AES_helpers.fsti.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.AESopt2.fst
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Vale.X64.Memory.buffer128 Vale.X64.Decls.quad32 Vale.X64.QuickCodes.fuel Prims.unit FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_fuel Vale.X64.QuickCode.va_lemma_norm_mods Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_xmm Vale.X64.QuickCode.va_Mod_reg64 Vale.X64.Machine_s.rR11 Vale.X64.QuickCode.va_Mod_flags Vale.X64.QuickCode.va_Mod_ok Prims.Nil FStar.Pervasives.assert_norm Prims.eq2 Prims.list Vale.X64.QuickCode.__proj__QProc__item__mods Vale.AES.X64.AESopt2.va_code_Ghash_register FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.tuple3 Vale.X64.State.vale_state Vale.X64.QuickCodes.va_wp_sound_code_norm Prims.l_and Vale.X64.QuickCodes.label Vale.X64.QuickCodes.va_range1 Prims.b2t Vale.X64.Decls.va_get_ok Vale.Def.Types_s.quad32 Vale.X64.Decls.va_get_xmm Vale.Def.Types_s.reverse_bytes_quad32 Vale.AES.GHash.ghash_incremental Prims.int Vale.AES.GHash.poly128 Vale.AES.GHash.fun_seq_quad32_LE_poly128 Vale.Math.Poly2_s.poly Vale.Math.Poly2.Bits_s.of_quad32 FStar.Seq.Base.seq FStar.Seq.Base.create Vale.X64.QuickCode.quickCode Vale.AES.X64.AESopt2.va_qcode_Ghash_register
module Vale.AES.X64.AESopt2
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Seq
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.AES.AES_s
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsVector
open Vale.X64.InsAes
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.AES.AES_helpers
open Vale.Poly1305.Math    // For lemma_poly_bits64()
open Vale.AES.GCM_helpers
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.Arch.TypesNative
open Vale.X64.CPU_Features_s
open Vale.AES.X64.PolyOps

open Vale.Math.Poly2_s
open Vale.Math.Poly2
open Vale.Math.Poly2.Bits_s
open Vale.Math.Poly2.Bits
open Vale.Math.Poly2.Lemmas
open Vale.AES.GF128_s
open Vale.AES.GF128
open Vale.AES.GHash
#reset-options "--z3rlimit 50"
//-- MulAdd_step

[@ "opaque_to_smt"]
let va_code_MulAdd_step m power_index a0 a1 a2 a3 b c =
  (va_Block (va_CCons (if (m = 0) then va_Block (va_CCons (va_code_VPolyMul a0 b c false false)
    (va_CCons (va_code_VPolyMul a1 b c false true) (va_CCons (va_code_VPolyMul a2 b c true false)
    (va_CCons (va_code_VPolyMul b b c true true) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) a2
    (va_coerce_xmm_to_opr128 a1)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_op_opr128_xmm 4)) (va_CCons (va_code_Mem128_lemma ()) (va_CCons (va_code_VPolyAdd
    (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3)
    (va_op_reg64_reg64 rRbp) 16 Secret)) (va_CNil ()))))))))) else va_Block (va_CCons
    (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) c (va_op_reg_opr64_reg64 rR9) (16
    `op_Multiply` power_index - 32) Secret) (va_CCons (va_code_VPolyMul a0 b c false false)
    (va_CCons (if (m = 1) then va_Block (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 4) a1
    (va_coerce_xmm_to_opr128 a0)) (va_CNil ())) else va_Block (va_CCons (va_code_VPolyAdd
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_coerce_xmm_to_opr128 a0)) (va_CNil ()))) (va_CCons
    (va_code_VPolyMul a1 b c false true) (va_CCons (va_code_VPolyMul a2 b c true false) (va_CCons
    (va_code_VPolyMul a3 b c true true) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6)
    (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a1)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6)
    (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a2)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 7)
    (va_op_xmm_xmm 7) (va_coerce_xmm_to_opr128 a3)) (va_CCons (if (m = 4) then va_Block (va_CCons
    (va_code_Mem128_lemma ()) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 112 Secret))
    (va_CNil ()))) else va_Block (va_CNil ())) (va_CNil ())))))))))))) (va_CCons (if (m < 4) then
    va_Block (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0)
    (va_op_reg_opr64_reg64 rRbp) (48 + 16 `op_Multiply` m) Secret) (va_CNil ())) else va_Block
    (va_CNil ())) (va_CNil ()))))

[@ "opaque_to_smt"]
let va_codegen_success_MulAdd_step m power_index a0 a1 a2 a3 b c =
  (va_pbool_and (if (m = 0) then va_pbool_and (va_codegen_success_VPolyMul a0 b c false false)
    (va_pbool_and (va_codegen_success_VPolyMul a1 b c false true) (va_pbool_and
    (va_codegen_success_VPolyMul a2 b c true false) (va_pbool_and (va_codegen_success_VPolyMul b b
    c true true) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) a2
    (va_coerce_xmm_to_opr128 a1)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 8)
    (va_op_xmm_xmm 8) (va_op_opr128_xmm 4)) (va_pbool_and (va_codegen_success_Mem128_lemma ())
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 16 Secret))
    (va_ttrue ())))))))) else va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) c (va_op_reg_opr64_reg64 rR9) (16 `op_Multiply` power_index - 32)
    Secret) (va_pbool_and (va_codegen_success_VPolyMul a0 b c false false) (va_pbool_and (if (m =
    1) then va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4) a1 (va_coerce_xmm_to_opr128
    a0)) (va_ttrue ()) else va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4)
    (va_op_xmm_xmm 4) (va_coerce_xmm_to_opr128 a0)) (va_ttrue ())) (va_pbool_and
    (va_codegen_success_VPolyMul a1 b c false true) (va_pbool_and (va_codegen_success_VPolyMul a2 b
    c true false) (va_pbool_and (va_codegen_success_VPolyMul a3 b c true true) (va_pbool_and
    (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a1))
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_coerce_xmm_to_opr128 a2)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 7)
    (va_op_xmm_xmm 7) (va_coerce_xmm_to_opr128 a3)) (va_pbool_and (if (m = 4) then va_pbool_and
    (va_codegen_success_Mem128_lemma ()) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm
    8) (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp)
    112 Secret)) (va_ttrue ())) else va_ttrue ()) (va_ttrue ()))))))))))) (va_pbool_and (if (m < 4)
    then va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 3)
    (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rRbp) (48 + 16 `op_Multiply` m) Secret) (va_ttrue ())
    else va_ttrue ()) (va_ttrue ())))

[@"opaque_to_smt"]
let va_lemma_MulAdd_step va_b0 va_s0 m power_index a0 a1 a2 a3 b c hkeys_b scratch_b h prev data =
  va_reveal_opaque (`%va_code_MulAdd_step) (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in
  let (data_i:poly) = pdata (5 - m) in
  let (z0:quad32) = (if (m = 1) then va_eval_xmm va_s0 a1 else va_get_xmm 4 va_s0) in
  Vale.AES.GF128.lemma_Mul128_accum (of_quad32 z0) (of_quad32 (va_get_xmm 6 va_s0)) (of_quad32
    (va_get_xmm 7 va_s0)) (if (m = 5) then add prev data_i else data_i) (Vale.AES.GHash.gf128_power
    h (m + 1));
  let va_b12 = va_tl va_b1 in
  let va_c12 = va_hd va_b1 in
  let (va_fc12, va_s12) =
  (
    if (m = 0) then
    (
      let va_b13 = va_get_block va_c12 in
      let (va_s14, va_fc14) = va_lemma_VPolyMul (va_hd va_b13) va_s0 a0 b c false false in
      let va_b14 = va_tl va_b13 in
      let (va_s15, va_fc15) = va_lemma_VPolyMul (va_hd va_b14) va_s14 a1 b c false true in
      let va_b15 = va_tl va_b14 in
      let (va_s16, va_fc16) = va_lemma_VPolyMul (va_hd va_b15) va_s15 a2 b c true false in
      let va_b16 = va_tl va_b15 in
      let (va_s17, va_fc17) = va_lemma_VPolyMul (va_hd va_b16) va_s16 b b c true true in
      let va_b17 = va_tl va_b16 in
      Vale.AES.GF128.lemma_Mul128 data_i (Vale.AES.GHash.gf128_power h 1);
      Vale.Math.Poly2.lemma_add_commute (of_quad32 (va_eval_xmm va_s17 a1)) (of_quad32 (va_eval_xmm
        va_s17 a2));
      let (va_s20, va_fc20) = va_lemma_VPolyAdd (va_hd va_b17) va_s17 (va_op_xmm_xmm 6) a2
        (va_coerce_xmm_to_opr128 a1) in
      let va_b20 = va_tl va_b17 in
      let (va_s21, va_fc21) = va_lemma_VPolyAdd (va_hd va_b20) va_s20 (va_op_xmm_xmm 8)
        (va_op_xmm_xmm 8) (va_op_opr128_xmm 4) in
      let va_b21 = va_tl va_b20 in
      let (va_s22, va_fc22) = va_lemma_Mem128_lemma (va_hd va_b21) va_s21
        (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 16 Secret scratch_b 1 in
      let va_b22 = va_tl va_b21 in
      let (va_s23, va_fc23) = va_lemma_VPolyAdd (va_hd va_b22) va_s22 (va_op_xmm_xmm 8)
        (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64
        rRbp) 16 Secret) in
      let va_b23 = va_tl va_b22 in
      let (va_s12, va_f23) = va_lemma_empty_total va_s23 va_b23 in
      let va_f22 = va_lemma_merge_total va_b22 va_s22 va_fc23 va_s23 va_f23 va_s12 in
      let va_f21 = va_lemma_merge_total va_b21 va_s21 va_fc22 va_s22 va_f22 va_s12 in
      let va_f20 = va_lemma_merge_total va_b20 va_s20 va_fc21 va_s21 va_f21 va_s12 in
      let va_f17 = va_lemma_merge_total va_b17 va_s17 va_fc20 va_s20 va_f20 va_s12 in
      let va_f16 = va_lemma_merge_total va_b16 va_s16 va_fc17 va_s17 va_f17 va_s12 in
      let va_f15 = va_lemma_merge_total va_b15 va_s15 va_fc16 va_s16 va_f16 va_s12 in
      let va_f14 = va_lemma_merge_total va_b14 va_s14 va_fc15 va_s15 va_f15 va_s12 in
      let va_fc12 = va_lemma_merge_total va_b13 va_s0 va_fc14 va_s14 va_f14 va_s12 in
      (va_fc12, va_s12)
    )
    else
    (
      let va_b24 = va_get_block va_c12 in
      let (va_s25, va_fc25) = va_lemma_Load128_buffer (va_hd va_b24) va_s0
        (va_op_heaplet_mem_heaplet 0) c (va_op_reg_opr64_reg64 rR9) (16 `op_Multiply` power_index -
        32) Secret hkeys_b power_index in
      let va_b25 = va_tl va_b24 in
      let (va_s26, va_fc26) = va_lemma_VPolyMul (va_hd va_b25) va_s25 a0 b c false false in
      let va_b26 = va_tl va_b25 in
      let va_b27 = va_tl va_b26 in
      let va_c27 = va_hd va_b26 in
      let (va_fc27, va_s27) =
      (
        if (m = 1) then
        (
          let va_b28 = va_get_block va_c27 in
          let (va_s29, va_fc29) = va_lemma_VPolyAdd (va_hd va_b28) va_s26 (va_op_xmm_xmm 4) a1
            (va_coerce_xmm_to_opr128 a0) in
          let va_b29 = va_tl va_b28 in
          let (va_s27, va_f29) = va_lemma_empty_total va_s29 va_b29 in
          let va_fc27 = va_lemma_merge_total va_b28 va_s26 va_fc29 va_s29 va_f29 va_s27 in
          (va_fc27, va_s27)
        )
        else
        (
          let va_b30 = va_get_block va_c27 in
          let (va_s31, va_fc31) = va_lemma_VPolyAdd (va_hd va_b30) va_s26 (va_op_xmm_xmm 4)
            (va_op_xmm_xmm 4) (va_coerce_xmm_to_opr128 a0) in
          let va_b31 = va_tl va_b30 in
          let (va_s27, va_f31) = va_lemma_empty_total va_s31 va_b31 in
          let va_fc27 = va_lemma_merge_total va_b30 va_s26 va_fc31 va_s31 va_f31 va_s27 in
          (va_fc27, va_s27)
        )
      ) in
      let (va_s32, va_fc32) = va_lemma_VPolyMul (va_hd va_b27) va_s27 a1 b c false true in
      let va_b32 = va_tl va_b27 in
      let (va_s33, va_fc33) = va_lemma_VPolyMul (va_hd va_b32) va_s32 a2 b c true false in
      let va_b33 = va_tl va_b32 in
      let (va_s34, va_fc34) = va_lemma_VPolyMul (va_hd va_b33) va_s33 a3 b c true true in
      let va_b34 = va_tl va_b33 in
      let (va_s35, va_fc35) = va_lemma_VPolyAdd (va_hd va_b34) va_s34 (va_op_xmm_xmm 6)
        (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a1) in
      let va_b35 = va_tl va_b34 in
      let (va_s36, va_fc36) = va_lemma_VPolyAdd (va_hd va_b35) va_s35 (va_op_xmm_xmm 6)
        (va_op_xmm_xmm 6) (va_coerce_xmm_to_opr128 a2) in
      let va_b36 = va_tl va_b35 in
      let (va_s37, va_fc37) = va_lemma_VPolyAdd (va_hd va_b36) va_s36 (va_op_xmm_xmm 7)
        (va_op_xmm_xmm 7) (va_coerce_xmm_to_opr128 a3) in
      let va_b37 = va_tl va_b36 in
      let va_b38 = va_tl va_b37 in
      let va_c38 = va_hd va_b37 in
      let (va_fc38, va_s38) =
      (
        if (m = 4) then
        (
          let va_b39 = va_get_block va_c38 in
          let (va_s40, va_fc40) = va_lemma_Mem128_lemma (va_hd va_b39) va_s37
            (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 112 Secret scratch_b 7 in
          let va_b40 = va_tl va_b39 in
          let (va_s41, va_fc41) = va_lemma_VPolyAdd (va_hd va_b40) va_s40 (va_op_xmm_xmm 8)
            (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64
            rRbp) 112 Secret) in
          let va_b41 = va_tl va_b40 in
          let (va_s38, va_f41) = va_lemma_empty_total va_s41 va_b41 in
          let va_f40 = va_lemma_merge_total va_b40 va_s40 va_fc41 va_s41 va_f41 va_s38 in
          let va_fc38 = va_lemma_merge_total va_b39 va_s37 va_fc40 va_s40 va_f40 va_s38 in
          (va_fc38, va_s38)
        )
        else
        (
          let va_b42 = va_get_block va_c38 in
          let (va_s38, va_fc38) = va_lemma_empty_total va_s37 va_b42 in
          (va_fc38, va_s38)
        )
      ) in
      let (va_s12, va_f38) = va_lemma_empty_total va_s38 va_b38 in
      let va_f37 = va_lemma_merge_total va_b37 va_s37 va_fc38 va_s38 va_f38 va_s12 in
      let va_f36 = va_lemma_merge_total va_b36 va_s36 va_fc37 va_s37 va_f37 va_s12 in
      let va_f35 = va_lemma_merge_total va_b35 va_s35 va_fc36 va_s36 va_f36 va_s12 in
      let va_f34 = va_lemma_merge_total va_b34 va_s34 va_fc35 va_s35 va_f35 va_s12 in
      let va_f33 = va_lemma_merge_total va_b33 va_s33 va_fc34 va_s34 va_f34 va_s12 in
      let va_f32 = va_lemma_merge_total va_b32 va_s32 va_fc33 va_s33 va_f33 va_s12 in
      let va_f27 = va_lemma_merge_total va_b27 va_s27 va_fc32 va_s32 va_f32 va_s12 in
      let va_f26 = va_lemma_merge_total va_b26 va_s26 va_fc27 va_s27 va_f27 va_s12 in
      let va_f25 = va_lemma_merge_total va_b25 va_s25 va_fc26 va_s26 va_f26 va_s12 in
      let va_fc12 = va_lemma_merge_total va_b24 va_s0 va_fc25 va_s25 va_f25 va_s12 in
      (va_fc12, va_s12)
    )
  ) in
  let va_b43 = va_tl va_b12 in
  let va_c43 = va_hd va_b12 in
  let (va_fc43, va_s43) =
  (
    if (m < 4) then
    (
      let va_b44 = va_get_block va_c43 in
      let (va_s45, va_fc45) = va_lemma_Load128_buffer (va_hd va_b44) va_s12
        (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rRbp) (48 + 16
        `op_Multiply` m) Secret scratch_b (3 + m) in
      let va_b45 = va_tl va_b44 in
      let (va_s43, va_f45) = va_lemma_empty_total va_s45 va_b45 in
      let va_fc43 = va_lemma_merge_total va_b44 va_s12 va_fc45 va_s45 va_f45 va_s43 in
      (va_fc43, va_s43)
    )
    else
    (
      let va_b46 = va_get_block va_c43 in
      let (va_s43, va_fc43) = va_lemma_empty_total va_s12 va_b46 in
      (va_fc43, va_s43)
    )
  ) in
  let (va_sM, va_f43) = va_lemma_empty_total va_s43 va_b43 in
  let va_f12 = va_lemma_merge_total va_b12 va_s12 va_fc43 va_s43 va_f43 va_sM in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc12 va_s12 va_f12 va_sM in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_MulAdd_step m power_index a0 a1 a2 a3 b c hkeys_b scratch_b h prev data va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_MulAdd_step (va_code_MulAdd_step m power_index a0 a1 a2 a3 b c)
    va_s0 m power_index a0 a1 a2 a3 b c hkeys_b scratch_b h prev data in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_xmm 8 va_sM (va_update_xmm 7 va_sM (va_update_xmm 6 va_sM
    (va_update_xmm 4 va_sM (va_update_xmm 0 va_sM (va_update_flags va_sM (va_update_ok va_sM
    (va_update_operand_xmm c va_sM (va_update_operand_xmm b va_sM (va_update_operand_xmm a3 va_sM
    (va_update_operand_xmm a2 va_sM (va_update_operand_xmm a1 va_sM (va_update_operand_xmm a0 va_sM
    va_s0))))))))))))));
  va_lemma_norm_mods ([va_Mod_xmm 8; va_Mod_xmm 7; va_Mod_xmm 6; va_Mod_xmm 4; va_Mod_xmm 0;
    va_Mod_flags; va_mod_xmm c; va_mod_xmm b; va_mod_xmm a3; va_mod_xmm a2; va_mod_xmm a1;
    va_mod_xmm a0]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- MulAdd_unroll_i

val va_code_MulAdd_unroll_i : rev_bytes:bool -> rev_blocks:bool -> is_first:bool -> is_last:bool ->
  power_index:int -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last power_index =
  (va_Block (va_CCons (if is_last then va_Block (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 8) (va_op_opr128_xmm 0)) (va_CNil ())) else va_Block (va_CCons (if rev_blocks
    then va_Block (va_CCons (va_code_Add64 (va_op_dst_opr64_reg64 rR11) (va_const_opr64 16))
    (va_CNil ())) else va_Block (va_CCons (va_code_Sub64 (va_op_dst_opr64_reg64 rR11)
    (va_const_opr64 16)) (va_CNil ()))) (va_CNil ()))) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm
    1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm
    2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false true) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm
    3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true false) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm
    5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true true) (va_CCons (va_Block (va_CNil ())) (va_CCons
    (if not is_last then va_Block (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 1)
    (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rR11) 0 Secret) (va_CCons (if not rev_bytes then
    va_Block (va_CCons (va_code_Pshufb (va_op_xmm_xmm 0) (va_op_xmm_xmm 9)) (va_CNil ())) else
    va_Block (va_CNil ())) (va_CNil ()))) else va_Block (va_CNil ())) (va_CCons (if is_first then
    va_Block (va_CCons (va_code_Mov128 (va_op_xmm_xmm 4) (va_op_xmm_xmm 1)) (va_CNil ())) else
    va_Block (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 1))
    (va_CNil ()))) (va_CCons (if not is_last then va_Block (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 1) (va_op_reg_opr64_reg64 rR9) (16 `op_Multiply`
    power_index - 32) Secret) (va_CNil ())) else va_Block (va_CNil ())) (va_CCons (if is_first then
    va_Block (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 2) (va_op_opr128_xmm 3))
    (va_CCons (va_code_Mov128 (va_op_xmm_xmm 7) (va_op_xmm_xmm 5)) (va_CNil ()))) else va_Block
    (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 2)) (va_CCons
    (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 3)) (va_CCons
    (va_code_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 5)) (va_CNil ())))))
    (va_CCons (if not is_last then va_Block (va_CCons (va_code_Mov128 (va_op_xmm_xmm 5)
    (va_op_xmm_xmm 1)) (va_CNil ())) else va_Block (va_CNil ())) (va_CNil ())))))))))))))

val va_codegen_success_MulAdd_unroll_i : rev_bytes:bool -> rev_blocks:bool -> is_first:bool ->
  is_last:bool -> power_index:int -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last power_index =
  (va_pbool_and (if is_last then va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 8) (va_op_opr128_xmm 0)) (va_ttrue ()) else va_pbool_and (if rev_blocks then
    va_pbool_and (va_codegen_success_Add64 (va_op_dst_opr64_reg64 rR11) (va_const_opr64 16))
    (va_ttrue ()) else va_pbool_and (va_codegen_success_Sub64 (va_op_dst_opr64_reg64 rR11)
    (va_const_opr64 16)) (va_ttrue ())) (va_ttrue ())) (va_pbool_and (va_codegen_success_VPolyMul
    (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false true)
    (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm
    5) true false) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 5) true true) (va_pbool_and (if not is_last then va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 1) (va_op_xmm_xmm 0)
    (va_op_reg_opr64_reg64 rR11) 0 Secret) (va_pbool_and (if not rev_bytes then va_pbool_and
    (va_codegen_success_Pshufb (va_op_xmm_xmm 0) (va_op_xmm_xmm 9)) (va_ttrue ()) else va_ttrue ())
    (va_ttrue ())) else va_ttrue ()) (va_pbool_and (if is_first then va_pbool_and
    (va_codegen_success_Mov128 (va_op_xmm_xmm 4) (va_op_xmm_xmm 1)) (va_ttrue ()) else va_pbool_and
    (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 1))
    (va_ttrue ())) (va_pbool_and (if not is_last then va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 1)
    (va_op_reg_opr64_reg64 rR9) (16 `op_Multiply` power_index - 32) Secret) (va_ttrue ()) else
    va_ttrue ()) (va_pbool_and (if is_first then va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 6) (va_op_xmm_xmm 2) (va_op_opr128_xmm 3)) (va_pbool_and
    (va_codegen_success_Mov128 (va_op_xmm_xmm 7) (va_op_xmm_xmm 5)) (va_ttrue ())) else
    va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm
    2)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 3)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 7)
    (va_op_xmm_xmm 7) (va_op_opr128_xmm 5)) (va_ttrue ())))) (va_pbool_and (if not is_last then
    va_pbool_and (va_codegen_success_Mov128 (va_op_xmm_xmm 5) (va_op_xmm_xmm 1)) (va_ttrue ()) else
    va_ttrue ()) (va_ttrue ())))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_MulAdd_unroll_i (va_mods:va_mods_t) (rev_bytes:bool) (rev_blocks:bool) (is_first:bool)
  (is_last:bool) (power_index:int) (scratch_len:nat64) (n:nat) (m:int) (hkeys_b:buffer128)
  (scratch_in_b:buffer128) (h:poly) (prev:poly) (data:(seq quad32)) : (va_quickCode unit
  (va_code_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last power_index)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let (pdata:(Prims.int
    -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let
    (scratch_index:int) = index_opt_rev rev_blocks scratch_len n (n - (m + 2)) in let (data_i:poly)
    = pdata (n - m - 1) in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 288 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods is_last (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 290 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 0) (va_op_xmm_xmm 8) (va_op_opr128_xmm 0)) (va_QEmpty (()))))
    (qblock va_mods (fun (va_s:va_state) -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 292 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods rev_blocks (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 294 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Add64 (va_op_dst_opr64_reg64 rR11) (va_const_opr64 16)) (va_QEmpty (())))) (qblock
    va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 298 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Sub64 (va_op_dst_opr64_reg64 rR11) (va_const_opr64 16)) (va_QEmpty (()))))) (fun
    (va_s:va_state) va_g -> va_QEmpty (()))))) (fun (va_s:va_state) va_g -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 300 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 301 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 302 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true false) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 303 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true true) (fun
    (va_s:va_state) _ -> va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 304 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (m + 1 >= 0) (fun _ -> let (va_arg69:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h (m
    + 1) in let (va_arg68:Vale.Math.Poly2_s.poly) = va_if (n = m + 1) (fun _ -> add prev data_i)
    (fun _ -> data_i) in let (va_arg67:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 7 va_s) in
    let (va_arg66:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 6 va_s) in let
    (va_arg65:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 4 va_s) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 304 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128_accum va_arg65 va_arg66 va_arg67 va_arg68
    va_arg69) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 306 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods (not is_last) (qblock va_mods (fun (va_s:va_state) -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 308 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 1) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64
    rR11) 0 Secret scratch_in_b scratch_index) (fun (va_s:va_state) _ -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 309 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods (not rev_bytes) (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 311 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Pshufb (va_op_xmm_xmm 0) (va_op_xmm_xmm 9)) (va_QEmpty (())))) (qblock va_mods (fun
    (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QEmpty (()))))) (qblock
    va_mods (fun (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 314 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods is_first (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 316 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 4) (va_op_xmm_xmm 1)) (va_QEmpty (())))) (qblock va_mods (fun
    (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 320 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 1)) (va_QEmpty
    (()))))) (fun (va_s:va_state) va_g -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 322 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods (not is_last) (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 324 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 1) (va_op_reg_opr64_reg64
    rR9) (16 `op_Multiply` power_index - 32) Secret hkeys_b power_index) (va_QEmpty (())))) (qblock
    va_mods (fun (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 326 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods is_first (qblock va_mods (fun (va_s:va_state) -> let
    (va_arg64:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 1 in let
    (va_arg63:Vale.Math.Poly2_s.poly) = va_if (n = m + 1) (fun _ -> add prev data_i) (fun _ ->
    data_i) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 328 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128 va_arg63 va_arg64) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 329 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 2) (va_op_opr128_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 330 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 7) (va_op_xmm_xmm 5)) (va_QEmpty (())))))) (qblock va_mods (fun
    (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 334 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 335 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 336 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 5)) (va_QEmpty
    (()))))))) (fun (va_s:va_state) va_g -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 338 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods (not is_last) (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 340 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 5) (va_op_xmm_xmm 1)) (va_QEmpty (())))) (qblock va_mods (fun
    (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QEmpty (())))))))))))))))


val va_lemma_MulAdd_unroll_i : va_b0:va_code -> va_s0:va_state -> rev_bytes:bool -> rev_blocks:bool
  -> is_first:bool -> is_last:bool -> power_index:int -> scratch_len:nat64 -> n:nat -> m:int ->
  hkeys_b:buffer128 -> scratch_in_b:buffer128 -> h:poly -> prev:poly -> data:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last
    power_index) va_s0 /\ va_get_ok va_s0 /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let (scratch_index:int) = index_opt_rev
    rev_blocks scratch_len n (n - (m + 2)) in pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\
    FStar.Seq.Base.length #quad32 data >= n /\ (0 <= m /\ m < n /\ n <= scratch_len) /\ (is_first
    <==> m == 0) /\ (is_last <==> m == n - 1) /\ 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 /\ Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 1 va_s0) (va_get_reg64 rRdi
    va_s0) scratch_in_b scratch_len (va_get_mem_layout va_s0) Secret /\ va_get_reg64 rRdi va_s0 +
    16 `op_Multiply` scratch_len <= pow2_64 /\ Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8
    va_s0) == prev /\ va_get_reg64 rR11 va_s0 == va_get_reg64 rRdi va_s0 + 16 `op_Multiply`
    (scratch_index + (if rev_blocks then (-1) else 1)) /\ (0 <= power_index /\ power_index < 8) /\
    (~is_first ==> add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0)) 64))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 n (m - 1)) /\ va_get_xmm 0 va_s0 ==
    Vale.Def.Types_s.reverse_bytes_quad32 (va_subscript_FStar__Seq__Base__seq data (n - m - 1)) /\
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 5 va_s0) == Vale.AES.GHash.gf128_power h (m + 1)
    /\ (~rev_bytes ==> va_get_xmm 9 va_s0 == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    202182159 134810123 67438087 66051))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128
    data in let (scratch_index:int) = index_opt_rev rev_blocks scratch_len n (n - (m + 2)) in
    (~is_last ==> va_get_xmm 0 va_sM == quad32_opt_rev (not rev_bytes)
    (Vale.X64.Decls.buffer128_read scratch_in_b scratch_index (va_get_mem_heaplet 1 va_sM))) /\
    (~is_last ==> va_get_xmm 5 va_sM == Vale.X64.Decls.buffer128_read hkeys_b power_index
    (va_get_mem_heaplet 0 va_sM)) /\ (~is_last ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11
    va_s0 + (if rev_blocks then 16 else (-16))) /\ (is_last ==> va_get_reg64 rR11 va_sM ==
    va_get_reg64 rR11 va_s0) /\ add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 n m) /\ va_state_eq 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_flags va_sM (va_update_ok va_sM va_s0)))))))))))))
[@"opaque_to_smt"]
let va_lemma_MulAdd_unroll_i va_b0 va_s0 rev_bytes rev_blocks is_first is_last power_index
  scratch_len n m hkeys_b scratch_in_b h prev data =
  let (va_mods:va_mods_t) = [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_flags; va_Mod_ok] in
  let va_qc = va_qcode_MulAdd_unroll_i va_mods rev_bytes rev_blocks is_first is_last power_index
    scratch_len n m hkeys_b scratch_in_b h prev data in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_MulAdd_unroll_i rev_bytes rev_blocks
    is_first is_last power_index) va_qc va_s0 (fun va_s0 va_sM va_g -> let () = va_g in label
    va_range1
    "***** POSTCONDITION NOT MET AT line 236 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_ok va_sM) /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let (scratch_index:int) = index_opt_rev
    rev_blocks scratch_len n (n - (m + 2)) in label va_range1
    "***** POSTCONDITION NOT MET AT line 280 column 106 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (~is_last ==> va_get_xmm 0 va_sM == quad32_opt_rev (not rev_bytes)
    (Vale.X64.Decls.buffer128_read scratch_in_b scratch_index (va_get_mem_heaplet 1 va_sM))) /\
    label va_range1
    "***** POSTCONDITION NOT MET AT line 281 column 71 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (~is_last ==> va_get_xmm 5 va_sM == Vale.X64.Decls.buffer128_read hkeys_b power_index
    (va_get_mem_heaplet 0 va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 282 column 94 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (~is_last ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0 + va_if rev_blocks (fun _ ->
    16) (fun _ -> (-16))) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 283 column 52 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (is_last ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 285 column 61 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 n m))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([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_flags; va_Mod_ok]) va_sM
    va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_MulAdd_unroll_i (rev_bytes:bool) (rev_blocks:bool) (is_first:bool) (is_last:bool)
  (power_index:int) (scratch_len:nat64) (n:nat) (m:int) (hkeys_b:buffer128)
  (scratch_in_b:buffer128) (h:poly) (prev:poly) (data:(seq quad32)) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let (scratch_index:int) = index_opt_rev
    rev_blocks scratch_len n (n - (m + 2)) in pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\
    FStar.Seq.Base.length #quad32 data >= n /\ (0 <= m /\ m < n /\ n <= scratch_len) /\ (is_first
    <==> m == 0) /\ (is_last <==> m == n - 1) /\ 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 /\ Vale.X64.Decls.validSrcAddrs128 (va_get_mem_heaplet 1 va_s0) (va_get_reg64 rRdi
    va_s0) scratch_in_b scratch_len (va_get_mem_layout va_s0) Secret /\ va_get_reg64 rRdi va_s0 +
    16 `op_Multiply` scratch_len <= pow2_64 /\ Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8
    va_s0) == prev /\ va_get_reg64 rR11 va_s0 == va_get_reg64 rRdi va_s0 + 16 `op_Multiply`
    (scratch_index + va_if rev_blocks (fun _ -> (-1)) (fun _ -> 1)) /\ (0 <= power_index /\
    power_index < 8) /\ (~is_first ==> add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4
    va_s0)) (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0)) 64))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 n (m - 1)) /\ va_get_xmm 0 va_s0 ==
    Vale.Def.Types_s.reverse_bytes_quad32 (va_subscript_FStar__Seq__Base__seq data (n - m - 1)) /\
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 5 va_s0) == Vale.AES.GHash.gf128_power h (m + 1)
    /\ (~rev_bytes ==> va_get_xmm 9 va_s0 == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    202182159 134810123 67438087 66051)) /\ (forall (va_x_efl:Vale.X64.Flags.t) (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) . let va_sM = 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_flags va_x_efl va_s0))))))))) in va_get_ok va_sM /\ (let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let
    (scratch_index:int) = index_opt_rev rev_blocks scratch_len n (n - (m + 2)) in (~is_last ==>
    va_get_xmm 0 va_sM == quad32_opt_rev (not rev_bytes) (Vale.X64.Decls.buffer128_read
    scratch_in_b scratch_index (va_get_mem_heaplet 1 va_sM))) /\ (~is_last ==> va_get_xmm 5 va_sM
    == Vale.X64.Decls.buffer128_read hkeys_b power_index (va_get_mem_heaplet 0 va_sM)) /\ (~is_last
    ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0 + va_if rev_blocks (fun _ -> 16) (fun _
    -> (-16))) /\ (is_last ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0) /\ add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 n m) ==> va_k va_sM (())))


val va_wpProof_MulAdd_unroll_i : rev_bytes:bool -> rev_blocks:bool -> is_first:bool -> is_last:bool
  -> power_index:int -> scratch_len:nat64 -> n:nat -> m:int -> hkeys_b:buffer128 ->
  scratch_in_b:buffer128 -> h:poly -> prev:poly -> data:(seq 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_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last
    power_index scratch_len n m hkeys_b scratch_in_b h prev data va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MulAdd_unroll_i rev_bytes rev_blocks
    is_first is_last power_index) ([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_flags]) va_s0
    va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last power_index scratch_len n m
  hkeys_b scratch_in_b h prev data va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_MulAdd_unroll_i (va_code_MulAdd_unroll_i rev_bytes rev_blocks
    is_first is_last power_index) va_s0 rev_bytes rev_blocks is_first is_last power_index
    scratch_len n m hkeys_b scratch_in_b h prev data in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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_flags va_sM (va_update_ok va_sM
    va_s0))))))))))));
  va_lemma_norm_mods ([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_flags]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_MulAdd_unroll_i (rev_bytes:bool) (rev_blocks:bool) (is_first:bool) (is_last:bool)
  (power_index:int) (scratch_len:nat64) (n:nat) (m:int) (hkeys_b:buffer128)
  (scratch_in_b:buffer128) (h:poly) (prev:poly) (data:(seq quad32)) : (va_quickCode unit
  (va_code_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last power_index)) =
  (va_QProc (va_code_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last power_index)
    ([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_flags]) (va_wp_MulAdd_unroll_i rev_bytes
    rev_blocks is_first is_last power_index scratch_len n m hkeys_b scratch_in_b h prev data)
    (va_wpProof_MulAdd_unroll_i rev_bytes rev_blocks is_first is_last power_index scratch_len n m
    hkeys_b scratch_in_b h prev data))
//--
//-- MulAdd_unroll_n

val va_code_MulAdd_unroll_n : rev_bytes:bool -> rev_blocks:bool -> exactly6:bool -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_MulAdd_unroll_n rev_bytes rev_blocks exactly6 =
  (va_Block (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5)
    (va_op_reg_opr64_reg64 rR9) (-32) Secret) (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 1) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rR11) 0 Secret)
    (va_CCons (if not rev_bytes then va_Block (va_CCons (va_code_Pshufb (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 9)) (va_CNil ())) else va_Block (va_CNil ())) (va_CCons (if exactly6 then
    va_Block (va_CCons (va_code_MulAdd_unroll_i rev_bytes rev_blocks true false 1) (va_CCons
    (va_code_MulAdd_unroll_i rev_bytes rev_blocks false false 3) (va_CCons (va_code_MulAdd_unroll_i
    rev_bytes rev_blocks false false 4) (va_CCons (va_code_MulAdd_unroll_i rev_bytes rev_blocks
    false false 6) (va_CCons (va_code_MulAdd_unroll_i rev_bytes rev_blocks false false 7) (va_CCons
    (va_code_MulAdd_unroll_i rev_bytes rev_blocks false true 0) (va_CNil ()))))))) else va_Block
    (va_CCons (va_IfElse (va_cmp_eq (va_op_cmp_reg64 rRdx) (va_const_cmp 1)) (va_Block (va_CCons
    (va_code_MulAdd_unroll_i rev_bytes rev_blocks true true 1) (va_CNil ()))) (va_Block (va_CCons
    (va_code_MulAdd_unroll_i rev_bytes rev_blocks true false 1) (va_CCons (va_IfElse (va_cmp_ne
    (va_op_cmp_reg64 rRdx) (va_const_cmp 2)) (va_Block (va_CCons (va_code_MulAdd_unroll_i rev_bytes
    rev_blocks false false 3) (va_CCons (va_IfElse (va_cmp_ne (va_op_cmp_reg64 rRdx) (va_const_cmp
    3)) (va_Block (va_CCons (va_code_MulAdd_unroll_i rev_bytes rev_blocks false false 4) (va_CCons
    (va_IfElse (va_cmp_ne (va_op_cmp_reg64 rRdx) (va_const_cmp 4)) (va_Block (va_CCons
    (va_code_MulAdd_unroll_i rev_bytes rev_blocks false false 6) (va_CNil ()))) (va_Block (va_CNil
    ()))) (va_CNil ())))) (va_Block (va_CNil ()))) (va_CNil ())))) (va_Block (va_CNil ())))
    (va_CCons (va_code_MulAdd_unroll_i rev_bytes rev_blocks false true 0) (va_CNil ()))))))
    (va_CNil ()))) (va_CNil ()))))))

val va_codegen_success_MulAdd_unroll_n : rev_bytes:bool -> rev_blocks:bool -> exactly6:bool -> Tot
  va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_MulAdd_unroll_n rev_bytes rev_blocks exactly6 =
  (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5)
    (va_op_reg_opr64_reg64 rR9) (-32) Secret) (va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 1) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rR11) 0 Secret)
    (va_pbool_and (if not rev_bytes then va_pbool_and (va_codegen_success_Pshufb (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 9)) (va_ttrue ()) else va_ttrue ()) (va_pbool_and (if exactly6 then va_pbool_and
    (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks true false 1) (va_pbool_and
    (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false false 3) (va_pbool_and
    (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false false 4) (va_pbool_and
    (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false false 6) (va_pbool_and
    (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false false 7) (va_pbool_and
    (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false true 0) (va_ttrue ())))))) else
    va_pbool_and (va_pbool_and (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks true true
    1) (va_pbool_and (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks true false 1)
    (va_pbool_and (va_pbool_and (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false
    false 3) (va_pbool_and (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false false 4)
    (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false false 6)))
    (va_codegen_success_MulAdd_unroll_i rev_bytes rev_blocks false true 0)))) (va_ttrue ()))
    (va_ttrue ())))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_MulAdd_unroll_n (va_mods:va_mods_t) (rev_bytes:bool) (rev_blocks:bool) (exactly6:bool)
  (scratch_len:nat64) (hkeys_b:buffer128) (scratch_in_b:buffer128) (h:poly) (prev:poly) (data:(seq
  quad32)) : (va_quickCode unit (va_code_MulAdd_unroll_n rev_bytes rev_blocks exactly6)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let (pdata:(Prims.int
    -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let
    (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) = index_opt_rev
    rev_blocks scratch_len n (n - 1) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 384 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64
    rR9) (-32) Secret hkeys_b 0) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 386 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 1) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64
    rR11) 0 Secret scratch_in_b scratch_index) (fun (va_s:va_state) _ -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 387 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods (not rev_bytes) (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 389 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Pshufb (va_op_xmm_xmm 0) (va_op_xmm_xmm 9)) (va_QEmpty (())))) (qblock va_mods (fun
    (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 392 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods exactly6 (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 394 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks true false 1 scratch_len n 0 hkeys_b
    scratch_in_b h prev data) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 395 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false false 3 scratch_len n 1 hkeys_b
    scratch_in_b h prev data) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 396 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false false 4 scratch_len n 2 hkeys_b
    scratch_in_b h prev data) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 397 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false false 6 scratch_len n 3 hkeys_b
    scratch_in_b h prev data) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 398 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false false 7 scratch_len n 4 hkeys_b
    scratch_in_b h prev data) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 399 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false true 0 scratch_len n 5 hkeys_b
    scratch_in_b h prev data) (va_QEmpty (()))))))))) (qblock va_mods (fun (va_s:va_state) ->
    va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 403 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qIf va_mods (Cmp_eq (va_op_cmp_reg64 rRdx) (va_const_cmp 1)) (qblock va_mods (fun
    (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 405 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks true true 1 scratch_len n 0 hkeys_b scratch_in_b
    h prev data) (va_QEmpty (())))) (qblock va_mods (fun (va_s:va_state) -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 409 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks true false 1 scratch_len n 0 hkeys_b
    scratch_in_b h prev data) (fun (va_s:va_state) _ -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 410 column 16 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qIf va_mods (Cmp_ne (va_op_cmp_reg64 rRdx) (va_const_cmp 2)) (qblock va_mods (fun
    (va_s:va_state) -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 412 column 32 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false false 3 scratch_len n 1 hkeys_b
    scratch_in_b h prev data) (fun (va_s:va_state) _ -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 413 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qIf va_mods (Cmp_ne (va_op_cmp_reg64 rRdx) (va_const_cmp 3)) (qblock va_mods (fun
    (va_s:va_state) -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 415 column 36 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false false 4 scratch_len n 2 hkeys_b
    scratch_in_b h prev data) (fun (va_s:va_state) _ -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 416 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qIf va_mods (Cmp_ne (va_op_cmp_reg64 rRdx) (va_const_cmp 4)) (qblock va_mods (fun
    (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 418 column 40 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false false 6 scratch_len n 3 hkeys_b
    scratch_in_b h prev data) (va_QEmpty (())))) (qblock va_mods (fun (va_s:va_state) -> va_QEmpty
    (())))) (fun (va_s:va_state) va_g -> va_QEmpty (()))))) (qblock va_mods (fun (va_s:va_state) ->
    va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QEmpty (()))))) (qblock va_mods (fun
    (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 422 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_i rev_bytes rev_blocks false true 0 scratch_len n (n - 1) hkeys_b
    scratch_in_b h prev data) (va_QEmpty (()))))))) (fun (va_s:va_state) va_g -> va_QEmpty (())))))
    (fun (va_s:va_state) va_g -> va_QEmpty (())))))))


val va_lemma_MulAdd_unroll_n : va_b0:va_code -> va_s0:va_state -> rev_bytes:bool -> rev_blocks:bool
  -> exactly6:bool -> scratch_len:nat64 -> hkeys_b:buffer128 -> scratch_in_b:buffer128 -> h:poly ->
  prev:poly -> data:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd_unroll_n rev_bytes rev_blocks exactly6) va_s0
    /\ va_get_ok va_s0 /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let (n:Prims.nat) = FStar.Seq.Base.length
    #quad32 data in let (scratch_index:int) = index_opt_rev rev_blocks scratch_len n (n - 1) in
    pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ (exactly6 ==> n == 6) /\ (~exactly6 ==> 1 <=
    n /\ n < 6) /\ n <= scratch_len /\ hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_layout va_s0) (va_get_reg64 rR9 va_s0 - 32) h /\ scratch_b_data rev_bytes
    rev_blocks scratch_in_b scratch_len 6 (va_get_mem_heaplet 1 va_s0) (va_get_mem_layout va_s0)
    (va_get_reg64 rRdi va_s0) data /\ va_get_reg64 rRdi va_s0 + 16 `op_Multiply` scratch_len <=
    pow2_64 /\ Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0) == prev /\ (~exactly6 ==>
    va_get_reg64 rRdx va_s0 == n) /\ va_get_reg64 rR11 va_s0 == va_get_reg64 rRdi va_s0 + 16
    `op_Multiply` scratch_index /\ (~rev_bytes ==> va_get_xmm 9 va_s0 == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128
    data in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) =
    index_opt_rev rev_blocks scratch_len n (n - 1) in add (add (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_sM)) (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6
    va_sM)) 64)) (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM))
    128) == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 n (n - 1) /\ (l_and exactly6
    (~rev_blocks) ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0 - 80)) /\ va_state_eq
    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_flags va_sM (va_update_ok
    va_sM va_s0))))))))))))))
[@"opaque_to_smt"]
let va_lemma_MulAdd_unroll_n va_b0 va_s0 rev_bytes rev_blocks exactly6 scratch_len hkeys_b
  scratch_in_b h prev data =
  let (va_mods:va_mods_t) = [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_flags;
    va_Mod_ok] in
  let va_qc = va_qcode_MulAdd_unroll_n va_mods rev_bytes rev_blocks exactly6 scratch_len hkeys_b
    scratch_in_b h prev data in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_MulAdd_unroll_n rev_bytes rev_blocks
    exactly6) va_qc va_s0 (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 344 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_ok va_sM) /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let (n:Prims.nat) = FStar.Seq.Base.length
    #quad32 data in let (scratch_index:int) = index_opt_rev rev_blocks scratch_len n (n - 1) in
    label va_range1
    "***** POSTCONDITION NOT MET AT line 381 column 65 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 n (n - 1)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 382 column 75 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (l_and exactly6 (~rev_blocks) ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0 - 80))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([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_flags;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_MulAdd_unroll_n (rev_bytes:bool) (rev_blocks:bool) (exactly6:bool) (scratch_len:nat64)
  (hkeys_b:buffer128) (scratch_in_b:buffer128) (h:poly) (prev:poly) (data:(seq quad32))
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let (n:Prims.nat) = FStar.Seq.Base.length
    #quad32 data in let (scratch_index:int) = index_opt_rev rev_blocks scratch_len n (n - 1) in
    pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ (exactly6 ==> n == 6) /\ (~exactly6 ==> 1 <=
    n /\ n < 6) /\ n <= scratch_len /\ hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_layout va_s0) (va_get_reg64 rR9 va_s0 - 32) h /\ scratch_b_data rev_bytes
    rev_blocks scratch_in_b scratch_len 6 (va_get_mem_heaplet 1 va_s0) (va_get_mem_layout va_s0)
    (va_get_reg64 rRdi va_s0) data /\ va_get_reg64 rRdi va_s0 + 16 `op_Multiply` scratch_len <=
    pow2_64 /\ Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0) == prev /\ (~exactly6 ==>
    va_get_reg64 rRdx va_s0 == n) /\ va_get_reg64 rR11 va_s0 == va_get_reg64 rRdi va_s0 + 16
    `op_Multiply` scratch_index /\ (~rev_bytes ==> va_get_xmm 9 va_s0 == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 202182159 134810123 67438087 66051)) /\ (forall
    (va_x_efl:Vale.X64.Flags.t) (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) . let va_sM = 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_flags va_x_efl va_s0)))))))))) in va_get_ok va_sM /\ (let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) =
    index_opt_rev rev_blocks scratch_len n (n - 1) in add (add (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_sM)) (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6
    va_sM)) 64)) (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM))
    128) == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 n (n - 1) /\ (l_and exactly6
    (~rev_blocks) ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0 - 80)) ==> va_k va_sM
    (())))


val va_wpProof_MulAdd_unroll_n : rev_bytes:bool -> rev_blocks:bool -> exactly6:bool ->
  scratch_len:nat64 -> hkeys_b:buffer128 -> scratch_in_b:buffer128 -> h:poly -> prev:poly ->
  data:(seq 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_MulAdd_unroll_n rev_bytes rev_blocks exactly6 scratch_len
    hkeys_b scratch_in_b h prev data va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MulAdd_unroll_n rev_bytes rev_blocks
    exactly6) ([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_flags]) va_s0 va_k ((va_sM,
    va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_MulAdd_unroll_n rev_bytes rev_blocks exactly6 scratch_len hkeys_b scratch_in_b h
  prev data va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_MulAdd_unroll_n (va_code_MulAdd_unroll_n rev_bytes rev_blocks
    exactly6) va_s0 rev_bytes rev_blocks exactly6 scratch_len hkeys_b scratch_in_b h prev data in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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_flags
    va_sM (va_update_ok va_sM va_s0)))))))))))));
  va_lemma_norm_mods ([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_flags]) va_sM
    va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_MulAdd_unroll_n (rev_bytes:bool) (rev_blocks:bool) (exactly6:bool) (scratch_len:nat64)
  (hkeys_b:buffer128) (scratch_in_b:buffer128) (h:poly) (prev:poly) (data:(seq quad32)) :
  (va_quickCode unit (va_code_MulAdd_unroll_n rev_bytes rev_blocks exactly6)) =
  (va_QProc (va_code_MulAdd_unroll_n rev_bytes rev_blocks exactly6) ([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_flags]) (va_wp_MulAdd_unroll_n rev_bytes rev_blocks exactly6
    scratch_len hkeys_b scratch_in_b h prev data) (va_wpProof_MulAdd_unroll_n rev_bytes rev_blocks
    exactly6 scratch_len hkeys_b scratch_in_b h prev data))
//--
//-- MulAdd_unroll

val va_code_MulAdd_unroll : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_MulAdd_unroll () =
  (va_Block (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3)
    (va_op_reg_opr64_reg64 rR9) (-32) Secret) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 1)
    (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) false false) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 5)
    (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) false true) (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rRbp) 48 Secret)
    (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 6) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) true false)
    (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) true true)
    (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3)
    (va_op_reg_opr64_reg64 rR9) (-16) Secret) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6)
    (va_op_xmm_xmm 6) (va_op_opr128_xmm 5)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 5)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) false false) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 8)
    (va_op_xmm_xmm 8) (va_op_opr128_xmm 4)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 4)
    (va_op_xmm_xmm 1) (va_op_opr128_xmm 5)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 1)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) false true) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 2)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) true false) (va_CCons (va_code_Mem128_lemma ()) (va_CCons
    (va_code_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_opr_code_Mem128
    (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 16 Secret)) (va_CCons (va_code_VPolyMul
    (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) true true) (va_CCons
    (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64
    rRbp) 64 Secret) (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm
    5) (va_op_reg_opr64_reg64 rR9) 16 Secret) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6)
    (va_op_xmm_xmm 6) (va_op_opr128_xmm 1)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 1)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6)
    (va_op_xmm_xmm 6) (va_op_opr128_xmm 2)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 2)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false true) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 7)
    (va_op_xmm_xmm 7) (va_op_opr128_xmm 3)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 3)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true false) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 5)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true true) (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rRbp) 80 Secret)
    (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 1)) (va_CCons
    (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 1) (va_op_reg_opr64_reg64
    rR9) 32 Secret) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 2)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 1) false false) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 3)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 1) false true) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7)
    (va_op_opr128_xmm 5)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 1) true false) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 1) true true) (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 3)
    (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rRbp) 96 Secret) (va_CCons (va_code_VPolyAdd
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 2)) (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 2) (va_op_reg_opr64_reg64 rR9) 64 Secret)
    (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 3)) (va_CCons
    (va_code_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) false false) (va_CCons
    (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 5)) (va_CCons
    (va_code_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) false true) (va_CCons
    (va_code_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 1)) (va_CCons
    (va_code_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) true false) (va_CCons
    (va_code_Mem128_lemma ()) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 112 Secret))
    (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) true true)
    (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 3)) (va_CCons
    (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3) (va_op_reg_opr64_reg64
    rR9) 80 Secret) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 5)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 8)
    (va_op_xmm_xmm 3) false true) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 1)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 8)
    (va_op_xmm_xmm 3) true false) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7)
    (va_op_opr128_xmm 2)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 8)
    (va_op_xmm_xmm 3) false false) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_op_xmm_xmm 3) true true) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 5)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 1)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4)
    (va_op_opr128_xmm 2)) (va_CCons (va_code_ZeroXmm (va_op_xmm_xmm 3)) (va_CCons
    (va_code_PinsrdImm (va_op_xmm_xmm 3) 3254779904 3 (va_op_reg_opr64_reg64 rRax)) (va_CCons
    (va_code_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 8)) (va_CNil
    ()))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

val va_codegen_success_MulAdd_unroll : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_MulAdd_unroll () =
  (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3)
    (va_op_reg_opr64_reg64 rR9) (-32) Secret) (va_pbool_and (va_codegen_success_VPolyMul
    (va_op_xmm_xmm 1) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) false false) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) false true)
    (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm
    0) (va_op_reg_opr64_reg64 rRbp) 48 Secret) (va_pbool_and (va_codegen_success_VPolyMul
    (va_op_xmm_xmm 6) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) true false) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) true true)
    (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm
    3) (va_op_reg_opr64_reg64 rR9) (-16) Secret) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 5)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) false false)
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_op_opr128_xmm 4)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4)
    (va_op_xmm_xmm 1) (va_op_opr128_xmm 5)) (va_pbool_and (va_codegen_success_VPolyMul
    (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) false true) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) true false)
    (va_pbool_and (va_codegen_success_Mem128_lemma ()) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3)
    (va_op_reg64_reg64 rRbp) 16 Secret)) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm
    3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) true true) (va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0)
    (va_op_reg_opr64_reg64 rRbp) 64 Secret) (va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64 rR9) 16 Secret)
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 1)) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 1)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 2)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false true)
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7)
    (va_op_opr128_xmm 3)) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 3)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true false) (va_pbool_and (va_codegen_success_VPolyMul
    (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true true) (va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0)
    (va_op_reg_opr64_reg64 rRbp) 80 Secret) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 1)) (va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 1)
    (va_op_reg_opr64_reg64 rR9) 32 Secret) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 2)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 1) false false)
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 3)) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 3)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 1) false true) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 5)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 1) true false)
    (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm
    1) true true) (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 3)
    (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64 rRbp) 96 Secret) (va_pbool_and
    (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 2))
    (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm
    2) (va_op_reg_opr64_reg64 rR9) 64 Secret) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 3)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) false false)
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 5)) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 5)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) false true) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 1)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) true false)
    (va_pbool_and (va_codegen_success_Mem128_lemma ()) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_opr_code_Mem128 (va_op_heaplet_mem_heaplet 3)
    (va_op_reg64_reg64 rRbp) 112 Secret)) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm
    2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) true true) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 3)) (va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3)
    (va_op_reg_opr64_reg64 rR9) 80 Secret) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 5)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 8) (va_op_xmm_xmm 3) false true)
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 1)) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 1)
    (va_op_xmm_xmm 8) (va_op_xmm_xmm 3) true false) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 2)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 8) (va_op_xmm_xmm 3) false false)
    (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_op_xmm_xmm
    3) true true) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)
    (va_op_opr128_xmm 5)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 6)
    (va_op_xmm_xmm 6) (va_op_opr128_xmm 1)) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 2)) (va_pbool_and
    (va_codegen_success_ZeroXmm (va_op_xmm_xmm 3)) (va_pbool_and (va_codegen_success_PinsrdImm
    (va_op_xmm_xmm 3) 3254779904 3 (va_op_reg_opr64_reg64 rRax)) (va_pbool_and
    (va_codegen_success_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 8))
    (va_ttrue ())))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_MulAdd_unroll (va_mods:va_mods_t) (hkeys_b:buffer128) (scratch_b:buffer128) (h:poly)
  (prev:poly) (data:(seq quad32)) : (va_quickCode unit (va_code_MulAdd_unroll ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let (pdata:(Prims.int
    -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in let (data0:poly)
    = pdata 0 in let (data1:poly) = pdata 1 in let (data2:poly) = pdata 2 in let (data3:poly) =
    pdata 3 in let (data4:poly) = pdata 4 in let (data5:poly) = pdata 5 in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 465 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3) (va_op_reg_opr64_reg64
    rR9) (-32) Secret hkeys_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 466 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) false false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 467 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 468 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64
    rRbp) 48 Secret scratch_b 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 469 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 6) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) true false) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 470 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_xmm_xmm 3) true true) (fun
    (va_s:va_state) _ -> let (va_arg128:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 1 in
    let (va_arg127:Vale.Math.Poly2_s.poly) = data5 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 471 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128 va_arg127 va_arg128) (let
    (z:Vale.Math.Poly2_s.poly) = mul data5 (Vale.AES.GHash.gf128_power h 1) in va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 473 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (z == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 0) (let
    (va_arg126:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 6 va_s) in let
    (va_arg125:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 5 va_s) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 475 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.lemma_add_commute va_arg125 va_arg126) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 478 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3) (va_op_reg_opr64_reg64
    rR9) (-16) Secret hkeys_b 1) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 479 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 5)) (fun
    (va_s:va_state) _ -> let (z0:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 1 va_s) in va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 484 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) false false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 485 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_op_opr128_xmm 4)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 486 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 1) (va_op_opr128_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 487 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 488 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) true false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 489 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Mem128_lemma (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 16 Secret
    scratch_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 489 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_opr_code_Mem128
    (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 16 Secret)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 491 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 3) true true) (fun
    (va_s:va_state) _ -> let (va_arg124:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 2 in
    let (va_arg123:Vale.Math.Poly2_s.poly) = data4 in let (va_arg122:Vale.Math.Poly2_s.poly) =
    of_quad32 (va_get_xmm 7 va_s) in let (va_arg121:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm
    6 va_s) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 492 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128_accum z0 va_arg121 va_arg122 va_arg123 va_arg124)
    (let z = add z (mul data4 (Vale.AES.GHash.gf128_power h 2)) in va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 494 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (z == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 497 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64
    rRbp) 64 Secret scratch_b 4) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 498 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64
    rR9) 16 Secret hkeys_b 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 499 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 1)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 503 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 504 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 506 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 507 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 509 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true false) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 510 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true true) (fun
    (va_s:va_state) _ -> let (va_arg120:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 3 in
    let (va_arg119:Vale.Math.Poly2_s.poly) = data3 in let (va_arg118:Vale.Math.Poly2_s.poly) =
    of_quad32 (va_get_xmm 7 va_s) in let (va_arg117:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm
    6 va_s) in let (va_arg116:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 4 va_s) in va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 511 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128_accum va_arg116 va_arg117 va_arg118 va_arg119
    va_arg120) (let z = add z (mul data3 (Vale.AES.GHash.gf128_power h 3)) in va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 513 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (z == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 2) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 516 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64
    rRbp) 80 Secret scratch_b 5) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 517 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 1)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 519 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 1) (va_op_reg_opr64_reg64
    rR9) 32 Secret hkeys_b 4) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 520 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 524 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 1) false false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 525 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 527 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 1) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 528 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 530 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 1) true false) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 531 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 1) true true) (fun
    (va_s:va_state) _ -> let (va_arg115:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 4 in
    let (va_arg114:Vale.Math.Poly2_s.poly) = data2 in let (va_arg113:Vale.Math.Poly2_s.poly) =
    of_quad32 (va_get_xmm 7 va_s) in let (va_arg112:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm
    6 va_s) in let (va_arg111:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 4 va_s) in va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 532 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128_accum va_arg111 va_arg112 va_arg113 va_arg114
    va_arg115) (let z = add z (mul data2 (Vale.AES.GHash.gf128_power h 4)) in va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 534 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (z == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 537 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 3) (va_op_xmm_xmm 0) (va_op_reg_opr64_reg64
    rRbp) 96 Secret scratch_b 6) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 538 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 540 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 2) (va_op_reg_opr64_reg64
    rR9) 64 Secret hkeys_b 6) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 541 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 545 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) false false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 546 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 548 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 549 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 1)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 551 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) true false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 552 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Mem128_lemma (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 112 Secret
    scratch_b 7) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 552 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_opr_code_Mem128
    (va_op_heaplet_mem_heaplet 3) (va_op_reg64_reg64 rRbp) 112 Secret)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 553 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 2) true true) (fun
    (va_s:va_state) _ -> let (va_arg110:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 5 in
    let (va_arg109:Vale.Math.Poly2_s.poly) = data1 in let (va_arg108:Vale.Math.Poly2_s.poly) =
    of_quad32 (va_get_xmm 7 va_s) in let (va_arg107:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm
    6 va_s) in let (va_arg106:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 4 va_s) in va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 554 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128_accum va_arg106 va_arg107 va_arg108 va_arg109
    va_arg110) (let z = add z (mul data1 (Vale.AES.GHash.gf128_power h 5)) in va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 556 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (z == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 4) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 559 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 561 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3) (va_op_reg_opr64_reg64
    rR9) 80 Secret hkeys_b 7) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 562 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 566 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 8) (va_op_xmm_xmm 3) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 567 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 1)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 569 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 8) (va_op_xmm_xmm 3) true false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 570 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 572 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 8) (va_op_xmm_xmm 3) false false) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 573 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_op_xmm_xmm 3) true true) (fun
    (va_s:va_state) _ -> let (va_arg105:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 6 in
    let (va_arg104:Vale.Math.Poly2_s.poly) = add prev data0 in let
    (va_arg103:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 7 va_s) in let
    (va_arg102:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 6 va_s) in let
    (va_arg101:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 4 va_s) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 574 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128_accum va_arg101 va_arg102 va_arg103 va_arg104
    va_arg105) (let z = add z (mul (add prev data0) (Vale.AES.GHash.gf128_power h 6)) in va_qAssert
    va_range1
    "***** PRECONDITION NOT MET AT line 576 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (z == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 5) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 579 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 581 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 6) (va_op_opr128_xmm 1)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 584 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 586 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_ZeroXmm (va_op_xmm_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 587 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_PinsrdImm (va_op_xmm_xmm 3) 3254779904 3 (va_op_reg_opr64_reg64 rRax)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 588 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 8)) (va_QEmpty
    (()))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))


val va_lemma_MulAdd_unroll : va_b0:va_code -> va_s0:va_state -> hkeys_b:buffer128 ->
  scratch_b:buffer128 -> h:poly -> prev:poly -> data:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd_unroll ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in pclmulqdq_enabled /\ avx_enabled /\ sse_enabled /\ FStar.Seq.Base.length #quad32 data == 6
    /\ hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0) (va_get_mem_layout va_s0) (va_get_reg64
    rR9 va_s0 - 32) h /\ scratch_b_data true true scratch_b 8 5 (va_get_mem_heaplet 3 va_s0)
    (va_get_mem_layout va_s0) (va_get_reg64 rRbp va_s0) data /\ va_get_xmm 7 va_s0 ==
    Vale.Def.Types_s.reverse_bytes_quad32 (va_subscript_FStar__Seq__Base__seq data 5) /\ add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s0)) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_s0))) (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read
    scratch_b 1 (va_get_mem_heaplet 3 va_s0))) == prev)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128
    data in add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64))
    (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 5 /\ va_get_xmm 3 va_sM ==
    Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0 0 0 3254779904) /\ va_state_eq 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 rRax va_sM (va_update_flags va_sM (va_update_ok va_sM
    va_s0))))))))))))))
[@"opaque_to_smt"]
let va_lemma_MulAdd_unroll va_b0 va_s0 hkeys_b scratch_b h prev data =
  let (va_mods:va_mods_t) = [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 rRax; va_Mod_flags;
    va_Mod_ok] in
  let va_qc = va_qcode_MulAdd_unroll va_mods hkeys_b scratch_b h prev data in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_MulAdd_unroll ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 427 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_ok va_sM) /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in label va_range1
    "***** POSTCONDITION NOT MET AT line 453 column 55 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_sM)) 64)) (Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM)) 128) ==
    Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 5) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 455 column 44 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_xmm 3 va_sM == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0 0 0 3254779904))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([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 rRax; va_Mod_flags;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_MulAdd_unroll (hkeys_b:buffer128) (scratch_b:buffer128) (h:poly) (prev:poly) (data:(seq
  quad32)) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in pclmulqdq_enabled /\ avx_enabled /\
    sse_enabled /\ FStar.Seq.Base.length #quad32 data == 6 /\ hkeys_b_powers hkeys_b
    (va_get_mem_heaplet 0 va_s0) (va_get_mem_layout va_s0) (va_get_reg64 rR9 va_s0 - 32) h /\
    scratch_b_data true true scratch_b 8 5 (va_get_mem_heaplet 3 va_s0) (va_get_mem_layout va_s0)
    (va_get_reg64 rRbp va_s0) data /\ va_get_xmm 7 va_s0 == Vale.Def.Types_s.reverse_bytes_quad32
    (va_subscript_FStar__Seq__Base__seq data 5) /\ add (add (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_s0)) (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0)))
    (Vale.Math.Poly2.Bits_s.of_quad32 (Vale.X64.Decls.buffer128_read scratch_b 1
    (va_get_mem_heaplet 3 va_s0))) == prev) /\ (forall (va_x_efl:Vale.X64.Flags.t) (va_x_rax: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) . let va_sM =
    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 rRax va_x_rax (va_upd_flags va_x_efl va_s0)))))))))) in
    va_get_ok va_sM /\ (let (pdata:(Prims.int -> Vale.AES.GHash.poly128)) =
    Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in add (add (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_sM)) (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6
    va_sM)) 64)) (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM))
    128) == Vale.AES.GHash.ghash_unroll_back h prev pdata 0 6 5 /\ va_get_xmm 3 va_sM ==
    Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0 0 0 3254779904) ==> va_k va_sM (())))


val va_wpProof_MulAdd_unroll : hkeys_b:buffer128 -> scratch_b:buffer128 -> h:poly -> prev:poly ->
  data:(seq 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_MulAdd_unroll hkeys_b scratch_b h prev data va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MulAdd_unroll ()) ([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 rRax; va_Mod_flags]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_MulAdd_unroll hkeys_b scratch_b h prev data va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_MulAdd_unroll (va_code_MulAdd_unroll ()) va_s0 hkeys_b scratch_b h
    prev data in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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 rRax va_sM (va_update_flags
    va_sM (va_update_ok va_sM va_s0)))))))))))));
  va_lemma_norm_mods ([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 rRax; va_Mod_flags]) va_sM
    va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_MulAdd_unroll (hkeys_b:buffer128) (scratch_b:buffer128) (h:poly) (prev:poly)
  (data:(seq quad32)) : (va_quickCode unit (va_code_MulAdd_unroll ())) =
  (va_QProc (va_code_MulAdd_unroll ()) ([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 rRax;
    va_Mod_flags]) (va_wp_MulAdd_unroll hkeys_b scratch_b h prev data) (va_wpProof_MulAdd_unroll
    hkeys_b scratch_b h prev data))
//--
//-- Reduce

val va_code_Reduce : last_adds:bool -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Reduce last_adds =
  (va_Block (va_CCons (va_code_VLow64ToHigh (va_op_xmm_xmm 5) (va_op_xmm_xmm 6)) (va_CCons
    (va_code_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 5)) (va_CCons
    (va_code_VSwap (va_op_xmm_xmm 0) (va_op_xmm_xmm 4)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm
    4) (va_op_xmm_xmm 4) (va_op_xmm_xmm 3) false true) (va_CCons (va_code_VHigh64ToLow
    (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 7)
    (va_op_xmm_xmm 7) (va_op_opr128_xmm 6)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm 4)
    (va_op_xmm_xmm 4) (va_op_opr128_xmm 0)) (va_CCons (va_code_VSwap (va_op_xmm_xmm 8)
    (va_op_xmm_xmm 4)) (va_CCons (va_code_VPolyMul (va_op_xmm_xmm 4) (va_op_xmm_xmm 4)
    (va_op_xmm_xmm 3) false true) (va_CCons (if last_adds then va_Block (va_CCons (va_code_VPolyAdd
    (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_op_opr128_xmm 7)) (va_CCons (va_code_VPolyAdd
    (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_op_opr128_xmm 4)) (va_CNil ()))) else va_Block (va_CNil
    ())) (va_CNil ()))))))))))))

val va_codegen_success_Reduce : last_adds:bool -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Reduce last_adds =
  (va_pbool_and (va_codegen_success_VLow64ToHigh (va_op_xmm_xmm 5) (va_op_xmm_xmm 6)) (va_pbool_and
    (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 5))
    (va_pbool_and (va_codegen_success_VSwap (va_op_xmm_xmm 0) (va_op_xmm_xmm 4)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_xmm_xmm 3) false true)
    (va_pbool_and (va_codegen_success_VHigh64ToLow (va_op_xmm_xmm 6) (va_op_xmm_xmm 6))
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7)
    (va_op_opr128_xmm 6)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 4)
    (va_op_xmm_xmm 4) (va_op_opr128_xmm 0)) (va_pbool_and (va_codegen_success_VSwap (va_op_xmm_xmm
    8) (va_op_xmm_xmm 4)) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 4)
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 3) false true) (va_pbool_and (if last_adds then va_pbool_and
    (va_codegen_success_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_op_opr128_xmm 7))
    (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8)
    (va_op_opr128_xmm 4)) (va_ttrue ())) else va_ttrue ()) (va_ttrue ())))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Reduce (va_mods:va_mods_t) (last_adds:bool) (f:poly) : (va_quickCode unit
  (va_code_Reduce last_adds)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (g:Vale.Math.Poly2_s.poly) = add (Vale.Math.Poly2_s.monomial 128) f in let
    (c:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.shift f (-1)) 63 in
    let (a0:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s) in let
    (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s) in let
    (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s) in let
    (a:Vale.Math.Poly2_s.poly) = add (add a0 (Vale.Math.Poly2_s.shift a1 64))
    (Vale.Math.Poly2_s.shift a2 128) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 617 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VLow64ToHigh (va_op_xmm_xmm 5) (va_op_xmm_xmm 6)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 618 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 619 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VSwap (va_op_xmm_xmm 0) (va_op_xmm_xmm 4)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 620 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_xmm_xmm 3) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 621 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VHigh64ToLow (va_op_xmm_xmm 6) (va_op_xmm_xmm 6)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 622 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 7) (va_op_xmm_xmm 7) (va_op_opr128_xmm 6)) (fun
    (va_s:va_state) _ -> let (va_arg33:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 0 va_s) in let (va_arg32:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_s) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 623 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.lemma_add_commute va_arg32 va_arg33) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 624 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_opr128_xmm 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 626 column 10 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VSwap (va_op_xmm_xmm 8) (va_op_xmm_xmm 4)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 627 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 4) (va_op_xmm_xmm 4) (va_op_xmm_xmm 3) false true) (fun
    (va_s:va_state) _ -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 628 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_qInlineIf va_mods last_adds (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 630 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_op_opr128_xmm 7)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 631 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 8) (va_op_xmm_xmm 8) (va_op_opr128_xmm 4)) (va_QEmpty
    (()))))) (qblock va_mods (fun (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g ->
    let (va_arg31:Vale.Math.Poly2_s.poly) = f in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 633 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_reduce_rev a0 a1 a2 va_arg31 64) (va_QEmpty
    (())))))))))))))))


val va_lemma_Reduce : va_b0:va_code -> va_s0:va_state -> last_adds:bool -> f:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Reduce last_adds) va_s0 /\ va_get_ok va_s0 /\ (let
    (g:Vale.Math.Poly2_s.poly) = add (Vale.Math.Poly2_s.monomial 128) f in let
    (c:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.shift f (-1)) 63 in
    let (a0:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0) in let
    (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0) in let
    (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0) in let
    (a:Vale.Math.Poly2_s.poly) = add (add a0 (Vale.Math.Poly2_s.shift a1 64))
    (Vale.Math.Poly2_s.shift a2 128) in pclmulqdq_enabled /\ avx_enabled /\ Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 3 va_s0)) (-64) == c /\ Vale.Math.Poly2_s.degree
    f < 64 /\ Vale.Math.Poly2_s.degree g == 128 /\ Vale.Math.Poly2_s.poly_index f 0)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (g:Vale.Math.Poly2_s.poly) = add (Vale.Math.Poly2_s.monomial 128) f in let
    (c:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.shift f (-1)) 63 in
    let (a0:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0) in let
    (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0) in let
    (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0) in let
    (a:Vale.Math.Poly2_s.poly) = add (add a0 (Vale.Math.Poly2_s.shift a1 64))
    (Vale.Math.Poly2_s.shift a2 128) in let xi = (if last_adds then
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM) else add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM)) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 7 va_sM))) (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM))) in xi ==
    Vale.Math.Poly2_s.reverse (mod (Vale.Math.Poly2_s.reverse a 255) g) 127) /\ va_state_eq 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 0 va_sM (va_update_flags va_sM
    (va_update_ok va_sM va_s0)))))))))))
[@"opaque_to_smt"]
let va_lemma_Reduce va_b0 va_s0 last_adds f =
  let (va_mods:va_mods_t) = [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 0; va_Mod_flags; va_Mod_ok] in
  let va_qc = va_qcode_Reduce va_mods last_adds f in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Reduce last_adds) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 593 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_ok va_sM) /\ (let (g:Vale.Math.Poly2_s.poly) = add (Vale.Math.Poly2_s.monomial 128) f
    in let (c:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.shift f (-1))
    63 in let (a0:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0)
    in let (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0) in
    let (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0) in let
    (a:Vale.Math.Poly2_s.poly) = add (add a0 (Vale.Math.Poly2_s.shift a1 64))
    (Vale.Math.Poly2_s.shift a2 128) in label va_range1
    "***** POSTCONDITION NOT MET AT line 614 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (let xi = va_if last_adds (fun _ -> Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM)) (fun
    _ -> add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM))
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM))) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_sM))) in label va_range1
    "***** POSTCONDITION NOT MET AT line 615 column 49 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (xi == Vale.Math.Poly2_s.reverse (mod (Vale.Math.Poly2_s.reverse a 255) g) 127)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([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 0; va_Mod_flags; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Reduce (last_adds:bool) (f:poly) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (let (g:Vale.Math.Poly2_s.poly) = add (Vale.Math.Poly2_s.monomial 128) f in
    let (c:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.shift f (-1)) 63
    in let (a0:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0) in
    let (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0) in let
    (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0) in let
    (a:Vale.Math.Poly2_s.poly) = add (add a0 (Vale.Math.Poly2_s.shift a1 64))
    (Vale.Math.Poly2_s.shift a2 128) in pclmulqdq_enabled /\ avx_enabled /\ Vale.Math.Poly2_s.shift
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 3 va_s0)) (-64) == c /\ Vale.Math.Poly2_s.degree
    f < 64 /\ Vale.Math.Poly2_s.degree g == 128 /\ Vale.Math.Poly2_s.poly_index f 0) /\ (forall
    (va_x_efl:Vale.X64.Flags.t) (va_x_xmm0: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) . let va_sM =
    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 0 va_x_xmm0 (va_upd_flags va_x_efl
    va_s0))))))) in va_get_ok va_sM /\ (let (g:Vale.Math.Poly2_s.poly) = add
    (Vale.Math.Poly2_s.monomial 128) f in let (c:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.shift f (-1)) 63 in let
    (a0:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_s0) in let
    (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 6 va_s0) in let
    (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_s0) in let
    (a:Vale.Math.Poly2_s.poly) = add (add a0 (Vale.Math.Poly2_s.shift a1 64))
    (Vale.Math.Poly2_s.shift a2 128) in let xi = va_if last_adds (fun _ ->
    Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM)) (fun _ -> add (add
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM)) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 7 va_sM))) (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 4 va_sM))) in xi ==
    Vale.Math.Poly2_s.reverse (mod (Vale.Math.Poly2_s.reverse a 255) g) 127) ==> va_k va_sM (())))


val va_wpProof_Reduce : last_adds:bool -> f:poly -> va_s0:va_state -> va_k:(va_state -> unit ->
  Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Reduce last_adds f va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Reduce last_adds) ([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 0;
    va_Mod_flags]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Reduce last_adds f va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Reduce (va_code_Reduce last_adds) va_s0 last_adds f in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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 0 va_sM
    (va_update_flags va_sM (va_update_ok va_sM va_s0))))))))));
  va_lemma_norm_mods ([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 0; va_Mod_flags]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Reduce (last_adds:bool) (f:poly) : (va_quickCode unit (va_code_Reduce last_adds)) =
  (va_QProc (va_code_Reduce last_adds) ([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 0; va_Mod_flags]) (va_wp_Reduce last_adds f)
    (va_wpProof_Reduce last_adds f))
//--
//-- ReduceLast

[@ "opaque_to_smt" va_qattr]
let va_code_ReduceLast last_adds =
  (va_Block (va_CCons (va_code_Reduce last_adds) (va_CCons (va_Block (va_CNil ())) (va_CCons
    (va_Block (va_CNil ())) (va_CNil ())))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_ReduceLast last_adds =
  (va_pbool_and (va_codegen_success_Reduce last_adds) (va_ttrue ()))

[@ "opaque_to_smt" va_qattr]
let va_qcode_ReduceLast (va_mods:va_mods_t) (last_adds:bool) (h_LE:quad32) (y_prev:quad32)
  (data:(seq quad32)) : (va_quickCode unit (va_code_ReduceLast last_adds)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 664 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_gf128_low_shift ()) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 665 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_gf128_degree ()) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 666 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Reduce last_adds gf128_modulus_low_terms) (fun (va_s:va_state) _ -> va_qAssertSquash
    va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 668 column 36 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (n - 1 >= 0) (fun _ -> let (va_arg27:Prims.nat) = n - 1 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 668 column 36 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GHash.lemma_ghash_unroll_back_forward h prev pdata 0 va_arg27)
    (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 670 column 31 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (n - 1 >= 0) (fun _ -> let (va_arg26:Prims.nat) = n - 1 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 670 column 31 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GHash.lemma_ghash_poly_of_unroll h prev pdata 0 va_arg26) (let
    (va_arg25:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = data in let
    (va_arg24:Vale.Def.Types_s.quad32) = y_prev in let (va_arg23:Vale.Def.Types_s.quad32) = h_LE in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 672 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GHash.lemma_ghash_incremental_poly va_arg23 va_arg24 va_arg25) (let
    (va_arg22:Vale.Def.Types_s.quad32) = Vale.Def.Types_s.reverse_bytes_quad32
    (Vale.AES.GHash.ghash_incremental h_LE y_prev data) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 674 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Bits.lemma_to_of_quad32 va_arg22) (va_QEmpty (()))))))))))))

[@"opaque_to_smt"]
let va_lemma_ReduceLast va_b0 va_s0 last_adds h_LE y_prev data =
  let (va_mods:va_mods_t) = [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 0; va_Mod_flags; va_Mod_ok] in
  let va_qc = va_qcode_ReduceLast va_mods last_adds h_LE y_prev data in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_ReduceLast last_adds) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 636 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_ok va_sM) /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in label va_range1
    "***** POSTCONDITION NOT MET AT line 660 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (let xi = va_if last_adds (fun _ -> Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM)) (fun
    _ -> add (add (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_sM))
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 7 va_sM))) (Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 4 va_sM))) in label va_range1
    "***** POSTCONDITION NOT MET AT line 661 column 85 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (Vale.Math.Poly2.Bits_s.to_quad32 xi == Vale.Def.Types_s.reverse_bytes_quad32
    (Vale.AES.GHash.ghash_incremental h_LE y_prev data)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 662 column 39 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (xi == Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Math.Poly2.Bits_s.to_quad32 xi))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([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 0; va_Mod_flags; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_ReduceLast last_adds h_LE y_prev data va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_ReduceLast (va_code_ReduceLast last_adds) va_s0 last_adds h_LE
    y_prev data in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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 0 va_sM
    (va_update_flags va_sM (va_update_ok va_sM va_s0))))))))));
  va_lemma_norm_mods ([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 0; va_Mod_flags]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- GhashUnroll_n

[@ "opaque_to_smt" va_qattr]
let va_code_GhashUnroll_n rev_bytes rev_blocks exactly6 =
  (va_Block (va_CCons (va_code_MulAdd_unroll_n rev_bytes rev_blocks exactly6) (va_CCons
    (va_code_ZeroXmm (va_op_xmm_xmm 3)) (va_CCons (va_code_PinsrdImm (va_op_xmm_xmm 3) 3254779904 3
    (va_op_reg_opr64_reg64 rR10)) (va_CCons (va_code_ReduceLast true) (va_CNil ()))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_GhashUnroll_n rev_bytes rev_blocks exactly6 =
  (va_pbool_and (va_codegen_success_MulAdd_unroll_n rev_bytes rev_blocks exactly6) (va_pbool_and
    (va_codegen_success_ZeroXmm (va_op_xmm_xmm 3)) (va_pbool_and (va_codegen_success_PinsrdImm
    (va_op_xmm_xmm 3) 3254779904 3 (va_op_reg_opr64_reg64 rR10)) (va_pbool_and
    (va_codegen_success_ReduceLast true) (va_ttrue ())))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_GhashUnroll_n (va_mods:va_mods_t) (rev_bytes:bool) (rev_blocks:bool) (exactly6:bool)
  (scratch_len:nat64) (hkeys_b:buffer128) (scratch_in_b:buffer128) (h_LE:quad32) (y_prev:quad32)
  (data:(seq quad32)) : (va_quickCode unit (va_code_GhashUnroll_n rev_bytes rev_blocks exactly6)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) =
    index_opt_rev rev_blocks scratch_len n (n - 1) in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 719 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_MulAdd_unroll_n rev_bytes rev_blocks exactly6 scratch_len hkeys_b scratch_in_b h prev
    data) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 720 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_ZeroXmm (va_op_xmm_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 721 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_PinsrdImm (va_op_xmm_xmm 3) 3254779904 3 (va_op_reg_opr64_reg64 rR10)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 722 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_ReduceLast true h_LE y_prev data) (va_QEmpty (())))))))

[@"opaque_to_smt"]
let va_lemma_GhashUnroll_n va_b0 va_s0 rev_bytes rev_blocks exactly6 scratch_len hkeys_b
  scratch_in_b h_LE y_prev data =
  let (va_mods:va_mods_t) = [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 rR10;
    va_Mod_flags; va_Mod_ok] in
  let va_qc = va_qcode_GhashUnroll_n va_mods rev_bytes rev_blocks exactly6 scratch_len hkeys_b
    scratch_in_b h_LE y_prev data in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_GhashUnroll_n rev_bytes rev_blocks
    exactly6) va_qc va_s0 (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 677 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_ok va_sM) /\ (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (prev:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let
    (pdata:(Prims.int -> Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data
    in let (n:Prims.nat) = FStar.Seq.Base.length #quad32 data in let (scratch_index:int) =
    index_opt_rev rev_blocks scratch_len n (n - 1) in label va_range1
    "***** POSTCONDITION NOT MET AT line 716 column 74 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_xmm 8 va_sM == Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental
    h_LE y_prev data)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 717 column 75 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (l_and exactly6 (~rev_blocks) ==> va_get_reg64 rR11 va_sM == va_get_reg64 rR11 va_s0 - 80))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([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 rR10;
    va_Mod_flags; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_GhashUnroll_n rev_bytes rev_blocks exactly6 scratch_len hkeys_b scratch_in_b h_LE
  y_prev data va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_GhashUnroll_n (va_code_GhashUnroll_n rev_bytes rev_blocks exactly6)
    va_s0 rev_bytes rev_blocks exactly6 scratch_len hkeys_b scratch_in_b h_LE y_prev data in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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 rR10
    va_sM (va_update_flags va_sM (va_update_ok va_sM va_s0))))))))))))));
  va_lemma_norm_mods ([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 rR10;
    va_Mod_flags]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Ghash_register

[@ "opaque_to_smt" va_qattr]
let va_code_Ghash_register () =
  (va_Block (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5)
    (va_op_reg_opr64_reg64 rR9) (-32) Secret) (va_CCons (va_Block (va_CNil ())) (va_CCons
    (va_code_VPolyAdd (va_op_xmm_xmm 0) (va_op_xmm_xmm 8) (va_op_opr128_xmm 0)) (va_CCons
    (va_code_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false) (va_CCons
    (va_code_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false true) (va_CCons
    (va_code_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true false) (va_CCons
    (va_code_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true true) (va_CCons
    (va_code_Mov128 (va_op_xmm_xmm 4) (va_op_xmm_xmm 1)) (va_CCons (va_code_VPolyAdd (va_op_xmm_xmm
    6) (va_op_xmm_xmm 2) (va_op_opr128_xmm 3)) (va_CCons (va_code_Mov128 (va_op_xmm_xmm 7)
    (va_op_xmm_xmm 5)) (va_CCons (va_code_ZeroXmm (va_op_xmm_xmm 3)) (va_CCons (va_code_PinsrdImm
    (va_op_xmm_xmm 3) 3254779904 3 (va_op_reg_opr64_reg64 rR11)) (va_CCons (va_code_Reduce true)
    (va_CNil ())))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Ghash_register () =
  (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5)
    (va_op_reg_opr64_reg64 rR9) (-32) Secret) (va_pbool_and (va_codegen_success_VPolyAdd
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 8) (va_op_opr128_xmm 0)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false)
    (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm
    5) false true) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0)
    (va_op_xmm_xmm 5) true false) (va_pbool_and (va_codegen_success_VPolyMul (va_op_xmm_xmm 5)
    (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true true) (va_pbool_and (va_codegen_success_Mov128
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 1)) (va_pbool_and (va_codegen_success_VPolyAdd (va_op_xmm_xmm
    6) (va_op_xmm_xmm 2) (va_op_opr128_xmm 3)) (va_pbool_and (va_codegen_success_Mov128
    (va_op_xmm_xmm 7) (va_op_xmm_xmm 5)) (va_pbool_and (va_codegen_success_ZeroXmm (va_op_xmm_xmm
    3)) (va_pbool_and (va_codegen_success_PinsrdImm (va_op_xmm_xmm 3) 3254779904 3
    (va_op_reg_opr64_reg64 rR11)) (va_pbool_and (va_codegen_success_Reduce true) (va_ttrue
    ())))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Ghash_register (va_mods:va_mods_t) (hkeys_b:buffer128) (h_LE:quad32) (y_prev:quad32) :
  (va_quickCode unit (va_code_Ghash_register ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 755 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64
    rR9) (-32) Secret hkeys_b 0) (fun (va_s:va_state) _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 756 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 5 va_s) == Vale.AES.GHash.gf128_power h 1)
    (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 758 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (0 >= 0 /\ (fun a_336 (s_337:(FStar.Seq.Base.seq a_336)) (i_338:Prims.nat) -> let
    (i_312:Prims.nat) = i_338 in Prims.b2t (Prims.op_LessThan i_312 (FStar.Seq.Base.length #a_336
    s_337))) Vale.Def.Types_s.quad32 data 0) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 758 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_get_xmm 0 va_s == Vale.Def.Types_s.reverse_bytes_quad32 (FStar.Seq.Base.index
    #Vale.Def.Types_s.quad32 data 0)) (let (data_i:poly) = pdata 0 in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 760 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 0) (va_op_xmm_xmm 8) (va_op_opr128_xmm 0)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 761 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 1) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false false) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 762 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 2) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) false true) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 763 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 3) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true false) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 764 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyMul (va_op_xmm_xmm 5) (va_op_xmm_xmm 0) (va_op_xmm_xmm 5) true true) (fun
    (va_s:va_state) _ -> let (va_arg54:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 1 in
    let (va_arg53:Vale.Math.Poly2_s.poly) = add prev data_i in let
    (va_arg52:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 7 va_s) in let
    (va_arg51:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 6 va_s) in let
    (va_arg50:Vale.Math.Poly2_s.poly) = of_quad32 (va_get_xmm 4 va_s) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 765 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128_accum va_arg50 va_arg51 va_arg52 va_arg53
    va_arg54) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 766 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 4) (va_op_xmm_xmm 1)) (fun (va_s:va_state) _ -> let
    (va_arg49:Vale.Math.Poly2_s.poly) = Vale.AES.GHash.gf128_power h 1 in let
    (va_arg48:Vale.Math.Poly2_s.poly) = add prev data_i in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 767 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_Mul128 va_arg48 va_arg49) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 768 column 13 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_VPolyAdd (va_op_xmm_xmm 6) (va_op_xmm_xmm 2) (va_op_opr128_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 769 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 7) (va_op_xmm_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 770 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_ZeroXmm (va_op_xmm_xmm 3)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 771 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_PinsrdImm (va_op_xmm_xmm 3) 3254779904 3 (va_op_reg_opr64_reg64 rR11)) (fun
    (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 772 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_gf128_low_shift ()) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 773 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_gf128_degree ()) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 774 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (va_quick_Reduce true gf128_modulus_low_terms) (fun (va_s:va_state) _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 775 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s) == Vale.AES.GF128.mod_rev 128
    (Vale.AES.GHash.ghash_unroll_back h prev pdata 0 1 0) gf128_modulus) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 776 column 36 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GHash.lemma_ghash_unroll_back_forward h prev pdata 0 0) (va_qAssert
    va_range1
    "***** PRECONDITION NOT MET AT line 777 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s) == Vale.AES.GF128.mod_rev 128
    (Vale.AES.GHash.ghash_unroll h prev pdata 0 0 0) gf128_modulus) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 778 column 31 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GHash.lemma_ghash_poly_of_unroll h prev pdata 0 0) (va_qAssert
    va_range1
    "***** PRECONDITION NOT MET AT line 779 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s) == Vale.AES.GHash.ghash_poly h prev pdata
    0 1) (let (va_arg47:Vale.Def.Types_s.quad32) = y_prev in let (va_arg46:Vale.Def.Types_s.quad32)
    = h_LE in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 780 column 33 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.AES.GHash.lemma_ghash_incremental_poly va_arg46 va_arg47 data)
    (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 781 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_xmm 8 va_s) == Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE y_prev data)))
    (let (va_arg45:Vale.Def.Types_s.quad32) = Vale.Def.Types_s.reverse_bytes_quad32
    (Vale.AES.GHash.ghash_incremental h_LE y_prev data) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 782 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes/Vale.AES.X64.AESopt2.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Bits.lemma_to_of_quad32 va_arg45) (va_QEmpty
    (()))))))))))))))))))))))))))))))
val va_lemma_Ghash_register : va_b0:va_code -> va_s0:va_state -> hkeys_b:buffer128 -> h_LE:quad32
  -> y_prev:quad32
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Ghash_register ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in pclmulqdq_enabled
    /\ avx_enabled /\ sse_enabled /\ hkeys_b_powers hkeys_b (va_get_mem_heaplet 0 va_s0)
    (va_get_mem_layout va_s0) (va_get_reg64 rR9 va_s0 - 32) h /\ Vale.Math.Poly2.Bits_s.of_quad32
    (va_get_xmm 8 va_s0) == prev)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (h:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 h_LE) in let (data:(FStar.Seq.Base.seq
    Vale.Def.Types_s.quad32)) = FStar.Seq.Base.create #Vale.Def.Types_s.quad32 1
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_get_xmm 0 va_s0)) in let
    (prev:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32
    (Vale.Def.Types_s.reverse_bytes_quad32 y_prev) in let (pdata:(Prims.int ->
    Vale.AES.GHash.poly128)) = Vale.AES.GHash.fun_seq_quad32_LE_poly128 data in va_get_xmm 8 va_sM
    == Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.GHash.ghash_incremental h_LE y_prev data))
    /\ va_state_eq 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_flags
    va_sM (va_update_ok va_sM va_s0))))))))))))))

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    hkeys_b: Vale.X64.Memory.buffer128 ->
    h_LE: Vale.X64.Decls.quad32 ->
    y_prev: Vale.X64.Decls.quad32
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)