Merge remote-tracking branch 'origin/develop' into feat/ublock_block_…

…cipher

.github/workflows/run-doctest.yaml

@@ -34,4 +34,6 @@ jobs:
     - name: Run test
       run: |
             cd /home/runner/_work/claasp
-            make test
+            make test
+      env:
+        GUROBI_COMPUTE_SERVER: ${{ secrets.GUROBI_COMPUTE_SERVER }}

.github/workflows/run-pytest-and-sonarcloud-scan.yaml

@@ -39,6 +39,8 @@ jobs:
       run: |
             cd /home/runner/_work/claasp
             make remote-pytest
+      env:
+        GUROBI_COMPUTE_SERVER: ${{ secrets.GUROBI_COMPUTE_SERVER }}
 
     - name: Upload Coverage.xml to artifacts
       uses: actions/upload-artifact@v4
@@ -72,4 +74,4 @@ jobs:
       env:
         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}
-    needs: run-pytest
+    needs: run-pytest

claasp/cipher_modules/models/sat/cms_models/cms_cipher_model.py

@@ -42,6 +42,7 @@
 For any further information, visit `CryptoMiniSat - XOR clauses
 <https://www.msoos.org/xor-clauses/>`_.
 """
+from claasp.cipher_modules.models.sat.sat_model import SatModel
 from claasp.cipher_modules.models.sat.utils import utils
 from claasp.cipher_modules.models.sat.sat_models.sat_cipher_model import SatCipherModel
 from claasp.name_mappings import (CONSTANT, SBOX, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT,
@@ -82,7 +83,7 @@ def build_cipher_model(self, fixed_variables=[]):
             sage: cms.build_cipher_model()
         """
         variables = []
-        constraints = self.fix_variables_value_constraints(fixed_variables)
+        constraints = SatModel.fix_variables_value_constraints(fixed_variables)
         component_types = [CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION]
         operation_types = ['AND', 'MODADD', 'MODSUB', 'NOT', 'OR', 'ROTATE', 'SHIFT', 'SHIFT_BY_VARIABLE_AMOUNT', 'XOR']
         self._model_constraints = constraints

claasp/cipher_modules/models/sat/cms_models/cms_xor_differential_model.py

@@ -42,6 +42,7 @@
 For any further information, visit `CryptoMiniSat - XOR clauses
 <https://www.msoos.org/xor-clauses/>`_.
 """
+from claasp.cipher_modules.models.sat.sat_model import SatModel
 from claasp.cipher_modules.models.sat.utils import utils
 from claasp.cipher_modules.models.sat.sat_models.sat_xor_differential_model import SatXorDifferentialModel
 from claasp.name_mappings import WORD_OPERATION, CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, \
@@ -86,7 +87,7 @@ def build_xor_differential_trail_model(self, weight=-1, fixed_variables=[]):
         """
         variables = []
         self._variables_list = []
-        constraints = self.fix_variables_value_constraints(fixed_variables)
+        constraints = SatModel.fix_variables_value_constraints(fixed_variables)
         component_types = [CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, LINEAR_LAYER, SBOX, MIX_COLUMN, WORD_OPERATION]
         operation_types = ['AND', 'MODADD', 'MODSUB', 'NOT', 'OR', 'ROTATE', 'SHIFT', 'XOR']
         self._model_constraints = constraints

claasp/cipher_modules/models/sat/sat_model.py

@@ -65,7 +65,8 @@
 from claasp.cipher_modules.models.sat import solvers
 from claasp.cipher_modules.models.sat.utils import utils
 from claasp.cipher_modules.models.utils import set_component_solution, convert_solver_solution_to_dictionary
-from claasp.name_mappings import SBOX
+from claasp.name_mappings import SBOX, CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, \
+    WORD_OPERATION
 
 
 class SatModel:
