val serialize_seq_flbytes_correct (sz: nat)
    : Lemma (serializer_correct (parse_seq_flbytes sz) (serialize_seq_flbytes' sz))
let serialize_seq_flbytes_correct
  (sz: nat)
: Lemma
  (serializer_correct (parse_seq_flbytes sz) (serialize_seq_flbytes' sz))
= let prf
    (input: Seq.lseq byte sz)
  : Lemma
    (
      let ser = serialize_seq_flbytes' sz input in
      Seq.length ser == sz /\
      parse (parse_seq_flbytes sz) ser == Some (input, sz)
    )
  = ()
  in
  Classical.forall_intro prf
val serialize_seq_flbytes_correct (sz: nat)
    : Lemma (serializer_correct (parse_seq_flbytes sz) (serialize_seq_flbytes' sz))
let serialize_seq_flbytes_correct (sz: nat)
    : Lemma (serializer_correct (parse_seq_flbytes sz) (serialize_seq_flbytes' sz)) =
let prf (input: Seq.lseq byte sz)
    : Lemma
    (let ser = serialize_seq_flbytes' sz input in
      Seq.length ser == sz /\ parse (parse_seq_flbytes sz) ser == Some (input, sz)) =
  ()
in
Classical.forall_intro prf
LowParse.Spec.SeqBytes.Base.fst.checked
prims.fst.checked LowParse.Spec.FLData.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.SeqBytes.Base.fst
Prims.nat FStar.Classical.forall_intro FStar.Seq.Properties.lseq LowParse.Bytes.byte Prims.l_and Prims.eq2 FStar.Seq.Base.length LowParse.Spec.SeqBytes.Base.serialize_seq_flbytes' FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse LowParse.Spec.SeqBytes.Base.parse_seq_flbytes FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern LowParse.Bytes.bytes LowParse.Spec.Base.serializer_correct LowParse.Spec.Base.total_constant_size_parser_kind
module LowParse.Spec.SeqBytes.Base
include LowParse.Spec.FLData

let parse_seq_flbytes_gen
  (sz: nat)
  (s: bytes { Seq.length s == sz } )
: Tot (Seq.lseq byte sz)
= s

let tot_parse_seq_flbytes
  (sz: nat)
: Tot (tot_parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
= tot_make_total_constant_size_parser sz (Seq.lseq byte sz) (parse_seq_flbytes_gen sz)

let parse_seq_flbytes
  (sz: nat)
: Tot (parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
= tot_parse_seq_flbytes sz

let serialize_seq_flbytes'
  (sz: nat)
: Tot (bare_serializer (Seq.lseq byte sz))
= fun (x: Seq.lseq byte sz) -> (
    x
  )

let serialize_seq_flbytes_correct
  (sz: nat)
: Lemma
val serialize_seq_flbytes_correct (sz: nat)
    : Lemma (serializer_correct (parse_seq_flbytes sz) (serialize_seq_flbytes' sz))
sz: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serializer_correct (LowParse.Spec.SeqBytes.Base.parse_seq_flbytes sz)
        (LowParse.Spec.SeqBytes.Base.serialize_seq_flbytes' sz))