val va_wpProof_VPolyMulLow : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2: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_VPolyMulLow dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_VPolyMulLow dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_VPolyMulLow dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VPolyMulLow (va_code_VPolyMulLow dst src1 src2) va_s0 dst src1 src2
    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)
val va_wpProof_VPolyMulLow : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2: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_VPolyMulLow dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_VPolyMulLow dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_VPolyMulLow dst src1 src2 va_s0 va_k =
let va_sM, va_f0 = va_lemma_VPolyMulLow (va_code_VPolyMulLow dst src1 src2) va_s0 dst src1 src2 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)
Vale.AES.PPC64LE.PolyOps.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.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.AES.GHash_BE.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.PPC64LE.PolyOps.fst
Vale.PPC64LE.Decls.va_operand_vec_opr Vale.PPC64LE.Decls.va_state Prims.unit Vale.PPC64LE.Decls.va_fuel FStar.Pervasives.Native.Mktuple3 Vale.PPC64LE.QuickCode.va_lemma_norm_mods Prims.Cons Vale.PPC64LE.QuickCode.mod_t Vale.PPC64LE.QuickCode.va_mod_vec_opr Prims.Nil Prims._assert Vale.PPC64LE.Decls.va_state_eq Vale.PPC64LE.Decls.va_update_ok Vale.PPC64LE.Decls.va_update_operand_vec_opr Vale.PPC64LE.Decls.va_lemma_upd_update FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.tuple2 Vale.PPC64LE.Machine_s.state Vale.AES.PPC64LE.PolyOps.va_lemma_VPolyMulLow Vale.AES.PPC64LE.PolyOps.va_code_VPolyMulLow
module Vale.AES.PPC64LE.PolyOps
open Vale.Def.Types_s
open Vale.Arch.Types
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.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.GHash_BE
//-- VPolyAdd

[@ "opaque_to_smt"]
let va_code_VPolyAdd dst src1 src2 =
  (va_Block (va_CCons (va_code_Vxor dst src1 src2) (va_CNil ())))

[@ "opaque_to_smt"]
let va_codegen_success_VPolyAdd dst src1 src2 =
  (va_pbool_and (va_codegen_success_Vxor dst src1 src2) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_VPolyAdd va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_VPolyAdd) (va_code_VPolyAdd dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src1) in
  let (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src2) in
  Vale.Math.Poly2.Words.lemma_add_quad32 (va_eval_vec_opr va_s0 src1) (va_eval_vec_opr va_s0 src2);
  let (va_s5, va_fc5) = va_lemma_Vxor (va_hd va_b1) va_s0 dst src1 src2 in
  let va_b5 = va_tl va_b1 in
  let (va_sM, va_f5) = va_lemma_empty_total va_s5 va_b5 in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc5 va_s5 va_f5 va_sM in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_VPolyAdd dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VPolyAdd (va_code_VPolyAdd dst src1 src2) va_s0 dst src1 src2 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)

//--
//-- VPolyAnd

[@ "opaque_to_smt"]
let va_code_VPolyAnd dst src1 src2 =
  (va_Block (va_CCons (va_code_Vand dst src1 src2) (va_CNil ())))

[@ "opaque_to_smt"]
let va_codegen_success_VPolyAnd dst src1 src2 =
  (va_pbool_and (va_codegen_success_Vand dst src1 src2) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_VPolyAnd va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_VPolyAnd) (va_code_VPolyAnd dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src1) in
  let (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src2) in
  Vale.Math.Poly2.Words.lemma_and_quad32 (va_eval_vec_opr va_s0 src1) (va_eval_vec_opr va_s0 src2);
  let (va_s5, va_fc5) = va_lemma_Vand (va_hd va_b1) va_s0 dst src1 src2 in
  let va_b5 = va_tl va_b1 in
  let (va_sM, va_f5) = va_lemma_empty_total va_s5 va_b5 in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc5 va_s5 va_f5 va_sM in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_VPolyAnd dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VPolyAnd (va_code_VPolyAnd dst src1 src2) va_s0 dst src1 src2 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)

//--
//-- VSwap

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

