val init_hash (hsz: hash_size_t) (r: HST.erid) : HST.St (hash #hsz)
let init_hash (hsz:hash_size_t) (r:HST.erid): HST.St (hash #hsz) 
= rg_alloc (hreg hsz) r
val init_hash (hsz: hash_size_t) (r: HST.erid) : HST.St (hash #hsz)
let init_hash (hsz: hash_size_t) (r: HST.erid) : HST.St (hash #hsz) =
rg_alloc (hreg hsz) r
MerkleTree.Low.Hashfunctions.fst.checked
prims.fst.checked MerkleTree.Spec.fst.checked MerkleTree.New.High.fst.checked MerkleTree.Low.Datastructures.fst.checked LowStar.Vector.fst.checked LowStar.RVector.fst.checked LowStar.Regional.Instances.fst.checked LowStar.Regional.fst.checked LowStar.ConstBuffer.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Monotonic.HyperStack.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.All.fst.checked EverCrypt.Helpers.fsti.checked
MerkleTree.Low.Hashfunctions.fst
MerkleTree.Low.Datastructures.hash_size_t FStar.HyperStack.ST.erid LowStar.Regional.rg_alloc MerkleTree.Low.Datastructures.hash MerkleTree.Low.Datastructures.hreg
module MerkleTree.Low.Hashfunctions

open EverCrypt.Helpers

open FStar.All
open FStar.Integers
open FStar.Mul

open LowStar.Buffer
open LowStar.BufferOps
open LowStar.Vector
open LowStar.Regional
open LowStar.RVector
open LowStar.Regional.Instances

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module MHS = FStar.Monotonic.HyperStack
module HH = FStar.Monotonic.HyperHeap

module B = LowStar.Buffer
module CB = LowStar.ConstBuffer
module V = LowStar.Vector
module RV = LowStar.RVector
module RVI = LowStar.Regional.Instances

module S = FStar.Seq

module U32 = FStar.UInt32
module MTH = MerkleTree.New.High
module MTS = MerkleTree.Spec

open Lib.IntTypes

open MerkleTree.Low.Datastructures

#set-options "--z3rlimit 10 --initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
val init_hash (hsz: hash_size_t) (r: HST.erid) : HST.St (hash #hsz)
hsz: MerkleTree.Low.Datastructures.hash_size_t -> r: FStar.HyperStack.ST.erid
  -> FStar.HyperStack.ST.St MerkleTree.Low.Datastructures.hash