// This file describes how to reverse engineer a specification
// polynomial using Elimination term orders

// This singular file extracts a word-level spec polynomials from a
// 2-bit GF multiplier circuit

// Spec should be: 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
// This is not RTTO, it should be the abstraction term order
// bit-level vars > word-level output Z > word-leven inputs A, B

ring R = (2, X), (z_0,z_1,r_0, s_0, s_3, s_1, s_2, a_0, a_1, b_0, b_1, Z, A, B), 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 = 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;



printf("Reduced GB of J + J0 should contain the spec poly Z+A*B");
printf("GB of J + J0 is:");

option(redSB);
G = groebner(J+J0);
G;