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

type principal=string


type vars = {
  c : principal ;
  w : principal ;
  p : principal ;
  d : principal ;
  q : string ;
  r : int }
type hashes = {
  hc : bytes ;
  hw : bytes ;
  hp : bytes ;
  hd : bytes ;
  hq : bytes ;
  hr : bytes }
type macs = {
  pLogincpdq : bytes ;
  dLogincpdq : bytes ;
  dReject : bytes ;
  cReject : bytes ;
  cBasicreplyr : bytes ;
  cRedirectw : bytes ;
  wRedirectcpdw : bytes ;
  wRequestq : bytes ;
  cReplyr : bytes ;
  wExtraq : bytes ;
  cFault : bytes }
type keys = {
  key_cw : bytes ;
  key_cp : bytes ;
  key_cd : bytes ;
  key_wc : bytes ;
  key_wp : bytes ;
  key_wd : bytes ;
  key_pc : bytes ;
  key_pw : bytes ;
  key_pd : bytes ;
  key_dc : bytes ;
  key_dw : bytes ;
  key_dp : 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
val empty_store_p : principal -> bool -> store
val empty_store_d : principal -> bool -> store

type preds = 
| Send_Login of (principal * bytes * int* principal * principal * principal * string)
| Send_Redirect of (principal * bytes * int* principal)
| Send_Request of (principal * bytes * int* string)
| Send_Reply of (principal * bytes * int* int)
| Send_Extra of (principal * bytes * int* string)
| Send_Fault of (principal * bytes * int)
| Send_Reject of (principal * bytes * int)
| Send_Basicreply of (principal * bytes * int* int)
| Recv_Login of (principal * bytes * int * principal * principal * principal * string)
| Recv_Redirect of (principal * bytes * int * principal)
| Recv_Request of (principal * bytes * int * principal * principal * principal * string)
| Recv_Reply of (principal * bytes * int * int)
| Recv_Extra of (principal * bytes * int * string)
| Recv_Fault of (principal * bytes * int)
| Recv_Reject of (principal * bytes * int * principal * principal * principal)
| Recv_Basicreply of (principal * bytes * int * int)



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

type wired_d_start =
  | Wired_in_d_start_of_p_Reject_cpdqLogin___c_cpdqLogin_cpdq__ of (principal * principal * principal) * store

type wired_c_cpdqLogin =
  | Wired_in_c_cpdqLogin_of_d_rBasicreply_Reject_cpdqLogin_r__p_Reject_cpdqLogin___ of (int) * store
  | Wired_in_c_cpdqLogin_of_p_wRedirect_cpdqLogin_w__ of (principal) * store

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

type wired_c_qRequest_cpdwRedirect =
  | Wired_in_c_qRequest_cpdwRedirect_of_w_Fault_qRequest_cpdwRedirect___ of (unit) * store
  | Wired_in_c_qRequest_cpdwRedirect_of_w_rReply_qRequest_cpdwRedirect_r__ of (int) * store

type wired_w_rReply_qRequest_cpdwRedirect =
  | Wired_in_w_rReply_qRequest_cpdwRedirect_of_c_qExtra_rReply_cpdwRedirect_q__ of (string) * store

type wired_w_rReply_qExtra_cpdwRedirect =
  | Wired_in_w_rReply_qExtra_cpdwRedirect_of_c_qExtra_rReply_cpdwRedirect_q__ of (string) * store

type wired_c_qExtra_rReply_cpdwRedirect =
  | Wired_in_c_qExtra_rReply_cpdwRedirect_of_w_rReply_qExtra_cpdwRedirect_r__ of (int) * store
  | Wired_in_c_qExtra_rReply_cpdwRedirect_of_w_Fault_rqExtra_cpdwRedirect___ of (unit) * store
val receiveWired_p_start: store -> wired_p_start

val receiveWired_d_start: store -> wired_d_start

val receiveWired_c_cpdqLogin: store -> wired_c_cpdqLogin

val receiveWired_w_start: store -> wired_w_start

val receiveWired_c_qRequest_cpdwRedirect: store -> wired_c_qRequest_cpdwRedirect

val receiveWired_w_rReply_qRequest_cpdwRedirect: store -> wired_w_rReply_qRequest_cpdwRedirect

val receiveWired_w_rReply_qExtra_cpdwRedirect: store -> wired_w_rReply_qExtra_cpdwRedirect

val receiveWired_c_qExtra_rReply_cpdwRedirect: store -> wired_c_qExtra_rReply_cpdwRedirect
 val sendWired_Login_c_start: principal -> principal -> principal -> string ->  store -> store

 val sendWired_Reject_p_cpdqLogin:  store -> store

 val sendWired_Basicreply_d_Reject_cpdqLogin: int ->  store -> store

 val sendWired_Redirect_p_cpdqLogin: principal ->  store -> store

 val sendWired_Request_c_wRedirect_cpdqLogin: string ->  store -> store

 val sendWired_Fault_w_qRequest_cpdwRedirect:  store -> store

 val sendWired_Reply_w_qRequest_cpdwRedirect: int ->  store -> store

 val sendWired_Extra_c_rReply_qRequest_cpdwRedirect: string ->  store -> store

 val sendWired_Reply_w_qExtra_rReply_cpdwRedirect: int ->  store -> store

 val sendWired_Extra_c_rReply_qExtra_cpdwRedirect: string ->  store -> store

 val sendWired_Fault_w_qExtra_rReply_cpdwRedirect:  store -> store