val timestamp_vs : Lib.IntTypes.size_t
let timestamp_vs = size timestamp_vsv
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"
[@@ noextract_to "krml"] noextract
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)
#pop-options

[@@ noextract_to "krml"]
inline_for_extraction noextract
/
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
Lib.IntTypes.size_t
Lib.IntTypes.size Impl.Noise.Instances.Test.timestamp_vsv
let timestamp_vs =
  
size timestamp_vsv