val lookup: cs:role -> n:random -> ST (option (r:HST.ex_rid{r <> root}))
  (requires (fun h -> True))
  (ensures (fun _ _ _ -> True))
val lookup: cs:role -> n:random -> ST (option (r:HST.ex_rid{r <> root}))
  (requires (fun h -> True))
  (ensures (fun _ _ _ -> True))
let lookup role n = MDM.lookup nonce_rid_table n
﻿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

let role_nonce cs n r = registered n r

#reset-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1 --z3rlimit 10"

let rec mkHelloRandom cs r =
  HST.recall nonce_rid_table;
  let rand = Random.sample32 28ul in
  let ts = timestamp() in
  let n : random = ts @| rand in
  if ideal then
    match MDM.lookup nonce_rid_table n with
      | None   -> MDM.extend nonce_rid_table n r; n
      | Some _ -> mkHelloRandom cs r // formally retry to exclude collisions.
  else n
/
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
  -> FStar.HyperStack.ST.ST
    (FStar.Pervasives.Native.option (r:
          FStar.HyperStack.ST.ex_rid{r <> FStar.Monotonic.HyperHeap.root}))
MiTLS.TLSConstants.role MiTLS.Nonce.random FStar.Monotonic.DependentMap.lookup MiTLS.Nonce.n_rid MiTLS.Nonce.injective MiTLS.Mem.tls_tables_region MiTLS.Nonce.nonce_rid_table FStar.Pervasives.Native.option 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
let lookup role n =
  
MDM.lookup nonce_rid_table n