val va_quick_High64ToLow (dst: va_operand_xmm) (a: poly)
    : (va_quickCode unit (va_code_High64ToLow dst))
let va_quick_High64ToLow (dst:va_operand_xmm) (a:poly) : (va_quickCode unit (va_code_High64ToLow
  dst)) =
  (va_QProc (va_code_High64ToLow dst) ([va_Mod_reg64 rR12; va_Mod_flags; va_mod_xmm dst])
    (va_wp_High64ToLow dst a) (va_wpProof_High64ToLow dst a))
val va_quick_High64ToLow (dst: va_operand_xmm) (a: poly)
    : (va_quickCode unit (va_code_High64ToLow dst))
let va_quick_High64ToLow (dst: va_operand_xmm) (a: poly)
    : (va_quickCode unit (va_code_High64ToLow dst)) =
(va_QProc (va_code_High64ToLow dst)
    ([va_Mod_reg64 rR12; va_Mod_flags; va_mod_xmm dst])
    (va_wp_High64ToLow dst a)
    (va_wpProof_High64ToLow dst a))
Vale.AES.X64.GF128_Mul.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.Flags.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 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.X64.GF128_Mul.fst
Vale.X64.Decls.va_operand_xmm Vale.Math.Poly2_s.poly Vale.X64.QuickCode.va_QProc Prims.unit Vale.AES.X64.GF128_Mul.va_code_High64ToLow Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_reg64 Vale.X64.Machine_s.rR12 Vale.X64.QuickCode.va_Mod_flags Vale.X64.QuickCode.va_mod_xmm Prims.Nil Vale.AES.X64.GF128_Mul.va_wp_High64ToLow Vale.AES.X64.GF128_Mul.va_wpProof_High64ToLow Vale.X64.QuickCode.va_quickCode
module Vale.AES.X64.GF128_Mul
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.AES.GF128_s
open Vale.AES.GF128
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
//-- ShiftLeft128_1

