val mt_path_length_step:
  k:index_t ->
  j:index_t{k <= j} ->
  actd:bool ->
  Tot (sl:uint32_t{U32.v sl = MTH.mt_path_length_step (U32.v k) (U32.v j) actd})
let mt_path_length_step k j actd =
  if j = 0ul then 0ul
  else (if k % 2ul = 0ul
       then (if j = k || (j = k + 1ul && not actd) then 0ul else 1ul)
       else 1ul)
val mt_path_length_step:
  k:index_t ->
  j:index_t{k <= j} ->
  actd:bool ->
  Tot (sl:uint32_t{U32.v sl = MTH.mt_path_length_step (U32.v k) (U32.v j) actd})
let mt_path_length_step k j actd =
if j = 0ul
then 0ul
else (if k % 2ul = 0ul then (if j = k || (j = k + 1ul && not actd) then 0ul else 1ul) else 1ul)
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.index_t Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Unsigned FStar.Integers.W32 Prims.bool Prims.op_Equality FStar.UInt32.t FStar.UInt32.__uint_to_t FStar.Integers.op_Percent Prims.op_BarBar Prims.op_AmpAmp FStar.Integers.op_Plus Prims.op_Negation LowStar.Vector.uint32_t Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.op_GreaterThanOrEqual FStar.UInt32.v MerkleTree.New.High.mt_path_length_step
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))
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))

