// ((arg_0 * 42) + (arg_1 * 1337) + arg_2) + (arg_2 ^ arg_3) + (arg_4 << 1) mod 256
var_29 = var_19 + var_25 + var_28;
return var_29 & 255;
}
```

Python equivalent:
```python
def code(n1,n2,n3,n4,n5):
var19 = ((n1 * 42) + (n2 * 1337) + n3)
var25 = n3 ^ n4
var28 = n5 << 1

return (var19+var25+var28) & 255
```

## Getting the element block values

At that point I had an idea from what to expect from the challenge and I wanted to check what byte value those weird symbols had.
This can be done by setting a break-point at the `_code` function and inspecting the var0..var4 using the Watch expression functionality of Firefox.

A similar approach was used to create the Symbol Byte Value mapping table below.

### Symbol Mapping table

| Hex Value | Image |
| -------------- | ------------------------------------ |
| d4 c2 bd 78 37 |  |
| ab a0 c2 d4 bd |  |
| 3d b3 60 b7 37 |  |
| 01 12 19 8a 31 |  |
| 05 b7 96 a3 ab |  |
| f7 a0 b3 94 77 |  |
| 8a 31 60 3d 87 |  |
| 78 37 01 12 19 |  |
| 30 78 37 01 12 |  |
| c0 8a 31 60 3d |  |

## Finding the correct order

### First try

My first approach was to brute-force all possible combinations to check if there was only one correct answer with the following code:

```python
def code(n1,n2,n3,n4,n5):
var19 = ((n1 * 42) + (n2 * 1337) + n3)
var25 = n3 ^ n4
var28 = n5 << 1

return (var19+var25+var28) & 255

def solve(name, n1, n2, n3, n4, n5):
if code(n1,n2,n3,n4,n5) == 0:
print(f"{name} n1={hex(n1)} n2={hex(n2)} n3={hex(n3)} n4={hex(n4)}, n5={hex(n5)}")

nums = [0x78, 0x37, 0x01, 0x12, 0x19,
0x8a, 0x31, 0x60, 0x3d, 0x87,
0xf7, 0xa0, 0xb3, 0x94, 0x77,
0x05, 0xb7, 0x96, 0xa3, 0xab]

#row1
for n4 in nums:
for n5 in nums:
n1 = 0xd4
n2 = 0xc2
n3 = 0xbd
solve("row1",n1,n2,n3,n4,n5)

#row2
for n2 in nums:
for n3 in nums:
for n4 in nums:
for n5 in nums:
n1 = 0x30
solve("row2",n1,n2,n3,n4,n5)

#row3
for n2 in nums:
for n3 in nums:
for n4 in nums:
for n5 in nums:
n1 = 0xc0
solve("row3",n1,n2,n3,n4,n5)

#row4
for n2 in nums:
for n3 in nums:
for n4 in nums:
for n5 in nums:
n1 = 0x60
solve("row4",n1,n2,n3,n4,n5)
#row5
for n2 in nums:
for n3 in nums:
for n4 in nums:
for n5 in nums:
n1 = 0x94
solve("row5",n1,n2,n3,n4,n5)

#col1
for n4 in nums:
for n5 in nums:
n1 = 0xd4
n2 = 0x30
n3 = 0xc0
solve("col1",n1,n2,n3,n4,n5)

#col2
for n2 in nums:
for n3 in nums:
for n4 in nums:
for n5 in nums:
n1 = 0xc2
solve("col2",n1,n2,n3,n4,n5)

#col3
for n2 in nums:
for n3 in nums:
for n4 in nums:
for n5 in nums:
n1 = 0xbd
solve("col3",n1,n2,n3,n4,n5)

#col4
for n2 in nums:
for n3 in nums:
for n4 in nums:
for n5 in nums:
n1 = 0xa0
solve("col4",n1,n2,n3,n4,n5)

