val is_priv_list : Prims.list Lib.IntTypes.uint8
let is_priv_list = List.Tot.map u8_from_UInt8 [
  0x60uy;  0xC6uy;  0x69uy;  0x73uy;  0x51uy;  0xFFuy;  0x4Auy;  0xECuy;  0x29uy;  0xCDuy; 
  0xBAuy;  0xABuy;  0xF2uy;  0xFBuy;  0xE3uy;  0x46uy;  0x7Cuy;  0xC2uy;  0x54uy;  0xF8uy; 
  0x1Buy;  0xE8uy;  0xE7uy;  0x8Duy;  0x76uy;  0x5Auy;  0x2Euy;  0x63uy;  0x33uy;  0x9Fuy; 
  0xC9uy;  0x5Auy ]
module Spec.Noise.XX.Test

open Spec.Noise
open Spec.Noise.Instances
open Spec.Noise.Utils

open FStar.All
module IO = FStar.IO
module List = FStar.List

open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence

#set-options "--z3rlimit 15 --fuel 0 --ifuel 0"

(*** XX handshake *)
/
Spec.Noise.Utils.fst.checked Spec.Noise.Instances.fst.checked Spec.Noise.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Spec.Noise.XX.Test.fst
Prims.list Lib.IntTypes.uint8
FStar.List.Tot.Base.map FStar.UInt8.t Lib.IntTypes.uint8 Lib.RawIntTypes.u8_from_UInt8 Prims.Cons FStar.UInt8.__uint_to_t Prims.Nil
let is_priv_list =
  
List.Tot.map u8_from_UInt8
  [
    0x60uy; 0xC6uy; 0x69uy; 0x73uy; 0x51uy; 0xFFuy; 0x4Auy; 0xECuy; 0x29uy; 0xCDuy; 0xBAuy; 0xABuy;
    0xF2uy; 0xFBuy; 0xE3uy; 0x46uy; 0x7Cuy; 0xC2uy; 0x54uy; 0xF8uy; 0x1Buy; 0xE8uy; 0xE7uy; 0x8Duy;
    0x76uy; 0x5Auy; 0x2Euy; 0x63uy; 0x33uy; 0x9Fuy; 0xC9uy; 0x5Auy
  ]