val va_lemma_ReduceMulRev128 : va_b0:va_code -> va_s0:va_state -> a:poly -> b:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_ReduceMulRev128 ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree a <= 127 /\ Vale.Math.Poly2_s.degree b <= 127 /\ va_get_vec 1 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse a 127) /\ va_get_vec 2 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse b 127)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse
    (Vale.AES.GF128_s.gf128_mul a b) 127) /\ va_state_eq va_sM (va_update_vec 6 va_sM
    (va_update_vec 5 va_sM (va_update_vec 4 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)))))))))))
let va_lemma_ReduceMulRev128 va_b0 va_s0 a b =
  let (va_mods:va_mods_t) = [va_Mod_vec 6; va_Mod_vec 5; va_Mod_vec 4; 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_ReduceMulRev128 va_mods a b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_ReduceMulRev128 ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 315 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 327 column 55 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.reverse
    (Vale.AES.GF128_s.gf128_mul a b) 127))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 6; va_Mod_vec 5; va_Mod_vec 4; 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)
val va_lemma_ReduceMulRev128 : va_b0:va_code -> va_s0:va_state -> a:poly -> b:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_ReduceMulRev128 ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree a <= 127 /\ Vale.Math.Poly2_s.degree b <= 127 /\ va_get_vec 1 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse a 127) /\ va_get_vec 2 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse b 127)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse
    (Vale.AES.GF128_s.gf128_mul a b) 127) /\ va_state_eq va_sM (va_update_vec 6 va_sM
    (va_update_vec 5 va_sM (va_update_vec 4 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)))))))))))
let va_lemma_ReduceMulRev128 va_b0 va_s0 a b =
let va_mods:va_mods_t =
  [
    va_Mod_vec 6;
    va_Mod_vec 5;
    va_Mod_vec 4;
    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_ReduceMulRev128 va_mods a b in
let va_sM, va_fM, va_g =
  va_wp_sound_code_norm (va_code_ReduceMulRev128 ())
    va_qc
    va_s0
    (fun va_s0 va_sM va_g ->
        let () = va_g in
        label va_range1
          "***** POSTCONDITION NOT MET AT line 315 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 327 column 55 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.reverse (Vale.AES.GF128_s.gf128_mul a
                      b)
                  127)))
in
assert_norm (va_qc.mods == va_mods);
va_lemma_norm_mods ([
      va_Mod_vec 6;
      va_Mod_vec 5;
      va_Mod_vec 4;
      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)
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.Decls.va_code Vale.PPC64LE.Decls.va_state Vale.Math.Poly2_s.poly Vale.PPC64LE.QuickCodes.fuel Prims.unit FStar.Pervasives.Native.Mktuple2 Vale.PPC64LE.Decls.va_fuel Vale.PPC64LE.QuickCode.va_lemma_norm_mods Prims.Cons Vale.PPC64LE.QuickCode.mod_t Vale.PPC64LE.QuickCode.va_Mod_vec Vale.PPC64LE.QuickCode.va_Mod_reg Vale.PPC64LE.QuickCode.va_Mod_ok Prims.Nil FStar.Pervasives.assert_norm Prims.eq2 Prims.list Vale.PPC64LE.QuickCode.__proj__QProc__item__mods Vale.AES.PPC64LE.GF128_Mul.va_code_ReduceMulRev128 FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.tuple3 Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCodes.va_wp_sound_code_norm Prims.l_and Vale.PPC64LE.QuickCodes.label Vale.PPC64LE.QuickCodes.va_range1 Prims.b2t Vale.PPC64LE.Decls.va_get_ok Vale.Def.Types_s.quad32 Vale.PPC64LE.Decls.va_get_vec Vale.Math.Poly2.Bits_s.to_quad32 Vale.Math.Poly2_s.reverse Vale.AES.GF128_s.gf128_mul Vale.PPC64LE.QuickCode.quickCode Vale.AES.PPC64LE.GF128_Mul.va_qcode_ReduceMulRev128
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
  (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_lemma_ClmulRev64High : va_b0:va_code -> va_s0:va_state -> a:poly -> b:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_ClmulRev64High ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree a <= 63 /\ Vale.Math.Poly2_s.degree b <= 63 /\
    Vale.Math.Poly2_s.reverse a 63 == Vale.Math.Poly2.Bits_s.of_double32
    (Vale.Arch.Types.quad32_double_hi (va_get_vec 1 va_s0)) /\ Vale.Math.Poly2_s.reverse b 63 ==
    Vale.Math.Poly2.Bits_s.of_double32 (Vale.Arch.Types.quad32_double_hi (va_get_vec 2 va_s0)) /\
    l_or (Vale.Math.Poly2.Bits_s.of_double32 (Vale.Arch.Types.quad32_double_lo (va_get_vec 1
    va_s0)) == zero) (Vale.Math.Poly2.Bits_s.of_double32 (Vale.Arch.Types.quad32_double_lo
    (va_get_vec 2 va_s0)) == zero)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse
    (Vale.Math.Poly2_s.mul a b) 127) /\ va_state_eq va_sM (va_update_vec 2 va_sM (va_update_vec 1
    va_sM (va_update_ok va_sM va_s0)))))
