val registered : n: MiTLS.Nonce.random -> r: FStar.HyperStack.ST.ex_rid{r <> FStar.Monotonic.HyperHeap.root}
  -> Prims.logical
let registered (n:random) (r:HST.ex_rid{r <> root}) =
  HST.witnessed (HST.region_contains_pred r) /\
  HST.witnessed (MDM.contains nonce_rid_table n r)
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,
// if it maps distinct nonces to distinct rids
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)

//nonce_rid_table:
//  A monotone, injective partial map in the tls_tables_region, from random to rid
//  Essentially: m:(r:random  -> Tot (n_rid r)) {injective m}
//  Equivalently m:(random  -> Tot rid) {injective m}
//We could conditionally allocate this table based on the ideal flag
//See the style, e.g., in StreamAE
//However, in this case, we have just a single global table and the additional
//allocation seems rather mild. Still, would be nice to do remove this allocation someday.
let nonce_rid_table : MDM.t tls_tables_region random n_rid injective =
  MDM.alloc ()

//A nonce n is fresh in h if the nonce_rid_table doesn't contain it
let fresh (n:random) (h:HS.mem) = MDM.sel (HS.sel h nonce_rid_table) n = None

//A region is fresh if no nonce is associated with it
let fresh_region_nonce (r:HST.ex_rid{r <> root}) (h:HS.mem) : GTot Type0 =
  forall n. Some r <> MDM.sel (HS.sel h nonce_rid_table) n

//A nonce n is registered to region r, if the table contains n -> Some r;
/
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: MiTLS.Nonce.random -> r: FStar.HyperStack.ST.ex_rid{r <> FStar.Monotonic.HyperHeap.root}
  -> Prims.logical
MiTLS.Nonce.random FStar.HyperStack.ST.ex_rid Prims.b2t Prims.op_disEquality FStar.Monotonic.HyperHeap.rid Prims.l_or FStar.HyperStack.ST.is_eternal_region Prims.l_and Prims.eq2 Prims.int FStar.Monotonic.HyperHeap.color Prims.op_Negation FStar.Monotonic.HyperHeap.rid_freeable FStar.Monotonic.HyperHeap.root FStar.HyperStack.ST.witnessed FStar.HyperStack.ST.region_contains_pred FStar.Monotonic.DependentMap.contains MiTLS.Nonce.n_rid MiTLS.Nonce.injective MiTLS.Mem.tls_tables_region MiTLS.Nonce.nonce_rid_table Prims.logical
let registered (n: random) (r: HST.ex_rid{r <> root}) =
  
HST.witnessed (HST.region_contains_pred r) /\ HST.witnessed (MDM.contains nonce_rid_table n r)