[@ "opaque_to_smt" va_qattr]
let va_code_ShiftLeft128_1 () =
  (va_Block (va_CCons (va_code_Mov128 (va_op_xmm_xmm 2) (va_op_xmm_xmm 1)) (va_CCons (va_code_Psrld
    (va_op_xmm_xmm 2) 31) (va_CCons (va_code_Pslld (va_op_xmm_xmm 1) 1) (va_CCons (va_code_VPslldq4
    (va_op_xmm_xmm 2) (va_op_xmm_xmm 2)) (va_CCons (va_code_Pxor (va_op_xmm_xmm 1) (va_op_xmm_xmm
    2)) (va_CNil ())))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_ShiftLeft128_1 () =
  (va_pbool_and (va_codegen_success_Mov128 (va_op_xmm_xmm 2) (va_op_xmm_xmm 1)) (va_pbool_and
    (va_codegen_success_Psrld (va_op_xmm_xmm 2) 31) (va_pbool_and (va_codegen_success_Pslld
    (va_op_xmm_xmm 1) 1) (va_pbool_and (va_codegen_success_VPslldq4 (va_op_xmm_xmm 2)
    (va_op_xmm_xmm 2)) (va_pbool_and (va_codegen_success_Pxor (va_op_xmm_xmm 1) (va_op_xmm_xmm 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 59 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 2) (va_op_xmm_xmm 1)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 60 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Psrld (va_op_xmm_xmm 2) 31) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 61 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pslld (va_op_xmm_xmm 1) 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 62 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_VPslldq4 (va_op_xmm_xmm 2) (va_op_xmm_xmm 2)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 63 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pxor (va_op_xmm_xmm 1) (va_op_xmm_xmm 2)) (fun (va_s:va_state) _ -> let
    (va_arg8:Vale.Math.Poly2_s.poly) = a in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 65 column 23 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.AES.GF128.lemma_shift_left_1 va_arg8) (va_QEmpty (())))))))))

[@"opaque_to_smt"]
let va_lemma_ShiftLeft128_1 va_b0 va_s0 a =
  let (va_mods:va_mods_t) = [va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_flags; 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 45 column 1 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 57 column 39 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_get_xmm 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_xmm 2; va_Mod_xmm 1; va_Mod_flags; 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_xmm 2 va_sM (va_update_xmm 1 va_sM (va_update_flags va_sM
    (va_update_ok va_sM va_s0)))));
  va_lemma_norm_mods ([va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_flags]) 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_Mov128 (va_op_xmm_xmm 3) (va_op_xmm_xmm 1)) (va_CCons (va_code_Psrld
    (va_op_xmm_xmm 3) 31) (va_CCons (va_code_Mov128 (va_op_xmm_xmm 4) (va_op_xmm_xmm 2)) (va_CCons
    (va_code_Psrld (va_op_xmm_xmm 4) 31) (va_CCons (va_code_Pslld (va_op_xmm_xmm 1) 1) (va_CCons
    (va_code_Pslld (va_op_xmm_xmm 2) 1) (va_CCons (va_code_VPslldq4 (va_op_xmm_xmm 5)
    (va_op_xmm_xmm 3)) (va_CCons (va_code_VPslldq4 (va_op_xmm_xmm 4) (va_op_xmm_xmm 4)) (va_CCons
    (va_code_PinsrdImm (va_op_xmm_xmm 3) 0 0 (va_op_reg_opr64_reg64 rR12)) (va_CCons
    (va_code_Pshufd (va_op_xmm_xmm 3) (va_op_xmm_xmm 3) 3) (va_CCons (va_code_Pxor (va_op_xmm_xmm
    3) (va_op_xmm_xmm 4)) (va_CCons (va_code_Pxor (va_op_xmm_xmm 1) (va_op_xmm_xmm 5)) (va_CCons
    (va_code_Pxor (va_op_xmm_xmm 2) (va_op_xmm_xmm 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_Mov128 (va_op_xmm_xmm 3) (va_op_xmm_xmm 1)) (va_pbool_and
    (va_codegen_success_Psrld (va_op_xmm_xmm 3) 31) (va_pbool_and (va_codegen_success_Mov128
    (va_op_xmm_xmm 4) (va_op_xmm_xmm 2)) (va_pbool_and (va_codegen_success_Psrld (va_op_xmm_xmm 4)
    31) (va_pbool_and (va_codegen_success_Pslld (va_op_xmm_xmm 1) 1) (va_pbool_and
    (va_codegen_success_Pslld (va_op_xmm_xmm 2) 1) (va_pbool_and (va_codegen_success_VPslldq4
    (va_op_xmm_xmm 5) (va_op_xmm_xmm 3)) (va_pbool_and (va_codegen_success_VPslldq4 (va_op_xmm_xmm
    4) (va_op_xmm_xmm 4)) (va_pbool_and (va_codegen_success_PinsrdImm (va_op_xmm_xmm 3) 0 0
    (va_op_reg_opr64_reg64 rR12)) (va_pbool_and (va_codegen_success_Pshufd (va_op_xmm_xmm 3)
    (va_op_xmm_xmm 3) 3) (va_pbool_and (va_codegen_success_Pxor (va_op_xmm_xmm 3) (va_op_xmm_xmm
    4)) (va_pbool_and (va_codegen_success_Pxor (va_op_xmm_xmm 1) (va_op_xmm_xmm 5)) (va_pbool_and
    (va_codegen_success_Pxor (va_op_xmm_xmm 2) (va_op_xmm_xmm 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 91 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 3) (va_op_xmm_xmm 1)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 92 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Psrld (va_op_xmm_xmm 3) 31) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 95 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 4) (va_op_xmm_xmm 2)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 96 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Psrld (va_op_xmm_xmm 4) 31) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 100 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pslld (va_op_xmm_xmm 1) 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 101 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pslld (va_op_xmm_xmm 2) 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 105 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_VPslldq4 (va_op_xmm_xmm 5) (va_op_xmm_xmm 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 106 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_VPslldq4 (va_op_xmm_xmm 4) (va_op_xmm_xmm 4)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 109 column 14 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_PinsrdImm (va_op_xmm_xmm 3) 0 0 (va_op_reg_opr64_reg64 rR12)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 110 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pshufd (va_op_xmm_xmm 3) (va_op_xmm_xmm 3) 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 113 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pxor (va_op_xmm_xmm 3) (va_op_xmm_xmm 4)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 117 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pxor (va_op_xmm_xmm 1) (va_op_xmm_xmm 5)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 118 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pxor (va_op_xmm_xmm 2) (va_op_xmm_xmm 3)) (fun (va_s:va_state) _ -> 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 120 column 25 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.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 /\
    avx_enabled /\ sse_enabled /\ Vale.Math.Poly2_s.degree hi < 127 /\ Vale.Math.Poly2_s.degree lo
    <= 127 /\ va_get_xmm 1 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 lo /\ va_get_xmm 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_xmm 1 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mod b n) /\ va_get_xmm 2 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.div b n)) /\ va_state_eq va_sM
    (va_update_xmm 5 va_sM (va_update_xmm 4 va_sM (va_update_xmm 3 va_sM (va_update_xmm 2 va_sM
    (va_update_xmm 1 va_sM (va_update_reg64 rR12 va_sM (va_update_flags 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_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1;
    va_Mod_reg64 rR12; va_Mod_flags; 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 68 column 1 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 81 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (let n = Vale.Math.Poly2_s.monomial 128 in label va_range1
    "***** POSTCONDITION NOT MET AT line 82 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.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 83 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (let b = Vale.Math.Poly2_s.shift a 1 in label va_range1
    "***** POSTCONDITION NOT MET AT line 84 column 37 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_get_xmm 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 85 column 37 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_get_xmm 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_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1;
    va_Mod_reg64 rR12; va_Mod_flags; 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 /\ avx_enabled /\ sse_enabled /\ Vale.Math.Poly2_s.degree hi < 127 /\
    Vale.Math.Poly2_s.degree lo <= 127 /\ va_get_xmm 1 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 lo
    /\ va_get_xmm 2 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 hi /\ (forall
    (va_x_efl:Vale.X64.Flags.t) (va_x_r12:nat64) (va_x_xmm1:quad32) (va_x_xmm2:quad32)
    (va_x_xmm3:quad32) (va_x_xmm4:quad32) (va_x_xmm5:quad32) . let va_sM = va_upd_xmm 5 va_x_xmm5
    (va_upd_xmm 4 va_x_xmm4 (va_upd_xmm 3 va_x_xmm3 (va_upd_xmm 2 va_x_xmm2 (va_upd_xmm 1 va_x_xmm1
    (va_upd_reg64 rR12 va_x_r12 (va_upd_flags va_x_efl 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_xmm 1 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.mod b n) /\ va_get_xmm 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_xmm 5;
    va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_reg64 rR12; va_Mod_flags]) 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_xmm 5 va_sM (va_update_xmm 4 va_sM (va_update_xmm 3 va_sM
    (va_update_xmm 2 va_sM (va_update_xmm 1 va_sM (va_update_reg64 rR12 va_sM (va_update_flags
    va_sM (va_update_ok va_sM va_s0)))))))));
  va_lemma_norm_mods ([va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2; va_Mod_xmm 1;
    va_Mod_reg64 rR12; va_Mod_flags]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_ShiftLeft2_128_1 (lo:poly) (hi:poly) : (va_quickCode unit (va_code_ShiftLeft2_128_1
  ())) =
  (va_QProc (va_code_ShiftLeft2_128_1 ()) ([va_Mod_xmm 5; va_Mod_xmm 4; va_Mod_xmm 3; va_Mod_xmm 2;
    va_Mod_xmm 1; va_Mod_reg64 rR12; va_Mod_flags]) (va_wp_ShiftLeft2_128_1 lo hi)
    (va_wpProof_ShiftLeft2_128_1 lo hi))
//--
//-- ClmulRev64

val va_code_ClmulRev64 : dstHi:bool -> srcHi:bool -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_ClmulRev64 dstHi srcHi =
  (va_Block (va_CCons (va_code_Pclmulqdq (va_op_xmm_xmm 1) (va_op_xmm_xmm 2) dstHi srcHi) (va_CCons
    (va_code_ShiftLeft128_1 ()) (va_CNil ()))))

val va_codegen_success_ClmulRev64 : dstHi:bool -> srcHi:bool -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_ClmulRev64 dstHi srcHi =
  (va_pbool_and (va_codegen_success_Pclmulqdq (va_op_xmm_xmm 1) (va_op_xmm_xmm 2) dstHi srcHi)
    (va_pbool_and (va_codegen_success_ShiftLeft128_1 ()) (va_ttrue ())))

[@ "opaque_to_smt" va_qattr]
let va_qcode_ClmulRev64 (va_mods:va_mods_t) (a:poly) (b:poly) (dstHi:bool) (srcHi:bool) :
  (va_quickCode unit (va_code_ClmulRev64 dstHi srcHi)) =
  (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 138 column 14 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_quick_Pclmulqdq (va_op_xmm_xmm 1) (va_op_xmm_xmm 2) dstHi srcHi) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 139 column 19 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.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_arg6:Vale.Math.Poly2_s.poly) = b in let (va_arg5:Vale.Math.Poly2_s.poly) = a in va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 141 column 30 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (fun (_:unit) -> Vale.Math.Poly2.Lemmas.lemma_mul_reverse_shift_1 va_arg5 va_arg6 63)
    (va_QEmpty (()))))))


val va_lemma_ClmulRev64 : va_b0:va_code -> va_s0:va_state -> a:poly -> b:poly -> dstHi:bool ->
  srcHi:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_ClmulRev64 dstHi srcHi) va_s0 /\ va_get_ok va_s0 /\
    (pclmulqdq_enabled /\ avx_enabled /\ sse_enabled) /\ 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 (if dstHi then Vale.Arch.Types.quad32_double_hi (va_get_xmm
    1 va_s0) else Vale.Arch.Types.quad32_double_lo (va_get_xmm 1 va_s0)) /\
    Vale.Math.Poly2_s.reverse b 63 == Vale.Math.Poly2.Bits_s.of_double32 (if srcHi then
    Vale.Arch.Types.quad32_double_hi (va_get_xmm 2 va_s0) else Vale.Arch.Types.quad32_double_lo
    (va_get_xmm 2 va_s0))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_xmm 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_xmm 2 va_sM (va_update_xmm 1
    va_sM (va_update_flags va_sM (va_update_ok va_sM va_s0))))))
[@"opaque_to_smt"]
let va_lemma_ClmulRev64 va_b0 va_s0 a b dstHi srcHi =
  let (va_mods:va_mods_t) = [va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_flags; va_Mod_ok] in
  let va_qc = va_qcode_ClmulRev64 va_mods a b dstHi srcHi in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_ClmulRev64 dstHi srcHi) va_qc va_s0
    (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 123 column 1 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 136 column 51 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/x64/Vale.AES.X64.GF128_Mul.vaf *****"
    (va_get_xmm 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_xmm 2; va_Mod_xmm 1; va_Mod_flags; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_ClmulRev64 (a:poly) (b:poly) (dstHi:bool) (srcHi:bool) (va_s0:va_state) (va_k:(va_state
  -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (pclmulqdq_enabled /\ avx_enabled /\ sse_enabled) /\ 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 (va_if dstHi (fun _ -> Vale.Arch.Types.quad32_double_hi
    (va_get_xmm 1 va_s0)) (fun _ -> Vale.Arch.Types.quad32_double_lo (va_get_xmm 1 va_s0))) /\
    Vale.Math.Poly2_s.reverse b 63 == Vale.Math.Poly2.Bits_s.of_double32 (va_if srcHi (fun _ ->
    Vale.Arch.Types.quad32_double_hi (va_get_xmm 2 va_s0)) (fun _ ->
    Vale.Arch.Types.quad32_double_lo (va_get_xmm 2 va_s0))) /\ (forall (va_x_efl:Vale.X64.Flags.t)
    (va_x_xmm1:quad32) (va_x_xmm2:quad32) . let va_sM = va_upd_xmm 2 va_x_xmm2 (va_upd_xmm 1
    va_x_xmm1 (va_upd_flags va_x_efl va_s0)) in va_get_ok va_sM /\ va_get_xmm 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_ClmulRev64 : a:poly -> b:poly -> dstHi:bool -> srcHi:bool -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_ClmulRev64 a b dstHi srcHi va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_ClmulRev64 dstHi srcHi) ([va_Mod_xmm
    2; va_Mod_xmm 1; va_Mod_flags]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_ClmulRev64 a b dstHi srcHi va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_ClmulRev64 (va_code_ClmulRev64 dstHi srcHi) va_s0 a b dstHi srcHi in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_xmm 2 va_sM (va_update_xmm 1 va_sM (va_update_flags va_sM
    (va_update_ok va_sM va_s0)))));
  va_lemma_norm_mods ([va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_flags]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_ClmulRev64 (a:poly) (b:poly) (dstHi:bool) (srcHi:bool) : (va_quickCode unit
  (va_code_ClmulRev64 dstHi srcHi)) =
  (va_QProc (va_code_ClmulRev64 dstHi srcHi) ([va_Mod_xmm 2; va_Mod_xmm 1; va_Mod_flags])
    (va_wp_ClmulRev64 a b dstHi srcHi) (va_wpProof_ClmulRev64 a b dstHi srcHi))
//--
//-- High64ToLow

val va_code_High64ToLow : dst:va_operand_xmm -> Tot va_code
[@ "opaque_to_smt"]
let va_code_High64ToLow dst =
  (va_Block (va_CCons (va_code_PinsrdImm dst 0 0 (va_op_reg_opr64_reg64 rR12)) (va_CCons
    (va_code_Pshufd dst dst 14) (va_CNil ()))))

val va_codegen_success_High64ToLow : dst:va_operand_xmm -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_High64ToLow dst =
  (va_pbool_and (va_codegen_success_PinsrdImm dst 0 0 (va_op_reg_opr64_reg64 rR12)) (va_pbool_and
    (va_codegen_success_Pshufd dst dst 14) (va_ttrue ())))


val va_lemma_High64ToLow : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm -> a:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_High64ToLow dst) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_get_ok va_s0 /\ sse_enabled /\ Vale.Math.Poly2_s.degree a <= 127 /\ va_eval_xmm va_s0 dst ==
    Vale.Math.Poly2.Bits_s.to_quad32 a))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_xmm va_sM dst == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.div a
    (Vale.Math.Poly2_s.monomial 64)) /\ va_state_eq va_sM (va_update_reg64 rR12 va_sM
    (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_xmm dst va_sM va_s0))))))
[@"opaque_to_smt"]
let va_lemma_High64ToLow va_b0 va_s0 dst a =
  va_reveal_opaque (`%va_code_High64ToLow) (va_code_High64ToLow dst);
  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_PinsrdImm (va_hd va_b1) va_s0 dst 0 0 (va_op_reg_opr64_reg64 rR12)
    in
  let va_b2 = va_tl va_b1 in
  let (va_s3, va_fc3) = va_lemma_Pshufd (va_hd va_b2) va_s2 dst dst 14 in
  let va_b3 = va_tl va_b2 in
  Vale.Math.Poly2.Words.lemma_quad32_double_shift a;
  let (va_sM, va_f3) = va_lemma_empty_total va_s3 va_b3 in
  let va_f2 = va_lemma_merge_total va_b2 va_s2 va_fc3 va_s3 va_f3 va_sM 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_High64ToLow (dst:va_operand_xmm) (a:poly) (va_s0:va_state) (va_k:(va_state -> unit ->
  Type0)) : Type0 =
  (va_is_dst_xmm dst va_s0 /\ va_get_ok va_s0 /\ sse_enabled /\ Vale.Math.Poly2_s.degree a <= 127
    /\ va_eval_xmm va_s0 dst == Vale.Math.Poly2.Bits_s.to_quad32 a /\ (forall
    (va_x_dst:va_value_xmm) (va_x_efl:Vale.X64.Flags.t) (va_x_r12:nat64) . let va_sM = va_upd_reg64
    rR12 va_x_r12 (va_upd_flags va_x_efl (va_upd_operand_xmm dst va_x_dst va_s0)) in va_get_ok
    va_sM /\ va_eval_xmm va_sM dst == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.div a
    (Vale.Math.Poly2_s.monomial 64)) ==> va_k va_sM (())))


val va_wpProof_High64ToLow : dst:va_operand_xmm -> a: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_High64ToLow dst a va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_High64ToLow dst) ([va_Mod_reg64 rR12;
    va_Mod_flags; va_mod_xmm dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_High64ToLow dst a va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_High64ToLow (va_code_High64ToLow dst) va_s0 dst a in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg64 rR12 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_reg64 rR12; va_Mod_flags; va_mod_xmm dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_High64ToLow (dst:va_operand_xmm) (a:poly) : (va_quickCode unit (va_code_High64ToLow
val va_quick_High64ToLow (dst: va_operand_xmm) (a: poly)
    : (va_quickCode unit (va_code_High64ToLow dst))
dst: Vale.X64.Decls.va_operand_xmm -> a: Vale.Math.Poly2_s.poly
  -> Vale.X64.QuickCode.va_quickCode Prims.unit (Vale.AES.X64.GF128_Mul.va_code_High64ToLow dst)