val validate_bounded_der_length32
      (vmin: der_length_t)
      (min: U32.t{U32.v min == vmin})
      (vmax: der_length_t)
      (max: U32.t{U32.v max == vmax /\ U32.v min <= U32.v max})
    : Tot (validator (parse_bounded_der_length32 (vmin) (vmax)))
let validate_bounded_der_length32
  (vmin: der_length_t)
  (min: U32.t { U32.v min == vmin } )
  (vmax: der_length_t)
  (max: U32.t { U32.v max == vmax /\ U32.v min <= U32.v max } )
: Tot (
  validator (parse_bounded_der_length32 (vmin) (vmax)))
= fun #rrel #rel input pos ->
    let h = HST.get () in
    [@inline_let]
    let _ =
      valid_facts (parse_bounded_der_length32 (U32.v min) (U32.v max)) h input (uint64_to_uint32 pos);
      parse_bounded_der_length32_unfold (U32.v min) (U32.v max) (bytes_of_slice_from h input (uint64_to_uint32 pos));
      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 x = read_u8 input (uint64_to_uint32 pos) in
      let len = der_length_payload_size_of_tag8 x in
      let tg1 = tag_of_der_length32_impl min in
      let l1 = der_length_payload_size_of_tag8 tg1 in
      let tg2 = tag_of_der_length32_impl max in
      let l2 = der_length_payload_size_of_tag8 tg2 in
      if (len `U8.lt` l1) || ( l2 `U8.lt` len)
      then validator_error_generic
      else
        [@inline_let] let _ = valid_facts (parse_der_length_payload32 x) h input (uint64_to_uint32 v) in
        let v2 = validate_der_length_payload32 x input v in
        if is_error v2
        then v2
        else
          let y = read_der_length_payload32 x input (uint64_to_uint32 v) in
          if y `U32.lt` min || max `U32.lt` y
          then validator_error_generic
          else v2
val validate_bounded_der_length32
      (vmin: der_length_t)
      (min: U32.t{U32.v min == vmin})
      (vmax: der_length_t)
      (max: U32.t{U32.v max == vmax /\ U32.v min <= U32.v max})
    : Tot (validator (parse_bounded_der_length32 (vmin) (vmax)))
let validate_bounded_der_length32
      (vmin: der_length_t)
      (min: U32.t{U32.v min == vmin})
      (vmax: der_length_t)
      (max: U32.t{U32.v max == vmax /\ U32.v min <= U32.v max})
    : Tot (validator (parse_bounded_der_length32 (vmin) (vmax))) =
fun #rrel #rel input pos ->
  let h = HST.get () in
  [@@ inline_let ]let _ =
    valid_facts (parse_bounded_der_length32 (U32.v min) (U32.v max)) h input (uint64_to_uint32 pos);
    parse_bounded_der_length32_unfold (U32.v min)
      (U32.v max)
      (bytes_of_slice_from h input (uint64_to_uint32 pos));
    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 x = read_u8 input (uint64_to_uint32 pos) in
    let len = der_length_payload_size_of_tag8 x in
    let tg1 = tag_of_der_length32_impl min in
    let l1 = der_length_payload_size_of_tag8 tg1 in
    let tg2 = tag_of_der_length32_impl max in
    let l2 = der_length_payload_size_of_tag8 tg2 in
    if (len `U8.lt` l1) || (l2 `U8.lt` len)
    then validator_error_generic
    else
      [@@ inline_let ]let _ =
        valid_facts (parse_der_length_payload32 x) h input (uint64_to_uint32 v)
      in
      let v2 = validate_der_length_payload32 x input v in
      if is_error v2
      then v2
      else
        let y = read_der_length_payload32 x input (uint64_to_uint32 v) in
        if y `U32.lt` min || max `U32.lt` y then validator_error_generic else v2
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
LowParse.Spec.DER.der_length_t FStar.UInt32.t Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual LowParse.Spec.DER.der_length_max FStar.UInt32.v LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt64.t LowParse.Low.ErrorCode.is_error Prims.bool Prims.op_BarBar FStar.UInt8.lt LowParse.Low.ErrorCode.validator_error_generic FStar.UInt32.lt LowParse.Spec.Base.refine_with_tag FStar.UInt8.t LowParse.Spec.DER.tag_of_der_length32 LowParse.Low.DER.read_der_length_payload32 LowParse.Low.ErrorCode.uint64_to_uint32 LowParse.Low.DER.validate_der_length_payload32 Prims.unit LowParse.Low.Base.Spec.valid_facts LowParse.Spec.DER.parse_der_length_payload_kind LowParse.Spec.DER.parse_der_length_payload32 FStar.UInt8.v LowParse.Spec.DER.der_length_payload_size_of_tag LowParse.Spec.DER.der_length_payload_size_of_tag8 Prims.op_LessThan LowParse.Spec.DER.tag_of_der_length LowParse.Spec.DER.tag_of_der_length32_impl LowParse.Low.Int.read_u8 LowParse.Low.Int.validate_u8 LowParse.Spec.Int.parse_u8_kind LowParse.Spec.Int.parse_u8 LowParse.Spec.DER.parse_bounded_der_length32_unfold LowParse.Slice.bytes_of_slice_from LowParse.Spec.DER.parse_bounded_der_length32_kind LowParse.Spec.BoundedInt.bounded_int32 LowParse.Spec.DER.parse_bounded_der_length32 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 } )
: 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

