val hashed (a:alg) (b:hashable a) : Type0
val hashed (a:alg) (b:hashable a) : Type0
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))
﻿(** computational assumption: collision resistance *)
module MiTLS.Hashing.CRF
open MiTLS

open MiTLS.Mem
include MiTLS.Hashing
open FStar.Bytes
/
prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Hashing.CRF.fst
a: MiTLS.Hashing.Spec.alg -> b: MiTLS.Hashing.hashable a -> Type0
MiTLS.Hashing.Spec.alg MiTLS.Hashing.hashable Prims.l_imp Prims.b2t MiTLS.Hashing.CRF.crf FStar.HyperStack.ST.witnessed FStar.Monotonic.DependentMap.contains MiTLS.Hashing.CRF.range MiTLS.Hashing.CRF.domain MiTLS.Hashing.CRF.inv MiTLS.Mem.tls_tables_region MiTLS.Hashing.CRF.table MiTLS.Hashing.CRF.Computed MiTLS.Hashing.tag MiTLS.Hashing.h
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))