val wrap_serializer32_constant_length_precond
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (#s: serializer p)
      (s32: serializer32 s)
      (len: nat)
    : GTot Type0
val wrap_serializer32_constant_length_precond
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (#s: serializer p)
      (s32: serializer32 s)
      (len: nat)
    : GTot Type0
let wrap_serializer32_constant_length_precond
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (#s: serializer p)
  (s32: serializer32 s)
  (len: nat)
: GTot Type0
= k.parser_kind_high == Some k.parser_kind_low /\
  k.parser_kind_low == len
module MiTLS.LowParseWrappers
open MiTLS
include MiTLS.TLSError // for AD_decode_error
include FStar.Error // for Correct, Error
include MiTLS.Parse // for pinverse, lemma_(p?)inverse_*, etc.
open LowParse.SLow.Base
include FStar.Bytes // for bytes, lbytes, length, equal

#reset-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection' --z3rlimit 16 --z3cliopt smt.arith.nl=false --max_fuel 2 --max_ifuel 2"
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Parse.fst.checked LowParse.SLow.Base.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.LowParseWrappers.fst
s32: LowParse.SLow.Base.serializer32 s -> len: Prims.nat -> Prims.GTot Type0
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.SLow.Base.serializer32 Prims.nat Prims.l_and Prims.eq2 FStar.Pervasives.Native.option LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_high FStar.Pervasives.Native.Some LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_low
let wrap_serializer32_constant_length_precond
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (#s: serializer p)
      (s32: serializer32 s)
      (len: nat)
    : GTot Type0 =
  
k.parser_kind_high == Some k.parser_kind_low /\ k.parser_kind_low == len