diff --git a/claasp/components/and_component.py b/claasp/components/and_component.py index bc24342c..2e55e41b 100644 --- a/claasp/components/and_component.py +++ b/claasp/components/and_component.py @@ -17,6 +17,7 @@ # **************************************************************************** +from claasp.cipher_modules.models.sat.utils import utils as sat_utils from claasp.cipher_modules.models.smt.utils import utils as smt_utils from claasp.cipher_modules.models.milp.utils import utils as milp_utils from claasp.components.multi_input_non_linear_logical_operator_component import MultiInputNonlinearLogicalOperator @@ -376,6 +377,42 @@ def get_bit_based_vectorized_python_code(self, params, convert_output_to_bytes): def get_byte_based_vectorized_python_code(self, params): return [f' {self.id} =byte_vector_AND({params})'] + def sat_constraints(self): + """ + Return a list of variables and a list of clauses for AND operation in SAT CIPHER model. + + This method support AND operation using more than two operands. + + .. SEEALSO:: + + :ref:`sat-standard` for the format. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.fancy_block_cipher import FancyBlockCipher + sage: fancy = FancyBlockCipher(number_of_rounds=3) + sage: and_component = fancy.component_from(0, 8) + sage: and_component.sat_constraints() + (['and_0_8_0', + 'and_0_8_1', + 'and_0_8_2', + ... + '-and_0_8_11 xor_0_7_11', + '-and_0_8_11 key_23', + 'and_0_8_11 -xor_0_7_11 -key_23']) + """ + _, input_bit_ids = self._generate_input_ids() + output_bit_len, output_bit_ids = self._generate_output_ids() + constraints = [] + for i in range(output_bit_len): + constraints.extend(sat_utils.cnf_and(output_bit_ids[i], input_bit_ids[i::output_bit_len])) + + return output_bit_ids, constraints + def smt_constraints(self): """ Return a variable list and SMT-LIB list asserts representing AND operation FOR SMT CIPHER model. diff --git a/claasp/components/multi_input_non_linear_logical_operator_component.py b/claasp/components/multi_input_non_linear_logical_operator_component.py index c93dcf8c..cd80347e 100644 --- a/claasp/components/multi_input_non_linear_logical_operator_component.py +++ b/claasp/components/multi_input_non_linear_logical_operator_component.py @@ -365,42 +365,6 @@ def milp_xor_linear_mask_propagation_constraints(self, model): return result - def sat_constraints(self): - """ - Return a list of variables and a list of clauses for AND operation in SAT CIPHER model. - - This method support AND operation using more than two operands. - - .. SEEALSO:: - - :ref:`sat-standard` for the format. - - INPUT: - - - None - - EXAMPLES:: - - sage: from claasp.ciphers.block_ciphers.fancy_block_cipher import FancyBlockCipher - sage: fancy = FancyBlockCipher(number_of_rounds=3) - sage: and_component = fancy.component_from(0, 8) - sage: and_component.sat_constraints() - (['and_0_8_0', - 'and_0_8_1', - 'and_0_8_2', - ... - '-and_0_8_11 xor_0_7_11', - '-and_0_8_11 key_23', - 'and_0_8_11 -xor_0_7_11 -key_23']) - """ - _, input_bit_ids = self._generate_input_ids() - output_bit_len, output_bit_ids = self._generate_output_ids() - constraints = [] - for i in range(output_bit_len): - constraints.extend(sat_utils.cnf_and(output_bit_ids[i], input_bit_ids[i::output_bit_len])) - - return output_bit_ids, constraints - def sat_xor_differential_propagation_constraints(self, model=None): """ Return a list of variables and a list of clauses for AND operation in SAT XOR DIFFERENTIAL model.