val mt_get_path_step_pre (#h: HS.mem) (mtr: HH.rid) (path: const_path_p) (i: U32.t)
    : HST.ST bool pf pt
let mt_get_path_step_pre
  (#h:HS.mem)
  (mtr:HH.rid)
  (path:const_path_p)
  (i:U32.t)
: HST.ST bool pf pt
= let hash_size = MTNL.Path?.hash_size (B.index (CB.cast path) 0ul) in
  MTNL.mt_get_path_step_pre #hash_size mtr path i
val mt_get_path_step_pre (#h: HS.mem) (mtr: HH.rid) (path: const_path_p) (i: U32.t)
    : HST.ST bool pf pt
let mt_get_path_step_pre (#h: HS.mem) (mtr: HH.rid) (path: const_path_p) (i: U32.t)
    : HST.ST bool pf pt =
let hash_size = MTNL.Path?.hash_size (B.index (CB.cast path) 0ul) in
MTNL.mt_get_path_step_pre #hash_size mtr path i
MerkleTree.fsti.checked
prims.fst.checked MerkleTree.Spec.fst.checked MerkleTree.Low.Serialization.fst.checked MerkleTree.Low.Hashfunctions.fst.checked MerkleTree.Low.Datastructures.fst.checked MerkleTree.Low.fst.checked MerkleTree.EverCrypt.fsti.checked LowStar.ConstBuffer.fsti.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
MerkleTree.fsti
FStar.Monotonic.HyperStack.mem FStar.Monotonic.HyperHeap.rid MerkleTree.const_path_p FStar.UInt32.t MerkleTree.Low.mt_get_path_step_pre FStar.Ghost.hide MerkleTree.Low.Datastructures.hash_size_t Prims.bool MerkleTree.Low.__proj__Path__item__hash_size MerkleTree.Low.path LowStar.Monotonic.Buffer.index MerkleTree.path LowStar.ConstBuffer.qbuf_pre LowStar.ConstBuffer.as_qbuf LowStar.ConstBuffer.cast FStar.UInt32.__uint_to_t MerkleTree.pf MerkleTree.pt
module MerkleTree

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

module B = LowStar.Buffer
module CB = LowStar.ConstBuffer

module U32 = FStar.UInt32
module U64 = FStar.UInt64

module MTS = MerkleTree.Spec
module MTNL = MerkleTree.Low
module MTNLHF = MerkleTree.Low.Hashfunctions
module MTNLE = MerkleTree.EverCrypt
module MTNLD = MerkleTree.Low.Datastructures
module MTNLS = MerkleTree.Low.Serialization


let hash_size_t = MTNLD.hash_size_t
let offset_t = MTNL.offset_t
let index_t = MTNL.index_t
let hash #hash_size = MTNLD.hash #hash_size

type path = MTNL.path
type path_p = B.pointer path
type const_path_p = MTNL.const_pointer path

let merkle_tree = MTNL.merkle_tree
let mt_p = MTNL.mt_p
let const_mt_p = MTNL.const_mt_p

inline_for_extraction noextract
let pf = fun _ -> False
inline_for_extraction noextract
let pt = fun _ _ _ -> True

[@ (Comment "  Constructor for hashes") "c_inline"]
let mt_init_hash (hash_size:hash_size_t) (r:HST.erid): HST.ST (hash #hash_size) pf pt = MTNLHF.init_hash hash_size r

[@ (Comment "  Destructor for hashes")  "c_inline"]
let mt_free_hash (#hash_size:Ghost.erased hash_size_t) (h:hash #hash_size): HST.ST unit pf pt = MTNLHF.free_hash h


[@ (Comment "  Constructor for paths") "c_inline"]
let mt_init_path (hash_size:hash_size_t) (mtr:HH.rid) (r:HST.erid): HST.ST path_p pf pt = MTNL.init_path hash_size mtr r

[@ (Comment "  Destructor for paths") "c_inline"]
let mt_free_path (path:path_p): HST.ST unit pf pt = MTNL.free_path path

[@ (Comment "  Length of a path

  @param[in] p Path

  return The length of the path") "c_inline"]
let mt_get_path_length (mtr:HH.rid) (path:const_path_p): HST.ST U32.t pf pt = MTNL.mt_get_path_length mtr path

[@ (Comment "  Insert hash into path

  @param[in] p Path
  @param[in] hash Hash to insert") "c_inline"]
let mt_path_insert
  (#h:HS.mem)
  (#mtr:HH.rid)
  (path:path_p)
  (hash:hash #(MTNL.Path?.hash_size (B.get h path 0)))
: HST.ST unit pf pt
= let hash_size = MTNL.Path?.hash_size (B.index path 0ul) in
  MTNL.mt_path_insert #hash_size mtr path hash

inline_for_extraction
let path_hash_size (#h:HS.mem) (path:path_p) = MTNL.Path?.hash_size (B.get h path 0)
inline_for_extraction
let const_path_hash_size (#h:HS.mem) (path:const_path_p) = path_hash_size #h (CB.cast path)
inline_for_extraction
let tree_hash_size (#h:HS.mem) (mt:mt_p) = MTNL.MT?.hash_size (B.get h mt 0)
inline_for_extraction
let const_tree_hash_size (#h:HS.mem) (mt:const_mt_p) = tree_hash_size #h (CB.cast mt)

[@ (Comment "  Get step on a path

  @param[in] p Path
  @param[in] i Path step index

  return The hash at step i of p") "c_inline"]
let mt_get_path_step
  (#h:HS.mem)
  (#mtr:HH.rid)
  (path:const_path_p)
  (i:U32.t)
: HST.ST (hash #(const_path_hash_size #h path)) pf pt
= let hash_size = MTNL.Path?.hash_size (B.index (CB.cast path) 0ul) in
  MTNL.mt_get_path_step #hash_size mtr path i

[@ (Comment "  Precondition predicate for mt_get_path_step") "c_inline"]
let mt_get_path_step_pre
  (#h:HS.mem)
  (mtr:HH.rid)
  (path:const_path_p)
  (i:U32.t)
val mt_get_path_step_pre (#h: HS.mem) (mtr: HH.rid) (path: const_path_p) (i: U32.t)
    : HST.ST bool pf pt
mtr: FStar.Monotonic.HyperHeap.rid -> path: MerkleTree.const_path_p -> i: FStar.UInt32.t
  -> FStar.HyperStack.ST.ST Prims.bool