arxpy.smt.verification_impossible module

Verify impossible differentials found by the SMT solver.

arxpy.smt.verification_impossible.fast_empirical_weight(id_found, verbose_lvl=0, debug=False, filename=None)

Computes the empirical weight of the model using C code.

If filename is not None, the output will be printed to the given file rather than the to stdout.

The argument verbose_lvl can take an integer between 0 (no verbose) and 3 (full verbose).

>>> from arxpy.differential.difference import XorDiff, RXDiff
>>> from arxpy.differential.characteristic import BvCharacteristic
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> from arxpy.smt.search_impossible import SearchID
>>> from arxpy.smt.verification_impossible import fast_empirical_weight
>>> ChaskeyPi.set_rounds(2)
>>> ch = BvCharacteristic(ChaskeyPi, XorDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchID(ch)
>>> id_found = search_problem.solve(2)
>>> fast_empirical_weight(id_found)
inf
>>> ch = BvCharacteristic(ChaskeyPi, RXDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchID(ch)
>>> id_found = search_problem.solve(2)
>>> fast_empirical_weight(id_found)
inf