val ds_result : a: Type -> Type
let ds_result (a : Type) = result a ds_error
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 *)
/
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
a: Type -> Type
Spec.Noise.Base.Definitions.result Spec.Noise.API.DState.Definitions.ds_error
let ds_result (a: Type) =
  
result a ds_error