val va_lemma_VSwap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm -> src:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_VSwap dst src) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ (let (a:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 src) in avx_enabled)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 src) in
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_sM dst) == Vale.Math.Poly2.swap a 64) /\
    va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst va_sM
    va_s0)))))
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_xmm va_s0 src) in
  let (va_s3, va_fc3) = va_lemma_VPalignr8 (va_hd va_b1) va_s0 dst src src 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)
val va_lemma_VSwap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm -> src:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_VSwap dst src) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ (let (a:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 src) in avx_enabled)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 src) in
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_sM dst) == Vale.Math.Poly2.swap a 64) /\
    va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst va_sM
    va_s0)))))
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_xmm va_s0 src) in
let va_s3, va_fc3 = va_lemma_VPalignr8 (va_hd va_b1) va_s0 dst src src 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)
Vale.AES.X64.PolyOps.fst.checked
Vale.X64.State.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsVector.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.InsAes.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.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 prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.X64.PolyOps.fst
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Vale.X64.Decls.va_operand_xmm Vale.X64.Decls.va_fuel FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_lemma_merge_total FStar.Pervasives.Native.tuple2 Vale.X64.State.vale_state Vale.X64.Decls.va_lemma_empty_total Prims.unit Vale.Math.Poly2.Bits.lemma_of_to_quad32 Vale.Math.Poly2.swap Vale.Math.Poly2.Words.lemma_quad32_double_swap Prims.list Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_tl Vale.X64.InsVector.va_lemma_VPalignr8 Vale.X64.Decls.va_hd Vale.Math.Poly2_s.poly Vale.Math.Poly2.Bits_s.of_quad32 Vale.X64.Decls.va_eval_xmm Vale.X64.Decls.va_get_block Vale.X64.Decls.va_reveal_opaque Vale.AES.X64.PolyOps.va_code_VSwap
module Vale.AES.X64.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.X64.Machine_s
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsVector
open Vale.X64.InsAes
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.X64.CPU_Features_s
//-- VPolyAdd

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

[@ "opaque_to_smt"]
let va_codegen_success_VPolyAdd dst src1 src2 =
  (va_pbool_and (va_codegen_success_VPxor 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_xmm va_s0 src1) in
  let (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_opr128 va_s0 src2) in
  Vale.Math.Poly2.Words.lemma_add_quad32 (va_eval_xmm va_s0 src1) (va_eval_opr128 va_s0 src2);
  let (va_s5, va_fc5) = va_lemma_VPxor (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_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- PolyAnd

[@ "opaque_to_smt"]
let va_code_PolyAnd dst src =
  (va_Block (va_CCons (va_code_Pand dst (va_coerce_xmm_to_opr128 src)) (va_CNil ())))

[@ "opaque_to_smt"]
let va_codegen_success_PolyAnd dst src =
  (va_pbool_and (va_codegen_success_Pand dst (va_coerce_xmm_to_opr128 src)) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_PolyAnd va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_PolyAnd) (va_code_PolyAnd dst src);
  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_xmm va_s0 dst) in
  let (a2:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 src) in
  Vale.Math.Poly2.Words.lemma_and_quad32 (va_eval_xmm va_s0 dst) (va_eval_xmm va_s0 src);
  let (va_s5, va_fc5) = va_lemma_Pand (va_hd va_b1) va_s0 dst (va_coerce_xmm_to_opr128 src) 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_PolyAnd dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_PolyAnd (va_code_PolyAnd dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- VHigh64ToLow

[@ "opaque_to_smt"]
let va_code_VHigh64ToLow dst src =
  (va_Block (va_CCons (va_code_Vpsrldq8 dst src) (va_CNil ())))

[@ "opaque_to_smt"]
let va_codegen_success_VHigh64ToLow dst src =
  (va_pbool_and (va_codegen_success_Vpsrldq8 dst src) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_VHigh64ToLow va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_VHigh64ToLow) (va_code_VHigh64ToLow 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_xmm va_s0 src) in
  let (va_s3, va_fc3) = va_lemma_Vpsrldq8 (va_hd va_b1) va_s0 dst src in
  let va_b3 = va_tl va_b1 in
  Vale.Math.Poly2.Words.lemma_quad32_double_shift a;
  Vale.Math.Poly2.Lemmas.lemma_shift_is_div a 64;
  Vale.Math.Poly2.Bits.lemma_of_to_quad32 (Vale.Math.Poly2_s.shift 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_VHigh64ToLow dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VHigh64ToLow (va_code_VHigh64ToLow dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- VLow64ToHigh

[@ "opaque_to_smt"]
let va_code_VLow64ToHigh dst src =
  (va_Block (va_CCons (va_code_Vpslldq8 dst src) (va_CNil ())))

[@ "opaque_to_smt"]
let va_codegen_success_VLow64ToHigh dst src =
  (va_pbool_and (va_codegen_success_Vpslldq8 dst src) (va_ttrue ()))

[@"opaque_to_smt"]
let va_lemma_VLow64ToHigh va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_VLow64ToHigh) (va_code_VLow64ToHigh 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_xmm va_s0 src) in
  let (va_s3, va_fc3) = va_lemma_Vpslldq8 (va_hd va_b1) va_s0 dst src in
  let va_b3 = va_tl va_b1 in
  Vale.Math.Poly2.Words.lemma_quad32_double_shift a;
  Vale.Math.Poly2.Lemmas.lemma_mask_is_mod a 64;
  Vale.Math.Poly2.lemma_shift_is_mul (Vale.Math.Poly2.mask a 64) 64;
  Vale.Math.Poly2.Bits.lemma_of_to_quad32 (Vale.Math.Poly2_s.shift (Vale.Math.Poly2.mask a 64) 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_VLow64ToHigh dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_VLow64ToHigh (va_code_VLow64ToHigh dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_flags; va_mod_xmm 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_VPalignr8 dst src src) (va_CNil ())))

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

[@"opaque_to_smt"]
val va_lemma_VSwap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm -> src:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_VSwap dst src) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ (let (a:Vale.Math.Poly2_s.poly) =
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 src) in avx_enabled)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (a:Vale.Math.Poly2_s.poly) = Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_s0 src) in
    Vale.Math.Poly2.Bits_s.of_quad32 (va_eval_xmm va_sM dst) == Vale.Math.Poly2.swap a 64) /\
    va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst va_sM
    va_s0)))))

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    dst: Vale.X64.Decls.va_operand_xmm ->
    src: Vale.X64.Decls.va_operand_xmm
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)