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)
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)
let compute a text =
  let h00 = ST.get() in
  push_frame();
  let tlen = Hacl.Hash.Definitions.hash_len a in
  let output = LowStar.Buffer.alloca 0uy tlen in
  let len = Bytes.len text in
  if len = 0ul then
    begin
    let input = LowStar.Buffer.null in
    //18-09-01 this could follow from LowStar.Buffer or Bytes properties
    let h0 = ST.get() in
    Seq.lemma_eq_intro (reveal text) (LowStar.Buffer.as_seq h0 input);
    EverCrypt.Hash.Incremental.hash a output input len
    end
  else
    begin
    let h0 = ST.get() in
    push_frame();
    let input = LowStar.Buffer.alloca 0uy len in
    store_bytes text input;
    EverCrypt.Hash.Incremental.hash a output input len;
    pop_frame()
    end;
  let t = Bytes.of_buffer tlen output in
  pop_frame();
  t
﻿(* Copyright (C) 2012--2015 Microsoft Research and INRIA *)
module MiTLS.Hashing
open MiTLS
friend Lib.IntTypes

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
/
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 Lib.IntTypes.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.Bytes.fsti.checked EverCrypt.Hash.Incremental.fst.checked
MiTLS.Hashing.fst
a: MiTLS.Hashing.Spec.alg -> text: MiTLS.Hashing.hashable a
  -> FStar.HyperStack.ST.Stack (MiTLS.Hashing.Spec.tag a)
MiTLS.Hashing.Spec.alg MiTLS.Hashing.hashable MiTLS.Hashing.Spec.tag Prims.unit FStar.HyperStack.ST.pop_frame FStar.Bytes.bytes Prims.b2t Prims.op_Equality FStar.UInt.uint_t FStar.UInt32.v FStar.Bytes.len FStar.Bytes.of_buffer LowStar.Buffer.trivial_preorder Lib.IntTypes.uint8 FStar.Bytes.length FStar.UInt32.t FStar.UInt32.__uint_to_t EverCrypt.Hash.Incremental.hash FStar.Seq.Base.lemma_eq_intro FStar.Bytes.byte FStar.Bytes.reveal LowStar.Monotonic.Buffer.as_seq FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.Buffer.buffer FStar.UInt8.t LowStar.Buffer.null Prims.bool FStar.Bytes.store_bytes LowStar.Monotonic.Buffer.mbuffer Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Buffer.alloca FStar.UInt8.__uint_to_t FStar.HyperStack.ST.push_frame Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.int Prims.l_or Lib.IntTypes.range Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.op_GreaterThan Lib.IntTypes.v Spec.Hash.Definitions.hash_length Hacl.Hash.Definitions.hash_len
let compute a text =
  
let h00 = ST.get () in
push_frame ();
let tlen = Hacl.Hash.Definitions.hash_len a in
let output = LowStar.Buffer.alloca 0uy tlen in
let len = Bytes.len text in
if len = 0ul
then
  let input = LowStar.Buffer.null in
  let h0 = ST.get () in
  Seq.lemma_eq_intro (reveal text) (LowStar.Buffer.as_seq h0 input);
  EverCrypt.Hash.Incremental.hash a output input len
else
  (let h0 = ST.get () in
    push_frame ();
    let input = LowStar.Buffer.alloca 0uy len in
    store_bytes text input;
    EverCrypt.Hash.Incremental.hash a output input len;
    pop_frame ());
let t = Bytes.of_buffer tlen output in
pop_frame ();
t