[@"opaque_to_smt"]
let va_lemma_ClmulRev64High va_b0 va_s0 a b =
  let (va_mods:va_mods_t) = [va_Mod_vec 2; va_Mod_vec 1; va_Mod_ok] in
  let va_qc = va_qcode_ClmulRev64High va_mods a b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_ClmulRev64High ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 101 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 114 column 49 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.reverse
    (Vale.Math.Poly2_s.mul a b) 127))) 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)

[@ va_qattr]
let va_wp_ClmulRev64High (a:poly) (b:poly) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ Vale.Math.Poly2_s.degree a <= 63 /\ Vale.Math.Poly2_s.degree b <= 63 /\
    Vale.Math.Poly2_s.reverse a 63 == Vale.Math.Poly2.Bits_s.of_double32
    (Vale.Arch.Types.quad32_double_hi (va_get_vec 1 va_s0)) /\ Vale.Math.Poly2_s.reverse b 63 ==
    Vale.Math.Poly2.Bits_s.of_double32 (Vale.Arch.Types.quad32_double_hi (va_get_vec 2 va_s0)) /\
    l_or (Vale.Math.Poly2.Bits_s.of_double32 (Vale.Arch.Types.quad32_double_lo (va_get_vec 1
    va_s0)) == zero) (Vale.Math.Poly2.Bits_s.of_double32 (Vale.Arch.Types.quad32_double_lo
    (va_get_vec 2 va_s0)) == zero) /\ (forall (va_x_v1:quad32) (va_x_v2:quad32) . let va_sM =
    va_upd_vec 2 va_x_v2 (va_upd_vec 1 va_x_v1 va_s0) in va_get_ok va_sM /\ va_get_vec 1 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.mul a b) 127)
    ==> va_k va_sM (())))


val va_wpProof_ClmulRev64High : a:poly -> b: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_ClmulRev64High a b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_ClmulRev64High ()) ([va_Mod_vec 2;
    va_Mod_vec 1]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_ClmulRev64High a b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_ClmulRev64High (va_code_ClmulRev64High ()) va_s0 a b 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)

[@ "opaque_to_smt" va_qattr]
let va_quick_ClmulRev64High (a:poly) (b:poly) : (va_quickCode unit (va_code_ClmulRev64High ())) =
  (va_QProc (va_code_ClmulRev64High ()) ([va_Mod_vec 2; va_Mod_vec 1]) (va_wp_ClmulRev64High a b)
    (va_wpProof_ClmulRev64High a b))
//--
//-- High64ToLow

[@ "opaque_to_smt"]
let va_code_High64ToLow dst src =
  (va_Block (va_CCons (va_code_Vsldoi dst (va_op_vec_opr_vec 0) src 8) (va_CNil ())))

[@ "opaque_to_smt"]
let va_codegen_success_High64ToLow dst src =
  (va_pbool_and (va_codegen_success_Vsldoi dst (va_op_vec_opr_vec 0) src 8) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_High64ToLow va_b0 va_s0 dst src a =
  va_reveal_opaque (`%va_code_High64ToLow) (va_code_High64ToLow dst src);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (va_s2, va_fc2) = va_lemma_Vsldoi (va_hd va_b1) va_s0 dst (va_op_vec_opr_vec 0) src 8 in
  let va_b2 = va_tl va_b1 in
  Vale.Math.Poly2.Words.lemma_quad32_double_shift a;
  let (va_sM, va_f2) = va_lemma_empty_total va_s2 va_b2 in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc2 va_s2 va_f2 va_sM in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_High64ToLow dst src a va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_High64ToLow (va_code_High64ToLow dst src) va_s0 dst src a in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_vec_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Low64ToHigh

[@ "opaque_to_smt" va_qattr]
let va_code_Low64ToHigh dst src =
  (va_Block (va_CCons (va_code_Vsldoi dst src (va_op_vec_opr_vec 0) 8) (va_CNil ())))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Low64ToHigh dst src =
  (va_pbool_and (va_codegen_success_Vsldoi dst src (va_op_vec_opr_vec 0) 8) (va_ttrue ()))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Low64ToHigh (va_mods:va_mods_t) (dst:vec_opr) (src:vec_opr) (a:poly) : (va_quickCode
  unit (va_code_Low64ToHigh dst src)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 156 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vsldoi dst src (va_op_vec_opr_vec 0) 8) (fun (va_s:va_state) _ -> let
    (va_arg4:Vale.Math.Poly2_s.poly) = a in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 157 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.Words.lemma_quad32_double_shift va_arg4) (va_QEmpty (())))))

[@"opaque_to_smt"]
let va_lemma_Low64ToHigh va_b0 va_s0 dst src a =
  let (va_mods:va_mods_t) = [va_Mod_ok; va_mod_vec_opr dst] in
  let va_qc = va_qcode_Low64ToHigh va_mods dst src a in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Low64ToHigh dst src) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 144 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 154 column 66 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_eval_vec_opr va_sM dst == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2_s.mod a (Vale.Math.Poly2_s.monomial 64)) (Vale.Math.Poly2_s.monomial 64)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_ok; va_mod_vec_opr dst]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Low64ToHigh dst src a va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Low64ToHigh (va_code_Low64ToHigh dst src) va_s0 dst src a in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_vec_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- AddPoly

val va_code_AddPoly : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Tot va_code
[@ "opaque_to_smt"]
let va_code_AddPoly dst src1 src2 =
  (va_Block (va_CCons (va_code_Vxor dst src1 src2) (va_CNil ())))

val va_codegen_success_AddPoly : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_AddPoly dst src1 src2 =
  (va_pbool_and (va_codegen_success_Vxor dst src1 src2) (va_ttrue ()))


val va_lemma_AddPoly : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr -> a:poly -> b:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AddPoly dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree a <= 127 /\ Vale.Math.Poly2_s.degree b <= 127 /\ va_eval_vec_opr va_s0
    src1 == Vale.Math.Poly2.Bits_s.to_quad32 a /\ va_eval_vec_opr va_s0 src2 ==
    Vale.Math.Poly2.Bits_s.to_quad32 b))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.add a b) /\
    va_state_eq va_sM (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@"opaque_to_smt"]
let va_lemma_AddPoly va_b0 va_s0 dst src1 src2 a b =
  va_reveal_opaque (`%va_code_AddPoly) (va_code_AddPoly dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (va_s2, va_fc2) = va_lemma_Vxor (va_hd va_b1) va_s0 dst src1 src2 in
  let va_b2 = va_tl va_b1 in
  Vale.Math.Poly2.Words.lemma_add128 a b;
  let (va_sM, va_f2) = va_lemma_empty_total va_s2 va_b2 in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc2 va_s2 va_f2 va_sM in
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_AddPoly (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr)
  (a:poly) (b:poly) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ Vale.Math.Poly2_s.degree a <= 127 /\ Vale.Math.Poly2_s.degree b <= 127 /\
    va_eval_vec_opr va_s0 src1 == Vale.Math.Poly2.Bits_s.to_quad32 a /\ va_eval_vec_opr va_s0 src2
    == Vale.Math.Poly2.Bits_s.to_quad32 b /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM =
    va_upd_operand_vec_opr dst va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.add a b) ==> va_k va_sM (())))


