val iv_buffer : Type0
let iv_buffer = b:A.array U8.t { A.length b == iv_len }
module Zeta.Steel.HashAccumulator
module U8 = FStar.UInt8
module U32 = FStar.UInt32
module A = Steel.ST.Array
open Steel.ST.Util

inline_for_extraction noextract
let max_input_length = pow2 31 - 1

// NOTE: we do not have an agile spec for the keyed hash functionality :(, so
// we're making Blake2-dependent assumptions without corresponding agile predicates
noextract inline_for_extraction
let hashable_bytes = s:Seq.seq U8.t { Seq.length s <= max_input_length }
let hashable_buffer = b:A.array U8.t { A.length b <= max_input_length }

inline_for_extraction noextract
let iv_len = 96
/
Steel.ST.Util.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.HashAccumulator.fsti
Type0
Steel.ST.Array.array FStar.UInt8.t Prims.eq2 Prims.int Steel.ST.Array.length Zeta.Steel.HashAccumulator.iv_len
let iv_buffer =
  
b: A.array U8.t {A.length b == iv_len}