/*

QARMA

clang qarma-milp.c -o qarma-milp
./qarma-milp > qarma-milp.lp

*/

#include <stdio.h>

const int R_PARAM = 6; /* number of rounds is 2 * R_PARAM + 2 */
int dummy = 0;         /* next unused dummy variable index */
int rel_count = 0;     /* relation number */

//#define TRANSITIONS_67
#define TRANSITIONS_51

int abs(x) { return (x < 0 ? (-x) : x); };

// names of variables

// K_0 to K_15 cells of the key   (not in this program)
// T_0 to T_!5 cells of the tweak (not in this program)

// X_0_r to X_15_r cells of state at beginning of round r (or end of previous round)
// Y_0_r to Y_15_r cells of state after roundtweakey addition in round r (not in this program)

// ShuffleCells permutation (we use the MIDORI permutation)

//                             0, 1, 2, 3,   4, 5, 6, 7,   8, 9,10,11,  12,13,14,15
const int SHUFFLE_P[16]     = {0,11, 6,13,  10, 1,12, 7,   5,14, 3, 8,  15, 4, 9, 2};
const int SHUFFLE_P_inv[16] = {0, 5,15,10,  13, 8, 2, 7,  11,14, 4, 1,   6, 3, 9,12};
//                             0, 1, 2, 3,   4, 5, 6, 7,   8, 9,10,11,  12,13,14,15
const int IDENTITY[16]      = {0, 1, 2, 3,   4, 5, 6, 7,   8, 9,10,11,  12,13,14,15};

int main_1();
int main_2();

int main(int argc, const char *argv[])
{
	main_2();
}

// In the internal state matrix the data is stored as follows
//
//  0  1  2  3
//  4  5  6  7
//  8  9 10 11
// 12 13 14 15

//#define printrelheader() printf(" R%d: ",rel_count++)
 #define printrelheader() 