val va_wpProof_AddPoly : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> a:poly -> b: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_AddPoly dst src1 src2 a b va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddPoly dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_AddPoly dst src1 src2 a b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_AddPoly (va_code_AddPoly dst src1 src2) va_s0 dst src1 src2 a b in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_vec_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_AddPoly (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr)
  (a:poly) (b:poly) : (va_quickCode unit (va_code_AddPoly dst src1 src2)) =
  (va_QProc (va_code_AddPoly dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_AddPoly dst src1 src2 a
    b) (va_wpProof_AddPoly dst src1 src2 a b))
//--
//-- Clmul128

val va_code_Clmul128 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Clmul128 () =
  (va_Block (va_CCons (va_code_Vspltisw (va_op_vec_opr_vec 0) 0) (va_CCons (va_code_VSwap
    (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 1)) (va_CCons (va_code_High64ToLow (va_op_vec_opr_vec
    4) (va_op_vec_opr_vec 3)) (va_CCons (va_code_Low64ToHigh (va_op_vec_opr_vec 5)
    (va_op_vec_opr_vec 3)) (va_CCons (va_code_VPolyMul (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 3)
    (va_op_vec_opr_vec 2)) (va_CCons (va_code_VPolyMulLow (va_op_vec_opr_vec 4) (va_op_vec_opr_vec
    4) (va_op_vec_opr_vec 2)) (va_CCons (va_code_VPolyMulHigh (va_op_vec_opr_vec 5)
    (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 2)) (va_CCons (va_code_Low64ToHigh (va_op_vec_opr_vec
    1) (va_op_vec_opr_vec 3)) (va_CCons (va_code_High64ToLow (va_op_vec_opr_vec 2)
    (va_op_vec_opr_vec 3)) (va_CCons (va_code_AddPoly (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 4)) (va_CCons (va_code_AddPoly (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 5)
    (va_op_vec_opr_vec 2)) (va_CNil ())))))))))))))

