let repeat_range_vale (max:nat { max < size_k_w_256}) (block:block_w) (hash:hash256) =
  Spec.Loops.repeat_range 0 max (shuffle_core_opaque block) hash
let repeat_range_vale (max: nat{max < size_k_w_256}) (block: block_w) (hash: hash256) =
Spec.Loops.repeat_range 0 max (shuffle_core_opaque block) hash
Vale.SHA.PPC64LE.SHA_helpers.fsti.checked
Vale.SHA2.Wrapper.fsti.checked Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Sel.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Spec.Loops.fst.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.SHA.PPC64LE.SHA_helpers.fsti
Prims.nat Prims.b2t Prims.op_LessThan Vale.SHA.PPC64LE.SHA_helpers.size_k_w_256 Vale.SHA.PPC64LE.SHA_helpers.block_w Vale.SHA.PPC64LE.SHA_helpers.hash256 Spec.Loops.repeat_range Vale.SHA.PPC64LE.SHA_helpers.shuffle_core_opaque
module Vale.SHA.PPC64LE.SHA_helpers

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open FStar.Seq
open Vale.Arch.Types
open Vale.Def.Sel
open Vale.SHA2.Wrapper
open Vale.Def.Words.Four_s

unfold let (.[]) = FStar.Seq.index

#reset-options "--max_fuel 0 --max_ifuel 0"

// Specialize these definitions (from Spec.SHA2.fst) for SHA256
unfold let size_k_w_256 = 64
val word:Type0
(* Number of words for a block size *)
let size_block_w_256 = 16
(* Define the size block in bytes *)
let block_length =
  4 (*word_length a*) * size_block_w_256
let block_w  = m:seq word {length m = size_block_w_256}
let counter = nat
val k : (s:seq word {length s = size_k_w_256})
let hash256 = m:Seq.seq word {Seq.length m = 8}

(* Input data. *)
type byte = UInt8.t
type bytes = Seq.seq byte

(* Input data, multiple of a block length. *)
let bytes_blocks =
  l:bytes { Seq.length l % block_length = 0 }

// Hide various SHA2 definitions
val ws_opaque (b:block_w) (t:counter{t < size_k_w_256}):nat32
val shuffle_core_opaque (block:block_w) (hash:hash256) (t:counter{t < size_k_w_256}):hash256
val update_multi_opaque (hash:hash256) (blocks:bytes_blocks):hash256
val update_multi_transparent (hash:hash256) (blocks:bytes_blocks):hash256

// Hide some functions that operate on words & bytes
val word_to_nat32 (x:word) : nat32
val nat32_to_word (x:nat32) : word

//unfold let bytes_blocks256 = bytes_blocks SHA2_256
val repeat_range_vale : max: Prims.nat{max < Vale.SHA.PPC64LE.SHA_helpers.size_k_w_256} ->
    block: Vale.SHA.PPC64LE.SHA_helpers.block_w ->
    hash: Vale.SHA.PPC64LE.SHA_helpers.hash256
  -> Vale.SHA.PPC64LE.SHA_helpers.hash256

    max: Prims.nat{max < Vale.SHA.PPC64LE.SHA_helpers.size_k_w_256} ->
    block: Vale.SHA.PPC64LE.SHA_helpers.block_w ->
    hash: Vale.SHA.PPC64LE.SHA_helpers.hash256
  -> Vale.SHA.PPC64LE.SHA_helpers.hash256