val of_bytes (b:BS.bytes) : Tot (s:seq UInt8.t{b === s /\ length b == length s})
let of_bytes b = b
val of_bytes (b:BS.bytes) : Tot (s:seq UInt8.t{b === s /\ length b == length s})
let of_bytes b =
b
Vale.Arch.BufferFriend.fst.checked
Vale.Wrapper.X64.Poly.fsti.checked Vale.Poly1305.Util.fsti.checked Vale.Lib.Seqs_s.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked prims.fst.checked LowStar.BufferView.Up.fst.checked Lib.RawIntTypes.fst.checked Lib.IntTypes.fst.checked Lib.ByteSequence.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Endianness.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Arch.BufferFriend.fst
Lib.ByteSequence.bytes FStar.Seq.Base.seq FStar.UInt8.t Prims.l_and Prims.op_Equals_Equals_Equals Prims.eq2 Prims.nat FStar.Seq.Base.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC
module Vale.Arch.BufferFriend
open FStar.Mul
friend Lib.IntTypes
friend Lib.RawIntTypes
friend Lib.ByteSequence
friend LowStar.BufferView.Up
friend FStar.Endianness

module PU = Vale.Poly1305.Util
module IT = Vale.Interop.Types
module PS = Vale.Wrapper.X64.Poly
module BS = Lib.ByteSequence
module Raw = Lib.RawIntTypes

unfold let (.[]) = index
val of_bytes (b:BS.bytes) : Tot (s:seq UInt8.t{b === s /\ length b == length s})
b: Lib.ByteSequence.bytes
  -> s:
    FStar.Seq.Base.seq FStar.UInt8.t {b === s /\ FStar.Seq.Base.length b == FStar.Seq.Base.length s}