# atari-proofs
The goal of this project is to formally prove a lower bound on the time it takes to beat the game [*Dragster*](https://en.wikipedia.org/wiki/Dragster_(video_game)).
Here is the plan:
- Implement a partial Atari 2600 emulator in [Coq](https://coq.inria.fr/).
- Connect it to the [Iris](https://iris-project.org/) separation logic framework.
    - Documentation is sparse, but an explanation of how to define a language can be found [here](https://github.com/tchajed/iris-simp-lang).
    - Iris can be used for assembly code — see [this project](https://github.com/logsem/cerise-stack).
- Along the way, do some toy proofs. For example, prove that `LABEL: JMP LABEL` does not affect memory.
- Attempt to prove a useful lower bound for Dragster.
    - The final theorem should not mention the Iris logic. It should look something like this:
        - In any reachable state, if RAM location 0b0000000 is nonzero, some function of RAM locations 0b0110011, 0b0110101, and 0b0110111 is greater than some number.
            - Yes, there's only 128 bytes of RAM!
    - Due to *Dragster*'s history, it will be interesting to see whether I can prove a bound greater than 5.51 seconds, or not.

.git
.DS_Store