/*

clang qarma-reltweak.c -o qarma-reltweak

./qarma-reltweak 2 3 > qarma-reltweak-67-3-full.lp
./qarma-reltweak 2 4 > qarma-reltweak-67-4-full.lp
./qarma-reltweak 2 5 > qarma-reltweak-67-5-full.lp
./qarma-reltweak 2 6 > qarma-reltweak-67-6-full.lp
./qarma-reltweak 2 7 > qarma-reltweak-67-7-full.lp
./qarma-reltweak 2 8 > qarma-reltweak-67-8-full.lp
./qarma-reltweak 1 9 > qarma-reltweak-67-9-half.lp
./qarma-reltweak 1 10 > qarma-reltweak-67-10-half.lp
./qarma-reltweak 1 11 > qarma-reltweak-67-11-half.lp

*/

#include <stdio.h>

#define TRANSITIONS_67
//#define TRANSITIONS_51

/* number of rounds is 2 * R_PARAM + 2, here R_PARAM + 1 simulated */

int R_PARAM = 6;

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

int main_1(); /* does only half of the cipher */
int main_2(); /* does both halves through reflector */

int main(int argc, const char *argv[])
{
	int type;
	
	if ( (argc != 3) )
		goto param_error;

	sscanf(argv[1],"%d",&type);

	if ((type < 1) || (type > 2))
		goto param_error;

	sscanf(argv[2],"%d",&R_PARAM);

	if ((R_PARAM < 3) || (R_PARAM > 12))
		goto param_error;

	if (type == 1)
		main_1();
	else
		main_2();

	return 0;

param_error:

	printf("Usage: qarma-reltweak type rounds\n"
	       "type = 1 for half cipher, type = 2 for full cipher\n"
	       "3 <= rounds <= 12\n");

	return 1;
	
}

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

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

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

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

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

int rel_count = 0;         /* next unused dummy variable index */
int dummy = 0;         /* next unused dummy variable index */

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

// names of variables

// K_0 to K_15 cells of the key   (not in this program)

// T_0 to T_15 cells of the tweak

// X_0_r to X_15_r cells of state at beginning of round r (or end of previous round)
//   Usually: output of a MixColumns, input to tweak addition
// Use Z_i_r for backward rounds

// Y_0_r to Y_15_r cells of state after roundtweakey addition in round r
//   Usually: output of tweak addition, input to MixColumns
// Use W_i_r for backward rounds

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

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

// 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

// Tweak permutation

//                              0, 1, 2, 3,   4, 5, 6, 7,   8, 9,10,11,  12,13,14,15
const int TWEAKEY_P[16]     = { 6, 5,14,15,   0, 1, 2, 3,   7,12,13, 4,   8, 9,10,11};
const int TWEAKEY_P_inv[16] = { 4, 5, 6, 7,  11, 1, 0, 8,  12,13,14,15,   9,10, 2, 3};
//                              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};

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

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");
	}
}

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

#if 1

