// This file verifies a 2-bit integer multiplier over Q

// Lex order RTTO
// Ring R = 0..., 0 = field of characteristic 0 = Q
ring R = 0, (z_0, z_1, z_2, z_3, e_9, e_8, e_7, e_6, e_5, e_4, e_3, e_2, e_1, a_0, a_1, b_0, b_1), lp;

// Under non RTTO order, e.g. deglex, J + J0 will NOT be a GB itself!
// Deglex = degree lex
//ring r = 0, (a_0, a_1, b_0, b_1, e_1, e_2, e_3, e_4, e_5, e_6, e_7, e_8, e_9, z_0, z_1, z_2, z_3), Dp;

poly f_spec = (z_0 + 2*z_1 + 4*z_2 + 8*z_3) - (a_0 + 2*a_1)*(b_0 + 2*b_1); //spec
poly f1 = z_3 - e_9*e_5;
poly f2 = z_2 - (e_9 + e_5 -2*e_9*e_5);
poly f3 = z_1 - (e_4 + e_1 - 2*e_4*e_1);
poly f4 = z_0 - (a_0*b_0);
poly f5 = e_1 - (a_1*b_0);
poly f6 = e_2 - (1-b_0);
poly f7 = e_3 - (b_0 + a_0 - a_0*b_0);
poly f8 = e_4 - (a_0*b_1);
poly f9 = e_5 - (b_1*a_1);
poly f10 = e_6 - e_3*b_0;
poly f11 = e_7 - (e_6 + e_2 - 2*e_6*e_2);
poly f12 = e_8 - e_7*e_1;
poly f13 = e_9 - (e_8*e_4);

ideal J = f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13;

ideal J0 = a_0^2 - a_0, a_1^2 - a_1, b_0^2 - b_0, b_1^2 - b_1;

printf("J+J0 = minimal GB even for integer arithmetic circuits");
printf("J + J0 is:");
J+J0;

printf("non reduced but minimal GB(J+J0) is:");
option(noredSB);
groebner(J+J0);

printf("Verification: f_spec mod (J+J0) should be 0");
reduce(f_spec, J+J0);