cascada.abstractproperty.opmodel module

Manipulate property models of bit-vector operations (w.r.t an abstract property).

`InvalidOpModelError`	Raised when the OpModel is not valid and a valid one was expected.
`OpModel`	Represent property models of bit-vector operations.
`PartialOpModel`	Represent property models of operations with fixed operands.
`make_partial_op_model`	Return the partial property model of the given bit-vector partial operation.
`ModelIdentity`	Represent the (trivial) property model of the identity function.
`WeakModel`	Represent weak models of bit-vector operations w.r.t some property.
`BranchNumberModel`	Represent property models of bit-vector operations based on the branch number.
`WDTModel`	Represent WDT-based models of bit-vector operations w.r.t some property.

exception cascada.abstractproperty.opmodel.InvalidOpModelError[source]

Bases: Exception

Raised when the OpModel is not valid and a valid one was expected.

class cascada.abstractproperty.opmodel.OpModel(input_prop)[source]

Bases: object

Represent property models of bit-vector operations.

A (bit-vector) property model of a bit-vector Operation \(f\) for a particular Property is a set of bit-vector constraints that models the propagation probability of Property over \(f\). See Property.

Note

For the Value and Difference Property types, the propagation probability satisfies that for any fixed \(\alpha\), the sum of the probabilities of \(\alpha\) propagating to \(\beta\) (for all \(\beta\)) is equal to 1. In particular, if the propagation probability of \((\alpha, \beta)\) is 1, then \(\alpha\) uniquely propagates to \(\beta\).

For the LinearMask property this is different (see linear.opmodel.OpModel).

A model of \(f\) is mainly given by three bit-vector formulas or constraints: the validity_constraint constraint, the weight_constraint and the pr_one_constraint:

The validity constraint (with inputs \((\alpha, \beta)\)) is True if and only if the propagation probability of \((\alpha, \beta)\) is non-zero, that is, \(P(\alpha, \beta) \neq 0\).
The weight constraint (with inputs \((w, \alpha, \beta)\) is True if and only if the bit-vector \(w\) is equals to the negative binary logarithm (weight) of the propagation probability of \((\alpha, \beta)\), that is, \(w = -log_2(P(\alpha, \beta)))\).
The probability-one constraint (with inputs \((\alpha, \beta)\)) is True if and only if the propagation probability of \((\alpha, \beta)\) is 1.

Note

The weight constraint is only defined for inputs \((w, \alpha, \beta)\) where the propagation probability of \((\alpha, \beta)\) is non-zero.

