val aliasKeyCrt_s_org_list:character_string_llist IA5_STRING aliasKeyCrt_s_org_len
val aliasKeyCrt_s_org_list:character_string_llist IA5_STRING aliasKeyCrt_s_org_len
let aliasKeyCrt_s_org_list
: character_string_llist IA5_STRING aliasKeyCrt_s_org_len
= [0x49uy; 0x6euy; 0x63uy; 0x2euy]
(* 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 *)
let aliasKeyCrt_serialNumber_len = 8ul
noextract inline_for_extraction 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]
let aliasKeyCrt_serialNumber_buf = IB.igcmalloc_of_list HS.root aliasKeyCrt_serialNumber_list
#pop-options

(* AliasKeyTBS Names *)
(* Common Name in IA5 (ASCII): `Platform Identity` *)
#push-options "--z3rlimit 50 --fuel 0"
let aliasKeyCrt_s_common_len = 17ul
noextract inline_for_extraction let aliasKeyCrt_s_common_list
: character_string_llist IA5_STRING aliasKeyCrt_s_common_len
= [@ inline_let]
  let l = [0x50uy; 0x6cuy; 0x61uy; 0x74uy;
           0x66uy; 0x6fuy; 0x72uy; 0x6duy;
           0x20uy; 0x49uy; 0x64uy; 0x65uy;
           0x6euy; 0x74uy; 0x69uy; 0x74uy;
           0x79uy] in
  assert_norm ( List.length l == 17 );
  assert (Seq.length (Seq.createL l) == 17);
  assert ( l == Seq.seq_to_list (Seq.createL l) );
  Seq.lemma_index_is_nth (Seq.createL l) 1;
  Seq.lemma_index_is_nth (Seq.createL l) 2;
  Seq.lemma_index_is_nth (Seq.createL l) 3;
  Seq.lemma_index_is_nth (Seq.createL l) 4;
  Seq.lemma_index_is_nth (Seq.createL l) 5;
  Seq.lemma_index_is_nth (Seq.createL l) 6;
  Seq.lemma_index_is_nth (Seq.createL l) 7;
  Seq.lemma_index_is_nth (Seq.createL l) 8;
  Seq.lemma_index_is_nth (Seq.createL l) 9;
  Seq.lemma_index_is_nth (Seq.createL l) 10;
  Seq.lemma_index_is_nth (Seq.createL l) 11;
  Seq.lemma_index_is_nth (Seq.createL l) 12;
  Seq.lemma_index_is_nth (Seq.createL l) 13;
  Seq.lemma_index_is_nth (Seq.createL l) 14;
  Seq.lemma_index_is_nth (Seq.createL l) 15;
  Seq.lemma_index_is_nth (Seq.createL l) 16;
  assert_norm ( l `List.Tot.index` 0  == 0x50uy /\
                l `List.Tot.index` 1  == 0x6cuy /\
                l `List.Tot.index` 2  == 0x61uy /\
                l `List.Tot.index` 3  == 0x74uy /\
                l `List.Tot.index` 4  == 0x66uy /\
                l `List.Tot.index` 5  == 0x6fuy /\
                l `List.Tot.index` 6  == 0x72uy /\
                l `List.Tot.index` 7  == 0x6duy /\
                l `List.Tot.index` 8  == 0x20uy /\
                l `List.Tot.index` 9  == 0x49uy /\
                l `List.Tot.index` 10 == 0x64uy /\
                l `List.Tot.index` 11 == 0x65uy /\
                l `List.Tot.index` 12 == 0x6euy /\
                l `List.Tot.index` 13 == 0x74uy /\
                l `List.Tot.index` 14 == 0x69uy /\
                l `List.Tot.index` 15 == 0x74uy /\
                l `List.Tot.index` 16 == 0x79uy );
  assert ( (Seq.createL l).[0]  == 0x50uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[0]);
  assert ( (Seq.createL l).[1]  == 0x6cuy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[1]);
  assert ( (Seq.createL l).[2]  == 0x61uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[2]);
  assert ( (Seq.createL l).[3]  == 0x74uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[3]);
  assert ( (Seq.createL l).[4]  == 0x66uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[4]);
  assert ( (Seq.createL l).[5]  == 0x6fuy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[5]);
  assert ( (Seq.createL l).[6]  == 0x72uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[6]);
  assert ( (Seq.createL l).[7]  == 0x6duy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[7]);
  assert ( (Seq.createL l).[8]  == 0x20uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[8]);
  assert ( (Seq.createL l).[9]  == 0x49uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[9]);
  assert ( (Seq.createL l).[10] == 0x64uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[10]);
  assert ( (Seq.createL l).[11] == 0x65uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[11]);
  assert ( (Seq.createL l).[12] == 0x6euy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[12]);
  assert ( (Seq.createL l).[13] == 0x74uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[13]);
  assert ( (Seq.createL l).[14] == 0x69uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[14]);
  assert ( (Seq.createL l).[15] == 0x74uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[15]);
  assert ( (Seq.createL l).[16] == 0x79uy /\ valid_character_string_byte IA5_STRING (Seq.createL l).[16]);
  l
let aliasKeyCrt_s_common_buf = IB.igcmalloc_of_list HS.root aliasKeyCrt_s_common_list

#push-options "--fuel 6"
/
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
ASN1.Base.character_string_llist ASN1.Base.IA5_STRING L0.Test.Definitions.aliasKeyCrt_s_org_len
Prims.Cons ASN1.Base.byte FStar.UInt8.__uint_to_t Prims.Nil
let aliasKeyCrt_s_org_list:character_string_llist IA5_STRING aliasKeyCrt_s_org_len =
  
[0x49uy; 0x6euy; 0x63uy; 0x2euy]