val nonce_id_table:MDM.t tls_tables_region random n_id (fun x -> True)
val nonce_id_table:MDM.t tls_tables_region random n_id (fun x -> True)
let nonce_id_table : MDM.t tls_tables_region random n_id (fun x -> True) =
  MDM.alloc ()
(* This module maintains a injective monotonic map from nonces to ids *)
module MiTLS.IdNonce
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open MiTLS.TLSConstants
open MiTLS.TLSInfo

module N= MiTLS.Nonce
module MDM = FStar.Monotonic.DependentMap
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

//The goal of the rest of the module is to provide id_of_nonce
//and to prove that the two are mutual inverses
type n_id (n:random) = i:id{nonce_of_id i = n}

//nonce_id_table:
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Nonce.fsti.checked MiTLS.Mem.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.Bytes.fsti.checked
MiTLS.IdNonce.fst
FStar.Monotonic.DependentMap.t MiTLS.Mem.tls_tables_region
  MiTLS.TLSInfo.random
  MiTLS.IdNonce.n_id
  (fun _ -> Prims.l_True)
FStar.Monotonic.DependentMap.alloc MiTLS.TLSInfo.random MiTLS.IdNonce.n_id FStar.DependentMap.t FStar.Monotonic.DependentMap.opt Prims.l_True MiTLS.Mem.tls_tables_region FStar.Monotonic.DependentMap.t
let nonce_id_table:MDM.t tls_tables_region random n_id (fun x -> True) =
  
MDM.alloc ()