val va_lemma_SHA256_rnds2 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src:va_operand_xmm -> t:counter -> block:block_w -> hash_orig:hash256
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SHA256_rnds2 dst src) va_s0 /\ va_is_dst_xmm dst va_s0
    /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ sha_enabled /\ t + 1 < size_k_w_256 /\
    (va_get_xmm 0 va_s0).lo0 == add_wrap (word_to_nat32 (index k t)) (ws_opaque block t) /\
    (va_get_xmm 0 va_s0).lo1 == add_wrap (word_to_nat32 (index k (t + 1))) (ws_opaque block (t +
    1)) /\ make_hash (va_eval_xmm va_s0 src) (va_eval_xmm va_s0 dst) == repeat_range 0 t
    (shuffle_core_opaque block) hash_orig))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    make_hash (va_eval_xmm va_sM dst) (va_eval_xmm va_s0 src) == repeat_range 0 (t + 2)
    (shuffle_core_opaque block) hash_orig /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_xmm dst va_sM va_s0))))
let va_lemma_SHA256_rnds2 va_b0 va_s0 dst src t block hash_orig =
  va_reveal_opaque (`%va_code_SHA256_rnds2) (va_code_SHA256_rnds2 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr (I.ins_SHA256_rnds2) (OReg dst) (OReg src))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr (I.ins_SHA256_rnds2) (OReg dst) (OReg src)))
    va_s0 in
  lemma_sha256_rnds2 (va_eval_xmm va_old_s src) (va_eval_xmm va_old_s dst) (va_get_xmm 0 va_old_s)
    t block hash_orig;
  (va_sM, va_fM)
val va_lemma_SHA256_rnds2 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src:va_operand_xmm -> t:counter -> block:block_w -> hash_orig:hash256
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SHA256_rnds2 dst src) va_s0 /\ va_is_dst_xmm dst va_s0
    /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ sha_enabled /\ t + 1 < size_k_w_256 /\
    (va_get_xmm 0 va_s0).lo0 == add_wrap (word_to_nat32 (index k t)) (ws_opaque block t) /\
    (va_get_xmm 0 va_s0).lo1 == add_wrap (word_to_nat32 (index k (t + 1))) (ws_opaque block (t +
    1)) /\ make_hash (va_eval_xmm va_s0 src) (va_eval_xmm va_s0 dst) == repeat_range 0 t
    (shuffle_core_opaque block) hash_orig))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    make_hash (va_eval_xmm va_sM dst) (va_eval_xmm va_s0 src) == repeat_range 0 (t + 2)
    (shuffle_core_opaque block) hash_orig /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_xmm dst va_sM va_s0))))
let va_lemma_SHA256_rnds2 va_b0 va_s0 dst src t block hash_orig =
va_reveal_opaque (`%va_code_SHA256_rnds2) (va_code_SHA256_rnds2 dst src);
let va_old_s:va_state = va_s0 in
va_ins_lemma (mk_ins (make_instr (I.ins_SHA256_rnds2) (OReg dst) (OReg src))) va_s0;
let va_sM, va_fM =
  va_eval_ins (mk_ins (make_instr (I.ins_SHA256_rnds2) (OReg dst) (OReg src))) va_s0
in
lemma_sha256_rnds2 (va_eval_xmm va_old_s src)
  (va_eval_xmm va_old_s dst)
  (va_get_xmm 0 va_old_s)
  t
  block
  hash_orig;
(va_sM, va_fM)
Vale.X64.InsSha.fst.checked
Vale.X64.Taint_Semantics.fst.checked Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.Decls.fst.checked Vale.X64.Decls.fst.checked Vale.X64.CryptoInstructions_s.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Types_s.fst.checked Spec.SHA2.fsti.checked Spec.Hash.Definitions.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.X64.InsSha.fst
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Vale.X64.Decls.va_operand_xmm Vale.SHA.SHA_helpers.counter Vale.SHA.SHA_helpers.block_w Vale.SHA.SHA_helpers.hash256 Vale.X64.State.vale_state Vale.X64.Lemmas.fuel FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_fuel Prims.unit Vale.SHA.SHA_helpers.lemma_sha256_rnds2 Vale.X64.Decls.va_eval_xmm Vale.X64.Decls.va_get_xmm FStar.Pervasives.Native.tuple2 Prims.nat Vale.X64.Decls.va_eval_ins Vale.X64.Taint_Semantics.mk_ins Vale.X64.InsLemmas.make_instr Prims.Cons Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.inOut Vale.X64.Instruction_s.opXmm Prims.Nil Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.oneXmm Vale.X64.Machine_s.OReg Vale.X64.Machine_s.quad32 Vale.X64.Machine_s.reg_xmm Vale.X64.Instruction_s.PreserveFlags Vale.X64.Instructions_s.ins_SHA256_rnds2 Vale.X64.Decls.va_ins_lemma Vale.X64.Decls.va_reveal_opaque Vale.X64.InsSha.va_code_SHA256_rnds2
module Vale.X64.InsSha
open Vale.Def.Types_s
open Vale.X64.Machine_s
open Vale.X64
open Vale.X64.State
open Vale.X64.StateLemmas
open Vale.X64.InsLemmas
open Vale.X64.Taint_Semantics
open Vale.X64.Decls
open Vale.X64.CryptoInstructions_s
open Spec.Hash.Definitions
open Spec.SHA2
open Vale.X64.CPU_Features_s
module I = Vale.X64.Instructions_s
module S = Vale.X64.Machine_Semantics_s
module P = Vale.X64.Print_s

friend Vale.X64.Decls
#reset-options "--initial_fuel 4 --max_fuel 4 --max_ifuel 2 --z3rlimit 20"
//-- SHA256_rnds2

[@ "opaque_to_smt"]
let va_code_SHA256_rnds2 dst src =
  (mk_ins (make_instr (I.ins_SHA256_rnds2) (OReg dst) (OReg src)))

[@ "opaque_to_smt"]
let va_codegen_success_SHA256_rnds2 dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
val va_lemma_SHA256_rnds2 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src:va_operand_xmm -> t:counter -> block:block_w -> hash_orig:hash256
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SHA256_rnds2 dst src) va_s0 /\ va_is_dst_xmm dst va_s0
    /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ sha_enabled /\ t + 1 < size_k_w_256 /\
    (va_get_xmm 0 va_s0).lo0 == add_wrap (word_to_nat32 (index k t)) (ws_opaque block t) /\
    (va_get_xmm 0 va_s0).lo1 == add_wrap (word_to_nat32 (index k (t + 1))) (ws_opaque block (t +
    1)) /\ make_hash (va_eval_xmm va_s0 src) (va_eval_xmm va_s0 dst) == repeat_range 0 t
    (shuffle_core_opaque block) hash_orig))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    make_hash (va_eval_xmm va_sM dst) (va_eval_xmm va_s0 src) == repeat_range 0 (t + 2)
    (shuffle_core_opaque block) hash_orig /\ va_state_eq 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 ->
    t: Vale.SHA.SHA_helpers.counter ->
    block: Vale.SHA.SHA_helpers.block_w ->
    hash_orig: Vale.SHA.SHA_helpers.hash256
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)