val dstate_is_transport: #dc: dconfig -> dstate dc -> Tot bool
val dstate_is_transport: #dc: dconfig -> dstate dc -> Tot bool
let dstate_is_transport : #dc:dconfig -> dstate dc -> Tot bool =
  fun #sc st -> not (dstate_is_handshake st)
module Spec.Noise.API.DState.Definitions

module State = Spec.Noise.API.State.Definitions
open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base
open Spec.Noise.WellFormedness
open Spec.Noise.SPatterns
open Lib.ByteSequence
open FStar.Mul
open FStar.List.Tot

open Spec.Noise.API.Device

#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"

(*** Errors *)
(* All the errors which can happen *)
type ds_error =
| Incorrect_transition (* Id function called while state did not have proper status *)
| Premessage (* Error while processing the premessages *)
| No_key (* Missing key *)
| Already_key (* Key already received *)
| Rs_rejected_by_policy (* Remote static key rejected by the validation policy *)
| Rs_not_certified (* Remote static key rejected by the payload validation function *)
| Already_peer (* We received a remote static while we already know who the remote peer is *)
| Peer_conflict (* Two peers have the same static key *)
| Unknown_peer_id (* Couldn't find a peer in the device *)
| Input_size (* If the input message doesn't have the proper size *)
| DH_error (* A DH operation failed *)
| Decryption (* An authenticated decryption failed *)
| Saturated_nonce (* Nonce is saturated *)

let ds_result (a : Type) = result a ds_error

(*** Configuration *)

/// We need a way to convert a dconfig to an sconfig
noextract
//[@ (strict_on_arguments [0])]
val dconfig_to_sconfig (dc : dconfig) : State.sconfig


(*** DState *)

(* DState identifier - the dstates all have a unique identifier, like the peers *)

val dstate : dconfig -> Type0

val dstate_get_pattern : #dc:dconfig -> dstate dc -> wfs_handshake_pattern
val dstate_get_status : #dc:dconfig -> dstate dc -> State.status
val dstate_is_initiator : #dc:dconfig -> dstate dc -> Tot bool
/
Spec.Noise.WellFormedness.fsti.checked Spec.Noise.SPatterns.fst.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked Spec.Noise.API.State.Definitions.fsti.checked Spec.Noise.API.Device.fsti.checked prims.fst.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.API.DState.Definitions.fsti
st: Spec.Noise.API.DState.Definitions.dstate dc -> Prims.bool
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.API.DState.Definitions.dstate Prims.op_Negation Spec.Noise.API.DState.Definitions.dstate_is_handshake Prims.bool
let dstate_is_transport: #dc: dconfig -> dstate dc -> Tot bool =
  
fun #sc st -> not (dstate_is_handshake st)