val lemma_serialize_asn1_length_of_bound_size
  (min: asn1_length_t)
  (max: asn1_length_t { min <= max /\ max <= asn1_length_max })
  (y': bounded_int32 min max)
: Lemma
  (
    Seq.length (serialize (serialize_asn1_length_of_bound min max) y') == (
      if y' `U32.lt` 128ul
      then 1
      else if y' `U32.lt` 256ul
      then 2
      else if y' `U32.lt` 65536ul
      then 3
      else if y' `U32.lt` 16777216ul
      then 4
      else 5
 ))
val lemma_serialize_asn1_length_of_bound_size
  (min: asn1_length_t)
  (max: asn1_length_t { min <= max /\ max <= asn1_length_max })
  (y': bounded_int32 min max)
: Lemma
  (
    Seq.length (serialize (serialize_asn1_length_of_bound min max) y') == (
      if y' `U32.lt` 128ul
      then 1
      else if y' `U32.lt` 256ul
      then 2
      else if y' `U32.lt` 65536ul
      then 3
      else if y' `U32.lt` 16777216ul
      then 4
      else 5
 ))
let lemma_serialize_asn1_length_of_bound_size min max
= serialize_bounded_der_length32_size 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'

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
/
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} ->
    y': LowParse.Spec.BoundedInt.bounded_int32 min max
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Base.length (LowParse.Spec.Base.serialize (ASN1.Spec.Length.serialize_asn1_length_of_bound
                min
                max)
            y') ==
      (match FStar.UInt32.lt y' 128ul with
        | true -> 1
        | _ ->
          (match FStar.UInt32.lt y' 256ul with
            | true -> 2
            | _ ->
              (match FStar.UInt32.lt y' 65536ul with
                | true -> 3
                | _ ->
                  (match FStar.UInt32.lt y' 16777216ul with
                    | true -> 4
                    | _ -> 5)
                  <:
                  Prims.int)
              <:
              Prims.int)
          <:
          Prims.int))
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.serialize_bounded_der_length32_size LowParse.Spec.BoundedInt.bounded_int32 Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.int FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.Base.serialize ASN1.Spec.Length.parse_asn1_length_of_bound_kind ASN1.Spec.Length.parse_asn1_length_of_bound ASN1.Spec.Length.serialize_asn1_length_of_bound FStar.UInt32.lt FStar.UInt32.__uint_to_t Prims.bool Prims.Nil FStar.Pervasives.pattern
let lemma_serialize_asn1_length_of_bound_size min max =
  
serialize_bounded_der_length32_size min max