Modsub component

class MODSUB(current_round_number, current_round_number_of_components, input_id_links, input_bit_positions, output_bit_size, modulus)

Bases: Modular

algebraic_polynomials(model)

Return a list of polynomials representing Modular subtraction operation

INPUT:

• model – model object; a model instance

EXAMPLES:

sage: from claasp.cipher_modules.models.algebraic.algebraic_model import AlgebraicModel
sage: from claasp.cipher import Cipher
sage: cipher = Cipher("cipher_name", "permutation", ["input"], [8], 8)
sage: cipher.add_round()
sage: modsub_0_0 = cipher.add_MODSUB_component(["input","input"], [[0,1,2,3],[4,5,6,7]], 4)
sage: modsub_component = cipher.get_component_from_id('modsub_0_0')
sage: algebraic = AlgebraicModel(cipher)
sage: modsub_component.algebraic_polynomials(algebraic)
[modsub_0_0_b0_0,
 modsub_0_0_b0_0 + modsub_0_0_y0 + modsub_0_0_x4 + modsub_0_0_x0,
 modsub_0_0_x4*modsub_0_0_b0_0 + modsub_0_0_x0*modsub_0_0_b0_0 + modsub_0_0_x0*modsub_0_0_x4 + modsub_0_0_b0_1 + modsub_0_0_b0_0 + modsub_0_0_x4,
 modsub_0_0_b0_1 + modsub_0_0_y1 + modsub_0_0_x5 + modsub_0_0_x1,
 modsub_0_0_x5*modsub_0_0_b0_1 + modsub_0_0_x1*modsub_0_0_b0_1 + modsub_0_0_x1*modsub_0_0_x5 + modsub_0_0_b0_2 + modsub_0_0_b0_1 + modsub_0_0_x5,
 modsub_0_0_b0_2 + modsub_0_0_y2 + modsub_0_0_x6 + modsub_0_0_x2,
 modsub_0_0_x6*modsub_0_0_b0_2 + modsub_0_0_x2*modsub_0_0_b0_2 + modsub_0_0_x2*modsub_0_0_x6 + modsub_0_0_b0_3 + modsub_0_0_b0_2 + modsub_0_0_x6,
 modsub_0_0_b0_3 + modsub_0_0_y3 + modsub_0_0_x7 + modsub_0_0_x3]

as_python_dictionary()

check_output_size(available_word_sizes, fixed, word_size)

cms_constraints()

Return a list of variables and a list of clauses for Modular Subtraction in CMS CIPHER model.

See also

SAT standard of Cipher for the format.

Warning

This method heavily relies on the fact that modular subtraction is always performed using two operands.

INPUT:

• None

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.raiden_block_cipher import RaidenBlockCipher
sage: raiden = RaidenBlockCipher(number_of_rounds=3)
sage: modsub_component = raiden.component_from(0, 7)
sage: modsub_component.cms_constraints()
(['temp_carry_plaintext_32',
  'temp_carry_plaintext_33',
  'temp_carry_plaintext_34',
  ...
  'modsub_0_7_31 -modadd_0_4_31 temp_input_plaintext_63',
  'modsub_0_7_31 modadd_0_4_31 -temp_input_plaintext_63',
  '-modsub_0_7_31 -modadd_0_4_31 -temp_input_plaintext_63'])

cms_xor_differential_propagation_constraints(model)

cms_xor_linear_mask_propagation_constraints(model=None)

Return a list of variables and a list of clauses for fixing variables in CMS XOR LINEAR model.

See also

CMS XOR LINEAR model for the format, [LWR2016] for the algorithm.

Warning

This method heavily relies on the fact that modular addition/substration is always performed using two addenda.

INPUT:

• model – model object (default: None); a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: modadd_component = speck.component_from(0, 1)
sage: modadd_component.cms_xor_linear_mask_propagation_constraints()
(['modadd_0_1_0_i',
  'modadd_0_1_1_i',
  'modadd_0_1_2_i',
  ...
  'hw_modadd_0_1_14_o -modadd_0_1_14_o modadd_0_1_30_i',
  'hw_modadd_0_1_15_o modadd_0_1_15_o -modadd_0_1_31_i',
  'hw_modadd_0_1_15_o -modadd_0_1_15_o modadd_0_1_31_i'])

