val accv (a:alg) : Type0
val accv (a:alg) : Type0
let accv (a:alg) = accv' a
﻿(* 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

#push-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 40"
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


(* 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...

//17-01-26 two steps required for abstraction for datatypes
/
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 -> Type0
MiTLS.Hashing.Spec.alg MiTLS.Hashing.accv'
let accv (a: alg) =
  
accv' a