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)))
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)))
let finalize #a (Inputs b) = compute a b
﻿(* 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
private type accv' (a:alg) =  | Inputs: b: hashable a -> accv' a
let accv (a:alg) = accv' a

let content #a v =
  match v with Inputs b -> b

let start a = Inputs empty_bytes
let extend #a (Inputs b0) b1 =
  assume (FStar.UInt.fits (length b0 + length b1) 32);
  assume ((length b0 + length b1) `Spec.Agile.Hash.less_than_max_input_length` a);
/
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
v: MiTLS.Hashing.accv a
  -> FStar.HyperStack.ST.ST
    (t: MiTLS.Hashing.Spec.tag a {t == MiTLS.Hashing.h a (MiTLS.Hashing.content v)})
MiTLS.Hashing.Spec.alg MiTLS.Hashing.accv MiTLS.Hashing.hashable MiTLS.Hashing.compute MiTLS.Hashing.Spec.tag Prims.eq2 FStar.Bytes.bytes Prims.l_or Prims.b2t Prims.op_Equality Prims.int FStar.UInt.size Prims.op_GreaterThanOrEqual FStar.Bytes.length Spec.Hash.Definitions.hash_length FStar.UInt32.t FStar.Bytes.len Hacl.Hash.Definitions.hash_len MiTLS.Hashing.h MiTLS.Hashing.content
let finalize #a (Inputs b) =
  
compute a b