val mkHelloRandom: cs:role -> r:HST.ex_rid{r <> root} -> ST random
  (requires (fun h -> fresh_region_nonce r h))
  (ensures (fun h0 n h1 ->
    let nonce_rid_table_as_hsref =  nonce_rid_table in
    HS.modifies (Set.singleton tls_tables_region) h0 h1 /\ //modifies at most the tables region
    HS.modifies_ref tls_tables_region (Set.singleton (HS.as_addr nonce_rid_table_as_hsref)) h0 h1 /\ //and within it, at most the nonce_rid_table
    (b2t ideal ==> 
      fresh n h0 /\        //if we're ideal then the nonce is fresh
      registered n r /\     //the nonce n is associated with r
      role_nonce cs n r)))
val mkHelloRandom: cs:role -> r:HST.ex_rid{r <> root} -> ST random
  (requires (fun h -> fresh_region_nonce r h))
  (ensures (fun h0 n h1 ->
    let nonce_rid_table_as_hsref =  nonce_rid_table in
    HS.modifies (Set.singleton tls_tables_region) h0 h1 /\ //modifies at most the tables region
    HS.modifies_ref tls_tables_region (Set.singleton (HS.as_addr nonce_rid_table_as_hsref)) h0 h1 /\ //and within it, at most the nonce_rid_table
    (b2t ideal ==> 
      fresh n h0 /\        //if we're ideal then the nonce is fresh
      registered n r /\     //the nonce n is associated with r
      role_nonce cs n r)))
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
﻿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"
/
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 -> r: FStar.HyperStack.ST.ex_rid{r <> FStar.Monotonic.HyperHeap.root}
  -> FStar.HyperStack.ST.ST MiTLS.Nonce.random
MiTLS.TLSConstants.role 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.ideal MiTLS.Nonce.random Prims.unit FStar.Monotonic.DependentMap.extend MiTLS.Nonce.n_rid MiTLS.Nonce.injective MiTLS.Mem.tls_tables_region MiTLS.Nonce.nonce_rid_table MiTLS.Nonce.mkHelloRandom FStar.Pervasives.Native.option FStar.Monotonic.DependentMap.lookup Prims.bool FStar.Bytes.op_At_Bar FStar.Bytes.lbytes MiTLS.Nonce.timestamp FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t MiTLS.Random.sample32 FStar.UInt32.__uint_to_t FStar.HyperStack.ST.recall FStar.Monotonic.DependentMap.imap FStar.Monotonic.DependentMap.grows
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
else n