val maybe_aggregate_hashes : b: Prims.bool ->
    h0: Zeta.Steel.HashAccumulator.hash_value_t ->
    h1: Zeta.Steel.HashAccumulator.hash_value_t
  -> Zeta.Steel.HashAccumulator.hash_value_t
let maybe_aggregate_hashes (b:bool) (h0 h1: hash_value_t) =
  if b then aggregate_hashes h0 h1
  else h0
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
let iv_t = Seq.lseq U8.t iv_len
let iv_buffer = b:A.array U8.t { A.length b == iv_len }

[@@erasable]
val hash_value_t : Type0

val ha
  : Type0

val ha_val (r:ha) (v:hash_value_t)
  : vprop
  
val initial_hash
  : hash_value_t

val hash_one_value (iv:iv_t) (_:hashable_bytes)
  : hash_value_t

val aggregate_hashes (_ _: hash_value_t)
  : hash_value_t

val initial_hash_unit (h:hash_value_t)
  : Lemma (aggregate_hashes initial_hash h == h)

val aggregate_hashes_commutative (h1 h2:hash_value_t)
  : Lemma (aggregate_hashes h1 h2 == aggregate_hashes h2 h1)

val aggregate_hashes_associative (h1 h2 h3:hash_value_t)
  : Lemma (aggregate_hashes h1 (aggregate_hashes h2 h3) ==
           aggregate_hashes (aggregate_hashes h1 h2) h3)

(*** THE MAIN INTERFACE ***)

(** Create an instance of a hash accumulator in the heap *)
val create (_:unit)
  : STT ha
    emp
    (fun s -> ha_val s initial_hash)

(** Free the hash accumulator *)
val reclaim (#h:hash_value_t) (s:ha)
  : STT unit
    (ha_val s h)
    (fun _ -> emp)
/
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

    b: Prims.bool ->
    h0: Zeta.Steel.HashAccumulator.hash_value_t ->
    h1: Zeta.Steel.HashAccumulator.hash_value_t
  -> Zeta.Steel.HashAccumulator.hash_value_t
Prims.bool Zeta.Steel.HashAccumulator.hash_value_t Zeta.Steel.HashAccumulator.aggregate_hashes
let maybe_aggregate_hashes (b: bool) (h0 h1: hash_value_t) =
  
if b then aggregate_hashes h0 h1 else h0