From the html source, we can know `cs` has the form of `[a-z]{12}`. The key space expanding to ${26}^{12}$ which makes bruteforce impossible.
We fetch the `checker.wasm` and decompile it with some traditional approaches:```shwget https://github.com/WebAssembly/wabt/releases/download/{version}/wabt-{version}-{platform}.tar.gztar zxvf wabt-{version}-{platform}.tar.gzcd wabt-{version}cp /PATH/TO/checker.wasm .bin/wasm2c checker.wasm -o checker.ccp wasm-rt-impl.c wasm-rt-impl.h wasm-rt.h```Then you can decompile it using `IDA(Pro)`:```c__int64 __fastcall w2c_checker_checker_0(unsigned int *a1, unsigned int a2, unsigned int a3){  unsigned int v5; // [rsp+18h] [rbp-118h]  unsigned int v6; // [rsp+1Ch] [rbp-114h]  unsigned int v7; // [rsp+1Ch] [rbp-114h]  unsigned int v8; // [rsp+20h] [rbp-110h]  unsigned int v9; // [rsp+20h] [rbp-110h]  unsigned int v10; // [rsp+24h] [rbp-10Ch]  unsigned int v11; // [rsp+24h] [rbp-10Ch]  unsigned int v12; // [rsp+58h] [rbp-D8h]  unsigned int v13; // [rsp+74h] [rbp-BCh]  unsigned int v14; // [rsp+78h] [rbp-B8h]  unsigned int v15; // [rsp+A0h] [rbp-90h]  char v16; // [rsp+C4h] [rbp-6Ch]  unsigned int v17; // [rsp+C8h] [rbp-68h]  int v18; // [rsp+D0h] [rbp-60h]  unsigned int v19; // [rsp+E4h] [rbp-4Ch]  unsigned int v20; // [rsp+F4h] [rbp-3Ch]  unsigned int v21; // [rsp+118h] [rbp-18h]  unsigned int v22; // [rsp+120h] [rbp-10h]  char v23; // [rsp+12Ch] [rbp-4h]
  v22 = *a1 - 32;  *a1 = v22;  i32_store(a1 + 4, v22 + 28LL, a2);  i32_store(a1 + 4, v22 + 24LL, a3);  v21 = i32_load(a1 + 4, v22 + 24LL);  i32_store(a1 + 4, v22 + 20LL, v22);  v20 = v22 - ((4 * v21 + 15) & 0xFFFFFFF0);  *a1 = v20;  i32_store(a1 + 4, v22 + 16LL, v21);  i32_store(a1 + 4, v22 + 12LL, 0LL);  while ( 1 )  {    v19 = i32_load(a1 + 4, v22 + 12LL);    if ( v19 >= (unsigned int)i32_load(a1 + 4, v22 + 24LL) )      break;    v18 = i32_load(a1 + 4, v22 + 28LL);    v17 = i32_load(a1 + 4, v22 + 12LL) + v18;    v16 = i32_load8_u(a1 + 4, v17);    v15 = 4 * i32_load(a1 + 4, v22 + 12LL) + v20;    i32_store(a1 + 4, v15, (unsigned int)(v16 - 97));    v10 = i32_load(a1 + 4, v22 + 12LL) + 1;    i32_store(a1 + 4, v22 + 12LL, v10);  }  v23 = 0;  if ( !(unsigned int)i32_load(a1 + 4, v20 + 4LL) )  {    v23 = 0;    if ( !(unsigned int)i32_load(a1 + 4, v20 + 32LL) )    {      v23 = 0;      if ( !(unsigned int)i32_load(a1 + 4, v20 + 44LL) )      {        v14 = i32_load(a1 + 4, v20);        v13 = i32_load(a1 + 4, v20 + 8LL);        v8 = i32_load(a1 + 4, v20 + 12LL);        v6 = i32_load(a1 + 4, v20 + 16LL);        v23 = 0;        if ( (w2c_checker_f1(a1, v14, v13, v8, v6) & 1) != 0 )        {          v12 = i32_load(a1 + 4, v20 + 20LL);          v11 = i32_load(a1 + 4, v20 + 24LL);          v9 = i32_load(a1 + 4, v20 + 28LL);          v7 = i32_load(a1 + 4, v20 + 36LL);          v5 = i32_load(a1 + 4, v20 + 40LL);          v23 = w2c_checker_f2(a1, v12, v11, v9, v7, v5);        }      }    }  }  i32_load(a1 + 4, v22 + 20LL);  *a1 = v22 + 32;  return v23 & 1;}_BOOL8 __fastcall w2c_checker_f1(_DWORD *a1, unsigned int a2, unsigned int a3, unsigned int a4, unsigned int a5){  int v9; // [rsp+44h] [rbp-94h]  int v10; // [rsp+4Ch] [rbp-8Ch]  int v11; // [rsp+54h] [rbp-84h]  int v12; // [rsp+7Ch] [rbp-5Ch]  int v13; // [rsp+A4h] [rbp-34h]  unsigned int v14; // [rsp+C8h] [rbp-10h]  bool v15; // [rsp+D4h] [rbp-4h]
  v14 = *a1 - 16;  i32_store(a1 + 4, v14 + 12LL, a2);  i32_store(a1 + 4, v14 + 8LL, a3);  i32_store(a1 + 4, v14 + 4LL, a4);  i32_store(a1 + 4, v14, a5);  v15 = 0;  if ( (unsigned int)i32_load(a1 + 4, v14 + 12LL) == 22 )  {    v13 = i32_load(a1 + 4, v14 + 8LL);    v15 = 0;    if ( (unsigned int)i32_load(a1 + 4, v14 + 4LL) + v13 == 30 )    {      v12 = i32_load(a1 + 4, v14 + 4LL);      v15 = 0;      if ( (unsigned int)i32_load(a1 + 4, v14) * v12 == 168 )      {        v11 = i32_load(a1 + 4, v14 + 12LL);        v10 = i32_load(a1 + 4, v14 + 8LL) + v11;        v9 = i32_load(a1 + 4, v14 + 4LL) + v10;        return (unsigned int)i32_load(a1 + 4, v14) + v9 == 66;      }    }  }  return v15;}_BOOL8 __fastcall w2c_checker_f2(        _DWORD *a1,        unsigned int a2,        unsigned int a3,        unsigned int a4,        unsigned int a5,        unsigned int a6){  int v11; // [rsp+4Ch] [rbp-154h]  int v12; // [rsp+74h] [rbp-12Ch]  int v13; // [rsp+9Ch] [rbp-104h]  int v14; // [rsp+C8h] [rbp-D8h]  int v15; // [rsp+CCh] [rbp-D4h]  int v16; // [rsp+D4h] [rbp-CCh]  int v17; // [rsp+100h] [rbp-A0h]  int v18; // [rsp+104h] [rbp-9Ch]  int v19; // [rsp+10Ch] [rbp-94h]  int v20; // [rsp+134h] [rbp-6Ch]  int v21; // [rsp+13Ch] [rbp-64h]  int v22; // [rsp+144h] [rbp-5Ch]  int v23; // [rsp+14Ch] [rbp-54h]  int v24; // [rsp+174h] [rbp-2Ch]  int v25; // [rsp+17Ch] [rbp-24h]  int v26; // [rsp+184h] [rbp-1Ch]  int v27; // [rsp+18Ch] [rbp-14h]  unsigned int v28; // [rsp+190h] [rbp-10h]  bool v29; // [rsp+19Ch] [rbp-4h]
  v28 = *a1 - 32;  i32_store(a1 + 4, v28 + 28LL, a2);  i32_store(a1 + 4, v28 + 24LL, a3);  i32_store(a1 + 4, v28 + 20LL, a4);  i32_store(a1 + 4, v28 + 16LL, a5);  i32_store(a1 + 4, v28 + 12LL, a6);  v27 = i32_load(a1 + 4, v28 + 28LL);  v26 = i32_load(a1 + 4, v28 + 24LL) + v27;  v25 = i32_load(a1 + 4, v28 + 20LL) + v26;  v24 = i32_load(a1 + 4, v28 + 16LL) + v25;  v29 = 0;  if ( (unsigned int)i32_load(a1 + 4, v28 + 12LL) + v24 == 71 )  {    v23 = i32_load(a1 + 4, v28 + 28LL);    v22 = i32_load(a1 + 4, v28 + 24LL) * v23;    v21 = i32_load(a1 + 4, v28 + 20LL) * v22;    v20 = i32_load(a1 + 4, v28 + 16LL) * v21;    v29 = 0;    if ( (unsigned int)i32_load(a1 + 4, v28 + 12LL) * v20 == 449280 )    {      v19 = i32_load(a1 + 4, v28 + 28LL);      v18 = i32_load(a1 + 4, v28 + 28LL) * v19;      v17 = i32_load(a1 + 4, v28 + 24LL);      v29 = 0;      if ( (unsigned int)i32_load(a1 + 4, v28 + 24LL) * v17 + v18 == 724 )      {        v16 = i32_load(a1 + 4, v28 + 20LL);        v15 = i32_load(a1 + 4, v28 + 20LL) * v16;        v14 = i32_load(a1 + 4, v28 + 16LL);        v29 = 0;        if ( (unsigned int)i32_load(a1 + 4, v28 + 16LL) * v14 + v15 == 313 )        {          v13 = i32_load(a1 + 4, v28 + 12LL);          v29 = 0;          if ( (unsigned int)i32_load(a1 + 4, v28 + 12LL) * v13 == 64 )          {            v12 = i32_load(a1 + 4, v28 + 28LL);            v29 = 0;            if ( (unsigned int)i32_load(a1 + 4, v28 + 20LL) + v12 == 30 )            {              v11 = i32_load(a1 + 4, v28 + 28LL);              return v11 - (unsigned int)i32_load(a1 + 4, v28 + 16LL) == 5;            }          }        }      }    }  }  return v29;}```***Or***, if you have `JEB Decompiler`:```cint checker(int param0, int param1) {    int* ptr0 = __g0 - 8;
    __g0 -= 8;    *(ptr0 + 7) = param0;    *(ptr0 + 6) = param1;    int v0 = *(ptr0 + 6);    *(ptr0 + 5) = ptr0;    int* ptr1 = (int*)((int)ptr0 - ((v0 * 4 + 15) & 0xfffffff0));    __g0 = (int)ptr0 - ((v0 * 4 + 15) & 0xfffffff0);    *(ptr0 + 4) = v0;    *(ptr0 + 3) = 0;    while((unsigned int)*(ptr0 + 3) < (unsigned int)*(ptr0 + 6)) {        *(int*)(*(ptr0 + 3) * 4 + (int)ptr1) = (int)*(char*)(*(ptr0 + 3) + *(ptr0 + 7)) - 97;        ++*(ptr0 + 3);    }
    int v1 = 0;    if(!*(ptr1 + 1)) {        v1 = 0;        if(!*(ptr1 + 8)) {            v1 = 0;            if(!*(ptr1 + 11)) {                int v2 = __f1(*(ptr1 + 4), *(ptr1 + 3), *(ptr1 + 2), *ptr1);                v1 = 0;                if((v2 & 0x1) != 0) {                    v1 = __f2(*(ptr1 + 10), *(ptr1 + 9), *(ptr1 + 7), *(ptr1 + 6), *(ptr1 + 5));                }            }        }    }
    __g0 = ptr0 + 8;    return v1 & 0x1;}int __f1(int param0, int param1, int param2, int param3) {    int* ptr0 = __g0 - 4;
    *(ptr0 + 3) = param0;    *(ptr0 + 2) = param1;    *(ptr0 + 1) = param2;    *ptr0 = param3;    int v0 = 0;    if(*(ptr0 + 3) == 22) {        v0 = 0;        if(*(ptr0 + 1) + *(ptr0 + 2) == 30) {            v0 = 0;            if(*(ptr0 + 1) * *ptr0 == 168) {                v0 = (unsigned int)(*(ptr0 + 1) + *(ptr0 + 2) + (*(ptr0 + 3) + *ptr0) == 66);            }        }    }
    return v0 & 0x1;}int __f2(int param0, int param1, int param2, int param3, int param4) {    int* ptr0 = __g0 - 8;
    *(ptr0 + 7) = param0;    *(ptr0 + 6) = param1;    *(ptr0 + 5) = param2;    *(ptr0 + 4) = param3;    *(ptr0 + 3) = param4;    int v0 = 0;    if(*(ptr0 + 3) + *(ptr0 + 4) + (*(ptr0 + 5) + *(ptr0 + 6)) + *(ptr0 + 7) == 71) {        v0 = 0;        if(*(ptr0 + 3) * *(ptr0 + 4) * (*(ptr0 + 5) * *(ptr0 + 6)) * *(ptr0 + 7) == 0x6db00) {            v0 = 0;            if(*(ptr0 + 6) * *(ptr0 + 6) + *(ptr0 + 7) * *(ptr0 + 7) == 724) {                v0 = 0;                if(*(ptr0 + 4) * *(ptr0 + 4) + *(ptr0 + 5) * *(ptr0 + 5) == 313) {                    v0 = 0;                    if(*(ptr0 + 3) * *(ptr0 + 3) == 64) {                        v0 = 0;                        if(*(ptr0 + 5) + *(ptr0 + 7) == 30) {                            v0 = (unsigned int)(*(ptr0 + 7) - *(ptr0 + 4) == 5);                        }                    }                }            }        }    }
    return v0 & 0x1;}```which seems more readable.
However, if you compare the two codes, you will noticed that they pass arguments in the opposite order(Similar reports in [a writeup](https://ctftime.org/writeup/36277#:~:text=For%20some%20reason%2C%20in%20ReWasm%2C%20parameters%20appear%20in%20the%20reverse%20order%3A)).By trying the both, it turned out that `IDA` was correct.
The constrains can then be simplified to this solve script:```pyfrom z3 import *
x = [Int(f"x_{i}") for i in range(12)]c = [i - 97 for i in x]s = Solver()s.add(    0 == c[1],    0 == c[8],    0 == c[11],    c[0] == 22,    c[3] + c[2] == 30,    c[3] * c[4] == 168,    c[3] + c[2] + c[0] + c[4] == 66,    c[10] + c[9] + (c[7] + c[6]) + c[5] == 71,    c[10] * c[9] * (c[7] * c[6]) * c[5] == 449280,    c[6] * c[6] + c[5] * c[5] == 724,    c[9] * c[9] + c[7] * c[7] == 313,    c[10] * c[10] == 64,    c[7] + c[5] == 30,    c[5] - c[9] == 5,)s.check()m = s.model()x = [m[i].as_long() for i in x]print(bytes(x))
# osu{wasmosumania}```