val hash_init (#hsz: pos) : hash #hsz
let hash_init (#hsz:pos): hash #hsz =
  Seq.create hsz (Lib.IntTypes.u8 0)
val hash_init (#hsz: pos) : hash #hsz
let hash_init (#hsz: pos) : hash #hsz =
Seq.create hsz (Lib.IntTypes.u8 0)
MerkleTree.New.High.fst.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked MerkleTree.Spec.fst.checked Lib.IntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
MerkleTree.New.High.fst
Prims.pos FStar.Seq.Base.create Lib.IntTypes.uint8 Lib.IntTypes.u8 MerkleTree.New.High.hash
module MerkleTree.New.High

open FStar.Ghost
open FStar.Seq

module S = FStar.Seq

module U32 = FStar.UInt32
module U8 = FStar.UInt8

module MTS = MerkleTree.Spec

#set-options "--z3rlimit 10 --max_fuel 0 --max_ifuel 0"

type uint32_t = U32.t
type uint8_t = U8.t

type hash (#hsz:pos) = b:Spec.Hash.Definitions.bytes{Seq.length b = hsz}
type hashes (#hsz:pos) = S.seq (hash #hsz)
type hashess (#hsz:pos) = S.seq (hashes #hsz)

noextract
val hash_init (#hsz: pos) : hash #hsz
MerkleTree.New.High.hash