val create_device_IKpsk2
      (prologue: hashable wgc)
      (info: string)
      (sk: option aead_key)
      (static_identity: private_key wgc)
    : option (device_IKpsk2)
val create_device_IKpsk2
      (prologue: hashable wgc)
      (info: string)
      (sk: option aead_key)
      (static_identity: private_key wgc)
    : option (device_IKpsk2)
let create_device_IKpsk2 (prologue : hashable wgc) (info : string)
                         (sk : option aead_key)
                         (static_identity : private_key wgc) :
  option (device_IKpsk2) =
  create_device dconfig_IKpsk2 pattern_IKpsk2 prologue info sk (Some static_identity)
module Spec.Noise.API.Instances

open Spec.Noise
open Spec.Noise.Instances
open Spec.Noise.API.Device
open Spec.Noise.API.Session
open Spec.Noise.SPatterns
open Lib.Sequence
open Lib.ByteSequence
open Lib.RandomSequence
module S = Impl.Noise.String

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

(*** IKpsk2*)
/// Redefining string with more constraints
type string = s:string{
  String.length s <= pow2 31 /\
  (forall (i:nat{i < String.length s}). S.char_v (String.index s i) <= 255)
  }

(** Configuration *)
/// We don't accept any unknown static key
let policy_IKpsk2 : policy_function wgc = fun k -> false

/// For IKpsk2, the certification is useless: as we don't accept any unknown keys,
/// we don't need to certify received keys by using the payload.
let certification_IKpsk2 : certification_function wgc string unit =
  fun () k h -> None

let dconfig_IKpsk2 = {
  dc_nc = wgc;
  dc_info = string;
  dc_info_to_bytes = (fun s -> S.seq_char_to_uint8 (S.string_to_seq s));
  dc_policy = policy_IKpsk2;
  dc_cert_state = unit;
  dc_certification = certification_IKpsk2;
}

(** Device *)
type device_IKpsk2 = device dconfig_IKpsk2
/
Spec.Noise.SPatterns.fst.checked Spec.Noise.Instances.fst.checked Spec.Noise.API.Session.fsti.checked Spec.Noise.API.Device.fsti.checked Spec.Noise.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RandomSequence.fsti.checked Lib.ByteSequence.fsti.checked Impl.Noise.String.fst.checked FStar.String.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Spec.Noise.API.Instances.fst

    prologue: Spec.Noise.CryptoPrimitives.hashable Spec.Noise.Instances.wgc ->
    info: Spec.Noise.API.Instances.string ->
    sk: FStar.Pervasives.Native.option Spec.Noise.CryptoPrimitives.aead_key ->
    static_identity: Spec.Noise.CryptoPrimitives.private_key Spec.Noise.Instances.wgc
  -> FStar.Pervasives.Native.option Spec.Noise.API.Instances.device_IKpsk2
Spec.Noise.CryptoPrimitives.hashable Spec.Noise.Instances.wgc Spec.Noise.API.Instances.string FStar.Pervasives.Native.option Spec.Noise.CryptoPrimitives.aead_key Spec.Noise.CryptoPrimitives.private_key Spec.Noise.API.Device.Definitions.create_device Spec.Noise.API.Instances.dconfig_IKpsk2 Spec.Noise.SPatterns.pattern_IKpsk2 FStar.Pervasives.Native.Some Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_nc Spec.Noise.API.Instances.device_IKpsk2
let create_device_IKpsk2
      (prologue: hashable wgc)
      (info: string)
      (sk: option aead_key)
      (static_identity: private_key wgc)
    : option (device_IKpsk2) =
  
create_device dconfig_IKpsk2 pattern_IKpsk2 prologue info sk (Some static_identity)