#col5
for n2 in nums:
for n3 in nums:
for n4 in nums:
for n5 in nums:
n1 = 0x96
solve("col5",n1,n2,n3,n4,n5)
```

It turns out that with the exception of the col1 and row1, the other columns and rows had multiple possible solutions when using a pure brute-force approach without restricting that a value can be used only once.

Output:
```console
➜ dice-is-for-you python solve.py | cut -d " " -f 1 | sort | uniq -c
1 col1
601 col2
527 col3
789 col4
882 col5
1 row1
637 row2
740 row3
850 row4
728 row5
```

### Z3 FTW

My next approach was to use the Z3 SMT Solver to solve the `"sudoku like"` board with our rules and constraints.

```python
from z3 import *

nums = [0x78, 0x37, 0x01, 0x12, 0x19,
0x8a, 0x31, 0x60, 0x3d, 0x87,
0xf7, 0xa0, 0xb3, 0x94, 0x77,
0x05, 0xb7, 0x96, 0xa3, 0xab,
0xd4, 0xc2, 0xbd, 0x30, 0xc0]

def code(n1,n2,n3,n4,n5):
var19 = ((n1 * 42) + (n2 * 1337) + n3)
var25 = n3 ^ n4
var28 = n5 << 1

return (var19+var25+var28) & 255

"""
c00 c01 c02 c03 c04
c10 c11 c12 c13 c14
c20 c21 c22 c23 c24
c30 c31 c32 c33 c34
c40 c41 c42 c43 c44
"""

M = [[
BitVec(f"c{row}{col}",8)
for col in range(5)]
for row in range(5)]

s = Solver()
for row in M:
n1,n2,n3,n4,n5 = row
s.add(code(n1,n2,n3,n4,n5) == 0)

for col in zip(*M):
n1,n2,n3,n4,n5 = col
s.add(code(n1,n2,n3,n4,n5) == 0)

s.add(M[0][0] == 0xd4)
s.add(M[0][1] == 0xc2)
s.add(M[0][2] == 0xbd)
s.add(M[1][0] == 0x30)
s.add(M[2][0] == 0xc0)

s.add(Distinct(
[ M[row][col]
for col in range(5)
for row in range(5)]
))

for row in range(5):
for col in range(5):
block = []

for n in nums:
block.append(M[row][col] == n)

s.add(Or(block))

print(s.check())
print(s.model())
if s.check():
m = s.model()
print(m)
for row in range(5):
for col in range(5):
x = m[M[row][col]]
print(hex(int(x.as_string())), end=" ")
print()
```

### Output

```
0xd4 0xc2 0xbd 0xa0 0x96
0x30 0xf7 0x87 0x01 0x8a
0xc0 0xb3 0x77 0xb7 0x37
0x60 0xab 0x19 0x3d 0x78
0x94 0x31 0x05 0xa3 0x12
```

## Final board and flag

Now it was only a matter of using the Symbol Mapping table to get the flag


Flag:
`dice{d1ce_1s_y0u_is_th0nk_73da6}`

## Final Notes

The DiceCTF was fun with some very cool challenges, looking forward next editions of this CTF. :-)
Only 19 teams solved this challenge, I wonder if that is related to the tooling for debugging WebAssembly code.

### WebAssembly Debbuging Tooling

Although this write-up shows a linear approach to solved this challenge, my approach during the competition was not that straightforward.

At first, I tried to use Chromium to debug the wasm code. Which would not allow me to insert breakpoints with the following error message:

Which later I discovered that I could enable the WebAssembly Debugging: Enable DWARF support as a workaround.

I changed between Chrome and Firefox multiple times and it seems each of them has advantages and disadvantages for debugging WebAssembly.

One really cool feature present in Chrome that I don't think is present in Firefox is the ability to show the internal stack variables.

Meanwhile Firefox exposes the internal WebAssembly memory as variable `memory0` while on Chrome I had to open the dev tools, insert a breakpoint, go to `Module` -> `env-memory` -> `store object as global variable`