val timestamp: unit
  -> ST (lbytes 4)
      (requires (fun h0 -> True))
      (ensures (fun h0 _ h1 -> HS.modifies Set.empty h0 h1))
val timestamp: unit
  -> ST (lbytes 4)
      (requires (fun h0 -> True))
      (ensures (fun h0 _ h1 -> HS.modifies Set.empty h0 h1))
let timestamp: unit -> ST (lbytes 4)
  (requires (fun h0 -> True))
  (ensures (fun h0 _ h1 -> HS.modifies Set.empty h0 h1)) =
  fun () ->
  let time = FStar.Date.secondsFromDawn () in
  lemma_repr_bytes_values time;
  //assume(Platform.Bytes.repr_bytes time = FStar.Bytes.repr_bytes time);// temporary
  bytes_of_int 4 time
module MiTLS.Nonce
open MiTLS

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

type random = lbytes 32

inline_for_extraction
let ideal = Flags.ideal_Nonce // controls idealization of random sample: collision-avoidance.
/
prims.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Mem.fst.checked MiTLS.Flags.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.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.DependentMap.fsti.checked FStar.Date.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Nonce.fsti
_: Prims.unit -> FStar.HyperStack.ST.ST (FStar.Bytes.lbytes 4)
Prims.unit FStar.Bytes.bytes_of_int FStar.Bytes.lemma_repr_bytes_values FStar.Bytes.lbytes Prims.nat Prims.b2t Prims.op_LessThan Prims.pow2 FStar.Date.secondsFromDawn
let timestamp: unit
  -> ST (lbytes 4)
      (requires (fun h0 -> True))
      (ensures (fun h0 _ h1 -> HS.modifies Set.empty h0 h1)) =
  
fun () ->
  let time = FStar.Date.secondsFromDawn () in
  lemma_repr_bytes_values time;
  bytes_of_int 4 time