val serialize32_ext
      (#k1: parser_kind)
      (#t1: Type)
      (p1: parser k1 t1)
      (s1: serializer p1)
      (s1': serializer32 s1)
      (#k2: parser_kind)
      (#t2: Type)
      (p2: parser k2 t2)
      (u: squash (t1 == t2 /\ (forall (input: bytes). parse p1 input == parse p2 input)))
    : Tot (serializer32 (serialize_ext p1 s1 p2))
let serialize32_ext
  (#k1: parser_kind)
  (#t1: Type)
  (p1: parser k1 t1)
  (s1: serializer p1)
  (s1': serializer32 s1)
  (#k2: parser_kind)
  (#t2: Type)
  (p2: parser k2 t2)
  (u: squash (t1 == t2 /\ (forall (input: bytes) . parse p1 input == parse p2 input)))
: Tot (serializer32 (serialize_ext p1 s1 p2))
= fun input -> s1' input
val serialize32_ext
      (#k1: parser_kind)
      (#t1: Type)
      (p1: parser k1 t1)
      (s1: serializer p1)
      (s1': serializer32 s1)
      (#k2: parser_kind)
      (#t2: Type)
      (p2: parser k2 t2)
      (u: squash (t1 == t2 /\ (forall (input: bytes). parse p1 input == parse p2 input)))
    : Tot (serializer32 (serialize_ext p1 s1 p2))
let serialize32_ext
      (#k1: parser_kind)
      (#t1: Type)
      (p1: parser k1 t1)
      (s1: serializer p1)
      (s1': serializer32 s1)
      (#k2: parser_kind)
      (#t2: Type)
      (p2: parser k2 t2)
      (u: squash (t1 == t2 /\ (forall (input: bytes). parse p1 input == parse p2 input)))
    : Tot (serializer32 (serialize_ext p1 s1 p2)) =
fun input -> s1' input
LowParse.SLow.Base.fst.checked
prims.fst.checked LowParse.Spec.Base.fsti.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked
LowParse.SLow.Base.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.SLow.Base.serializer32 Prims.squash Prims.l_and Prims.eq2 Prims.l_Forall LowParse.Bytes.bytes FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse LowParse.SLow.Base.bytes32 LowParse.SLow.Base.serializer32_correct LowParse.Spec.Base.serialize_ext
module LowParse.SLow.Base
include LowParse.Spec.Base

module B32 = LowParse.Bytes32
module U32 = FStar.UInt32

let bytes32 = B32.bytes

let parser32_correct
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input: bytes32)
  (res: option (t * U32.t))
: GTot Type0
= let gp = parse p (B32.reveal input) in
  match res with
  | None -> gp == None
  | Some (hres, consumed) ->
    Some? gp /\ (
      let (Some (hres' , consumed')) = gp in
      hres == hres' /\
      U32.v consumed == (consumed' <: nat)
    )

[@unifier_hint_injective]
inline_for_extraction
let parser32
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot Type
= (input: bytes32) -> Tot (res: option (t * U32.t) { parser32_correct p input res } )

let parser32_consumes
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
  (input: bytes32)
: Lemma
  (Some? (p32 input) ==> (let (Some (_, consumed)) = p32 input in U32.v consumed <= B32.length input))
= ()

let parser32_consumes'
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
  (input: bytes32)
: Lemma
  (match p32 input with
  | Some (_, consumed) -> U32.v consumed <= B32.length input
  | _ -> True)
= ()

inline_for_extraction
let make_parser32
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (p32: (input: bytes32) -> Pure (option (t * U32.t)) (requires True) (ensures (fun res -> parser32_correct p input res)))
: Tot (parser32 p)
= (fun (input: bytes32) -> (p32 input <: (res: option (t * U32.t) { parser32_correct p input res } )))

inline_for_extraction
let coerce_parser32
  (t2: Type)
  (#k: parser_kind)
  (#t1: Type)
  (#p: parser k t1)
  (p32: parser32 p)
  (u: unit { t2 == t1 } )
: Tot (parser32 (coerce_parser t2 p))
= p32

let validator_correct
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (input: bytes32)
  (res: option U32.t)
: GTot Type0
= let gp = parse p (B32.reveal input) in
  match res with
  | None -> gp == None
  | Some (consumed) ->
    Some? gp /\ (
      let (Some (_ , consumed')) = gp in
      U32.v consumed == (consumed' <: nat)
    )

let validator
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
: Tot Type
= (input: bytes32) -> Tot (res: option U32.t { validator_correct p input res } )

let serializer32_correct
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (input: t)
  (res: bytes32)
: GTot Type0
= B32.reveal res == s input

let serializer32_correct'
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (input: t)
  (res: bytes32)
: GTot Type0
= B32.reveal res `bytes_equal` s input

[@unifier_hint_injective]
inline_for_extraction
let serializer32
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
: Tot Type
= (input: t) -> Tot (res: bytes32 { serializer32_correct s input res } )

let serializer32_correct_length
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (input: t)
  (res: bytes32)
: Lemma
  (requires (serializer32_correct s input res))
  (ensures (
    let len = FStar.Bytes.length res in
    k.parser_kind_low <= len /\ (
    match k.parser_kind_high with
    | Some max -> len <= max
    | _ -> True
  )))
  [SMTPat (serializer32_correct s input res); SMTPat (FStar.Bytes.length res)]
= serialize_length s input

inline_for_extraction
let serialize32_ext
  (#k1: parser_kind)
  (#t1: Type)
  (p1: parser k1 t1)
  (s1: serializer p1)
  (s1': serializer32 s1)
  (#k2: parser_kind)
  (#t2: Type)
  (p2: parser k2 t2)
  (u: squash (t1 == t2 /\ (forall (input: bytes) . parse p1 input == parse p2 input)))
val serialize32_ext
      (#k1: parser_kind)
      (#t1: Type)
      (p1: parser k1 t1)
      (s1: serializer p1)
      (s1': serializer32 s1)
      (#k2: parser_kind)
      (#t2: Type)
      (p2: parser k2 t2)
      (u: squash (t1 == t2 /\ (forall (input: bytes). parse p1 input == parse p2 input)))
    : Tot (serializer32 (serialize_ext p1 s1 p2))

    p1: LowParse.Spec.Base.parser k1 t1 ->
    s1: LowParse.Spec.Base.serializer p1 ->
    s1': LowParse.SLow.Base.serializer32 s1 ->
    p2: LowParse.Spec.Base.parser k2 t2 ->
    u75:
      Prims.squash (t1 == t2 /\
          (forall (input: LowParse.Bytes.bytes).
              LowParse.Spec.Base.parse p1 input == LowParse.Spec.Base.parse p2 input))
  -> LowParse.SLow.Base.serializer32 (LowParse.Spec.Base.serialize_ext p1 s1 p2)