val lemma_serialize_asn1_length_of_bound_unfold
  (min: asn1_length_t)
  (max: asn1_length_t { min <= max /\ max <= asn1_length_max })
  (y': bounded_int32 min max)
: Lemma (
    let res = serialize_asn1_length_of_bound min max `serialize` y' in
    let x = tag_of_der_length32_impl y' in
    let s1 = Seq.create 1 x in
    if x `U8.lt` 128uy
    then res `Seq.equal` s1
    else if x = 129uy
    then U32.v y' <= 255 /\ res `Seq.equal` (s1 `Seq.append` Seq.create 1 (Cast.uint32_to_uint8 y'))
    else
      let len = log256' (U32.v y') in
      res `Seq.equal` (s1 `Seq.append` serialize (serialize_bounded_integer len) y')
)
val lemma_serialize_asn1_length_of_bound_unfold
  (min: asn1_length_t)
  (max: asn1_length_t { min <= max /\ max <= asn1_length_max })
  (y': bounded_int32 min max)
: Lemma (
    let res = serialize_asn1_length_of_bound min max `serialize` y' in
    let x = tag_of_der_length32_impl y' in
    let s1 = Seq.create 1 x in
    if x `U8.lt` 128uy
    then res `Seq.equal` s1
    else if x = 129uy
    then U32.v y' <= 255 /\ res `Seq.equal` (s1 `Seq.append` Seq.create 1 (Cast.uint32_to_uint8 y'))
    else
      let len = log256' (U32.v y') in
      res `Seq.equal` (s1 `Seq.append` serialize (serialize_bounded_integer len) y')
)
let lemma_serialize_asn1_length_of_bound_unfold min max
= serialize_bounded_der_length32_unfold 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
/
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
      (let res =
          LowParse.Spec.Base.serialize (ASN1.Spec.Length.serialize_asn1_length_of_bound min max) y'
        in
        let x = LowParse.Spec.DER.tag_of_der_length32_impl y' in
        let s1 = FStar.Seq.Base.create 1 x in
        (match FStar.UInt8.lt x 128uy with
          | true -> FStar.Seq.Base.equal res s1
          | _ ->
            (match x = 129uy with
              | true ->
                FStar.UInt32.v y' <= 255 /\
                FStar.Seq.Base.equal res
                  (FStar.Seq.Base.append s1
                      (FStar.Seq.Base.create 1 (FStar.Int.Cast.uint32_to_uint8 y')))
              | _ ->
                let len = LowParse.Spec.BoundedInt.log256' (FStar.UInt32.v y') in
                FStar.Seq.Base.equal res
                  (FStar.Seq.Base.append s1
                      (LowParse.Spec.Base.serialize (LowParse.Spec.BoundedInt.serialize_bounded_integer
                              len)
                          y')))
            <:
            Type0)
        <:
        Type0))
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_unfold LowParse.Spec.BoundedInt.bounded_int32 Prims.unit Prims.l_True Prims.squash FStar.UInt8.lt FStar.UInt8.__uint_to_t FStar.Seq.Base.equal LowParse.Bytes.byte Prims.bool Prims.op_Equality FStar.UInt8.t FStar.UInt32.v FStar.Seq.Base.append FStar.Seq.Base.create FStar.Int.Cast.uint32_to_uint8 LowParse.Spec.Base.serialize LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.bounded_integer LowParse.Spec.BoundedInt.parse_bounded_integer LowParse.Spec.BoundedInt.serialize_bounded_integer LowParse.Spec.BoundedInt.integer_size LowParse.Spec.BoundedInt.log256' FStar.Seq.Base.seq Prims.op_LessThan LowParse.Spec.DER.der_length_max Prims.eq2 LowParse.Spec.DER.tag_of_der_length LowParse.Spec.DER.tag_of_der_length32_impl LowParse.Bytes.bytes 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 Prims.Nil FStar.Pervasives.pattern
let lemma_serialize_asn1_length_of_bound_unfold min max =
  
serialize_bounded_der_length32_unfold min max