Utils

get_component_hex_value(component, out_suffix, variable2value)
smt_and(formulae)

Return a string representing the AND of formulae in SMT-LIB standard.

INPUT:

  • formulae – list; the formulae which are operands

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_and
sage: smt_and(['a', 'c', 'e'])
'(and a c e)'
smt_assert(formula)

Return a string representing assert in SMT-LIB standard.

INPUT:

  • formula – string; the formula that must be asserted

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_assert
sage: smt_assert('(= a b c)')
'(assert (= a b c))'
smt_carry(x, y, previous_carry)

Return a list of strings.

The list represents the Boolean equality carry = Or(And(x, y), And(x, previous_carry), And(y, previous_carry)) in SMT-LIB standard. It represents the general form of a carry when performing modular addition between two bitvectors.

INPUT:

  • x – string; the bit of the first addendum

  • y – string; the bit of the second addendum

  • previous_carry – string; the previous carry

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_carry
sage: smt_carry('x_3', 'y_3', 'c_2')
'(or (and x_3 y_3) (and x_3 c_2) (and y_3 c_2))'
smt_distinct(variable_0, variable_1)

Return a string representing the Boolean inequality in SMT-LIB standard.

INPUT:

  • variable_0 – string; the first variable

  • variable_1 – string; the second variable

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_distinct
sage: smt_distinct('a', 'q')
'(distinct a q)'
smt_equivalent(formulae)

Return a string representing the equivalence of formulae in SMT-LIB standard.

INPUT:

  • formulae – list; the formulae that must be equivalent

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_equivalent
sage: smt_equivalent(['a', 'b', 'c', 'd'])
'(= a b c d)'
smt_implies(antecedent, consequent)

Return a string representing the implication in SMT-LIB standard.

INPUT:

  • antecedent – string; the formula that is the antecedent

  • consequent – string; the formula that is the consequent

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_implies
sage: smt_implies('(and a c)', '(or l f)')
'(=> (and a c) (or l f))'
smt_ite(condition, consequent, alternative)

Return a string representing the if-then-else in SMT-LIB standard.

INPUT:

  • condition – string; the formula that is the condition

  • consequent – string; the formula that is the consequent

  • antecedent – string; the formula that is the antecedent

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_ite
sage: smt_ite('t', '(and a b)', '(and a e)')
'(ite t (and a b) (and a e))'
smt_lipmaa(hw, alpha, beta, gamma, beta_1)

Return a string representing the Lipmaa-Moriai algorithm in SMT-LIB standard.

INPUT:

  • hw – string; the variable for the Hamming weight bit

  • alpha – string; the bit in the first mask

  • beta – string; the bit in the second mask

  • gamma – string; the bit in the result mask

  • beta_1 – string; the next bit in the second mask

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_lipmaa
sage: smt_lipmaa('hw', 'alpha', 'beta', 'gamma', 'beta_1')
'(or hw (not (xor alpha beta gamma beta_1)))'
smt_not(formula)

Return a string representing the negation of the formula in SMT-LIB standard.

INPUT:

  • formula – string; the formula that must be negated

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_not
sage: smt_not('(xor a e)')
'(not (xor a e))'
smt_or(formulae)

Return a string representing the OR of formulae in SMT-LIB standard.

INPUT:

  • formulae – list of str; the formulae which are operands

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_or
sage: smt_or(['b', 'd', 'f'])
'(or b d f)'
smt_xor(formulae)

Return a string representing the XOR of formulae in SMT-LIB standard.

INPUT:

  • formulae – list of str; the formulae which are operands

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.utils.utils import smt_xor
sage: smt_xor(['b', 'd', 'f'])
'(xor b d f)'