cp_constraints()

Return lists of declarations and constraints for Modular Addition component for CP CIPHER model.

INPUT:

• None

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.raiden_block_cipher import RaidenBlockCipher
sage: raiden = RaidenBlockCipher(number_of_rounds=3)
sage: modsub_component = raiden.component_from(0, 7)
sage: modsub_component.cp_constraints()
(['array[0..31] of var 0..1: constant_modsub_0_7= array1d(0..31,[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]);',
  ...
  'array[0..31] of var 0..1:minus_pre_modsub_0_7_1;'],
 ['constraint pre_modsub_0_7_0[0]=modadd_0_4[0];',
  'constraint pre_modsub_0_7_0[1]=modadd_0_4[1];',
  'constraint pre_modsub_0_7_0[2]=modadd_0_4[2];',
  ...
  'constraint pre_minus_pre_modsub_0_7_1[31]=(pre_modsub_0_7_1[31] + 1) mod 2;',
  'constraint modadd(pre_minus_pre_modsub_0_7_1, constant_modsub_0_7, minus_pre_modsub_0_7_1);',
  'constraint modadd(pre_modsub_0_7_0,minus_pre_modsub_0_7_1,modsub_0_7);'])

cp_deterministic_truncated_xor_differential_constraints(inverse=False)

Return lists of variables and constraints for Modular Addition/Substraction in CP deterministic truncated XOR differential model.

INPUT:

• inverse – boolean (default: False)

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: modadd_component = speck.component_from(0 ,1)
sage: modadd_component.cp_deterministic_truncated_xor_differential_constraints()
(['array[0..15] of var 0..2: pre_modadd_0_1_0;',
  'array[0..15] of var 0..2: pre_modadd_0_1_1;'],
 ['constraint pre_modadd_0_1_0[0] = rot_0_0[0];',
   ...
  'constraint pre_modadd_0_1_1[15] = plaintext[31];',
  'constraint modular_addition_word(pre_modadd_0_1_1, pre_modadd_0_1_0, modadd_0_1);'])

cp_deterministic_truncated_xor_differential_trail_constraints()

cp_twoterms_xor_differential_probability(input_1, input_2, out, input_length, cp_constraints, cp_declarations, c, model)

cp_xor_differential_propagation_constraints(model)

Return lists of declarations and constraints for the probability of Modular Addition/Substraction component for CP xor differential probability.

INPUT:

• model – model object; a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.cp.cp_model import CpModel
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: cp = CpModel(speck)
sage: modadd_component = speck.component_from(0, 1)
sage: modadd_component.cp_xor_differential_propagation_constraints(cp)
(['array[0..15] of var 0..1: pre_modadd_0_1_0;',
  ...
  'array[0..15] of var 0..1: eq_modadd_0_1 = Eq(Shi_pre_modadd_0_1_1, Shi_pre_modadd_0_1_0, Shi_modadd_0_1);'],
 ['constraint pre_modadd_0_1_0[0] = rot_0_0[0];',
  ...
  'constraint pre_modadd_0_1_1[15] = plaintext[31];',
  'constraint forall(j in 0..15)(if eq_modadd_0_1[j] = 1 then (sum([pre_modadd_0_1_1[j], pre_modadd_0_1_0[j], modadd_0_1[j]]) mod 2) = Shi_pre_modadd_0_1_0[j] else true endif) /\\ p[0] = 1600-100 * sum(eq_modadd_0_1);'])

cp_xor_linear_mask_propagation_constraints(model)

Return lists of declarations and constraints for the probability of Modular Addition/Substraction for CP xor linear model.

INPUT:

