val inv : f:
      FStar.Monotonic.DependentMap.partial_dependent_map MiTLS.Hashing.CRF.range
        MiTLS.Hashing.CRF.domain
  -> Prims.logical
let inv (f:MDM.partial_dependent_map range domain) = True
(** computational assumption: collision resistance *)
module MiTLS.Hashing.CRF
open MiTLS

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

//2018.04.24 SZ: to be moved elsewhere, set to false for real extraction
inline_for_extraction
let crf (_:alg) = false

(* Depending on a single, global idealization function, we keep a global
    inverse table for all (finalized) hash computations, and we use it to
    detect concrete collisions. Technically, this is modelled as
    non-termination of a stateful, partially-correct finalize filter.
    This may depend on some prior flag to keep the hashed input in the
    incremental hash implementation. (This is always the case for now.)  *)

module MDM = FStar.Monotonic.DependentMap 

// the precise types guarantee that the table stays empty when crf _ = false
private type range = | Computed: a: alg {crf a} -> t: tag a -> range
private type domain (r:range) =
  b:bytes {let Computed a t = r in length b `less_than_max_input_length` a /\ h a b = t}
/
prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.fsti.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Hashing.CRF.fsti

    f:
      FStar.Monotonic.DependentMap.partial_dependent_map MiTLS.Hashing.CRF.range
        MiTLS.Hashing.CRF.domain
  -> Prims.logical
FStar.Monotonic.DependentMap.partial_dependent_map MiTLS.Hashing.CRF.range MiTLS.Hashing.CRF.domain Prims.l_True Prims.logical
let inv (f: MDM.partial_dependent_map range domain) =
  
True