inline_for_extraction
let jump_der_length_payload32
  (x: U8.t { der_length_payload_size_of_tag x <= 4 } )
: Tot (jumper (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 pos;
      parse_der_length_payload32_unfold x (bytes_of_slice_from h input 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
      [@inline_let]
      let len = x `U8.sub` 128uy in
      [@inline_let] let _ =
        valid_facts parse_u8 h input pos;
        parser_kind_prop_equiv parse_u8_kind parse_u8;
        valid_facts (parse_bounded_integer (U8.v len)) h input pos;
        parser_kind_prop_equiv (parse_bounded_integer_kind (U8.v len)) (parse_bounded_integer (U8.v len))
      in
      pos `U32.add` Cast.uint8_to_uint32 len

inline_for_extraction
let read_der_length_payload32
  (x: U8.t { der_length_payload_size_of_tag x <= 4 } )
: Tot (leaf_reader (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 pos;
      parse_der_length_payload32_unfold x (bytes_of_slice_from h input 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
      [@inline_let]
      let res = Cast.uint8_to_uint32 x in
      [@inline_let] let _ = assert (tag_of_der_length32 res == x) in
      (res <: refine_with_tag tag_of_der_length32 x)
    else if x = 129uy
    then
      [@inline_let] let _ = valid_facts parse_u8 h input pos in
      let z = read_u8 input pos in
      [@inline_let] let res = Cast.uint8_to_uint32 z in
      [@inline_let] let _ = assert (tag_of_der_length32 res == x) in
      (res <: refine_with_tag tag_of_der_length32 x)
    else
      let len = x `U8.sub` 128uy in
      [@inline_let] let _ = valid_facts (parse_bounded_integer (U8.v len)) h input pos in
      if len = 2uy
      then
        let res = read_bounded_integer_2 () input pos in
        [@inline_let] let _ = assert (tag_of_der_length32 res == x) in
        (res <: refine_with_tag tag_of_der_length32 x)
      else if len = 3uy
      then
        let res = read_bounded_integer_3 () input pos in
        [@inline_let] let _ = assert (tag_of_der_length32 res == x) in
        (res <: refine_with_tag tag_of_der_length32 x)
      else
        let res = read_bounded_integer_4 () input pos in
        [@inline_let] let _ = assert (tag_of_der_length32 res == x) in
        (res <: refine_with_tag tag_of_der_length32 x)

inline_for_extraction
let validate_bounded_der_length32
  (vmin: der_length_t)
  (min: U32.t { U32.v min == vmin } )
  (vmax: der_length_t)
  (max: U32.t { U32.v max == vmax /\ U32.v min <= U32.v max } )
: Tot (
val validate_bounded_der_length32
      (vmin: der_length_t)
      (min: U32.t{U32.v min == vmin})
      (vmax: der_length_t)
      (max: U32.t{U32.v max == vmax /\ U32.v min <= U32.v max})
    : Tot (validator (parse_bounded_der_length32 (vmin) (vmax)))

    vmin: LowParse.Spec.DER.der_length_t ->
    min: FStar.UInt32.t{FStar.UInt32.v min == vmin} ->
    vmax: LowParse.Spec.DER.der_length_t ->
    max: FStar.UInt32.t{FStar.UInt32.v max == vmax /\ FStar.UInt32.v min <= FStar.UInt32.v max}
  -> LowParse.Low.Base.validator (LowParse.Spec.DER.parse_bounded_der_length32 vmin vmax)