val h (a: alg) (b: hashable a) : GTot (tag a)
val h (a: alg) (b: hashable a) : GTot (tag a)
let h (a:alg) (b:hashable a): GTot (tag a) =
  let v = Spec.Agile.Hash.hash a (Bytes.reveal b) in
  Bytes.hide v
(* Copyright (C) 2012--2015 Microsoft Research and INRIA *)
module MiTLS.Hashing
open MiTLS

open MiTLS.Declassify
open MiTLS.Mem

include MiTLS.Hashing.Spec

open FStar.HyperStack.ST
open FStar.Bytes
open FStar.Integers

module ST = FStar.HyperStack.ST

module B = LowStar.Buffer

// defining those on FStar.Bytes, not on EverCrypt's seq Uin8.t
type hashable (a:alg) = b:bytes {length b `less_than_max_input_length` a}
type tag (a:alg) = lbytes32 (Hacl.Hash.Definitions.hash_len a)

// 18-08-31 pure hash specification;
/
Spec.Agile.Hash.fsti.checked prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Declassify.fsti.checked LowStar.Buffer.fst.checked Hacl.Hash.Definitions.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Hashing.fsti
a: MiTLS.Hashing.Spec.alg -> b: MiTLS.Hashing.hashable a -> Prims.GTot (MiTLS.Hashing.tag a)
MiTLS.Hashing.Spec.alg MiTLS.Hashing.hashable FStar.Bytes.hide Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Hash.Definitions.hash_length' Spec.Agile.Hash.hash FStar.Bytes.reveal MiTLS.Hashing.tag
let h (a: alg) (b: hashable a) : GTot (tag a) =
  
let v = Spec.Agile.Hash.hash a (Bytes.reveal b) in
Bytes.hide v