val injective : n: FStar.Monotonic.DependentMap.partial_dependent_map MiTLS.Nonce.random MiTLS.Nonce.n_rid
  -> Prims.logical
let injective (n:MDM.partial_dependent_map random n_rid) =
  forall n1 n2. n1=!=n2 ==> (match DM.sel n n1, DM.sel n n2 with
        | Some r1, Some r2 -> r1 <> r2
        | _ -> True)
module MiTLS.Nonce
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open MiTLS.TLSConstants

module HS = FStar.HyperStack
module DM = FStar.DependentMap
module MDM = FStar.Monotonic.DependentMap
module HST = FStar.HyperStack.ST

type random = lbytes 32

inline_for_extraction
let ideal = Flags.ideal_Nonce // controls idealization of random sample: collision-avoidance.

let timestamp: unit -> ST (lbytes 4)
  (requires (fun h0 -> True))
  (ensures (fun h0 _ h1 -> HS.modifies Set.empty h0 h1)) =
  fun () ->
  let time = FStar.Date.secondsFromDawn () in
  lemma_repr_bytes_values time;
  //assume(Platform.Bytes.repr_bytes time = FStar.Bytes.repr_bytes time);// temporary
  bytes_of_int 4 time

// ex_rid: The type of a region id that is known
//         to exist in the current heap and in every future one
//2018.03.09 SZ: Excluded the case r = root
type ex_rid = r:HST.ex_rid{r <> root}

// MDM.map provide a dependent map type;
// In this case, we don't need the dependencey
// The n_rid type has a trivial depdendence on (n:random)
let n_rid = fun (n:random) -> (r:HST.ex_rid{r <> root})

// A partial map from nonces to rid is injective,
/
prims.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Mem.fst.checked MiTLS.Flags.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.DependentMap.fsti.checked FStar.Date.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Nonce.fsti
n: FStar.Monotonic.DependentMap.partial_dependent_map MiTLS.Nonce.random MiTLS.Nonce.n_rid
  -> Prims.logical
FStar.Monotonic.DependentMap.partial_dependent_map MiTLS.Nonce.random MiTLS.Nonce.n_rid Prims.l_Forall Prims.l_imp Prims.l_not Prims.eq2 FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option FStar.DependentMap.sel FStar.Monotonic.DependentMap.opt Prims.b2t Prims.op_disEquality FStar.HyperStack.ST.ex_rid Prims.l_or FStar.Monotonic.HyperHeap.rid FStar.HyperStack.ST.is_eternal_region Prims.l_and Prims.int FStar.Monotonic.HyperHeap.color Prims.op_Negation FStar.Monotonic.HyperHeap.rid_freeable FStar.Monotonic.HyperHeap.root FStar.Pervasives.Native.tuple2 Prims.l_True Prims.logical
let injective (n: MDM.partial_dependent_map random n_rid) =
  
forall n1 n2.
  n1 =!= n2 ==>
  (match DM.sel n n1, DM.sel n n2 with
    | Some r1, Some r2 -> r1 <> r2
    | _ -> True)