val pattern : Spec.Noise.SPatterns.wfs_handshake_pattern
let pattern = pattern_IKpsk2
/// Noise_IKpsk2_25519_ChaChaPoly_BLAKE2s instantiation of the NoiseAPI

module Impl.Noise.API.Instances.IKpsk2_25519_ChaChaPoly_BLAKE2s

open Lib.IntTypes

open Impl.Noise.Types
open Impl.Noise.CipherState
open Impl.Noise.SymmetricState
open Impl.Noise.HandshakeState
open Impl.Noise.API.Device
open Impl.Noise.API.DState
open Impl.Noise.API.Session
open Impl.Noise.String
open Spec.Noise

open Meta.Noise
open Impl.Noise.API.Instances.Common_25519_ChaChaPoly_BLAKE2s

module St = Impl.Noise.Stateful
module T = FStar.Tactics

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

// Aligning the .fsti
val _align_fsti : unit
/
Spec.Noise.fst.checked prims.fst.checked Meta.Noise.fsti.checked Lib.IntTypes.fsti.checked Impl.Noise.Types.fst.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.String.fst.checked Impl.Noise.Stateful.fst.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.CipherState.fsti.checked Impl.Noise.API.Session.fsti.checked Impl.Noise.API.Instances.Common_25519_ChaChaPoly_BLAKE2s.fst.checked Impl.Noise.API.DState.fsti.checked Impl.Noise.API.Device.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Impl.Noise.API.Instances.IKpsk2_25519_ChaChaPoly_BLAKE2s.fsti
Spec.Noise.SPatterns.wfs_handshake_pattern
Spec.Noise.SPatterns.pattern_IKpsk2
let pattern =
  
pattern_IKpsk2