FIX/Fix: Move SAT constraints for AND in correct module

Crypto-TII · Dec 2, 2023 · d86d85e · d86d85e
1 parent 5477059
commit d86d85e
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 36 deletions.
diff --git 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
@@ -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.