(*******************************)
(* Generated Session Interface *)
(*******************************)
open Data

type principal=string


type vars = {
  c : principal ;
  p : principal ;
  w : principal ;
  q : string ;
  x : string ;
  d : string ;
  o : string }
type hashes = {
  hc : bytes ;
  hp : bytes ;
  hw : bytes ;
  hq : bytes ;
  hx : bytes ;
  hd : bytes ;
  ho : bytes }
type macs = {
  pRequestcpwq : bytes ;
  wRequestcpwq : bytes ;
  wAudit : bytes ;
  cResumed : bytes ;
  pDetailsd : bytes ;
  wResume : bytes ;
  cResumeod : bytes ;
  wRetryo : bytes ;
  wForward : bytes ;
  cForward : bytes ;
  cReplyx : bytes }
type keys = {
  key_cp : bytes ;
  key_cw : bytes ;
  key_pc : bytes ;
  key_pw : bytes ;
  key_wc : bytes ;
  key_wp : bytes }
type header = {
  ts : int ;
  sid : bytes }
type store = 
  { vars : vars ; hashes : hashes ; macs : macs ; keys : keys ; header :  header}
val empty_store_c : principal -> bool -> store
val empty_store_p : principal -> bool -> store
val empty_store_w : principal -> bool -> store

type preds = 
| Send_Request of (principal * bytes * int* principal * principal * principal * string)
| Send_Forward of (principal * bytes * int)
| Send_Reply of (principal * bytes * int* string)
| Send_Audit of (principal * bytes * int)
| Send_Details of (principal * bytes * int* string)
| Send_Retry of (principal * bytes * int* string)
| Send_Resume of (principal * bytes * int)
| Recv_Request of (principal * bytes * int * principal * principal * principal * string)
| Recv_Forward of (principal * bytes * int * principal * principal * principal * string)
| Recv_Reply of (principal * bytes * int * string)
| Recv_Audit of (principal * bytes * int * principal * principal * principal)
| Recv_Details of (principal * bytes * int * string)
| Recv_Retry of (principal * bytes * int * string)
| Recv_Resume of (principal * bytes * int * string)



type wired_p_start =
  | Wired_in_p_start_of_c_cpwqRequest_cpwq__ of (principal * principal * principal * string) * store

type wired_p_Audit_cpwqRequest =
  | Wired_in_p_Audit_cpwqRequest_of_w_dDetails_Audit_cpwqRequest_d__ of (string) * store

type wired_w_dDetails_Audit_cpwqRequest =
  | Wired_in_w_dDetails_Audit_cpwqRequest_of_p_Resume_dDetails_cpwqRequest___ of (string) * store
  | Wired_in_w_dDetails_Audit_cpwqRequest_of_p_oRetry_dDetails_cpwqRequest_o__ of (string) * store

type wired_p_oRetry_dDetails_cpwqRequest =
  | Wired_in_p_oRetry_dDetails_cpwqRequest_of_w_dDetails_oRetry_cpwqRequest_d__ of (string) * store

type wired_w_dDetails_oRetry_cpwqRequest =
  | Wired_in_w_dDetails_oRetry_cpwqRequest_of_p_Resume_odDetails_cpwqRequest___ of (string) * store
  | Wired_in_w_dDetails_oRetry_cpwqRequest_of_p_oRetry_dDetails_cpwqRequest_o__ of (string) * store

type wired_w_start =
  | Wired_in_w_start_of_p_Audit_cpwqRequest___c_cpwqRequest_cpwq__ of (principal * principal * principal) * store
  | Wired_in_w_start_of_p_Forward_cpwqRequest___c_cpwqRequest_cpwq__ of (principal * principal * principal * string) * store

type wired_c_cpwqRequest =
  | Wired_in_c_cpwqRequest_of_w_xReply_dResume_cpwqRequest_x__p_Resume_dDetails_cpwqRequest_d__ of (string) * store
  | Wired_in_c_cpwqRequest_of_w_xReply_odResume_cpwqRequest_x__p_Resume_odDetails_cpwqRequest_od__ of (string) * store
  | Wired_in_c_cpwqRequest_of_w_xReply_Forward_cpwqRequest_x__p_Forward_cpwqRequest___ of (string) * store
val receiveWired_p_start: store -> wired_p_start

val receiveWired_p_Audit_cpwqRequest: store -> wired_p_Audit_cpwqRequest

val receiveWired_w_dDetails_Audit_cpwqRequest: store -> wired_w_dDetails_Audit_cpwqRequest

val receiveWired_p_oRetry_dDetails_cpwqRequest: store -> wired_p_oRetry_dDetails_cpwqRequest

val receiveWired_w_dDetails_oRetry_cpwqRequest: store -> wired_w_dDetails_oRetry_cpwqRequest

val receiveWired_w_start: store -> wired_w_start

val receiveWired_c_cpwqRequest: store -> wired_c_cpwqRequest
 val sendWired_Request_c_start: principal -> principal -> principal -> string ->  store -> store

 val sendWired_Audit_p_cpwqRequest:  store -> store

 val sendWired_Details_w_Audit_cpwqRequest: string ->  store -> store

 val sendWired_Resume_p_dDetails_Audit_cpwqRequest:  store -> store

 val sendWired_Reply_w_Resume_dDetails_cpwqRequest: string ->  store -> store

 val sendWired_Retry_p_dDetails_Audit_cpwqRequest: string ->  store -> store

 val sendWired_Details_w_oRetry_dDetails_cpwqRequest: string ->  store -> store

 val sendWired_Resume_p_dDetails_oRetry_cpwqRequest:  store -> store

 val sendWired_Reply_w_Resume_odDetails_cpwqRequest: string ->  store -> store

 val sendWired_Retry_p_dDetails_oRetry_cpwqRequest: string ->  store -> store

 val sendWired_Forward_p_cpwqRequest:  store -> store

 val sendWired_Reply_w_Forward_cpwqRequest: string ->  store -> store