rev_math.py

from z3 import *

text = [BitVec('text[%d]' % i, 8) for i in range(16)]
table = [4294498155L, 408514L, 428986L, 103869L, 466565L, 648745L, 122207L, 398062L, 723048L, 288564L, 548719L, 397546L, 4294549784L, 847445L, 618037L, 131763L, 555250L, 4294437458L, 416969L, 663660L, 391591L, 471484L, 718531L, 435812L, 370454L, 635503L, 421950L, 4294390916L, 952879L, 517643L, 887909L, 338372L, 742509L, 233247L, 4294708702L, 125426L, 781993L, 280801L, 339841L, 421393L, 385718L, 4294178736L, 718939L, 703230L, 552358L, 253329L, 651345L, 107608L, 599519L, 968314L, 587620L, 4294076186L, 439798L, 306151L, 326922L, 4294340692L, 841654L, 648872L, 119336L, 710885L, 982867L, 907246L, 949258L, 641728L, 956845L, 124204L, 667155L, 655190L, 4294745939L, 823348L, 976584L, 507075L, 4294439036L, 611875L, 126657L, 980618L, 765204L, 594354L, 904578L, 364723L, 479020L, 492198L, 172185L, 735171L, 614702L, 4294651837L, 361775L, 372708L, 780683L, 381112L, 983594L, 763550L, 204710L, 849204L, 321631L, 977907L, 873408L, 805138L, 633098L, 994765L, 628486L, 609682L, 4294549103L, 156746L, 137909L, 444850L, 953717L, 803114L, 855557L, 774647L, 984189L, 334577L, 183198L, 972727L, 4293997548L, 697900L, 288186L, 331524L, 970608L, 4293998426L, 528988L, 870554L, 648772L, 550050L, 636110L, 870403L, 444309L, 425870L, 675541L, 977407L, 420636L, 220379L, 503441L, 655181L, 193478L, 541351L, 4294867265L, 147195L, 260817L, 4294111708L, 738194L, 161358L, 4294777130L, 821392L, 134085L, 976266L, 519292L, 322272L, 4294743154L, 406253L, 291142L, 569482L, 193159L, 4294211030L, 119532L, 729270L, 626670L, 380194L, 4293995804L, 218563L, 357601L, 392128L, 338943L, 761043L, 947309L, 432421L, 218746L, 863693L, 395968L, 379563L, 4294331663L, 134162L, 4294526375L, 642151L, 855555L, 475007L, 618418L, 291199L, 613631L, 4294224736L, 513804L, 721125L, 312043L, 606964L, 477391L, 247927L, 252586L, 4294046883L, 528121L, 224078L, 138977L, 785723L, 432559L, 377920L, 463118L, 296220L, 710341L, 4294385432L, 159913L, 922661L, 777779L, 611899L, 956823L, 218700L, 4294713246L, 728730L, 510059L, 772468L, 919930L, 123690L, 431381L, 433734L, 4294306129L, 643424L, 857050L, 138559L, 707703L, 109636L, 958972L, 235825L, 150067L, 4294052995L, 837900L, 482626L, 292221L, 301018L, 4294288450L, 818914L, 699234L, 655112L, 4294225721L, 477013L, 267011L, 614751L, 512065L, 337413L, 343481L, 838477L, 4294041062L, 179763L, 778519L, 357615L, 513498L, 439687L, 817391L, 370548L, 4294489050L, 525094L, 296537L, 353570L, 660919L, 346604L, 267872L, 415171L, 645582L, 4294590851L]
array = map(lambda x: int(x.split(' ')[-1][:-1], 16), '''mov     [esp+4ACh+array], 1BA83922h
mov     [esp+4ACh+array+4], 220931E9h
mov     [esp+4ACh+array+8], 1FC925BEh
mov     [esp+4ACh+array+0Ch], 22371D94h
mov     [esp+4ACh+array+10h], 2902F5B6h
mov     [esp+4ACh+array+14h], 2BE60C89h
mov     [esp+4ACh+array+18h], 2ECF0F66h
mov     [esp+4ACh+array+1Ch], 21B0EA76h
mov     [esp+4ACh+array+20h], 13182B7Eh
mov     [esp+4ACh+array+24h], 1041F4B8h
mov     [esp+4ACh+array+28h], 2072953Dh
mov     [esp+4ACh+array+2Ch], 1228F22Fh
mov     [esp+4ACh+array+30h], 268F1E8Ch
mov     [esp+4ACh+array+34h], 1B82A0B0h
mov     [esp+4ACh+array+38h], 13591824h
mov     [esp+4ACh+array+3Ch], 1FACD5C7h'''.split('\n'))

s = Solver()
for i in range(16):
	s.add(reduce(lambda x, y: x + y, [text[j] * table[16 * i + j] for j in range(16)], 0) == array[i])

if s.check() == sat:
	model = s.model()
	text = [model[text[i]].as_long() for i in range(16)]
	text = bytearray(text)
	print `text`