val oid_node_COUNTRY_US : Prims.list FStar.UInt8.t
let oid_node_COUNTRY_US     = normalize_term([0x86uy; 0x48uy])
module ASN1.Spec.Value.OID

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open LowParse.Spec.SeqBytes.Base

open FStar.Integers

#set-options "--fuel 15 --ifuel 1"

(* Top level OID tuples
  =====================
#define MBEDTLS_OID_ISO_MEMBER_BODIES           "\x2a"          /* {iso(1) member-body(2)} */
#define MBEDTLS_OID_ISO_IDENTIFIED_ORG          "\x2b"          /* {iso(1) identified-organization(3)} */
#define MBEDTLS_OID_ISO_CCITT_DS                "\x55"          /* {joint-iso-ccitt(2) ds(5)} */
#define MBEDTLS_OID_ISO_ITU_COUNTRY             "\x60"          /* {joint-iso-itu-t(2) country(16)} */
*)
noextract inline_for_extraction let oid_head_ISO_MEMBER_BODIES  = normalize_term([0x2Auy])
noextract inline_for_extraction let oid_head_ISO_IDENTIFIED_ORG = normalize_term([0x2Buy])
noextract inline_for_extraction let oid_head_ISO_CCITT_DS       = normalize_term([0x55uy])
noextract inline_for_extraction let oid_head_ISO_ITU_COUNTRY    = normalize_term([0x60uy])

(* ISO Member bodies OID parts
  ============================
#define MBEDTLS_OID_COUNTRY_US                  "\x86\x48"      /* {us(840)} */
#define MBEDTLS_OID_ORG_RSA_DATA_SECURITY       "\x86\xf7\x0d"  /* {rsadsi(113549)} */
#define MBEDTLS_OID_RSA_COMPANY                 MBEDTLS_OID_ISO_MEMBER_BODIES MBEDTLS_OID_COUNTRY_US \
                                        MBEDTLS_OID_ORG_RSA_DATA_SECURITY /* {iso(1) member-body(2) us(840) rsadsi(113549)} */
#define MBEDTLS_OID_ORG_ANSI_X9_62              "\xce\x3d" /* ansi-X9-62(10045) */
#define MBEDTLS_OID_ANSI_X9_62                  MBEDTLS_OID_ISO_MEMBER_BODIES MBEDTLS_OID_COUNTRY_US \
                                        MBEDTLS_OID_ORG_ANSI_X9_62
/
prims.fst.checked LowParse.Spec.SeqBytes.Base.fst.checked FStar.UInt8.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Integers.fst.checked FStar.BigOps.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.OID.fst
Prims.list FStar.UInt8.t
FStar.Pervasives.normalize_term Prims.list FStar.UInt8.t Prims.Cons FStar.UInt8.__uint_to_t Prims.Nil
let oid_node_COUNTRY_US =
  
normalize_term ([0x86uy; 0x48uy])