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

type principal=string


type vars = {
  c : principal ;
  w : principal ;
  q : string ;
  x : int }
type hashes = {
  hc : bytes ;
  hw : bytes ;
  hq : bytes ;
  hx : bytes }
type macs = {
  wRequestcwq : bytes ;
  cReplyx : bytes ;
  wExtraq : bytes ;
  cFault : bytes }
type keys = {
  key_cw : bytes ;
  key_wc : 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_w : principal -> bool -> store

type preds = 
| Send_Request of (principal * bytes * int* principal * principal * string)
| Send_Reply of (principal * bytes * int* int)
| Send_Extra of (principal * bytes * int* string)
| Send_Fault of (principal * bytes * int)
| Recv_Request of (principal * bytes * int * principal * principal * string)
| Recv_Reply of (principal * bytes * int * int)
| Recv_Extra of (principal * bytes * int * string)
| Recv_Fault of (principal * bytes * int)



type wired_w_start =
  | Wired_in_w_start_of_c_cwqRequest_cwq__ of (principal * principal * string) * store

type wired_c_cwqRequest =
  | Wired_in_c_cwqRequest_of_w_Fault_cwqRequest___ of (unit) * store
  | Wired_in_c_cwqRequest_of_w_xReply_cwqRequest_x__ of (int) * store

type wired_w_xReply_cwqRequest =
  | Wired_in_w_xReply_cwqRequest_of_c_qExtra_cwxReply_q__ of (string) * store

type wired_w_xReply_cwqExtra =
  | Wired_in_w_xReply_cwqExtra_of_c_qExtra_cwxReply_q__ of (string) * store

type wired_c_qExtra_cwxReply =
  | Wired_in_c_qExtra_cwxReply_of_w_xReply_cwqExtra_x__ of (int) * store
  | Wired_in_c_qExtra_cwxReply_of_w_Fault_cwxqExtra___ of (unit) * store
val receiveWired_w_start: store -> wired_w_start

val receiveWired_c_cwqRequest: store -> wired_c_cwqRequest

val receiveWired_w_xReply_cwqRequest: store -> wired_w_xReply_cwqRequest

val receiveWired_w_xReply_cwqExtra: store -> wired_w_xReply_cwqExtra

val receiveWired_c_qExtra_cwxReply: store -> wired_c_qExtra_cwxReply
 val sendWired_Request_c_start: principal -> principal -> string ->  store -> store

 val sendWired_Fault_w_cwqRequest:  store -> store

 val sendWired_Reply_w_cwqRequest: int ->  store -> store

 val sendWired_Extra_c_xReply_cwqRequest: string ->  store -> store

 val sendWired_Reply_w_qExtra_cwxReply: int ->  store -> store

 val sendWired_Extra_c_xReply_cwqExtra: string ->  store -> store

 val sendWired_Fault_w_qExtra_cwxReply:  store -> store