val serialize_asn1_length_of_bound_eq
  (min: asn1_length_t)
  (max: asn1_length_t { min <= max /\ max <= asn1_length_max })
  (len: bounded_int32 min max)
: Lemma (
  serialize serialize_asn1_length len ==
  serialize (serialize_asn1_length_of_bound min max) len
)
val serialize_asn1_length_of_bound_eq
  (min: asn1_length_t)
  (max: asn1_length_t { min <= max /\ max <= asn1_length_max })
  (len: bounded_int32 min max)
: Lemma (
  serialize serialize_asn1_length len ==
  serialize (serialize_asn1_length_of_bound min max) len
)
let serialize_asn1_length_of_bound_eq min max len
= lemma_serialize_asn1_length_of_bound_unfold min max len;
  serialize_bounded_der_length32_unfold asn1_length_min asn1_length_max len
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'

let parse_asn1_length_of_bound min max
= parse_bounded_der_length32 min max

let serialize_asn1_length_of_bound min max
= serialize_bounded_der_length32 min max

let lemma_serialize_asn1_length_of_bound_unfold min max
= serialize_bounded_der_length32_unfold min max

let lemma_serialize_asn1_length_of_bound_size min max
= serialize_bounded_der_length32_size min max

/// Specialized for a specific ASN1 type
///

// let parse_asn1_length_of_type _a
// = parse_bounded_der_length32 (asn1_value_length_min_of_type _a) (asn1_value_length_max_of_type _a)

// let serialize_asn1_length_of_type _a
// = serialize_bounded_der_length32 (asn1_value_length_min_of_type _a) (asn1_value_length_max_of_type _a
/
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} ->
    len: LowParse.Spec.BoundedInt.bounded_int32 min max
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serialize ASN1.Spec.Length.serialize_asn1_length len ==
      LowParse.Spec.Base.serialize (ASN1.Spec.Length.serialize_asn1_length_of_bound min max) len)
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.BoundedInt.bounded_int32 LowParse.Spec.DER.serialize_bounded_der_length32_unfold ASN1.Base.asn1_length_min Prims.unit ASN1.Spec.Length.lemma_serialize_asn1_length_of_bound_unfold
let serialize_asn1_length_of_bound_eq min max len =
  
lemma_serialize_asn1_length_of_bound_unfold min max len;
serialize_bounded_der_length32_unfold asn1_length_min asn1_length_max len