val parse32_der_length_payload32 (x: U8.t{der_length_payload_size_of_tag x <= 4})
    : Tot (parser32 (parse_der_length_payload32 x))
let parse32_der_length_payload32
  (x: U8.t { der_length_payload_size_of_tag x <= 4 } )
: Tot (parser32 (parse_der_length_payload32 x))
= fun (input: bytes32) -> ((
    [@inline_let] let _ =
      parse_der_length_payload32_unfold x (B32.reveal input);
      assert_norm (pow2 (8 * 1) == 256);
      assert_norm (pow2 (8 * 2) == 65536);
      assert_norm (pow2 (8 * 3) == 16777216);
      assert_norm (pow2 (8 * 4) == 4294967296)
    in
    if x `U8.lt` 128uy
    then Some (Cast.uint8_to_uint32 x, 0ul)
    else if x = 128uy || x = 255uy
    then None
    else if x = 129uy
    then
      match parse32_u8 input with
      | None -> None
      | Some (z, consumed) ->
        if z `U8.lt` 128uy
        then None
        else Some ((Cast.uint8_to_uint32 z <: refine_with_tag tag_of_der_length32 x), consumed)
    else
      let len = x `U8.sub` 128uy in
      if len = 2uy
      then
        match parse32_bounded_integer 2 input with
        | None -> None
        | Some (y, consumed) ->
          if y `U32.lt `256ul
          then None
          else Some ((y <: refine_with_tag tag_of_der_length32 x), consumed)
      else if len = 3uy
      then
        match parse32_bounded_integer 3 input with
        | None -> None
        | Some (y, consumed) ->
          if y `U32.lt `65536ul
          then None
          else Some ((y <: refine_with_tag tag_of_der_length32 x), consumed)
      else
        match parse32_bounded_integer 4 input with
        | None -> None
        | Some (y, consumed) ->
          if y `U32.lt` 16777216ul
          then None
          else Some ((y <: refine_with_tag tag_of_der_length32 x), consumed)
  ) <: (res: _ { parser32_correct (parse_der_length_payload32 x) input res } ))
val parse32_der_length_payload32 (x: U8.t{der_length_payload_size_of_tag x <= 4})
    : Tot (parser32 (parse_der_length_payload32 x))
let parse32_der_length_payload32 (x: U8.t{der_length_payload_size_of_tag x <= 4})
    : Tot (parser32 (parse_der_length_payload32 x)) =
fun (input: bytes32) ->
  (([@@ inline_let ]let _ =
        parse_der_length_payload32_unfold x (B32.reveal input);
        assert_norm (pow2 (8 * 1) == 256);
        assert_norm (pow2 (8 * 2) == 65536);
        assert_norm (pow2 (8 * 3) == 16777216);
        assert_norm (pow2 (8 * 4) == 4294967296)
      in
      if x `U8.lt` 128uy
      then Some (Cast.uint8_to_uint32 x, 0ul)
      else
        if x = 128uy || x = 255uy
        then None
        else
          if x = 129uy
          then
            match parse32_u8 input with
            | None -> None
            | Some (z, consumed) ->
              if z `U8.lt` 128uy
              then None
              else
                Some ((Cast.uint8_to_uint32 z <: refine_with_tag tag_of_der_length32 x), consumed)
          else
            let len = x `U8.sub` 128uy in
            if len = 2uy
            then
              match parse32_bounded_integer 2 input with
              | None -> None
              | Some (y, consumed) ->
                if y `U32.lt` 256ul
                then None
                else Some ((y <: refine_with_tag tag_of_der_length32 x), consumed)
            else
              if len = 3uy
              then
                match parse32_bounded_integer 3 input with
                | None -> None
                | Some (y, consumed) ->
                  if y `U32.lt` 65536ul
                  then None
                  else Some ((y <: refine_with_tag tag_of_der_length32 x), consumed)
              else
                match parse32_bounded_integer 4 input with
                | None -> None
                | Some (y, consumed) ->
                  if y `U32.lt` 16777216ul
                  then None
                  else Some ((y <: refine_with_tag tag_of_der_length32 x), consumed))
    <:
    (res: _{parser32_correct (parse_der_length_payload32 x) input res}))
LowParse.SLow.DER.fst.checked
prims.fst.checked LowParse.Spec.DER.fsti.checked LowParse.SLow.Int.fsti.checked LowParse.SLow.Combinators.fst.checked LowParse.SLow.BoundedInt.fsti.checked LowParse.Math.fst.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.Mul.fst.checked FStar.Int.Cast.fst.checked
LowParse.SLow.DER.fst
FStar.UInt8.t Prims.b2t Prims.op_LessThanOrEqual LowParse.Spec.DER.der_length_payload_size_of_tag LowParse.SLow.Base.bytes32 FStar.UInt8.lt FStar.UInt8.__uint_to_t FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.refine_with_tag FStar.UInt32.t LowParse.Spec.DER.tag_of_der_length32 FStar.Pervasives.Native.Mktuple2 FStar.Int.Cast.uint8_to_uint32 FStar.UInt32.__uint_to_t Prims.bool Prims.op_BarBar Prims.op_Equality FStar.Pervasives.Native.None LowParse.SLow.Int.parse32_u8 FStar.Pervasives.Native.option LowParse.SLow.Base.parser32_correct LowParse.Spec.DER.parse_der_length_payload_kind LowParse.Spec.DER.parse_der_length_payload32 LowParse.SLow.BoundedInt.parse32_bounded_integer LowParse.Spec.BoundedInt.bounded_integer FStar.UInt32.lt FStar.UInt8.sub Prims.unit FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.pow2 FStar.Mul.op_Star LowParse.Spec.DER.parse_der_length_payload32_unfold FStar.Bytes.reveal LowParse.SLow.Base.parser32
module LowParse.SLow.DER
include LowParse.Spec.DER
include LowParse.SLow.Combinators
include LowParse.SLow.Int // for parse32_u8
include LowParse.SLow.BoundedInt // for bounded_integer
open FStar.Mul

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

#reset-options "--z3cliopt smt.arith.nl=false --max_fuel 0 --max_ifuel 0"

#push-options "--z3rlimit 16"

inline_for_extraction
let parse32_der_length_payload32
  (x: U8.t { der_length_payload_size_of_tag x <= 4 } )
val parse32_der_length_payload32 (x: U8.t{der_length_payload_size_of_tag x <= 4})
    : Tot (parser32 (parse_der_length_payload32 x))
x: FStar.UInt8.t{LowParse.Spec.DER.der_length_payload_size_of_tag x <= 4}
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.DER.parse_der_length_payload32 x)