val mt_sha256_compress: MTLH.hash_fun_t #32ul #(Ghost.hide MTH.sha256_compress)
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)))
val mt_sha256_compress: MTLH.hash_fun_t #32ul #(Ghost.hide MTH.sha256_compress)
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 ();
let cb = B.alloca (u8 0) 64ul in
B.blit src1 0ul cb 0ul hash_size;
B.blit src2 0ul cb 32ul hash_size;
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)))
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
MerkleTree.Low.Datastructures.hash FStar.UInt32.__uint_to_t Prims._assert FStar.Seq.Base.equal Lib.IntTypes.uint8 LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.trivial_preorder MerkleTree.New.High.sha256_compress LowStar.Regional.__proj__Rgl__item__r_repr MerkleTree.Low.Datastructures.hash_size_t MerkleTree.Low.Datastructures.hreg Prims.unit FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get FStar.HyperStack.ST.pop_frame EverCrypt.Hash.free FStar.Ghost.hide Spec.Hash.Definitions.fixed_len_alg Spec.Agile.Hash.finish Spec.Agile.Hash.update Spec.Agile.Hash.init EverCrypt.Hash.repr EverCrypt.Hash.finish EverCrypt.Hash.alg FStar.Seq.Base.append FStar.Seq.Base.empty Prims.eq2 Spec.Hash.Definitions.words_state Spec.Hash.Lemmas.update_multi_update Spec.Hash.Definitions.SHA2_256 EverCrypt.Hash.update_multi FStar.UInt64.__uint_to_t Hacl.Hash.Definitions.block_len EverCrypt.Hash.init EverCrypt.Hash.state EverCrypt.Hash.create_in FStar.Monotonic.HyperHeap.root LowStar.Monotonic.Buffer.blit LowStar.Monotonic.Buffer.mbuffer Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.l_and Prims.nat LowStar.Monotonic.Buffer.length FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t Prims.b2t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Buffer.alloca Lib.IntTypes.u8 FStar.HyperStack.ST.push_frame Spec.Hash.Definitions.hash_alg
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 = ()
val mt_sha256_compress: MTLH.hash_fun_t #32ul #(Ghost.hide MTH.sha256_compress)
MerkleTree.Low.Hashfunctions.hash_fun_t