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

type principal=string


type vars = {
  c : principal ;
  w : principal ;
  r : principal ;
  q : int }
type hashes = {
  hc : bytes ;
  hw : bytes ;
  hr : bytes ;
  hq : bytes }
type macs = {
  wCommitqcwr : bytes ;
  rCommitqcwr : bytes ;
  rFwd : bytes }
type keys = {
  key_cw : bytes ;
  key_cr : bytes ;
  key_wc : bytes ;
  key_wr : bytes ;
  key_rc : bytes ;
  key_rw : 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_r : principal -> bool -> store

type preds = 
| Send_Commit of (principal * bytes * int* int * principal * principal * principal)
| Send_Fwd of (principal * bytes * int)
| Recv_Commit of (principal * bytes * int * int * principal * principal * principal)
| Recv_Fwd of (principal * bytes * int * int * principal * principal * principal)



type wired_w_start =
  | Wired_in_w_start_of_c_qcwrCommit_qcwr__ of (int * principal * principal * principal) * store

type wired_r_start =
  | Wired_in_r_start_of_w_Fwd_qcwrCommit___c_qcwrCommit_qcwr__ of (int * principal * principal * principal) * store
val receiveWired_w_start: store -> wired_w_start

val receiveWired_r_start: store -> wired_r_start
 val sendWired_Commit_c_start: int -> principal -> principal -> principal ->  store -> store

 val sendWired_Fwd_w_qcwrCommit:  store -> store