// This file describes how to do verification using the
// Strong Nullstellensatz. 

// This singular file verifies a 2-bit GF 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 (output) A, B inputs
// 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
// variables ordered reverse topologically
// Reverse topological term order: LEX term order, with this variable order
ring R = (2, X), (Z, A, B,z_0,z_1,r_0, s_0, s_3, s_1, s_2, a_0, a_1, b_0, b_1), 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 + A*B; //Spec

// Implementation from gates

// Word-level to bit-level relationships
poly f1 = a_0 + A+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;


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

ideal J0_PI = a_0^2-a_0, b_0^2-b_0, a_1^2-a_1, b_1^2-b_1; 
//, s_0^2-s_0,
//s_1^2-s_1, s_2^2-s_2, s_3^2-s_3,r_0^2-s_0,
//A^4-A, B^4-B, Z^4-Z;

ideal G;

//G = groebner(J+J0_PI);

// Under RTTO, J + J0_PI = minimal Groebner basis
G = J + J0_PI;

// Reduce the spec modulo the GB(J+J0_PI)

poly r;

r = reduce(f_spec, G);

printf("If r = 0, then spec = circuit:");

printf("Remainder r is:");
r;

// Computing noredSB of J+J0_PI should = J+J0_PI itself
printf("Computing noredSB of J+J0_PI should = J+J0_PI itself!");
printf("J+J0_PI is a minimal GB!");
option(noredSB);

printf("J + J0_PI is:");
G;

printf("GB(J + J0_PI) is:");
groebner(J+J0_PI);

printf("Try changing the term order to deglex, and J+J0_PI will NOT be a Groebner Basis!");