1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
| """ 用Z3解出v5的值 v4 = [0x00004F17, 0x00009CF6, 0x00008DDB, 0x00008EA6, 0x00006929, 0x00009911, 0x000040A2, 0x00002F3E, 0x000062B6, 0x00004B82, 0x0000486C, 0x00004002, 0x000052D7, 0x00002DEF, 0x000028DC, 0x0000640D, 0x0000528F, 0x0000613B, 0x00004781, 0x00006B17, 0x00003237, 0x00002A93, 0x0000615F, 0x000050BE, 0x0000598E, 0x00004656, 0x00005B31, 0x0000313A, 0x00003010, 0x000067FE, 0x00004D5F, 0x000058DB, 0x00003799, 0x000060A0, 0x00002750, 0x00003759, 0x00008953, 0x00007122, 0x000081F9, 0x00005524, 0x00008971, 0x00003A1D] """ from z3 import * v5 = [BitVec("v5_%d" % i, 8) for i in range(42)] v4 = [0x00004F17, 0x00009CF6, 0x00008DDB, 0x00008EA6, 0x00006929, 0x00009911, 0x000040A2, 0x00002F3E, 0x000062B6, 0x00004B82, 0x0000486C, 0x00004002, 0x000052D7, 0x00002DEF, 0x000028DC, 0x0000640D, 0x0000528F, 0x0000613B, 0x00004781, 0x00006B17, 0x00003237, 0x00002A93, 0x0000615F, 0x000050BE, 0x0000598E, 0x00004656, 0x00005B31, 0x0000313A, 0x00003010, 0x000067FE, 0x00004D5F, 0x000058DB, 0x00003799, 0x000060A0, 0x00002750, 0x00003759, 0x00008953, 0x00007122, 0x000081F9, 0x00005524, 0x00008971, 0x00003A1D] s = Solver() s.add(v4[0] == 34 * v5[3] + 12 * v5[0] + 53 * v5[1] + 6 * v5[2] + 58 * v5[4] + 36 * v5[5] + v5[6]) s.add(v4[1] == 27 * v5[4] + 73 * v5[3] + 12 * v5[2] + 83 * v5[0] + 85 * v5[1] + 96 * v5[5] + 52 * v5[6]) s.add(v4[2] == 24 * v5[2] + 78 * v5[0] + 53 * v5[1] + 36 * v5[3] + 86 * v5[4] + 25 * v5[5] + 46 * v5[6]) s.add(v4[3] == 78 * v5[1] + 39 * v5[0] + 52 * v5[2] + 9 * v5[3] + 62 * v5[4] + 37 * v5[5] + 84 * v5[6]) s.add(v4[4] == 48 * v5[4] + 14 * v5[2] + 23 * v5[0] + 6 * v5[1] + 74 * v5[3] + 12 * v5[5] + 83 * v5[6]) s.add(v4[5] == 15 * v5[5] + 48 * v5[4] + 92 * v5[2] + 85 * v5[1] + 27 * v5[0] + 42 * v5[3] + 72 * v5[6]) s.add(v4[6] == 26 * v5[5] + 67 * v5[3] + 6 * v5[1] + 4 * v5[0] + 3 * v5[2] + 68 * v5[6]) s.add(v4[7] == 34 * v5[10] + 12 * v5[7] + 53 * v5[8] + 6 * v5[9] + 58 * v5[11] + 36 * v5[12] + v5[13]) s.add(v4[8] == 27 * v5[11] + 73 * v5[10] + 12 * v5[9] + 83 * v5[7] + 85 * v5[8] + 96 * v5[12] + 52 * v5[13]) s.add(v4[9] == 24 * v5[9] + 78 * v5[7] + 53 * v5[8] + 36 * v5[10] + 86 * v5[11] + 25 * v5[12] + 46 * v5[13]) s.add(v4[10] == 78 * v5[8] + 39 * v5[7] + 52 * v5[9] + 9 * v5[10] + 62 * v5[11] + 37 * v5[12] + 84 * v5[13]) s.add(v4[11] == 48 * v5[11] + 14 * v5[9] + 23 * v5[7] + 6 * v5[8] + 74 * v5[10] + 12 * v5[12] + 83 * v5[13]) s.add(v4[12] == 15 * v5[12] + 48 * v5[11] + 92 * v5[9] + 85 * v5[8] + 27 * v5[7] + 42 * v5[10] + 72 * v5[13]) s.add(v4[13] == 26 * v5[12] + 67 * v5[10] + 6 * v5[8] + 4 * v5[7] + 3 * v5[9] + 68 * v5[13]) s.add(v4[14] == 34 * v5[17] + 12 * v5[14] + 53 * v5[15] + 6 * v5[16] + 58 * v5[18] + 36 * v5[19] + v5[20]) s.add(v4[15] == 27 * v5[18] + 73 * v5[17] + 12 * v5[16] + 83 * v5[14] + 85 * v5[15] + 96 * v5[19] + 52 * v5[20]) s.add(v4[16] == 24 * v5[16] + 78 * v5[14] + 53 * v5[15] + 36 * v5[17] + 86 * v5[18] + 25 * v5[19] + 46 * v5[20]) s.add(v4[17] == 78 * v5[15] + 39 * v5[14] + 52 * v5[16] + 9 * v5[17] + 62 * v5[18] + 37 * v5[19] + 84 * v5[20]) s.add(v4[18] == 48 * v5[18] + 14 * v5[16] + 23 * v5[14] + 6 * v5[15] + 74 * v5[17] + 12 * v5[19] + 83 * v5[20]) s.add(v4[19] == 15 * v5[19] + 48 * v5[18] + 92 * v5[16] + 85 * v5[15] + 27 * v5[14] + 42 * v5[17] + 72 * v5[20]) s.add(v4[20] == 26 * v5[19] + 67 * v5[17] + 6 * v5[15] + 4 * v5[14] + 3 * v5[16] + 68 * v5[20]) s.add(v4[21] == 34 * v5[24] + 12 * v5[21] + 53 * v5[22] + 6 * v5[23] + 58 * v5[25] + 36 * v5[26] + v5[27]) s.add(v4[22] == 27 * v5[25] + 73 * v5[24] + 12 * v5[23] + 83 * v5[21] + 85 * v5[22] + 96 * v5[26] + 52 * v5[27]) s.add(v4[23] == 24 * v5[23] + 78 * v5[21] + 53 * v5[22] + 36 * v5[24] + 86 * v5[25] + 25 * v5[26] + 46 * v5[27]) s.add(v4[24] == 78 * v5[22] + 39 * v5[21] + 52 * v5[23] + 9 * v5[24] + 62 * v5[25] + 37 * v5[26] + 84 * v5[27]) s.add(v4[25] == 48 * v5[25] + 14 * v5[23] + 23 * v5[21] + 6 * v5[22] + 74 * v5[24] + 12 * v5[26] + 83 * v5[27]) s.add(v4[26] == 15 * v5[26] + 48 * v5[25] + 92 * v5[23] + 85 * v5[22] + 27 * v5[21] + 42 * v5[24] + 72 * v5[27]) s.add(v4[27] == 26 * v5[26] + 67 * v5[24] + 6 * v5[22] + 4 * v5[21] + 3 * v5[23] + 68 * v5[27]) s.add(v4[28] == 34 * v5[31] + 12 * v5[28] + 53 * v5[29] + 6 * v5[30] + 58 * v5[32] + 36 * v5[33] + v5[34]) s.add(v4[29] == 27 * v5[32] + 73 * v5[31] + 12 * v5[30] + 83 * v5[28] + 85 * v5[29] + 96 * v5[33] + 52 * v5[34]) s.add(v4[30] == 24 * v5[30] + 78 * v5[28] + 53 * v5[29] + 36 * v5[31] + 86 * v5[32] + 25 * v5[33] + 46 * v5[34]) s.add(v4[31] == 78 * v5[29] + 39 * v5[28] + 52 * v5[30] + 9 * v5[31] + 62 * v5[32] + 37 * v5[33] + 84 * v5[34]) s.add(v4[32] == 48 * v5[32] + 14 * v5[30] + 23 * v5[28] + 6 * v5[29] + 74 * v5[31] + 12 * v5[33] + 83 * v5[34]) s.add(v4[33] == 15 * v5[33] + 48 * v5[32] + 92 * v5[30] + 85 * v5[29] + 27 * v5[28] + 42 * v5[31] + 72 * v5[34]) s.add(v4[34] == 26 * v5[33] + 67 * v5[31] + 6 * v5[29] + 4 * v5[28] + 3 * v5[30] + 68 * v5[34]) s.add(v4[35] == 34 * v5[38] + 12 * v5[35] + 53 * v5[36] + 6 * v5[37] + 58 * v5[39] + 36 * v5[40] + v5[41]) s.add(v4[36] == 27 * v5[39] + 73 * v5[38] + 12 * v5[37] + 83 * v5[35] + 85 * v5[36] + 96 * v5[40] + 52 * v5[41]) s.add(v4[37] == 24 * v5[37] + 78 * v5[35] + 53 * v5[36] + 36 * v5[38] + 86 * v5[39] + 25 * v5[40] + 46 * v5[41]) s.add(v4[38] == 78 * v5[36] + 39 * v5[35] + 52 * v5[37] + 9 * v5[38] + 62 * v5[39] + 37 * v5[40] + 84 * v5[41]) s.add(v4[39] == 48 * v5[39] + 14 * v5[37] + 23 * v5[35] + 6 * v5[36] + 74 * v5[38] + 12 * v5[40] + 83 * v5[41]) s.add(v4[40] == 15 * v5[40] + 48 * v5[39] + 92 * v5[37] + 85 * v5[36] + 27 * v5[35] + 42 * v5[38] + 72 * v5[41]) s.add(v4[41] == 26 * v5[40] + 67 * v5[38] + 6 * v5[36] + 4 * v5[35] + 3 * v5[37] + 68 * v5[41])
assert s.check() == sat m = s.model() print("".join([chr(m[v5[i]].as_long()) for i in range(42)]))
|