val max_input_length : Prims.int
let max_input_length = pow2 31 - 1
module Zeta.Steel.HashAccumulator
module U8 = FStar.UInt8
module U32 = FStar.UInt32
module A = Steel.ST.Array
open Steel.ST.Util
/
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
Prims.int
Prims.op_Subtraction Prims.pow2
let max_input_length =
  
pow2 31 - 1