• model – model object; a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.cp.cp_model import CpModel
sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=22)
sage: modadd_component = speck.component_from(0, 1)
sage: cp = CpModel(speck)
sage: modadd_component.cp_xor_linear_mask_propagation_constraints(cp)
(['array[0..31] of var 0..1: modadd_0_1_i;',
  'array[0..15] of var 0..1: modadd_0_1_o;',
  ...
  'constraint pre_modadd_0_1_1[15]=modadd_0_1_i[31];',
  'constraint modadd_linear(pre_modadd_0_1_1, pre_modadd_0_1_0, modadd_0_1_o, p[0]);'])

create_bct_mzn_constraint_from_component_ids()

property description

get_bit_based_vectorized_python_code(params, convert_output_to_bytes)

get_byte_based_vectorized_python_code(params)

get_graph_representation()

get_word_operation_sign(sign, solution)

property id

property input_bit_positions

property input_bit_size

property input_id_links

is_forbidden(forbidden_types, forbidden_descriptions)

is_id_equal_to(component_id)

is_power_of_2_word_based(dto)

milp_bitwise_deterministic_truncated_xor_differential_binary_constraints(model)

Returns a list of variables and a list of constraints for modular addition component in deterministic truncated XOR differential model.

INPUTS:

• component – dict, the modular addition component in Graph Representation

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: cipher = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2)
sage: from claasp.cipher_modules.models.milp.milp_models.milp_bitwise_deterministic_truncated_xor_differential_model import MilpBitwiseDeterministicTruncatedXorDifferentialModel
sage: milp = MilpBitwiseDeterministicTruncatedXorDifferentialModel(cipher)
sage: milp.init_model_in_sage_milp_class()
sage: modadd_component = cipher.get_component_from_id("modadd_0_1")
sage: variables, constraints = modadd_component.milp_bitwise_deterministic_truncated_xor_differential_binary_constraints(milp)
sage: variables
[('x[rot_0_0_0_class_bit_0]', x_0),
 ('x[rot_0_0_0_class_bit_1]', x_1),
...
 ('x[modadd_0_1_15_class_bit_0]', x_94),
 ('x[modadd_0_1_15_class_bit_1]', x_95)]
sage: constraints
[x_96 == 2*x_0 + x_1,
 x_97 == 2*x_2 + x_3,
...
 1 <= 18 - x_30 + x_94 - 17*x_159,
 1 <= 19 - x_62 - x_63 - 17*x_159]

milp_bitwise_deterministic_truncated_xor_differential_constraints(model)

Returns a list of variables and a list of constraints for modular addition component in deterministic truncated XOR differential model.

INPUTS:

• component – dict, the modular addition component in Graph Representation

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: cipher = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2)
sage: from claasp.cipher_modules.models.milp.milp_models.milp_bitwise_deterministic_truncated_xor_differential_model import MilpBitwiseDeterministicTruncatedXorDifferentialModel
sage: milp = MilpBitwiseDeterministicTruncatedXorDifferentialModel(cipher)
sage: milp.init_model_in_sage_milp_class()
sage: modadd_component = cipher.get_component_from_id("modadd_0_1")
sage: variables, constraints = modadd_component.milp_bitwise_deterministic_truncated_xor_differential_constraints(milp)
sage: constraints
[x_48 <= 16,
 0 <= x_48,
 0 <= 16 + x_48 - 17*x_49,
 x_48 - 17*x_49 <= 0,
 ...
 2 <= 4 + x_47 - 4*x_157 + 4*x_160,
 x_157 <= x_15 + x_31]
 sage: len(constraints)
 430

milp_xor_differential_propagation_constraints(model)

Return a list of variables and a list of constrains modeling a component of type MODADD/MODSUB for MILP xor differential probability.

The constraints are extracted from [FWGSH2016].

INPUT:

