val cperform_IKpsk2_handshake_init_pre_post : pname: Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc 37ul ->
    prologue: Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc 34ul ->
    is: Impl.Noise.FlatStructures.keypair_t Impl.Noise.Instances.wg_inc ->
    ie: Impl.Noise.FlatStructures.keypair_t Impl.Noise.Instances.wg_inc ->
    rs: Impl.Noise.FlatStructures.keypair_t Impl.Noise.Instances.wg_inc ->
    re: Impl.Noise.FlatStructures.keypair_t Impl.Noise.Instances.wg_inc ->
    ist: Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc ->
    rst: Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc ->
    h0: FStar.Monotonic.HyperStack.mem ->
    r: Prims.unit ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Prims.logical
let cperform_IKpsk2_handshake_init_pre_post
  (pname : hashable_t wg_inc 37ul) (prologue : hashable_t wg_inc 34ul)
  (is ie rs re : keypair_t wg_inc)
  (ist rst : handshake_state_t wg_inc)
  (h0 : mem) (r : unit) (h1 : mem) =
  let is_v = eval_keypair h0 is in
  let ie_v = eval_keypair h0 ie in
  let rs_v = eval_keypair h0 rs in
  let re_v = eval_keypair h0 re in
  (**)
  let ismi = csend_message_pre_smi Spec.pattern_IKpsk2 false 0 in
  let rsmi = creceive_message_pre_smi Spec.pattern_IKpsk2 false 0 in
  (**)
  let ist_v1 = eval_handshake_state h1 ist ismi in
  let rst_v1 = eval_handshake_state h1 rst rsmi in
  let r_v1 = perform_IKpsk2_handshake_init_pre_ is_v ie_v rs_v re_v in
  match r_v1 with
  | None -> False
  | Some (ist_v1', rst_v1') ->
    rst_v1' == rst_v1 /\ ist_v1' == ist_v1
module Impl.Noise.Instances.Test

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST
module HST = FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Sequence
module S = Lib.Sequence

module BS = Lib.ByteSequence
open Lib.Buffer
open LowStar.BufferOps

open Spec.Noise
module Spec = Spec.Noise.Instances
open Impl.Noise.Types
open Impl.Noise.FlatStructures
open Impl.Noise.PatternMessages
open Impl.Noise.Instances

#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(* Align the .fst and the .fsti *)
let _align_beg = ()

(*** IKpsk2 *)
(**** Handshake test *)
[@@ noextract_to "krml"] noextract
let perform_IKpsk2_handshake_init_pre_ (is ie rs re : keypair Spec.wgc) :
  Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  (* Initialize *)
  let pist = Spec.initialize_IKpsk2 Spec.protocol_IKpsk2_prologue is ie in
  let prst = Spec.initialize_IKpsk2 Spec.protocol_IKpsk2_prologue rs re in
  (* Exchange the premessage *)
  let prres = Spec.send_premessage_IKpsk2 prst in
  match prres with
  | Fail e -> None
  | Res (pmsg, rst0) ->
    if S.length pmsg > max_size_t then None else
    let pires = Spec.receive_premessage_IKpsk2 pmsg pist in
    match pires with
    | Fail e -> None
    | Res ist0 ->
      Some (ist0, rst0)

