/* BYZANTINE AGREEMENT PROTOCOL */
/* this files contains the proof of agreement */
/* gxn 7/12/2001 */

/* replaced the probabilistic choice of the coins by a non-deterministic choice */
/* and suppose that the coin in round $r$ is flipped when at least $n-2t$ honest parties have read the main votes in round $r$ */
/* note that the coin can never be tossed earlier than this since $n-t$ shares are required before it can be revealed */
/* note that we have change the notations for the coins: for round r the coin is denoted \smvusersym{coin}$[r+1]$ */
/* this is to simplify the code: it allows the pre-votes for each round to be based on the coin for the previous round */
/* by setting the coin for round -1 (\smvusersym{coin}$[0]$) always to 0 */

/* instead of parties reading votes individually, we store the total number of honest votes for each preference  */
/* and for corrupted parties we include only boolean variables indicating what corrupted parties can vote for */
/* recalling that different parties may see corrupted parties vote for different values */
/* based on these totals we then know what combination of votes each party can read */
/* that is what the adversary can make parties vote for */
/* note that sometimes there will be a non-deterministic choice as to what a party will vote for */
/* this is a choice of the adversary since it depends on which votes a party reads */

/* an honest party must get at least $n-2t$ votes from other honest parties */
/* and the remaining votes can come from either honest or corrupted parties */
/* if we can show: ``if an honest party has a vote for a value then corrupted parties can also vote for this value'' */
/* we need only count up to $n-2t$ honest party votes and use corrupted parties for the remaining votes */
/* this has been proved (properties corrupted3 and corrupted4 in lemmas.smv) */

/* note that to deal with the validity part of the proof and to keep things consistent the initial round is 0 instead of 1 */
/* this is because the round variable is an ordset and cannot specify round=1, but we can specify round=0 */

/* one further change is that we let the pre-votes be cast before they are cast in the actual protocol */
/* now they are cast when a party reads the main-votes of the previous round */
/* note that this can only give the adversary more power */
/* however, in the original protocol at the time when the pre-votes are now cast */
/* an honest party has read the main-votes it will use to cast a pre-vote */
/* therefore at this time the adversary already knows what pre-vote the party is going make */
/* and hence moving the casting of pre-votes to this point makes no difference to what the adversary knows */
/* there is one added complication: we need to store two different possible pre-votes which depend on */
/* what value of the corresponding coin becomes when it is tossed */

/*-----------------------------------------------------------------------------------*/

/* CONSTANTS (n=10 & t=3) */
#define N 7 /* number of  honest parties */
#define M 4 /* M=n-2t number of honest pre and main votes that must be read */ 
#define K 4 /* K=2t+1-t=t+1 number of honest pre processing votes that must be read */ 

/* ABSTRACT DATA TYPES */
ordset PROC 1..N; /* set of parties  */
ordset VOTES 0..M; /* honest pre and main votes */
ordset PRE_PROC_VOTES 0..K; /* honest preprocessing votes */
ordset ROUNDS 0..; /* round numbers  */


/* DATA TYPES */
typedef PC {INITIAL , PRE_PROCESSING  , MAIN , DECIDE , COIN , DONE  }; 
/* INITIAL - make preprocessing vote (initial state)  */
/* PRE_PROCESSING - read preprocessing votes and make initial pre-vote  */
/* MAIN - read pre-votes and make main vote */
/* DECIDE - read main votes and make choice whether to decide or not and next pre-vote */
/* COIN - generate share of the coin */
/* DONE - finished */

/*-----------------------------------------------------------------------------------*/

module main(act){
		
	/*------------------------------INPUTS------------------------------------------*/

	act : PROC; /* SCHEDULER left unspecified */

	/* in certain cases a party can cast different votes depending on which votes it reads */
	/* we represent these choices using the following variables */
	/* note since this is decided by the adversary we leave these variables unspecified */
	/* pre votes */
	nd_pre  : 0..1;  /* non deterministic choice between voting for 0 and 1 */
	nd_pre1 : {0,2}; /* non deterministic choice between voting for 0 and coin */
	nd_pre2 : 1..2;  /* non deterministic choice between voting for 1 and coin */
	/* main votes */
	nd_main1 : {0,2}; /* non deterministic choice between voting for 0 and 2 */
	nd_main2 : 1..2;  /* non deterministic choice between voting for 1 and 2 */
	
	start : array PROC of 0..1; /* initial values of parties left unspecified */

	/* -------------------THE PROTOCOL FOR HONEST PARTIES---------------------------- */

	/* PHASE */
	pc : array PROC of PC; /* pc[i] - phase of party i */

	/* VALUES OF VOTES */
	/* pre-processing-votes: 0 or 1 */
	/* pre-votes: 0 or 1 */
	/* main-votes: 0, 1 or 2 where 2 denotes abstain */
	