@@ -258,8 +259,8 @@ def _sequential_counter_algorithm(self, hw_list, weight, dummy_id, greater_or_eq
 
         return dummy_variables, constraints
 
-    def _sequential_counter(self, hw_list, weight):
-        return self._sequential_counter_algorithm(hw_list, weight, 'dummy_hw_0')
+    def _sequential_counter(self, hw_list, weight, dummy_id='dummy_hw_0'):
+        return self._sequential_counter_algorithm(hw_list, weight, dummy_id)
 
     def _sequential_counter_greater_or_equal(self, weight, dummy_id):
         hw_list = [variable_id for variable_id in self._variables_list if variable_id.startswith('hw_')]
@@ -301,9 +302,9 @@ def _solve_with_external_sat_solver(self, model_type, solver_name, options, host
 
         # parsing the solution
         if status == 'SATISFIABLE':
-
             variable2value = self._get_solver_solution_parsed(variable2number, values)
             component2fields, total_weight = self._parse_solver_output(variable2value)
+
         else:
             component2fields, total_weight = {}, None
         if total_weight is not None:
@@ -340,7 +341,8 @@ def _solve_with_sage_sat_solver(self, model_type, solver_name):
 
         return solution
 
-    def fix_variables_value_constraints(self, fixed_variables=[]):
+    @staticmethod
+    def fix_variables_value_constraints(fixed_variables=[]):
         """
         Return lists of variables and clauses for fixing variables in CIPHER model.
 
@@ -369,7 +371,7 @@ def fix_variables_value_constraints(self, fixed_variables=[]):
             ....:    'bit_positions': [0, 1, 2, 3],
             ....:    'bit_values': [1, 1, 1, 0]
             ....: }]
-            sage: sat.fix_variables_value_constraints(fixed_variables)
+            sage: SatModel.fix_variables_value_constraints(fixed_variables)
             ['plaintext_0',
              '-plaintext_1',
              'plaintext_2',
@@ -483,6 +485,28 @@ def weight_constraints(self, weight):
 
         return self._counter(hw_list, weight)
 
+    def build_generic_sat_model_from_dictionary(self, component_and_model_types):
+        self._variables_list = []
+        self._model_constraints = []
+        component_types = [CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION]
+        operation_types = ['AND', 'MODADD', 'MODSUB', 'NOT', 'OR', 'ROTATE', 'SHIFT', 'SHIFT_BY_VARIABLE_AMOUNT', 'XOR']
+
+        for component_and_model_type in component_and_model_types:
+            component = component_and_model_type["component_object"]
+            model_type = component_and_model_type["model_type"]
+            operation = component.description[0]
+            if component.type not in component_types or (
+                    WORD_OPERATION == component.type and operation not in operation_types):
+                print(f'{component.id} not yet implemented')
+            else:
+                sat_xor_differential_propagation_constraints = getattr(component, model_type)
+                if model_type == 'sat_bitwise_deterministic_truncated_xor_differential_constraints':
+                    variables, constraints = sat_xor_differential_propagation_constraints()
+                else:
+                    variables, constraints = sat_xor_differential_propagation_constraints(self)
+                self._model_constraints.extend(constraints)
+                self._variables_list.extend(variables)
+
     @property
     def cipher_id(self):
         return self._cipher.id

claasp/cipher_modules/models/sat/sat_models/sat_bitwise_deterministic_truncated_xor_differential_model.py

@@ -50,13 +50,13 @@ def build_bitwise_deterministic_truncated_xor_differential_trail_model(self, num
 
             sage: from claasp.cipher_modules.models.sat.sat_models.sat_bitwise_deterministic_truncated_xor_differential_model import SatBitwiseDeterministicTruncatedXorDifferentialModel
             sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
-            sage: speck = SpeckBlockCipher(number_of_rounds=22)
+            sage: speck = SpeckBlockCipher(number_of_rounds=2)
             sage: sat = SatBitwiseDeterministicTruncatedXorDifferentialModel(speck)
             sage: sat.build_bitwise_deterministic_truncated_xor_differential_trail_model()
             ...
         """
         variables = []
-        constraints = self.fix_variables_value_constraints(fixed_variables)
+        constraints = SatBitwiseDeterministicTruncatedXorDifferentialModel.fix_variables_value_constraints(fixed_variables)
         self._variables_list = []
         self._model_constraints = constraints
         component_types = (CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION)
@@ -77,7 +77,8 @@ def build_bitwise_deterministic_truncated_xor_differential_trail_model(self, num
             self._variables_list.extend(variables)
             self._model_constraints.extend(constraints)
 
-    def fix_variables_value_constraints(self, fixed_variables=[]):
+    @staticmethod
+    def fix_variables_value_constraints(fixed_variables=[]):
         """
         Return constraints for fixed variables
 
@@ -109,7 +110,7 @@ def fix_variables_value_constraints(self, fixed_variables=[]):
             ....:    'bit_positions': [0, 1, 2, 3],
             ....:    'bit_values': [2, 1, 1, 0]
             ....: }]
-            sage: sat.fix_variables_value_constraints(fixed_variables)
+            sage: SatBitwiseDeterministicTruncatedXorDifferentialModel.fix_variables_value_constraints(fixed_variables)
             ['-plaintext_0_0',
              'plaintext_0_1',
              '-plaintext_1_0',
@@ -218,6 +219,10 @@ def find_lowest_varied_patterns_bitwise_deterministic_truncated_xor_differential
             sage: trail = S.find_lowest_varied_patterns_bitwise_deterministic_truncated_xor_differential_trail(get_single_key_scenario_format_for_fixed_values(speck))
             sage: trail['status']
             'SATISFIABLE'
+
+        .. SEEALSO::
+
+            :ref:`sat-solvers`
         """
         current_unknowns_count = 1
         start_building_time = time.time()

claasp/cipher_modules/models/sat/sat_models/sat_cipher_model.py

@@ -51,7 +51,7 @@ def build_cipher_model(self, fixed_variables=[]):
             sage: sat.build_cipher_model()
         """
         variables = []
-        constraints = self.fix_variables_value_constraints(fixed_variables)
+        constraints = SatModel.fix_variables_value_constraints(fixed_variables)
         self._variables_list = []
         self._model_constraints = constraints
         component_types = [CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION]
@@ -68,6 +68,31 @@ def build_cipher_model(self, fixed_variables=[]):
             self._model_constraints.extend(constraints)
             self._variables_list.extend(variables)
 
+    def build_generic_sat_model_from_dictionary(self, fixed_variables, component_and_model_types):
+        variables = []
+        constraints = SatModel.fix_variables_value_constraints(fixed_variables)
+        self._variables_list = []
+        self._model_constraints = constraints
+        component_types = [CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION]
+        operation_types = ['AND', 'MODADD', 'MODSUB', 'NOT', 'OR', 'ROTATE', 'SHIFT', 'SHIFT_BY_VARIABLE_AMOUNT', 'XOR']
+
+        for component_and_model_type in component_and_model_types:
+            component = component_and_model_type["component_object"]
+            model_type = component_and_model_type["model_type"]
+            operation = component.description[0]
+            if component.type not in component_types or (
+                    WORD_OPERATION == component.type and operation not in operation_types):
+                print(f'{component.id} not yet implemented')
+            else:
+                sat_xor_differential_propagation_constraints = getattr(component, model_type)
+                if model_type == 'sat_bitwise_deterministic_truncated_xor_differential_constraints':
+                    variables, constraints = sat_xor_differential_propagation_constraints()
+                else:
+                    variables, constraints = sat_xor_differential_propagation_constraints(self)
+
+                self._model_constraints.extend(constraints)
+                self._variables_list.extend(variables)
+
     def find_missing_bits(self, fixed_values=[], solver_name=solvers.SOLVER_DEFAULT):
         """
         Return the solution representing a generic flow of the cipher from plaintext and key to ciphertext.