val free_hash (#hsz: Ghost.erased hash_size_t) (h: hash #hsz)
    : HST.ST unit (requires (fun h0 -> (Rgl?.r_inv (hreg hsz)) h0 h)) (ensures (fun _ _ _ -> True))
let free_hash 
  (#hsz:Ghost.erased hash_size_t) 
  (h:hash #hsz): HST.ST unit
  (requires (fun h0 -> (Rgl?.r_inv (hreg hsz)) h0 h))
  (ensures (fun _ _ _ -> True))
= B.free h
val free_hash (#hsz: Ghost.erased hash_size_t) (h: hash #hsz)
    : HST.ST unit (requires (fun h0 -> (Rgl?.r_inv (hreg hsz)) h0 h)) (ensures (fun _ _ _ -> True))
let free_hash (#hsz: Ghost.erased hash_size_t) (h: hash #hsz)
    : HST.ST unit (requires (fun h0 -> (Rgl?.r_inv (hreg hsz)) h0 h)) (ensures (fun _ _ _ -> True)) =
B.free h
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
FStar.Ghost.erased MerkleTree.Low.Datastructures.hash_size_t MerkleTree.Low.Datastructures.hash FStar.Ghost.reveal LowStar.Monotonic.Buffer.free Lib.IntTypes.uint8 LowStar.Buffer.trivial_preorder Prims.unit FStar.Monotonic.HyperStack.mem LowStar.Regional.__proj__Rgl__item__r_inv MerkleTree.Low.Datastructures.hreg Prims.l_True
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"

let init_hash (hsz:hash_size_t) (r:HST.erid): HST.St (hash #hsz) 
= rg_alloc (hreg hsz) r

#set-options "--z3rlimit 200 --initial_fuel 2 --max_fuel 2 --initial_ifuel 2 --max_ifuel 2"

let free_hash 
  (#hsz:Ghost.erased hash_size_t) 
  (h:hash #hsz): HST.ST unit
  (requires (fun h0 -> (Rgl?.r_inv (hreg hsz)) h0 h))
val free_hash (#hsz: Ghost.erased hash_size_t) (h: hash #hsz)
    : HST.ST unit (requires (fun h0 -> (Rgl?.r_inv (hreg hsz)) h0 h)) (ensures (fun _ _ _ -> True))
h: MerkleTree.Low.Datastructures.hash -> FStar.HyperStack.ST.ST Prims.unit