val va_codegen_success_Clmul128 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Clmul128 () =
  (va_pbool_and (va_codegen_success_Vspltisw (va_op_vec_opr_vec 0) 0) (va_pbool_and
    (va_codegen_success_VSwap (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 1)) (va_pbool_and
    (va_codegen_success_High64ToLow (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 3)) (va_pbool_and
    (va_codegen_success_Low64ToHigh (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 3)) (va_pbool_and
    (va_codegen_success_VPolyMul (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 2))
    (va_pbool_and (va_codegen_success_VPolyMulLow (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 4)
    (va_op_vec_opr_vec 2)) (va_pbool_and (va_codegen_success_VPolyMulHigh (va_op_vec_opr_vec 5)
    (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 2)) (va_pbool_and (va_codegen_success_Low64ToHigh
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 3)) (va_pbool_and (va_codegen_success_High64ToLow
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3)) (va_pbool_and (va_codegen_success_AddPoly
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 4)) (va_pbool_and
    (va_codegen_success_AddPoly (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 2))
    (va_ttrue ()))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Clmul128 (va_mods:va_mods_t) (ab:poly) (cd:poly) : (va_quickCode (poly & poly)
  (va_code_Clmul128 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (n:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.monomial 64 in let (a:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2_s.div ab n in let (b:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mod ab n in
    let (c:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.div cd n in let (d:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2_s.mod cd n in let (ac:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mul a c in
    let (ad:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mul a d in let (bc:Vale.Math.Poly2_s.poly)
    = Vale.Math.Poly2_s.mul b c in let (bd:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mul b d in
    let (ab_sw:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.swap ab 64 in let
    (ab_hi:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mod ab n in let
    (ab_lo:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.div ab n) n in let
    (va_arg77:Vale.Math.Poly2_s.poly) = ab in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 202 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_arg77) (let
    (va_arg76:Vale.Math.Poly2_s.poly) = cd in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 203 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_arg76) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 205 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_QBind va_range1
    "***** PRECONDITION NOT MET AT line 206 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_VSwap (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 1)) (fun (va_s:va_state) _ -> let
    (va_arg75:Vale.Math.Poly2_s.poly) = ab in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 207 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.Bits.lemma_of_to_quad32 va_arg75) (let
    (va_arg74:Vale.Math.Poly2_s.poly) = ab in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 208 column 29 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Words.lemma_quad32_double_swap va_arg74) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 209 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 ab_sw) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 210 column 16 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_High64ToLow (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 3) ab_sw) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 211 column 16 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Low64ToHigh (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 3) ab_sw) (fun (va_s:va_state) _
    -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 212 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_vec 4 va_s == Vale.Math.Poly2.Bits_s.to_quad32 ab_hi) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 213 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_vec 5 va_s == Vale.Math.Poly2.Bits_s.to_quad32 ab_lo) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 215 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_VPolyMul (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 2)) (fun
    (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 217 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.Bits.lemma_of_to_quad32 ab_hi) (let
    (va_arg73:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.div ab_hi n in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 218 column 26 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_degree_negative va_arg73) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 219 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 ab_hi 64) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 220 column 16 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_VPolyMulLow (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 2)) (fun
    (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 222 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.Bits.lemma_of_to_quad32 ab_lo) (let
    (va_arg72:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.div ab n in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 223 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.Lemmas.lemma_div_mod_exact va_arg72 n) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 224 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 ab_lo 64) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 225 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 5) (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 2)) (fun
    (va_s:va_state) _ -> let (va_arg71:Vale.Math.Poly2_s.poly) = cd in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 227 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.Bits.lemma_of_to_quad32 va_arg71) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 228 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 ab_sw 64) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 229 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 ab_sw 64) (let
    (va_arg70:Vale.Math.Poly2_s.poly) = cd in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 230 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_arg70 64) (let
    (va_arg69:Vale.Math.Poly2_s.poly) = cd in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 231 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_arg69 64) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 232 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 3 va_s) == Vale.Math.Poly2_s.add ad bc) (va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 234 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 ab_hi 64) (let
    (va_arg68:Vale.Math.Poly2_s.poly) = ab in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 235 column 18 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_mod_mod va_arg68 n) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 236 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 4 va_s) == bd) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 238 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 ab_lo 64) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 239 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2.Bits_s.of_quad32 (va_get_vec 5 va_s) == ac) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 241 column 16 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Low64ToHigh (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 3) (Vale.Math.Poly2_s.add ad
    bc)) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 242 column 25 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_mod_distribute ad bc n) (let
    (va_arg67:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mod bc n in let
    (va_arg66:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mod ad n in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 243 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_distribute_left va_arg66 va_arg67 n)
    (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 244 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_vec 1 va_s == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.add
    (Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.mod ad n) n) (Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2_s.mod bc n) n))) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 246 column 16 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_High64ToLow (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3) (Vale.Math.Poly2_s.add ad
    bc)) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 247 column 25 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.AES.GHash_BE.lemma_div_distribute ad bc n) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 248 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_get_vec 2 va_s == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.add
    (Vale.Math.Poly2_s.div ad n) (Vale.Math.Poly2_s.div bc n))) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 250 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_AddPoly (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 4)
    (Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.mod ad n) n)
    (Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.mod bc n) n)) bd) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 251 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_AddPoly (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 2) ac
    (Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.div ad n) (Vale.Math.Poly2_s.div bc n))) (fun
    (va_s:va_state) _ -> let (va_arg65:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.div bc n in let
    (va_arg64:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.div ad n in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 253 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.lemma_add_commute va_arg64 va_arg65) (let
    (va_arg63:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.div ad n in let
    (va_arg62:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.div bc n in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 254 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.lemma_add_associate ac va_arg62 va_arg63) (let (hi:poly) =
    Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.add ac (Vale.Math.Poly2_s.div bc n))
    (Vale.Math.Poly2_s.div ad n) in let (va_arg61:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2_s.mod bc n) n in let (va_arg60:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2_s.mod ad n) n in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 256 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.lemma_add_commute va_arg60 va_arg61) (let (lo:poly) =
    Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.mod bc
    n) n) (Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.mod ad n) n)) bd in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 259 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_gf128_mul a b c d 64) (va_QEmpty ((lo,
    hi))))))))))))))))))))))))))))))))))))))))))))))))


val va_lemma_Clmul128 : va_b0:va_code -> va_s0:va_state -> ab:poly -> cd:poly
  -> Ghost (va_state & va_fuel & poly & poly)
  (requires (va_require_total va_b0 (va_code_Clmul128 ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree ab <= 127 /\ Vale.Math.Poly2_s.degree cd <= 127 /\ va_get_vec 1 va_s0
    == Vale.Math.Poly2.Bits_s.to_quad32 ab /\ va_get_vec 2 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 cd))
  (ensures (fun (va_sM, va_fM, lo, hi) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok
    va_sM /\ Vale.Math.Poly2_s.degree lo <= 127 /\ Vale.Math.Poly2_s.degree hi < 127 /\
    Vale.Math.Poly2_s.mul ab cd == Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.shift hi 128) lo /\
    va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 lo /\ va_get_vec 2 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 hi /\ va_state_eq va_sM (va_update_vec 5 va_sM (va_update_vec
    4 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_ok va_sM va_s0)))))))))
