val random (l: nat{l < pow2 32})
    : HyperStack.ST.ST (lbytes l) (requires fun h0 -> True) (ensures fun h0 _ h1 -> h0 == h1)
val random (l: nat{l < pow2 32})
    : HyperStack.ST.ST (lbytes l) (requires fun h0 -> True) (ensures fun h0 _ h1 -> h0 == h1)
let random (l: nat { l < pow2 32 })
  : HyperStack.ST.ST (lbytes l)
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> h0 == h1)
  =
  let open Lib.RandomSequence in
  snd (crypto_random entropy0 l)
module Model.Helpers

let lbytes (l:nat) = b:Seq.seq Lib.IntTypes.uint8 { Seq.length b = l }

let hide (b:Seq.seq UInt8.t) : lbytes (Seq.length b) =
  Seq.init (Seq.length b) (fun i -> Lib.RawIntTypes.u8_from_UInt8 (Seq.index b i))

let hide_eq (b:Seq.seq UInt8.t) : Lemma
  (ensures hide b == QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b)
  [ SMTPat (QUIC.Secret.Seq.seq_hide #Lib.IntTypes.U8 b) ]
= 
  assert (hide b `Seq.equal` QUIC.Secret.Seq.seq_hide b)

let reveal #l (b:lbytes l) : (QUIC.Spec.lbytes l) =
  Seq.init l (fun i -> Lib.RawIntTypes.u8_to_UInt8 (Seq.index b i)) 

let reveal_eq (b:Seq.seq Lib.IntTypes.uint8): Lemma
  (ensures reveal #(Seq.length b) b == QUIC.Secret.Seq.seq_reveal b)
  [ SMTPat (QUIC.Secret.Seq.seq_reveal b) ]
= 
  assert (reveal #(Seq.length b) b `Seq.equal` QUIC.Secret.Seq.seq_reveal b)


val correct (#l: nat) (b:Seq.seq UInt8.t{Seq.length b = l})
  : Lemma (reveal #l (hide b) == b)
  [SMTPat (reveal #l (hide b))]

val correct2 (#l: nat) (b:lbytes l)
  : Lemma (hide (reveal #l b) == b)
  [SMTPat (hide (reveal #l b))]
/
QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.RandomSequence.fsti.checked Lib.IntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked
Model.Helpers.fsti
l: Prims.nat{l < Prims.pow2 32} -> FStar.HyperStack.ST.ST (Model.Helpers.lbytes l)
Prims.nat Prims.b2t Prims.op_LessThan Prims.pow2 FStar.Pervasives.Native.snd Lib.RandomSequence.entropy Lib.ByteSequence.lbytes Lib.RandomSequence.crypto_random Lib.RandomSequence.entropy0 Model.Helpers.lbytes FStar.Monotonic.HyperStack.mem Prims.l_True Prims.eq2
let random (l: nat{l < pow2 32})
    : HyperStack.ST.ST (lbytes l) (requires fun h0 -> True) (ensures fun h0 _ h1 -> h0 == h1) =
  
let open Lib.RandomSequence in snd (crypto_random entropy0 l)