let shuffle_core = shuffle_core_
let shuffle_core =
shuffle_core_
Spec.SHA2.Lemmas.fst.checked
Spec.SHA2.Constants.fst.checked Spec.SHA2.fst.checked Spec.SHA2.fst.checked Spec.Loops.fst.checked Spec.Hash.Lemmas.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked Lib.UpdateMulti.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Spec.SHA2.Lemmas.fst
Spec.SHA2.Lemmas.shuffle_core_
module Spec.SHA2.Lemmas

open Lib.IntTypes
module C = Spec.SHA2.Constants
module S = FStar.Seq

open Spec.Hash.Definitions
open Spec.SHA2
open Spec.Hash.Lemmas

friend Spec.SHA2
friend Spec.Agile.Hash

#set-options "--z3rlimit 25 --fuel 0 --ifuel 0"

(* Scheduling function *)

(* Recursive Version *)
let rec ws_aux (a:sha2_alg) (b:block_w a) (t:counter{t < size_k_w a}): Tot (word a) =
  if t < block_word_length a then b.[t]
  else
    let t16 = ws_aux a b (t - 16) in
    let t15 = ws_aux a b (t - 15) in
    let t7  = ws_aux a b (t - 7) in
    let t2  = ws_aux a b (t - 2) in

    let s1 = _sigma1 a t2 in
    let s0 = _sigma0 a t15 in
    (s1 +. t7 +. s0 +. t16)

[@"opaque_to_smt"]
let ws = ws_aux

(* Core shuffling function *)
let shuffle_core_ (a:sha2_alg) (block:block_w a) (hash:words_state a) (t:counter{t < size_k_w a}): Tot (words_state a) =
  (**) assert(7 <= S.length hash);
  let a0 = hash.[0] in
  let b0 = hash.[1] in
  let c0 = hash.[2] in
  let d0 = hash.[3] in
  let e0 = hash.[4] in
  let f0 = hash.[5] in
  let g0 = hash.[6] in
  let h0 = hash.[7] in

  (**) assert(S.length (k0 a) = size_k_w a);
  let t1 = h0 +. (_Sigma1 a e0) +. (_Ch a e0 f0 g0) +. (k0 a).[t] +. (ws a block t) in
  let t2 = (_Sigma0 a a0) +. (_Maj a a0 b0 c0) in

  (**) assert(t < S.length (k0 a));
  let l = [ t1 +. t2; a0; b0; c0; d0 +. t1; e0; f0; g0 ] in
  assert_norm (List.Tot.length l = 8);
  S.seq_of_list l
val shuffle_core : a: Spec.Hash.Definitions.sha2_alg ->
    block: Spec.SHA2.block_w a ->
    hash: Spec.Hash.Definitions.words_state a ->
    t: Spec.SHA2.counter{t < Spec.SHA2.size_k_w a}
  -> Spec.Hash.Definitions.words_state a

    a: Spec.Hash.Definitions.sha2_alg ->
    block: Spec.SHA2.block_w a ->
    hash: Spec.Hash.Definitions.words_state a ->
    t: Spec.SHA2.counter{t < Spec.SHA2.size_k_w a}
  -> Spec.Hash.Definitions.words_state a