val ws_aux (a: sha2_alg) (b: block_w a) (t: counter{t < size_k_w a}) : Tot (word a)
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)
val ws_aux (a: sha2_alg) (b: block_w a) (t: counter{t < size_k_w a}) : Tot (word a)
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)
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.Hash.Definitions.sha2_alg Spec.SHA2.block_w Spec.SHA2.counter Prims.b2t Prims.op_LessThan Spec.SHA2.size_k_w Spec.Hash.Definitions.block_word_length Spec.SHA2.op_String_Access Spec.Hash.Definitions.word Prims.bool Spec.SHA2.op_Plus_Dot Spec.SHA2._sigma0 Spec.SHA2._sigma1 Spec.SHA2.Lemmas.ws_aux Prims.op_Subtraction
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 *)
val ws_aux (a: sha2_alg) (b: block_w a) (t: counter{t < size_k_w a}) : Tot (word a)

    a: Spec.Hash.Definitions.sha2_alg ->
    b: Spec.SHA2.block_w a ->
    t: Spec.SHA2.counter{t < Spec.SHA2.size_k_w a}
  -> Spec.Hash.Definitions.word a