val s_error_to_ds_error (e: State.s_error) : ds_error
val s_error_to_ds_error (e: State.s_error) : ds_error
let s_error_to_ds_error (e : State.s_error) : ds_error =
  match e with
  | State.Incorrect_transition -> Incorrect_transition
  | State.Premessage -> Premessage
  | State.No_key -> No_key
  | State.Already_key -> Already_key
  | State.Rs_not_valid -> Rs_rejected_by_policy
  | State.Input_size -> Input_size
  | State.DH_error -> DH_error
  | State.Decryption -> Decryption
  | State.Saturated_nonce -> Saturated_nonce
module Spec.Noise.API.DState.Definitions

open Lib.ByteSequence
open FStar.Mul
open FStar.List.Tot

friend Spec.Noise.Base.Definitions
module Base = Spec.Noise.Base.Definitions
module State = Spec.Noise.API.State.Definitions
friend Spec.Noise.API.State.Definitions
friend Spec.Noise.API.Device.Definitions
module M = Spec.Noise.Map
open Spec.Noise.API.MetaInfo

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

(*** API *)
/
Spec.Noise.Map.fst.checked Spec.Noise.Base.Definitions.fst.checked Spec.Noise.API.State.Definitions.fst.checked Spec.Noise.API.State.Definitions.fst.checked Spec.Noise.API.MetaInfo.fst.checked Spec.Noise.API.Device.Definitions.fst.checked prims.fst.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.API.DState.Definitions.fst
e: Spec.Noise.API.State.Definitions.s_error -> Spec.Noise.API.DState.Definitions.ds_error
Spec.Noise.API.State.Definitions.s_error Spec.Noise.API.DState.Definitions.Incorrect_transition Spec.Noise.API.DState.Definitions.Premessage Spec.Noise.API.DState.Definitions.No_key Spec.Noise.API.DState.Definitions.Already_key Spec.Noise.API.DState.Definitions.Rs_rejected_by_policy Spec.Noise.API.DState.Definitions.Input_size Spec.Noise.API.DState.Definitions.DH_error Spec.Noise.API.DState.Definitions.Decryption Spec.Noise.API.DState.Definitions.Saturated_nonce Spec.Noise.API.DState.Definitions.ds_error
let s_error_to_ds_error (e: State.s_error) : ds_error =
  
match e with
| State.Incorrect_transition -> Incorrect_transition
| State.Premessage -> Premessage
| State.No_key -> No_key
| State.Already_key -> Already_key
| State.Rs_not_valid -> Rs_rejected_by_policy
| State.Input_size -> Input_size
| State.DH_error -> DH_error
| State.Decryption -> Decryption
| State.Saturated_nonce -> Saturated_nonce