val va_qcode_ClmulRev64High (va_mods: va_mods_t) (a b: poly)
    : (va_quickCode unit (va_code_ClmulRev64High ()))
let va_qcode_ClmulRev64High (va_mods:va_mods_t) (a:poly) (b:poly) : (va_quickCode unit
  (va_code_ClmulRev64High ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (va_arg18:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 1 va_s) in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 116 column 24 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Bits.lemma_quad32_double va_arg18) (let
    (va_arg17:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 2 va_s) in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 117 column 24 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Bits.lemma_quad32_double va_arg17) (let
    (va_arg16:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 1 va_s) in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 118 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Lemmas.lemma_mask_is_mod va_arg16 64) (let
    (va_arg15:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 2 va_s) in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 119 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Lemmas.lemma_mask_is_mod va_arg15 64) (let
    (va_arg14:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 1 va_s) in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 120 column 23 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Lemmas.lemma_shift_is_div va_arg14 64) (let
    (va_arg13:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 2 va_s) in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 121 column 23 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Lemmas.lemma_shift_is_div va_arg13 64) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 122 column 17 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_VPolyMulHigh (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 2))
    (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 123 column 19 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_ShiftLeft128_1 (Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.reverse a 63)
    (Vale.Math.Poly2_s.reverse b 63))) (fun (va_s:va_state) _ -> let
    (va_arg12:Vale.Math.Poly2_s.poly) = b in let (va_arg11:Vale.Math.Poly2_s.poly) = a in va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 125 column 30 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Lemmas.lemma_mul_reverse_shift_1 va_arg11 va_arg12 63)
    (va_QEmpty (()))))))))))))
val va_qcode_ClmulRev64High (va_mods: va_mods_t) (a b: poly)
    : (va_quickCode unit (va_code_ClmulRev64High ()))
let va_qcode_ClmulRev64High (va_mods: va_mods_t) (a b: poly)
    : (va_quickCode unit (va_code_ClmulRev64High ())) =
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        let va_arg18:Vale.Math.Poly2_s.poly =
          Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 1 va_s)
        in
        va_qPURE va_range1
          "***** PRECONDITION NOT MET AT line 116 column 24 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
          (fun (_: unit) -> Vale.Math.Poly2.Bits.lemma_quad32_double va_arg18)
          (let va_arg17:Vale.Math.Poly2_s.poly =
              Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 2 va_s)
            in
            va_qPURE va_range1
              "***** PRECONDITION NOT MET AT line 117 column 24 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
              (fun (_: unit) -> Vale.Math.Poly2.Bits.lemma_quad32_double va_arg17)
              (let va_arg16:Vale.Math.Poly2_s.poly =
                  Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 1 va_s)
                in
                va_qPURE va_range1
                  "***** PRECONDITION NOT MET AT line 118 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
                  (fun (_: unit) -> Vale.Math.Poly2.Lemmas.lemma_mask_is_mod va_arg16 64)
                  (let va_arg15:Vale.Math.Poly2_s.poly =
                      Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 2 va_s)
                    in
                    va_qPURE va_range1
                      "***** PRECONDITION NOT MET AT line 119 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
                      (fun (_: unit) -> Vale.Math.Poly2.Lemmas.lemma_mask_is_mod va_arg15 64)
                      (let va_arg14:Vale.Math.Poly2_s.poly =
                          Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 1 va_s)
                        in
                        va_qPURE va_range1
                          "***** PRECONDITION NOT MET AT line 120 column 23 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
                          (fun (_: unit) -> Vale.Math.Poly2.Lemmas.lemma_shift_is_div va_arg14 64)
                          (let va_arg13:Vale.Math.Poly2_s.poly =
                              Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 2 va_s)
                            in
                            va_qPURE va_range1
                              "***** PRECONDITION NOT MET AT line 121 column 23 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
                              (fun (_: unit) ->
                                  Vale.Math.Poly2.Lemmas.lemma_shift_is_div va_arg13 64)
                              (va_QSeq va_range1
                                  "***** PRECONDITION NOT MET AT line 122 column 17 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
                                  (va_quick_VPolyMulHigh (va_op_vec_opr_vec 1)
                                      (va_op_vec_opr_vec 1)
                                      (va_op_vec_opr_vec 2))
                                  (va_QBind va_range1
                                      "***** PRECONDITION NOT MET AT line 123 column 19 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
                                      (va_quick_ShiftLeft128_1 (Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.reverse
                                                  a
                                                  63)
                                              (Vale.Math.Poly2_s.reverse b 63)))
                                      (fun (va_s: va_state) _ ->
                                          let va_arg12:Vale.Math.Poly2_s.poly = b in
                                          let va_arg11:Vale.Math.Poly2_s.poly = a in
                                          va_qPURE va_range1
                                            "***** PRECONDITION NOT MET AT line 125 column 30 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
                                            (fun (_: unit) ->
                                                Vale.Math.Poly2.Lemmas.lemma_mul_reverse_shift_1 va_arg11
                                                  va_arg12
                                                  63)
                                            (va_QEmpty (()))))))))))))
Vale.AES.PPC64LE.GF128_Mul.fst.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.QuickCodes.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsVector.fsti.checked Vale.PPC64LE.InsMem.fsti.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fsti.checked Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Words.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.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.Types_helpers.fsti.checked Vale.AES.PPC64LE.PolyOps.fsti.checked Vale.AES.GHash_BE.fsti.checked Vale.AES.GF128_s.fsti.checked Vale.AES.GF128.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.PPC64LE.GF128_Mul.fst
Vale.PPC64LE.QuickCode.va_mods_t Vale.Math.Poly2_s.poly Vale.PPC64LE.QuickCodes.qblock Prims.unit Prims.Cons Vale.PPC64LE.Decls.va_code Vale.AES.PPC64LE.PolyOps.va_code_VPolyMulHigh Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.AES.PPC64LE.GF128_Mul.va_code_ShiftLeft128_1 Prims.Nil Vale.PPC64LE.Machine_s.precode Vale.PPC64LE.Decls.ins Vale.PPC64LE.Decls.ocmp Vale.PPC64LE.Decls.va_state Vale.PPC64LE.QuickCodes.va_qPURE Prims.pure_post Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Vale.Math.Poly2_s.degree Prims.l_Forall Prims.l_imp Prims.eq2 Vale.Math.Poly2.Bits_s.of_double32 Vale.Arch.Types.quad32_double_lo Vale.Math.Poly2.Bits_s.to_quad32 Vale.Math.Poly2_s.mod Vale.Math.Poly2_s.monomial Vale.Arch.Types.quad32_double_hi Vale.Math.Poly2_s.div Vale.Math.Poly2_s.add Vale.Math.Poly2_s.mul Vale.Math.Poly2_s.shift Vale.PPC64LE.QuickCodes.va_range1 Vale.Math.Poly2.Bits.lemma_quad32_double Prims.l_True Vale.Math.Poly2.mask Vale.Math.Poly2.Lemmas.lemma_mask_is_mod Prims.op_Minus Vale.Math.Poly2.Lemmas.lemma_shift_is_div Vale.PPC64LE.QuickCodes.va_QSeq Vale.AES.PPC64LE.PolyOps.va_quick_VPolyMulHigh Vale.PPC64LE.QuickCodes.va_QBind Vale.AES.PPC64LE.GF128_Mul.va_quick_ShiftLeft128_1 Vale.Math.Poly2_s.reverse Prims.op_Addition Vale.Math.Poly2.Lemmas.lemma_mul_reverse_shift_1 Vale.PPC64LE.QuickCodes.va_QEmpty Vale.PPC64LE.QuickCodes.quickCodes Vale.Math.Poly2.Bits_s.of_quad32 Vale.PPC64LE.Decls.va_get_vec Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCode.va_quickCode Vale.AES.PPC64LE.GF128_Mul.va_code_ClmulRev64High
module Vale.AES.PPC64LE.GF128_Mul
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.TypesNative
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.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.InsBasic
open Vale.PPC64LE.InsMem
open Vale.PPC64LE.InsVector
open Vale.PPC64LE.QuickCode
open Vale.PPC64LE.QuickCodes
open Vale.AES.PPC64LE.PolyOps
open Vale.AES.Types_helpers
open Vale.AES.GHash_BE
//-- ShiftLeft128_1

[@ "opaque_to_smt" va_qattr]
let va_code_ShiftLeft128_1 () =
  (va_Block (va_CCons (va_code_Vspltisb (va_op_vec_opr_vec 2) 1) (va_CCons (va_code_Vsl
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 2)) (va_CNil ()))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_ShiftLeft128_1 () =
  (va_pbool_and (va_codegen_success_Vspltisb (va_op_vec_opr_vec 2) 1) (va_pbool_and
    (va_codegen_success_Vsl (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 2))
    (va_ttrue ())))

[@ "opaque_to_smt" va_qattr]
let va_qcode_ShiftLeft128_1 (va_mods:va_mods_t) (a:poly) : (va_quickCode unit
  (va_code_ShiftLeft128_1 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 60 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vspltisb (va_op_vec_opr_vec 2) 1) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 61 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vsl (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 2)) (fun
    (va_s:va_state) _ -> let (va_arg5:Vale.Math.Poly2_s.poly) = a in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 63 column 23 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_shift_left_1 va_arg5) (va_QEmpty (()))))))

[@"opaque_to_smt"]
let va_lemma_ShiftLeft128_1 va_b0 va_s0 a =
  let (va_mods:va_mods_t) = [va_Mod_vec 2; va_Mod_vec 1; va_Mod_ok] in
  let va_qc = va_qcode_ShiftLeft128_1 va_mods a in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_ShiftLeft128_1 ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 49 column 1 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 58 column 37 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.shift a 1))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 2; va_Mod_vec 1; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_ShiftLeft128_1 a va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_ShiftLeft128_1 (va_code_ShiftLeft128_1 ()) va_s0 a in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 2 va_sM (va_update_vec 1 va_sM (va_update_ok va_sM
    va_s0))));
  va_lemma_norm_mods ([va_Mod_vec 2; va_Mod_vec 1]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- ShiftLeft2_128_1

val va_code_ShiftLeft2_128_1 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_ShiftLeft2_128_1 () =
  (va_Block (va_CCons (va_code_Vspltisw (va_op_vec_opr_vec 0) 0) (va_CCons (va_code_LoadImm64
    (va_op_reg_opr_reg 10) 31) (va_CCons (va_code_Mtvsrws (va_op_vec_opr_vec 3) (va_op_reg_opr_reg
    10)) (va_CCons (va_code_Vsrw (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 3))
    (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 3) 4)
    (va_CCons (va_code_Vspltisb (va_op_vec_opr_vec 0) 1) (va_CCons (va_code_Vsl (va_op_vec_opr_vec
    1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 0)) (va_CCons (va_code_Vsl (va_op_vec_opr_vec 2)
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 0)) (va_CCons (va_code_Vxor (va_op_vec_opr_vec 2)
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3)) (va_CNil ())))))))))))

val va_codegen_success_ShiftLeft2_128_1 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_ShiftLeft2_128_1 () =
  (va_pbool_and (va_codegen_success_Vspltisw (va_op_vec_opr_vec 0) 0) (va_pbool_and
    (va_codegen_success_LoadImm64 (va_op_reg_opr_reg 10) 31) (va_pbool_and
    (va_codegen_success_Mtvsrws (va_op_vec_opr_vec 3) (va_op_reg_opr_reg 10)) (va_pbool_and
    (va_codegen_success_Vsrw (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 3))
    (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 0)
    (va_op_vec_opr_vec 3) 4) (va_pbool_and (va_codegen_success_Vspltisb (va_op_vec_opr_vec 0) 1)
    (va_pbool_and (va_codegen_success_Vsl (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 0)) (va_pbool_and (va_codegen_success_Vsl (va_op_vec_opr_vec 2)
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 0)) (va_pbool_and (va_codegen_success_Vxor
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3)) (va_ttrue ()))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_ShiftLeft2_128_1 (va_mods:va_mods_t) (lo:poly) (hi:poly) : (va_quickCode unit
  (va_code_ShiftLeft2_128_1 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 83 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vspltisw (va_op_vec_opr_vec 0) 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 84 column 14 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_LoadImm64 (va_op_reg_opr_reg 10) 31) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 85 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Mtvsrws (va_op_vec_opr_vec 3) (va_op_reg_opr_reg 10)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 86 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vsrw (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 3)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 87 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 3) 4) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 88 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vspltisb (va_op_vec_opr_vec 0) 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 89 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vsl (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 0)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 90 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vsl (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 0)) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 91 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3)) (fun
    (va_s:va_state) _ -> let (l:(Vale.Def.Words_s.four Vale.Def.Words_s.nat32)) =
    Vale.Def.Words.Four_s.four_map #nat32 #Vale.Def.Words_s.nat32 (fun (i:nat32) ->
    Vale.Arch.Types.ishl32 i 1) (va_get_vec 2 va_old_s) in let (r:(Vale.Def.Words_s.four
    Vale.Def.Words_s.nat32)) = Vale.Def.Words.Four_s.four_map #nat32 #Vale.Def.Words_s.nat32 (fun
    (i:nat32) -> Vale.Arch.Types.ishr32 i 31) (va_get_vec 2 va_old_s) in let
    (va_arg22:Vale.Def.Types_s.quad32) = va_get_vec 3 va_s in let
    (va_arg21:Vale.Def.Types_s.quad32) = Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 r) (Vale.Def.Words_s.__proj__Mkfour__item__lo1 r)
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 r) in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 95 column 30 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Arch.TypesNative.lemma_quad32_xor_commutes va_arg21 va_arg22) (let
    (va_arg20:Vale.Def.Types_s.quad32) = va_get_vec 3 va_s in let
    (va_arg19:Vale.Def.Types_s.quad32) = Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 r) (Vale.Def.Words_s.__proj__Mkfour__item__lo1 r)
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 r) in let (va_arg18:Vale.Def.Types_s.quad32) = l in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 96 column 32 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Arch.TypesNative.lemma_quad32_xor_associates va_arg18 va_arg19 va_arg20)
    (let (va_arg17:Vale.Math.Poly2_s.poly) = hi in let (va_arg16:Vale.Math.Poly2_s.poly) = lo in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 98 column 25 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_shift_2_left_1 va_arg16 va_arg17) (va_QEmpty
    (())))))))))))))))


val va_lemma_ShiftLeft2_128_1 : va_b0:va_code -> va_s0:va_state -> lo:poly -> hi:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_ShiftLeft2_128_1 ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree hi < 127 /\ Vale.Math.Poly2_s.degree lo <= 127 /\ va_get_vec 1 va_s0
    == Vale.Math.Poly2.Bits_s.to_quad32 lo /\ va_get_vec 2 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 hi))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let n = Vale.Math.Poly2_s.monomial 128 in let a = Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.mul
    hi n) lo in let b = Vale.Math.Poly2_s.shift a 1 in va_get_vec 1 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mod b n) /\ va_get_vec 2 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.div b n)) /\ va_state_eq va_sM
    (va_update_vec 3 va_sM (va_update_vec 2 va_sM (va_update_vec 1 va_sM (va_update_vec 0 va_sM
    (va_update_reg 10 va_sM (va_update_ok va_sM va_s0))))))))
