val write_IKpsk2 : payload: Spec.Noise.API.Session.encap_message -> sn: Spec.Noise.API.Instances.session_IKpsk2
  -> Spec.Noise.API.Session.sresult (Lib.ByteSequence.bytes *
        Spec.Noise.API.Session.session Spec.Noise.API.Instances.dconfig_IKpsk2)
let write_IKpsk2 (payload : encap_message) (sn : session_IKpsk2) =
  write #dconfig_IKpsk2 payload sn
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

// Will fail if we can't derive a public key from the private key
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)

let create_device_from_secret_IKpsk2
  (prologue : hashable wgc) (info : string)
  (sk : aead_key) (static_identity : enc_private_key_with_nonce dconfig_IKpsk2.dc_nc) :
  option (device_IKpsk2) =
  create_device_from_secret dconfig_IKpsk2 pattern_IKpsk2 prologue info sk (Some static_identity)

// The peer identifier is an arbitrary number, as opposed to the peer
// information, which should reflect a "meaningful" identity (usually the peer name).
let lookup_peer_by_id_IKpsk2 = lookup_peer_by_id #dconfig_IKpsk2
let lookup_peer_by_static_IKpsk2 = lookup_peer_by_static #dconfig_IKpsk2

// Calling this function will fail if there is already a peer in the device
// with [remote_static_key]. In the Low* implementation: it will leave the
// device unchanged.
let add_peer_IKpsk2
  (dv : device_IKpsk2) (pname : string) (remote_static_key : public_key wgc)
  (psk : preshared_key) : option (peer_id & device_IKpsk2) =
  add_peer #dconfig_IKpsk2 dv pname (Some remote_static_key) (Some psk)

// Remove a peer designated by its identifier.
// Does nothing if there is no peer with this identifier in the device.
let remove_peer_IKpsk2 = remove_peer #dconfig_IKpsk2

let serialize_device_secret_IKpsk2
  (dv : device_IKpsk2) (peer:peer dconfig_IKpsk2) (entr:entropy) :
  option bytes & entropy =
  serialize_peer_secret #dconfig_IKpsk2 dv peer entr

let serialize_peer_secret_IKpsk2 (dv : device_IKpsk2) (entr:entropy) :
  option bytes & entropy =
  serialize_device_secret #dconfig_IKpsk2 dv entr

let deserialize_device_secret_IKpsk2
  (dv : device_IKpsk2) (peer_name:string) (entr:entropy) (enc_keys : bytes) :
  option (peer dconfig_IKpsk2 & device_IKpsk2) =
  deserialize_peer_secret #dconfig_IKpsk2 dv peer_name true true enc_keys

(** Session *)
type session_IKpsk2 = session dconfig_IKpsk2

// Note that create_session might fail for several reasons
let create_initiator_IKpsk2 (dv : device_IKpsk2) (entr: entropy) (pid : peer_id) :
  sresult (session_IKpsk2 & device_IKpsk2) & entropy =
  create_session dv true entr (Some pid)
let create_responder_IKpsk2 (dv : device_IKpsk2) (entr: entropy) :
  sresult (session_IKpsk2 & device_IKpsk2) & entropy =
  create_session dv false entr None
/
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
payload: Spec.Noise.API.Session.encap_message -> sn: Spec.Noise.API.Instances.session_IKpsk2
  -> Spec.Noise.API.Session.sresult (Lib.ByteSequence.bytes *
        Spec.Noise.API.Session.session Spec.Noise.API.Instances.dconfig_IKpsk2)
Spec.Noise.API.Session.encap_message Spec.Noise.API.Instances.session_IKpsk2 Spec.Noise.API.Session.write Spec.Noise.API.Instances.dconfig_IKpsk2 Spec.Noise.API.Session.sresult FStar.Pervasives.Native.tuple2 Lib.ByteSequence.bytes Spec.Noise.API.Session.session
let write_IKpsk2 (payload: encap_message) (sn: session_IKpsk2) =
  
write #dconfig_IKpsk2 payload sn