val parse_asn1_length_of_bound
  (min: asn1_length_t)
  (max: asn1_length_t { min <= max /\ max <= asn1_length_max })
: parser (parse_asn1_length_of_bound_kind min max) (bounded_int32 min max)
val parse_asn1_length_of_bound
  (min: asn1_length_t)
  (max: asn1_length_t { min <= max /\ max <= asn1_length_max })
: parser (parse_asn1_length_of_bound_kind min max) (bounded_int32 min max)
let parse_asn1_length_of_bound min max
= parse_bounded_der_length32 min max
module ASN1.Spec.Length

open ASN1.Spec.Base
open LowParse.Spec.DER
open FStar.Integers

open ASN1.Base

#set-options "--z3rlimit 32 --fuel 0 --ifuel 1"

/// ASN1 length parser, based on `LowParse.Spec.DER`


// let parse_asn1_length
// = parse_bounded_der_length32 asn1_length_min asn1_length_max

// noextract
// let lemma_parse_asn1_length_unfold = parse_bounded_der_length32_unfold asn1_length_min asn1_length_max

// let serialize_asn1_length
// = serialize_bounded_der_length32 asn1_length_min asn1_length_max

// let lemma_serialize_asn1_length_unfold y'
// = serialize_bounded_der_length32_unfold asn1_length_min asn1_length_max y'

// let lemma_serialize_asn1_length_size y'
// = serialize_bounded_der_length32_size asn1_length_min asn1_length_max y'
/
prims.fst.checked LowParse.Spec.DER.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Length.fst

    min: ASN1.Base.asn1_length_t ->
    max: ASN1.Base.asn1_length_t{min <= max /\ max <= ASN1.Base.asn1_length_max}
  -> LowParse.Spec.Base.parser (ASN1.Spec.Length.parse_asn1_length_of_bound_kind min max)
      (LowParse.Spec.BoundedInt.bounded_int32 min max)
ASN1.Base.asn1_length_t Prims.l_and Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite ASN1.Base.asn1_length_max LowParse.Spec.DER.parse_bounded_der_length32 LowParse.Spec.Base.parser ASN1.Spec.Length.parse_asn1_length_of_bound_kind LowParse.Spec.BoundedInt.bounded_int32
let parse_asn1_length_of_bound min max =
  
parse_bounded_der_length32 min max