[@ "opaque_to_smt"]
let va_codegen_success_VSwap dst src =
  (va_pbool_and (va_codegen_success_Vsldoi dst src src 8) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_VSwap va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_VSwap) (va_code_VSwap dst src);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (a:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src) in
  let (va_s3, va_fc3) = va_lemma_Vsldoi (va_hd va_b1) va_s0 dst src src 8 in
  let va_b3 = va_tl va_b1 in
  Vale.Math.Poly2.Words.lemma_quad32_double_swap a;
  Vale.Math.Poly2.Bits.lemma_of_to_quad32 (Vale.Math.Poly2.swap a 64);
  let (va_sM, va_f3) = va_lemma_empty_total va_s3 va_b3 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)


[@"opaque_to_smt"]
let va_wpProof_VSwap dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VSwap (va_code_VSwap dst src) va_s0 dst src 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)

//--
//-- VPolyMul

[@ "opaque_to_smt"]
let va_code_VPolyMul dst src1 src2 =
  (va_Block (va_CCons (va_code_Vpmsumd dst src1 src2) (va_CNil ())))

[@ "opaque_to_smt"]
let va_codegen_success_VPolyMul dst src1 src2 =
  (va_pbool_and (va_codegen_success_Vpmsumd dst src1 src2) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_VPolyMul va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_VPolyMul) (va_code_VPolyMul dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src1) in
  let (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src2) in
  let (va_s4, va_fc4) = va_lemma_Vpmsumd (va_hd va_b1) va_s0 dst src1 src2 in
  let va_b4 = va_tl va_b1 in
  Vale.Math.Poly2.Bits.lemma_quad32_double a1;
  Vale.Math.Poly2.Bits.lemma_quad32_double a2;
  Vale.Math.Poly2.Lemmas.lemma_shift_is_div a1 64;
  Vale.Math.Poly2.Lemmas.lemma_shift_is_div a2 64;
  Vale.Math.Poly2.Lemmas.lemma_mask_is_mod a1 64;
  Vale.Math.Poly2.Lemmas.lemma_mask_is_mod a2 64;
  Vale.Math.Poly2.Bits.lemma_of_to_quad32 (Vale.Math.Poly2_s.add (Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2.mask a1 64) (Vale.Math.Poly2.mask a2 64)) (Vale.Math.Poly2_s.mul
    (Vale.Math.Poly2_s.shift a1 (-64)) (Vale.Math.Poly2_s.shift a2 (-64))));
  let (va_sM, va_f4) = va_lemma_empty_total va_s4 va_b4 in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc4 va_s4 va_f4 va_sM in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_VPolyMul dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VPolyMul (va_code_VPolyMul dst src1 src2) va_s0 dst src1 src2 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)

//--
//-- VPolyMulLow

[@ "opaque_to_smt"]
let va_code_VPolyMulLow dst src1 src2 =
  (va_Block (va_CCons (va_code_VPolyMul dst src1 src2) (va_CNil ())))

[@ "opaque_to_smt"]
let va_codegen_success_VPolyMulLow dst src1 src2 =
  (va_pbool_and (va_codegen_success_VPolyMul dst src1 src2) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_VPolyMulLow va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_VPolyMulLow) (va_code_VPolyMulLow dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (a1:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src1) in
  let (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_vec_opr va_s0 src2) in
  let (va_s4, va_fc4) = va_lemma_VPolyMul (va_hd va_b1) va_s0 dst src1 src2 in
  let va_b4 = va_tl va_b1 in
  Vale.AES.GHash_BE.lemma_add_mul_zero_low (Vale.Math.Poly2.mask a1 64) (Vale.Math.Poly2_s.shift a1
    (-64)) (Vale.Math.Poly2.mask a2 64) (Vale.Math.Poly2_s.shift a2 (-64));
  let (va_sM, va_f4) = va_lemma_empty_total va_s4 va_b4 in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc4 va_s4 va_f4 va_sM in
  (va_sM, va_fM)
val va_wpProof_VPolyMulLow : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2: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_VPolyMulLow dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_VPolyMulLow dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))

    dst: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src1: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src2: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    va_s0: Vale.PPC64LE.Decls.va_state ->
    va_k: (_: Vale.PPC64LE.Decls.va_state -> _: Prims.unit -> Type0)
  -> Prims.Ghost ((Vale.PPC64LE.Decls.va_state * Vale.PPC64LE.Decls.va_fuel) * Prims.unit)