val va_lemma_Load_two_lsb : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Load_two_lsb dst) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_get_ok va_s0 /\ sse_enabled))
  (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.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 2 0 0 0 /\ va_state_eq
    va_sM (va_update_flags va_sM (va_update_reg64 rR11 va_sM (va_update_ok va_sM
    (va_update_operand_xmm dst va_sM va_s0))))))
let va_lemma_Load_two_lsb va_b0 va_s0 dst =
  va_reveal_opaque (`%va_code_Load_two_lsb) (va_code_Load_two_lsb dst);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (va_s3, va_fc3) = va_lemma_ZeroXmm (va_hd va_b1) va_s0 dst in
  let va_b3 = va_tl va_b1 in
  Vale.Arch.Types.lemma_insert_nat64_nat32s (va_eval_xmm va_s3 dst) 2 0;
  assert (Vale.Arch.Types.two_to_nat32 (Vale.Def.Words_s.Mktwo #Vale.Def.Words_s.nat32 2 0) == 2);
  let (va_s6, va_fc6) = va_lemma_PinsrqImm (va_hd va_b3) va_s3 dst 2 0 (va_op_reg_opr64_reg64 rR11)
    in
  let va_b6 = va_tl va_b3 in
  let (va_sM, va_f6) = va_lemma_empty_total va_s6 va_b6 in
  let va_f3 = va_lemma_merge_total va_b3 va_s3 va_fc6 va_s6 va_f6 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)
val va_lemma_Load_two_lsb : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Load_two_lsb dst) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_get_ok va_s0 /\ sse_enabled))
  (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.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 2 0 0 0 /\ va_state_eq
    va_sM (va_update_flags va_sM (va_update_reg64 rR11 va_sM (va_update_ok va_sM
    (va_update_operand_xmm dst va_sM va_s0))))))
let va_lemma_Load_two_lsb va_b0 va_s0 dst =
va_reveal_opaque (`%va_code_Load_two_lsb) (va_code_Load_two_lsb dst);
let va_old_s:va_state = va_s0 in
let va_b1:va_codes = va_get_block va_b0 in
let va_s3, va_fc3 = va_lemma_ZeroXmm (va_hd va_b1) va_s0 dst in
let va_b3 = va_tl va_b1 in
Vale.Arch.Types.lemma_insert_nat64_nat32s (va_eval_xmm va_s3 dst) 2 0;
assert (Vale.Arch.Types.two_to_nat32 (Vale.Def.Words_s.Mktwo #Vale.Def.Words_s.nat32 2 0) == 2);
let va_s6, va_fc6 = va_lemma_PinsrqImm (va_hd va_b3) va_s3 dst 2 0 (va_op_reg_opr64_reg64 rR11) in
let va_b6 = va_tl va_b3 in
let va_sM, va_f6 = va_lemma_empty_total va_s6 va_b6 in
let va_f3 = va_lemma_merge_total va_b3 va_s3 va_fc6 va_s6 va_f6 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)
Vale.AES.X64.AESopt.fst.checked
Vale.X64.State.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.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.Transformers.Transform.fsti.checked Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Math.Poly2.Bits.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.AES.X64.PolyOps.fsti.checked Vale.AES.X64.AESopt2.fsti.checked Vale.AES.X64.AESGCM_expected_code.fsti.checked Vale.AES.GHash.fsti.checked Vale.AES.GF128_s.fsti.checked Vale.AES.GF128.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked Vale.AES.AES_helpers.fsti.checked Vale.AES.AES_common_s.fst.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.X64.AESopt.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.list Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_tl Vale.X64.InsVector.va_lemma_PinsrqImm Vale.X64.Decls.va_hd Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rR11 Prims.unit Prims._assert Prims.eq2 Prims.int Vale.Arch.Types.two_to_nat32 Vale.Def.Words_s.Mktwo Vale.Def.Words_s.nat32 Vale.Arch.Types.lemma_insert_nat64_nat32s Vale.X64.Decls.va_eval_xmm Vale.X64.InsVector.va_lemma_ZeroXmm Vale.X64.Decls.va_get_block Vale.X64.Decls.va_reveal_opaque Vale.AES.X64.AESopt.va_code_Load_two_lsb
module Vale.AES.X64.AESopt
open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Seq
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.AES.AES_s
open Vale.X64.Machine_s
open Vale.X64.Memory
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.AES.AES_helpers
//open Vale.Poly1305.Math    // For lemma_poly_bits64()
open Vale.AES.GCM_helpers
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.Arch.TypesNative
open Vale.X64.CPU_Features_s
open Vale.Math.Poly2_s
open Vale.AES.GF128_s
open Vale.AES.GF128
open Vale.AES.GHash
open Vale.AES.X64.PolyOps
open Vale.AES.X64.AESopt2
open Vale.AES.X64.AESGCM_expected_code
open Vale.Transformers.Transform
open FStar.Mul
let add = Vale.Math.Poly2_s.add
#reset-options "--z3rlimit 30"
//-- finish_aes_encrypt_le


val finish_aes_encrypt_le : alg:algorithm -> input_LE:quad32 -> key:(seq nat32)
  -> Lemma
  (requires (Vale.AES.AES_s.is_aes_key_LE alg key))
  (ensures (Vale.AES.AES_s.aes_encrypt_LE alg key input_LE == Vale.AES.AES_s.eval_cipher alg
    input_LE (Vale.AES.AES_s.key_to_round_keys_LE alg key)))
let finish_aes_encrypt_le alg input_LE key =
  Vale.AES.AES_s.aes_encrypt_LE_reveal ();
  Vale.AES.AES_s.eval_cipher_reveal ();
  ()
//--
//-- Load_two_lsb

[@ "opaque_to_smt"]
let va_code_Load_two_lsb dst =
  (va_Block (va_CCons (va_code_ZeroXmm dst) (va_CCons (va_code_PinsrqImm dst 2 0
    (va_op_reg_opr64_reg64 rR11)) (va_CNil ()))))

[@ "opaque_to_smt"]
let va_codegen_success_Load_two_lsb dst =
  (va_pbool_and (va_codegen_success_ZeroXmm dst) (va_pbool_and (va_codegen_success_PinsrqImm dst 2
    0 (va_op_reg_opr64_reg64 rR11)) (va_ttrue ())))

[@"opaque_to_smt"]
val va_lemma_Load_two_lsb : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Load_two_lsb dst) va_s0 /\ va_is_dst_xmm dst va_s0 /\
    va_get_ok va_s0 /\ sse_enabled))
  (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.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 2 0 0 0 /\ va_state_eq
    va_sM (va_update_flags va_sM (va_update_reg64 rR11 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
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)