val oid_node_ORG_DOD : Prims.list FStar.UInt8.t
let oid_node_ORG_DOD = normalize_term([0x06uy])
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
*)
noextract inline_for_extraction let oid_node_COUNTRY_US     = normalize_term([0x86uy; 0x48uy])
noextract inline_for_extraction let oid_node_ORG_RSA_DATA_SECURITY = normalize_term([0x86uy; 0xF7uy; 0x0Duy])
noextract inline_for_extraction let oid_RSA_COMPANY         = normalize_term(oid_head_ISO_MEMBER_BODIES @ oid_node_COUNTRY_US @ oid_node_ORG_RSA_DATA_SECURITY)

noextract inline_for_extraction let oid_node_ORG_ANSI_X9_62 = normalize_term([0xceuy; 0x3duy])
noextract inline_for_extraction let oid_ANSI_X9_62          = normalize_term(oid_head_ISO_MEMBER_BODIES @ oid_node_ORG_ANSI_X9_62)

(* ISO ITU OID parts
  ==================
#define MBEDTLS_OID_ORGANIZATION                "\x01"          /* {organization(1)} */
#define MBEDTLS_OID_ISO_ITU_US_ORG              MBEDTLS_OID_ISO_ITU_COUNTRY MBEDTLS_OID_COUNTRY_US MBEDTLS_OID_ORGANIZATION /* {joint-iso-itu-t(2) country(16) us(840) organization(1)} */

#define MBEDTLS_OID_ORG_GOV                     "\x65"          /* {gov(101)} */
#define MBEDTLS_OID_GOV                         MBEDTLS_OID_ISO_ITU_US_ORG MBEDTLS_OID_ORG_GOV /* {joint-iso-itu-t(2) country(16) us(840) organization(1) gov(101)} */

#define MBEDTLS_OID_ORG_NETSCAPE                "\x86\xF8\x42"  /* {netscape(113730)} */
#define MBEDTLS_OID_NETSCAPE                    MBEDTLS_OID_ISO_ITU_US_ORG MBEDTLS_OID_ORG_NETSCAPE /* Netscape OID {joint-iso-itu-t(2) country(16) us(840) organization(1) netscape(113730)} */
*)
noextract inline_for_extraction let oid_node_ORGANIZATION = normalize_term([0x01uy])
noextract inline_for_extraction let oid_ISO_ITU_US_ORG    = normalize_term(oid_head_ISO_ITU_COUNTRY @ oid_node_COUNTRY_US @ oid_node_ORGANIZATION)

noextract inline_for_extraction let oid_node_ISO_ORG_GOV  = normalize_term([0x65uy])
noextract inline_for_extraction let oid_GOV               = normalize_term(oid_ISO_ITU_US_ORG @ oid_node_ISO_ORG_GOV)

(* ISO arc for standard certificate and CRL extensions
  =====================================================
#define MBEDTLS_OID_ID_CE                       MBEDTLS_OID_ISO_CCITT_DS "\x1D" /**< id-ce OBJECT IDENTIFIER  ::=  {joint-iso-ccitt(2) ds(5) 29} */

#define MBEDTLS_OID_NIST_ALG                    MBEDTLS_OID_GOV "\x03\x04" /** { joint-iso-itu-t(2) country(16) us(840) organization(1) gov(101) csor(3) nistAlgorithm(4) */
*)
noextract inline_for_extraction let oid_ID_CE    = normalize_term(oid_head_ISO_CCITT_DS @ [0x1Duy])

noextract inline_for_extraction let oid_NIST_ALG = normalize_term(oid_GOV @ [0x03uy; 0x04uy])

(* Private Internet Extensions
   { iso(1) identified-organization(3) dod(6) internet(1)
                        security(5) mechanisms(5) pkix(7) }
  =========================================================
#define MBEDTLS_OID_INTERNET                    MBEDTLS_OID_ISO_IDENTIFIED_ORG MBEDTLS_OID_ORG_DOD "\x01"
#define MBEDTLS_OID_PKIX                        MBEDTLS_OID_INTERNET "\x05\x05\x07"
/
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_ORG_DOD =
  
normalize_term ([0x06uy])