val aliasKeyCrt_serialNumber_list:l:
List.llist byte_pub (v aliasKeyCrt_serialNumber_len)
  { valid_big_integer_as_octet_string aliasKeyCrt_serialNumber_len (B32.hide (Seq.createL l)) /\
    filter_x509_serialNumber (asn1_get_big_integer_as_octet_string aliasKeyCrt_serialNumber_len
          (B32.hide (Seq.createL l))) }
val aliasKeyCrt_serialNumber_list:l:
List.llist byte_pub (v aliasKeyCrt_serialNumber_len)
  { valid_big_integer_as_octet_string aliasKeyCrt_serialNumber_len (B32.hide (Seq.createL l)) /\
    filter_x509_serialNumber (asn1_get_big_integer_as_octet_string aliasKeyCrt_serialNumber_len
          (B32.hide (Seq.createL l))) }
let aliasKeyCrt_serialNumber_list
: l: List.llist byte_pub (v aliasKeyCrt_serialNumber_len)
  { valid_big_integer_as_octet_string aliasKeyCrt_serialNumber_len (B32.hide (Seq.createL l)) /\
    filter_x509_serialNumber (asn1_get_big_integer_as_octet_string aliasKeyCrt_serialNumber_len (B32.hide (Seq.createL l))) }
= [0x27uy; 0x48uy; 0x4Buy; 0xD6uy;
   0xF2uy; 0x10uy; 0xB4uy; 0xDAuy]
(* NOTE: Separating this module because verification
         with L0.* loaded becomes expensive *)
module L0.Test.Definitions

open LowStar.Comment
open LowStar.Printf
module Fail = LowStar.Failure
module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module HS  = FStar.HyperStack
module HST = FStar.HyperStack.ST
module B32 = FStar.Bytes

open Lib.IntTypes
open Spec.Hash.Definitions
open Hacl.Hash.Definitions

open ASN1.Spec
open ASN1.Low
open X509

open L0.Base
open L0.X509.Base
open L0.Declassify
open L0.Helpers
// open L0.Spec
// open L0.Impl
// open L0.Core

module Ed25519 = Hacl.Ed25519

#set-options "--z3rlimit 64 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

let aliasKeyCrt_version: x509_version_t = normalize_term x509_version_3

#push-options "--fuel 9"
(* AliasKeyTBS SerialNumber *)
/
X509.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked LowStar.Printf.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.Failure.fsti.checked LowStar.Comment.fsti.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked L0.X509.Base.fst.checked L0.Helpers.fsti.checked L0.Declassify.fsti.checked L0.Base.fst.checked Hacl.Hash.Definitions.fst.checked Hacl.Ed25519.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
L0.Test.Definitions.fst
l:
FStar.List.Tot.Properties.llist (Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB)
  (Lib.IntTypes.v L0.Test.Definitions.aliasKeyCrt_serialNumber_len)
  { ASN1.Spec.Value.BigInteger.valid_big_integer_as_octet_string L0.Test.Definitions.aliasKeyCrt_serialNumber_len
      (FStar.Bytes.hide (FStar.Seq.Properties.createL l)) /\
    X509.BasicFields.SerialNumber.filter_x509_serialNumber (ASN1.Spec.Value.BigInteger.asn1_get_big_integer_as_octet_string
          L0.Test.Definitions.aliasKeyCrt_serialNumber_len
          (FStar.Bytes.hide (FStar.Seq.Properties.createL l))) }
Prims.Cons Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.PUB FStar.UInt8.__uint_to_t Prims.Nil
let aliasKeyCrt_serialNumber_list:l:
List.llist byte_pub (v aliasKeyCrt_serialNumber_len)
  { valid_big_integer_as_octet_string aliasKeyCrt_serialNumber_len (B32.hide (Seq.createL l)) /\
    filter_x509_serialNumber (asn1_get_big_integer_as_octet_string aliasKeyCrt_serialNumber_len
          (B32.hide (Seq.createL l))) } =
  
[0x27uy; 0x48uy; 0x4Buy; 0xD6uy; 0xF2uy; 0x10uy; 0xB4uy; 0xDAuy]