val parse_bounded_der_length32_bare
      (min: der_length_t)
      (max: der_length_t{min <= max /\ max < 4294967296})
      (input: bytes)
    : Pure (option (bounded_int32 min max & consumed_length input))
      (requires True)
      (ensures (fun y -> y == parse (parse_bounded_der_length32 min max) input))
let parse_bounded_der_length32_bare
  (min: der_length_t)
  (max: der_length_t { min <= max /\ max < 4294967296 })
  (input: bytes)
: Pure (option (bounded_int32 min max & consumed_length input))
    (requires True)
    (ensures (fun y ->
      y == parse (parse_bounded_der_length32 min max) input
    ))
=
   parse_bounded_der_length32_unfold min max input;
   match parse_u8 input with
   | None -> None
   | Some (x, consumed_x) ->
     let len = der_length_payload_size_of_tag x in
     if der_length_payload_size min <= len && len <= der_length_payload_size max then
      let input' = Seq.slice input consumed_x (Seq.length input) in
      match (parse_der_length_payload32_bare x) input' with
      | Some (y, consumed_y) ->
        if min <= U32.v y && U32.v y <= max
        then Some (y, consumed_x + consumed_y)
        else None
      | None -> None
     else
       None
val parse_bounded_der_length32_bare
      (min: der_length_t)
      (max: der_length_t{min <= max /\ max < 4294967296})
      (input: bytes)
    : Pure (option (bounded_int32 min max & consumed_length input))
      (requires True)
      (ensures (fun y -> y == parse (parse_bounded_der_length32 min max) input))
let parse_bounded_der_length32_bare
      (min: der_length_t)
      (max: der_length_t{min <= max /\ max < 4294967296})
      (input: bytes)
    : Pure (option (bounded_int32 min max & consumed_length input))
      (requires True)
      (ensures (fun y -> y == parse (parse_bounded_der_length32 min max) input)) =
parse_bounded_der_length32_unfold min max input;
match parse_u8 input with
| None -> None
| Some (x, consumed_x) ->
  let len = der_length_payload_size_of_tag x in
  if der_length_payload_size min <= len && len <= der_length_payload_size max
  then
    let input' = Seq.slice input consumed_x (Seq.length input) in
    match (parse_der_length_payload32_bare x) input' with
    | Some (y, consumed_y) ->
      if min <= U32.v y && U32.v y <= max then Some (y, consumed_x + consumed_y) else None
    | None -> None
  else None
LowParse.Tot.DER.fst.checked
prims.fst.checked LowParse.Tot.BoundedInt.fst.checked LowParse.Spec.DER.fsti.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.Tot.DER.fst
LowParse.Spec.DER.der_length_t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan LowParse.Bytes.bytes LowParse.Tot.Int.parse_u8 FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 LowParse.Spec.BoundedInt.bounded_int32 LowParse.Spec.Base.consumed_length FStar.UInt8.t Prims.op_AmpAmp LowParse.Spec.DER.der_length_payload_size LowParse.Tot.DER.parse_der_length_payload32_bare LowParse.Spec.Base.refine_with_tag FStar.UInt32.t LowParse.Spec.DER.tag_of_der_length32 FStar.UInt32.v FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.op_Addition Prims.bool FStar.Pervasives.Native.option FStar.Seq.Base.seq LowParse.Bytes.byte FStar.Seq.Base.slice FStar.Seq.Base.length Prims.nat LowParse.Spec.DER.der_length_payload_size_of_tag Prims.unit LowParse.Spec.DER.parse_bounded_der_length32_unfold Prims.l_True Prims.eq2 LowParse.Spec.Base.parse LowParse.Spec.DER.parse_bounded_der_length32
module LowParse.Tot.DER
include LowParse.Spec.DER
include LowParse.Tot.BoundedInt

module U32 = FStar.UInt32
module U8 = FStar.UInt8

let parse_der_length_payload32_bare
  (x: U8.t { der_length_payload_size_of_tag x <= 4 } )
  (input: bytes)
: Pure (option ((refine_with_tag tag_of_der_length32 x) * consumed_length input))
    (requires True)
    (ensures (fun y ->
      y == parse (parse_der_length_payload32 x) input
    ))
=
    parse_der_length_payload32_unfold x input;
    if U8.v x < 128
    then Some (FStar.Int.Cast.uint8_to_uint32 x, 0)
    else if x = 128uy || x = 255uy
    then None
    else if x = 129uy
    then
      match parse_u8 input with
      | None -> None
      | Some (z, consumed) ->
        if U8.v z < 128
        then None
        else Some (FStar.Int.Cast.uint8_to_uint32 z, consumed)
    else
      let len : nat = U8.v x - 128 in
      let _ = parse_bounded_integer_spec len input in
      let res : option (bounded_integer len & consumed_length input) = (parse_bounded_integer len) input in
      match res with
      | None -> None
      | Some (z, consumed) ->
        if U32.v z >= pow2 (8 `op_Multiply` (len - 1))
        then Some ((z <: refine_with_tag tag_of_der_length32 x), consumed)
        else None

let parse_bounded_der_length32_bare
  (min: der_length_t)
  (max: der_length_t { min <= max /\ max < 4294967296 })
  (input: bytes)
: Pure (option (bounded_int32 min max & consumed_length input))
    (requires True)
    (ensures (fun y ->
      y == parse (parse_bounded_der_length32 min max) input
    ))
val parse_bounded_der_length32_bare
      (min: der_length_t)
      (max: der_length_t{min <= max /\ max < 4294967296})
      (input: bytes)
    : Pure (option (bounded_int32 min max & consumed_length input))
      (requires True)
      (ensures (fun y -> y == parse (parse_bounded_der_length32 min max) input))

    min: LowParse.Spec.DER.der_length_t ->
    max: LowParse.Spec.DER.der_length_t{min <= max /\ max < 4294967296} ->
    input: LowParse.Bytes.bytes
  -> Prims.Pure
    (FStar.Pervasives.Native.option (LowParse.Spec.BoundedInt.bounded_int32 min max *
          LowParse.Spec.Base.consumed_length input))