Skip to content

Instantly share code, notes, and snippets.

@key-moon

key-moon/sol.py Secret

Created December 12, 2021 15:43
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save key-moon/e04d05b8cf2c84687f2fee665769f43a to your computer and use it in GitHub Desktop.
Save key-moon/e04d05b8cf2c84687f2fee665769f43a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
sol.py
w2c_g0 = 0x200
memory = [0] * 0x1000
def i32_store(mem, ind, val):
mem[ind] = val
def i32_load(mem, ind):
return mem[ind]
def i32_store8(mem, ind, val):
mem[ind] = val & 255
def i32_load8_u(mem, ind):
return mem[ind] & 255
def f23(w2c_p0, w2c_p1, w2c_p2, w2c_p3, w2c_p4):
w2c_i0 = w2c_g0;
w2c_l5 = w2c_i0;
w2c_i0 = 32;
w2c_l6 = w2c_i0;
w2c_i0 = w2c_l5;
w2c_i1 = w2c_l6;
w2c_i0 -= w2c_i1;
w2c_l7 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i1 = w2c_p0;
i32_store((memory), (w2c_i0) + 28, w2c_i1);
w2c_i0 = w2c_l7;
w2c_i1 = w2c_p1;
i32_store((memory), (w2c_i0) + 24, w2c_i1);
w2c_i0 = w2c_l7;
w2c_i1 = w2c_p2;
i32_store((memory), (w2c_i0) + 20, w2c_i1);
w2c_i0 = w2c_l7;
w2c_i1 = w2c_p3;
i32_store((memory), (w2c_i0) + 16, w2c_i1);
w2c_i0 = w2c_l7;
w2c_i1 = w2c_p4;
i32_store((memory), (w2c_i0) + 12, w2c_i1);
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l8 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 24);
w2c_l9 = w2c_i0;
w2c_i0 = w2c_l8;
w2c_i1 = w2c_l9;
w2c_i0 += w2c_i1;
w2c_i0 = w2c_p0
w2c_l10 = w2c_i0;
w2c_i0 = w2c_l10;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l11 = w2c_i0;
w2c_i0 = 255;
w2c_l12 = w2c_i0;
w2c_i0 = w2c_l11;
w2c_i1 = w2c_l12;
w2c_i0 &= w2c_i1;
w2c_l13 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l14 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 12);
w2c_l15 = w2c_i0;
w2c_i0 = w2c_l14;
w2c_i1 = w2c_l15;
w2c_i0 += w2c_i1;
w2c_l16 = w2c_i0;
w2c_i0 = w2c_l16;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l17 = w2c_i0;
w2c_i0 = 255;
w2c_l18 = w2c_i0;
w2c_i0 = w2c_l17;
w2c_i1 = w2c_l18;
w2c_i0 &= w2c_i1;
w2c_l19 = w2c_i0;
w2c_i0 = w2c_l13;
w2c_i1 = w2c_l19;
w2c_i0 += w2c_i1;
w2c_l20 = w2c_i0;
w2c_i0 = 255;
w2c_l21 = w2c_i0;
w2c_i0 = w2c_l20;
w2c_i1 = w2c_l21;
w2c_i0 &= w2c_i1;
w2c_l22 = w2c_i0;
w2c_i0 = 1;
w2c_l23 = w2c_i0;
w2c_i0 = w2c_l22;
w2c_i1 = w2c_l23;
w2c_i0 <<= (w2c_i1 & 31);
w2c_l24 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l25 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 24);
w2c_l26 = w2c_i0;
w2c_i0 = w2c_l25;
w2c_i1 = w2c_l26;
w2c_i0 += w2c_i1;
w2c_l27 = w2c_i0;
w2c_i0 = w2c_l27;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l28 = w2c_i0;
w2c_i0 = 255;
w2c_l29 = w2c_i0;
w2c_i0 = w2c_l28;
w2c_i1 = w2c_l29;
w2c_i0 &= w2c_i1;
w2c_l30 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l31 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 12);
w2c_l32 = w2c_i0;
w2c_i0 = w2c_l31;
w2c_i1 = w2c_l32;
w2c_i0 += w2c_i1;
w2c_l33 = w2c_i0;
w2c_i0 = w2c_l33;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l34 = w2c_i0;
w2c_i0 = 255;
w2c_l35 = w2c_i0;
w2c_i0 = w2c_l34;
w2c_i1 = w2c_l35;
w2c_i0 &= w2c_i1;
w2c_l36 = w2c_i0;
w2c_i0 = w2c_l30;
w2c_i1 = w2c_l36;
w2c_i0 += w2c_i1;
w2c_l37 = w2c_i0;
w2c_i0 = 255;
w2c_l38 = w2c_i0;
w2c_i0 = w2c_l37;
w2c_i1 = w2c_l38;
w2c_i0 &= w2c_i1;
w2c_l39 = w2c_i0;
w2c_i0 = 7;
w2c_l40 = w2c_i0;
w2c_i0 = w2c_l39;
w2c_i1 = w2c_l40;
w2c_i0 = (w2c_i0 >> (w2c_i1 & 31));
w2c_l41 = w2c_i0;
w2c_i0 = w2c_l24;
w2c_i1 = w2c_l41;
w2c_i0 |= w2c_i1;
w2c_l42 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l43 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 20);
w2c_l44 = w2c_i0;
w2c_i0 = w2c_l43;
w2c_i1 = w2c_l44;
w2c_i0 += w2c_i1;
w2c_l45 = w2c_i0;
w2c_i0 = w2c_l45;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l46 = w2c_i0;
w2c_i0 = 255;
w2c_l47 = w2c_i0;
w2c_i0 = w2c_l46;
w2c_i1 = w2c_l47;
w2c_i0 &= w2c_i1;
w2c_l48 = w2c_i0;
w2c_i0 = w2c_l48;
w2c_i1 = w2c_l42;
w2c_i0 ^= w2c_i1;
w2c_l49 = w2c_i0;
w2c_i0 = w2c_l45;
w2c_i1 = w2c_l49;
i32_store8((memory), (w2c_i0), w2c_i1);
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l50 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 20);
w2c_l51 = w2c_i0;
w2c_i0 = w2c_l50;
w2c_i1 = w2c_l51;
w2c_i0 += w2c_i1;
w2c_l52 = w2c_i0;
w2c_i0 = w2c_l52;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l53 = w2c_i0;
w2c_i0 = 255;
w2c_l54 = w2c_i0;
w2c_i0 = w2c_l53;
w2c_i1 = w2c_l54;
w2c_i0 &= w2c_i1;
w2c_l55 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l56 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 24);
w2c_l57 = w2c_i0;
w2c_i0 = w2c_l56;
w2c_i1 = w2c_l57;
w2c_i0 += w2c_i1;
w2c_l58 = w2c_i0;
w2c_i0 = w2c_l58;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l59 = w2c_i0;
w2c_i0 = 255;
w2c_l60 = w2c_i0;
w2c_i0 = w2c_l59;
w2c_i1 = w2c_l60;
w2c_i0 &= w2c_i1;
w2c_l61 = w2c_i0;
w2c_i0 = w2c_l55;
w2c_i1 = w2c_l61;
w2c_i0 += w2c_i1;
w2c_l62 = w2c_i0;
w2c_i0 = 255;
w2c_l63 = w2c_i0;
w2c_i0 = w2c_l62;
w2c_i1 = w2c_l63;
w2c_i0 &= w2c_i1;
w2c_l64 = w2c_i0;
w2c_i0 = 2;
w2c_l65 = w2c_i0;
w2c_i0 = w2c_l64;
w2c_i1 = w2c_l65;
w2c_i0 <<= (w2c_i1 & 31);
w2c_l66 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l67 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 20);
w2c_l68 = w2c_i0;
w2c_i0 = w2c_l67;
w2c_i1 = w2c_l68;
w2c_i0 += w2c_i1;
w2c_l69 = w2c_i0;
w2c_i0 = w2c_l69;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l70 = w2c_i0;
w2c_i0 = 255;
w2c_l71 = w2c_i0;
w2c_i0 = w2c_l70;
w2c_i1 = w2c_l71;
w2c_i0 &= w2c_i1;
w2c_l72 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l73 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 24);
w2c_l74 = w2c_i0;
w2c_i0 = w2c_l73;
w2c_i1 = w2c_l74;
w2c_i0 += w2c_i1;
w2c_l75 = w2c_i0;
w2c_i0 = w2c_l75;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l76 = w2c_i0;
w2c_i0 = 255;
w2c_l77 = w2c_i0;
w2c_i0 = w2c_l76;
w2c_i1 = w2c_l77;
w2c_i0 &= w2c_i1;
w2c_l78 = w2c_i0;
w2c_i0 = w2c_l72;
w2c_i1 = w2c_l78;
w2c_i0 += w2c_i1;
w2c_l79 = w2c_i0;
w2c_i0 = 255;
w2c_l80 = w2c_i0;
w2c_i0 = w2c_l79;
w2c_i1 = w2c_l80;
w2c_i0 &= w2c_i1;
w2c_l81 = w2c_i0;
w2c_i0 = 6;
w2c_l82 = w2c_i0;
w2c_i0 = w2c_l81;
w2c_i1 = w2c_l82;
w2c_i0 = (w2c_i0 >> (w2c_i1 & 31));
w2c_l83 = w2c_i0;
w2c_i0 = w2c_l66;
w2c_i1 = w2c_l83;
w2c_i0 |= w2c_i1;
w2c_l84 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l85 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 16);
w2c_l86 = w2c_i0;
w2c_i0 = w2c_l85;
w2c_i1 = w2c_l86;
w2c_i0 += w2c_i1;
w2c_l87 = w2c_i0;
w2c_i0 = w2c_l87;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l88 = w2c_i0;
w2c_i0 = 255;
w2c_l89 = w2c_i0;
w2c_i0 = w2c_l88;
w2c_i1 = w2c_l89;
w2c_i0 &= w2c_i1;
w2c_l90 = w2c_i0;
w2c_i0 = w2c_l90;
w2c_i1 = w2c_l84;
w2c_i0 ^= w2c_i1;
w2c_l91 = w2c_i0;
w2c_i0 = w2c_l87;
w2c_i1 = w2c_l91;
i32_store8((memory), (w2c_i0), w2c_i1);
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l92 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 16);
w2c_l93 = w2c_i0;
w2c_i0 = w2c_l92;
w2c_i1 = w2c_l93;
w2c_i0 += w2c_i1;
w2c_l94 = w2c_i0;
w2c_i0 = w2c_l94;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l95 = w2c_i0;
w2c_i0 = 255;
w2c_l96 = w2c_i0;
w2c_i0 = w2c_l95;
w2c_i1 = w2c_l96;
w2c_i0 &= w2c_i1;
w2c_l97 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l98 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 20);
w2c_l99 = w2c_i0;
w2c_i0 = w2c_l98;
w2c_i1 = w2c_l99;
w2c_i0 += w2c_i1;
w2c_l100 = w2c_i0;
w2c_i0 = w2c_l100;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l101 = w2c_i0;
w2c_i0 = 255;
w2c_l102 = w2c_i0;
w2c_i0 = w2c_l101;
w2c_i1 = w2c_l102;
w2c_i0 &= w2c_i1;
w2c_l103 = w2c_i0;
w2c_i0 = w2c_l97;
w2c_i1 = w2c_l103;
w2c_i0 += w2c_i1;
w2c_l104 = w2c_i0;
w2c_i0 = 255;
w2c_l105 = w2c_i0;
w2c_i0 = w2c_l104;
w2c_i1 = w2c_l105;
w2c_i0 &= w2c_i1;
w2c_l106 = w2c_i0;
w2c_i0 = 3;
w2c_l107 = w2c_i0;
w2c_i0 = w2c_l106;
w2c_i1 = w2c_l107;
w2c_i0 <<= (w2c_i1 & 31);
w2c_l108 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l109 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 16);
w2c_l110 = w2c_i0;
w2c_i0 = w2c_l109;
w2c_i1 = w2c_l110;
w2c_i0 += w2c_i1;
w2c_l111 = w2c_i0;
w2c_i0 = w2c_l111;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l112 = w2c_i0;
w2c_i0 = 255;
w2c_l113 = w2c_i0;
w2c_i0 = w2c_l112;
w2c_i1 = w2c_l113;
w2c_i0 &= w2c_i1;
w2c_l114 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l115 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 20);
w2c_l116 = w2c_i0;
w2c_i0 = w2c_l115;
w2c_i1 = w2c_l116;
w2c_i0 += w2c_i1;
w2c_l117 = w2c_i0;
w2c_i0 = w2c_l117;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l118 = w2c_i0;
w2c_i0 = 255;
w2c_l119 = w2c_i0;
w2c_i0 = w2c_l118;
w2c_i1 = w2c_l119;
w2c_i0 &= w2c_i1;
w2c_l120 = w2c_i0;
w2c_i0 = w2c_l114;
w2c_i1 = w2c_l120;
w2c_i0 += w2c_i1;
w2c_l121 = w2c_i0;
w2c_i0 = 255;
w2c_l122 = w2c_i0;
w2c_i0 = w2c_l121;
w2c_i1 = w2c_l122;
w2c_i0 &= w2c_i1;
w2c_l123 = w2c_i0;
w2c_i0 = 5;
w2c_l124 = w2c_i0;
w2c_i0 = w2c_l123;
w2c_i1 = w2c_l124;
w2c_i0 = (w2c_i0 >> (w2c_i1 & 31));
w2c_l125 = w2c_i0;
w2c_i0 = w2c_l108;
w2c_i1 = w2c_l125;
w2c_i0 |= w2c_i1;
w2c_l126 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l127 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 12);
w2c_l128 = w2c_i0;
w2c_i0 = w2c_l127;
w2c_i1 = w2c_l128;
w2c_i0 += w2c_i1;
w2c_l129 = w2c_i0;
w2c_i0 = w2c_l129;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l130 = w2c_i0;
w2c_i0 = 255;
w2c_l131 = w2c_i0;
w2c_i0 = w2c_l130;
w2c_i1 = w2c_l131;
w2c_i0 &= w2c_i1;
w2c_l132 = w2c_i0;
w2c_i0 = w2c_l132;
w2c_i1 = w2c_l126;
w2c_i0 ^= w2c_i1;
w2c_l133 = w2c_i0;
w2c_i0 = w2c_l129;
w2c_i1 = w2c_l133;
i32_store8((memory), (w2c_i0), w2c_i1);
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l134 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 12);
w2c_l135 = w2c_i0;
w2c_i0 = w2c_l134;
w2c_i1 = w2c_l135;
w2c_i0 += w2c_i1;
w2c_l136 = w2c_i0;
w2c_i0 = w2c_l136;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l137 = w2c_i0;
w2c_i0 = 255;
w2c_l138 = w2c_i0;
w2c_i0 = w2c_l137;
w2c_i1 = w2c_l138;
w2c_i0 &= w2c_i1;
w2c_l139 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l140 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 16);
w2c_l141 = w2c_i0;
w2c_i0 = w2c_l140;
w2c_i1 = w2c_l141;
w2c_i0 += w2c_i1;
w2c_l142 = w2c_i0;
w2c_i0 = w2c_l142;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l143 = w2c_i0;
w2c_i0 = 255;
w2c_l144 = w2c_i0;
w2c_i0 = w2c_l143;
w2c_i1 = w2c_l144;
w2c_i0 &= w2c_i1;
w2c_l145 = w2c_i0;
w2c_i0 = w2c_l139;
w2c_i1 = w2c_l145;
w2c_i0 += w2c_i1;
w2c_l146 = w2c_i0;
w2c_i0 = 255;
w2c_l147 = w2c_i0;
w2c_i0 = w2c_l146;
w2c_i1 = w2c_l147;
w2c_i0 &= w2c_i1;
w2c_l148 = w2c_i0;
w2c_i0 = 4;
w2c_l149 = w2c_i0;
w2c_i0 = w2c_l148;
w2c_i1 = w2c_l149;
w2c_i0 <<= (w2c_i1 & 31);
w2c_l150 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l151 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 12);
w2c_l152 = w2c_i0;
w2c_i0 = w2c_l151;
w2c_i1 = w2c_l152;
w2c_i0 += w2c_i1;
w2c_l153 = w2c_i0;
w2c_i0 = w2c_l153;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l154 = w2c_i0;
w2c_i0 = 255;
w2c_l155 = w2c_i0;
w2c_i0 = w2c_l154;
w2c_i1 = w2c_l155;
w2c_i0 &= w2c_i1;
w2c_l156 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l157 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 16);
w2c_l158 = w2c_i0;
w2c_i0 = w2c_l157;
w2c_i1 = w2c_l158;
w2c_i0 += w2c_i1;
w2c_l159 = w2c_i0;
w2c_i0 = w2c_l159;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l160 = w2c_i0;
w2c_i0 = 255;
w2c_l161 = w2c_i0;
w2c_i0 = w2c_l160;
w2c_i1 = w2c_l161;
w2c_i0 &= w2c_i1;
w2c_l162 = w2c_i0;
w2c_i0 = w2c_l156;
w2c_i1 = w2c_l162;
w2c_i0 += w2c_i1;
w2c_l163 = w2c_i0;
w2c_i0 = 255;
w2c_l164 = w2c_i0;
w2c_i0 = w2c_l163;
w2c_i1 = w2c_l164;
w2c_i0 &= w2c_i1;
w2c_l165 = w2c_i0;
w2c_i0 = 4;
w2c_l166 = w2c_i0;
w2c_i0 = w2c_l165;
w2c_i1 = w2c_l166;
w2c_i0 = (w2c_i0 >> (w2c_i1 & 31));
w2c_l167 = w2c_i0;
w2c_i0 = w2c_l150;
w2c_i1 = w2c_l167;
w2c_i0 |= w2c_i1;
w2c_l168 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 28);
w2c_l169 = w2c_i0;
w2c_i0 = w2c_l7;
w2c_i0 = i32_load((memory), (w2c_i0) + 24);
w2c_l170 = w2c_i0;
w2c_i0 = w2c_l169;
w2c_i1 = w2c_l170;
w2c_i0 += w2c_i1;
w2c_l171 = w2c_i0;
w2c_i0 = w2c_l171;
w2c_i0 = i32_load8_u((memory), (w2c_i0));
w2c_l172 = w2c_i0;
w2c_i0 = 255;
w2c_l173 = w2c_i0;
w2c_i0 = w2c_l172;
w2c_i1 = w2c_l173;
w2c_i0 &= w2c_i1;
w2c_l174 = w2c_i0;
w2c_i0 = w2c_l174;
w2c_i1 = w2c_l168;
w2c_i0 ^= w2c_i1;
w2c_l175 = w2c_i0;
w2c_i0 = w2c_l171;
w2c_i1 = w2c_l175;
i32_store8((memory), (w2c_i0), w2c_i1);
def scramble(l, i1, i2, i3, i4):
for i in range(len(l)):
memory[0x100 + i] = l[i]
f23(0x100, i1, i2, i3, i4)
for i in range(len(l)):
l[i] = memory[0x100 + i]
return l
def s(a, b, c, d):
return scramble([a, b, c, d], 0, 1, 2, 3)
from z3 import *
def us(sa, sb, sc, sd):
av, bv, cv, dv = BitVec('a', 32), BitVec('b', 32) ,BitVec('c', 32) ,BitVec('d', 32)
sav, sbv, scv, sdv = s(av, bv, cv, dv)
sol = Solver()
sol.add(sav == sa)
sol.add(sbv == sb)
sol.add(scv == sc)
sol.add(sdv == sd)
assert(sol.check() == sat)
m = sol.model()
return m[av].as_long(), m[bv].as_long(), m[cv].as_long(), m[dv].as_long()
r = us(*s(1, 2, 3, 4))
print(r)
enc = "6dbf84f73cf6a112268b09525ea550a665e21cb2e3e13af7e3ea0ecb52f5b9cda5b6522b1e978734553f1d7956d4af94bfc3f4d68c8fba9eeecf4035550b9106f70d57d1a6cdaf3211eaaa78d71a9038b71be621241e8b608a43b107f8860f543ab0189aa063800de4bae7d0b11045b8"
enc = [int(enc[i:(i+2)], 16) for i in range(0, len(enc), 2)]
ops = [
(0, 4, 8, 12),
(5, 9, 13, 1),
(10, 14, 2, 6),
(15, 3, 7, 11),
(0, 1, 2, 3),
(5, 6, 7, 4),
(10, 11, 8, 9),
(15, 12, 13, 14)
]
invops = (ops * 128)[::-1]
res = b''
for chunk in [enc[i:][:16] for i in range(0, len(enc), 16)]:
print('='*(128*8//16))
for i, op in enumerate(invops):
r = us(chunk[op[0]], chunk[op[1]], chunk[op[2]], chunk[op[3]])
chunk[op[0]] = r[0]
chunk[op[1]] = r[1]
chunk[op[2]] = r[2]
chunk[op[3]] = r[3]
if i % 16 == 0: print('.', end="", flush=True)
res += b''.join([x.to_bytes(1, "little") for x in chunk])[8:]
print()
print(res)
# a, b, c, d = BitVec('a', 32), BitVec('b', 32) ,BitVec('c', 32) ,BitVec('d', 32)
# print(scramble([a, b, c, d], 0, 1, 2, 3))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment