val pubkey_t : Type0
let pubkey_t
  // (pubkey_alg: supported_crypto_alg_t)
=
  // match pubkey_alg with
  // | AlgID_ECDSA_P256 -> datatype_of_asn1_type BIT_STRING
  // | AlgID_Ed25519    ->
  bs: datatype_of_asn1_type BIT_STRING
                     { bs.bs_len == 33ul /\
                       bs.bs_unused_bits == 0ul}
module X509.Base

open ASN1.Base

(* Disabling them for now *)
// type supported_crypto_alg_t =
// | AlgID_ECDSA_P256
// | AlgID_Ed25519

unfold
let pubkey_len
  // (pubkey_alg: supported_crypto_alg_t)
=
  // match pubkey_alg with
  // | AlgID_ECDSA_P256 -> 32ul
  // | AlgID_Ed25519    ->
  32ul
/
prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked ASN1.Base.fst.checked
X509.Base.fst
Type0
ASN1.Base.datatype_of_asn1_type ASN1.Base.BIT_STRING Prims.l_and Prims.eq2 FStar.UInt32.t ASN1.Base.__proj__Mkbit_string_t__item__bs_len FStar.UInt32.__uint_to_t ASN1.Base.__proj__Mkbit_string_t__item__bs_unused_bits
let pubkey_t =
  
bs: datatype_of_asn1_type BIT_STRING {bs.bs_len == 33ul /\ bs.bs_unused_bits == 0ul}