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