let counter = nat
let counter =
nat
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
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
val counter : Type0
Type0