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))
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))
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)
  )
﻿(** 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))
/
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 -> b0: MiTLS.Hashing.hashable a -> b1: MiTLS.Hashing.hashable a
  -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.Hashing.Spec.alg MiTLS.Hashing.hashable MiTLS.Hashing.CRF.crf FStar.HyperStack.ST.testify 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.h Prims.unit FStar.Monotonic.DependentMap.imap FStar.HyperStack.ST.op_Bang FStar.Monotonic.DependentMap.grows FStar.HyperStack.ST.recall Prims.bool
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))