How to output the SSA form of a SMT problem ?

[Heawen]

Hi, your work is excellent. I'd like to learn how to find the best characteristic of a cipher by using the SMT solver. I want to read the SSA form of a SMT problem, but failed to output it.

[ranea]

If you set verbose_level to 3while calling one of the functions round_based_search_*, you can see in the output the SSA of the cipher (after Characteristic: [...] 'ssa': {...}) and a representation of the SMT problems (after SMT problem (size ...):).

For example:

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.smt.search import SkChSearchMode, DerMode, round_based_search_SkCh
>>> from arxpy.primitives import speck
>>> cipher = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> verbose_level = 3
>>> round_based_search_SkCh(cipher, XorDiff, 0, "btor", 1, 1, DerMode.Default, SkChSearchMode.FirstCh, False, verbose_level, None)

SpeckCipher Single-Key Search

[...]

Characteristic:
{[...]
 'ssa': {'assignments': ((dx0, dp0 >>> 7), (dx1, dp1 + dx0), (dx2, dx1 ^ k0), (dx3, dp1 <<< 2),
                         (dx4, dx2 ^ dx3)),
         'input_vars': (dp0, dp1),
         'output_vars': (dx2, dx4)}}

SMT problem (size 349):
assert ~(0x00000000 == (dp0 :: dp1))
assert 0x0000 == ((~(dp1 << 0x0001) ^ (dx1 << 0x0001)) & (~(dp1 << 0x0001) ^ ((dp0 >>> 7) << 0x0001)) & ((dp1 << 0x0001) ^ dx1 ^ dp1 ^ (dp0 >>> 7)))
assert w0 == PopCount(~((dx1 ^ ~dp1) & (~dp1 ^ (dp0 >>> 7)))[14:])
assert w == w0
minimize w

[...]

Although ArxPy shows a single SMT problem with minimize w, internally ArxPy creates several SMT problems and they do not contain minimize w (but these SMT problems share the assertions before the minimize w). Currently, ArxPy does not has a function to print in SMT-LIB2 all the SMT problems it creates.

[Heawen]

Thanks a lot