• model – model object; a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.milp.milp_model import MilpModel
sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2)
sage: modadd_component = speck.component_from(0, 1)
sage: milp = MilpModel(speck)
sage: milp.init_model_in_sage_milp_class()
sage: variables, constraints = modadd_component.milp_xor_differential_propagation_constraints(milp)
sage: variables
[('x[rot_0_0_0]', x_0),
('x[rot_0_0_1]', x_1),
...
('x[modadd_0_1_14]', x_46),
('x[modadd_0_1_15]', x_47)]
sage: constraints
[x_47 <= x_48,
x_15 <= x_48,
...
-2 <= -1*x_0 - x_16 - x_17 + x_32 + x_63,
x_64 == 100*x_49 + 100*x_50 + 100*x_51 + 100*x_52 + 100*x_53 + 100*x_54 + 100*x_55 + 100*x_56 + 100*x_57 + 100*x_58 + 100*x_59 + 100*x_60 + 100*x_61 + 100*x_62 + 100*x_63]

milp_xor_linear_mask_propagation_constraints(model)

Return lists of variables and constraints for probability of Modular Addition/Substraction for MILP xor linear model, for any arbitrary number of inputs.

INPUT:

• model – model object; a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.milp.milp_model import MilpModel
sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2)
sage: milp = MilpModel(speck)
sage: milp.init_model_in_sage_milp_class()
sage: modadd_component = speck.component_from(0, 1)
sage: variables, constraints = modadd_component.milp_xor_linear_mask_propagation_constraints(milp)
sage: variables
[('x[modadd_0_1_0_i]', x_0),
 ('x[modadd_0_1_1_i]', x_1),
...
 ('x[modadd_0_1_14_o]', x_46),
 ('x[modadd_0_1_15_o]', x_47)]
sage: constraints
[x_48 == 0,
0 <= -1*x_0 - x_16 + x_32 + x_48 + x_49,
0 <= x_0 + x_16 - x_32 + x_48 - x_49,
...
 -4 <= x_15 + x_31 + x_47 + x_63 + x_64,
 x_65 == x_48 + x_49 + x_50 + x_51 + x_52 + x_53 + x_54 + x_55 + x_56 + x_57 + x_58 + x_59 + x_60 + x_61 + x_62 + x_63,
 x_66 == 100*x_65]

minizinc_xor_differential_propagation_constraints(model)

Return variables and constraints for the component Modular Addition/Substraction for MINIZINC xor differential probability.

INPUT:

• model – model object; a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.fancy_block_cipher import FancyBlockCipher
sage: from claasp.cipher_modules.models.minizinc.minizinc_models.minizinc_xor_differential_model import MinizincXorDifferentialModel
sage: fancy = FancyBlockCipher(number_of_rounds=2)
sage: minizinc = MinizincXorDifferentialModel(fancy, sat_or_milp="milp")
sage: modadd_component = fancy.component_from(1, 9)
sage: _, constraints = modadd_component.minizinc_xor_differential_propagation_constraints(minizinc)
sage: constraints[6]
'constraint modular_addition_word(array1d(0..6-1, [modadd_1_9_x0,modadd_1_9_x1,modadd_1_9_x2,modadd_1_9_x3,modadd_1_9_x4,modadd_1_9_x5]),array1d(0..6-1, [modadd_1_9_x6,modadd_1_9_x7,modadd_1_9_x8,modadd_1_9_x9,modadd_1_9_x10,modadd_1_9_x11]),array1d(0..6-1, [modadd_1_9_y0_0,modadd_1_9_y1_0,modadd_1_9_y2_0,modadd_1_9_y3_0,modadd_1_9_y4_0,modadd_1_9_y5_0]), p_modadd_1_9_0, dummy_modadd_1_9_0, -1)=1;\n'

property output_bit_size

output_size_for_concatenate(available_word_sizes, fixed, word_size)

print()

print_as_python_dictionary()

print_values(code)

print_word_values(code)

sat_bitwise_deterministic_truncated_xor_differential_constraints()

Return a list of variables and a list of clauses for Modular Addition in DETERMINISTIC TRUNCATED XOR DIFFERENTIAL model.

See also

SAT standard of Cipher for the format.

INPUT:

