val asn1_int32_inbounds (min max: nat) (x: U32.t) : GTot bool
val asn1_int32_inbounds (min max: nat) (x: U32.t) : GTot bool
let asn1_int32_inbounds
  (min: nat)
  (max: nat)
  (x: U32.t)
: GTot bool
= not (U32.v x < min || max < U32.v x)
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
///////////////////////////////////////////////////////////////////////////
unfold
let asn1_length_t = nat //{within_bounds (Unsigned W32) n}

inline_for_extraction noextract unfold
let asn1_length_min (*: n: asn1_length_t {forall (n':asn1_length_t). n <= n'}*) = 0
inline_for_extraction noextract unfold
let asn1_length_max (*: n: asn1_length_t {forall (n':asn1_length_t). n >= n'}*) = 4294967295
inline_for_extraction noextract unfold
let asn1_length_inbound (x: nat) (min max: asn1_length_t): bool
= min <= x && x <= max
// unfold
// let asn1_length_inbound_t = n: asn1_length_t { asn1_length_inbound n asn1_length_min asn1_length_max }

(* Defining the min and max length of the serialization of ASN1 _value_, not Tag-Len-Value tuples. Note
   that a ASN1 tag always take 1 byte to serialize, a ASN1 length (of value) at most take 5 bytes to
   serialize. Thus the valid length range of ASN1 value's serialization is [asn1_length_min, asn1_length_max - 6].
   Specifically:
   1. BOOLEAN value takes 1 byte;
   2. INTEGER value takes 1-4 bytes (only positive signed integers, see `ASN1.Spec.Value.INTEGER` for details);
   3. ASN1_NULL value takes 0 bytes;
   4. OCTET_STRING value can take any valid ASN1 value length/size to serialize;
   5. OID is stored as OCTET_STRING;
   6. BIT_STRING value could take arbitrary greater-than-zero valid ASN1 value length/size of bytes, since
      it always take one byte to store the `unused_bits`, see `ASN1.Spec.Value.BIT_STRING` for details;
   7. SEQUENCE value could take arbitrary valid ASN1 value length/size of bytes. *)
inline_for_extraction noextract unfold
[@@ "opaque_to_smt"]
let asn1_value_length_min_of_type
  (a: asn1_tag_t)
: asn1_length_t
= match a with
  | BOOLEAN      -> 1                 (* Any `BOOLEAN` value {true, false} has length 1. *)
  | INTEGER      -> 1                 (* `INTEGER` values range in [0x00, 0x7F] has length 1. *)
  | ASN1_NULL    -> 0                 (* Any `ASN1_NULL` value has nothing to serialize and has length 0. *)
  | OCTET_STRING
  | IA5_STRING
  | PRINTABLE_STRING  -> asn1_length_min   (* An empty `OCTET_STRING` [] has length 0. *)
  | OID          -> asn1_length_min   (* `OID` is just `OCTET_STRING`. *)
  | UTC_TIME -> 13
  | Generalized_Time -> 15
  | BIT_STRING   -> 1                 (* An empty `BIT_STRING` with a leading byte of `unused_bits` has length 0. *)
  | SEQUENCE     -> asn1_length_min   (* An empty `SEQUENCE` has length 0. *)
  | SET          -> asn1_length_min   (* An empty `SET` has length 0. *)
  | CUSTOM_TAG _ _ _ -> asn1_length_min

inline_for_extraction noextract unfold
[@@ "opaque_to_smt"]
let asn1_value_length_max_of_type
  (a: asn1_tag_t)
: asn1_length_t
= match a with
  | BOOLEAN      -> 1                    (* Any `BOOLEAN` value {true, false} has length 1. *)
  | INTEGER      -> 4                    (* `INTEGER` values range in (0x7FFFFF, 0x7FFFFFFF] has length 4. *)
  | ASN1_NULL    -> 0                    (* Any `ASN1_NULL` value has nothing to serialize and has length 0. *)
  | OCTET_STRING
  | IA5_STRING
  | PRINTABLE_STRING -> asn1_length_max - 6  (* An `OCTET_STRING` of size `asn1_length_max - 6`. *)
  | OID          -> asn1_length_max - 6  (* `OID` is just `OCTET_STRING`. *)
  | UTC_TIME -> 13
  | Generalized_Time -> 15
  | BIT_STRING   -> asn1_length_max - 6  (* An `BIT_STRING` of size `asn1_length_max - 7` with a leading byte of `unused_bits`. *)
  | SEQUENCE     -> asn1_length_max - 6  (* An `SEQUENCE` whose value has length `asn1_length_max - 6` *)
  | SET          -> asn1_length_max - 6  (* An `SET` whose value has length `asn1_length_max - 6` *)
  | CUSTOM_TAG _ _ _ -> asn1_length_max - 6

/// Helper to assert a length `l` is a valid ASN1 value length of the given type `a`
noextract unfold
[@@ "opaque_to_smt"]
let asn1_value_length_inbound_of_type
  (a: asn1_tag_t) (l: nat)
: bool
= let min, max = asn1_value_length_min_of_type a, asn1_value_length_max_of_type a in
  asn1_length_inbound l min max

/// Valid ASN1 Value length subtype for a given type`a`
noextract unfold
[@@ "opaque_to_smt"]
let asn1_value_length_of_type
  (a: asn1_tag_t)
= l: asn1_length_t {asn1_value_length_inbound_of_type a l}

///////////////////////////////////////////////////////////////////////////
/////      bounded mathematical integers for ASN1 TLV lengths
///// Defines the valid length/size of a ASN1 DER Tag-Length-Value tuple
///////////////////////////////////////////////////////////////////////////

(* NOTE: The valid TLV length range of a ASN1 type is its valid value length
         range plus the corresponding Tag-Length length.
*)
noextract unfold
[@@ "opaque_to_smt"]
let asn1_TLV_length_min_of_type
  (a: asn1_tag_t)
: asn1_length_t
= match a with        (* Tag Len Val *)
  | BOOLEAN      -> 3 (*  1 + 1 + 1  *)
  | INTEGER      -> 3 (*  1 + 1 + 1  *)
  | ASN1_NULL    -> 2 (*  1 + 1 + 0  *)
  | OCTET_STRING
  | IA5_STRING
  | PRINTABLE_STRING -> 2 (*  1 + 1 + 0  *)
  | OID          -> 2 (*  1 + 1 + 0  *)
  | UTC_TIME -> 15
  | Generalized_Time -> 17
  | BIT_STRING   -> 3 (*  1 + 1 + 1  *)
  | SEQUENCE     -> 2 (*  1 + 1 + 0  *)
  | SET          -> 2 (*  1 + 1 + 0  *)
  | CUSTOM_TAG _ _ _ -> 2

noextract unfold
[@@ "opaque_to_smt"]
let asn1_TLV_length_max_of_type
  (a: asn1_tag_t)
: asn1_length_t
= match a with                       (* Tag Len Val *)
  | BOOLEAN      -> 3                (*  1 + 1 + 1  *)
  | INTEGER      -> 6                (*  1 + 1 + 4  *)
  | ASN1_NULL    -> 2                (*  1 + 1 + 0  *)
  | OCTET_STRING
  | IA5_STRING
  | PRINTABLE_STRING -> asn1_length_max  (*  1 + 5 + _  *)
  | OID          -> asn1_length_max  (*  1 + 5 + _  *)
  | UTC_TIME -> 15
  | Generalized_Time -> 17
  | BIT_STRING   -> asn1_length_max  (*  1 + 5 + _  *)
  | SEQUENCE     -> asn1_length_max  (*  1 + 5 + _  *)
  | SET          -> asn1_length_max  (*  1 + 5 + _  *)
  | CUSTOM_TAG _ _ _ -> asn1_length_max

/// Helper to assert a length `l` is a valid ASN1 TLV length of the given type `a`
noextract unfold
[@@ "opaque_to_smt"]
let asn1_TLV_length_inbound_of_type
  (a: asn1_tag_t) (x: nat)
: bool
= let min, max = asn1_TLV_length_min_of_type a, asn1_TLV_length_max_of_type a in
  asn1_length_inbound x min max

/// Valid ASN1 TLV length subtype for a given type`a`
noextract unfold
[@@ "opaque_to_smt"]
let asn1_TLV_length_of_type
  (a: asn1_tag_t)
= l: asn1_length_t {asn1_TLV_length_inbound_of_type a l}



///////////////////////////////////////////////////////////////////////////
/////      bounded machine integers for ASN1 TLV lengths
///// Defines the valid length/size of a ASN1 DER Tag-Length-Value tuple
////  Same as above, specified using the above definitions
///////////////////////////////////////////////////////////////////////////
unfold
/
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
min: FStar.Integers.nat -> max: FStar.Integers.nat -> x: FStar.UInt32.t -> Prims.GTot Prims.bool
FStar.Integers.nat FStar.UInt32.t Prims.op_Negation Prims.op_BarBar FStar.Integers.op_Less FStar.Integers.Signed FStar.Integers.Winfinite FStar.UInt32.v Prims.bool
let asn1_int32_inbounds (min max: nat) (x: U32.t) : GTot bool =
  
not (U32.v x < min || max < U32.v x)