val role_nonce (cs:role) (n:random) (r:HST.ex_rid{r <> root}) : Type0
val role_nonce (cs:role) (n:random) (r:HST.ex_rid{r <> root}) : Type0
let role_nonce cs n r = registered n r
﻿module MiTLS.Nonce

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
/
prims.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Random.fst.checked MiTLS.Mem.fst.checked FStar.UInt32.fsti.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.Bytes.fsti.checked
MiTLS.Nonce.fst

    cs: MiTLS.TLSConstants.role ->
    n: MiTLS.Nonce.random ->
    r: FStar.HyperStack.ST.ex_rid{r <> FStar.Monotonic.HyperHeap.root}
  -> Type0
MiTLS.TLSConstants.role 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 MiTLS.Nonce.registered
let role_nonce cs n r =
  
registered n r