void MixColumns(const int shuffle[16], const int postshuffle[16],
                char input, int inround, char output, int outround)
{
	int column,i,j,k;

	for(column = 0; column < 4; column++) /* column */
	{
		// ///////////////////////////////////////////////////////////////

		// branch number is 4:

		// sum of inputs
		printrelheader();
		for (i = 0; i < 4; i++)
			printf("%c_%i_%i + ", input, shuffle[i*4+column], inround);
		// sum of inputs
		for (i = 0; i < 3; i++)
			printf("%c_%i_%i + ", output, postshuffle[i*4+ column], outround);
		printf("%c_%i_%i", output, postshuffle[3*4 + column], outround);
		// at least 4 if active at all
		printf(" - 4 A%i >= 0\n", dummy);
		//printf(" >= 4 A%i\n", dummy);

		// is any input active, then dummy != 0

		for(i = 0; i < 4; i++)
		{
			printrelheader();
			printf("A%i - %c_%i_%i >= 0\n",dummy, input, shuffle[i*4+column], inround);
		}
		for(i = 0; i < 4; i++)
		{
			printrelheader();
			printf("A%i - %c_%i_%i >= 0\n",dummy, output, postshuffle[i*4+column], outround);
		}

		// but dummy != 0 *only* if there is some input, otherwise 0 -> 0 

		printrelheader();
		for (i = 0; i < 3; i++)
			printf("%c_%i_%i + ", input, shuffle[i*4+column], inround);
		printf("%c_%i_%i", input, shuffle[3*4+column], inround);
		printf(" - A%i >= 0\n", dummy);

		// similar with output

		printrelheader();
		for (i = 0; i < 3; i++)
			printf("%c_%i_%i + ", output, postshuffle[i*4 + column], outround);
		printf("%c_%i_%i", output, postshuffle[3*4 + column], outround);
		printf(" - A%i >= 0\n", dummy);

		dummy++;

		// ///////////////////////////////////////////////////////////////

		// If cell in row k active (as always after a permutation) then at least one of the 
		// other three is active in output column (and reverse direction also true)

 		for (k = 0; k < 4; k++)
 		{
			printrelheader();
			int not_first = 0;
			for (i = 0; i < 4; i++)
			  if (i != k)
			  {
			    if (not_first) printf(" + ");
			    not_first = 1;
				printf("%c_%i_%i", input, shuffle[i*4+column], inround);
			  }
			printf(" - %c_%i_%i >= 0 \n", output, postshuffle[k*4+column], outround);

			printrelheader();
			not_first = 0;
			for (i = 0; i < 4; i++)
			  if (i != k)
			  {
			    if (not_first) printf(" + ");
			    not_first = 1;
				printf("%c_%i_%i", output, postshuffle[i*4+column], outround);
			  }
			printf(" - %c_%i_%i >= 0 \n", input, shuffle[k*4+column], inround);
 		}

		// ///////////////////////////////////////////////////////////////

        // New constraint (thanks Christof)

		// ∀(i,j)∈[4]2,i̸=j:Xi+Xj ≥Yi−Yj
		
 		for (i = 0; i < 4; i++)
 		  for (j = 0; j < 4; j++)
 		  {
#ifdef TRANSITIONS_51
			if (i != j)
#endif
#ifdef TRANSITIONS_67
			if (abs ((i-j)%4) == 2)
#endif
 		  	{
				printrelheader();
				printf("%c_%i_%i + %c_%i_%i - %c_%i_%i + %c_%i_%i >= 0\n",
						input,  shuffle[i*4+column],      inround,
						input,  shuffle[j*4+column],      inround,
						output, postshuffle[i*4+column],  outround,
						output, postshuffle[j*4+column],  outround);

				printrelheader();
				printf("%c_%i_%i + %c_%i_%i - %c_%i_%i + %c_%i_%i >= 0\n",
						output, postshuffle[i*4+column],  outround,
						output, postshuffle[j*4+column],  outround,
						input,  shuffle[i*4+column],      inround,
						input,  shuffle[j*4+column],      inround);
			}
 		  }


		// ∀k∈[4]:∀j!=k:  Yj + sum(i!=j,k) Xi - Xk >= 0

 		for (k = 0; k < 4; k++)
	 	  for (j = 0; j < 4; j++)
	 		if (j != k)
	 		{
				printrelheader();
				int not_first = 0;
	 			printf("%c_%i_%i + ", output, postshuffle[j*4+column], outround);
		 		for (i = 0; i < 4; i++)
		 		  if ((i != k) && (i != j))
		 		  {
			        if (not_first) printf(" + ");
			        not_first = 1;
	 				printf("%c_%i_%i", input, shuffle[i*4+column], inround);
		 		  }
				printf(" - %c_%i_%i >= 0\n", input, shuffle[k*4+column], inround);
	 		}

 		for (k = 0; k < 4; k++)
	 	  for (j = 0; j < 4; j++)
	 		if (j != k)
	 		{
				printrelheader();
				int not_first = 0;
	 			printf("%c_%i_%i + ", input, shuffle[j*4+column], inround);
		 		for (i = 0; i < 4; i++)
		 		  if ((i != k) && (i != j))
		 		  {
			        if (not_first) printf(" + ");
			        not_first = 1;
	 				printf("%c_%i_%i", output, postshuffle[i*4+column], outround);
		 		  }
				printf(" - %c_%i_%i >= 0\n", output, postshuffle[k*4+column], outround);
	 		}

		//printf("\n");
	}
}

