// This file describes how to declare and instantiate a miter in an
// algebraic framework. This singular file miters a 2-bit multiplier
// circuit against a word-level spec.

// Spec: GF(2^2), P(X) = X^2+X+1, Z = A*B (mod P(X))
// Note (mod P(X)) is implicit, as everything in GF is (mod P(X))

// Implementation is a 2-bit Mastrovito multiplier circuit. The
// circuit is given in the gf.pdf slides, towards the end of the slide
// set. I'm going to use the same variables names as given in my slides.

// Variables of the ring:
//
// Word-level variables: Z_s for spec, Z (implementation) A, B inputs
// Free variable: t
// Bit level variables of the circuit:
// a_0,a_1,b_0,b_1,s_0,s_1,s_2,s_3,r_0,z_0,z_1
//

// declare the ring
ring r = (2, X), (Z_s, Z, A, B,a_0,a_1,b_0,b_1,s_0,s_1,s_2,s_3,r_0,z_0,z_1,t), lp;

// Note how multi-variate rings are declared.
// The last keyword 'lp' means that terms of polynomials are ordered lexicographically

minpoly = X^2+X+1;

// X = alpha here...

// First we will declare polynomials, and then declare an ideal

poly f_spec = Z_s + A*B; //Spec

// Implementation from gates

// Word-level to bit-level relationships
poly f1 = A+a_0 + a_1*X;
poly f2 = B + b_0 + b_1*X;
poly f3 = Z + z_0 + z_1*X;

// Polynomials representing the gates in the design

poly f4 = s_0 + a_0*b_0; // AND gate
poly f5 = s_1 + a_0*b_1; // AND gate
// You could introduce a bug in the design by replacing the AND gate at
// s_1 to an XOR gate at s_1
// BUG:
// poly f5 = s_1 + a_0 +b_1,
// AND gate replaced by XOR
// Other gates:
poly f6 = s_2 + a_1*b_0;
poly f7 = s_3 + a_1*b_1;
poly f8 = r_0 + s_1 + s_2;
poly f9 = z_0 + s_0 + s_3;
poly f10 = z_1 + r_0 + s_3;

// and now the miter polynomial

poly f_m = t*(Z_s-Z) + 1;

// Declare an ideal generated by the miter's polynomials
ideal J = f_spec, f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f_m;

// You could write out the ideal J:
printf("Ideal J is:", J);
J;


// We can compute the Groebner basis of ideal J
// G = groebner(J);

ideal G;

G = groebner(J);

printf("Groebner basis G of ideal J:");

G;


printf("If G = 1, then variety of ideal J is empty, or the miter in infeasible. \
 This is because 1=0 has no solutions!!");

printf("");
printf("");

printf("You should introduce a bug, as shown in poly f5, and recompute \
GB(J) and see for yourself the output G. If G is not equal to {1}, \
then variety is non-empty, i.e. solutions exist to ideal J.");