val padded_hash_fun: (#hsz:pos) -> (f:hash_fun_t #hsz) -> (lh:padded_hash #hsz) -> (rh:padded_hash #hsz) -> GTot (padded_hash #hsz)
let padded_hash_fun #hsz f lh rh =
  allow_inversion (padded_hash #hsz);
  match lh, rh with
  | HPad    , _        -> HPad
  | _       , HPad     -> lh
  | HRaw lhr, HRaw rhr -> HRaw (f lhr rhr)
val padded_hash_fun: (#hsz:pos) -> (f:hash_fun_t #hsz) -> (lh:padded_hash #hsz) -> (rh:padded_hash #hsz) -> GTot (padded_hash #hsz)
let padded_hash_fun #hsz f lh rh =
allow_inversion (padded_hash #hsz);
match lh, rh with
| HPad, _ -> HPad
| _, HPad -> lh
| HRaw lhr, HRaw rhr -> HRaw (f lhr rhr)
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
Prims.pos MerkleTree.Spec.hash_fun_t MerkleTree.Spec.padded_hash FStar.Pervasives.Native.Mktuple2 MerkleTree.Spec.HPad MerkleTree.Spec.hash MerkleTree.Spec.HRaw Prims.unit FStar.Pervasives.allow_inversion
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
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 ()

/// For simplicity, we will specify the root for a sequence of [i]
/// tags where [i <= 2^n] as the root of a full binary tree with [2^n]
/// leaves obtained by padding the sequence with dummies. This
/// requires extending the definitions of hashes and hash functions. Our
/// extended definition of hash justifies skipping any concrete
/// computation on dummies.
noeq
type padded_hash #hsz =
| HRaw: hr:hash #hsz -> padded_hash #hsz
| HPad // right padding to make the size of a Merkle tree a power of 2

val padded_hash_fun: (#hsz:pos) -> (f:hash_fun_t #hsz) -> (lh:padded_hash #hsz) -> (rh:padded_hash #hsz) -> GTot (padded_hash #hsz)
val padded_hash_fun: (#hsz:pos) -> (f:hash_fun_t #hsz) -> (lh:padded_hash #hsz) -> (rh:padded_hash #hsz) -> GTot (padded_hash #hsz)
f: MerkleTree.Spec.hash_fun_t -> lh: MerkleTree.Spec.padded_hash -> rh: MerkleTree.Spec.padded_hash
  -> Prims.GTot MerkleTree.Spec.padded_hash