[@"opaque_to_smt"]
let va_lemma_ShiftLeft2_128_1 va_b0 va_s0 lo hi =
  let (va_mods:va_mods_t) = [va_Mod_vec 3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 10;
    va_Mod_ok] in
  let va_qc = va_qcode_ShiftLeft2_128_1 va_mods lo hi in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_ShiftLeft2_128_1 ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 66 column 1 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 77 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (let n = Vale.Math.Poly2_s.monomial 128 in label va_range1
    "***** POSTCONDITION NOT MET AT line 78 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (let a = Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.mul hi n) lo in label va_range1
    "***** POSTCONDITION NOT MET AT line 79 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (let b = Vale.Math.Poly2_s.shift a 1 in label va_range1
    "***** POSTCONDITION NOT MET AT line 80 column 35 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mod b n)) /\ label
    va_range1
    "***** POSTCONDITION NOT MET AT line 81 column 35 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_vec 2 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.div b n)))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 10;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_ShiftLeft2_128_1 (lo:poly) (hi:poly) (va_s0:va_state) (va_k:(va_state -> unit -> Type0))
  : Type0 =
  (va_get_ok va_s0 /\ Vale.Math.Poly2_s.degree hi < 127 /\ Vale.Math.Poly2_s.degree lo <= 127 /\
    va_get_vec 1 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 lo /\ va_get_vec 2 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 hi /\ (forall (va_x_r10:nat64) (va_x_v0:quad32)
    (va_x_v1:quad32) (va_x_v2:quad32) (va_x_v3:quad32) . let va_sM = va_upd_vec 3 va_x_v3
    (va_upd_vec 2 va_x_v2 (va_upd_vec 1 va_x_v1 (va_upd_vec 0 va_x_v0 (va_upd_reg 10 va_x_r10
    va_s0)))) in va_get_ok va_sM /\ (let n = Vale.Math.Poly2_s.monomial 128 in let a =
    Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.mul hi n) lo in let b = Vale.Math.Poly2_s.shift a 1 in
    va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mod b n) /\
    va_get_vec 2 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.div b n)) ==> va_k
    va_sM (())))


val va_wpProof_ShiftLeft2_128_1 : lo:poly -> hi: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_ShiftLeft2_128_1 lo hi va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_ShiftLeft2_128_1 ()) ([va_Mod_vec 3;
    va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 10]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_ShiftLeft2_128_1 lo hi va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_ShiftLeft2_128_1 (va_code_ShiftLeft2_128_1 ()) va_s0 lo hi in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 3 va_sM (va_update_vec 2 va_sM (va_update_vec 1 va_sM
    (va_update_vec 0 va_sM (va_update_reg 10 va_sM (va_update_ok va_sM va_s0)))))));
  va_lemma_norm_mods ([va_Mod_vec 3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 10])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_ShiftLeft2_128_1 (lo:poly) (hi:poly) : (va_quickCode unit (va_code_ShiftLeft2_128_1
  ())) =
  (va_QProc (va_code_ShiftLeft2_128_1 ()) ([va_Mod_vec 3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0;
    va_Mod_reg 10]) (va_wp_ShiftLeft2_128_1 lo hi) (va_wpProof_ShiftLeft2_128_1 lo hi))
//--
//-- ClmulRev64High

val va_code_ClmulRev64High : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_ClmulRev64High () =
  (va_Block (va_CCons (va_code_VPolyMulHigh (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 2)) (va_CCons (va_code_ShiftLeft128_1 ()) (va_CNil ()))))

val va_codegen_success_ClmulRev64High : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_ClmulRev64High () =
  (va_pbool_and (va_codegen_success_VPolyMulHigh (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 2)) (va_pbool_and (va_codegen_success_ShiftLeft128_1 ()) (va_ttrue ())))

[@ "opaque_to_smt" va_qattr]
let va_qcode_ClmulRev64High (va_mods:va_mods_t) (a:poly) (b:poly) : (va_quickCode unit
val va_qcode_ClmulRev64High (va_mods: va_mods_t) (a b: poly)
    : (va_quickCode unit (va_code_ClmulRev64High ()))
va_mods: Vale.PPC64LE.QuickCode.va_mods_t -> a: Vale.Math.Poly2_s.poly -> b: Vale.Math.Poly2_s.poly
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit
      (Vale.AES.PPC64LE.GF128_Mul.va_code_ClmulRev64High ())