val compute_MD5SHA1 : data:
      b:
      FStar.Bytes.bytes
        { Spec.Hash.Definitions.less_than_max_input_length (FStar.Bytes.length b)
            Spec.Hash.Definitions.MD5 /\
          Spec.Hash.Definitions.less_than_max_input_length (FStar.Bytes.length b)
            Spec.Hash.Definitions.SHA1 }
  -> FStar.HyperStack.ST.STATE FStar.Bytes.bytes
let compute_MD5SHA1 data = compute MD5 data @| compute SHA1 data
(* 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;
// renamed from [hash] already included from EverCrypt.Hash
let h (a:alg) (b:hashable a): GTot (tag a) =
  let v = Spec.Agile.Hash.hash a (Bytes.reveal b) in
  Bytes.hide v

/// bytes wrapper for [EverCrypt.Hash.hash]
val compute: a:alg -> text:hashable a -> Stack (tag a)
  (requires fun h0 -> True)
  (ensures fun h0 t h1 ->
    let v = reveal text in
    B.modifies B.loc_none h0 h1 /\
    Seq.length v `less_than_max_input_length` a /\
    t = h a text)

(* IMPLEMENTATION PLACEHOLDER,
    simply buffering the bytes underneath *)

// 18-08-29 TODO actually use EverCrypt's incremental API, but this
// requires (1) any-length incremental, and (2) switching all these
// functions from pure to modifiying an abstract footprint...

val accv (a:alg) : Type0

val content: #a:alg -> accv a -> Tot (hashable a)

val start: a:alg -> Tot (v:accv a {content v == empty_bytes})
val extend: #a:alg -> v:accv a -> b:bytes -> Tot (v':accv a {length (content v) + length b = length (content v') /\  content v' == content v @| b})

val finalize: #a:alg -> v:accv a -> ST (t:tag a {t == h a (content v)})
  (requires (fun h0 -> True))
  (ensures (fun h0 t h1 -> B.(modifies loc_none h0 h1)))
/
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

    data:
      b:
      FStar.Bytes.bytes
        { Spec.Hash.Definitions.less_than_max_input_length (FStar.Bytes.length b)
            Spec.Hash.Definitions.MD5 /\
          Spec.Hash.Definitions.less_than_max_input_length (FStar.Bytes.length b)
            Spec.Hash.Definitions.SHA1 }
  -> FStar.HyperStack.ST.STATE FStar.Bytes.bytes
FStar.Bytes.bytes Prims.l_and Prims.b2t Spec.Hash.Definitions.less_than_max_input_length FStar.Bytes.length Spec.Hash.Definitions.MD5 Spec.Hash.Definitions.SHA1 FStar.Bytes.op_At_Bar MiTLS.Hashing.compute MiTLS.Hashing.tag
let compute_MD5SHA1 data =
  
compute MD5 data @| compute SHA1 data