	/* PRE_PROCESSING */
	pre_proc : PRE_PROC_VOTES; /* pre_proc - number of pre processing votes  */
	pre_proc_votes : array 0..1 of PRE_PROC_VOTES; /* pre_proc_votes[v] - number of pre processing votes for v  */	

	/* PRE_VOTE */
	pre : array ROUNDS of VOTES; /* pre[r] - number of pre-votes in round r */	
	pre_votes : array ROUNDS of array 0..1 of array 0..1 of VOTES; /* pre_votes[r][c][v] - number of pre-votes for v in round r if the coin in round r equals c */	

	/* MAIN_VOTE */
	main : array ROUNDS of VOTES; /* main[r] - number of main-votes so far in round r */	
	main_votes : array ROUNDS of array 0..2 of VOTES; /* main_votes[r][v] - number of main-votes so far for v in round r */	

	/* ROUND */
	round : array PROC of ROUNDS; /* round[i] - round party i is currently in */

	/* DECIDING */
	decide : array ROUNDS of array PROC of boolean; /* decide[r][i] party i decided in round r  */
	decide_value : array ROUNDS of array PROC of 0..1;	/* decide[r][i][v]=v what value party i decided on in round r (if the party decides)  */

	/* COIN */
	coin : array ROUNDS of { not_tossed , 0 , 1 }; /* coin[r] value of the coin in round r */

