val sha256_compress: hash_fun_t #32
let sha256_compress src1 src2 =
  let sz = Spec.Hash.Definitions.SHA2_256 in
  let hash_alg = Spec.Hash.Definitions.SHA2_256 in
  let acc = Spec.Agile.Hash.init hash_alg in
  let acc = Spec.Agile.Hash.update hash_alg acc (S.append src1 src2) in
  Spec.Agile.Hash.finish hash_alg acc ()
val sha256_compress: hash_fun_t #32
let sha256_compress src1 src2 =
let sz = Spec.Hash.Definitions.SHA2_256 in
let hash_alg = Spec.Hash.Definitions.SHA2_256 in
let acc = Spec.Agile.Hash.init hash_alg in
let acc = Spec.Agile.Hash.update hash_alg acc (S.append src1 src2) in
Spec.Agile.Hash.finish hash_alg acc ()
MerkleTree.Spec.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked FStar.StrongExcludedMiddle.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
MerkleTree.Spec.fst
MerkleTree.Spec.hash Spec.Agile.Hash.finish Spec.Hash.Definitions.words_state Spec.Agile.Hash.update FStar.Seq.Base.append Lib.IntTypes.uint8 Spec.Hash.Definitions.init_t Spec.Agile.Hash.init Spec.Hash.Definitions.hash_alg Spec.Hash.Definitions.SHA2_256
module MerkleTree.Spec

open FStar.Classical
open FStar.Mul
open FStar.Seq

module S = FStar.Seq

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 10"

// For SHA2_256, this is is a sequence of 32 bytes
// These are secret bytes, hence not an eqtype
type hash (#hsz:pos) = b:Spec.Hash.Definitions.bytes { Seq.length b = hsz }

type hash_fun_t (#hsz:pos) = hash #hsz -> hash #hsz -> GTot (hash #hsz)
val sha256_compress: hash_fun_t #32
MerkleTree.Spec.hash_fun_t