void PermuteTweak(int t[16])
{
	int tmp[16];
	int i,j;
	for(i=0; i < 16; i++)
	{
		j = TWEAKEY_P[i];
		tmp[i] = t[j];
	}

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

void PermuteTweakInv(int t[16])
{
	int tmp[16];
	int i,j;
	for(i=0; i < 16; i++)
	{
		j = TWEAKEY_P_inv[i];
		tmp[i] = t[j];
	}

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

#else

#define TWEAK_PERMUTE_OFFSET 1

void PermuteTweak(int t[16])
{
	for(int i=0; i < 16; i++)
	{
		t[i] = (t[i] + TWEAK_PERMUTE_OFFSET) % 16;
	}
}

void PermuteTweakInv(int t[16])
{
	for(int i=0; i < 16; i++)
	{
		t[i] = (t[i] + 16 - TWEAK_PERMUTE_OFFSET) % 16;
	}
}

#endif

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

/*

How to model the XOR of 2 or 3 valus.

C2_⊕[i1, i2, o, d] is the set of linear constraints

is {i1 ≤ d} ∪ {i2 ≤ d} ∪ {o ≤ d} ∪ {i1 + i2  + o ≥ 2d}.

C3_⊕[i1, i2, i3, o, d] is the set of linear constraints

is {i1 ≤ d} ∪ {i2 ≤ d} ∪ {i3 ≤ d} ∪ {o ≤ d} ∪ {i1 + i2 + i3 + o ≥ 2d}.

*/

void AddRoundTweak(char input, int round, char output, int nextround, int t[16])
{
	int i;

	for(i = 0; i < 16; i++)
	{ 
		// inputs: X_i_r and T_i
		// output: Y_i_r or X_i_{next r}

		printrelheader();
		printf("A%i - %c_%i_%i >= 0\n",     dummy, input,  i, round);     /* input 1 */
		printrelheader();
		printf("A%i - T_%i >= 0\n",         dummy, t[i]);                 /* input 2 */
		printrelheader();
		printf("A%i - %c_%i_%i >= 0\n",     dummy, output, i, nextround); /* output  */
		printrelheader();
		printf("%c_%i_%i + T_%i + %c_%i_%i - 2 A%i >= 0\n", 
											input,  i, round,
											t[i],
											output, i, nextround,
											dummy);
		dummy++;
	}
}

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

int main_1()
{
	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 ((j!=R_PARAM) || (i != 15)) printf(" + ");
			if (i == 15) printf("\n");
		}
	printf("\n");

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

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

	AddRoundTweak('I', 0, 'X', 0, t); /* all X_i_0 go into an S-Box, not I_0 */
	PermuteTweak(t);

	for (r = 0; r<R_PARAM; r++)
	{
		AddRoundTweak('X', r, 'Y', r, t);
		MixColumns(SHUFFLE_P, SHUFFLE_P_inv,'Y', r, 'X', r+1); /* all X_i_{r+1} go into an S-Box */
		PermuteTweak(t);
	}

	// Exclude trivial solution (all zeros)
	// Sum of active input and tweak cells must be at least 1

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

	printf("\n");

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

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

	for (i = 0; i < 16; i++) printf("I_%i_0\n",i);

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

	for (r=0;r<R_PARAM;r++)
		for (i = 0; i < 16; i++) printf("Y_%i_%i\n",i,r);

	for (i = 0; i < 16; i++) printf("T_%i\n",i);

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

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

	printf ("End\n");

	return 0;

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

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");

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

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

	// FORWARD ROUNDS
	
	// Prepare first X0

	AddRoundTweak('I', 0, 'X', 0, t); /* all X_i_0 go into an S-Box, not I_0 */
	PermuteTweak(t);

	for (r = 0; r<R_PARAM; r++)
	{
		AddRoundTweak('X', r, 'Y', r, t);
		MixColumns(SHUFFLE_P, IDENTITY,'Y', r, 'X', r+1); /* all X_i_{r+1} go into an S-Box */
		if (r != R_PARAM-1) PermuteTweak(t);
	}

	printf("\n");

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

	// BACKWARD ROUNDS

	for (r = R_PARAM-1; r>=0; r--)
	{
		//MixColumns(IDENTITY, SHUFFLE_P_inv,'Z', r+1, 'W', r);
		MixColumns(SHUFFLE_P, IDENTITY,'W', r, 'Z', r+1);
		AddRoundTweak('W', r, 'Z', r, t);
		PermuteTweakInv(t);
	}

	/* AddRoundTweak('Z', 0, 'O', 0, t); */ /* all Z_i_0 go into an S-Box, not I_0 */

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

	// Exclude trivial solution (all zeros)
	// Sum of all SBoxes AND of the tweak cells must be at least 1

	printf("\n");

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

	printf("\n");

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

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

	for (i = 0; i < 16; i++)
	{
		printf("I_%i_0\n",i);
		//printf("O_%i_0\n",i);
		printf("T_%i\n",i);
	}

	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 (r=0;r<R_PARAM;r++)
	  for (i = 0; i < 16; i++)
	  	{
			printf("Y_%i_%i\n",i,r);
			printf("W_%i_%i\n",i,r);
		}

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

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

	printf ("End\n");

	return 0;

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