val re_priv_list : Prims.list Lib.IntTypes.uint8
let re_priv_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x1Auy;  0xFEuy;  0x43uy;  0xFBuy;  0xFAuy;  0xAAuy;  0x3Auy;  0xFBuy;  0x29uy; 
  0xD1uy;  0xE6uy;  0x05uy;  0x3Cuy;  0x7Cuy;  0x94uy;  0x75uy;  0xD8uy;  0xBEuy;  0x61uy; 
  0x89uy;  0xF9uy;  0x5Cuy;  0xBBuy;  0xA8uy;  0x99uy;  0x0Fuy;  0x95uy;  0xB1uy;  0xEBuy; 
  0xF1uy;  0x73uy ]
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

(* ie_priv = "60320DB73158A35A255D051758E95ED4ABB2CDC69BB454110E827441213DDC47" *)
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 ]

let ie_priv : lbytes 32 =
  assert_norm(FStar.List.length ie_priv_list = 32);
  of_list ie_priv_list

(* rs_priv = "70E93EA141E1FC673E017E97EADC6B968F385C2AECB03BFB32AF3C54EC18DB5C" *)
let rs_priv_list = List.Tot.map u8_from_UInt8 [
  0x70uy;  0xE9uy;  0x3Euy;  0xA1uy;  0x41uy;  0xE1uy;  0xFCuy;  0x67uy;  0x3Euy;  0x01uy; 
  0x7Euy;  0x97uy;  0xEAuy;  0xDCuy;  0x6Buy;  0x96uy;  0x8Fuy;  0x38uy;  0x5Cuy;  0x2Auy; 
  0xECuy;  0xB0uy;  0x3Buy;  0xFBuy;  0x32uy;  0xAFuy;  0x3Cuy;  0x54uy;  0xECuy;  0x18uy; 
  0xDBuy;  0x5Cuy ]

let rs_priv : lbytes 32 =
  assert_norm(FStar.List.length rs_priv_list = 32);
  of_list rs_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 re_priv_list =
  
List.Tot.map u8_from_UInt8
  [
    0x00uy; 0x1Auy; 0xFEuy; 0x43uy; 0xFBuy; 0xFAuy; 0xAAuy; 0x3Auy; 0xFBuy; 0x29uy; 0xD1uy; 0xE6uy;
    0x05uy; 0x3Cuy; 0x7Cuy; 0x94uy; 0x75uy; 0xD8uy; 0xBEuy; 0x61uy; 0x89uy; 0xF9uy; 0x5Cuy; 0xBBuy;
    0xA8uy; 0x99uy; 0x0Fuy; 0x95uy; 0xB1uy; 0xEBuy; 0xF1uy; 0x73uy
  ]