[@@ noextract_to "krml"] noextract
let perform_IKpsk2_handshake_initiation_ (ist rst : handshake_state Spec.wgc)
                                         (ts : Spec.timestamp) :
  Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  (* Create initiation *)
  match Spec.create_initiation_IKpsk2 ts ist with
  | Fail e  -> None
  | Res (msg, ist1) ->
    (* Consume initiation *)
    if S.length msg > max_size_t then None else
    match Spec.consume_initiation_IKpsk2 msg rst with
    | Fail e -> None
    | Res (ts', rst1) ->
      Some(ist1, rst1)

[@@ noextract_to "krml"] noextract
let perform_IKpsk2_handshake_response_ (ist rst : handshake_state Spec.wgc) :
  Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  (* Create response *)
  match Spec.create_response_IKpsk2 rst with
  | Fail e  -> None
  | Res (msg, rst1) ->
    (* Consume response *)
    if S.length msg > max_size_t then None else
    match Spec.consume_response_IKpsk2 msg ist with
    | Fail e -> None
    | Res (eps, ist1) ->
      if S.length eps > 0 then None else
      Some(ist1, rst1)

[@@ noextract_to "krml"] noextract
let perform_IKpsk2_handshake_decomposed_
  (is ie rs re : keypair Spec.wgc)
  (psk : preshared_key)
  (ts : Spec.timestamp) :
  Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  match perform_IKpsk2_handshake_init_pre_ is ie rs re with
  | None -> None
  | Some (ist1, rst1) ->
    match perform_IKpsk2_handshake_initiation_ ist1 rst1 ts with
    | None -> None
    | Some (ist2, rst2) ->
      let ist3 = Spec.Noise.Base.set_psk psk ist2 in
      let rst3 = Spec.Noise.Base.set_psk psk rst2 in
      perform_IKpsk2_handshake_response_ ist3 rst3

let perform_IKpsk2_handshake_decompose_lem
  (is ie rs re : keypair Spec.wgc)
  (psk : preshared_key)
  (ts : Spec.timestamp) :
  Lemma(
    perform_IKpsk2_handshake is ie rs re psk ts ==
    perform_IKpsk2_handshake_decomposed_ is ie rs re psk ts)
  = ()

[@@ noextract_to "krml"] inline_for_extraction noextract
let premessage_IKpsk2_len : n:size_nat{n > 0} =
  assert_norm(premessage_vsv wg_inc Spec.pattern_IKpsk2 false > 0);
  premessage_vsv wg_inc Spec.pattern_IKpsk2 false

[@@ noextract_to "krml"] inline_for_extraction noextract
let initiation_IKpsk2_len :
  n:size_nat{n == pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 /\ n > 0}
  =
  assert_norm(pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 <= max_size_t);
  assert_norm(pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 > 0);
  pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0

[@@ noextract_to "krml"] inline_for_extraction noextract
let response_IKpsk2_len :
  n:size_nat{n == pat_message_vsv wg_inc Spec.pattern_IKpsk2 0 1 /\ n > 0}
  =
  assert_norm(pat_message_vsv wg_inc Spec.pattern_IKpsk2 0 1 <= max_size_t);
  assert_norm(pat_message_vsv wg_inc Spec.pattern_IKpsk2 0 1 > 0);
  pat_message_vsv wg_inc Spec.pattern_IKpsk2 0 1

(** initialize and exchange premessages *)
/
Spec.Noise.Instances.fst.checked Spec.Noise.Base.fst.checked Spec.Noise.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked Impl.Noise.SendReceive.fsti.checked Impl.Noise.PatternMessages.fst.checked Impl.Noise.Instances.fst.checked Impl.Noise.FlatStructures.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.Instances.Test.fst

    pname: Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc 37ul ->
    prologue: Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc 34ul ->
    is: Impl.Noise.FlatStructures.keypair_t Impl.Noise.Instances.wg_inc ->
    ie: Impl.Noise.FlatStructures.keypair_t Impl.Noise.Instances.wg_inc ->
    rs: Impl.Noise.FlatStructures.keypair_t Impl.Noise.Instances.wg_inc ->
    re: Impl.Noise.FlatStructures.keypair_t Impl.Noise.Instances.wg_inc ->
    ist: Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc ->
    rst: Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc ->
    h0: FStar.Monotonic.HyperStack.mem ->
    r: Prims.unit ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Prims.logical
Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc FStar.UInt32.__uint_to_t Impl.Noise.FlatStructures.keypair_t Impl.Noise.FlatStructures.handshake_state_t FStar.Monotonic.HyperStack.mem Prims.unit Prims.l_False Spec.Noise.Base.Definitions.handshake_state Spec.Noise.Instances.wgc Prims.l_and Prims.eq2 Impl.Noise.Types.get_config Prims.logical FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 Impl.Noise.Instances.Test.perform_IKpsk2_handshake_init_pre_ Prims.bool FStar.Pervasives.Native.uu___is_Some Spec.Noise.CryptoPrimitives.aead_key Spec.Noise.Base.Definitions.__proj__Mkcipher_state__item__k Spec.Noise.Base.Definitions.__proj__Mksymmetric_state__item__c_state Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__sym_state Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__sk Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Spec.Noise.CryptoPrimitives.keypair Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__static Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__s Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__ephemeral Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__e Spec.Noise.CryptoPrimitives.public_key Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__remote_static Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__rs Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__remote_ephemeral Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__re Spec.Noise.CryptoPrimitives.preshared_key Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__preshared Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__psk Impl.Noise.FlatStructures.eval_handshake_state Spec.Noise.MetaInfo.meta_info Spec.Noise.MetaInfo.creceive_message_pre_smi Spec.Noise.Instances.pattern_IKpsk2 Spec.Noise.MetaInfo.csend_message_pre_smi Impl.Noise.FlatStructures.eval_keypair
let cperform_IKpsk2_handshake_init_pre_post
      (pname: hashable_t wg_inc 37ul)
      (prologue: hashable_t wg_inc 34ul)
      (is ie rs re: keypair_t wg_inc)
      (ist rst: handshake_state_t wg_inc)
      (h0: mem)
      (r: unit)
      (h1: mem)
     =
  
let is_v = eval_keypair h0 is in
let ie_v = eval_keypair h0 ie in
let rs_v = eval_keypair h0 rs in
let re_v = eval_keypair h0 re in
let ismi = csend_message_pre_smi Spec.pattern_IKpsk2 false 0 in
let rsmi = creceive_message_pre_smi Spec.pattern_IKpsk2 false 0 in
let ist_v1 = eval_handshake_state h1 ist ismi in
let rst_v1 = eval_handshake_state h1 rst rsmi in
let r_v1 = perform_IKpsk2_handshake_init_pre_ is_v ie_v rs_v re_v in
match r_v1 with
| None -> False
| Some (ist_v1', rst_v1') -> rst_v1' == rst_v1 /\ ist_v1' == ist_v1