val va_quick_Aes_2rounds_4way
      (alg: algorithm)
      (n: pos)
      (init1 init2 init3 init4: quad32)
      (round_keys: (seq quad32))
    : (va_quickCode unit (va_code_Aes_2rounds_4way ()))
let va_quick_Aes_2rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
  (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit (va_code_Aes_2rounds_4way ())) =
  (va_QProc (va_code_Aes_2rounds_4way ()) ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm
    12; va_Mod_xmm 2]) (va_wp_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys)
    (va_wpProof_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys))
val va_quick_Aes_2rounds_4way
      (alg: algorithm)
      (n: pos)
      (init1 init2 init3 init4: quad32)
      (round_keys: (seq quad32))
    : (va_quickCode unit (va_code_Aes_2rounds_4way ()))
let va_quick_Aes_2rounds_4way
      (alg: algorithm)
      (n: pos)
      (init1 init2 init3 init4: quad32)
      (round_keys: (seq quad32))
    : (va_quickCode unit (va_code_Aes_2rounds_4way ())) =
(va_QProc (va_code_Aes_2rounds_4way ())
    ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2])
    (va_wp_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys)
    (va_wpProof_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys))
Vale.AES.X64.AESCTR.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.Poly1305.Math.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.GHash.fsti.checked Vale.AES.GHash.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
Vale.AES.X64.AESCTR.fst
Vale.AES.AES_common_s.algorithm Prims.pos Vale.X64.Decls.quad32 FStar.Seq.Base.seq Vale.X64.QuickCode.va_QProc Prims.unit Vale.AES.X64.AESCTR.va_code_Aes_2rounds_4way Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_flags Vale.X64.QuickCode.va_Mod_xmm Prims.Nil Vale.AES.X64.AESCTR.va_wp_Aes_2rounds_4way Vale.AES.X64.AESCTR.va_wpProof_Aes_2rounds_4way Vale.X64.QuickCode.va_quickCode
module Vale.AES.X64.AESCTR
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.AES.X64.GHash
open Vale.AES.GHash
open Vale.X64.CPU_Features_s
//-- 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 ();
  ()
//--
//-- Aes_round_4way

val va_code_Aes_round_4way : round_key:va_operand_xmm -> Tot va_code
[@ "opaque_to_smt"]
let va_code_Aes_round_4way round_key =
  (va_Block (va_CCons (va_code_AESNI_enc (va_op_xmm_xmm 2) round_key) (va_CCons (va_code_AESNI_enc
    (va_op_xmm_xmm 12) round_key) (va_CCons (va_code_AESNI_enc (va_op_xmm_xmm 13) round_key)
    (va_CCons (va_code_AESNI_enc (va_op_xmm_xmm 14) round_key) (va_CNil ()))))))

val va_codegen_success_Aes_round_4way : round_key:va_operand_xmm -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_Aes_round_4way round_key =
  (va_pbool_and (va_codegen_success_AESNI_enc (va_op_xmm_xmm 2) round_key) (va_pbool_and
    (va_codegen_success_AESNI_enc (va_op_xmm_xmm 12) round_key) (va_pbool_and
    (va_codegen_success_AESNI_enc (va_op_xmm_xmm 13) round_key) (va_pbool_and
    (va_codegen_success_AESNI_enc (va_op_xmm_xmm 14) round_key) (va_ttrue ())))))


val va_lemma_Aes_round_4way : va_b0:va_code -> va_s0:va_state -> alg:algorithm -> n:pos ->
  round_key:va_operand_xmm -> init1:quad32 -> init2:quad32 -> init3:quad32 -> init4:quad32 ->
  round_keys:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Aes_round_4way round_key) va_s0 /\ va_is_src_xmm
    round_key va_s0 /\ va_get_ok va_s0 /\ (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr
    alg /\ Vale.AES.AES_common_s.nr alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm
    2 va_s0 == Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_eval_xmm va_s0 round_key ==
    FStar.Seq.Base.index #quad32 round_keys n /\ 2 =!= round_key /\ 12 =!= round_key /\ 13 =!=
    round_key /\ 14 =!= round_key)))
  (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 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys n /\ va_get_xmm 12 va_sM ==
    Vale.AES.AES_s.eval_rounds init2 round_keys n /\ va_get_xmm 13 va_sM ==
    Vale.AES.AES_s.eval_rounds init3 round_keys n /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys n) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM (va_update_xmm 12 va_sM (va_update_xmm 2 va_sM
    (va_update_ok va_sM va_s0))))))))