	/* INITIAL VALUES */
	forall (i in PROC) {
		init(pc[i]) := INITIAL; 
		init(round[i]) := 0;
	}
	/* set all totals to be zero  */
	init(pre_proc) := 0;
	for(v = 0; v <= 1; v = v + 1) init(pre_proc_votes[v]) := 0;
	forall(r in ROUNDS){
		init(pre[r]) := 0;
		init(main[r]) := 0;
		for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) init(pre_votes[r][c][v]) := 0;
		for(v = 0; v <= 2; v = v + 1) init(main_votes[r][v]) := 0; 
	}
	/* initially undecided */
	forall(r in ROUNDS) forall(i in PROC) init(decide[r][i]) := 0;

	/* as explained the coin in round 0 is set to 0 then never changed */
	/* the remaining coins initially are not tossed */	
	forall(r in ROUNDS) init(coin[r]) := (r=0) ? 0 : not_tossed;

	/* NEXT VALUES */		
	switch (pc[act]) {				
		INITIAL : {
			/* move to pre processing */
			next(pc[act]) := PRE_PROCESSING;
			/* make pre processing vote based on the value of start[act] */
			next(pre_proc_votes[start[act]]) := (pre_proc_votes[start[act]])=K ? pre_proc_votes[start[act]] : pre_proc_votes[start[act]]+1;
			/* record that a pre processing vote has been cast */
			next(pre_proc) := pre_proc=K ?  pre_proc : pre_proc+1;
		}
		PRE_PROCESSING : { 
			if (pre_proc=K) { /* sufficient pre processing votes */
				/* move to MAIN */
				next(pc[act]) := MAIN;
				/* record that a pre vote has been cast */
				next(pre[round[act]]) := pre[round[act]]=M ?  pre[round[act]] : pre[round[act]]+1; 
				for(c = 0; c <= 1; c = c + 1) {
					/* sufficient votes to have a pre vote for either value therefore the vote is the adversary's choice */
					if (pre_proc_votes[0]>0 & pre_proc_votes[1]>0)
						next(pre_votes[round[act]][c][nd_pre]) := pre_votes[round[act]][c][nd_pre]=M ? pre_votes[round[act]][c][nd_pre] : pre_votes[round[act]][c][nd_pre]+1;
					/* pre vote for 0 only  */
					else if (pre_proc_votes[0]>0) 
						next(pre_votes[round[act]][c][0]) := pre_votes[round[act]][c][0]=M ? pre_votes[round[act]][c][0] : pre_votes[round[act]][c][0]+1;
					/* pre vote for 1 only  */
					else if (pre_proc_votes[1]>0) 
						next(pre_votes[round[act]][c][1]) := pre_votes[round[act]][c][1]=M ? pre_votes[round[act]][c][1] : pre_votes[round[act]][c][1]+1;
					/* the above should be the only cases but as a default suppose the adversary can choose */
					else 
						next(pre_votes[round[act]][c][nd_pre]) := pre_votes[round[act]][c][nd_pre]=M ? pre_votes[round[act]][c][nd_pre] : pre_votes[round[act]][c][nd_pre]+1;
				}
			}
		}
		MAIN : {
			/* read pre votes and cast main vote */
			/* to simplify the conditions have used the assumptions that there cannot be M votes for two distinct values in the same round */
			if ( pre[round[act]]=M & !coin[round[act]]=not_tossed ) { /* sufficient pre votes and  the coin has been tossed */
				/* move DECIDE */
				next(pc[act]) := DECIDE;
				/* record that the party has made a main vote */
				next(main[round[act]]) := main[round[act]]=M ? main[round[act]] : main[round[act]]+1;
				/* main vote for 0 or abstain only */
				if (pre_votes[round[act]][coin[round[act]]][0]=M & corrupted_pre[round[act]][coin[round[act]]][0] & (pre_votes[round[act]][coin[round[act]]][1]>0 | corrupted_pre[round[act]][coin[round[act]]][1]) )
					next(main_votes[round[act]][nd_main1]) := main_votes[round[act]][nd_main1]=M ? main_votes[round[act]][nd_main1] : main_votes[round[act]][nd_main1]+1;
				/* main vote for 1 or abstain only */
				else if (pre_votes[round[act]][coin[round[act]]][1]=M & corrupted_pre[round[act]][coin[round[act]]][1] & (pre_votes[round[act]][coin[round[act]]][0]>0 | corrupted_pre[round[act]][coin[round[act]]][0]) )
					next(main_votes[round[act]][nd_main2]) := main_votes[round[act]][nd_main2]=M ? main_votes[round[act]][nd_main2] : main_votes[round[act]][nd_main2]+1;
				/* main vote for 0 only */
				else if (pre_votes[round[act]][coin[round[act]]][0]=M & corrupted_pre[round[act]][coin[round[act]]][0])
					next(main_votes[round[act]][0]) := main_votes[round[act]][0]=M ? main_votes[round[act]][0] : main_votes[round[act]][0]+1;
				/* main vote for 1 only  */
				else if (pre_votes[round[act]][coin[round[act]]][1]=M & corrupted_pre[round[act]][coin[round[act]]][1])
					next(main_votes[round[act]][1]) := main_votes[round[act]][1]=M ? main_votes[round[act]][1] : main_votes[round[act]][1]+1;
				/* left with only a main vote for abstain */
				else
					next(main_votes[round[act]][2]) := main_votes[round[act]][2]=M ? main_votes[round[act]][2] : main_votes[round[act]][2]+1;
			}
		
		}
		DECIDE : {
			/* to simplify the model we allow decide_value to be set without decide being set to true in the case the value of decide_value does not matter */
			/* and again use the assumptions that there cannot be M votes for two distinct values in the same round */
			if (main[round[act]]=M) { /* sufficient main votes */
				next(pc[act]) := COIN; 
				/* record that a pre vote has been cast */
			    next(pre[round[act]+1]) := pre[round[act]+1]=M ?  pre[round[act]+1] : pre[round[act]+1]+1;
				/* must decide on 0 and cast a pre-vote for 0 */
				if (main_votes[round[act]][0]=M & corrupted_main[round[act]][0] & main_votes[round[act]][2]=0 & !corrupted_main[round[act]][2] & main_votes[round[act]][1]=0 & !corrupted_main[round[act]][1] ) {
					next(decide[round[act]][act]) := 1;
					next(decide_value[round[act]][act]) := 0;
					for(c = 0; c <= 1; c = c + 1) 
						next(pre_votes[round[act]+1][c][0]) := pre_votes[round[act]+1][c][0]=M ?  pre_votes[round[act]+1][c][0] : pre_votes[round[act]+1][c][0]+1;
				}
				/* must decide on 1 and cast a pre-vote for 1 */
				else if (main_votes[round[act]][1]=M & corrupted_main[round[act]][1] & main_votes[round[act]][2]=0 & !corrupted_main[round[act]][2] & main_votes[round[act]][0]=0 & !corrupted_main[round[act]][0] ) {
					next(decide[round[act]][act]) := 1;
					next(decide_value[round[act]][act]) := 1;
					for(c = 0; c <= 1; c = c + 1)					
						next(pre_votes[round[act]+1][c][1]) := pre_votes[round[act]+1][c][1]=M ?  pre_votes[round[act]+1][c][1] : pre_votes[round[act]+1][c][1]+1;
				}
				/* may decide on 0 and must cast a pre-vote for 0 */
				else if (main_votes[round[act]][0]=M & corrupted_main[round[act]][0] & main_votes[round[act]][1]=0 & !corrupted_main[round[act]][1] ) {
					next(decide[round[act]][act]) := {0,1};
					next(decide_value[round[act]][act]) := 0;
					for(c = 0; c <= 1; c = c + 1)
						next(pre_votes[round[act]+1][c][0]) := pre_votes[round[act]+1][c][0]=M ?  pre_votes[round[act]+1][c][0] : pre_votes[round[act]+1][c][0]+1;
				}
				/* may decide on 1 and must cast a pre-vote for 1 */
				else if (main_votes[round[act]][1]=M & corrupted_main[round[act]][1] & main_votes[round[act]][0]=0 & !corrupted_main[round[act]][0] ) {
					next(decide[round[act]][act]) := {0,1};
					next(decide_value[round[act]][act]) := 1;
					for(c = 0; c <= 1; c = c + 1)					
						next(pre_votes[round[act]+1][c][1]) := pre_votes[round[act]+1][c][1]=M ?  pre_votes[round[act]+1][c][1] : pre_votes[round[act]+1][c][1]+1;
				}
				/* cannot decide and must cast a pre-vote for 0 */
				else if ( (main_votes[round[act]][0]>0 | corrupted_main[round[act]][0]) & (main_votes[round[act]][2]<M | !corrupted_main[round[act]][2]) & main_votes[round[act]][1]=0 & !corrupted_main[round[act]][1] ) {
					for(c = 0; c <= 1; c = c + 1)
						next(pre_votes[round[act]+1][c][0]) := pre_votes[round[act]+1][c][0]=M ?  pre_votes[round[act]+1][c][0] : pre_votes[round[act]+1][c][0]+1;
				}
				/* cannot decide and must cast a pre-vote for 1 */
				else if ( (main_votes[round[act]][1]>0 | corrupted_main[round[act]][1]) & (main_votes[round[act]][2]<M | !corrupted_main[round[act]][2]) & main_votes[round[act]][0]=0 & !corrupted_main[round[act]][0] ) {
					for(c = 0; c <= 1; c = c + 1)					
						next(pre_votes[round[act]+1][c][1]) := pre_votes[round[act]+1][c][1]=M ?  pre_votes[round[act]+1][c][1] : pre_votes[round[act]+1][c][1]+1;
				}
				/* may vote for 0 or coin (cannot decide) */
				else if ( (main_votes[round[act]][0]>0 | corrupted_main[round[act]][0]) & (main_votes[round[act]][2]>0 | corrupted_main[round[act]][2]) & main_votes[round[act]][1]=0 & !corrupted_main[round[act]][1] ) {
					if (nd_pre1=0) { /* concrete vote for 0 */
						for(c = 0; c <= 1; c = c + 1)
							next(pre_votes[round[act]+1][c][0]) := pre_votes[round[act]+1][c][0]=M ?  pre_votes[round[act]+1][c][0] : pre_votes[round[act]+1][c][0]+1;
					}
					else { /* coin */
					for(c = 0; c <= 1; c = c + 1)					
						next(pre_votes[round[act]+1][c][c]) := pre_votes[round[act]+1][c][c]=M ?  pre_votes[round[act]+1][c][c] : pre_votes[round[act]+1][c][c]+1;
					}
				}
				/* may vote for 1 or coin (cannot decide) */
				else if ( (main_votes[round[act]][1]>0 | corrupted_main[round[act]][1]) & (main_votes[round[act]][2]>0 | corrupted_main[round[act]][2]) & main_votes[round[act]][0]=0 & !corrupted_main[round[act]][0] ) {
					if (nd_pre2=1) { /* concrete vote for 1 */
						for(c = 0; c <= 1; c = c + 1)					
							next(pre_votes[round[act]+1][c][1]) := pre_votes[round[act]+1][c][1]=M ?  pre_votes[round[act]+1][c][1] : pre_votes[round[act]+1][c][1]+1;
					}
					else { /* coin */
						for(c = 0; c <= 1; c = c + 1)					
							next(pre_votes[round[act]+1][c][c]) := pre_votes[round[act]+1][c][c]=M ?  pre_votes[round[act]+1][c][c] : pre_votes[round[act]+1][c][c]+1;
					}
				}
				else {
				/* left with a vote for coin  (cannot decide) */
					for(c = 0; c <= 1; c = c + 1)					
						next(pre_votes[round[act]+1][c][c]) := pre_votes[round[act]+1][c][c]=M ?  pre_votes[round[act]+1][c][c] : pre_votes[round[act]+1][c][c]+1;
				}
			}
		}					   
		COIN : {
			/* if decided in previous round then done else continue */
			next(pc[act]) := (round[act]>0 & decide[round[act]-1][act]) ? DONE : MAIN;
			next(round[act]) := (round[act]>0 & decide[round[act]-1][act]) ? round[act] : round[act]+1; /* increase round */
			/* toss coin if at least M honest parties have reached this stage and the coin has not been tossed */
			next(coin[round[act]+1]) := pre[round[act]+1]=M & coin[round[act]+1]=not_tossed  ? {0,1} : coin[round[act]+1];
		}
			
	}

	/* -------------------------CORRUPTED PARTIES------------------------------------------ */

	/* corrupted_pre[v] is true if a corrupted party can have a pre vote for v in round r */
	corrupted_pre : array ROUNDS of array 0..1 of array 0..1 of boolean;
	/* corrupted_main[v] is true if a corrupted party can have a main vote for v in round r */
	corrupted_main : array ROUNDS of array 0..2 of boolean;

	/* INITIAL VALUES */
	/* initially cannot vote for either */
	forall(r in ROUNDS){
		for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) init(corrupted_pre[r][c][v]) := 0;
		for(v = 0; v <= 2; v = v + 1) init(corrupted_main[r][v]) := 0;
	}
	/* NEXT VALUES */
	/* pre votes: for round 0 need at least one preprocessing vote from an honest party for a value to vote for that value */ 
	/* in general to vote v either need a main vote for v (from either an honest or corrupted party) in the previous round */
	/* or is able to vote for the coin, that is, there are need sufficient abstain main votes in the previous round */
	forall (r in ROUNDS) {
		if (r=0) {
			for(v = 0; v <= 1; v = v + 1) next(corrupted_pre[r][0][v]) := (next(pre_proc_votes[v])>0);
			for(v = 0; v <= 1; v = v + 1) next(corrupted_pre[r][1][v]) := (next(pre_proc_votes[v])>0);
		}
		else {
			next(corrupted_pre[r][0][0]) := (next(main[r-1])=M & ( (next(main_votes[r-1][0])>0 | next(corrupted_main[r-1][0])) | (next(main_votes[r-1][2])=M & next(corrupted_main[r-1][2])) )) ? 1 : 0;
			next(corrupted_pre[r][0][1]) := (next(main[r-1])=M & (next(main_votes[r-1][1])>0 | next(corrupted_main[r-1][1]))) ? 1 : 0;
			next(corrupted_pre[r][1][0]) := (next(main[r-1])=M & (next(main_votes[r-1][0])>0 | next(corrupted_main[r-1][0]))) ? 1 : 0;
			next(corrupted_pre[r][1][1]) := (next(main[r-1])=M & ( (next(main_votes[r-1][1])>0 | next(corrupted_main[r-1][1])) | (next(main_votes[r-1][2])=M & next(corrupted_main[r-1][2])) )) ? 1 : 0;
		}
	}
	/* main votes: to vote for v (0 or 1) need M pre votes for v from honest parties also pre votes for v from corrupted parties */
	/* to vote for abstain need a pre vote for 0 and a pre vote for 1 (from either honest or corrupted parties) */
	forall (r in ROUNDS) {
		if (next(coin[r])=0) {
			for(v = 0; v <= 1; v = v + 1) next(corrupted_main[r][v]) := (next(pre[r])=M & next(pre_votes[r][0][v])=M & next(corrupted_pre[r][0][v]) ) ? 1 : 0;
			next(corrupted_main[r][2]) := ( next(pre[r])=M & (next(pre_votes[r][0][0])>0 | next(corrupted_pre[r][0][0])) & (next(pre_votes[r][0][1])>0 | next(corrupted_pre[r][0][1])) ) ? 1 : 0;
		}
		else if (next(coin[r])=1) {
			for(v = 0; v <= 1; v = v + 1) next(corrupted_main[r][v]) := (next(pre[r])=M & next(pre_votes[r][1][v])=M & next(corrupted_pre[r][1][v]) ) ? 1 : 0;
			next(corrupted_main[r][2]) := ( next(pre[r])=M & (next(pre_votes[r][1][0])>0 | next(corrupted_pre[r][1][0])) & (next(pre_votes[r][1][1])>0 | next(corrupted_pre[r][1][1])) ) ? 1 : 0;
		}
	}

	/* -----------------------END OF PROTOCOL----------------------------------- */

