val finalize: #a:alg -> v:accv a -> ST (tag a)
  (requires (fun h0 -> True))
  (ensures (fun h0 t h1 ->
    let b = content v in
    //18-01-03 TODO modifies (Set.as_set [TLSConstants.tls_tables_region]) h0 h1 /\
    t = h a b /\ hashed a b
  ))
val finalize: #a:alg -> v:accv a -> ST (tag a)
  (requires (fun h0 -> True))
  (ensures (fun h0 t h1 ->
    let b = content v in
    //18-01-03 TODO modifies (Set.as_set [TLSConstants.tls_tables_region]) h0 h1 /\
    t = h a b /\ hashed a b
  ))
let finalize #a v =
  let t = Hashing.finalize v in
  if crf a then (
    let x = Computed a t in
    let b = Hashing.content v in
    match MDM.lookup table x with
      | None -> MDM.extend table x b
      | Some b' -> if b <> b' then stop "hash collision detected");
  t
﻿(** computational assumption: collision resistance *)
module MiTLS.Hashing.CRF
open MiTLS

open MiTLS.Mem
include MiTLS.Hashing
open FStar.Bytes

let hashed (a:alg) (b:hashable a) =
  crf a ==> (
    let t = h a b in
    let b: domain (Computed a t) = b in
    witnessed (MDM.contains table (Computed a t) b))

let crf_injective a b0 b1 =
  if crf a then (
    recall table;
    let f = !table in
    testify(MDM.contains table (Computed a (h a b0)) b0);
    testify(MDM.contains table (Computed a (h a b1)) b1)
  )
/
prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Hashing.CRF.fst
v: MiTLS.Hashing.accv a -> FStar.HyperStack.ST.ST (MiTLS.Hashing.tag a)
MiTLS.Hashing.Spec.alg MiTLS.Hashing.accv MiTLS.Hashing.tag Prims.unit MiTLS.Hashing.CRF.crf FStar.Monotonic.DependentMap.extend MiTLS.Hashing.CRF.range MiTLS.Hashing.CRF.domain MiTLS.Hashing.CRF.inv MiTLS.Mem.tls_tables_region MiTLS.Hashing.CRF.table Prims.op_disEquality FStar.Bytes.bytes Prims.l_or Prims.b2t Spec.Hash.Definitions.less_than_max_input_length FStar.Bytes.length Prims.l_and Prims.op_Equality MiTLS.Hashing.h Prims.logical MiTLS.Hashing.CRF.stop Prims.bool FStar.Pervasives.Native.option FStar.Monotonic.DependentMap.lookup MiTLS.Hashing.hashable MiTLS.Hashing.content MiTLS.Hashing.CRF.Computed Prims.eq2 MiTLS.Hashing.finalize
let finalize #a v =
  
let t = Hashing.finalize v in
if crf a
then
  (let x = Computed a t in
    let b = Hashing.content v in
    match MDM.lookup table x with
    | None -> MDM.extend table x b
    | Some b' -> if b <> b' then stop "hash collision detected");
t