val hide (b: Seq.seq UInt8.t) : lbytes (Seq.length b)
val hide (b: Seq.seq UInt8.t) : lbytes (Seq.length b)
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))
module Model.Helpers

let lbytes (l:nat) = b:Seq.seq Lib.IntTypes.uint8 { Seq.length b = l }
/
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
b: FStar.Seq.Base.seq FStar.UInt8.t -> Model.Helpers.lbytes (FStar.Seq.Base.length b)
FStar.Seq.Base.seq FStar.UInt8.t FStar.Seq.Base.init Lib.IntTypes.uint8 FStar.Seq.Base.length Prims.nat Prims.b2t Prims.op_LessThan Lib.RawIntTypes.u8_from_UInt8 FStar.Seq.Base.index Model.Helpers.lbytes
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))