val parse32_bcvli:parser32 parse_bcvli
let parse32_bcvli
: parser32 parse_bcvli
= fun input -> ((
    [@inline_let] let _ =
      parse_bcvli_eq (B32.reveal input)
    in
    match parse32_bounded_integer_le_1 input with
    | None -> None
    | Some (x32, consumed_x) ->
      if x32 `U32.lt` 253ul
      then Some (x32, consumed_x)
      else
        let input' = B32.slice input consumed_x (B32.len input) in
        if x32 = 253ul
        then
          match parse32_bounded_integer_le_2 input' with
          | None -> None
          | Some (y, consumed_y) ->
            if y `U32.lt` 253ul then None else Some (y, consumed_x `U32.add` consumed_y)
        else if x32 = 254ul
        then
          match parse32_bounded_integer_le_4 input' with
          | None -> None
          | Some (y, consumed_y) ->
            if y `U32.lt` 65536ul then None else Some (y, consumed_x `U32.add` consumed_y)
        else
          None
  ) <: (res: _ { parser32_correct parse_bcvli input res } ))
val parse32_bcvli:parser32 parse_bcvli
let parse32_bcvli:parser32 parse_bcvli =
fun input ->
  (([@@ inline_let ]let _ = parse_bcvli_eq (B32.reveal input) in
      match parse32_bounded_integer_le_1 input with
      | None -> None
      | Some (x32, consumed_x) ->
        if x32 `U32.lt` 253ul
        then Some (x32, consumed_x)
        else
          let input' = B32.slice input consumed_x (B32.len input) in
          if x32 = 253ul
          then
            match parse32_bounded_integer_le_2 input' with
            | None -> None
            | Some (y, consumed_y) ->
              if y `U32.lt` 253ul then None else Some (y, consumed_x `U32.add` consumed_y)
          else
            if x32 = 254ul
            then
              match parse32_bounded_integer_le_4 input' with
              | None -> None
              | Some (y, consumed_y) ->
                if y `U32.lt` 65536ul then None else Some (y, consumed_x `U32.add` consumed_y)
            else None)
    <:
    (res: _{parser32_correct parse_bcvli input res}))
LowParse.SLow.BCVLI.fst.checked
prims.fst.checked LowParse.Spec.BCVLI.fsti.checked LowParse.SLow.Combinators.fst.checked LowParse.SLow.BoundedInt.fsti.checked LowParse.Bytes32.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked
LowParse.SLow.BCVLI.fst
LowParse.SLow.Base.bytes32 LowParse.SLow.BoundedInt.parse32_bounded_integer_le_1 FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 FStar.UInt32.t LowParse.Spec.BoundedInt.bounded_integer FStar.UInt32.lt FStar.UInt32.__uint_to_t FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.bool Prims.op_Equality LowParse.SLow.BoundedInt.parse32_bounded_integer_le_2 FStar.UInt32.add FStar.Pervasives.Native.option LowParse.SLow.Base.parser32_correct LowParse.Spec.BCVLI.parse_bcvli_kind LowParse.Spec.BCVLI.parse_bcvli LowParse.SLow.BoundedInt.parse32_bounded_integer_le_4 FStar.Bytes.bytes Prims.eq2 FStar.Seq.Base.seq FStar.UInt8.t FStar.Bytes.reveal FStar.Seq.Base.slice FStar.UInt32.v FStar.Bytes.len FStar.Bytes.slice Prims.unit LowParse.Spec.BCVLI.parse_bcvli_eq
module LowParse.SLow.BCVLI
include LowParse.Spec.BCVLI
include LowParse.SLow.Combinators // for make_total_constant_size_parser32
include LowParse.SLow.BoundedInt // for bounded_integer_le

module B32 = LowParse.Bytes32
module Seq = FStar.Seq
module U32 = FStar.UInt32
module Cast = FStar.Int.Cast

#push-options "--max_fuel 0"

let parse32_bcvli
val parse32_bcvli:parser32 parse_bcvli
LowParse.SLow.Base.parser32 LowParse.Spec.BCVLI.parse_bcvli