val perform_IKpsk2_handshake
      (is ie rs re: keypair Spec.wgc)
      (psk: preshared_key)
      (ts: Spec.timestamp)
    : Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc)))
val perform_IKpsk2_handshake
      (is ie rs re: keypair Spec.wgc)
      (psk: preshared_key)
      (ts: Spec.timestamp)
    : Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc)))
let perform_IKpsk2_handshake (is ie rs re : keypair Spec.wgc)
                             (psk : preshared_key)
                             (ts : Spec.timestamp) :
  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 ->
    (* Create initiation *)
    match Spec.create_initiation_IKpsk2 ts ist0 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 rst0 with
      | Fail e -> None
      | Res (ts', rst1) ->
        (* Set the preshared keys before the response message *)
        let ist1 = Spec.Noise.Base.set_psk psk ist1 in
        let rst1 = Spec.Noise.Base.set_psk psk rst1 in
        (* Create response *)
        match Spec.create_response_IKpsk2 rst1 with
        | Fail e -> None
        | Res (response, rst2) ->
          (* Consume response *)
          if S.length response > max_size_t then None else
          match Spec.consume_response_IKpsk2 response ist1 with
          | Fail e -> None
          | Res (eps, ist2) ->
            if S.length eps > 0 then None else
            Some (ist2, rst2)
module Impl.Noise.Instances.Test

open FStar.Mul
open FStar.HyperStack
open 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 15 --fuel 0 --ifuel 0"

(* Align the .fst and the .fsti *)
private val _align_beg : unit

(*** IKpsk2 *)
(**** Handshake test *)
#push-options "--z3rlimit 50 --ifuel 1"
/
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.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
Impl.Noise.Instances.Test.fsti

    is: Spec.Noise.CryptoPrimitives.keypair Spec.Noise.Instances.wgc ->
    ie: Spec.Noise.CryptoPrimitives.keypair Spec.Noise.Instances.wgc ->
    rs: Spec.Noise.CryptoPrimitives.keypair Spec.Noise.Instances.wgc ->
    re: Spec.Noise.CryptoPrimitives.keypair Spec.Noise.Instances.wgc ->
    psk: Spec.Noise.CryptoPrimitives.preshared_key ->
    ts: Spec.Noise.Instances.timestamp
  -> FStar.Pervasives.Native.option (Spec.Noise.Base.Definitions.handshake_state Spec.Noise.Instances.wgc
         *
        Spec.Noise.Base.Definitions.handshake_state Spec.Noise.Instances.wgc)
Spec.Noise.CryptoPrimitives.keypair Spec.Noise.Instances.wgc Spec.Noise.CryptoPrimitives.preshared_key Spec.Noise.Instances.timestamp Spec.Noise.Base.Definitions.pre_error FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 Spec.Noise.Base.Definitions.handshake_state Lib.ByteSequence.bytes Prims.op_GreaterThan Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.max_size_t Prims.bool Spec.Noise.Instances.create_initiation_IKpsk2 Spec.Noise.Base.Definitions.error Spec.Noise.Instances.consume_initiation_IKpsk2 Spec.Noise.CryptoPrimitives.hashable Spec.Noise.Instances.create_response_IKpsk2 Spec.Noise.Instances.consume_response_IKpsk2 FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option Spec.Noise.Base.Definitions.set_psk Spec.Noise.Base.Definitions.peresult Spec.Noise.Instances.receive_premessage_IKpsk2 Lib.Sequence.seq Lib.IntTypes.int_t Spec.Noise.Instances.send_premessage_IKpsk2 Spec.Noise.Instances.initialize_IKpsk2 Spec.Noise.Instances.protocol_IKpsk2_prologue
let perform_IKpsk2_handshake
      (is ie rs re: keypair Spec.wgc)
      (psk: preshared_key)
      (ts: Spec.timestamp)
    : Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  
let pist = Spec.initialize_IKpsk2 Spec.protocol_IKpsk2_prologue is ie in
let prst = Spec.initialize_IKpsk2 Spec.protocol_IKpsk2_prologue rs re in
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 ->
      match Spec.create_initiation_IKpsk2 ts ist0 with
      | Fail e -> None
      | Res (msg, ist1) ->
        if S.length msg > max_size_t
        then None
        else
          match Spec.consume_initiation_IKpsk2 msg rst0 with
          | Fail e -> None
          | Res (ts', rst1) ->
            let ist1 = Spec.Noise.Base.set_psk psk ist1 in
            let rst1 = Spec.Noise.Base.set_psk psk rst1 in
            match Spec.create_response_IKpsk2 rst1 with
            | Fail e -> None
            | Res (response, rst2) ->
              if S.length response > max_size_t
              then None
              else
                match Spec.consume_response_IKpsk2 response ist1 with
                | Fail e -> None
                | Res (eps, ist2) -> if S.length eps > 0 then None else Some (ist2, rst2)