val 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))
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
val 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))
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
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
FStar.UInt8.t Prims.b2t Prims.op_LessThanOrEqual LowParse.Spec.DER.der_length_payload_size_of_tag LowParse.Bytes.bytes Prims.op_LessThan FStar.UInt8.v FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.refine_with_tag FStar.UInt32.t LowParse.Spec.DER.tag_of_der_length32 LowParse.Spec.Base.consumed_length FStar.Pervasives.Native.Mktuple2 FStar.Int.Cast.uint8_to_uint32 Prims.bool Prims.op_BarBar Prims.op_Equality FStar.UInt8.__uint_to_t FStar.Pervasives.Native.None LowParse.Tot.Int.parse_u8 FStar.Pervasives.Native.option LowParse.Spec.BoundedInt.bounded_integer Prims.op_GreaterThanOrEqual FStar.UInt32.v Prims.pow2 Prims.op_Multiply Prims.op_Subtraction LowParse.Tot.BoundedInt.parse_bounded_integer Prims.unit LowParse.Spec.BoundedInt.parse_bounded_integer_spec Prims.nat LowParse.Spec.DER.parse_der_length_payload32_unfold Prims.l_True Prims.eq2 LowParse.Spec.Base.parse LowParse.Spec.DER.parse_der_length_payload32
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
    ))
val 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))

    x: FStar.UInt8.t{LowParse.Spec.DER.der_length_payload_size_of_tag x <= 4} ->
    input: LowParse.Bytes.bytes
  -> Prims.Pure
    (FStar.Pervasives.Native.option (LowParse.Spec.Base.refine_with_tag LowParse.Spec.DER.tag_of_der_length32
            x *
          LowParse.Spec.Base.consumed_length input))