[@"opaque_to_smt"]
let va_lemma_Clmul128 va_b0 va_s0 ab cd =
  let (va_mods:va_mods_t) = [va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec 3; va_Mod_vec 2; va_Mod_vec 1;
    va_Mod_vec 0; va_Mod_ok] in
  let va_qc = va_qcode_Clmul128 va_mods ab cd in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Clmul128 ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let (lo, hi) = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 174 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 184 column 26 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2_s.degree lo <= 127) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 185 column 25 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2_s.degree hi < 127) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 186 column 47 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2_s.mul ab cd == Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.shift hi 128) lo) /\
    label va_range1
    "***** POSTCONDITION NOT MET AT line 187 column 28 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 lo) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 188 column 28 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 hi)) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec 3; va_Mod_vec 2; va_Mod_vec 1;
    va_Mod_vec 0; va_Mod_ok]) va_sM va_s0;
  let (lo, hi) = va_g in
  (va_sM, va_fM, lo, hi)

[@ va_qattr]
let va_wp_Clmul128 (ab:poly) (cd:poly) (va_s0:va_state) (va_k:(va_state -> (poly & poly) -> Type0))
  : Type0 =
  (va_get_ok va_s0 /\ Vale.Math.Poly2_s.degree ab <= 127 /\ Vale.Math.Poly2_s.degree cd <= 127 /\
    va_get_vec 1 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 ab /\ va_get_vec 2 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 cd /\ (forall (va_x_v0:quad32) (va_x_v1:quad32)
    (va_x_v2:quad32) (va_x_v3:quad32) (va_x_v4:quad32) (va_x_v5:quad32) (lo:poly) (hi:poly) . let
    va_sM = va_upd_vec 5 va_x_v5 (va_upd_vec 4 va_x_v4 (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_s0))))) in va_get_ok va_sM /\
    Vale.Math.Poly2_s.degree lo <= 127 /\ Vale.Math.Poly2_s.degree hi < 127 /\
    Vale.Math.Poly2_s.mul ab cd == Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.shift hi 128) lo /\
    va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 lo /\ va_get_vec 2 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 hi ==> va_k va_sM ((lo, hi))))


val va_wpProof_Clmul128 : ab:poly -> cd:poly -> va_s0:va_state -> va_k:(va_state -> (poly & poly)
  -> Type0)
  -> Ghost (va_state & va_fuel & (poly & poly))
  (requires (va_t_require va_s0 /\ va_wp_Clmul128 ab cd va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Clmul128 ()) ([va_Mod_vec 5;
    va_Mod_vec 4; va_Mod_vec 3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0]) va_s0 va_k ((va_sM,
    va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Clmul128 ab cd va_s0 va_k =
  let (va_sM, va_f0, lo, hi) = va_lemma_Clmul128 (va_code_Clmul128 ()) va_s0 ab cd in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 5 va_sM (va_update_vec 4 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_ok va_sM
    va_s0))))))));
  va_lemma_norm_mods ([va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec 3; va_Mod_vec 2; va_Mod_vec 1;
    va_Mod_vec 0]) va_sM va_s0;
  let va_g = (lo, hi) in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Clmul128 (ab:poly) (cd:poly) : (va_quickCode (poly & poly) (va_code_Clmul128 ())) =
  (va_QProc (va_code_Clmul128 ()) ([va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec 3; va_Mod_vec 2;
    va_Mod_vec 1; va_Mod_vec 0]) (va_wp_Clmul128 ab cd) (va_wpProof_Clmul128 ab cd))
//--
//-- ClmulRev128

val va_code_ClmulRev128 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_ClmulRev128 () =
  (va_Block (va_CCons (va_code_Clmul128 ()) (va_CCons (va_code_ShiftLeft2_128_1 ()) (va_CNil ()))))

val va_codegen_success_ClmulRev128 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_ClmulRev128 () =
  (va_pbool_and (va_codegen_success_Clmul128 ()) (va_pbool_and (va_codegen_success_ShiftLeft2_128_1
    ()) (va_ttrue ())))

[@ "opaque_to_smt" va_qattr]
let va_qcode_ClmulRev128 (va_mods:va_mods_t) (ab:poly) (cd:poly) : (va_quickCode (poly & poly)
  (va_code_ClmulRev128 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 279 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Clmul128 (Vale.Math.Poly2_s.reverse ab 127) (Vale.Math.Poly2_s.reverse cd 127)) (fun
    (va_s:va_state) va_g -> let (lo, hi) = va_g in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 280 column 21 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_ShiftLeft2_128_1 lo hi) (fun (va_s:va_state) _ -> let (m:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2_s.shift (Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.shift hi 128) lo) 1 in let
    (va_arg13:Vale.Math.Poly2_s.poly) = lo in let (va_arg12:Vale.Math.Poly2_s.poly) = hi in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 283 column 25 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_combine_define va_arg12 va_arg13 128) (va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 284 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_split_define m 128) (let (lo:poly) =
    Vale.Math.Poly2_s.mod m (Vale.Math.Poly2_s.monomial 128) in let (hi:poly) =
    Vale.Math.Poly2_s.div m (Vale.Math.Poly2_s.monomial 128) in let
    (va_arg11:Vale.Math.Poly2_s.poly) = cd in let (va_arg10:Vale.Math.Poly2_s.poly) = ab in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 287 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_arg10 va_arg11 127)
    (va_QEmpty ((lo, hi)))))))))


