// Use the same field F_8 = F_2 (mod X^3 + X + 1)
// that was used for interpolation

ring r = (2,X), (Z_s, Z, A, t, z_0, z_1, z_2, b_1, b_2, b_3, a_2, a_1, a_0), lp;

minpoly = X^3 + X + 1;

// Spec = interpolated polynomial
// Output word Z_s, input word A
poly f_spec = Z_s - ((X2+X+1)*A7+(X2+1)*A6+(X)*A5+(X+1)*A4+(X2+X+1)*A3+(X2+1)*A);

// Implementation
poly f_A = A - (a_0 + a_1* X + a_2*X^2);
poly f_Z = Z - (z_0 + z_1*X + z_2*X^2);

// z_2 = a_1 OR b_1
poly f1 = z_2 - (b_1 + a_1 + b_1*a_1);
// b_1 = a_2 AND a_0'
poly f2 = b_1 - (a_2*(1+a_0));

// z1 = b2 OR b3
poly f3 = z_1 - (b_2 + b_3 + b_2*b_3);
poly f4 = b_2 - ((1+a_2)*a_1);
poly f5 = b_3 - (a_2*(1+a_1)*a_0);

// z_0 = a2 OR a1 OR a0
poly f6 = z_0 -( a_2 + a_1 + a_0 + a_2*a_1 + a_2*a_0 + a_1*a_0 + a_2*a_1*a_0);

// the miter polynomial

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

// The ideal generated by the miter
ideal Jm = f_spec, f_A, f_Z, f1, f2, f3, f4, f5, f6, fm;

// The ideal of vanishing polynomials (need only for primary inputs)
ideal J0 = a_0^2-a_0, a_1^2-a_1, a_2^2-a_2;

ideal G;

G = groebner(Jm+J0);

printf("If G=GB(Jm+J0)=1, the interpolated spec and the synthesized circuit are equivalent");
G;