N window heuristic helper

convert_clauses(clauses)

generate_window_size_clauses(first_input_difference, second_input_difference, output_difference, aux_var)

Returns a set of clauses representing a simplified CNF (Conjunctive Normal Form) expression for the n-window size heuristic applied to a + b = c. Specifically, these clauses ensure that no more than n variables are true (i.e., there are no sequences of n+1 ones in the carry differences of a + b = c). These clauses were obtained after simplifying the formula below (in sympy notation): formula_temp = Equivalent(And(*[Xor(A[i], B[i], C[i]) for i in range(n - 1)]), aux); formula = And(Not(And(aux, Xor(A[n - 1], B[n - 1], C[n - 1]))), formula_temp). The variable aux is used to store the conjunctions of the carries of the addition of the n - 1 bits of A and B. aux will serve as a variable to allow users to perform a global count on the number of full n-window sequences.

INPUT:

• a – list: List of binary variables representing the input differences a

• b – list: List of binary variables representing the input differences b

• c – list: List of binary variables representing the input differences c

• aux – integer: Auxiliary variable used to store the conjunctions of the carry differences from the addition of the first n - 1 bit differences of a and b

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.utils.n_window_heuristic_helper import generate_window_size_clauses
sage: a = [1, 2, 3, 4]
sage: b = [5, 6, 7, 8]
sage: c = [9, 10, 11, 12]
sage: aux = 10
sage: cnf = generate_window_size_clauses(a, b, c, aux) # doctest:+SKIP
sage: cnf # doctest:+SKIP
['4   -4   -10', '8   -10   -8']

generating_n_window_clauses(window_size_plus_one)

load_list(filename)

Load a list from a file using pickle.

save_list(data, filename)

Save a list to a file using pickle.