val mt_create: r:HST.erid -> init:hash #32ul -> HST.ST mt_p
   (requires (fun h0 ->
     Rgl?.r_inv (MTLD.hreg 32ul) h0 init /\
     HH.disjoint r (B.frameOf init)))
   (ensures (fun h0 mt h1 ->
     // memory safety
     B.modifies B.(loc_union (mt_loc mt) (B.loc_all_regions_from false (B.frameOf init))) h0 h1 /\
     mt_safe h1 mt /\
     // correctness
     MerkleTree.Low.MT?.hash_size (B.get h1 mt 0) = 32ul /\
     mt_lift h1 mt == MTH.mt_create 32 MTH.sha256_compress (Rgl?.r_repr (MTLD.hreg 32ul) h0 init)))
let mt_create r init =
  mt_create_custom 32ul (MerkleTree.New.High.sha256_compress) r init mt_sha256_compress
val mt_create: r:HST.erid -> init:hash #32ul -> HST.ST mt_p
   (requires (fun h0 ->
     Rgl?.r_inv (MTLD.hreg 32ul) h0 init /\
     HH.disjoint r (B.frameOf init)))
   (ensures (fun h0 mt h1 ->
     // memory safety
     B.modifies B.(loc_union (mt_loc mt) (B.loc_all_regions_from false (B.frameOf init))) h0 h1 /\
     mt_safe h1 mt /\
     // correctness
     MerkleTree.Low.MT?.hash_size (B.get h1 mt 0) = 32ul /\
     mt_lift h1 mt == MTH.mt_create 32 MTH.sha256_compress (Rgl?.r_repr (MTLD.hreg 32ul) h0 init)))
let mt_create r init =
mt_create_custom 32ul (MerkleTree.New.High.sha256_compress) r init mt_sha256_compress
MerkleTree.EverCrypt.fst.checked
Spec.Hash.Lemmas.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked MerkleTree.New.High.fst.checked MerkleTree.Low.Hashfunctions.fst.checked MerkleTree.Low.Datastructures.fst.checked MerkleTree.Low.fst.checked LowStar.Regional.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Hash.fsti.checked
MerkleTree.EverCrypt.fst
FStar.HyperStack.ST.erid MerkleTree.EverCrypt.hash FStar.UInt32.__uint_to_t MerkleTree.Low.mt_create_custom FStar.Ghost.hide MerkleTree.Spec.hash_fun_t FStar.UInt32.v MerkleTree.New.High.sha256_compress MerkleTree.EverCrypt.mt_sha256_compress MerkleTree.Low.mt_p MerkleTree.EverCrypt.mt_p
module MerkleTree.EverCrypt

open MerkleTree.Low

module HH = FStar.Monotonic.HyperHeap
module B = LowStar.Buffer

module HST = FStar.HyperStack.ST
module MTH = MerkleTree.New.High
module MTLD = MerkleTree.Low.Datastructures
module MLH = MerkleTree.Low.Hashfunctions
module Hash = Spec.Hash.Definitions

open LowStar.Regional

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

module S = FStar.Seq

module EHS = EverCrypt.Hash

open MerkleTree.Low.Datastructures

open Lib.IntTypes

/// A definition whose sole purpose is to align the .fsti with the .fst
noextract let _align = ()

#push-options "--z3rlimit 150 --ifuel 1"
let mt_sha256_compress src1 src2 dst =
  let hash_size = 32ul in
  [@inline_let]
  let hash_alg = Spec.Hash.Definitions.SHA2_256 in
  let hh0 = HST.get () in
  HST.push_frame ();
  // KaRaMeL can't extract `EHS.blockLen EHS.SHA256` (= 64ul)
  let cb = B.alloca (u8 0) 64ul in
  B.blit src1 0ul cb 0ul hash_size;
  B.blit src2 0ul cb 32ul hash_size;

  // ONLY WORKS BECAUSE hash_alg is inline_for_extraction and is known to be SHA2_256
  let st = EHS.create_in hash_alg HyperStack.root in
  EHS.init #(Ghost.hide hash_alg) st;
  let hh1 = HST.get () in
  assert (S.equal (S.append
                    (Rgl?.r_repr(hreg hash_size) hh0 src1)
                    (Rgl?.r_repr(hreg hash_size) hh0 src2))
                  (B.as_seq hh1 cb));

  EHS.update_multi #(Ghost.hide hash_alg) st 0UL cb (Hacl.Hash.Definitions.block_len Spec.Hash.Definitions.SHA2_256);
  Spec.Hash.Lemmas.update_multi_update Spec.Hash.Definitions.SHA2_256 (EHS.repr st hh1) (B.as_seq hh1 cb);
  let hh2 = HST.get () in
  assert (EHS.repr st hh2 ==
            Spec.Agile.Hash.update hash_alg (Spec.Agile.Hash.init hash_alg)
                                            (B.as_seq hh1 cb));
  assert (S.equal (S.append S.empty (B.as_seq hh1 cb))
                  (B.as_seq hh1 cb));
  EHS.finish #(Ghost.hide hash_alg) st dst;
  let hh3 = HST.get () in
  assert (S.equal (B.as_seq hh3 dst)
                  (Spec.Agile.Hash.finish hash_alg (EHS.repr st hh2) ()));
  assert (S.equal (B.as_seq hh3 dst)
                  (Spec.Agile.Hash.finish hash_alg (Spec.Agile.Hash.update hash_alg (Spec.Agile.Hash.init hash_alg) (B.as_seq hh1 cb)) ()));
  assert (S.equal (B.as_seq hh3 dst)
                  (MTH.sha256_compress
                    (Rgl?.r_repr(hreg hash_size) hh0 src1)
                    (Rgl?.r_repr(hreg hash_size) hh0 src2)));
  EHS.free st;
  HST.pop_frame ();

  let hh4 = HST.get () in
  assert (S.equal (B.as_seq hh4 dst)
                  (MTH.sha256_compress
                    (Rgl?.r_repr(hreg hash_size) hh0 src1)
                    (Rgl?.r_repr(hreg hash_size) hh0 src2)))
#pop-options
val mt_create: r:HST.erid -> init:hash #32ul -> HST.ST mt_p
   (requires (fun h0 ->
     Rgl?.r_inv (MTLD.hreg 32ul) h0 init /\
     HH.disjoint r (B.frameOf init)))
   (ensures (fun h0 mt h1 ->
     // memory safety
     B.modifies B.(loc_union (mt_loc mt) (B.loc_all_regions_from false (B.frameOf init))) h0 h1 /\
     mt_safe h1 mt /\
     // correctness
     MerkleTree.Low.MT?.hash_size (B.get h1 mt 0) = 32ul /\
     mt_lift h1 mt == MTH.mt_create 32 MTH.sha256_compress (Rgl?.r_repr (MTLD.hreg 32ul) h0 init)))
r: FStar.HyperStack.ST.erid -> init: MerkleTree.EverCrypt.hash
  -> FStar.HyperStack.ST.ST MerkleTree.EverCrypt.mt_p