val 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)
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 } )))
val 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)
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})))
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.SLow.Base.bytes32 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 FStar.UInt32.t Prims.l_True LowParse.SLow.Base.parser32_correct LowParse.SLow.Base.parser32
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)))
val 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)

    p: LowParse.Spec.Base.parser k t ->
    p32:
      (input: LowParse.SLow.Base.bytes32
          -> Prims.Pure (FStar.Pervasives.Native.option (t * FStar.UInt32.t)))
  -> LowParse.SLow.Base.parser32 p