val va_lemma_ClmulRev128 : va_b0:va_code -> va_s0:va_state -> ab:poly -> cd:poly
  -> Ghost (va_state & va_fuel & poly & poly)
  (requires (va_require_total va_b0 (va_code_ClmulRev128 ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree ab <= 127 /\ Vale.Math.Poly2_s.degree cd <= 127 /\ va_get_vec 1 va_s0
    == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse ab 127) /\ va_get_vec 2 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse cd 127)))
  (ensures (fun (va_sM, va_fM, lo, hi) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok
    va_sM /\ Vale.Math.Poly2_s.degree lo <= 127 /\ Vale.Math.Poly2_s.degree hi <= 127 /\
    Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.mul ab cd) 255 == Vale.Math.Poly2_s.add
    (Vale.Math.Poly2_s.shift hi 128) lo /\ va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32
    lo /\ va_get_vec 2 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 hi /\ va_state_eq va_sM
    (va_update_vec 5 va_sM (va_update_vec 4 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_ClmulRev128 va_b0 va_s0 ab cd =
  let (va_mods:va_mods_t) = [va_Mod_vec 5; va_Mod_vec 4; 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_ClmulRev128 va_mods ab cd in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_ClmulRev128 ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let (lo, hi) = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 262 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 273 column 26 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2_s.degree lo <= 127) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 274 column 26 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2_s.degree hi <= 127) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 275 column 61 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.mul ab cd) 255 == Vale.Math.Poly2_s.add
    (Vale.Math.Poly2_s.shift hi 128) lo) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 276 column 28 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 lo) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 277 column 28 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 hi)) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 5; va_Mod_vec 4; 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;
  let (lo, hi) = va_g in
  (va_sM, va_fM, lo, hi)

[@ va_qattr]
let va_wp_ClmulRev128 (ab:poly) (cd:poly) (va_s0:va_state) (va_k:(va_state -> (poly & poly) ->
  Type0)) : Type0 =
  (va_get_ok va_s0 /\ Vale.Math.Poly2_s.degree ab <= 127 /\ Vale.Math.Poly2_s.degree cd <= 127 /\
    va_get_vec 1 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse ab 127) /\
    va_get_vec 2 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse cd 127) /\
    (forall (va_x_r10:nat64) (va_x_v0:quad32) (va_x_v1:quad32) (va_x_v2:quad32) (va_x_v3:quad32)
    (va_x_v4:quad32) (va_x_v5:quad32) (lo:poly) (hi:poly) . let va_sM = va_upd_vec 5 va_x_v5
    (va_upd_vec 4 va_x_v4 (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 /\
    Vale.Math.Poly2_s.degree lo <= 127 /\ Vale.Math.Poly2_s.degree hi <= 127 /\
    Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.mul ab cd) 255 == Vale.Math.Poly2_s.add
    (Vale.Math.Poly2_s.shift hi 128) lo /\ va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32
    lo /\ va_get_vec 2 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 hi ==> va_k va_sM ((lo, hi))))


val va_wpProof_ClmulRev128 : ab:poly -> cd:poly -> va_s0:va_state -> va_k:(va_state -> (poly &
  poly) -> Type0)
  -> Ghost (va_state & va_fuel & (poly & poly))
  (requires (va_t_require va_s0 /\ va_wp_ClmulRev128 ab cd va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_ClmulRev128 ()) ([va_Mod_vec 5;
    va_Mod_vec 4; 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_ClmulRev128 ab cd va_s0 va_k =
  let (va_sM, va_f0, lo, hi) = va_lemma_ClmulRev128 (va_code_ClmulRev128 ()) va_s0 ab cd in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 5 va_sM (va_update_vec 4 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 5; va_Mod_vec 4; 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 = (lo, hi) in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_ClmulRev128 (ab:poly) (cd:poly) : (va_quickCode (poly & poly) (va_code_ClmulRev128
  ())) =
  (va_QProc (va_code_ClmulRev128 ()) ([va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec 3; va_Mod_vec 2;
    va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 10]) (va_wp_ClmulRev128 ab cd) (va_wpProof_ClmulRev128
    ab cd))
//--
//-- Gf128ModulusRev

val va_code_Gf128ModulusRev : dst:va_operand_vec_opr -> Tot va_code
[@ "opaque_to_smt"]
let va_code_Gf128ModulusRev dst =
  (va_Block (va_CCons (va_code_Vxor dst dst dst) (va_CCons (va_code_LoadImmShl64 (va_op_reg_opr_reg
    10) (-7936)) (va_CCons (va_code_Mtvsrws (va_op_vec_opr_vec 3) (va_op_reg_opr_reg 10)) (va_CCons
    (va_code_Vsldoi dst (va_op_vec_opr_vec 3) dst 12) (va_CNil ()))))))

val va_codegen_success_Gf128ModulusRev : dst:va_operand_vec_opr -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_Gf128ModulusRev dst =
  (va_pbool_and (va_codegen_success_Vxor dst dst dst) (va_pbool_and
    (va_codegen_success_LoadImmShl64 (va_op_reg_opr_reg 10) (-7936)) (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_Vsldoi dst (va_op_vec_opr_vec 3) dst 12) (va_ttrue ())))))


val va_lemma_Gf128ModulusRev : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Gf128ModulusRev dst) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_get_ok va_s0 /\ dst =!= 3))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse
    gf128_modulus_low_terms 127) /\ Vale.Math.Poly2.Bits_s.of_double32
    (Vale.Arch.Types.quad32_double_lo (va_eval_vec_opr va_sM dst)) == zero /\ va_state_eq va_sM
    (va_update_vec 3 va_sM (va_update_reg 10 va_sM (va_update_ok va_sM (va_update_operand_vec_opr
    dst va_sM va_s0))))))
