let u32_64 = Int.Cast.uint32_to_uint64
let u32_64 =
Int.Cast.uint32_to_uint64
MerkleTree.Low.fst.checked
prims.fst.checked MerkleTree.Spec.fst.checked MerkleTree.New.High.fst.checked MerkleTree.Low.VectorExtras.fst.checked MerkleTree.Low.Hashfunctions.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 Lib.ByteBuffer.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Monotonic.HyperStack.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Integers.fst.checked FStar.Int.Cast.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.fst
FStar.Int.Cast.uint32_to_uint64
module MerkleTree.Low

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 U64 = FStar.UInt64

module MTH = MerkleTree.New.High
module MTS = MerkleTree.Spec

open Lib.IntTypes

open MerkleTree.Low.Datastructures
open MerkleTree.Low.Hashfunctions
open MerkleTree.Low.VectorExtras

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

type const_pointer (a:Type0) = b:CB.const_buffer a{CB.length b == 1 /\ CB.qual_of b == CB.MUTABLE}

/// Low-level Merkle tree data structure
///
// NOTE: because of a lack of 64-bit LowStar.Buffer support, currently
// we cannot change below to some other types.
type index_t = uint32_t

let uint32_32_max = 4294967295ul
inline_for_extraction
let uint32_max = 4294967295UL
let uint64_max = 18446744073709551615UL
let offset_range_limit = uint32_max
val u32_64 : a: FStar.UInt32.t -> b: FStar.UInt64.t{FStar.UInt64.v b = FStar.UInt32.v a}
a: FStar.UInt32.t -> b: FStar.UInt64.t{FStar.UInt64.v b = FStar.UInt32.v a}