val new_region: parent:HST.erid -> ST (r:HST.ex_rid{r <> root})
  (requires (fun h -> True))
  (ensures (fun h0 r h1 ->
        HS.extends r parent /\
        HS.fresh_region r h0 h1 /\ //it's fresh with respect to the current heap
        fresh_region_nonce r h1))
val new_region: parent:HST.erid -> ST (r:HST.ex_rid{r <> root})
  (requires (fun h -> True))
  (ensures (fun h0 r h1 ->
        HS.extends r parent /\
        HS.fresh_region r h0 h1 /\ //it's fresh with respect to the current heap
        fresh_region_nonce r h1))
let new_region parent =
  HST.recall nonce_rid_table;
  let m0 = HST.op_Bang nonce_rid_table in
  HST.testify_forall_region_contains_pred 
    #(n:random{Some? (MDM.sel m0 n)}) #(fun n -> Some?.v (MDM.sel m0 n)) ();
  let r = new_region parent in
  HST.witness_region r;
  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

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

let lookup role n = MDM.lookup nonce_rid_table 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
parent: FStar.HyperStack.ST.erid
  -> FStar.HyperStack.ST.ST (r: FStar.HyperStack.ST.ex_rid{r <> FStar.Monotonic.HyperHeap.root})
FStar.HyperStack.ST.erid 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 Prims.unit FStar.HyperStack.ST.witness_region FStar.HyperStack.ST.new_region FStar.HyperStack.ST.testify_forall_region_contains_pred MiTLS.Nonce.random FStar.Pervasives.Native.uu___is_Some MiTLS.Nonce.n_rid FStar.Monotonic.DependentMap.sel FStar.Pervasives.Native.__proj__Some__item__v FStar.Monotonic.DependentMap.imap MiTLS.Nonce.injective FStar.HyperStack.ST.op_Bang FStar.Monotonic.DependentMap.grows MiTLS.Nonce.nonce_rid_table FStar.HyperStack.ST.recall
let new_region parent =
  
HST.recall nonce_rid_table;
let m0 = HST.op_Bang nonce_rid_table in
HST.testify_forall_region_contains_pred #(n: random{Some? (MDM.sel m0 n)})
  #(fun n -> Some?.v (MDM.sel m0 n))
  ();
let r = new_region parent in
HST.witness_region r;
r