val reveal (#l: _) (b: lbytes l) : (QUIC.Spec.lbytes l)
let reveal #l (b:lbytes l) : (QUIC.Spec.lbytes l) =
  Seq.init l (fun i -> Lib.RawIntTypes.u8_to_UInt8 (Seq.index b i))
val reveal (#l: _) (b: lbytes l) : (QUIC.Spec.lbytes l)
let reveal #l (b: lbytes l) : (QUIC.Spec.lbytes l) =
Seq.init l (fun i -> Lib.RawIntTypes.u8_to_UInt8 (Seq.index b i))
Model.Helpers.fsti.checked
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
Prims.nat Model.Helpers.lbytes FStar.Seq.Base.init FStar.UInt8.t Prims.b2t Prims.op_LessThan Lib.RawIntTypes.u8_to_UInt8 FStar.Seq.Base.index Lib.IntTypes.uint8 QUIC.Spec.Base.lbytes
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)
val reveal (#l: _) (b: lbytes l) : (QUIC.Spec.lbytes l)
b: Model.Helpers.lbytes l -> QUIC.Spec.Base.lbytes l