• None

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: modadd_component = speck.component_from(0, 1)
sage: modadd_component.sat_bitwise_deterministic_truncated_xor_differential_constraints()
(['modadd_0_1_0_0',
  'modadd_0_1_1_0',
  'modadd_0_1_2_0',
  ...
  'rot_0_0_15_0 plaintext_31_0 -rot_0_0_15_1 -modadd_0_1_15_0',
  'rot_0_0_15_0 plaintext_31_0 -plaintext_31_1 -modadd_0_1_15_0',
  'modadd_0_1_15_0 -rot_0_0_15_1 -plaintext_31_1 -modadd_0_1_15_1'])

sat_constraints()

Return a list of variables and a list of clauses for Modular Subtraction in SAT CIPHER model.

See also

SAT standard of Cipher for the format.

Warning

This method heavily relies on the fact that modular subtraction is always performed using two operands.

INPUT:

• None

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.raiden_block_cipher import RaidenBlockCipher
sage: raiden = RaidenBlockCipher(number_of_rounds=3)
sage: modsub_component = raiden.component_from(0, 7)
sage: modsub_component.sat_constraints()
(['temp_carry_plaintext_32',
  'temp_carry_plaintext_33',
  'temp_carry_plaintext_34',
  ...
  'modsub_0_7_31 -modadd_0_4_31 temp_input_plaintext_63',
  'modsub_0_7_31 modadd_0_4_31 -temp_input_plaintext_63',
  '-modsub_0_7_31 -modadd_0_4_31 -temp_input_plaintext_63'])

sat_xor_differential_propagation_constraints(model)

Return a list of variables and a list of clauses for Modular Addition/Substraction in SAT XOR DIFFERENTIAL model.

See also

SAT standard of Cipher for the format, [LM2001] for the algorithm.

Warning

This method heavily relies on the fact that modular addition is always performed using two addenda.

INPUT:

• model – model object; a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.sat.sat_model import SatModel
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatModel(speck)
sage: modadd_component = speck.component_from(0, 1)
sage: modadd_component.sat_xor_differential_propagation_constraints(sat)
(['modadd_0_1_0',
  'modadd_0_1_1',
  'modadd_0_1_2',
  ...
  'modadd_0_1_15 -rot_0_0_15 plaintext_31',
  'modadd_0_1_15 rot_0_0_15 -plaintext_31',
  '-modadd_0_1_15 -rot_0_0_15 -plaintext_31'])

sat_xor_linear_mask_propagation_constraints(model=None)

Return a list of variables and a list of clauses for fixing variables in SAT XOR LINEAR model.

See also

SAT standard of Cipher for the format, [LWR2016] for the algorithm.

Warning

This method heavily relies on the fact that modular addition is always performed using two addenda.

INPUT:

• model – model object (default: None); a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: modadd_component = speck.component_from(0, 1)
sage: modadd_component.sat_xor_linear_mask_propagation_constraints()
(['modadd_0_1_0_i',
  'modadd_0_1_1_i',
  'modadd_0_1_2_i',
  ...
  'hw_modadd_0_1_14_o -modadd_0_1_14_o modadd_0_1_30_i',
  'hw_modadd_0_1_15_o modadd_0_1_15_o -modadd_0_1_31_i',
  'hw_modadd_0_1_15_o -modadd_0_1_15_o modadd_0_1_31_i'])

select_bits(code)

select_words(code, word_size, input=True)

set_description(description)

set_id(id_string)

set_input_bit_positions(bit_positions)

set_input_id_links(input_id_links)

smt_constraints()

Return a variable list and SMT-LIB list asserts for Modular Subtraction in SMT CIPHER model.

Warning

This method heavily relies on the fact that modular subtraction is always performed using two operands.

INPUT:

• None

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.raiden_block_cipher import RaidenBlockCipher
sage: raiden = RaidenBlockCipher(number_of_rounds=3)
sage: modsub_component = raiden.component_from(0, 7)
sage: modsub_component.smt_constraints()
(['temp_carry_plaintext_32',
  'temp_carry_plaintext_33',
  ...
  'modsub_0_7_30',
  'modsub_0_7_31'],
 ['(assert (= temp_carry_plaintext_32 (and (not plaintext_33) temp_carry_plaintext_33)))',
  '(assert (= temp_carry_plaintext_33 (and (not plaintext_34) temp_carry_plaintext_34)))',
  ...
  '(assert (= modsub_0_7_30 (xor modadd_0_4_30 temp_input_plaintext_62 carry_modsub_0_7_30)))',
  '(assert (= modsub_0_7_31 (xor modadd_0_4_31 temp_input_plaintext_63)))'])

smt_xor_differential_propagation_constraints(model=None)

Return a variable list and SMT-LIB list asserts for Modular Addition/Substraction in SMT XOR DIFFERENTIAL model [LM2001].

Warning

This method heavily relies on the fact that modular addition is always performed using two addenda.

INPUT:

• model – model object (default: None); a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.tea_block_cipher import TeaBlockCipher
sage: tea = TeaBlockCipher(number_of_rounds=3)
sage: modadd_component = tea.component_from(0, 1)
sage: modadd_component.smt_xor_differential_propagation_constraints()
(['modadd_0_1_0',
  'modadd_0_1_1',
  ...
  'hw_modadd_0_1_30',
  'hw_modadd_0_1_31'],
 ['(assert (= (not hw_modadd_0_1_0) (= shift_0_0_1 key_1 modadd_0_1_1)))',
  '(assert (= (not hw_modadd_0_1_1) (= shift_0_0_2 key_2 modadd_0_1_2)))',
  ...
  '(assert (or hw_modadd_0_1_29 (not (xor shift_0_0_29 key_29 modadd_0_1_29 key_30))))',
  '(assert (or hw_modadd_0_1_30 (not (xor shift_0_0_30 key_30 modadd_0_1_30 key_31))))',
  '(assert (not (xor modadd_0_1_31 shift_0_0_31 key_31)))'])

smt_xor_linear_mask_propagation_constraints(model=None)

Return a variable list and SMT-LIB list asserts for Modular Addition/Substraction in SMT XOR LINEAR model [LWR2016].

Warning

This method heavily relies on the fact that modular addition is always performed using two addenda.

INPUT:

• model – model object (default: None); a model instance

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.tea_block_cipher import TeaBlockCipher
sage: tea = TeaBlockCipher(number_of_rounds=3)
sage: modadd_component = tea.component_from(0, 1)
sage: modadd_component.smt_xor_linear_mask_propagation_constraints()
(['modadd_0_1_0_i',
  'modadd_0_1_1_i',
  ...
  'hw_modadd_0_1_30_o',
  'hw_modadd_0_1_31_o'],
 ['(assert (not hw_modadd_0_1_0_o))',
  '(assert (= hw_modadd_0_1_1_o (xor modadd_0_1_0_o modadd_0_1_0_i modadd_0_1_32_i)))',
  '(assert (= hw_modadd_0_1_2_o (xor hw_modadd_0_1_1_o modadd_0_1_1_o modadd_0_1_1_i modadd_0_1_33_i)))',
  ...
  '(assert (=> (xor modadd_0_1_30_o modadd_0_1_62_i) hw_modadd_0_1_30_o))',
  '(assert (=> (xor modadd_0_1_31_o modadd_0_1_63_i) hw_modadd_0_1_31_o))'])

property suffixes

twoterms_milp_probability_xor_linear_constraints(binary_variable, integer_variable, input_vars, output_vars, chunk_number)

Return lists of variables and constraints for the probability of Modular Addition/Substraction for two inputs MILP xor linear model.

Note

Using the 8 inequalities as described in Fu2016 https://eprint.iacr.org/2016/407.pdf

https://github.com/fukai6/milp_speck/blob/master/speck_diff_find.py

INPUT:

• binary_variable – boolean MIPVariable

• integer_variable – integer MIPVariable

• input_vars – list

• output_vars – list

• chunk_number – integer

property type

cp_twoterms(input_1, input_2, out, component_name, input_length, cp_constraints, cp_declarations)