val rcode_is_error (c: rcode) : bool
val rcode_is_error (c: rcode) : bool
let rcode_is_error (c : rcode) : bool = Error? c
/// 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

inline_for_extraction noextract
let pattern = pattern_IKpsk2

[@@ T.postprocess_with (fun () -> T.norm [delta; zeta; iota; primops]; T.trefl())]
let num_pattern_messages = List.Tot.length pattern.messages

let _ : squash(List.Tot.length pattern.messages = num_pattern_messages) =
  normalize_term_spec(List.Tot.length pattern.messages)

inline_for_extraction noextract
let use_serialization = true

[@@ noextract_to "krml"] inline_for_extraction noextract
let idc_ : valid_idc =
  mk_idc inc pattern hstring_smficc (uint_id_cl U32) (uint_id_cl U32)
         (false_stateful_policy_function inc (with_onorm (check_hsk_is_psk pattern)))
         (false_certification_state inc hstring_smficc.St.smficc_stateful)
         use_serialization

[@@ (strict_on_arguments [0]); noextract_to "krml"]
inline_for_extraction noextract
let idc () = idc_ ()

(* Some helpers *)
/
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
c: Impl.Noise.API.Session.rcode -> Prims.bool
Impl.Noise.API.Session.rcode Impl.Noise.API.Session.uu___is_Error Prims.bool
let rcode_is_error (c: rcode) : bool =
  
Error? c