val wrap_serializer32_constant_length
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (#s: serializer p)
      (s32: serializer32 s)
      (len: nat)
      (u: unit{wrap_serializer32_constant_length_precond s32 len})
      (x: t)
    : Tot (lbytes len)
val wrap_serializer32_constant_length
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (#s: serializer p)
      (s32: serializer32 s)
      (len: nat)
      (u: unit{wrap_serializer32_constant_length_precond s32 len})
      (x: t)
    : Tot (lbytes len)
let wrap_serializer32_constant_length
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (#s: serializer p)
  (s32: serializer32 s)
  (len: nat)
  (u: unit { wrap_serializer32_constant_length_precond s32 len } )
  (x: t)
: Tot (lbytes len)
= [@inline_let]
  let y = s32 x in
  [@inline_let]
  let _ =
    serialize_length s x;
    le_antisym (length y) len
  in
  y
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"

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

private
let le_antisym
  (x y: int)
: Lemma
  (requires (x <= y /\ y <= x))
  (ensures (x == y))
= ()
/
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 ->
    u40: u42: Prims.unit{MiTLS.LowParseWrappers.wrap_serializer32_constant_length_precond s32 len} ->
    x: t
  -> FStar.Bytes.lbytes len
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.SLow.Base.serializer32 Prims.nat Prims.unit MiTLS.LowParseWrappers.wrap_serializer32_constant_length_precond MiTLS.LowParseWrappers.le_antisym FStar.Bytes.length LowParse.Spec.Base.serialize_length LowParse.SLow.Base.bytes32 LowParse.SLow.Base.serializer32_correct FStar.Bytes.lbytes
let wrap_serializer32_constant_length
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (#s: serializer p)
      (s32: serializer32 s)
      (len: nat)
      (u: unit{wrap_serializer32_constant_length_precond s32 len})
      (x: t)
    : Tot (lbytes len) =
  
[@@ inline_let ]let y = s32 x in
[@@ inline_let ]let _ =
  serialize_length s x;
  le_antisym (length y) len
in
y