val ie_priv_list : Prims.list Lib.IntTypes.uint8
let ie_priv_list = List.Tot.map u8_from_UInt8 [
  0x60uy;  0x32uy;  0x0Duy;  0xB7uy;  0x31uy;  0x58uy;  0xA3uy;  0x5Auy;  0x25uy;  0x5Duy; 
  0x05uy;  0x17uy;  0x58uy;  0xE9uy;  0x5Euy;  0xD4uy;  0xABuy;  0xB2uy;  0xCDuy;  0xC6uy; 
  0x9Buy;  0xB4uy;  0x54uy;  0x11uy;  0x0Euy;  0x82uy;  0x74uy;  0x41uy;  0x21uy;  0x3Duy; 
  0xDCuy;  0x47uy ]
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 *)

(* is_priv = "60C6697351FF4AEC29CDBAABF2FBE3467CC254F81BE8E78D765A2E63339FC95A" *)
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 ]

let is_priv : lbytes 32 =
  assert_norm(FStar.List.length is_priv_list = 32);
  of_list is_priv_list
/
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 ie_priv_list =
  
List.Tot.map u8_from_UInt8
  [
    0x60uy; 0x32uy; 0x0Duy; 0xB7uy; 0x31uy; 0x58uy; 0xA3uy; 0x5Auy; 0x25uy; 0x5Duy; 0x05uy; 0x17uy;
    0x58uy; 0xE9uy; 0x5Euy; 0xD4uy; 0xABuy; 0xB2uy; 0xCDuy; 0xC6uy; 0x9Buy; 0xB4uy; 0x54uy; 0x11uy;
    0x0Euy; 0x82uy; 0x74uy; 0x41uy; 0x21uy; 0x3Duy; 0xDCuy; 0x47uy
  ]