val validate_der_length_payload32 (x: U8.t{der_length_payload_size_of_tag x <= 4})
    : Tot (validator (parse_der_length_payload32 x))
let validate_der_length_payload32
  (x: U8.t { der_length_payload_size_of_tag x <= 4 } )
: Tot (validator (parse_der_length_payload32 x))
= fun #rrel #rel input pos ->
    let h = HST.get () in
    [@inline_let] let _ =
      valid_facts (parse_der_length_payload32 x) h input (uint64_to_uint32 pos);
      assert (U64.v pos <= U32.v input.len);
      parse_der_length_payload32_unfold x (bytes_of_slice_from h input (uint64_to_uint32 pos));
      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 pos
    else if x = 128uy || x = 255uy
    then validator_error_generic
    else if x = 129uy
    then
      [@inline_let] let _ = valid_facts parse_u8 h input (uint64_to_uint32 pos) in
      let v = validate_u8 () input pos in
      if is_error v
      then v
      else
        let z = read_u8 input (uint64_to_uint32 pos) in
        if z `U8.lt` 128uy
        then validator_error_generic
        else v
    else
      let len = x `U8.sub` 128uy in
      [@inline_let] let _ = valid_facts (parse_bounded_integer (U8.v len)) h input (uint64_to_uint32 pos) in
      if len = 2uy
      then
        let v = validate_bounded_integer 2 input pos in
        if is_error v
        then v
        else
          let y = read_bounded_integer_2 () input (uint64_to_uint32 pos) in
          if y `U32.lt `256ul
          then validator_error_generic
          else v
      else if len = 3uy
      then
        let v = validate_bounded_integer 3 input pos in
        if is_error v
        then v
        else
          let y = read_bounded_integer_3 () input (uint64_to_uint32 pos) in
          if y `U32.lt `65536ul
          then validator_error_generic
          else v
      else
        let v = validate_bounded_integer 4 input pos in
        if is_error v
        then v
        else
          let y = read_bounded_integer_4 () input (uint64_to_uint32 pos) in
          if y `U32.lt` 16777216ul
          then validator_error_generic
          else v
val validate_der_length_payload32 (x: U8.t{der_length_payload_size_of_tag x <= 4})
    : Tot (validator (parse_der_length_payload32 x))
let validate_der_length_payload32 (x: U8.t{der_length_payload_size_of_tag x <= 4})
    : Tot (validator (parse_der_length_payload32 x)) =
fun #rrel #rel input pos ->
  let h = HST.get () in
  [@@ inline_let ]let _ =
    valid_facts (parse_der_length_payload32 x) h input (uint64_to_uint32 pos);
    assert (U64.v pos <= U32.v input.len);
    parse_der_length_payload32_unfold x (bytes_of_slice_from h input (uint64_to_uint32 pos));
    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 pos
  else
    if x = 128uy || x = 255uy
    then validator_error_generic
    else
      if x = 129uy
      then
        [@@ inline_let ]let _ = valid_facts parse_u8 h input (uint64_to_uint32 pos) in
        let v = validate_u8 () input pos in
        if is_error v
        then v
        else
          let z = read_u8 input (uint64_to_uint32 pos) in
          if z `U8.lt` 128uy then validator_error_generic else v
      else
        let len = x `U8.sub` 128uy in
        [@@ inline_let ]let _ =
          valid_facts (parse_bounded_integer (U8.v len)) h input (uint64_to_uint32 pos)
        in
        if len = 2uy
        then
          let v = validate_bounded_integer 2 input pos in
          if is_error v
          then v
          else
            let y = read_bounded_integer_2 () input (uint64_to_uint32 pos) in
            if y `U32.lt` 256ul then validator_error_generic else v
        else
          if len = 3uy
          then
            let v = validate_bounded_integer 3 input pos in
            if is_error v
            then v
            else
              let y = read_bounded_integer_3 () input (uint64_to_uint32 pos) in
              if y `U32.lt` 65536ul then validator_error_generic else v
          else
            let v = validate_bounded_integer 4 input pos in
            if is_error v
            then v
            else
              let y = read_bounded_integer_4 () input (uint64_to_uint32 pos) in
              if y `U32.lt` 16777216ul then validator_error_generic else v
LowParse.Low.DER.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.DER.fsti.checked LowParse.Low.Int.fsti.checked LowParse.Low.BoundedInt.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Ghost.fsti.checked
LowParse.Low.DER.fst
FStar.UInt8.t Prims.b2t Prims.op_LessThanOrEqual LowParse.Spec.DER.der_length_payload_size_of_tag LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt64.t FStar.UInt8.lt FStar.UInt8.__uint_to_t Prims.bool Prims.op_BarBar Prims.op_Equality LowParse.Low.ErrorCode.validator_error_generic LowParse.Low.ErrorCode.is_error LowParse.Low.Int.read_u8 LowParse.Low.ErrorCode.uint64_to_uint32 LowParse.Low.Int.validate_u8 Prims.unit LowParse.Low.Base.Spec.valid_facts LowParse.Spec.Int.parse_u8_kind LowParse.Spec.Int.parse_u8 FStar.UInt32.lt FStar.UInt32.__uint_to_t LowParse.Spec.BoundedInt.bounded_integer LowParse.Low.BoundedInt.read_bounded_integer_2 LowParse.Low.BoundedInt.validate_bounded_integer LowParse.Low.BoundedInt.read_bounded_integer_3 LowParse.Low.BoundedInt.read_bounded_integer_4 LowParse.Spec.BoundedInt.parse_bounded_integer_kind FStar.UInt8.v LowParse.Spec.BoundedInt.parse_bounded_integer FStar.UInt8.sub FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.pow2 FStar.Mul.op_Star LowParse.Spec.DER.parse_der_length_payload32_unfold LowParse.Slice.bytes_of_slice_from Prims._assert FStar.UInt64.v FStar.UInt32.v LowParse.Slice.__proj__Mkslice__item__len LowParse.Spec.DER.parse_der_length_payload_kind LowParse.Spec.Base.refine_with_tag FStar.UInt32.t LowParse.Spec.DER.tag_of_der_length32 LowParse.Spec.DER.parse_der_length_payload32 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowParse.Low.Base.validator
module LowParse.Low.DER
include LowParse.Spec.DER
include LowParse.Low.Int // for parse_u8
include LowParse.Low.BoundedInt // for bounded_integer
open FStar.Mul

module U8 = FStar.UInt8
module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
module Cast = FStar.Int.Cast
module U64 = FStar.UInt64

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

#push-options "--z3rlimit 32"

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