val mt_verify
      (#h: HS.mem)
      (#hash_size: Ghost.erased hash_size_t)
      (#hash_spec: MTS.hash_fun_t #(U32.v hash_size))
      (mt: const_mt_p)
      (tgt max: UInt64.t)
      (mtr: HH.rid)
      (path:
          const_path_p
            { let phs = const_path_hash_size #h path in
              phs = const_tree_hash_size #h mt /\ phs = Ghost.reveal hash_size })
      (root: hash #(const_path_hash_size #h path))
    : HST.ST bool pf pt
let mt_verify
  (#h:HS.mem)
  (#hash_size:Ghost.erased hash_size_t)
  (#hash_spec:MTS.hash_fun_t #(U32.v hash_size))
  (mt:const_mt_p)
  (tgt:UInt64.t)
  (max:UInt64.t)
  (mtr:HH.rid)
  (path:const_path_p{let phs = const_path_hash_size #h path in phs = const_tree_hash_size #h mt /\ phs = Ghost.reveal hash_size})
  (root:hash #(const_path_hash_size #h path))
: HST.ST bool pf pt
= let dmt = B.index (CB.cast mt) 0ul in
  let hsz = MTNL.MT?.hash_size dmt in
  MTNL.mt_verify #hsz #hash_spec mt tgt max mtr path root
val mt_verify
      (#h: HS.mem)
      (#hash_size: Ghost.erased hash_size_t)
      (#hash_spec: MTS.hash_fun_t #(U32.v hash_size))
      (mt: const_mt_p)
      (tgt max: UInt64.t)
      (mtr: HH.rid)
      (path:
          const_path_p
            { let phs = const_path_hash_size #h path in
              phs = const_tree_hash_size #h mt /\ phs = Ghost.reveal hash_size })
      (root: hash #(const_path_hash_size #h path))
    : HST.ST bool pf pt
let mt_verify
      (#h: HS.mem)
      (#hash_size: Ghost.erased hash_size_t)
      (#hash_spec: MTS.hash_fun_t #(U32.v hash_size))
      (mt: const_mt_p)
      (tgt max: UInt64.t)
      (mtr: HH.rid)
      (path:
          const_path_p
            { let phs = const_path_hash_size #h path in
              phs = const_tree_hash_size #h mt /\ phs = Ghost.reveal hash_size })
      (root: hash #(const_path_hash_size #h path))
    : HST.ST bool pf pt =
let dmt = B.index (CB.cast mt) 0ul in
let hsz = MTNL.MT?.hash_size dmt in
MTNL.mt_verify #hsz #hash_spec mt tgt max mtr path root
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.Ghost.erased MerkleTree.hash_size_t MerkleTree.Spec.hash_fun_t FStar.UInt32.v FStar.Ghost.reveal MerkleTree.const_mt_p FStar.UInt64.t FStar.Monotonic.HyperHeap.rid MerkleTree.const_path_p Prims.l_and Prims.b2t Prims.op_Equality MerkleTree.Low.Datastructures.hash_size_t MerkleTree.const_tree_hash_size MerkleTree.const_path_hash_size MerkleTree.hash MerkleTree.Low.mt_verify FStar.Ghost.hide Prims.bool MerkleTree.Low.__proj__MT__item__hash_size MerkleTree.Low.merkle_tree LowStar.Monotonic.Buffer.index 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)
: 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


[@ (Comment "  Construction with custom hash functions

  @param[in]  hash_size Hash size (in bytes)
  @param[in]  i         The initial hash

  return The new Merkle tree") "c_inline"]
let mt_create_custom
  (hash_size:hash_size_t)
  (hash_spec:Ghost.erased (MTS.hash_fun_t #(U32.v hash_size)))
  (r:HST.erid)
  (i:hash #hash_size)
  (hash_fun:MTNLHF.hash_fun_t #hash_size #hash_spec)
: HST.ST mt_p pf pt
= MTNL.mt_create_custom hash_size hash_spec r i hash_fun


[@ (Comment "  Destruction

  @param[in]  mt  The Merkle tree") "c_inline"]
let mt_free (mt:mt_p): HST.ST unit pf pt = MTNL.mt_free mt


[@ (Comment "  Insertion

  @param[in]  mt  The Merkle tree
  @param[in]  v   The tree does not take ownership of the hash, it makes a copy of its content.

 Note: The content of the hash will be overwritten with an arbitrary value.") "c_inline"]
let mt_insert
  (#h:HS.mem)
  (mt:mt_p)
  (v:hash #(tree_hash_size #h mt))
: HST.ST unit pf pt
= let hash_size = MTNL.MT?.hash_size (B.index mt 0ul) in
  MTNL.mt_insert hash_size mt v

[@ (Comment "  Precondition predicate for mt_insert") "c_inline"]
let mt_insert_pre
  (#h:HS.mem)
  (mt:const_mt_p)
  (v:hash #(const_tree_hash_size #h mt))
: HST.ST bool pf pt
= let hash_size = MTNL.MT?.hash_size (B.index (CB.cast mt) 0ul) in
  MTNL.mt_insert_pre #hash_size mt v


[@ (Comment "  Getting the Merkle root

  @param[in]  mt   The Merkle tree
  @param[out] root The Merkle root") "c_inline"]
let mt_get_root
  (#h:HS.mem)
  (mt:const_mt_p)
  (root:hash #(const_tree_hash_size #h mt))
: HST.ST unit pf pt
= let hash_size = MTNL.MT?.hash_size (B.index (CB.cast mt) 0ul) in
  MTNL.mt_get_root #hash_size mt root

[@ (Comment "  Precondition predicate for mt_get_root") "c_inline"]
let mt_get_root_pre
  (#h:HS.mem)
  (mt:const_mt_p)
  (root:hash #(const_tree_hash_size #h mt))
: HST.ST bool pf pt
= let hash_size = MTNL.MT?.hash_size (B.index (CB.cast mt) 0ul) in
  MTNL.mt_get_root_pre #hash_size mt root


[@ (Comment "  Getting a Merkle path

  @param[in]  mt   The Merkle tree
  @param[in]  idx  The index of the target hash
  @param[out] path A resulting Merkle path that contains the leaf hash.
  @param[out] root The Merkle root

  return The number of elements in the tree

  Notes:
  - The resulting path contains pointers to hashes in the tree, not copies of
    the hash values.
  - idx must be within the currently held indices in the tree (past the
    last flush index).") "c_inline"]
let mt_get_path
  (#h:HS.mem)
  (mt:const_mt_p)
  (idx:offset_t)
  (path:path_p{path_hash_size #h path = const_tree_hash_size #h mt})
  (root:hash #(path_hash_size #h path))
: HST.ST index_t pf pt
= let hash_size = MTNL.MT?.hash_size (B.index (CB.cast mt) 0ul) in
  MTNL.mt_get_path #hash_size mt idx path root

[@ (Comment "  Precondition predicate for mt_get_path") "c_inline"]
let mt_get_path_pre
  (#h:HS.mem)
  (mt:const_mt_p)
  (idx:offset_t)
  (path:const_path_p{const_path_hash_size #h path = const_tree_hash_size #h mt})
  (root:hash #(const_path_hash_size #h path))
: HST.ST bool pf pt
= let hash_size = MTNL.MT?.hash_size (B.index (CB.cast mt) 0ul) in
  MTNL.mt_get_path_pre #hash_size mt idx path root


[@ (Comment "  Flush the Merkle tree

  @param[in]  mt   The Merkle tree") "c_inline"]
let mt_flush (mt:mt_p): HST.ST unit pf pt = MTNL.mt_flush mt

[@ (Comment "  Precondition predicate for mt_flush") "c_inline"]
let mt_flush_pre (mt:const_mt_p): HST.ST bool pf pt = MTNL.mt_flush_pre mt


[@ (Comment "  Flush the Merkle tree up to a given index

  @param[in]  mt   The Merkle tree
  @param[in]  idx  The index up to which to flush the tree") "c_inline"]
let mt_flush_to (mt:mt_p) (idx:offset_t): HST.ST unit pf pt = MTNL.mt_flush_to mt idx

[@ (Comment "  Precondition predicate for mt_flush_to")]
let mt_flush_to_pre (mt:const_mt_p) (idx:offset_t): HST.ST bool pf pt = MTNL.mt_flush_to_pre mt idx


[@ (Comment "  Retract the Merkle tree down to a given index

  @param[in]  mt   The Merkle tree
  @param[in]  idx  The index to retract the tree to

 Note: The element and idx will remain in the tree.") "c_inline"]
let mt_retract_to (mt:mt_p) (idx:offset_t): HST.ST unit pf pt = MTNL.mt_retract_to mt idx

[@ (Comment "  Precondition predicate for mt_retract_to") "c_inline"]
let mt_retract_to_pre (mt:const_mt_p) (idx:offset_t): HST.ST bool pf pt = MTNL.mt_retract_to_pre mt idx


[@ (Comment "  Client-side verification

  @param[in]  mt   The Merkle tree
  @param[in]  tgt  The index of the target hash
  @param[in]  max  The maximum index + 1 of the tree when the path was generated
  @param[in]  path The Merkle path to verify
  @param[in]  root

  return true if the verification succeeded, false otherwise

  Note: max - tgt must be less than 2^32.") "c_inline"]
let mt_verify
  (#h:HS.mem)
  (#hash_size:Ghost.erased hash_size_t)
  (#hash_spec:MTS.hash_fun_t #(U32.v hash_size))
  (mt:const_mt_p)
  (tgt:UInt64.t)
  (max:UInt64.t)
  (mtr:HH.rid)
  (path:const_path_p{let phs = const_path_hash_size #h path in phs = const_tree_hash_size #h mt /\ phs = Ghost.reveal hash_size})
  (root:hash #(const_path_hash_size #h path))
val mt_verify
      (#h: HS.mem)
      (#hash_size: Ghost.erased hash_size_t)
      (#hash_spec: MTS.hash_fun_t #(U32.v hash_size))
      (mt: const_mt_p)
      (tgt max: UInt64.t)
      (mtr: HH.rid)
      (path:
          const_path_p
            { let phs = const_path_hash_size #h path in
              phs = const_tree_hash_size #h mt /\ phs = Ghost.reveal hash_size })
      (root: hash #(const_path_hash_size #h path))
    : HST.ST bool pf pt

    mt: MerkleTree.const_mt_p ->
    tgt: FStar.UInt64.t ->
    max: FStar.UInt64.t ->
    mtr: FStar.Monotonic.HyperHeap.rid ->
    path:
      MerkleTree.const_path_p
        { let phs = MerkleTree.const_path_hash_size path in
          phs = MerkleTree.const_tree_hash_size mt /\ phs = FStar.Ghost.reveal hash_size } ->
    root: MerkleTree.hash
  -> FStar.HyperStack.ST.ST Prims.bool