val lemma_inverse_serializer32_parser32_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})
      (p32: parser32 p)
      (msg: string)
      (x: t)
    : Lemma
    (lemma_inverse_g_f (wrap_serializer32_constant_length s32 len u)
        (wrap_parser32_constant_length s32 len u p32 msg)
        x)
val lemma_inverse_serializer32_parser32_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})
      (p32: parser32 p)
      (msg: string)
      (x: t)
    : Lemma
    (lemma_inverse_g_f (wrap_serializer32_constant_length s32 len u)
        (wrap_parser32_constant_length s32 len u p32 msg)
        x)
let lemma_inverse_serializer32_parser32_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 } )
  (p32: parser32 p)
  (msg: string)
  (x: t)
: Lemma
  (lemma_inverse_g_f (wrap_serializer32_constant_length s32 len u) (wrap_parser32_constant_length s32 len u p32 msg) x)
= serializer32_then_parser32 s p32 s32 x
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))
= ()

inline_for_extraction
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

inline_for_extraction
let wrap_parser32_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 } )
  (p32: parser32 p)
  (msg: string)
: Tot (pinverse_t (wrap_serializer32_constant_length s32 len u))
= fun (x: lbytes len) ->
  match p32 x with
  | Some (y, _) -> Correct y
  | _ -> fatal Decode_error msg

let bytes_equal_intro
  (b1 b2: bytes)
: Lemma
  (requires (reveal b1 == reveal b2))
  (ensures (equal b1 b2))
= ()

let wrap_parser32_total_constant_length_precond
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (p32: parser32 p)
  (len: nat)
: GTot Type0
= k.parser_kind_high == Some k.parser_kind_low /\
  k.parser_kind_low == len /\
  k.parser_kind_metadata == Some ParserKindMetadataTotal

inline_for_extraction
let wrap_parser32_total_constant_length
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (#s: serializer p)
  (s32: serializer32 s)
  (p32: parser32 p)
  (len: nat)
  (u: unit { wrap_parser32_total_constant_length_precond p32 len } )
  (x: lbytes len)
: Tot (y: t { s32 y == x } )
= [@inline_let] let _ = parser_kind_prop_equiv k p in
  match p32 x with
  | Some (y, consumed) ->
    [@inline_let]
    let _ = parser32_then_serializer32' p32 s32 x y consumed in
    y

let lemma_pinverse_serializer32_parser32_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 } )
  (p32: parser32 p)
  (msg: string)
  (x: lbytes len)
: Lemma
  (lemma_pinverse_f_g #t #(lbytes len) eq2 (wrap_serializer32_constant_length s32 len u) (wrap_parser32_constant_length s32 len u p32 msg) x)
= if (Some? (p32 x))
  then begin
    let (Some (y, consumed)) = p32 x in
    parser32_then_serializer32' p32 s32 x y consumed
  end else ()
/
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 ->
    u152: u158: Prims.unit{MiTLS.LowParseWrappers.wrap_serializer32_constant_length_precond s32 len} ->
    p32: LowParse.SLow.Base.parser32 p ->
    msg: Prims.string ->
    x: t
  -> FStar.Pervasives.Lemma
    (ensures
      MiTLS.Parse.lemma_inverse_g_f (MiTLS.LowParseWrappers.wrap_serializer32_constant_length s32
            len
            u152)
        (MiTLS.LowParseWrappers.wrap_parser32_constant_length s32 len u152 p32 msg)
        x)
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 LowParse.SLow.Base.parser32 Prims.string LowParse.SLow.Base.serializer32_then_parser32 Prims.l_True Prims.squash MiTLS.Parse.lemma_inverse_g_f FStar.Bytes.lbytes MiTLS.LowParseWrappers.wrap_serializer32_constant_length MiTLS.LowParseWrappers.wrap_parser32_constant_length Prims.Nil FStar.Pervasives.pattern
let lemma_inverse_serializer32_parser32_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})
      (p32: parser32 p)
      (msg: string)
      (x: t)
    : Lemma
    (lemma_inverse_g_f (wrap_serializer32_constant_length s32 len u)
        (wrap_parser32_constant_length s32 len u p32 msg)
        x) =
  
serializer32_then_parser32 s p32 s32 x