val mt_safe_elts:
  #hsz:hash_size_t ->
  h:HS.mem -> lv:uint32_t{lv <= merkle_tree_size_lg} ->
  hs:hash_vv hsz {V.size_of hs = merkle_tree_size_lg} ->
  i:index_t -> j:index_t{j >= i} ->
  GTot Type0 (decreases (32 - U32.v lv))
let rec mt_safe_elts #hsz h lv hs i j =
  if lv = merkle_tree_size_lg then true
  else (let ofs = offset_of i in
       V.size_of (V.get h hs lv) == j - ofs /\
       mt_safe_elts #hsz h (lv + 1ul) hs (i / 2ul) (j / 2ul))
val mt_safe_elts:
  #hsz:hash_size_t ->
  h:HS.mem -> lv:uint32_t{lv <= merkle_tree_size_lg} ->
  hs:hash_vv hsz {V.size_of hs = merkle_tree_size_lg} ->
  i:index_t -> j:index_t{j >= i} ->
  GTot Type0 (decreases (32 - U32.v lv))
let rec mt_safe_elts #hsz h lv hs i j =
if lv = merkle_tree_size_lg
then true
else
  (let ofs = offset_of i in
    V.size_of (V.get h hs lv) == j - ofs /\ mt_safe_elts #hsz h (lv + 1ul) hs (i / 2ul) (j / 2ul))
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
MerkleTree.Low.Datastructures.hash_size_t FStar.Monotonic.HyperStack.mem LowStar.Vector.uint32_t Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Unsigned FStar.Integers.W32 MerkleTree.Low.merkle_tree_size_lg MerkleTree.Low.Datastructures.hash_vv Prims.op_Equality LowStar.Vector.size_of MerkleTree.Low.Datastructures.hash_vec MerkleTree.Low.index_t FStar.Integers.op_Greater_Equals Prims.bool Prims.l_and Prims.eq2 FStar.UInt32.t MerkleTree.Low.Datastructures.hash LowStar.Vector.get FStar.Integers.op_Subtraction MerkleTree.Low.mt_safe_elts FStar.Integers.op_Plus FStar.UInt32.__uint_to_t FStar.Integers.op_Slash MerkleTree.Low.offset_of
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

type offset_t = uint64_t
inline_for_extraction noextract unfold let u32_64 = Int.Cast.uint32_to_uint64
inline_for_extraction noextract unfold let u64_32 = Int.Cast.uint64_to_uint32

private inline_for_extraction
let offsets_connect (x:offset_t) (y:offset_t): Tot bool = y >= x && (y - x) <= offset_range_limit

private inline_for_extraction
let split_offset (tree:offset_t) (index:offset_t{offsets_connect tree index}): Tot index_t =
  [@inline_let] let diff = U64.sub_mod index tree in
  assert (diff <= offset_range_limit);
  Int.Cast.uint64_to_uint32 diff

private inline_for_extraction
let add64_fits (x:offset_t) (i:index_t): Tot bool = uint64_max - x >= (u32_64 i)

private inline_for_extraction
let join_offset (tree:offset_t) (i:index_t{add64_fits tree i}): Tot (r:offset_t{offsets_connect tree r}) =
  U64.add tree (u32_64 i)

inline_for_extraction val merkle_tree_size_lg: uint32_t
let merkle_tree_size_lg = 32ul

// A Merkle tree `MT i j hs rhs_ok rhs` stores all necessary hashes to generate
// a Merkle path for each element from the index `i` to `j-1`.
// - Parameters
// `hs`: a 2-dim store for hashes, where `hs[0]` contains leaf hash values.
// `rhs_ok`: to check the rightmost hashes are up-to-date
// `rhs`: a store for "rightmost" hashes, manipulated only when required to
//        calculate some merkle paths that need the rightmost hashes
//        as a part of them.
// `mroot`: during the construction of `rhs` we can also calculate the Merkle
//          root of the tree. If `rhs_ok` is true then it has the up-to-date
//          root value.
noeq type merkle_tree =
| MT: hash_size:hash_size_t ->
      offset:offset_t ->
      i:index_t -> j:index_t{i <= j /\ add64_fits offset j} ->
      hs:hash_vv hash_size {V.size_of hs = merkle_tree_size_lg} ->
      rhs_ok:bool ->
      rhs:hash_vec #hash_size {V.size_of rhs = merkle_tree_size_lg} ->
      mroot:hash #hash_size ->
      hash_spec:Ghost.erased (MTS.hash_fun_t #(U32.v hash_size)) ->
      hash_fun:hash_fun_t #hash_size #hash_spec ->
      merkle_tree

type mt_p = B.pointer merkle_tree
type const_mt_p = const_pointer merkle_tree

inline_for_extraction
let merkle_tree_conditions (#hsz:Ghost.erased hash_size_t) (offset:uint64_t) (i j:uint32_t) (hs:hash_vv hsz) (rhs_ok:bool) (rhs:hash_vec #hsz) (mroot:hash #hsz): Tot bool =
  j >= i && add64_fits offset j &&
  V.size_of hs = merkle_tree_size_lg &&
  V.size_of rhs = merkle_tree_size_lg

// The maximum number of currently held elements in the tree is (2^32 - 1).
// cwinter: even when using 64-bit indices, we fail if the underlying 32-bit
// vector is full; this can be fixed if necessary.
private inline_for_extraction
val mt_not_full_nst: mtv:merkle_tree -> Tot bool
let mt_not_full_nst mtv = MT?.j mtv < uint32_32_max

val mt_not_full: HS.mem -> mt_p -> GTot bool
let mt_not_full h mt = mt_not_full_nst (B.get h mt 0)

/// (Memory) Safety

val offset_of: i:index_t -> Tot index_t
let offset_of i = if i % 2ul = 0ul then i else i - 1ul

// `mt_safe_elts` says that it is safe to access an element from `i` to `j - 1`
// at level `lv` in the Merkle tree, i.e., hs[lv][k] (i <= k < j) is a valid
// element.
inline_for_extraction noextract
val mt_safe_elts:
  #hsz:hash_size_t ->
  h:HS.mem -> lv:uint32_t{lv <= merkle_tree_size_lg} ->
  hs:hash_vv hsz {V.size_of hs = merkle_tree_size_lg} ->
  i:index_t -> j:index_t{j >= i} ->
  GTot Type0 (decreases (32 - U32.v lv))
val mt_safe_elts:
  #hsz:hash_size_t ->
  h:HS.mem -> lv:uint32_t{lv <= merkle_tree_size_lg} ->
  hs:hash_vv hsz {V.size_of hs = merkle_tree_size_lg} ->
  i:index_t -> j:index_t{j >= i} ->
  GTot Type0 (decreases (32 - U32.v lv))

    h: FStar.Monotonic.HyperStack.mem ->
    lv: LowStar.Vector.uint32_t{lv <= MerkleTree.Low.merkle_tree_size_lg} ->
    hs:
      MerkleTree.Low.Datastructures.hash_vv hsz
        {LowStar.Vector.size_of hs = MerkleTree.Low.merkle_tree_size_lg} ->
    i: MerkleTree.Low.index_t ->
    j: MerkleTree.Low.index_t{j >= i}
  -> Prims.GTot Type0