int main_1()
{
	int i,j,r;

	printf("Minimize\n"); /* print objective function */

	// ////////////////////////////////////////////////////////////////
	//
	// Now model the cipher as one short round and R_PARAM full ones
	// Input is {X_i_0}_i, goes into first S-Box layer, then round function
	// Generates {X_i_1}_i, which goes into second layer.
	// There is a total of R_PARAM+1 S-Box layers in half cipher, so the
	// last variable block is {X_(R_PARAM)_1}_i
	//
	// First, the variables

	for (j=0;j<=R_PARAM;j++)
		for (i = 0; i < 16; i++)
		{
			printf("X_%i_%i",i,j);
			if ((j!=R_PARAM) || (i != 15)) printf(" + ");
			if (i == 15) printf("\n");
		}
	printf("\n");

	// ////////////////////////////////////////////////////////////////
	//
	// Now model half of the cipher as one short round and R_PARAM full ones

	printf("Subject To\n"); /* round function constraints */

	for (r = 0; r<R_PARAM; r++)
	{
		MixColumns(SHUFFLE_P, IDENTITY, 'X', r, 'X', r+1);
	}

	// ////////////////////////////////////////////////////////////////
	//
	// At least one S-box must be active per round

	//for (j=0;j<R_PARAM;j++)
	j =0; // this suffices
		{
		for (i = 0; i < 16; i++)
		{
			printf("X_%i_%i",i,j);
			if (i != 15) printf(" + ");
		}
		printf(" >= 1\n");
	}

	printf("\n");

	// ////////////////////////////////////////////////////////////////
	//
	// Declare variables as binary

	printf("Binary\n"); /* binary constraints */
	for (r=0;r<=R_PARAM;r++)
		for (i = 0; i < 16; i++) printf("X_%i_%i\n",i,r);

	for (i = 0; i < dummy; i++) printf("A%i\n",i);

	printf ("End\n");
	return 0;
}


#define SBOX_OUT sboxlayers++; printf("\\\\ Sbox layer %d ready\n", sboxlayers);

int main_2()
{
	int i,j,r;
	int t[16];

	// ///////////////////////////////////////////////////////////////////
	//
	// initially the tweak is in its input state, no permutation

	for (i = 0; i < 16; i++) t[i] = i;

	printf("Minimize\n"); /* print objective function */

	for (j=0;j<=R_PARAM;j++)
		for (i = 0; i < 16; i++)
		{
			printf("X_%i_%i + ",i,j);
			if (i == 15) printf("\n");
		}
	for (j=0;j<=R_PARAM;j++)
		for (i = 0; i < 16; i++)
		{
			printf("Z_%i_%i",i,j);
			if ((j!=R_PARAM) || (i != 15)) printf(" + ");
			if (i == 15) printf("\n");
		}
	printf("\n");

	// ///////////////////////////////////////////////////////////////////
	//
	// Now model the cipher 

	printf("Subject To\n"); /* round function constraints */

	// FORWARD ROUNDS
	
	int sboxlayers = 0;
	
	for (r = 0; r<R_PARAM; r++)
	{
		MixColumns(SHUFFLE_P, IDENTITY, 'X', r, 'X', r+1);
	}

	// (pseudo)-reflector
	
	MixColumns(SHUFFLE_P, SHUFFLE_P,'X', R_PARAM, 'Z', R_PARAM); 

	// BACKWARD ROUNDS (we "read" them forward, though)

	for (r = 0; r<R_PARAM; r++)
	{
		MixColumns(SHUFFLE_P, IDENTITY, 'Z', r, 'Z', r+1);
	}

	// ///////////////////////////////////////////////////////////////////

	// Exclude trivial solution (no active input)

	printrelheader();
	for (i = 0; i < 16; i++)
	{
		printf("X_%i_%i",i,0);
		if (i != 15) printf(" + ");
	}
	printf(" >= 1\n");

	printf("\n");

	// ///////////////////////////////////////////////////////////////////
	//
	// Declare variables as binary

	printf("Binary\n"); /* binary constraints */

	for (r=0;r<=R_PARAM;r++)
	  for (i = 0; i < 16; i++)
	  	{
			printf("X_%i_%i\n",i,r);
			printf("Z_%i_%i\n",i,r);
		}

	for (i = 0; i < dummy; i++) printf("A%i\n",i);

	// ///////////////////////////////////////////////////////////////////

	printf ("End\n");

	return 0;

	// ///////////////////////////////////////////////////////////////////
}