val initiation_IKpsk2_len:n: size_nat{n == pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 /\ n > 0}
val initiation_IKpsk2_len:n: size_nat{n == pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 /\ n > 0}
let initiation_IKpsk2_len :
  n:size_nat{n == pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 /\ n > 0}
  =
  assert_norm(pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 <= max_size_t);
  assert_norm(pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 > 0);
  pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0
module Impl.Noise.Instances.Test

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST
module HST = 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 50 --fuel 1 --ifuel 1"

(* Align the .fst and the .fsti *)
let _align_beg = ()

(*** IKpsk2 *)
(**** Handshake test *)
[@@ noextract_to "krml"] noextract
let perform_IKpsk2_handshake_init_pre_ (is ie rs re : keypair Spec.wgc) :
  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 ->
      Some (ist0, rst0)

[@@ noextract_to "krml"] noextract
let perform_IKpsk2_handshake_initiation_ (ist rst : handshake_state Spec.wgc)
                                         (ts : Spec.timestamp) :
  Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  (* Create initiation *)
  match Spec.create_initiation_IKpsk2 ts ist 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 rst with
    | Fail e -> None
    | Res (ts', rst1) ->
      Some(ist1, rst1)

[@@ noextract_to "krml"] noextract
let perform_IKpsk2_handshake_response_ (ist rst : handshake_state Spec.wgc) :
  Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  (* Create response *)
  match Spec.create_response_IKpsk2 rst with
  | Fail e  -> None
  | Res (msg, rst1) ->
    (* Consume response *)
    if S.length msg > max_size_t then None else
    match Spec.consume_response_IKpsk2 msg ist with
    | Fail e -> None
    | Res (eps, ist1) ->
      if S.length eps > 0 then None else
      Some(ist1, rst1)

[@@ noextract_to "krml"] noextract
let perform_IKpsk2_handshake_decomposed_
  (is ie rs re : keypair Spec.wgc)
  (psk : preshared_key)
  (ts : Spec.timestamp) :
  Tot (option ((handshake_state Spec.wgc) & (handshake_state Spec.wgc))) =
  match perform_IKpsk2_handshake_init_pre_ is ie rs re with
  | None -> None
  | Some (ist1, rst1) ->
    match perform_IKpsk2_handshake_initiation_ ist1 rst1 ts with
    | None -> None
    | Some (ist2, rst2) ->
      let ist3 = Spec.Noise.Base.set_psk psk ist2 in
      let rst3 = Spec.Noise.Base.set_psk psk rst2 in
      perform_IKpsk2_handshake_response_ ist3 rst3

let perform_IKpsk2_handshake_decompose_lem
  (is ie rs re : keypair Spec.wgc)
  (psk : preshared_key)
  (ts : Spec.timestamp) :
  Lemma(
    perform_IKpsk2_handshake is ie rs re psk ts ==
    perform_IKpsk2_handshake_decomposed_ is ie rs re psk ts)
  = ()

[@@ noextract_to "krml"] inline_for_extraction noextract
let premessage_IKpsk2_len : n:size_nat{n > 0} =
  assert_norm(premessage_vsv wg_inc Spec.pattern_IKpsk2 false > 0);
  premessage_vsv wg_inc Spec.pattern_IKpsk2 false
/
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.SendReceive.fsti.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 FStar.Ghost.fsti.checked
Impl.Noise.Instances.Test.fst
n:
(n: Prims.nat{n <= Prims.pow2 32 - 1})
  { n ==
    Impl.Noise.PatternMessages.Definitions.pat_message_vsv Impl.Noise.Instances.wg_inc
      Spec.Noise.Instances.pattern_IKpsk2
      12
      0 /\ n > 0 }
Impl.Noise.PatternMessages.Definitions.pat_message_vsv Impl.Noise.Instances.wg_inc Spec.Noise.Instances.pattern_IKpsk2 Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_GreaterThan Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t
let initiation_IKpsk2_len:n: size_nat{n == pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 /\ n > 0} =
  
assert_norm (pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 <= max_size_t);
assert_norm (pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0 > 0);
pat_message_vsv wg_inc Spec.pattern_IKpsk2 12 0