[@"opaque_to_smt"]
let va_lemma_Aes_round_4way va_b0 va_s0 alg n round_key init1 init2 init3 init4 round_keys =
  va_reveal_opaque (`%va_code_Aes_round_4way) (va_code_Aes_round_4way round_key);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  Vale.AES.AES_s.eval_rounds_reveal ();
  Vale.AES.AES_helpers.commute_sub_bytes_shift_rows_forall ();
  let (va_s8, va_fc8) = va_lemma_AESNI_enc (va_hd va_b1) va_s0 (va_op_xmm_xmm 2) round_key in
  let va_b8 = va_tl va_b1 in
  let (va_s9, va_fc9) = va_lemma_AESNI_enc (va_hd va_b8) va_s8 (va_op_xmm_xmm 12) round_key in
  let va_b9 = va_tl va_b8 in
  let (va_s10, va_fc10) = va_lemma_AESNI_enc (va_hd va_b9) va_s9 (va_op_xmm_xmm 13) round_key in
  let va_b10 = va_tl va_b9 in
  let (va_s11, va_fc11) = va_lemma_AESNI_enc (va_hd va_b10) va_s10 (va_op_xmm_xmm 14) round_key in
  let va_b11 = va_tl va_b10 in
  let (va_sM, va_f11) = va_lemma_empty_total va_s11 va_b11 in
  let va_f10 = va_lemma_merge_total va_b10 va_s10 va_fc11 va_s11 va_f11 va_sM in
  let va_f9 = va_lemma_merge_total va_b9 va_s9 va_fc10 va_s10 va_f10 va_sM in
  let va_f8 = va_lemma_merge_total va_b8 va_s8 va_fc9 va_s9 va_f9 va_sM in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc8 va_s8 va_f8 va_sM in
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Aes_round_4way (alg:algorithm) (n:pos) (round_key:va_operand_xmm) (init1:quad32)
  (init2:quad32) (init3:quad32) (init4:quad32) (round_keys:(seq quad32)) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_src_xmm round_key va_s0 /\ va_get_ok va_s0 /\ (aesni_enabled /\ (1 <= n /\ n <
    Vale.AES.AES_common_s.nr alg /\ Vale.AES.AES_common_s.nr alg <= FStar.Seq.Base.length #quad32
    round_keys) /\ va_get_xmm 2 va_s0 == Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\
    va_get_xmm 12 va_s0 == Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13
    va_s0 == Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_eval_xmm va_s0 round_key ==
    FStar.Seq.Base.index #quad32 round_keys n /\ 2 =!= round_key /\ 12 =!= round_key /\ 13 =!=
    round_key /\ 14 =!= round_key) /\ (forall (va_x_xmm2:quad32) (va_x_xmm12:quad32)
    (va_x_xmm13:quad32) (va_x_xmm14:quad32) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags
    va_x_efl (va_upd_xmm 14 va_x_xmm14 (va_upd_xmm 13 va_x_xmm13 (va_upd_xmm 12 va_x_xmm12
    (va_upd_xmm 2 va_x_xmm2 va_s0)))) in va_get_ok va_sM /\ (va_get_xmm 2 va_sM ==
    Vale.AES.AES_s.eval_rounds init1 round_keys n /\ va_get_xmm 12 va_sM ==
    Vale.AES.AES_s.eval_rounds init2 round_keys n /\ va_get_xmm 13 va_sM ==
    Vale.AES.AES_s.eval_rounds init3 round_keys n /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys n) ==> va_k va_sM (())))


val va_wpProof_Aes_round_4way : alg:algorithm -> n:pos -> round_key:va_operand_xmm -> init1:quad32
  -> init2:quad32 -> init3:quad32 -> init4:quad32 -> round_keys:(seq quad32) -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Aes_round_4way alg n round_key init1 init2 init3 init4
    round_keys va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Aes_round_4way round_key)
    ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2]) va_s0 va_k ((va_sM,
    va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Aes_round_4way alg n round_key init1 init2 init3 init4 round_keys va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Aes_round_4way (va_code_Aes_round_4way round_key) va_s0 alg n
    round_key init1 init2 init3 init4 round_keys in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM
    (va_update_xmm 12 va_sM (va_update_xmm 2 va_sM (va_update_ok va_sM va_s0)))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Aes_round_4way (alg:algorithm) (n:pos) (round_key:va_operand_xmm) (init1:quad32)
  (init2:quad32) (init3:quad32) (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit
  (va_code_Aes_round_4way round_key)) =
  (va_QProc (va_code_Aes_round_4way round_key) ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13;
    va_Mod_xmm 12; va_Mod_xmm 2]) (va_wp_Aes_round_4way alg n round_key init1 init2 init3 init4
    round_keys) (va_wpProof_Aes_round_4way alg n round_key init1 init2 init3 init4 round_keys))
//--
//-- Aes_2rounds_4way

val va_code_Aes_2rounds_4way : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Aes_2rounds_4way () =
  (va_Block (va_CCons (va_code_Aes_round_4way (va_op_xmm_xmm 3)) (va_CCons (va_code_Aes_round_4way
    (va_op_xmm_xmm 4)) (va_CNil ()))))

val va_codegen_success_Aes_2rounds_4way : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Aes_2rounds_4way () =
  (va_pbool_and (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 3)) (va_pbool_and
    (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 4)) (va_ttrue ())))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Aes_2rounds_4way (va_mods:va_mods_t) (alg:algorithm) (n:pos) (init1:quad32)
  (init2:quad32) (init3:quad32) (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit
  (va_code_Aes_2rounds_4way ())) =
  (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 162 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg n (va_op_xmm_xmm 3) init1 init2 init3 init4 round_keys) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 163 column 19 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg (n + 1) (va_op_xmm_xmm 4) init1 init2 init3 init4 round_keys)
    (va_QEmpty (())))))


val va_lemma_Aes_2rounds_4way : va_b0:va_code -> va_s0:va_state -> alg:algorithm -> n:pos ->
  init1:quad32 -> init2:quad32 -> init3:quad32 -> init4:quad32 -> round_keys:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Aes_2rounds_4way ()) va_s0 /\ va_get_ok va_s0 /\
    (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr alg - 1 /\ Vale.AES.AES_common_s.nr
    alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm 2 va_s0 ==
    Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_get_xmm 3 va_s0 ==
    FStar.Seq.Base.index #quad32 round_keys n /\ va_get_xmm 4 va_s0 == FStar.Seq.Base.index #quad32
    round_keys (n + 1))))
  (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 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 1) /\ va_get_xmm 12
    va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 1) /\ va_get_xmm 13 va_sM ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n + 1) /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n + 1)) /\ va_state_eq va_sM (va_update_flags
    va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM (va_update_xmm 12 va_sM (va_update_xmm 2
    va_sM (va_update_ok va_sM va_s0))))))))
[@"opaque_to_smt"]
let va_lemma_Aes_2rounds_4way va_b0 va_s0 alg n init1 init2 init3 init4 round_keys =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm
    2; va_Mod_ok] in
  let va_qc = va_qcode_Aes_2rounds_4way va_mods alg n init1 init2 init3 init4 round_keys in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Aes_2rounds_4way ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 130 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 157 column 54 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 1)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 158 column 54 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 12 va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 1)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 159 column 54 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 13 va_sM == Vale.AES.AES_s.eval_rounds init3 round_keys (n + 1)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 160 column 54 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 14 va_sM == Vale.AES.AES_s.eval_rounds init4 round_keys (n + 1)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Aes_2rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
  (init4:quad32) (round_keys:(seq quad32)) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr alg - 1 /\
    Vale.AES.AES_common_s.nr alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm 2 va_s0
    == Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_get_xmm 3 va_s0 ==
    FStar.Seq.Base.index #quad32 round_keys n /\ va_get_xmm 4 va_s0 == FStar.Seq.Base.index #quad32
    round_keys (n + 1)) /\ (forall (va_x_xmm2:quad32) (va_x_xmm12:quad32) (va_x_xmm13:quad32)
    (va_x_xmm14:quad32) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_xmm
    14 va_x_xmm14 (va_upd_xmm 13 va_x_xmm13 (va_upd_xmm 12 va_x_xmm12 (va_upd_xmm 2 va_x_xmm2
    va_s0)))) in va_get_ok va_sM /\ (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1
    round_keys (n + 1) /\ va_get_xmm 12 va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n +
    1) /\ va_get_xmm 13 va_sM == Vale.AES.AES_s.eval_rounds init3 round_keys (n + 1) /\ va_get_xmm
    14 va_sM == Vale.AES.AES_s.eval_rounds init4 round_keys (n + 1)) ==> va_k va_sM (())))


val va_wpProof_Aes_2rounds_4way : alg:algorithm -> n:pos -> init1:quad32 -> init2:quad32 ->
  init3:quad32 -> init4:quad32 -> round_keys:(seq quad32) -> va_s0:va_state -> va_k:(va_state ->
  unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys
    va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Aes_2rounds_4way ()) ([va_Mod_flags;
    va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Aes_2rounds_4way (va_code_Aes_2rounds_4way ()) va_s0 alg n init1
    init2 init3 init4 round_keys in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM
    (va_update_xmm 12 va_sM (va_update_xmm 2 va_sM (va_update_ok va_sM va_s0)))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Aes_2rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
val va_quick_Aes_2rounds_4way
      (alg: algorithm)
      (n: pos)
      (init1 init2 init3 init4: quad32)
      (round_keys: (seq quad32))
    : (va_quickCode unit (va_code_Aes_2rounds_4way ()))

    alg: Vale.AES.AES_common_s.algorithm ->
    n: Prims.pos ->
    init1: Vale.X64.Decls.quad32 ->
    init2: Vale.X64.Decls.quad32 ->
    init3: Vale.X64.Decls.quad32 ->
    init4: Vale.X64.Decls.quad32 ->
    round_keys: FStar.Seq.Base.seq Vale.X64.Decls.quad32
  -> Vale.X64.QuickCode.va_quickCode Prims.unit (Vale.AES.X64.AESCTR.va_code_Aes_2rounds_4way ())