Hacker handle: 0xc3

# Notes
The addresses I give here are as shown in Ghidra; `angr` loads the binary at `0x400000` instead of at `0x100000`.

## Execution instructions / description of files
- `solve_determine_phobos.py`: contains code that computes the constraints for valid Phobi. When run, outputs `phobos.out`.
- `solve_check_phobos.py`: contains code that computes the constraints for meaningful (i.e. Phobos-having) words. When run, outputs a few of them on stdout.
- `find_words_with_phobos.py`: contains code that runs `./Stone` with many different valid word inputs to find words that have Phobi. Outputs them.
- `codec.py`: Converts between word/phobos representations
- `README.md`: You're reading it!
- `phobos.out`: contains phobos-word pairs
- `README_MBF.md`, `solve_5b.py`, `angr_mbf`, `hellas.mbf`: see `README_MBF.md`.

## Part 1
Part 1 indicates we need to do some analysis; we'll open the program in Ghidra to have a look.

The main function is easily found at `0x101060`. It consists of three paths:

1. Not enough arguments have been given.
2. A word attempt is given but is invalid
3. A valid word is given and it has the following phobos.
4. A valid word is given but it has no meaning.

The function `validate_and_process_word` at `0x1012b0` distinguishes between cases 2-4, and gives a word's phobos (if it has one). It takes an out-param to store this in (a `char[14]` containing 14 hex digits) and an in-param, the word attempt.

If we look at the end of the function, we see a label (`end_invalid`) which is jumped to in case a word is invalid; in this case the return value is `-1`. There is a while loop at the top of the function that processes the given word and in some paths jumps to this label, so this is probably the part that validates a word.

The Ghidra decompilation is fairly messy and doesn't show what happens that well; looking at the disassembly and stepping through using a debugger gives more insight. The requirements are: a word needs to be 16 characters long and consist of characters in `[@A-FHJ-NP-RT-Y0-9]` to be valid.

Writing a script (`find_words_with_phobos.py`) that checks all valid words one-by-one we easily find words with Phobi: the word "AAAAAAAAAAAAAAAB" has phobos "00000000040000", for instance.

### Internal representation

A word is expanded into a 5-byte-per-character form, where the bytes are each of the bits of the character's index into the alphabet; i.e. 'A' is `0x0000000001` and '5' is `0x0101000101`.

If the word is valid, the code performs another check, calling `0x101220` (`check_has_phobos`). If the first byte of the result is zero, the code gets the phobos (a call to `0x1046b0`, `get_phobos`), converts it to a hexadecimal representation, and returns.

The phobos as returned by `get_phobos` is in a similar one-bit-per-byte representation and is 56 bytes long, and is compacted into a hex string by turning 8 bytes into two hex digits. In total this yields 14 hex digits giving us a phobos.

Conversions to and from these representations can be found in `codec.py`.

## Part 2
The code at `0x101220` checks whether a word has a Phobos. The symbolic execution script that gets the constraints on the word can be found in `solve_check_has_phobos.py`. It runs the function, setting some input parameters, then adds the `al == 0` constraint when the simulation reaches the end of the function and solves for inputs that satisfy that constraint.

At first I attempted to run the code as-is, providing an array of 80 bytes which were constrained to be 1 or 0, but when running this under `angr` it quickly gets out of hand; the number of states generated by the `if` statements is just too much to deal with, and the assignment does talk about bypassing decoding steps, so I ended up solving it differently.

My eventual solution hooks `0x101242`, skipping the whole decoding nonsense and simply setting `al` to the next 'decoded' byte each loop iteration. This strategy evades state explosion, and calling `sim.explore()` with `find=base + 0x12a0` (the address of the `ret` instruction) now completes quickly.
To the solver of the found state we add the constraint that `al` must equal `0`. Solving for the inputs that satisfy that constraint then yields inputs which correspond to words that have meaning. `solve_check_phobos.py` then ends by printing some of these words.

## Part 3/4
The code at `0x1046b0` computes the Phobos for a given word.

`solve_determine_phobos.py` contains code that gets the constraints for valid Phobi, and when run generates `phobos.out` by solving the constraints to get a list of valid Phobi and then solving for a word that satisfies that Phobos.

To get the constraints on Phobi, we re-use a bunch of code from `solve_check_has_phobos.py`, with slight modifications. We start by getting the constraints for valid words, doing basically what `solve_check_has_phobos.py` does except we also store the IR variables in an expanded state.
Once the `check_has_phobos` function has run, we want to run the algorithm that computes a phobos. This takes a place to put the phobos as an out-param, and a pointer to the expanded word IR as an in-param. We store the (symbolic) expanded word IR in memory and pass a pointer to it in `rsi`, and we set `rip` to `0x1046b0`.
We also hook `0x1046f0`, which would ordinarily store the computed bit of the phobos in memory, and we save that computed bit in a list instead. We can later solve for those bits to get the possible Phobi.