# Smart Solver solved without SMT and Z3
Well the heading is intentional since I did not know about SMT and Z3 when I solved this problem during the CTF, and solved it logically. So read this if you are interested in a logical solution to the problem.

# Overview

The binary that we are provided uses a lot of instructions to compare each character of a string with all other characters of the string, if any of the test fails it just jumps to a location that exits. So we have to find that string which passes all tests.

# Observations
- The string length is `73`
- The operations compare the numeric value of characters with each other so it defines a lexographic order for a character with all other characters of the string.

# Idea

Given a string with 73 characters `s[73]`, Consider a `73 X 73` 2-d array `a[73][73]`. Define `a[i][j]` in the following manner -:
```
if(s[i] == s[j]):
a[i][j] = -1
elif(s[i] < s[j]):
a[i][j] = 0
else:
a[i][j] = 1
```

Now note that we can obtain the entire 2-d array `a` from the binary if we are able to parse the instructions in the disassembled code of the binary. This is because each character is compared with a number of other characters using either the `jbe` or `jae` instruction and if it is not compared with some character then it is safe to assume that both of them are equal, since no other possibility exists.

## Code to parse the binary and get the 2-d array

### Some debugging aids which can be safely ignored
The code includes some `try-except` and `assert` statements to verify that what we are doing is right. The variable `ct` is the error counter. The code throws one error at an instruction before the comparisons are even started so `ct` is not allowed to be greater than 1.

```
import re
import json
import sys
a=[[-1 for i in range(73)] for i in range(73)]

def dump_data():
# Objective a[i][j] = 0 if s[i] < s[j] , 1 if(s[i] > s[j]), -1 if (s[i] == s[j])

regex = '.*movzx e([ad])x,BYTE PTR \[rbp-(0x[0-9a-f]*)\].*' # regex to match src and dest
jmp_reg = '.*j([ab])e.*' # regex to match operator (less or greater)

src,dst=-1,-1
ct=0
with open("disassembly",'r') as f:
for line in f.readlines():
# print(line)
try:
reg, pos = re.match(regex, line).groups()
pos = int(pos, 16) - 0xd8

if(reg == 'd'):
assert src == -1
src = pos
print("Setting src to ",pos)
elif(reg == 'a'):
assert dst == -1
dst = pos
print("Setting dst to ", pos)


except Exception as e:

if isinstance(e, AssertionError):
ct += 1
print(src, dst)
print(line)
if(ct>1):
sys.exit(-1)
try:
oper = re.match(jmp_reg, line).groups()[0]
assert src != -1 and dst != -1 and a[src][dst] == -1
if oper == 'b':
print("oper is b")
a[src][dst] = 0
else:
print("Oper is a")
a[src][dst] = 1
src, dst = -1, -1
except Exception as e:
if isinstance(e,AssertionError):
ct += 1
print(src, dst)
print(line)
if(ct > 1):
sys.exit(-1)


open("out", 'w').write(json.dumps(a))
```

# Reversing the 2-d array to obtain flag
So now we have `a[73][73]`. How to obtain the string `s[73]` from this 2-d array. So the idea is this, we can first group indices that map to the same character i.e indexes `x` and `y` belong to the same group if `s[x][y] == -1 == s[y][x]`.

**Note:** We do not need to ensure the second condition since that is a problem constraint and it cannot fail otherwise the data would be wrong. So what I mean is that for data to be correct the following invariant needs to be satisfied
```
s[i][j] = ~s[j][i] if (s[i][j] != -1) else s[i][j] == -1 == s[j][i]
```

- Once we have grouped the characters we know that characters at indices in the same group are same.
- Also note that suppose for an index `i` we can compute `less_ct[i] = count({j: s[i][j] == 0})`, `gt_ct[i] = count({j: s[i][j] == 1})` and `eq_ct[i] = count({j: a[i][j] == 0})` . `less_ct[i]` is a count of the number of characters which are lexographically **larger** than `s[i]`.
- Now suppose character indices `i1, i2, i3` belong to a group `G` i.e they map to same character. So they will have the same values of these quantities since the character comparison will yield equivalent results. So the variables `less_ct, gt_ct` are indeed a characterstic of the group and not of a particular index.
- Now suppose a group is mapped to the character `'b'`. How will its `less_ct` compare to the group that maps to the character `'c'`? It is obvious that the number of characters that are lexographically larger than `'c'` are less than the number of characters that are lexographically larger than `'b'` since the latter set will also include the characters that are equal to `'c'`.
- So it is convincing enough that if we sort these groups on the basis of `less_ct` and start assigning them the characters from `'a'` we could complete the entire string.

**Note:** We have made an assumption that all characters from `'a'` to `'z'` are being used. And this assumption only holds true if the number of groups that we are able to form are >= 26. In our case we got 28 groups i.e. all 26 alpahabets and `'{'` and `'}'`

## Code to obtain string from 2-d array

**Note:** It seemed like that we need to reverse the flag after obtaining the entire string to have the format `flag{...}`
```
def rev():
data=json.loads(open('out','r').read())
ingroup = [False for i in range(73)]

groups=[]

for i in range(73):
if(ingroup[i]):
continue
ele = data[i]
eq_ct,less_ct,gt_ct=0,0,0
same_indexes = []
for j in range(73):
b=ele[j]
if b==-1:
eq_ct+=1
same_indexes.append(j)
ingroup[j] = True
elif (b==0):
less_ct+=1
else:
gt_ct+=1
groups.append({"eq_ct":eq_ct,"less_ct":less_ct,"gt_ct":gt_ct,"same_indexes":same_indexes})
groups.sort(key=lambda x: x['less_ct'])
flag=['' for i in range(73)]
for i in range(len(groups)):
c = chr(ord('a')+i) if(i!=len(groups)-1) else '}'
group = groups[i]
for index in group['same_indexes']:
flag[index] = c
flag="".join(flag)[::-1]
print(flag)
```

# Result
`flag{thequickbrownfoxjumpedoverthelazydogandlearnedhowtoautomateanalysis}`