val certification_IKpsk2:certification_function wgc string unit
val certification_IKpsk2:certification_function wgc string unit
let certification_IKpsk2 : certification_function wgc string unit =
  fun () k h -> None
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,
/
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
Spec.Noise.API.Device.Definitions.certification_function Spec.Noise.Instances.wgc
  Spec.Noise.API.Instances.string
  Prims.unit
Prims.unit Spec.Noise.CryptoPrimitives.public_key Spec.Noise.Instances.wgc Spec.Noise.CryptoPrimitives.hashable FStar.Pervasives.Native.None Spec.Noise.API.Instances.string FStar.Pervasives.Native.option
let certification_IKpsk2:certification_function wgc string unit =
  
fun () k h -> None