/*-------------------------------HISTORY VARIABLES---------------------------------------*/
		
	/* for each round records the first party to have a main-vote for each value */
	history_main_votes : array ROUNDS of array 0..2 of PROC;
	forall (r in ROUNDS) for(v = 0; v <= 2; v = v + 1) {
		init(history_main_votes[r][v]) := act;
		next(history_main_votes[r][v]) := next(main_votes[r][v])>0 & main_votes[r][v]=0 ? act : history_main_votes[r][v];
	}
	/* for each round records the first party to have a pre-vote for each value */
	history_pre_votes : array ROUNDS of array 0..1 of array 0..1 of PROC;
	forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) {
		init(history_pre_votes[r][c][v]) := act;
		next(history_pre_votes[r][c][v]) := next(pre_votes[r][c][v])>0 & pre_votes[r][c][v]=0 ? act : history_pre_votes[r][c][v];
	}
	/* for each round records the first party to have a pre-vote */
	history_pre : array ROUNDS of PROC;
	forall (r in ROUNDS) {
		init(history_pre[r]) := act;
		next(history_pre[r]) := next(pre[r])>0 & pre[r]=0 ? act : history_pre[r];
	}
	/* records the first party to have a pre-processing-vote for each value */
	history_pre_proc_votes : array 0..1 of PROC;
	for(v = 0; v <= 1; v = v + 1) {
		init(history_pre_proc_votes[v]) := act;
		next(history_pre_proc_votes[v]) := next(pre_proc_votes[v])>0 & pre_proc_votes[v]=0 ? act : history_pre_proc_votes[v];
	}
	/* records the party which flips the coin */
	history_coin : array ROUNDS of PROC;
	forall (r in ROUNDS) {
		init(history_coin[r]) := act;
		next(history_coin[r]) := !next(coin[r])=not_tossed & coin[r]=not_tossed ? act : history_coin[r];
	}

	/*---------------------------ASSUMPTIONS-------------------------------------*/

	/* 1-4: there cannot be M votes for v and M votes for v'  */
	/* these follows from the fact if this was not true there would be */
	/* M+M=(N-2T) + (N-2T)=N-T+(N-3T)>N-T honest parties */
	/* which is a contradiction since there are only N-T honest parties */
	forall (r in ROUNDS) {
		assumption1[r] : assert G !( main_votes[r][2]=M & main_votes[r][0]=M);
		assumption2[r] : assert G !( main_votes[r][2]=M & main_votes[r][1]=M);
		assumption3[r] : assert G !( main_votes[r][0]=M & main_votes[r][1]=M);
		assume assumption1[r], assumption2[r], assumption3[r];
	} 	
	forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) {
		assumption4[r][c] : assert G !( pre_votes[r][c][0]=M & pre_votes[r][c][1]=M);
		assume assumption4[r][c];
	} 	


	/*------------------ADDITIONAL INVARIANTS-----------------------------------*/

	/* these are proved in a separate file (lemmas.smv) */
	
	forall (r in ROUNDS) forall (n in VOTES) {
		lemma5[r][n] : assert G ( pre[r]=n -> G (pre[r]>=n) );
		assume lemma5[r][n];
	}
	forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) forall (n in VOTES) {
		lemma9[r][c][v][n] : assert G ( pre_votes[r][c][v]>=n -> G (pre_votes[r][c][v]>=n) );
		assume lemma9[r][c][v][n];
	}
	forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) for(v = 0; v <= 1; v = v + 1) {
		lemma11[r][c][v] : assert G (pre_votes[r][c][v]>0 -> G (pre_votes[r][c][v]>0) );
		assume lemma11[r][c][v];
	}
	forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) {
		lemma16[r][c] : assert G ( pre_votes[r][c][1]=0 -> pre_votes[r][c][0]=pre[r] );
		assume lemma16[r][c];
	}
	forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) {
		lemma17[r][c] : assert G ( pre_votes[r][c][0]=0 -> pre_votes[r][c][1]=pre[r] );
		assume lemma17[r][c];
	}
	forall (r in ROUNDS) forall (n in VOTES) {
		lemma19[r][n] : assert G ( main[r]>=n -> G (main[r]>=n)  );
		assume lemma19[r][n];
	}
	forall (r in ROUNDS) for(v = 0; v <= 2; v = v + 1) forall (n in VOTES) {
		lemma23[r][v][n] : assert G ( main_votes[r][v]>=n -> G (main_votes[r][v]>=n) );
		assume lemma23[r][v][n];
	}
	forall (r in ROUNDS) for(v = 0; v <= 2; v = v + 1) {
		lemma25[r][v] : assert G ( main_votes[r][v]>0 -> G (main_votes[r][v]>0) );
		assume lemma25[r][v];
	}
	forall (r in ROUNDS) {
		lemma31[r] : assert G ( (main_votes[r][1]=0 & main_votes[r][2]=0) -> main_votes[r][0]=main[r] );
		assume lemma31[r];
	}
	forall (r in ROUNDS) {
		lemma32[r] : assert G ( (main_votes[r][0]=0 & main_votes[r][2]=0) -> main_votes[r][1]=main[r] );
		assume lemma32[r];
	}
	forall (r in ROUNDS) {
		lemma33[r] : assert G ( (main_votes[r][0]=0 & main_votes[r][1]=0) -> main_votes[r][2]=main[r] );
		assume lemma33[r];
	}
	forall (r in ROUNDS) forall (i in PROC)  {
		lemma37[r][i] : assert G ( decide[r][i] -> G (decide[r][i]) );
		assume lemma37[r][i];
	}
	forall (r in ROUNDS) for (v = 0; v <= 2; v = v + 1) {
		corrupted1[r][v] : assert G ( corrupted_main[r][v] -> G (corrupted_main[r][v]) );
		assume corrupted1[r][v];		
	}
	forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) for (v = 0; v <= 1; v = v + 1) {
		corrupted2[r][c][v] : assert G ( corrupted_pre[r][c][v] -> G (corrupted_pre[r][c][v]) );
		assume corrupted2[r][c][v];
	}
	forall (r in ROUNDS) for (v = 0; v <= 2; v = v + 1) {
		corrupted5[r][v] : assert G ( main_votes[r][v]>0 -> corrupted_main[r][v] );
		assume corrupted5[r][v];
	}
	forall (r in ROUNDS) for (c = 0; c <= 1; c = c + 1) for (v = 0; v <= 1; v = v + 1) {
		corrupted6[r][c][v] : assert G ( pre_votes[r][c][v]>0 -> corrupted_pre[r][c][v] );
		assume corrupted6[r][c][v];
	}
	forall (r in ROUNDS) for(c = 0; c <= 1; c = c + 1) {
		coin2[r][c] : assert G ( coin[r]=c  -> G ( coin[r]=c ) );
			assume coin2[r][c];
	}
	forall (r in ROUNDS) {
		lemma40[r] : assert G ( (main_votes[r][0]>0 | corrupted_main[r][0]) -> ( main_votes[r][1]=0 & !corrupted_main[r][1] ) );
		assume lemma40[r];
	}
	forall (r in ROUNDS) {
		lemma41[r] : assert G ( (main_votes[r][1]>0 | corrupted_main[r][1]) -> ( main_votes[r][0]=0 & !corrupted_main[r][0] ) );
		assume lemma41[r];
	}

	/*------------------------SUBLEMMAS FOR AGREEMENT----------------------------------*/

	/* if a party decides on v then there are no main votes for !v and less than M for abstain  */
	forall (i in PROC) forall (r in ROUNDS) for(v = 0; v <= 1; v = v + 1) {
		inv1[i][r][v] : assert G ( (decide[r][i] & decide_value[r][i]=v) -> (main_votes[r][v]=M & main_votes[r][v+1 mod 2]=0 & !corrupted_main[r][v+1 mod 2] & main_votes[r][2]<M) );
		using lemma40[r],
			lemma41[r],
			lemma23[r][v][M],
			corrupted1[r],
			/* assumptions */
			assumption1[r],
			assumption2[r],
			/* abstractions */
			VOTES->{0,M},
			/* free variables */
			corrupted_main//free,
			corrupted_main[r][v+1 mod 2],
			corrupted_pre//free,
			main//free,
			main_votes//free,
			main_votes[r][v],
			pre//free,
			pre_votes//free,
			pre_proc//free,
			pre_proc_votes//free
			prove inv1[i][r][v];
	}
	/* if a party decides on v then no party has a pre_vote for !v in the next round  */
	forall (i in PROC) forall (r in ROUNDS) for(v = 0; v <= 1; v = v + 1) for (c = 0; c <= 1; c = c + 1){
		inv2[i][r][v][c] : assert G ( (decide[r][i] & decide_value[r][i]=v) -> ( pre_votes[r+1][c][v+1 mod 2]=0 & !corrupted_pre[r+1][c][v+1 mod 2] ) );
		forall (j in PROC) {
			subcase inv2[i][r][v][c][j] of inv2[i][r][v][c] for j=history_pre_votes[r+1][c][v+1 mod 2];
			using inv1[i][r][v],
				lemma19[r][M],
				lemma23[r][0][M],
				lemma23[r][1][M],
				lemma23[r][2][M],
				lemma25[r][v+1 mod 2],
				lemma25[r][2],
				lemma31[r], 
				lemma32[r], 
				lemma33[r],
				corrupted1[r],
				/* abstractions */
				VOTES->{0,M},
				ROUNDS->{0,r,r+1},
				/* free variables */
				coin//free,
				corrupted_main//free,
				corrupted_pre//free,
				corrupted_pre[r+1][c][v+1 mod 2],
				decide//free,
				decide[r][i],
				main//free,
				main_votes//free,
				pc//free,
				pc[j],
				pre//free,
				pre_proc//free,
				pre_proc_votes//free,
				pre_votes//free,
				pre_votes[r+1][c][v+1 mod 2],
				round//free,
				round[j]
				prove inv2[i][r][v][c][j];
		}
	}
	/* if a party decides on 0, then there are no main_votes for 1 in the next round  */
	forall (i in PROC) forall (r in ROUNDS) for(v = 0; v <= 1; v = v + 1) {
		inv3[i][r][v] : assert G ( (decide[r][i] & decide_value[r][i]=v) ->   (  main_votes[r+1][v+1 mod 2]=0 & !corrupted_main[r+1][v+1 mod 2] ) );
		forall (j in PROC) {
			subcase inv3[i][r][v][j] of inv3[i][r][v] for j=history_main_votes[r+1][v+1 mod 2];
			using (inv3[i][r][v][j]),
				inv2[i][r][v],
				lemma9[r+1][0][0][M],
				lemma9[r+1][0][1][M],
				lemma9[r+1][1][0][M],
				lemma9[r+1][1][1][M],
				lemma25[r+1][v+1 mod 2],
				/* abstractions */
				VOTES->{0,M},
				ROUNDS->{r,r+1},
				/* free variables */
				coin//free,
				corrupted_main//free,
				corrupted_main[r+1][v+1 mod 2],
				corrupted_pre//free,
				decide//free,
				decide[r][i],
				main//free,
				main_votes//free,
				main_votes[r+1][v+1 mod 2],
				pc//free,
				pc[j],
				pre//free,
				pre[r+1],
				pre_proc//free,
				pre_proc_votes//free,
				pre_votes//free,
				start//free
				prove inv3[i][r][v][j];
		}
	}
	/* if a party decides on 0, then there are no main_votes for abstain in the next round  */
	forall (i in PROC) forall (r in ROUNDS) for(v = 0; v <= 1; v = v + 1) {
		inv4[i][r][v] : assert G ( (decide[r][i] & decide_value[r][i]=v) ->   (  main_votes[r+1][2]=0 & !corrupted_main[r+1][2] ) );
		forall (j in PROC) {
			subcase inv4[i][r][v][j] of inv4[i][r][v] for j=history_main_votes[r+1][2];
			using (inv4[i][r][v][j]),
				inv2[i][r][v],
				lemma9[r+1][0][0][M],
				lemma9[r+1][1][0][M],
				lemma9[r+1][0][1][M],
				lemma9[r+1][1][1][M],
				lemma11[r+1],
				lemma16[r+1],
				lemma17[r+1],
				lemma25[r+1][2],
				corrupted2[r+1],
				corrupted6[r+1],
				/* abstractions */
				VOTES->{0,M},
				ROUNDS->{r,r+1},
				/* free variables */
				coin//free,
				corrupted_main//free,
				corrupted_main[r+1][2],
				corrupted_pre//free,
				decide//free,
				main//free,
				main_votes//free,
				main_votes[r+1][2],
				pc//free,
				pc[j],
				pre//free,
				pre_proc//free,
				pre_proc_votes//free,
				pre_votes//free,
				round//free,
				round[j]
				prove inv4[i][r][v][j];
		}
	}
	/*----------------AGREEMENT PROOF---------------------------------*/

	
	/* if two parties decide in the same round  they decide on the same value */
	forall (i in PROC) forall (r in ROUNDS) forall (j in PROC) {
		agree1[i][r][j] : assert G ( (decide[r][i] & decide[r][j]) -> decide_value[r][j]=decide_value[r][i] );
		using inv1[i][r],
			lemma25[r],
			corrupted1[r],
			/* abstractions */
			VOTES->{0,M},
			/* free variables */
			coin//free,
			corrupted_pre//free,
			corrupted_main//free,
			main//free,
			main_votes//free,
			pre//free,
			pre_proc//free,
			pre_proc_votes//free,
			pre_votes//free,
			start//free
			prove agree1[i][r][j];
	}
	/* if a party decides in round r and other party decides in round r+1, then they must decide on the same value */
	forall (i in PROC) forall (r in ROUNDS) forall (j in PROC) {
		agree2[i][r][j] : assert G ( (decide[r][i] & decide[r+1][j]) -> decide_value[r+1][j]=decide_value[r][i] );
		using inv3[i][r],
			lemma25[r+1],
			corrupted1[r+1],
			/* abstractions */
			VOTES->{0,M},
			ROUNDS->{r,r+1},
			/* free variables */
			coin//free,
			corrupted_pre//free,
			corrupted_main//free,
			decide//free,
			decide[r][i],
			decide[r+1][j],
			main//free,
			main_votes//free,
			pre//free,
			pre_proc//free,
			pre_proc_votes//free,
			pre_votes//free,
			start//free
			prove agree2[i][r][j];
	}
	/* if party i decides in round r and is the first party to decide, then any other party (j) must decide in round r or round r+1 */
	/* to prove this property we require some assumptions which we cannot prove because we are using ordset */
	
	/* the premise is that no party has decided before round r */
	/* noting that a party continues for one more round after it decides under fairness we have */
	/* all parties reaches round r+1 */
	/* and any party that does not decide in round r reaches round r+2 */
 	/* (note that therefore these assumptions includes fairness requirements) */
 	forall (i in PROC) forall (r in ROUNDS) {
		agreement_assumption1[i][r] : assert F ( round[i]=r+1 );
		agreement_assumption2[i][r] : assert G ( !decide[r][i] ) -> F ( round[i]=r+2 );
		assume agreement_assumption1[i][r], agreement_assumption2[i][r];
	}
	/* the proof is then given by */
	forall (i in PROC) forall (r in ROUNDS) forall (j in PROC) {
		agree3[i][r][j] : assert G ( (decide[r][i]) -> F (decide[r][j] | decide[r+1][j]) );
		using inv1[i][r],				
			inv3[i][r],
			inv4[i][r],
			lemma5[r+1][M],
			lemma19[r][M],
			lemma19[r+1][M],
			lemma23[r][0][M],
			lemma23[r+1][0][M],
			lemma23[r][1][M],
			lemma23[r+1][1][M],
			lemma25[r],
			lemma25[r+1],
			lemma31[r+1],
			lemma32[r+1],
			lemma37[r],
			lemma37[r+1],
			corrupted1[r+1],
			corrupted5[r+1],
			coin2[r],
			coin2[r+1],
			/* assumed properties */				
			agreement_assumption1[j][r],
			agreement_assumption2[j][r],
			/* abstractions */
			VOTES->{0,M},
			ROUNDS->{r-1,r,r+1},
			/* free variables */
			coin//free,
			corrupted_pre//free,
			corrupted_main//free,
			decide//free,
			decide[r][j],
			decide[r][i],
			decide[r+1][j],
			main//free,
			main_votes//free,
			pre//free,
			pre_proc//free,
			pre_proc_votes//free,
			pre_votes//free,
			round//free,
			round[j]
			prove agree3[i][r][j];
	}


}