val perform_IKpsk2_handshake_initiation_ (ist rst: handshake_state Spec.wgc) (ts: Spec.timestamp)
    : Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc)))
val perform_IKpsk2_handshake_initiation_ (ist rst: handshake_state Spec.wgc) (ts: Spec.timestamp)
    : Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc)))
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)
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)
/
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

    ist: Spec.Noise.Base.Definitions.handshake_state Spec.Noise.Instances.wgc ->
    rst: Spec.Noise.Base.Definitions.handshake_state Spec.Noise.Instances.wgc ->
    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.Base.Definitions.handshake_state Spec.Noise.Instances.wgc Spec.Noise.Instances.timestamp Spec.Noise.Instances.create_initiation_IKpsk2 Spec.Noise.Base.Definitions.error FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 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.consume_initiation_IKpsk2 Spec.Noise.CryptoPrimitives.hashable FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option
let perform_IKpsk2_handshake_initiation_ (ist rst: handshake_state Spec.wgc) (ts: Spec.timestamp)
    : Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  
match Spec.create_initiation_IKpsk2 ts ist with
| Fail e -> None
| Res (msg, ist1) ->
  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)