val parser32_correct
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (input: bytes32)
      (res: option (t * U32.t))
    : GTot Type0
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)
    )
val parser32_correct
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (input: bytes32)
      (res: option (t * U32.t))
    : GTot Type0
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))
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.eq2 LowParse.Spec.Base.consumed_length FStar.Bytes.reveal FStar.Pervasives.Native.None Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_Some Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n FStar.UInt32.v Prims.nat Prims.logical LowParse.Spec.Base.parse
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))
val parser32_correct
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (input: bytes32)
      (res: option (t * U32.t))
    : GTot Type0

    p: LowParse.Spec.Base.parser k t ->
    input: LowParse.SLow.Base.bytes32 ->
    res: FStar.Pervasives.Native.option (t * FStar.UInt32.t)
  -> Prims.GTot Type0