[@"opaque_to_smt"]
let va_lemma_Gf128ModulusRev va_b0 va_s0 dst =
  va_reveal_opaque (`%va_code_Gf128ModulusRev) (va_code_Gf128ModulusRev dst);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  Vale.AES.GF128.lemma_gf128_constant_rev (va_eval_vec_opr va_s0 dst);
  let (va_s3, va_fc3) = va_lemma_Vxor (va_hd va_b1) va_s0 dst dst dst in
  let va_b3 = va_tl va_b1 in
  let (va_s4, va_fc4) = va_lemma_LoadImmShl64 (va_hd va_b3) va_s3 (va_op_reg_opr_reg 10) (-7936) in
  let va_b4 = va_tl va_b3 in
  Vale.AES.Types_helpers.lemma_ishl_64 ((-7936) `op_Modulus` pow2_64) 16;
  let (va_s6, va_fc6) = va_lemma_Mtvsrws (va_hd va_b4) va_s4 (va_op_vec_opr_vec 3)
    (va_op_reg_opr_reg 10) in
  let va_b6 = va_tl va_b4 in
  let (va_s7, va_fc7) = va_lemma_Vsldoi (va_hd va_b6) va_s6 dst (va_op_vec_opr_vec 3) dst 12 in
  let va_b7 = va_tl va_b6 in
  Vale.Math.Poly2.Lemmas.lemma_split_define (Vale.Math.Poly2_s.reverse gf128_modulus_low_terms 127)
    64;
  Vale.Math.Poly2.Lemmas.lemma_index_all ();
  Vale.Math.Poly2.Lemmas.lemma_reverse_define_all ();
  Vale.Math.Poly2.lemma_equal (Vale.Math.Poly2_s.mod (Vale.Math.Poly2_s.reverse
    gf128_modulus_low_terms 127) (Vale.Math.Poly2_s.monomial 64)) zero;
  Vale.Math.Poly2.Bits.lemma_quad32_double (Vale.Math.Poly2_s.reverse gf128_modulus_low_terms 127);
  let (va_sM, va_f7) = va_lemma_empty_total va_s7 va_b7 in
  let va_f6 = va_lemma_merge_total va_b6 va_s6 va_fc7 va_s7 va_f7 va_sM in
  let va_f4 = va_lemma_merge_total va_b4 va_s4 va_fc6 va_s6 va_f6 va_sM in
  let va_f3 = va_lemma_merge_total va_b3 va_s3 va_fc4 va_s4 va_f4 va_sM in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc3 va_s3 va_f3 va_sM in
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Gf128ModulusRev (dst:va_operand_vec_opr) (va_s0:va_state) (va_k:(va_state -> unit ->
  Type0)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_get_ok va_s0 /\ dst =!= 3 /\ (forall
    (va_x_dst:va_value_vec_opr) (va_x_r10:nat64) (va_x_v3:quad32) . let va_sM = va_upd_vec 3
    va_x_v3 (va_upd_reg 10 va_x_r10 (va_upd_operand_vec_opr dst va_x_dst va_s0)) in va_get_ok va_sM
    /\ va_eval_vec_opr va_sM dst == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse
    gf128_modulus_low_terms 127) /\ Vale.Math.Poly2.Bits_s.of_double32
    (Vale.Arch.Types.quad32_double_lo (va_eval_vec_opr va_sM dst)) == zero ==> va_k va_sM (())))


val va_wpProof_Gf128ModulusRev : dst:va_operand_vec_opr -> va_s0:va_state -> va_k:(va_state -> unit
  -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Gf128ModulusRev dst va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Gf128ModulusRev dst) ([va_Mod_vec 3;
    va_Mod_reg 10; va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Gf128ModulusRev dst va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Gf128ModulusRev (va_code_Gf128ModulusRev dst) va_s0 dst in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 3 va_sM (va_update_reg 10 va_sM (va_update_ok va_sM
    (va_update_operand_vec_opr dst va_sM va_s0)))));
  va_lemma_norm_mods ([va_Mod_vec 3; va_Mod_reg 10; va_mod_vec_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Gf128ModulusRev (dst:va_operand_vec_opr) : (va_quickCode unit (va_code_Gf128ModulusRev
  dst)) =
  (va_QProc (va_code_Gf128ModulusRev dst) ([va_Mod_vec 3; va_Mod_reg 10; va_mod_vec_opr dst])
    (va_wp_Gf128ModulusRev dst) (va_wpProof_Gf128ModulusRev dst))
//--
//-- ReduceMulRev128

[@ "opaque_to_smt" va_qattr]
let va_code_ReduceMulRev128 () =
  (va_Block (va_CCons (va_code_ClmulRev128 ()) (va_CCons (va_code_Vmr (va_op_vec_opr_vec 6)
    (va_op_vec_opr_vec 2)) (va_CCons (va_code_Gf128ModulusRev (va_op_vec_opr_vec 2)) (va_CCons
    (va_code_ClmulRev128 ()) (va_CCons (va_code_Vmr (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 2))
    (va_CCons (va_code_Gf128ModulusRev (va_op_vec_opr_vec 2)) (va_CCons (va_code_ClmulRev64High ())
    (va_CCons (va_code_AddPoly (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 5))
    (va_CCons (va_code_AddPoly (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 6))
    (va_CNil ())))))))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_ReduceMulRev128 () =
  (va_pbool_and (va_codegen_success_ClmulRev128 ()) (va_pbool_and (va_codegen_success_Vmr
    (va_op_vec_opr_vec 6) (va_op_vec_opr_vec 2)) (va_pbool_and (va_codegen_success_Gf128ModulusRev
    (va_op_vec_opr_vec 2)) (va_pbool_and (va_codegen_success_ClmulRev128 ()) (va_pbool_and
    (va_codegen_success_Vmr (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 2)) (va_pbool_and
    (va_codegen_success_Gf128ModulusRev (va_op_vec_opr_vec 2)) (va_pbool_and
    (va_codegen_success_ClmulRev64High ()) (va_pbool_and (va_codegen_success_AddPoly
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 5)) (va_pbool_and
    (va_codegen_success_AddPoly (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 6))
    (va_ttrue ()))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_ReduceMulRev128 (va_mods:va_mods_t) (a:poly) (b:poly) : (va_quickCode unit
  (va_code_ReduceMulRev128 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 329 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_gf128_degree ()) (let (va_arg31:Vale.Math.Poly2_s.poly) =
    b in let (va_arg30:Vale.Math.Poly2_s.poly) = a in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 330 column 27 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_gf128_reduce_rev va_arg30 va_arg31
    gf128_modulus_low_terms 128) (let (m:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.monomial 128
    in let (h:Vale.Math.Poly2_s.poly) = gf128_modulus_low_terms in let (ab:Vale.Math.Poly2_s.poly)
    = Vale.Math.Poly2_s.mul a b in let (rh:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.reverse h
    127 in let (rab:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.reverse ab 255 in let
    (rd:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mod rab m in let (rdh:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.mul (Vale.Math.Poly2_s.reverse rd 127) h) 255 in
    let (rdhL:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.mod rdh m in let
    (rdhLh:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2_s.reverse (Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2_s.reverse rdhL 127) h) 127 in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 341 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_ClmulRev128 a b) (fun (va_s:va_state) va_g -> let ((lo1:poly), (hi1:poly)) = va_g in
    let (va_arg29:Vale.Math.Poly2_s.poly) = lo1 in let (va_arg28:Vale.Math.Poly2_s.poly) = hi1 in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 342 column 25 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_combine_define va_arg28 va_arg29 128) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 343 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vmr (va_op_vec_opr_vec 6) (va_op_vec_opr_vec 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 345 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Gf128ModulusRev (va_op_vec_opr_vec 2)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 346 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_ClmulRev128 (Vale.Math.Poly2_s.reverse rd 127) h) (fun (va_s:va_state) va_g -> let
    ((lo2:poly), (hi2:poly)) = va_g in let (va_arg27:Vale.Math.Poly2_s.poly) = lo2 in let
    (va_arg26:Vale.Math.Poly2_s.poly) = hi2 in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 347 column 25 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_combine_define va_arg26 va_arg27 128) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 348 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Vmr (va_op_vec_opr_vec 5) (va_op_vec_opr_vec 2)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 350 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_Gf128ModulusRev (va_op_vec_opr_vec 2)) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 352 column 31 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_quad32_double_hi_rev rdhL) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 353 column 31 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_quad32_double_hi_rev rh) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 354 column 19 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_ClmulRev64High (Vale.Math.Poly2_s.reverse rdhL 127) h) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 356 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_AddPoly (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 5) rdhLh
    (Vale.Math.Poly2_s.div rdh m)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 357 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GF128_Mul.vaf *****"
    (va_quick_AddPoly (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 6)
    (Vale.Math.Poly2_s.add rdhLh (Vale.Math.Poly2_s.div rdh m)) (Vale.Math.Poly2_s.div rab m))
    (va_QEmpty (()))))))))))))))))))
val va_lemma_ReduceMulRev128 : va_b0:va_code -> va_s0:va_state -> a:poly -> b:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_ReduceMulRev128 ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree a <= 127 /\ Vale.Math.Poly2_s.degree b <= 127 /\ va_get_vec 1 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse a 127) /\ va_get_vec 2 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse b 127)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.reverse
    (Vale.AES.GF128_s.gf128_mul a b) 127) /\ va_state_eq va_sM (va_update_vec 6 va_sM
    (va_update_vec 5 va_sM (va_update_vec 4 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_b0: Vale.PPC64LE.Decls.va_code ->
    va_s0: Vale.PPC64LE.Decls.va_state ->
    a: Vale.Math.Poly2_s.poly ->
    b: Vale.Math.Poly2_s.poly
  -> Prims.Ghost (Vale.PPC64LE.Decls.va_state * Vale.PPC64LE.Decls.va_fuel)