val va_wp_SHA256_msg1
      (dst src: va_operand_xmm)
      (t: counter)
      (block: block_w)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_SHA256_msg1 (dst:va_operand_xmm) (src:va_operand_xmm) (t:counter) (block:block_w)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ sha_enabled /\ ((16 <=
    t && t < size_k_w_256)) /\ va_eval_xmm va_s0 dst == ws_quad32 (t - 16) block /\ (va_eval_xmm
    va_s0 src).lo0 == ws_opaque block (t - 12) /\ (forall (va_x_dst:va_value_xmm) . let va_sM =
    va_upd_operand_xmm dst va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_xmm va_sM dst == ws_partial
    t block ==> va_k va_sM (())))
val va_wp_SHA256_msg1
      (dst src: va_operand_xmm)
      (t: counter)
      (block: block_w)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_SHA256_msg1
      (dst src: va_operand_xmm)
      (t: counter)
      (block: block_w)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0 =
(va_is_dst_xmm dst va_s0 /\ va_is_src_xmm src va_s0 /\ va_get_ok va_s0 /\ sha_enabled /\
  ((16 <= t && t < size_k_w_256)) /\ va_eval_xmm va_s0 dst == ws_quad32 (t - 16) block /\
  (va_eval_xmm va_s0 src).lo0 == ws_opaque block (t - 12) /\
  (forall (va_x_dst: va_value_xmm).
      let va_sM = va_upd_operand_xmm dst va_x_dst va_s0 in
      va_get_ok va_sM /\ va_eval_xmm va_sM dst == ws_partial t block ==> va_k va_sM (())))
Vale.X64.InsSha.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsVector.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.SHA.SHA_helpers.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Spec.SHA2.fsti.checked Spec.Loops.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.X64.InsSha.fsti
Vale.X64.Decls.va_operand_xmm Vale.SHA.SHA_helpers.counter Vale.SHA.SHA_helpers.block_w Vale.X64.Decls.va_state Prims.unit Prims.l_and Vale.X64.Decls.va_is_dst_xmm Vale.X64.Decls.va_is_src_xmm Prims.b2t Vale.X64.Decls.va_get_ok Vale.X64.CPU_Features_s.sha_enabled Prims.op_AmpAmp Prims.op_LessThanOrEqual Prims.op_LessThan Vale.SHA.SHA_helpers.size_k_w_256 Prims.eq2 Vale.Def.Types_s.quad32 Vale.X64.Decls.va_eval_xmm Vale.SHA.SHA_helpers.ws_quad32 Prims.op_Subtraction Vale.Def.Words_s.nat32 Vale.Def.Words_s.__proj__Mkfour__item__lo0 Vale.Def.Types_s.nat32 Vale.SHA.SHA_helpers.ws_opaque Prims.l_Forall Vale.X64.Decls.va_value_xmm Prims.l_imp Vale.SHA.SHA_helpers.ws_partial Vale.X64.State.vale_state Vale.X64.Decls.va_upd_operand_xmm
module Vale.X64.InsSha
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Spec.SHA2
open Spec.Hash.Definitions
open Vale.SHA.SHA_helpers
open Vale.X64.Machine_s
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.QuickCode
open Vale.X64.InsVector
open FStar.UInt32

open FStar.Seq
open Spec.Loops
open Vale.X64.CPU_Features_s
//-- SHA256_rnds2

val va_code_SHA256_rnds2 : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_code

val va_codegen_success_SHA256_rnds2 : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_pbool

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_qattr]
let va_wp_SHA256_rnds2 (dst:va_operand_xmm) (src:va_operand_xmm) (t:counter) (block:block_w)
  (hash_orig:hash256) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (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 /\ (forall (va_x_dst:va_value_xmm) . let va_sM =
    va_upd_operand_xmm dst va_x_dst va_s0 in 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_k va_sM (())))

val va_wpProof_SHA256_rnds2 : dst:va_operand_xmm -> src:va_operand_xmm -> t:counter ->
  block:block_w -> hash_orig:hash256 -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_SHA256_rnds2 dst src t block hash_orig va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_SHA256_rnds2 dst src) ([va_mod_xmm
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_SHA256_rnds2 (dst:va_operand_xmm) (src:va_operand_xmm) (t:counter) (block:block_w)
  (hash_orig:hash256) : (va_quickCode unit (va_code_SHA256_rnds2 dst src)) =
  (va_QProc (va_code_SHA256_rnds2 dst src) ([va_mod_xmm dst]) (va_wp_SHA256_rnds2 dst src t block
    hash_orig) (va_wpProof_SHA256_rnds2 dst src t block hash_orig))
//--
//-- SHA256_msg1

val va_code_SHA256_msg1 : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_code

val va_codegen_success_SHA256_msg1 : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_pbool

val va_lemma_SHA256_msg1 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_xmm ->
  src:va_operand_xmm -> t:counter -> block:block_w
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SHA256_msg1 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 /\ ((16 <= t && t < size_k_w_256))
    /\ va_eval_xmm va_s0 dst == ws_quad32 (t - 16) block /\ (va_eval_xmm va_s0 src).lo0 ==
    ws_opaque block (t - 12)))
  (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 == ws_partial t block /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_xmm dst va_sM va_s0))))
[@ va_qattr]
let va_wp_SHA256_msg1 (dst:va_operand_xmm) (src:va_operand_xmm) (t:counter) (block:block_w)
val va_wp_SHA256_msg1
      (dst src: va_operand_xmm)
      (t: counter)
      (block: block_w)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0

    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 ->
    va_s0: Vale.X64.Decls.va_state ->
    va_k: (_: Vale.X64.Decls.va_state -> _: Prims.unit -> Type0)
  -> Type0