By default, the \(n_w\)-bit input Variable \(w\) of the weight constraint is interpreted as the non-negative integer \(w[0] + 2 w[1] + \dots + 2^{n_w−1} w[n_w − 1]\). However, since the propagation weight can be a non-integer value for some properties and functions, \(w\) can also be interpreted as the rational value \(2^{−l}(w[0] + 2w[1] + \dots + 2^{n_w−1} w[n_w − 1]\) for a given fixed number \(l\) (num_frac_bits) of fractional bits.

Moreover, weight constraints can also be True if \(w\) is equals to weight of the propagation probability up to some error bounded by error.

An OpModel is defined for a type of Property and a bit-vector Operation \(f\) . The input property \(\alpha\) is used when initializing the OpModel object, and the output property \(\beta\) is given in the arguments of the methods OpModel.validity_constraint, OpModel.weight_constraint and OpModel.pr_one_constraint (among others).

In some cases, the validity, weight or probability-one constraints use auxiliary external (different from the input and output properties) variables in the bit-vector expression. These external variables can be obtained from external_vars_validity_constraint, external_vars_weight_constraint and external_vars_pr_one_constraint respectively.

Note

OpModel of functions with scalar operands are not supported.

This class is not meant to be instantiated but to provide a base class for creating models of some operation w.r.t some property, (see XorModelBvAdd, LinearModelBvAdd or BitModelBvAdd for some examples).

Note

It is highly recommended that new models of bit-vector operations are tested with TestOpModelGeneric (see differential/tests/test_opmodel.py or linear/tests/test_opmodel.py for some examples).

prop_type: the particular Property type

op: the bit-vector Operation \(f\)

input_prop: a list containing the Property associated to each bit-vector operand.

vrepr()[source]

Return an executable string representation.

This method returns a string so that eval(self.vrepr()) and self have the same content.

validity_constraint(output_prop)[source]

Return the validity constraint for a given output Property.

The validity constraint is a bit-vector expression that depends on the input property OpModel.input_prop and the output property output_prop and it is True if and only if the input property propagates to the output property with non-zero probability.

If both the input and output properties are constant values, this method returns the Constant 0b1 or 0b0 depending on whether the corresponding propagation has non-zero probability. Otherwise, this method returns a bit-vector Term containing the input and output properties as Variable objects.

pr_one_constraint(output_prop)[source]

Return the probability-one constraint for a given output Property.

Return the constraint that evaluates to True if the input Property propagates to the given output Property with probability one.

This method returns a bit-vector expression that depends on the input property OpModel.input_prop and the output property output_prop and it is True if and only if the input property propagates to the output property with probability 1.

If both the input and output properties are constant values, this method returns the Constant 0b1 or 0b0 depending on whether the corresponding propagation has probability 1. Otherwise, this method returns a bit-vector Term containing the input and output properties as Variable objects.

weight_constraint(output_prop, weight_variable)[source]

Return the weight constraint for a given output Property and weight Variable.

The weight constraint is a bit-vector expression that depends on the input property OpModel.input_prop, the output property output_prop and the weight variable weight_variable. This expression is True if and only if the weight (negative binary logarithm of the probability) of the input property propagating to the output property is equals to weight_variable.

Note

It is assumed that the corresponding propagation has non-zero probability.

If the input and output properties and the weight variable are constant values, this method returns the Constant 0b1 or 0b0 depending on whether the corresponding propagation has the given weight. Otherwise, this method returns a bit-vector Term containing the input and output properties and the weight as Variable objects.

Subclasses can either reimplement this method or implement the method bv_weight. In the last case, the weight constraint is defined as BvComp(weight_variable, self.bv_weight(output_prop)).

bv_weight(output_prop)[source]

Return the bit-vector weight for a given output Property.

The bit-vector weight is a bit-vector expression that depends on the input property OpModel.input_prop and the output property output_prop. This bit-vector function represents an approximation of the negative binary logarithm (weight) of the probability of the input property propagating to the output property.

Note

This method is optional and subclasses of OpModel don’t need to implement it (as opposed to OpModel.weight_constraint).

It is assumed that the corresponding propagation has non-zero probability.

If the input and output properties are constant values, this method returns a Constant of bit-size weight_width denoting the weight of the valid propagation. Otherwise, this method returns a bit-vector Term containing the input and output properties as Variable objects.

max_weight()[source]: Return the maximum value the weight variable can achieve in OpModel.weight_constraint.

weight_width()[source]: Return the width of the weight variable used OpModel.weight_constraint.

decimal_weight(output_prop)[source]

Return the decimal.Decimal weight for a given constant output Property.

This method returns, as a decimal number, the weight (negative binary logarithm) of the probability of the input property propagating to the output property.

This method only works when the input property and the output property are constant values, but provides a better approximation than the bit-vector weight from OpModel.weight_constraint.

num_frac_bits()[source]

Return the number of fractional bits used in the weight variable of OpModel.weight_constraint.

If the number of fractional bits is k, then the bit-vector weight variable w of OpModel.weight_constraint represents the number 2^{-k} * bv2int(w). In particular, if k == 0, then w represents an integer number. Otherwise, the k least significant bits of w denote the fractional part of the number represented by w.

error()[source]

Return the maximum difference between OpModel.weight_constraint and the exact weight.

The exact weight is exact value (without error) of the negative binary logarithm (weight) of the propagation probability of \((\alpha, \beta)\).

Note

The exact weight can be computed in TestOpModelGeneric.get_empirical_weight_slow.

This method returns an upper bound (in absolute value) of the maximum difference (over all input and output properties) between the bit-vector weight from OpModel.weight_constraint and the exact weight.

Note that the exact weight might still differ from decimal_weight.

external_vars_validity_constraint(output_prop)[source]: Return the list of external variables of validity_constraint for a given output Property (an empty list by default).

external_vars_pr_one_constraint(output_prop)[source]: Return the list of external variables of pr_one_constraint for a given output Property (an empty list by default).

external_vars_weight_constraint(output_prop, weight_variable)[source]: Return the list of external variables of weight_constraint for a given output Property and weight Variable (an empty list by default).

class cascada.abstractproperty.opmodel.PartialOpModel[source]

Bases: object

Represent property models of operations with fixed operands.

This class is not meant to be instantiated but to provide a base class for property models of operations with fixed operands generated through make_partial_op_model.

base_op: a subclass of Operation denoting the base operator.

vrepr()[source]

Return an executable string representation.

This method returns a string so that eval(self.vrepr()) and self have the same content.

cascada.abstractproperty.opmodel.make_partial_op_model(abstract_partial_op_model, fixed_args)[source]

Return the partial property model of the given bit-vector partial operation.

The argument abstract_partial_op_model is an (abstract) subclass of PartialOpModel containing the base operator.

The argument fixed_args is a tuple, with the same length as the number of operands of the base operator, containing None, scalar or Constant elements. If fixed_args[i] is None, the i-th operand is not fixed; otherwise, the i-th operand is replaced with fixed_args[i]. See also make_partial_operation.

The resulting class is a subclass of abstract_partial_op_model.

class cascada.abstractproperty.opmodel.ModelIdentity(input_prop)[source]

Bases: cascada.abstractproperty.opmodel.OpModel

Represent the (trivial) property model of the identity function.

This model is used to rename a complex intermediate property with a new name.

op: alias of cascada.bitvector.operation.BvIdentity

validity_constraint(output_prop)[source]

Return the validity constraint for a given output Property.

The validity constraint is a bit-vector expression that depends on the input property OpModel.input_prop and the output property output_prop and it is True if and only if the input property propagates to the output property with non-zero probability.

If both the input and output properties are constant values, this method returns the Constant 0b1 or 0b0 depending on whether the corresponding propagation has non-zero probability. Otherwise, this method returns a bit-vector Term containing the input and output properties as Variable objects.

pr_one_constraint(output_prop)[source]

Return the probability-one constraint for a given output Property.

Return the constraint that evaluates to True if the input Property propagates to the given output Property with probability one.

This method returns a bit-vector expression that depends on the input property OpModel.input_prop and the output property output_prop and it is True if and only if the input property propagates to the output property with probability 1.

If both the input and output properties are constant values, this method returns the Constant 0b1 or 0b0 depending on whether the corresponding propagation has probability 1. Otherwise, this method returns a bit-vector Term containing the input and output properties as Variable objects.

bv_weight(output_prop)[source]

Return the bit-vector weight for a given output Property.

The bit-vector weight is a bit-vector expression that depends on the input property OpModel.input_prop and the output property output_prop. This bit-vector function represents an approximation of the negative binary logarithm (weight) of the probability of the input property propagating to the output property.

Note

This method is optional and subclasses of OpModel don’t need to implement it (as opposed to OpModel.weight_constraint).

It is assumed that the corresponding propagation has non-zero probability.

If the input and output properties are constant values, this method returns a Constant of bit-size weight_width denoting the weight of the valid propagation. Otherwise, this method returns a bit-vector Term containing the input and output properties as Variable objects.

max_weight()[source]: Return the maximum value the weight variable can achieve in OpModel.weight_constraint.

weight_width()[source]: Return the width of the weight variable used OpModel.weight_constraint.

decimal_weight(output_prop)[source]

Return the decimal.Decimal weight for a given constant output Property.

This method returns, as a decimal number, the weight (negative binary logarithm) of the probability of the input property propagating to the output property.

This method only works when the input property and the output property are constant values, but provides a better approximation than the bit-vector weight from OpModel.weight_constraint.

num_frac_bits()[source]

Return the number of fractional bits used in the weight variable of OpModel.weight_constraint.

If the number of fractional bits is k, then the bit-vector weight variable w of OpModel.weight_constraint represents the number 2^{-k} * bv2int(w). In particular, if k == 0, then w represents an integer number. Otherwise, the k least significant bits of w denote the fractional part of the number represented by w.

error()[source]

Return the maximum difference between OpModel.weight_constraint and the exact weight.

The exact weight is exact value (without error) of the negative binary logarithm (weight) of the propagation probability of \((\alpha, \beta)\).

Note

The exact weight can be computed in TestOpModelGeneric.get_empirical_weight_slow.

This method returns an upper bound (in absolute value) of the maximum difference (over all input and output properties) between the bit-vector weight from OpModel.weight_constraint and the exact weight.

Note that the exact weight might still differ from decimal_weight.

class cascada.abstractproperty.opmodel.WeakModel(input_prop)[source]

Bases: object

Represent weak models of bit-vector operations w.r.t some property.

A weak model is an OpModel where the propagation weight of a Property pair \((\alpha, \beta)\) is one of the following cases:

If \(\alpha = 0 = \beta\), the weight is zero2zero_weight.
If \(\alpha \neq 0 \neq \beta\), the weight is nonzero2nonzero_weight.
If \(\alpha = 0 \neq \beta\), the weight is zero2nonzero_weight.
If \(\alpha \neq 0 = \beta\), the weight is nonzero2zero_weight.

If any of weights zero2zero_weight, nonzero2nonzero_weight, zero2nonzero_weight or nonzero2zero_weight is math.inf, the propagation probability of the corresponding case is assumed to be 0.

This class is not meant to be instantiated but to provide a base class for weak models of operations (generated for example through differential.opmodel.get_weak_model or linear.opmodel.get_weak_model).

zero2zero_weight: a decimal.Decimal denoting the weight of the zero to zero transitions (math.inf if these transitions are invalid)

nonzero2nonzero_weight: a decimal.Decimal denoting the weight of the non-zero to non-zero transitions (math.inf if these transitions are invalid)

zero2nonzero_weight: a decimal.Decimal denoting the weight of the zero to non-zero transitions (math.inf if these transitions are invalid)

nonzero2zero_weight: a decimal.Decimal denoting the weight of the non-zero to zero transitions (math.inf if these transitions are invalid)

precision: the number of fraction bits used in the bit-vector weight (0 if all non-math.inf attributes *_weight are integer values)

class cascada.abstractproperty.opmodel.BranchNumberModel(input_prop)[source]

Bases: cascada.abstractproperty.opmodel.WeakModel

Represent property models of bit-vector operations based on the branch number.

Let \((y_0, y_1, \dots, y_m) = f(x_1, x_2, \dots, x_n)\) be a bit-vector function with input words \(x_i\) and output words \(y_j\). Given a property pair \(((P_{x_1}, \dots, P_{x_n}), (P_{y_1}, \dots, P_{y_n}))\) over \(f\), we say that the property \(P_{x_i}\) over \(x_i\) is active if \(P_{x_i} \neq 0\) (similar for \(P_{y_j}\)).

A BranchNumberModel of an Operation \(f\) is an OpModel where the propagation weight of a Property pair \((\alpha, \beta)\) is one of the four cases of WeakModel but with the additional constraint that if \((\alpha, \beta)\) is non-zero and its number of active words is strictly less than \(B\) then it is invalid.

The number \(B\) is usually the branch number of \(f\), that is, the minimum number of active words (at the input and at the output) among all non-zero property pairs. Nevertheless, any \(2 \le B \le n + m\) can be used.

Since an Operation outputs a single bit-vector, the class attribute output_widths of BranchNumberModel delimits the output words of \(f\) (for the counting of active output words).

Note

To extract the output words from an Operation with a BranchNumberModel, use PropExtract instead of Extract.

This class is not meant to be instantiated but to provide a base class for branch-number-based models of operations (generated for example through differential.opmodel.get_branch_number_model or linear.opmodel.get_branch_number_model).

output_widths: a tuple containing the widths of the output words

branch_number: the branch number \(B\)

zero2zero_weight: a decimal.Decimal denoting the weight of the zero to zero transitions (math.inf if all these transitions are invalid)

nonzero2nonzero_weight: a decimal.Decimal denoting the weight of the non-zero to non-zero transitions (math.inf if all these transitions are invalid)

zero2nonzero_weight: a decimal.Decimal denoting the weight of the zero to non-zero transitions (math.inf if all these transitions are invalid)

nonzero2zero_weight: a decimal.Decimal denoting the weight of the non-zero to zero transitions (math.inf if all these transitions are invalid)

precision: the number of fraction bits used in the bit-vector weight (0 if all non-math.inf attributes *_weight are integer values)

class cascada.abstractproperty.opmodel.WDTModel(input_prop)[source]

Bases: object

Represent WDT-based models of bit-vector operations w.r.t some property.

A model based on a Weight Distribution Table (WDT) is an OpModel where the propagation weight is obtained from a 2-dimensional table WDT such that WDT[a][b] contains the propagation weight of the input-output Property pair \((a, b)\).

Note

For the Difference (resp. LinearMask) property, the WDT is also known as the Difference Distribution Table or DDT (resp. Linear Approximation Table or LAT).

This class is not meant to be instantiated but to provide a base class for WDT-based models of operations (generated for example through differential.opmodel.get_wdt_model or linear.opmodel.get_wdt_model).

weight_distribution_table: a 2-dimensional tuple containing the distribution of the propagations weights, where math.inf entries correspond to invalid transitions

loop_rows_then_columns: whether to extract the constraints from weight_distribution_table by looping first over the rows (input properties) and then over the columns (output properties) or vice-versa

precision: the number of fraction bits used in the bit-vector weight (0 if all the weights in weight_distribution_table are integer values)