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

type principal=string


type vars = {
  c : principal ;
  w : principal ;
  q : int }
type hashes = {
  hc : bytes ;
  hw : bytes ;
  hq : bytes }
type macs = {
  wCommitqcw : bytes ;
  cAck : bytes ;
  wReveal : 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_Commit of (principal * bytes * int* int * principal * principal)
| Send_Ack of (principal * bytes * int)
| Send_Reveal of (principal * bytes * int)
| Recv_Commit of (principal * bytes * int * principal * principal)
| Recv_Ack of (principal * bytes * int)
| Recv_Reveal of (principal * bytes * int * int)



type wired_w_start =
  | Wired_in_w_start_of_c_qcwCommit_qcw__ of (principal * principal) * store

type wired_c_qcwCommit =
  | Wired_in_c_qcwCommit_of_w_Ack_qcwCommit___ of (unit) * store

type wired_w_Ack_qcwCommit =
  | Wired_in_w_Ack_qcwCommit_of_c_Reveal_qcwAck___ of (int) * store
val receiveWired_w_start: store -> wired_w_start

val receiveWired_c_qcwCommit: store -> wired_c_qcwCommit

val receiveWired_w_Ack_qcwCommit: store -> wired_w_Ack_qcwCommit
 val sendWired_Commit_c_start: int -> principal -> principal ->  store -> store

 val sendWired_Ack_w_qcwCommit:  store -> store

 val sendWired_Reveal_c_Ack_qcwCommit:  store -> store