val asn1_length_t : Type0
let asn1_length_t = nat
module ASN1.Base
open FStar.Integers

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

let (.[]) = FStar.Seq.index
let byte = uint_8

inline_for_extraction noextract
let bytes = Seq.seq byte

inline_for_extraction noextract
let lbytes = Seq.Properties.lseq byte

//////////////////////////////////////////////////////////////////////////
/////                           ASN1 Types
/////////////////////////////////////////////////////////////////////////
type asn1_tag_value_t = b: byte {v b <= 0b11111}
type asn1_tag_form_t =
| PRIMITIVE
| CONSTRUCTED
type asn1_tag_class_t =
// (* NOTE: UNIVERSAL is reserved *) | UNIVERSAL
| APPLICATION
| CONTEXT_SPECIFIC
| PRIVATE

type asn1_tag_t: Type =
| BOOLEAN
| INTEGER
| ASN1_NULL
| OCTET_STRING
| PRINTABLE_STRING
| IA5_STRING
| BIT_STRING
| OID
| UTC_TIME
| Generalized_Time
| SEQUENCE
| SET
| CUSTOM_TAG: tag_class: asn1_tag_class_t ->
              tag_form : asn1_tag_form_t  ->
              tag_value: asn1_tag_value_t ->
              asn1_tag_t

type asn1_type = t: asn1_tag_t {not (CUSTOM_TAG? t)}

inline_for_extraction
let the_asn1_tag (a: asn1_tag_t)
: Tot Type
= (a': asn1_tag_t{a == a'})

/// A specific ASN1 type
// inline_for_extraction
// let the_asn1_tag (a: asn1_type)
// : Tot Type
// = (a': asn1_type{a == a'})

/// Non constructive ASN1 types
let asn1_primitive_type
= (a: asn1_type{a =!= SEQUENCE /\ a =!= SET})

let character_string_type : Type
= a: asn1_tag_t { a == IA5_STRING \/ a == PRINTABLE_STRING }

inline_for_extraction noextract
let asn1_implicit_tagging
  (t1 t2: asn1_tag_t)
: asn1_tag_t
= t1

///////////////////////////////////////////////////////////////////////////
/////      bounded mathematical integers for ASN1 value lengths
///// Defines the valid length/size of a ASN1 DER values
///////////////////////////////////////////////////////////////////////////
/
prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked
ASN1.Base.fst
Type0
FStar.Integers.nat
let asn1_length_t =
  
nat