Merge pull request #119 from Crypto-TII/fix/sat-constraints-for-compo…

…nents

Fix SAT constraints for AND and OR

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.

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.

claasp/components/or_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.components.multi_input_non_linear_logical_operator_component import MultiInputNonlinearLogicalOperator
 
@@ -211,6 +212,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_OR({params})']
 
+    def sat_constraints(self):
+        """
+        Return a list of variables and a list of clauses for OR 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.permutations.gift_permutation import GiftPermutation
+            sage: gift = GiftPermutation(number_of_rounds=3)
+            sage: or_component = gift.component_from(0, 4)
+            sage: or_component.sat_constraints()
+            (['or_0_4_0',
+              'or_0_4_1',
+              'or_0_4_2',
+              ...
+              'or_0_4_31 -xor_0_3_31',
+              'or_0_4_31 -xor_0_1_31',
+              '-or_0_4_31 xor_0_3_31 xor_0_1_31'])
+        """
+        _, 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_or(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 for OR operation in SMT CIPHER model.

tests/unit/components/and_component_test.py

@@ -64,6 +64,20 @@ def test_generic_sign_linear_constraints():
     assert and_component.generic_sign_linear_constraints(input_constraints, output) == 1
 
 
+def test_sat_constraints():
+    fancy = FancyBlockCipher(number_of_rounds=3)
+    and_component = fancy.component_from(0, 8)
+    output_bit_ids, constraints = and_component.sat_constraints()
+
+    assert output_bit_ids[0] == 'and_0_8_0'
+    assert output_bit_ids[1] == 'and_0_8_1'
+    assert output_bit_ids[2] == 'and_0_8_2'
+
+    assert constraints[-3] == '-and_0_8_11 xor_0_7_11'
+    assert constraints[-2] == '-and_0_8_11 key_23'
+    assert constraints[-1] == 'and_0_8_11 -xor_0_7_11 -key_23'
+
+
 def test_smt_constraints():
     fancy = FancyBlockCipher(number_of_rounds=3)
     and_component = fancy.component_from(0, 8)

tests/unit/components/multi_input_non_linear_logical_operator_component_test.py

@@ -82,20 +82,6 @@ def test_milp_xor_linear_mask_propagation_constraints():
     assert str(constraints[-1]) == "x_49 == 10*x_48"
 
 
-def test_sat_constraints():
-    fancy = FancyBlockCipher(number_of_rounds=3)
-    and_component = fancy.component_from(0, 8)
-    output_bit_ids, constraints = and_component.sat_constraints()
-
-    assert output_bit_ids[0] == 'and_0_8_0'
-    assert output_bit_ids[1] == 'and_0_8_1'
-    assert output_bit_ids[2] == 'and_0_8_2'
-
-    assert constraints[-3] == '-and_0_8_11 xor_0_7_11'
-    assert constraints[-2] == '-and_0_8_11 key_23'
-    assert constraints[-1] == 'and_0_8_11 -xor_0_7_11 -key_23'
-
-
 def test_sat_xor_differential_propagation_constraints():
     fancy = FancyBlockCipher(number_of_rounds=3)
     and_component = fancy.component_from(0, 8)

tests/unit/components/or_component_test.py

@@ -53,6 +53,20 @@ def test_generic_sign_linear_constraints():
     assert or_component.generic_sign_linear_constraints(input_tert, output) == 1
 
 
+def test_sat_constraints():
+    gift = GiftPermutation(number_of_rounds=3)
+    or_component = gift.component_from(0, 4)
+    output_bit_ids, constraints = or_component.sat_constraints()
+
+    assert output_bit_ids[0] == 'or_0_4_0'
+    assert output_bit_ids[1] == 'or_0_4_1'
+    assert output_bit_ids[2] == 'or_0_4_2'
+
+    assert constraints[-3] == 'or_0_4_31 -xor_0_3_31'
+    assert constraints[-2] == 'or_0_4_31 -xor_0_1_31'
+    assert constraints[-1] == '-or_0_4_31 xor_0_3_31 xor_0_1_31'
+
+
 def test_smt_constraints():
     gift = GiftPermutation(number_of_rounds=3)
     or_component = gift.component_from(0, 4)