#push-options "--initial_fuel 1 --max_fuel 1"
val mt_safe_elts_constr:
  #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} ->
  Lemma (requires (V.size_of (V.get h hs lv) == j - offset_of i /\
                  mt_safe_elts #hsz h (lv + 1ul) hs (i / 2ul) (j / 2ul)))
        (ensures (mt_safe_elts #hsz h lv hs i j))
let mt_safe_elts_constr #_ h lv hs i j = ()

val mt_safe_elts_head:
  #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} ->
  Lemma (requires (mt_safe_elts #hsz h lv hs i j))
        (ensures (V.size_of (V.get h hs lv) == j - offset_of i))
let mt_safe_elts_head #_ h lv hs i j = ()

val mt_safe_elts_rec:
  #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} ->
  Lemma (requires (mt_safe_elts #hsz h lv hs i j))
        (ensures (mt_safe_elts #hsz h (lv + 1ul) hs (i / 2ul) (j / 2ul)))
let mt_safe_elts_rec #_ h lv hs i j = ()

val mt_safe_elts_init:
  #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} ->
  Lemma (requires (V.forall_ h hs lv (V.size_of hs)
                    (fun hv -> V.size_of hv = 0ul)))
        (ensures (mt_safe_elts #hsz h lv hs 0ul 0ul))
        (decreases (32 - U32.v lv))
let rec mt_safe_elts_init #hsz h lv hs =
  if lv = merkle_tree_size_lg then ()
  else mt_safe_elts_init #hsz h (lv + 1ul) hs
#pop-options

val mt_safe_elts_preserved:
  #hsz:hash_size_t ->
  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} ->
  p:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (V.live h0 hs /\
                  mt_safe_elts #hsz h0 lv hs i j /\
                  loc_disjoint p (V.loc_vector_within hs lv (V.size_of hs)) /\
                  modifies p h0 h1))
        (ensures (mt_safe_elts #hsz h1 lv hs i j))
        (decreases (32 - U32.v lv))
        [SMTPat (V.live h0 hs);
        SMTPat (mt_safe_elts #hsz h0 lv hs i j);
        SMTPat (loc_disjoint p (RV.loc_rvector hs));
        SMTPat (modifies p h0 h1)]
#push-options "--z3rlimit 100 --initial_fuel 2 --max_fuel 2"
let rec mt_safe_elts_preserved #hsz lv hs i j p h0 h1 =
  if lv = merkle_tree_size_lg then ()
  else (V.get_preserved hs lv p h0 h1;
       mt_safe_elts_preserved #hsz (lv + 1ul) hs (i / 2ul) (j / 2ul) p h0 h1)
#pop-options

// `mt_safe` is the invariant of a Merkle tree through its lifetime.
// It includes liveness, regionality, disjointness (to each data structure),
// and valid element access (`mt_safe_elts`).
inline_for_extraction noextract
val mt_safe: HS.mem -> mt_p -> GTot Type0
let mt_safe h mt =
  B.live h mt /\ B.freeable mt /\
  (let mtv = B.get h mt 0 in
  // Liveness & Accessibility
  RV.rv_inv h (MT?.hs mtv) /\
  RV.rv_inv h (MT?.rhs mtv) /\
  Rgl?.r_inv (hreg (MT?.hash_size mtv)) h (MT?.mroot mtv) /\
  mt_safe_elts h 0ul (MT?.hs mtv) (MT?.i mtv) (MT?.j mtv) /\
  // Regionality
  HH.extends (V.frameOf (MT?.hs mtv)) (B.frameOf mt) /\
  HH.extends (V.frameOf (MT?.rhs mtv)) (B.frameOf mt) /\
  HH.extends (B.frameOf (MT?.mroot mtv)) (B.frameOf mt) /\
  HH.disjoint (V.frameOf (MT?.hs mtv)) (V.frameOf (MT?.rhs mtv)) /\
  HH.disjoint (V.frameOf (MT?.hs mtv)) (B.frameOf (MT?.mroot mtv)) /\
  HH.disjoint (V.frameOf (MT?.rhs mtv)) (B.frameOf (MT?.mroot mtv)))

// Since a Merkle tree satisfies regionality, it's ok to take all regions from
// a tree pointer as a location of the tree.
val mt_loc: mt_p -> GTot loc
let mt_loc mt = B.loc_all_regions_from false (B.frameOf mt)

val mt_safe_preserved:
  mt:mt_p -> p:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (mt_safe h0 mt /\
                  loc_disjoint p (mt_loc mt) /\
                  modifies p h0 h1))
        (ensures (B.get h0 mt 0 == B.get h1 mt 0 /\
                 mt_safe h1 mt))
let mt_safe_preserved mt p h0 h1 =
  assert (loc_includes (mt_loc mt) (B.loc_buffer mt));
  let mtv = B.get h0 mt 0 in
  assert (loc_includes (mt_loc mt) (RV.loc_rvector (MT?.hs mtv)));
  assert (loc_includes (mt_loc mt) (RV.loc_rvector (MT?.rhs mtv)));
  assert (loc_includes (mt_loc mt) (V.loc_vector (MT?.hs mtv)));
  assert (loc_includes (mt_loc mt)
           (B.loc_all_regions_from false (B.frameOf (MT?.mroot mtv))));
  RV.rv_inv_preserved (MT?.hs mtv) p h0 h1;
  RV.rv_inv_preserved (MT?.rhs mtv) p h0 h1;
  Rgl?.r_sep (hreg (MT?.hash_size mtv)) (MT?.mroot mtv) p h0 h1;
  V.loc_vector_within_included (MT?.hs mtv) 0ul (V.size_of (MT?.hs mtv));
  mt_safe_elts_preserved 0ul (MT?.hs mtv) (MT?.i mtv) (MT?.j mtv) p h0 h1

/// Lifting to a high-level Merkle tree structure

val mt_safe_elts_spec:
  #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} ->
  Lemma (requires (RV.rv_inv h hs /\
                  mt_safe_elts #hsz h lv hs i j))
        (ensures (MTH.hs_wf_elts #(U32.v hsz)
                   (U32.v lv) (RV.as_seq h hs)
                   (U32.v i) (U32.v j)))
        (decreases (32 - U32.v lv))
#push-options "--z3rlimit 100 --initial_fuel 2 --max_fuel 2"
let rec mt_safe_elts_spec #_ h lv hs i j =
  if lv = merkle_tree_size_lg then ()
  else mt_safe_elts_spec h (lv + 1ul) hs (i / 2ul) (j / 2ul)
#pop-options

val merkle_tree_lift:
  h:HS.mem ->
  mtv:merkle_tree{
    RV.rv_inv h (MT?.hs mtv) /\
    RV.rv_inv h (MT?.rhs mtv) /\
    Rgl?.r_inv (hreg (MT?.hash_size mtv)) h (MT?.mroot mtv) /\
    mt_safe_elts #(MT?.hash_size mtv) h 0ul (MT?.hs mtv) (MT?.i mtv) (MT?.j mtv)} ->
  GTot (r:MTH.merkle_tree #(U32.v (MT?.hash_size mtv)) {MTH.mt_wf_elts #_ r})
let merkle_tree_lift h mtv =
  mt_safe_elts_spec h 0ul (MT?.hs mtv) (MT?.i mtv) (MT?.j mtv);
  MTH.MT #(U32.v (MT?.hash_size mtv))
    (U32.v (MT?.i mtv))
    (U32.v (MT?.j mtv))
    (RV.as_seq h (MT?.hs mtv))
    (MT?.rhs_ok mtv)
    (RV.as_seq h (MT?.rhs mtv))
    (Rgl?.r_repr (hreg (MT?.hash_size mtv)) h (MT?.mroot mtv))
    (Ghost.reveal (MT?.hash_spec mtv))

val mt_lift:
  h:HS.mem -> mt:mt_p{mt_safe h mt} ->
  GTot (r:MTH.merkle_tree #(U32.v (MT?.hash_size (B.get h mt 0))) {MTH.mt_wf_elts #_ r})
let mt_lift h mt =
  merkle_tree_lift h (B.get h mt 0)

val mt_preserved:
  mt:mt_p -> p:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (mt_safe h0 mt /\
                  loc_disjoint p (mt_loc mt) /\
                  modifies p h0 h1))
        (ensures (mt_safe_preserved mt p h0 h1;
                 mt_lift h0 mt == mt_lift h1 mt))
let mt_preserved mt p h0 h1 =
  assert (loc_includes (B.loc_all_regions_from false (B.frameOf mt))
                       (B.loc_buffer mt));
  B.modifies_buffer_elim mt p h0 h1;
  assert (B.get h0 mt 0 == B.get h1 mt 0);
  assert (loc_includes (B.loc_all_regions_from false (B.frameOf mt))
                       (RV.loc_rvector (MT?.hs (B.get h0 mt 0))));
  assert (loc_includes (B.loc_all_regions_from false (B.frameOf mt))
                       (RV.loc_rvector (MT?.rhs (B.get h0 mt 0))));
  assert (loc_includes (B.loc_all_regions_from false (B.frameOf mt))
                       (B.loc_buffer (MT?.mroot (B.get h0 mt 0))));
  RV.as_seq_preserved (MT?.hs (B.get h0 mt 0)) p h0 h1;
  RV.as_seq_preserved (MT?.rhs (B.get h0 mt 0)) p h0 h1;
  B.modifies_buffer_elim (MT?.mroot (B.get h0 mt 0)) p h0 h1


/// Construction

// Note that the public function for creation is `mt_create` defined below,
// which builds a tree with an initial hash.
#push-options "--z3rlimit 100 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
private
val create_empty_mt:
  hash_size:hash_size_t ->
  hash_spec:Ghost.erased (MTS.hash_fun_t #(U32.v hash_size)) ->
  hash_fun:hash_fun_t #hash_size #hash_spec ->
  r:HST.erid ->
  HST.ST mt_p
   (requires (fun _ -> true))
   (ensures (fun h0 mt h1 ->
     let dmt = B.get h1 mt 0 in
     // memory safety
     B.frameOf mt = r /\
     modifies (mt_loc mt) h0 h1 /\
     mt_safe h1 mt /\
     mt_not_full h1 mt /\
     // correctness
     MT?.hash_size dmt = hash_size /\
     MT?.offset dmt = 0UL /\
     merkle_tree_lift h1 dmt == MTH.create_empty_mt #_ #(Ghost.reveal hash_spec) ()))
let create_empty_mt hsz hash_spec hash_fun r =
  [@inline_let] let hrg = hreg hsz in
  [@inline_let] let hvrg = hvreg hsz in
  [@inline_let] let hvvrg = hvvreg hsz in
  let hs_region = HST.new_region r in
  let hs = RV.alloc_rid hvrg merkle_tree_size_lg hs_region in
  let h0 = HST.get () in
  mt_safe_elts_init #hsz h0 0ul hs;
  let rhs_region = HST.new_region r in
  let rhs = RV.alloc_rid hrg merkle_tree_size_lg rhs_region in
  let h1 = HST.get () in
  assert (RV.as_seq h1 rhs == S.create 32 (MTH.hash_init #(U32.v hsz)));
  RV.rv_inv_preserved hs (V.loc_vector rhs) h0 h1;
  RV.as_seq_preserved hs (V.loc_vector rhs) h0 h1;
  V.loc_vector_within_included hs 0ul (V.size_of hs);
  mt_safe_elts_preserved #hsz 0ul hs 0ul 0ul (V.loc_vector rhs) h0 h1;
  let mroot_region = HST.new_region r in
  let mroot = rg_alloc hrg mroot_region in
  let h2 = HST.get () in
  RV.as_seq_preserved hs loc_none h1 h2;
  RV.as_seq_preserved rhs loc_none h1 h2;
  mt_safe_elts_preserved #hsz 0ul hs 0ul 0ul loc_none h1 h2;
  let mt = B.malloc r (MT hsz 0UL 0ul 0ul hs false rhs mroot hash_spec hash_fun) 1ul in
  let h3 = HST.get () in
  RV.as_seq_preserved hs loc_none h2 h3;
  RV.as_seq_preserved rhs loc_none h2 h3;
  Rgl?.r_sep hrg mroot loc_none h2 h3;
  mt_safe_elts_preserved #hsz 0ul hs 0ul 0ul loc_none h2 h3;
  mt
#pop-options

/// Destruction (free)

val mt_free: mt:mt_p ->
  HST.ST unit
   (requires (fun h0 -> mt_safe h0 mt))
   (ensures (fun h0 _ h1 -> modifies (mt_loc mt) h0 h1))
#push-options "--z3rlimit 100"
let mt_free mt =
  let mtv = !*mt in
  RV.free (MT?.hs mtv);
  RV.free (MT?.rhs mtv);
  [@inline_let] let rg = hreg (MT?.hash_size mtv) in
  rg_free rg (MT?.mroot mtv);
  B.free mt
#pop-options

/// Insertion

private
val as_seq_sub_upd:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector #a #rst rg ->
  i:uint32_t{i < V.size_of rv} -> v:Rgl?.repr rg ->
  Lemma (requires (RV.rv_inv h rv))
        (ensures (S.equal (S.upd (RV.as_seq h rv) (U32.v i) v)
                          (S.append
                            (RV.as_seq_sub h rv 0ul i)
                            (S.cons v (RV.as_seq_sub h rv (i + 1ul) (V.size_of rv))))))
#push-options "--z3rlimit 20"
let as_seq_sub_upd #a #rst #rg h rv i v =
  Seq.Properties.slice_upd (RV.as_seq h rv) 0 (U32.v i) (U32.v i) v;
  Seq.Properties.slice_upd (RV.as_seq h rv) (U32.v i + 1) (U32.v (V.size_of rv)) (U32.v i) v;
  RV.as_seq_seq_slice rg h (V.as_seq h rv)
    0 (U32.v (V.size_of rv)) 0 (U32.v i);
  assert (S.equal (S.slice (RV.as_seq h rv) 0 (U32.v i))
                  (RV.as_seq_sub h rv 0ul i));
  RV.as_seq_seq_slice rg h (V.as_seq h rv)
    0 (U32.v (V.size_of rv)) (U32.v i + 1) (U32.v (V.size_of rv));
  assert (S.equal (S.slice (RV.as_seq h rv) (U32.v i + 1) (U32.v (V.size_of rv)))
                  (RV.as_seq_sub h rv (i + 1ul) (V.size_of rv)));
  assert (S.index (S.upd (RV.as_seq h rv) (U32.v i) v) (U32.v i) == v)
#pop-options

// `hash_vv_insert_copy` inserts a hash element at a level `lv`, by copying
// and pushing its content to `hs[lv]`. For detailed insertion procedure, see
// `insert_` and `mt_insert`.
#push-options "--z3rlimit 100 --initial_fuel 1 --max_fuel 1"
private
inline_for_extraction
val hash_vv_insert_copy:
  #hsz:hash_size_t ->
  lv:uint32_t{lv < merkle_tree_size_lg} ->
  i:Ghost.erased index_t ->
  j:index_t{
   Ghost.reveal i <= j &&
    U32.v j < pow2 (32 - U32.v lv) - 1 &&
    j < uint32_32_max} ->
  hs:hash_vv hsz {V.size_of hs = merkle_tree_size_lg} ->
  v:hash #hsz ->
  HST.ST unit
    (requires (fun h0 ->
      RV.rv_inv h0 hs /\
      Rgl?.r_inv (hreg hsz) h0 v /\
      HH.disjoint (V.frameOf hs) (B.frameOf v) /\
      mt_safe_elts #hsz h0 lv hs (Ghost.reveal i) j))
    (ensures (fun h0 _ h1 ->
      // memory safety
      modifies (loc_union
                 (RV.rs_loc_elem (hvreg hsz) (V.as_seq h0 hs) (U32.v lv))
                 (V.loc_vector_within hs lv (lv + 1ul)))
               h0 h1 /\
      RV.rv_inv h1 hs /\
      Rgl?.r_inv (hreg hsz) h1 v /\
      V.size_of (V.get h1 hs lv) == j + 1ul - offset_of (Ghost.reveal i) /\
      V.size_of (V.get h1 hs lv) == V.size_of (V.get h0 hs lv) + 1ul /\
      mt_safe_elts #hsz h1 (lv + 1ul) hs (Ghost.reveal i / 2ul) (j / 2ul) /\
      RV.rv_loc_elems h0 hs (lv + 1ul) (V.size_of hs) ==
      RV.rv_loc_elems h1 hs (lv + 1ul) (V.size_of hs) /\
      // correctness
      (mt_safe_elts_spec #hsz h0 lv hs (Ghost.reveal i) j;
      S.equal (RV.as_seq h1 hs)
      (MTH.hashess_insert
        (U32.v lv) (U32.v (Ghost.reveal i)) (U32.v j)
        (RV.as_seq h0 hs) (Rgl?.r_repr (hreg hsz) h0 v))) /\
      S.equal (S.index (RV.as_seq h1 hs) (U32.v lv))
      (S.snoc (S.index (RV.as_seq h0 hs) (U32.v lv))
      (Rgl?.r_repr (hreg hsz) h0 v))))
let hash_vv_insert_copy #hsz lv i j hs v =
  let hh0 = HST.get () in
  mt_safe_elts_rec hh0 lv hs (Ghost.reveal i) j;

  /// 1) Insert an element at the level `lv`, where the new vector is not yet
  /// connected to `hs`.
  let ihv = RV.insert_copy (hcpy hsz) (V.index hs lv) v in
  let hh1 = HST.get () in

  // 1-0) Basic disjointness conditions
  V.forall2_forall_left hh0 hs 0ul (V.size_of hs) lv
    (fun b1 b2 -> HH.disjoint (Rgl?.region_of (hvreg hsz) b1)
                              (Rgl?.region_of (hvreg hsz) b2));
  V.forall2_forall_right hh0 hs 0ul (V.size_of hs) lv
    (fun b1 b2 -> HH.disjoint (Rgl?.region_of (hvreg hsz) b1)
                              (Rgl?.region_of (hvreg hsz) b2));
  V.loc_vector_within_included hs lv (lv + 1ul);
  V.loc_vector_within_included hs (lv + 1ul) (V.size_of hs);
  V.loc_vector_within_disjoint hs lv (lv + 1ul) (lv + 1ul) (V.size_of hs);

  // 1-1) For the `modifies` postcondition.
  assert (modifies (RV.rs_loc_elem (hvreg hsz) (V.as_seq hh0 hs) (U32.v lv)) hh0 hh1);

  // 1-2) Preservation
  Rgl?.r_sep (hreg hsz) v (RV.loc_rvector (V.get hh0 hs lv)) hh0 hh1;
  RV.rv_loc_elems_preserved
    hs (lv + 1ul) (V.size_of hs)
    (RV.loc_rvector (V.get hh0 hs lv)) hh0 hh1;

  // 1-3) For `mt_safe_elts`
  assert (V.size_of ihv == j + 1ul - offset_of (Ghost.reveal i)); // head updated
  mt_safe_elts_preserved
    (lv + 1ul) hs (Ghost.reveal i / 2ul) (j / 2ul)
    (RV.loc_rvector (V.get hh0 hs lv)) hh0 hh1; // tail not yet

  // 1-4) For the `rv_inv` postcondition
  RV.rs_loc_elems_elem_disj
    (hvreg hsz) (V.as_seq hh0 hs) (V.frameOf hs)
    0 (U32.v (V.size_of hs)) 0 (U32.v lv) (U32.v lv);
  RV.rs_loc_elems_parent_disj
    (hvreg hsz) (V.as_seq hh0 hs) (V.frameOf hs)
    0 (U32.v lv);
  RV.rv_elems_inv_preserved
    hs 0ul lv (RV.loc_rvector (V.get hh0 hs lv))
    hh0 hh1;
  assert (RV.rv_elems_inv hh1 hs 0ul lv);

  RV.rs_loc_elems_elem_disj
    (hvreg hsz) (V.as_seq hh0 hs) (V.frameOf hs)
    0 (U32.v (V.size_of hs))
    (U32.v lv + 1) (U32.v (V.size_of hs))
    (U32.v lv);
  RV.rs_loc_elems_parent_disj
    (hvreg hsz) (V.as_seq hh0 hs) (V.frameOf hs)
    (U32.v lv + 1) (U32.v (V.size_of hs));
  RV.rv_elems_inv_preserved
    hs (lv + 1ul) (V.size_of hs) (RV.loc_rvector (V.get hh0 hs lv))
    hh0 hh1;
  assert (RV.rv_elems_inv hh1 hs (lv + 1ul) (V.size_of hs));

  // assert (rv_itself_inv hh1 hs);
  // assert (elems_reg hh1 hs);

  // 1-5) Correctness
  assert (S.equal (RV.as_seq hh1 ihv)
                  (S.snoc (RV.as_seq hh0 (V.get hh0 hs lv)) (Rgl?.r_repr (hreg hsz) hh0 v)));

  /// 2) Assign the updated vector to `hs` at the level `lv`.
  RV.assign hs lv ihv;
  let hh2 = HST.get () in

  // 2-1) For the `modifies` postcondition.
  assert (modifies (V.loc_vector_within hs lv (lv + 1ul)) hh1 hh2);
  assert (modifies (loc_union
                     (RV.rs_loc_elem (hvreg hsz) (V.as_seq hh0 hs) (U32.v lv))
                     (V.loc_vector_within hs lv (lv + 1ul))) hh0 hh2);

  // 2-2) Preservation
  Rgl?.r_sep (hreg hsz) v (RV.loc_rvector hs) hh1 hh2;
  RV.rv_loc_elems_preserved
    hs (lv + 1ul) (V.size_of hs)
    (V.loc_vector_within hs lv (lv + 1ul)) hh1 hh2;

  // 2-3) For `mt_safe_elts`
  assert (V.size_of (V.get hh2 hs lv) == j + 1ul - offset_of (Ghost.reveal i));
  mt_safe_elts_preserved
    (lv + 1ul) hs (Ghost.reveal i / 2ul) (j / 2ul)
    (V.loc_vector_within hs lv (lv + 1ul)) hh1 hh2;

  // 2-4) Correctness
  RV.as_seq_sub_preserved hs 0ul lv (loc_rvector ihv) hh0 hh1;
  RV.as_seq_sub_preserved hs (lv + 1ul) merkle_tree_size_lg (loc_rvector ihv) hh0 hh1;
  assert (S.equal (RV.as_seq hh2 hs)
                  (S.append
                    (RV.as_seq_sub hh0 hs 0ul lv)
                    (S.cons (RV.as_seq hh1 ihv)
                            (RV.as_seq_sub hh0 hs (lv + 1ul) merkle_tree_size_lg))));
  as_seq_sub_upd hh0 hs lv (RV.as_seq hh1 ihv)
#pop-options

private
val insert_index_helper_even:
  lv:uint32_t{lv < merkle_tree_size_lg} ->
  j:index_t{U32.v j < pow2 (32 - U32.v lv) - 1} ->
  Lemma (requires (j % 2ul <> 1ul))
        (ensures (U32.v j % 2 <> 1 /\ j / 2ul == (j + 1ul) / 2ul))
let insert_index_helper_even lv j = ()

#push-options "--z3rlimit 100 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
private
val insert_index_helper_odd:
  lv:uint32_t{lv < merkle_tree_size_lg} ->
  i:index_t ->
  j:index_t{i <= j && U32.v j < pow2 (32 - U32.v lv) - 1} ->
  Lemma (requires (j % 2ul = 1ul /\
                  j < uint32_32_max))
        (ensures (U32.v j % 2 = 1 /\
                 U32.v (j / 2ul) < pow2 (32 - U32.v (lv + 1ul)) - 1 /\
                 (j + 1ul) / 2ul == j / 2ul + 1ul /\
                 j - offset_of i > 0ul))
let insert_index_helper_odd lv i j = ()
#pop-options

private
val loc_union_assoc_4:
  a:loc -> b:loc -> c:loc -> d:loc ->
  Lemma (loc_union (loc_union a b) (loc_union c d) ==
        loc_union (loc_union a c) (loc_union b d))
let loc_union_assoc_4 a b c d =
  loc_union_assoc (loc_union a b) c d;
  loc_union_assoc a b c;
  loc_union_assoc a c b;
  loc_union_assoc (loc_union a c) b d

private
val insert_modifies_rec_helper:
  #hsz:hash_size_t ->
  lv:uint32_t{lv < merkle_tree_size_lg} ->
  hs:hash_vv hsz {V.size_of hs = merkle_tree_size_lg} ->
  aloc:loc ->
  h:HS.mem ->
  Lemma (loc_union
          (loc_union
            (loc_union
              (RV.rs_loc_elem (hvreg hsz) (V.as_seq h hs) (U32.v lv))
              (V.loc_vector_within hs lv (lv + 1ul)))
            aloc)
          (loc_union
            (loc_union
              (RV.rv_loc_elems h hs (lv + 1ul) (V.size_of hs))
              (V.loc_vector_within hs (lv + 1ul) (V.size_of hs)))
            aloc) ==
          loc_union
            (loc_union
              (RV.rv_loc_elems h hs lv (V.size_of hs))
              (V.loc_vector_within hs lv (V.size_of hs)))
            aloc)
#push-options "--z3rlimit 100 --initial_fuel 2 --max_fuel 2"
let insert_modifies_rec_helper #hsz lv hs aloc h =
  assert (V.loc_vector_within hs lv (V.size_of hs) ==
         loc_union (V.loc_vector_within hs lv (lv + 1ul))
                   (V.loc_vector_within hs (lv + 1ul) (V.size_of hs)));
  RV.rs_loc_elems_rec_inverse (hvreg hsz) (V.as_seq h hs) (U32.v lv) (U32.v (V.size_of hs));
  assert (RV.rv_loc_elems h hs lv (V.size_of hs) ==
         loc_union (RV.rs_loc_elem (hvreg hsz) (V.as_seq h hs) (U32.v lv))
                   (RV.rv_loc_elems h hs (lv + 1ul) (V.size_of hs)));

  // Applying some association rules...
  loc_union_assoc
    (loc_union
      (RV.rs_loc_elem (hvreg hsz) (V.as_seq h hs) (U32.v lv))
      (V.loc_vector_within hs lv (lv + 1ul))) aloc
    (loc_union
      (loc_union
        (RV.rv_loc_elems h hs (lv + 1ul) (V.size_of hs))
        (V.loc_vector_within hs (lv + 1ul) (V.size_of hs)))
      aloc);
  loc_union_assoc
    (loc_union
      (RV.rv_loc_elems h hs (lv + 1ul) (V.size_of hs))
      (V.loc_vector_within hs (lv + 1ul) (V.size_of hs))) aloc aloc;
  loc_union_assoc
    (loc_union
      (RV.rs_loc_elem (hvreg hsz) (V.as_seq h hs) (U32.v lv))
      (V.loc_vector_within hs lv (lv + 1ul)))
    (loc_union
      (RV.rv_loc_elems h hs (lv + 1ul) (V.size_of hs))
      (V.loc_vector_within hs (lv + 1ul) (V.size_of hs)))
    aloc;
  loc_union_assoc_4
    (RV.rs_loc_elem (hvreg hsz) (V.as_seq h hs) (U32.v lv))
    (V.loc_vector_within hs lv (lv + 1ul))
    (RV.rv_loc_elems h hs (lv + 1ul) (V.size_of hs))
    (V.loc_vector_within hs (lv + 1ul) (V.size_of hs))
#pop-options

private
val insert_modifies_union_loc_weakening:
  l1:loc -> l2:loc -> l3:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (modifies l1 h0 h1))
        (ensures (modifies (loc_union (loc_union l1 l2) l3) h0 h1))
let insert_modifies_union_loc_weakening l1 l2 l3 h0 h1 =
  B.loc_includes_union_l l1 l2 l1;
  B.loc_includes_union_l (loc_union l1 l2) l3 (loc_union l1 l2)

private
val insert_snoc_last_helper:
  #a:Type -> s:S.seq a{S.length s > 0} -> v:a ->
  Lemma (S.index (S.snoc s v) (S.length s - 1) == S.last s)
let insert_snoc_last_helper #a s v = ()

private
val rv_inv_rv_elems_reg:
  #a:Type0 -> #rst:Type -> #rg:regional rst a ->
  h:HS.mem -> rv:rvector rg ->
  i:uint32_t -> j:uint32_t{i <= j && j <= V.size_of rv} ->
  Lemma (requires (RV.rv_inv h rv))
        (ensures (RV.rv_elems_reg h rv i j))
let rv_inv_rv_elems_reg #a #rst #rg h rv i j = ()

// `insert_` recursively inserts proper hashes to each level `lv` by
// accumulating a compressed hash. For example, if there are three leaf elements
// in the tree, `insert_` will change `hs` as follow:
// (`hij` is a compressed hash from `hi` to `hj`)
//
//     BEFORE INSERTION        AFTER INSERTION
// lv
// 0   h0  h1  h2       ====>  h0  h1  h2  h3
// 1   h01                     h01 h23
// 2                           h03
//
private
val insert_:
  #hsz:hash_size_t ->
  #hash_spec:Ghost.erased (MTS.hash_fun_t #(U32.v hsz)) ->
  lv:uint32_t{lv < merkle_tree_size_lg} ->
  i:Ghost.erased index_t ->
  j:index_t{
    Ghost.reveal i <= j &&
    U32.v j < pow2 (32 - U32.v lv) - 1 &&
    j < uint32_32_max} ->
  hs:hash_vv hsz {V.size_of hs = merkle_tree_size_lg} ->
  acc:hash #hsz ->
  hash_fun:hash_fun_t #hsz #hash_spec ->
  HST.ST unit
         (requires (fun h0 ->
           RV.rv_inv h0 hs /\
           Rgl?.r_inv (hreg hsz) h0 acc /\
           HH.disjoint (V.frameOf hs) (B.frameOf acc) /\
           mt_safe_elts h0 lv hs (Ghost.reveal i) j))
         (ensures (fun h0 _ h1 ->
           // memory safety
           modifies (loc_union
                      (loc_union
                        (RV.rv_loc_elems h0 hs lv (V.size_of hs))
                        (V.loc_vector_within hs lv (V.size_of hs)))
                      (B.loc_all_regions_from false (B.frameOf acc)))
                    h0 h1 /\
           RV.rv_inv h1 hs /\
           Rgl?.r_inv (hreg hsz) h1 acc /\
           mt_safe_elts h1 lv hs (Ghost.reveal i) (j + 1ul) /\
           // correctness
           (mt_safe_elts_spec h0 lv hs (Ghost.reveal i) j;
           S.equal (RV.as_seq h1 hs)
                   (MTH.insert_ #(U32.v hsz) #hash_spec (U32.v lv) (U32.v (Ghost.reveal i)) (U32.v j)
                     (RV.as_seq h0 hs) (Rgl?.r_repr (hreg hsz) h0 acc)))))
         (decreases (U32.v j))
#push-options "--z3rlimit 800 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
let rec insert_ #hsz #hash_spec lv i j hs acc hash_fun =
  let hh0 = HST.get () in
  hash_vv_insert_copy lv i j hs acc;
  let hh1 = HST.get () in

  // Base conditions
  V.loc_vector_within_included hs lv (lv + 1ul);
  V.loc_vector_within_included hs (lv + 1ul) (V.size_of hs);
  V.loc_vector_within_disjoint hs lv (lv + 1ul) (lv + 1ul) (V.size_of hs);

  assert (V.size_of (V.get hh1 hs lv) == j + 1ul - offset_of (Ghost.reveal i));
  assert (mt_safe_elts hh1 (lv + 1ul) hs (Ghost.reveal i / 2ul) (j / 2ul));

  if j % 2ul = 1ul
  then (insert_index_helper_odd lv (Ghost.reveal i) j;
       assert (S.length (S.index (RV.as_seq hh0 hs) (U32.v lv)) > 0);
       let lvhs = V.index hs lv in
       assert (U32.v (V.size_of lvhs) ==
              S.length (S.index (RV.as_seq hh0 hs) (U32.v lv)) + 1);
       assert (V.size_of lvhs > 1ul);

       /// 3) Update the accumulator `acc`.
       hash_vec_rv_inv_r_inv hh1 (V.get hh1 hs lv) (V.size_of (V.get hh1 hs lv) - 2ul);
       assert (Rgl?.r_inv (hreg hsz) hh1 acc);
       hash_fun (V.index lvhs (V.size_of lvhs - 2ul)) acc acc;
       let hh2 = HST.get () in

       // 3-1) For the `modifies` postcondition
       assert (modifies (B.loc_all_regions_from false (B.frameOf acc)) hh1 hh2);
       assert (modifies
                (loc_union
                  (loc_union
                    (RV.rs_loc_elem (hvreg hsz) (V.as_seq hh0 hs) (U32.v lv))
                    (V.loc_vector_within hs lv (lv + 1ul)))
                  (B.loc_all_regions_from false (B.frameOf acc)))
                hh0 hh2);

       // 3-2) Preservation
       RV.rv_inv_preserved
         hs (B.loc_region_only false (B.frameOf acc)) hh1 hh2;
       RV.as_seq_preserved
         hs (B.loc_region_only false (B.frameOf acc)) hh1 hh2;
       RV.rv_loc_elems_preserved
         hs (lv + 1ul) (V.size_of hs)
         (B.loc_region_only false (B.frameOf acc)) hh1 hh2;
       assert (RV.rv_inv hh2 hs);
       assert (Rgl?.r_inv (hreg hsz) hh2 acc);

       // 3-3) For `mt_safe_elts`
       V.get_preserved hs lv
         (B.loc_region_only false (B.frameOf acc)) hh1 hh2; // head preserved
       mt_safe_elts_preserved
         (lv + 1ul) hs (Ghost.reveal i / 2ul) (j / 2ul)
         (B.loc_region_only false (B.frameOf acc)) hh1 hh2; // tail preserved

       // 3-4) Correctness
       insert_snoc_last_helper
         (RV.as_seq hh0 (V.get hh0 hs lv))
         (Rgl?.r_repr (hreg hsz) hh0 acc);
       assert (S.equal (Rgl?.r_repr (hreg hsz) hh2 acc) // `nacc` in `MTH.insert_`
                       ((Ghost.reveal hash_spec)
                         (S.last (S.index (RV.as_seq hh0 hs) (U32.v lv)))
                         (Rgl?.r_repr (hreg hsz) hh0 acc)));

       /// 4) Recursion
       insert_ (lv + 1ul)
         (Ghost.hide (Ghost.reveal i / 2ul)) (j / 2ul)
         hs acc hash_fun;
       let hh3 = HST.get () in

       // 4-0) Memory safety brought from the postcondition of the recursion
       assert (RV.rv_inv hh3 hs);
       assert (Rgl?.r_inv (hreg hsz) hh3 acc);
       assert (modifies (loc_union
                          (loc_union
                            (RV.rv_loc_elems hh0 hs (lv + 1ul) (V.size_of hs))
                            (V.loc_vector_within hs (lv + 1ul) (V.size_of hs)))
                          (B.loc_all_regions_from false (B.frameOf acc)))
                        hh2 hh3);
       assert (modifies
                (loc_union
                  (loc_union
                    (loc_union
                      (RV.rs_loc_elem (hvreg hsz) (V.as_seq hh0 hs) (U32.v lv))
                      (V.loc_vector_within hs lv (lv + 1ul)))
                    (B.loc_all_regions_from false (B.frameOf acc)))
                  (loc_union
                    (loc_union
                      (RV.rv_loc_elems hh0 hs (lv + 1ul) (V.size_of hs))
                      (V.loc_vector_within hs (lv + 1ul) (V.size_of hs)))
                    (B.loc_all_regions_from false (B.frameOf acc))))
                hh0 hh3);

       // 4-1) For `mt_safe_elts`
       rv_inv_rv_elems_reg hh2 hs (lv + 1ul) (V.size_of hs);
       RV.rv_loc_elems_included hh2 hs (lv + 1ul) (V.size_of hs);
       assert (loc_disjoint
                (V.loc_vector_within hs lv (lv + 1ul))
                (RV.rv_loc_elems hh2 hs (lv + 1ul) (V.size_of hs)));
       assert (loc_disjoint
                (V.loc_vector_within hs lv (lv + 1ul))
                (B.loc_all_regions_from false (B.frameOf acc)));
       V.get_preserved hs lv
         (loc_union
           (loc_union
             (V.loc_vector_within hs (lv + 1ul) (V.size_of hs))
             (RV.rv_loc_elems hh2 hs (lv + 1ul) (V.size_of hs)))
           (B.loc_all_regions_from false (B.frameOf acc)))
         hh2 hh3;

       assert (V.size_of (V.get hh3 hs lv) ==
              j + 1ul - offset_of (Ghost.reveal i)); // head preserved
       assert (mt_safe_elts hh3 (lv + 1ul) hs
                (Ghost.reveal i / 2ul) (j / 2ul + 1ul)); // tail by recursion
       mt_safe_elts_constr hh3 lv hs (Ghost.reveal i) (j + 1ul);
       assert (mt_safe_elts hh3 lv hs (Ghost.reveal i) (j + 1ul));

       // 4-2) Correctness
       mt_safe_elts_spec hh2 (lv + 1ul) hs (Ghost.reveal i / 2ul) (j / 2ul);
       assert (S.equal (RV.as_seq hh3 hs)
       (MTH.insert_ #(U32.v hsz) #(Ghost.reveal hash_spec) (U32.v lv + 1) (U32.v (Ghost.reveal i) / 2) (U32.v j / 2)
         (RV.as_seq hh2 hs) (Rgl?.r_repr (hreg hsz) hh2 acc)));
       mt_safe_elts_spec hh0 lv hs (Ghost.reveal i) j;
       MTH.insert_rec #(U32.v hsz) #(Ghost.reveal hash_spec) (U32.v lv) (U32.v (Ghost.reveal i)) (U32.v j)
         (RV.as_seq hh0 hs) (Rgl?.r_repr (hreg hsz) hh0 acc);
       assert (S.equal (RV.as_seq hh3 hs)
       (MTH.insert_ #(U32.v hsz) #(Ghost.reveal hash_spec) (U32.v lv) (U32.v (Ghost.reveal i)) (U32.v j)
         (RV.as_seq hh0 hs) (Rgl?.r_repr (hreg hsz) hh0 acc))))
  else (insert_index_helper_even lv j;
       // memory safety
       assert (mt_safe_elts hh1 (lv + 1ul) hs (Ghost.reveal i / 2ul) ((j + 1ul) / 2ul));
       mt_safe_elts_constr hh1 lv hs (Ghost.reveal i) (j + 1ul);
       assert (mt_safe_elts hh1 lv hs (Ghost.reveal i) (j + 1ul));
       assert (modifies
                (loc_union
                  (RV.rs_loc_elem (hvreg hsz) (V.as_seq hh0 hs) (U32.v lv))
                  (V.loc_vector_within hs lv (lv + 1ul)))
                hh0 hh1);
       insert_modifies_union_loc_weakening
         (loc_union
           (RV.rs_loc_elem (hvreg hsz) (V.as_seq hh0 hs) (U32.v lv))
           (V.loc_vector_within hs lv (lv + 1ul)))
         (B.loc_all_regions_from false (B.frameOf acc))
         (loc_union
           (loc_union
             (RV.rv_loc_elems hh0 hs (lv + 1ul) (V.size_of hs))
             (V.loc_vector_within hs (lv + 1ul) (V.size_of hs)))
           (B.loc_all_regions_from false (B.frameOf acc)))
         hh0 hh1;
       // correctness
       mt_safe_elts_spec hh0 lv hs (Ghost.reveal i) j;
       MTH.insert_base #(U32.v hsz) #(Ghost.reveal hash_spec) (U32.v lv) (U32.v (Ghost.reveal i)) (U32.v j)
         (RV.as_seq hh0 hs) (Rgl?.r_repr (hreg hsz) hh0 acc);
       assert (S.equal (RV.as_seq hh1 hs)
              (MTH.insert_ #(U32.v hsz) #(Ghost.reveal hash_spec) (U32.v lv) (U32.v (Ghost.reveal i)) (U32.v j)
                (RV.as_seq hh0 hs) (Rgl?.r_repr (hreg hsz) hh0 acc))));

  /// 5) Proving the postcondition after recursion
  let hh4 = HST.get () in

  // 5-1) For the `modifies` postcondition.
  assert (modifies
           (loc_union
             (loc_union
               (loc_union
                 (RV.rs_loc_elem (hvreg hsz) (V.as_seq hh0 hs) (U32.v lv))
                 (V.loc_vector_within hs lv (lv + 1ul)))
               (B.loc_all_regions_from false (B.frameOf acc)))
             (loc_union
               (loc_union
                 (RV.rv_loc_elems hh0 hs (lv + 1ul) (V.size_of hs))
                 (V.loc_vector_within hs (lv + 1ul) (V.size_of hs)))
               (B.loc_all_regions_from false (B.frameOf acc))))
           hh0 hh4);
  insert_modifies_rec_helper
    lv hs (B.loc_all_regions_from false (B.frameOf acc)) hh0;

  // 5-2) For `mt_safe_elts`
  assert (mt_safe_elts hh4 lv hs (Ghost.reveal i) (j + 1ul));

  // 5-3) Preservation
  assert (RV.rv_inv hh4 hs);
  assert (Rgl?.r_inv (hreg hsz) hh4 acc);

  // 5-4) Correctness
  mt_safe_elts_spec hh0 lv hs (Ghost.reveal i) j;
  assert (S.equal (RV.as_seq hh4 hs)
                  (MTH.insert_ #(U32.v hsz) #hash_spec (U32.v lv) (U32.v (Ghost.reveal i)) (U32.v j)
                    (RV.as_seq hh0 hs) (Rgl?.r_repr (hreg hsz) hh0 acc))) // QED
#pop-options

private inline_for_extraction
val mt_insert_pre_nst: mtv:merkle_tree -> v:hash #(MT?.hash_size mtv) -> Tot bool
let mt_insert_pre_nst mtv v = mt_not_full_nst mtv && add64_fits (MT?.offset mtv) ((MT?.j mtv) + 1ul)

val mt_insert_pre: #hsz:Ghost.erased hash_size_t -> mt:const_mt_p -> v:hash #hsz -> HST.ST bool
  (requires (fun h0 -> mt_safe h0 (CB.cast mt) /\ (MT?.hash_size (B.get h0 (CB.cast mt) 0)) = Ghost.reveal hsz))
  (ensures (fun _ _ _ -> True))
let mt_insert_pre #hsz mt v =
  let mt = !*(CB.cast mt) in
  assert (MT?.hash_size mt == (MT?.hash_size mt));
  mt_insert_pre_nst mt v

// `mt_insert` inserts a hash to a Merkle tree. Note that this operation
// manipulates the content in `v`, since it uses `v` as an accumulator during
// insertion.
#push-options "--z3rlimit 100 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
val mt_insert:
  hsz:Ghost.erased hash_size_t ->
  mt:mt_p -> v:hash #hsz ->
  HST.ST unit
   (requires (fun h0 ->
     let dmt = B.get h0 mt 0 in
     mt_safe h0 mt /\
     Rgl?.r_inv (hreg hsz) h0 v /\
     HH.disjoint (B.frameOf mt) (B.frameOf v) /\
     MT?.hash_size dmt = Ghost.reveal hsz /\
     mt_insert_pre_nst dmt v))
   (ensures (fun h0 _ h1 ->
     // memory safety
     modifies (loc_union
                (mt_loc mt)
                (B.loc_all_regions_from false (B.frameOf v)))
              h0 h1 /\
     mt_safe h1 mt /\
     // correctness
     MT?.hash_size (B.get h1 mt 0) = Ghost.reveal hsz /\
     mt_lift h1 mt == MTH.mt_insert (mt_lift h0 mt) (Rgl?.r_repr (hreg hsz) h0 v)))
#pop-options
#push-options "--z3rlimit 40"
let mt_insert hsz mt v =
  let hh0 = HST.get () in
  let mtv = !*mt in
  let hs = MT?.hs mtv in
  let hsz = MT?.hash_size mtv in
  insert_ #hsz #(Ghost.reveal (MT?.hash_spec mtv)) 0ul (Ghost.hide (MT?.i mtv)) (MT?.j mtv) hs v (MT?.hash_fun mtv);
  let hh1 = HST.get () in
  RV.rv_loc_elems_included hh0 (MT?.hs mtv) 0ul (V.size_of hs);
  V.loc_vector_within_included hs 0ul (V.size_of hs);
  RV.rv_inv_preserved
    (MT?.rhs mtv)
    (loc_union
      (loc_union
        (RV.rv_loc_elems hh0 hs 0ul (V.size_of hs))
        (V.loc_vector_within hs 0ul (V.size_of hs)))
      (B.loc_all_regions_from false (B.frameOf v)))
    hh0 hh1;
  RV.as_seq_preserved
    (MT?.rhs mtv)
    (loc_union
      (loc_union
        (RV.rv_loc_elems hh0 hs 0ul (V.size_of hs))
        (V.loc_vector_within hs 0ul (V.size_of hs)))
      (B.loc_all_regions_from false (B.frameOf v)))
    hh0 hh1;
  Rgl?.r_sep (hreg hsz) (MT?.mroot mtv)
    (loc_union
      (loc_union
        (RV.rv_loc_elems hh0 hs 0ul (V.size_of hs))
        (V.loc_vector_within hs 0ul (V.size_of hs)))
      (B.loc_all_regions_from false (B.frameOf v)))
    hh0 hh1;
  mt *= MT (MT?.hash_size mtv)
           (MT?.offset mtv)
           (MT?.i mtv)
           (MT?.j mtv + 1ul)
           (MT?.hs mtv)
           false // `rhs` is always deprecated right after an insertion.
           (MT?.rhs mtv)
           (MT?.mroot mtv)
           (MT?.hash_spec mtv)
           (MT?.hash_fun mtv);
  let hh2 = HST.get () in
  RV.rv_inv_preserved
    (MT?.hs mtv) (B.loc_buffer mt) hh1 hh2;
  RV.rv_inv_preserved
    (MT?.rhs mtv) (B.loc_buffer mt) hh1 hh2;
  RV.as_seq_preserved
    (MT?.hs mtv) (B.loc_buffer mt) hh1 hh2;
  RV.as_seq_preserved
    (MT?.rhs mtv) (B.loc_buffer mt) hh1 hh2;
  Rgl?.r_sep (hreg hsz) (MT?.mroot mtv) (B.loc_buffer mt) hh1 hh2;
  mt_safe_elts_preserved
    0ul (MT?.hs mtv) (MT?.i mtv) (MT?.j mtv + 1ul) (B.loc_buffer mt)
    hh1 hh2
#pop-options

// `mt_create` initiates a Merkle tree with a given initial hash `init`.
// A valid Merkle tree should contain at least one element.
val mt_create_custom:
  hsz:hash_size_t ->
  hash_spec:Ghost.erased (MTS.hash_fun_t #(U32.v hsz)) ->
  r:HST.erid -> init:hash #hsz -> hash_fun:hash_fun_t #hsz #hash_spec -> HST.ST mt_p
   (requires (fun h0 ->
     Rgl?.r_inv (hreg hsz) h0 init /\
     HH.disjoint r (B.frameOf init)))
   (ensures (fun h0 mt h1 ->
     // memory safety
     modifies (loc_union (mt_loc mt) (B.loc_all_regions_from false (B.frameOf init))) h0 h1 /\
     mt_safe h1 mt /\
     // correctness
     MT?.hash_size (B.get h1 mt 0) = hsz /\
     mt_lift h1 mt == MTH.mt_create (U32.v hsz) (Ghost.reveal hash_spec) (Rgl?.r_repr (hreg hsz) h0 init)))
#push-options "--z3rlimit 40"
let mt_create_custom hsz hash_spec r init hash_fun =
  let hh0 = HST.get () in
  let mt = create_empty_mt hsz hash_spec hash_fun r in
  mt_insert hsz mt init;
  let hh2 = HST.get () in
  mt
#pop-options

/// Construction and Destruction of paths

// Since each element pointer in `path` is from the target Merkle tree and
// each element has different location in `MT?.hs` (thus different region id),
// we cannot use the regionality property for `path`s. Hence here we manually
// define invariants and representation.
noeq type path =
| Path: hash_size:hash_size_t ->
        hashes:V.vector (hash #hash_size) ->
        path
type path_p = B.pointer path
type const_path_p = const_pointer path

private
let phashes (h:HS.mem) (p:path_p)
: GTot (V.vector (hash #(Path?.hash_size (B.get h p 0)))) 
= Path?.hashes (B.get h p 0)

// Memory safety of a path as an invariant
inline_for_extraction noextract
val path_safe:
  h:HS.mem -> mtr:HH.rid -> p:path_p -> GTot Type0
let path_safe h mtr p =
  B.live h p /\ B.freeable p /\
  V.live h (phashes h p) /\ V.freeable (phashes h p) /\
  HST.is_eternal_region (V.frameOf (phashes h p)) /\
  (let hsz = Path?.hash_size (B.get h p 0) in
  V.forall_all h (phashes h p)
    (fun hp -> Rgl?.r_inv (hreg hsz) h hp /\
               HH.includes mtr (Rgl?.region_of (hreg hsz) hp)) /\
  HH.extends (V.frameOf (phashes h p)) (B.frameOf p) /\
  HH.disjoint mtr (B.frameOf p))

val path_loc: path_p -> GTot loc
let path_loc p = B.loc_all_regions_from false (B.frameOf p)

val lift_path_:
  #hsz:hash_size_t ->
  h:HS.mem ->
  hs:S.seq (hash #hsz) ->
  i:nat ->
  j:nat{
    i <= j /\ j <= S.length hs /\
    V.forall_seq hs i j (fun hp -> Rgl?.r_inv (hreg hsz) h hp)} ->
  GTot (hp:MTH.path #(U32.v hsz) {S.length hp = j - i}) (decreases j)
let rec lift_path_ #hsz h hs i j =
  if i = j then S.empty
  else (S.snoc (lift_path_ h hs i (j - 1))
               (Rgl?.r_repr (hreg hsz) h (S.index hs (j - 1))))

// Representation of a path
val lift_path:
  #hsz:hash_size_t ->
  h:HS.mem -> mtr:HH.rid -> p:path_p {path_safe h mtr p /\ (Path?.hash_size (B.get h p 0)) = hsz} ->
  GTot (hp:MTH.path #(U32.v hsz) {S.length hp = U32.v (V.size_of (phashes h p))})
let lift_path #hsz h mtr p =
  lift_path_ h (V.as_seq h (phashes h p))
    0 (S.length (V.as_seq h (phashes h p)))

val lift_path_index_:
  #hsz:hash_size_t ->
  h:HS.mem ->
  hs:S.seq (hash #hsz) ->
  i:nat -> j:nat{i <= j && j <= S.length hs} ->
  k:nat{i <= k && k < j} ->
  Lemma (requires (V.forall_seq hs i j (fun hp -> Rgl?.r_inv (hreg hsz) h hp)))
        (ensures (Rgl?.r_repr (hreg hsz) h (S.index hs k) ==
                 S.index (lift_path_ h hs i j) (k - i)))
        (decreases j)
        [SMTPat (S.index (lift_path_ h hs i j) (k - i))]
#push-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
let rec lift_path_index_ #hsz h hs i j k =
  if i = j then ()
  else if k = j - 1 then ()
  else lift_path_index_ #hsz h hs i (j - 1) k
#pop-options

val lift_path_index:
  h:HS.mem -> mtr:HH.rid ->
  p:path_p -> i:uint32_t ->
  Lemma (requires (path_safe h mtr p /\
                  i < V.size_of (phashes h p)))
        (ensures (let hsz = Path?.hash_size (B.get h p 0) in
                 Rgl?.r_repr (hreg hsz) h (V.get h (phashes h p) i) ==
                 S.index (lift_path #(hsz) h mtr p) (U32.v i)))
let lift_path_index h mtr p i =
  lift_path_index_ h (V.as_seq h (phashes h p))
    0 (S.length (V.as_seq h (phashes h p))) (U32.v i)

val lift_path_eq:
  #hsz:hash_size_t ->
  h:HS.mem ->
  hs1:S.seq (hash #hsz) -> hs2:S.seq (hash #hsz) ->
  i:nat -> j:nat ->
  Lemma (requires (i <= j /\ j <= S.length hs1 /\ j <= S.length hs2 /\
                  S.equal (S.slice hs1 i j) (S.slice hs2 i j) /\
                  V.forall_seq hs1 i j (fun hp -> Rgl?.r_inv (hreg hsz) h hp) /\
                  V.forall_seq hs2 i j (fun hp -> Rgl?.r_inv (hreg hsz) h hp)))
        (ensures (S.equal (lift_path_ h hs1 i j) (lift_path_ h hs2 i j)))
let lift_path_eq #hsz h hs1 hs2 i j =
  assert (forall (k:nat{i <= k && k < j}).
           S.index (lift_path_ h hs1 i j) (k - i) ==
           Rgl?.r_repr (hreg hsz) h (S.index hs1 k));
  assert (forall (k:nat{i <= k && k < j}).
           S.index (lift_path_ h hs2 i j) (k - i) ==
           Rgl?.r_repr (hreg hsz) h (S.index hs2 k));
  assert (forall (k:nat{k < j - i}).
           S.index (lift_path_ h hs1 i j) k ==
           Rgl?.r_repr (hreg hsz) h (S.index hs1 (k + i)));
  assert (forall (k:nat{k < j - i}).
           S.index (lift_path_ h hs2 i j) k ==
           Rgl?.r_repr (hreg hsz) h (S.index hs2 (k + i)));
  assert (forall (k:nat{k < j - i}).
           S.index (S.slice hs1 i j) k == S.index (S.slice hs2 i j) k);
  assert (forall (k:nat{i <= k && k < j}).
           S.index (S.slice hs1 i j) (k - i) == S.index (S.slice hs2 i j) (k - i))

private
val path_safe_preserved_:
  #hsz:hash_size_t ->
  mtr:HH.rid -> hs:S.seq (hash #hsz) ->
  i:nat -> j:nat{i <= j && j <= S.length hs} ->
  dl:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma
    (requires (V.forall_seq hs i j
                (fun hp ->
                  Rgl?.r_inv (hreg hsz) h0 hp /\
                  HH.includes mtr (Rgl?.region_of (hreg hsz) hp)) /\
              loc_disjoint dl (B.loc_all_regions_from false mtr) /\
              modifies dl h0 h1))
    (ensures (V.forall_seq hs i j
               (fun hp ->
                 Rgl?.r_inv (hreg hsz) h1 hp /\
                 HH.includes mtr (Rgl?.region_of (hreg hsz) hp))))
    (decreases j)
let rec path_safe_preserved_ #hsz mtr hs i j dl h0 h1 =
  if i = j then ()
  else (assert (loc_includes
                 (B.loc_all_regions_from false mtr)
                 (B.loc_all_regions_from false
                   (Rgl?.region_of (hreg hsz) (S.index hs (j - 1)))));
       Rgl?.r_sep (hreg hsz) (S.index hs (j - 1)) dl h0 h1;
       path_safe_preserved_ mtr hs i (j - 1) dl h0 h1)

val path_safe_preserved:
  mtr:HH.rid -> p:path_p ->
  dl:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (path_safe h0 mtr p /\
                  loc_disjoint dl (path_loc p) /\
                  loc_disjoint dl (B.loc_all_regions_from false mtr) /\
                  modifies dl h0 h1))
        (ensures (path_safe h1 mtr p))
let path_safe_preserved mtr p dl h0 h1 =
  assert (loc_includes (path_loc p) (B.loc_buffer p));
  assert (loc_includes (path_loc p) (V.loc_vector (phashes h0 p)));
  path_safe_preserved_
    mtr (V.as_seq h0 (phashes h0 p))
    0 (S.length (V.as_seq h0 (phashes h0 p))) dl h0 h1

val path_safe_init_preserved:
  mtr:HH.rid -> p:path_p ->
  dl:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (path_safe h0 mtr p /\
                  V.size_of (phashes h0 p) = 0ul /\
                  B.loc_disjoint dl (path_loc p) /\
                  modifies dl h0 h1))
        (ensures (path_safe h1 mtr p /\
                 V.size_of (phashes h1 p) = 0ul))
let path_safe_init_preserved mtr p dl h0 h1 =
  assert (loc_includes (path_loc p) (B.loc_buffer p));
  assert (loc_includes (path_loc p) (V.loc_vector (phashes h0 p)))

val path_preserved_:
  #hsz:hash_size_t ->
  mtr:HH.rid ->
  hs:S.seq (hash #hsz) ->
  i:nat -> j:nat{i <= j && j <= S.length hs} ->
  dl:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (V.forall_seq hs i j
                    (fun hp -> Rgl?.r_inv (hreg hsz) h0 hp /\
                               HH.includes mtr (Rgl?.region_of (hreg hsz) hp)) /\
                  loc_disjoint dl (B.loc_all_regions_from false mtr) /\
                  modifies dl h0 h1))
        (ensures (path_safe_preserved_ mtr hs i j dl h0 h1;
                 S.equal (lift_path_ h0 hs i j)
                         (lift_path_ h1 hs i j)))
        (decreases j)
#push-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
let rec path_preserved_ #hsz mtr hs i j dl h0 h1 =
  if i = j then ()
  else (path_safe_preserved_ mtr hs i (j - 1) dl h0 h1;
       path_preserved_ mtr hs i (j - 1) dl h0 h1;
       assert (loc_includes
                (B.loc_all_regions_from false mtr)
                (B.loc_all_regions_from false
                  (Rgl?.region_of (hreg hsz) (S.index hs (j - 1)))));
       Rgl?.r_sep (hreg hsz) (S.index hs (j - 1)) dl h0 h1)
#pop-options

val path_preserved:
  mtr:HH.rid -> p:path_p ->
  dl:loc -> h0:HS.mem -> h1:HS.mem ->
  Lemma (requires (path_safe h0 mtr p /\
                  loc_disjoint dl (path_loc p) /\
                  loc_disjoint dl (B.loc_all_regions_from false mtr) /\
                  modifies dl h0 h1))
        (ensures (path_safe_preserved mtr p dl h0 h1;                 
                 let hsz0 = (Path?.hash_size (B.get h0 p 0)) in
                 let hsz1 = (Path?.hash_size (B.get h1 p 0)) in
                 let b:MTH.path = lift_path #hsz0 h0 mtr p in
                 let a:MTH.path = lift_path #hsz1 h1 mtr p in
                 hsz0 = hsz1 /\ S.equal b a))
let path_preserved mtr p dl h0 h1 =
  assert (loc_includes (path_loc p) (B.loc_buffer p));
  assert (loc_includes (path_loc p) (V.loc_vector (phashes h0 p)));
  path_preserved_ mtr (V.as_seq h0 (phashes h0 p))
    0 (S.length (V.as_seq h0 (phashes h0 p)))
    dl h0 h1

val init_path:
  hsz:hash_size_t ->
  mtr:HH.rid -> r:HST.erid ->
  HST.ST path_p
    (requires (fun h0 -> HH.disjoint mtr r))
    (ensures (fun h0 p h1 ->
      // memory safety
      path_safe h1 mtr p /\
      // correctness
      Path?.hash_size (B.get h1 p 0) = hsz /\
      S.equal (lift_path #hsz h1 mtr p) S.empty))
let init_path hsz mtr r =
  let nrid = HST.new_region r in
  (B.malloc r (Path hsz (rg_alloc (hvreg hsz) nrid)) 1ul)

val clear_path:
  mtr:HH.rid -> p:path_p ->
  HST.ST unit
    (requires (fun h0 -> path_safe h0 mtr p))
    (ensures (fun h0 _ h1 ->
      // memory safety
      path_safe h1 mtr p /\
      // correctness
      V.size_of (phashes h1 p) = 0ul /\
      S.equal (lift_path #(Path?.hash_size (B.get h1 p 0)) h1 mtr p) S.empty))
let clear_path mtr p =
  let pv = !*p in
  p *= Path (Path?.hash_size pv) (V.clear (Path?.hashes pv))

val free_path:
  p:path_p ->
  HST.ST unit
    (requires (fun h0 ->
      B.live h0 p /\ B.freeable p /\
      V.live h0 (phashes h0 p) /\ V.freeable (phashes h0 p) /\
      HH.extends (V.frameOf (phashes h0 p)) (B.frameOf p)))
    (ensures (fun h0 _ h1 ->
      modifies (path_loc p) h0 h1))
let free_path p =
  let pv = !*p in
  V.free (Path?.hashes pv);
  B.free p

/// Getting the Merkle root and path

// Construct "rightmost hashes" for a given (incomplete) Merkle tree.
// This function calculates the Merkle root as well, which is the final
// accumulator value.
private
val construct_rhs:
  #hsz:hash_size_t ->
  #hash_spec:Ghost.erased (MTS.hash_fun_t #(U32.v hsz)) ->
  lv:uint32_t{lv <= merkle_tree_size_lg} ->
  hs:hash_vv hsz {V.size_of hs = merkle_tree_size_lg} ->
  rhs:hash_vec #hsz {V.size_of rhs = merkle_tree_size_lg} ->
  i:index_t ->
  j:index_t{i <= j && (U32.v j) < pow2 (32 - U32.v lv)} ->
  acc:hash #hsz ->
  actd:bool ->
  hash_fun:hash_fun_t #hsz #(Ghost.reveal hash_spec) ->
  HST.ST unit
   (requires (fun h0 ->
     RV.rv_inv h0 hs /\ RV.rv_inv h0 rhs /\
     HH.disjoint (V.frameOf hs) (V.frameOf rhs) /\
     Rgl?.r_inv (hreg hsz) h0 acc /\
     HH.disjoint (B.frameOf acc) (V.frameOf hs) /\
     HH.disjoint (B.frameOf acc) (V.frameOf rhs) /\
     mt_safe_elts #hsz h0 lv hs i j))
   (ensures (fun h0 _ h1 ->
     // memory safety
     modifies (loc_union
                (RV.loc_rvector rhs)
                (B.loc_all_regions_from false (B.frameOf acc)))
              h0 h1 /\
     RV.rv_inv h1 rhs /\
     Rgl?.r_inv (hreg hsz) h1 acc /\
     // correctness
     (mt_safe_elts_spec #hsz h0 lv hs i j;
     MTH.construct_rhs #(U32.v hsz) #(Ghost.reveal hash_spec)
       (U32.v lv)
       (Rgl?.r_repr (hvvreg hsz) h0 hs)
       (Rgl?.r_repr (hvreg hsz) h0 rhs)
       (U32.v i) (U32.v j)
       (Rgl?.r_repr (hreg hsz) h0 acc) actd ==
     (Rgl?.r_repr (hvreg hsz) h1 rhs, Rgl?.r_repr (hreg hsz) h1 acc)
     )))
   (decreases (U32.v j))

#push-options "--z3rlimit 250 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
let rec construct_rhs #hsz #hash_spec lv hs rhs i j acc actd hash_fun =
  let hh0 = HST.get () in

  if j = 0ul then begin
    assert (RV.rv_inv hh0 hs);
    assert (mt_safe_elts #hsz hh0 lv hs i j);
    mt_safe_elts_spec #hsz hh0 lv hs 0ul 0ul;
    assert (MTH.hs_wf_elts #(U32.v hsz)
                           (U32.v lv) (RV.as_seq hh0 hs)
                           (U32.v i) (U32.v j));
    let hh1 = HST.get() in
    assert (MTH.construct_rhs #(U32.v hsz) #(Ghost.reveal hash_spec)
                              (U32.v lv)
                              (Rgl?.r_repr (hvvreg hsz) hh0 hs)
                              (Rgl?.r_repr (hvreg hsz) hh0 rhs)
                              (U32.v i) (U32.v j)
           (Rgl?.r_repr (hreg hsz) hh0 acc) actd ==
             (Rgl?.r_repr (hvreg hsz) hh1 rhs, Rgl?.r_repr (hreg hsz) hh1 acc))
  end
  else
    let ofs = offset_of i in
    begin
    (if j % 2ul = 0ul
    then begin
      Math.Lemmas.pow2_double_mult (32 - U32.v lv - 1);
      mt_safe_elts_rec #hsz hh0 lv hs i j;
      construct_rhs #hsz #hash_spec (lv + 1ul) hs rhs (i / 2ul) (j / 2ul) acc actd hash_fun;
      let hh1 = HST.get () in
      // correctness
      mt_safe_elts_spec #hsz hh0 lv hs i j;
      MTH.construct_rhs_even #(U32.v hsz) #hash_spec
        (U32.v lv) (Rgl?.r_repr (hvvreg hsz) hh0 hs) (Rgl?.r_repr (hvreg hsz) hh0 rhs)
        (U32.v i) (U32.v j) (Rgl?.r_repr (hreg hsz) hh0 acc) actd;
      assert (MTH.construct_rhs #(U32.v hsz) #hash_spec
               (U32.v lv)
               (Rgl?.r_repr (hvvreg hsz) hh0 hs)
               (Rgl?.r_repr (hvreg hsz) hh0 rhs)
               (U32.v i) (U32.v j)
               (Rgl?.r_repr (hreg hsz) hh0 acc)
               actd ==
             (Rgl?.r_repr (hvreg hsz) hh1 rhs, Rgl?.r_repr (hreg hsz) hh1 acc))
    end
    else begin
      if actd
      then begin
        RV.assign_copy (hcpy hsz) rhs lv acc;        
        let hh1 = HST.get () in
        // memory safety
        Rgl?.r_sep (hreg hsz) acc
          (B.loc_all_regions_from false (V.frameOf rhs)) hh0 hh1;
        RV.rv_inv_preserved
          hs (B.loc_all_regions_from false (V.frameOf rhs))
          hh0 hh1;
        RV.as_seq_preserved
          hs (B.loc_all_regions_from false (V.frameOf rhs))
          hh0 hh1;
        RV.rv_inv_preserved
          (V.get hh0 hs lv) (B.loc_all_regions_from false (V.frameOf rhs))
          hh0 hh1;
        V.loc_vector_within_included hs lv (V.size_of hs);
        mt_safe_elts_preserved lv hs i j
          (B.loc_all_regions_from false (V.frameOf rhs))
          hh0 hh1;
        mt_safe_elts_head hh1 lv hs i j;
        hash_vv_rv_inv_r_inv hh1 hs lv (j - 1ul - ofs);

        // correctness
        assert (S.equal (RV.as_seq hh1 rhs)
                        (S.upd (RV.as_seq hh0 rhs) (U32.v lv)
                               (Rgl?.r_repr (hreg hsz) hh0 acc)));

        hash_fun (V.index (V.index hs lv) (j - 1ul - ofs)) acc acc;
        let hh2 = HST.get () in
        // memory safety
        mt_safe_elts_preserved lv hs i j
          (B.loc_all_regions_from false (B.frameOf acc)) hh1 hh2;
        RV.rv_inv_preserved
          hs (B.loc_region_only false (B.frameOf acc)) hh1 hh2;
        RV.rv_inv_preserved
          rhs (B.loc_region_only false (B.frameOf acc)) hh1 hh2;
        RV.as_seq_preserved
          hs (B.loc_region_only false (B.frameOf acc)) hh1 hh2;
        RV.as_seq_preserved
          rhs (B.loc_region_only false (B.frameOf acc)) hh1 hh2;

        // correctness
        hash_vv_as_seq_get_index hh0 hs lv (j - 1ul - ofs);
        assert (Rgl?.r_repr (hreg hsz) hh2 acc ==
               (Ghost.reveal hash_spec) (S.index (S.index (RV.as_seq hh0 hs) (U32.v lv))
                                        (U32.v j - 1 - U32.v ofs))
               (Rgl?.r_repr (hreg hsz) hh0 acc))
      end
      else begin
        mt_safe_elts_head hh0 lv hs i j;
        hash_vv_rv_inv_r_inv hh0 hs lv (j - 1ul - ofs);
        hash_vv_rv_inv_disjoint hh0 hs lv (j - 1ul - ofs) (B.frameOf acc);
        Cpy?.copy (hcpy hsz) hsz (V.index (V.index hs lv) (j - 1ul - ofs)) acc;
        let hh1 = HST.get () in
        // memory safety
        V.loc_vector_within_included hs lv (V.size_of hs);
        mt_safe_elts_preserved lv hs i j
          (B.loc_all_regions_from false (B.frameOf acc)) hh0 hh1;
        RV.rv_inv_preserved
          hs (B.loc_all_regions_from false (B.frameOf acc)) hh0 hh1;
        RV.rv_inv_preserved
          rhs (B.loc_all_regions_from false (B.frameOf acc)) hh0 hh1;
        RV.as_seq_preserved
          hs (B.loc_all_regions_from false (B.frameOf acc)) hh0 hh1;
        RV.as_seq_preserved
          rhs (B.loc_all_regions_from false (B.frameOf acc)) hh0 hh1;

        // correctness
        hash_vv_as_seq_get_index hh0 hs lv (j - 1ul - ofs);
        assert (Rgl?.r_repr (hreg hsz) hh1 acc ==
                 S.index (S.index (RV.as_seq hh0 hs) (U32.v lv))
                         (U32.v j - 1 - U32.v ofs))
      end;
      let hh3 = HST.get () in
      assert (S.equal (RV.as_seq hh3 hs) (RV.as_seq hh0 hs));
      assert (S.equal (RV.as_seq hh3 rhs)
                      (if actd
                      then S.upd (RV.as_seq hh0 rhs) (U32.v lv)
                                 (Rgl?.r_repr (hreg hsz) hh0 acc)
                      else RV.as_seq hh0 rhs));
      assert (Rgl?.r_repr (hreg hsz) hh3 acc ==
             (if actd
             then (Ghost.reveal hash_spec) (S.index (S.index (RV.as_seq hh0 hs) (U32.v lv))
                                           (U32.v j - 1 - U32.v ofs))
                              (Rgl?.r_repr (hreg hsz) hh0 acc)
             else S.index (S.index (RV.as_seq hh0 hs) (U32.v lv))
                          (U32.v j - 1 - U32.v ofs)));

      mt_safe_elts_rec hh3 lv hs i j;
      construct_rhs #hsz #hash_spec (lv + 1ul) hs rhs (i / 2ul) (j / 2ul) acc true hash_fun;
      let hh4 = HST.get () in
      mt_safe_elts_spec hh3 (lv + 1ul) hs (i / 2ul) (j / 2ul);
      assert (MTH.construct_rhs #(U32.v hsz) #hash_spec
               (U32.v lv + 1)
               (Rgl?.r_repr (hvvreg hsz) hh3 hs)
               (Rgl?.r_repr (hvreg hsz) hh3 rhs)
               (U32.v i / 2) (U32.v j / 2)
               (Rgl?.r_repr (hreg hsz) hh3 acc) true ==
             (Rgl?.r_repr (hvreg hsz) hh4 rhs, Rgl?.r_repr (hreg hsz) hh4 acc));
      mt_safe_elts_spec hh0 lv hs i j;
      MTH.construct_rhs_odd #(U32.v hsz) #hash_spec
        (U32.v lv) (Rgl?.r_repr (hvvreg hsz) hh0 hs) (Rgl?.r_repr (hvreg hsz) hh0 rhs)
        (U32.v i) (U32.v j) (Rgl?.r_repr (hreg hsz) hh0 acc) actd;
      assert (MTH.construct_rhs #(U32.v hsz) #hash_spec
               (U32.v lv)
               (Rgl?.r_repr (hvvreg hsz) hh0 hs)
               (Rgl?.r_repr (hvreg hsz) hh0 rhs)
               (U32.v i) (U32.v j)
               (Rgl?.r_repr (hreg hsz) hh0 acc) actd ==
             (Rgl?.r_repr (hvreg hsz) hh4 rhs, Rgl?.r_repr (hreg hsz) hh4 acc))
    end)
  end
#pop-options

private inline_for_extraction
val mt_get_root_pre_nst: mtv:merkle_tree -> rt:hash #(MT?.hash_size mtv) -> Tot bool
let mt_get_root_pre_nst mtv rt = true

val mt_get_root_pre:
  #hsz:Ghost.erased hash_size_t ->
  mt:const_mt_p ->
  rt:hash #hsz ->
  HST.ST bool
   (requires (fun h0 ->
     let mt = CB.cast mt in
     MT?.hash_size (B.get h0 mt 0) = Ghost.reveal hsz /\
     mt_safe h0 mt /\ Rgl?.r_inv (hreg hsz) h0 rt /\
     HH.disjoint (B.frameOf mt) (B.frameOf rt)))
   (ensures (fun _ _ _ -> True))
let mt_get_root_pre #hsz mt rt =
  let mt = CB.cast mt in
  let mt = !*mt in
  let hsz = MT?.hash_size mt in
  assert (MT?.hash_size mt = hsz);
  mt_get_root_pre_nst mt rt

// `mt_get_root` returns the Merkle root. If it's already calculated with
// up-to-date hashes, the root is returned immediately. Otherwise it calls
// `construct_rhs` to build rightmost hashes and to calculate the Merkle root
// as well.
val mt_get_root:
  #hsz:Ghost.erased hash_size_t ->
  mt:const_mt_p ->
  rt:hash #hsz ->
  HST.ST unit
   (requires (fun h0 ->
     let mt = CB.cast mt in
     let dmt = B.get h0 mt 0 in
     MT?.hash_size dmt = (Ghost.reveal hsz) /\
     mt_get_root_pre_nst dmt rt /\
     mt_safe h0 mt /\ Rgl?.r_inv (hreg hsz) h0 rt /\
     HH.disjoint (B.frameOf mt) (B.frameOf rt)))
   (ensures (fun h0 _ h1 ->
     let mt = CB.cast mt in
     // memory safety
     modifies (loc_union
                (mt_loc mt)
                (B.loc_all_regions_from false (B.frameOf rt)))
              h0 h1 /\
     mt_safe h1 mt /\
     (let mtv0 = B.get h0 mt 0 in
     let mtv1 = B.get h1 mt 0 in
     MT?.hash_size mtv0 = (Ghost.reveal hsz) /\
     MT?.hash_size mtv1 = (Ghost.reveal hsz) /\
     MT?.i mtv1 = MT?.i mtv0 /\ MT?.j mtv1 = MT?.j mtv0 /\
     MT?.hs mtv1 == MT?.hs mtv0 /\ MT?.rhs mtv1 == MT?.rhs mtv0 /\
     MT?.offset mtv1 == MT?.offset mtv0 /\
     MT?.rhs_ok mtv1 = true /\
     Rgl?.r_inv (hreg hsz) h1 rt /\
     // correctness
     MTH.mt_get_root (mt_lift h0 mt) (Rgl?.r_repr (hreg hsz) h0 rt) ==
     (mt_lift h1 mt, Rgl?.r_repr (hreg hsz) h1 rt))))
#push-options "--z3rlimit 150 --initial_fuel 1 --max_fuel 1"
let mt_get_root #hsz mt rt =
  let mt = CB.cast mt in
  let hh0 = HST.get () in
  let mtv = !*mt in
  let prefix = MT?.offset mtv in
  let i = MT?.i mtv in
  let j = MT?.j mtv in
  let hs = MT?.hs mtv in
  let rhs = MT?.rhs mtv in
  let mroot = MT?.mroot mtv in
  let hash_size = MT?.hash_size mtv in
  let hash_spec = MT?.hash_spec mtv in
  let hash_fun = MT?.hash_fun mtv in
  if MT?.rhs_ok mtv
  then begin
    Cpy?.copy (hcpy hash_size) hash_size mroot rt;
    let hh1 = HST.get () in
    mt_safe_preserved mt
      (B.loc_all_regions_from false (Rgl?.region_of (hreg hsz) rt)) hh0 hh1;
    mt_preserved mt
      (B.loc_all_regions_from false (Rgl?.region_of (hreg hsz) rt)) hh0 hh1;
    MTH.mt_get_root_rhs_ok_true
      (mt_lift hh0 mt) (Rgl?.r_repr (hreg hsz) hh0 rt);
    assert (MTH.mt_get_root (mt_lift hh0 mt) (Rgl?.r_repr (hreg hsz) hh0 rt) ==
           (mt_lift hh1 mt, Rgl?.r_repr (hreg hsz) hh1 rt))
  end
  else begin
    construct_rhs #hash_size #hash_spec 0ul hs rhs i j rt false hash_fun;
    let hh1 = HST.get () in
    // memory safety
    assert (RV.rv_inv hh1 rhs);
    assert (Rgl?.r_inv (hreg hsz) hh1 rt);
    assert (B.live hh1 mt);
    RV.rv_inv_preserved
      hs (loc_union
           (RV.loc_rvector rhs)
           (B.loc_all_regions_from false (B.frameOf rt)))
      hh0 hh1;
    RV.as_seq_preserved
      hs (loc_union
           (RV.loc_rvector rhs)
           (B.loc_all_regions_from false (B.frameOf rt)))
      hh0 hh1;
    V.loc_vector_within_included hs 0ul (V.size_of hs);
    mt_safe_elts_preserved 0ul hs i j
      (loc_union
        (RV.loc_rvector rhs)
        (B.loc_all_regions_from false (B.frameOf rt)))
      hh0 hh1;

    // correctness
    mt_safe_elts_spec hh0 0ul hs i j;
    assert (MTH.construct_rhs #(U32.v hash_size) #hash_spec 0
             (Rgl?.r_repr (hvvreg hsz) hh0 hs)
             (Rgl?.r_repr (hvreg hsz) hh0 rhs)
             (U32.v i) (U32.v j)
             (Rgl?.r_repr (hreg hsz) hh0 rt) false ==
           (Rgl?.r_repr (hvreg hsz) hh1 rhs, Rgl?.r_repr (hreg hsz) hh1 rt));

    Cpy?.copy (hcpy hash_size) hash_size rt mroot;
    let hh2 = HST.get () in
    // memory safety
    RV.rv_inv_preserved
      hs (B.loc_all_regions_from false (B.frameOf mroot))
      hh1 hh2;
    RV.rv_inv_preserved
      rhs (B.loc_all_regions_from false (B.frameOf mroot))
      hh1 hh2;
    RV.as_seq_preserved
      hs (B.loc_all_regions_from false (B.frameOf mroot))
      hh1 hh2;
    RV.as_seq_preserved
      rhs (B.loc_all_regions_from false (B.frameOf mroot))
      hh1 hh2;
    B.modifies_buffer_elim
      rt (B.loc_all_regions_from false (B.frameOf mroot))
      hh1 hh2;
    mt_safe_elts_preserved 0ul hs i j
      (B.loc_all_regions_from false (B.frameOf mroot))
      hh1 hh2;

    // correctness
    assert (Rgl?.r_repr (hreg hsz) hh2 mroot == Rgl?.r_repr (hreg hsz) hh1 rt);

    mt *= MT hash_size prefix i j hs true rhs mroot hash_spec hash_fun;
    let hh3 = HST.get () in
    // memory safety
    Rgl?.r_sep (hreg hsz) rt (B.loc_buffer mt) hh2 hh3;
    RV.rv_inv_preserved hs (B.loc_buffer mt) hh2 hh3;
    RV.rv_inv_preserved rhs (B.loc_buffer mt) hh2 hh3;
    RV.as_seq_preserved hs (B.loc_buffer mt) hh2 hh3;
    RV.as_seq_preserved rhs (B.loc_buffer mt) hh2 hh3;
    Rgl?.r_sep (hreg hsz) mroot (B.loc_buffer mt) hh2 hh3;
    mt_safe_elts_preserved 0ul hs i j
      (B.loc_buffer mt) hh2 hh3;
    assert (mt_safe hh3 mt);

    // correctness
    MTH.mt_get_root_rhs_ok_false
      (mt_lift hh0 mt) (Rgl?.r_repr (hreg hsz) hh0 rt);
    assert (MTH.mt_get_root (mt_lift hh0 mt) (Rgl?.r_repr (hreg hsz) hh0 rt) ==
           (MTH.MT #(U32.v hash_size)
                   (U32.v i) (U32.v j)
                   (RV.as_seq hh0 hs)
                   true
                   (RV.as_seq hh1 rhs)
                   (Rgl?.r_repr (hreg hsz) hh1 rt)
                   hash_spec,
                   Rgl?.r_repr (hreg hsz) hh1 rt));
    assert (MTH.mt_get_root (mt_lift hh0 mt) (Rgl?.r_repr (hreg hsz) hh0 rt) ==
           (mt_lift hh3 mt, Rgl?.r_repr (hreg hsz) hh3 rt))
  end
#pop-options

inline_for_extraction
val mt_path_insert:
  #hsz:hash_size_t ->
  mtr:HH.rid -> p:path_p -> hp:hash #hsz ->
  HST.ST unit
    (requires (fun h0 ->
      path_safe h0 mtr p /\
      not (V.is_full (phashes h0 p)) /\
     Rgl?.r_inv (hreg hsz) h0 hp /\
      HH.disjoint mtr (B.frameOf p) /\
      HH.includes mtr (B.frameOf hp) /\
      Path?.hash_size (B.get h0 p 0) = hsz))
    (ensures (fun h0 _ h1 ->      
      // memory safety
      modifies (path_loc p) h0 h1 /\
      path_safe h1 mtr p /\      
      // correctness
      (let hsz0 = Path?.hash_size (B.get h0 p 0) in
       let hsz1 = Path?.hash_size (B.get h1 p 0) in
       (let before:(S.seq (MTH.hash #(U32.v hsz0))) = lift_path h0 mtr p in       
        let after:(S.seq (MTH.hash #(U32.v hsz1))) = lift_path h1 mtr p in
        V.size_of (phashes h1 p) = V.size_of (phashes h0 p) + 1ul /\
        hsz = hsz0 /\ hsz = hsz1 /\        
        (let hspec:(S.seq (MTH.hash #(U32.v hsz))) = (MTH.path_insert #(U32.v hsz) before (Rgl?.r_repr (hreg hsz) h0 hp)) in
          S.equal hspec after)))))
#push-options "--z3rlimit 20 --initial_fuel 1 --max_fuel 1"
let mt_path_insert #hsz mtr p hp =  
  let pth = !*p in
  let pv = Path?.hashes pth in
  let hh0 = HST.get () in
  let ipv = V.insert pv hp in
  let hh1 = HST.get () in
  path_safe_preserved_
    mtr (V.as_seq hh0 pv) 0 (S.length (V.as_seq hh0 pv))
    (B.loc_all_regions_from false (V.frameOf ipv)) hh0 hh1;
  path_preserved_
    mtr (V.as_seq hh0 pv) 0 (S.length (V.as_seq hh0 pv))
    (B.loc_all_regions_from false (V.frameOf ipv)) hh0 hh1;
  Rgl?.r_sep (hreg hsz) hp
    (B.loc_all_regions_from false (V.frameOf ipv)) hh0 hh1;
  p *= Path hsz ipv;
  let hh2 = HST.get () in
  path_safe_preserved_
    mtr (V.as_seq hh1 ipv) 0 (S.length (V.as_seq hh1 ipv))
    (B.loc_region_only false (B.frameOf p)) hh1 hh2;
  path_preserved_
    mtr (V.as_seq hh1 ipv) 0 (S.length (V.as_seq hh1 ipv))
    (B.loc_region_only false (B.frameOf p)) hh1 hh2;
  Rgl?.r_sep (hreg hsz) hp
    (B.loc_region_only false (B.frameOf p)) hh1 hh2;
  assert (S.equal (lift_path hh2 mtr p)
                  (lift_path_ hh1 (S.snoc (V.as_seq hh0 pv) hp)
                    0 (S.length (V.as_seq hh1 ipv))));
  lift_path_eq hh1 (S.snoc (V.as_seq hh0 pv) hp) (V.as_seq hh0 pv)
    0 (S.length (V.as_seq hh0 pv))
#pop-options

// For given a target index `k`, the number of elements (in the tree) `j`,
// and a boolean flag (to check the existence of rightmost hashes), we can
// calculate a required Merkle path length.
//
// `mt_path_length` is a postcondition of `mt_get_path`, and a precondition
// of `mt_verify`. For detailed description, see `mt_get_path` and `mt_verify`.
private
val mt_path_length_step:
  k:index_t ->
  j:index_t{k <= j} ->
  actd:bool ->
  Tot (sl:uint32_t{U32.v sl = MTH.mt_path_length_step (U32.v k) (U32.v j) actd})
val mt_path_length_step:
  k:index_t ->
  j:index_t{k <= j} ->
  actd:bool ->
  Tot (sl:uint32_t{U32.v sl = MTH.mt_path_length_step (U32.v k) (U32.v j) actd})
k: MerkleTree.Low.index_t -> j: MerkleTree.Low.index_t{k <= j} -> actd: Prims.bool
  -> sl:
    LowStar.Vector.uint32_t
      { FStar.UInt32.v sl =
        MerkleTree.New.High.mt_path_length_step (FStar.UInt32.v k) (FStar.UInt32.v j) actd }