val update_multi_transparent (hash:hash256) (blocks:bytes_blocks):hash256
let update_multi_transparent (hash:hash256) (blocks:bytes_blocks) =
  update_multi SHA2_256 hash () blocks
val update_multi_transparent (hash:hash256) (blocks:bytes_blocks):hash256
let update_multi_transparent (hash: hash256) (blocks: bytes_blocks) =
update_multi SHA2_256 hash () blocks
Vale.SHA.PPC64LE.SHA_helpers.fst.checked
Vale.SHA2.Wrapper.fst.checked Vale.SHA2.Wrapper.fst.checked Vale.Lib.Seqs_s.fst.checked Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.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.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Spec.SHA2.Lemmas.fst.checked Spec.SHA2.Lemmas.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.fsti.checked prims.fst.checked Lib.UpdateMulti.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.SHA.PPC64LE.SHA_helpers.fst
Vale.SHA.PPC64LE.SHA_helpers.hash256 Vale.SHA.PPC64LE.SHA_helpers.bytes_blocks Spec.Agile.Hash.update_multi Spec.Hash.Definitions.SHA2_256
module Vale.SHA.PPC64LE.SHA_helpers

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Spec.SHA2
open Spec.SHA2.Lemmas
open Spec.Agile.Hash
open Spec.Hash.Definitions
open Spec.Hash.Lemmas
open Vale.Def.Types_s
open Vale.Def.Words_s
open FStar.Seq
open FStar.UInt32  // Interop with UInt-based SHA spec
open Vale.Arch.Types
open Vale.Arch.TypesNative
open Vale.Def.Sel
open Vale.SHA2.Wrapper

friend Spec.SHA2
friend Spec.SHA2.Lemmas
friend Vale.SHA2.Wrapper

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

// Define these specific converters here, so that F* only reasons about
// the correctness of the conversion once, rather that at every call site
let vv (u:Lib.IntTypes.uint32) : nat32 = Lib.IntTypes.v u
let to_uint32 (n:nat32) : Lib.IntTypes.uint32 = Lib.IntTypes.u32 n
let word = Lib.IntTypes.uint32
let k = (Spec.SHA2.k0 SHA2_256)

val add_mod_lemma:x:Lib.IntTypes.uint32 -> y:Lib.IntTypes.uint32 ->
		  Lemma (add_mod x y == Lib.IntTypes.(x +. y))
			[SMTPat (Lib.IntTypes.(x +. y))]
let add_mod_lemma x y = ()

unfold let ws_opaque_aux = ws
let ws_opaque (b:block_w) (t:counter{t < size_k_w_256}) : nat32 =
  vv (ws_opaque_aux SHA2_256 b t)

unfold let shuffle_core_opaque_aux = shuffle_core
let shuffle_core_opaque (block:block_w) (hash:hash256) (t:counter{t < size_k_w_256}):hash256 =
  shuffle_core_opaque_aux SHA2_256 block hash t

[@"opaque_to_smt"] let update_multi_opaque_aux = opaque_make update_multi
irreducible let update_multi_reveal = opaque_revealer (`%update_multi_opaque_aux) update_multi_opaque_aux update_multi
let update_multi_opaque (hash:hash256) (blocks:bytes_blocks):hash256 =
  update_multi_opaque_aux SHA2_256 hash () blocks
val update_multi_transparent (hash:hash256) (blocks:bytes_blocks):hash256
hash: Vale.SHA.PPC64LE.SHA_helpers.hash256 -> blocks: Vale.SHA.PPC64LE.SHA_helpers.bytes_blocks
  -> Vale.SHA.PPC64LE.SHA_helpers.hash256