val asn1_value_length_of_big_integer : Type0
let asn1_value_length_of_big_integer
= l: asn1_length_t { 1 <= l /\ l <= asn1_length_max - 6}
module ASN1.Spec.Value.BigInteger

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Spec.Bytes32
open LowParse.Spec.DER

open FStar.Integers

module U32 = FStar.UInt32
module B32 = FStar.Bytes

(*

  encoded -----parse------>  decoded
   bytes  <---serialize--- octet string
*)

unfold
/
prims.fst.checked LowParse.Spec.DER.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Bytes32.fst.checked ASN1.Spec.Base.fst.checked ASN1.Low.Length.fsti.checked ASN1.Base.fst.checked
ASN1.Spec.Value.BigInteger.fsti
Type0
ASN1.Base.asn1_length_t Prims.l_and Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.op_Subtraction ASN1.Base.asn1_length_max
let asn1_value_length_of_big_integer =
  
l: asn1_length_t{1 <= l /\ l <= asn1_length_max - 6}