val stop (#a: Type) (s: string) : ST a (requires (fun h -> True)) (ensures (fun h0 r h1 -> False))
val stop (#a: Type) (s: string) : ST a (requires (fun h -> True)) (ensures (fun h0 r h1 -> False))
let rec stop (#a:Type) (s:string) : ST a
  (requires (fun h -> True))
  (ensures (fun h0 r h1 -> False)) = stop s
(** 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}

private let inv (f:MDM.partial_dependent_map range domain) = True // a bit overkill?
private let table : MDM.t tls_tables_region range domain inv = MDM.alloc()

// witnessing that we hashed this particular content (for collision detection)
// to be replaced by a witness of inclusion in a global table of all hash computations.
// (not sure how to manage that table)

//val hashed: a:alg -> b:bytes -> Type
val hashed (a:alg) (b:hashable a) : Type0

val crf_injective (a:alg) (b0 b1:hashable a): ST unit  // should be STTot
  (requires fun h0 -> hashed a b0 /\ hashed a b1)
  (ensures fun t0 _ t1 -> t0 == t1 /\ (crf a /\ h a b0 =  h a b1 ==> b0 = b1))

/// We use [stop] to model the exclusion of "bad" events, in this case
/// a hash collision.  We should review this "flagless" style for
/// crypto modelling.
/
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
s: Prims.string -> FStar.HyperStack.ST.ST a
Prims.string MiTLS.Hashing.CRF.stop FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_False
let rec stop (#a: Type) (s: string)
    : ST a (requires (fun h -> True)) (ensures (fun h0 r h1 -> False)) =
  
stop s